| Name | 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 | |
| (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 | |
| Best CPU time to get the best result obtained on this benchmark | |
| 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 |
LAUNCH ON wulflinc12 THE 2005-09-20 02:54:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3197 boxname=wulflinc12 idbench=853 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4a697c297ecbc7d83b192d907b1ba64c /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-seba.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-seba.opb IDLAUNCH: 3197 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 908800 kB Buffers: 33272 kB Cached: 61844 kB SwapCached: 492 kB Active: 44520 kB Inactive: 53184 kB HighTotal: 131008 kB HighFree: 67004 kB LowTotal: 903652 kB LowFree: 841796 kB SwapTotal: 2097136 kB SwapFree: 2096072 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5884 kB Slab: 22396 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:14:38 (client local time) WITH STATUS 0 IN 1208.13 SECONDS stats: 3197 7 1208.13 0
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 % |
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/11233/stat): 11233 (minisat+_script) R 11232 11233 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796854549 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/11233/statm): 174 3 169 147 0 27 0 [pid=11233] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=11234 New process pid=11235 New process pid=11236 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 One traced child (pid=11235) exited with status: 0 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=11236) exited with status: 0 One traced child (pid=11234) exited with status: 0 New process pid=11237 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-seba.opb [startup+10.0037 s] Raw data (loadavg): 0.94 0.90 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 3567 0 0 0 963 17 0 0 25 0 1 0 1796854555 14852096 3205 4294967295 134512640 135094434 3221224432 3221221180 134676331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 3626 3205 145 145 0 3481 0 [pid=11237] vsize: 14504 Current children cumulated CPU time (s) 9.81 Current children cumulated vsize (Kb) 16628 [startup+20.0045 s] Raw data (loadavg): 0.95 0.90 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 14780 0 0 0 1881 63 0 0 22 0 1 0 1796854555 59080704 13414 4294967295 134512640 135094434 3221224432 3221221392 134553669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 14424 13414 145 145 0 14279 0 [pid=11237] vsize: 57696 Current children cumulated CPU time (s) 19.45 Current children cumulated vsize (Kb) 59820 [startup+30.0054 s] Raw data (loadavg): 0.96 0.91 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29413 0 0 0 2755 123 0 0 25 0 1 0 1796854555 135815168 28047 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33158 28047 145 145 0 33013 0 [pid=11237] vsize: 132632 Current children cumulated CPU time (s) 28.79 Current children cumulated vsize (Kb) 134756 [startup+40.0062 s] Raw data (loadavg): 0.96 0.91 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29524 0 0 0 3754 124 0 0 25 0 1 0 1796854555 136122368 28158 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33233 28158 145 145 0 33088 0 [pid=11237] vsize: 132932 Current children cumulated CPU time (s) 38.79 Current children cumulated vsize (Kb) 135056 [startup+50.007 s] Raw data (loadavg): 0.97 0.91 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29565 0 0 0 4754 124 0 0 25 0 1 0 1796854555 136261632 28199 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33267 28199 145 145 0 33122 0 [pid=11237] vsize: 133068 Current children cumulated CPU time (s) 48.79 Current children cumulated vsize (Kb) 135192 [startup+60.0078 s] Raw data (loadavg): 0.97 0.91 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29589 0 0 0 5754 124 0 0 25 0 1 0 1796854555 136351744 28223 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33289 28223 145 145 0 33144 0 [pid=11237] vsize: 133156 Current children cumulated CPU time (s) 58.79 Current children cumulated vsize (Kb) 135280 [startup+70.0087 s] Raw data (loadavg): 0.98 0.92 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29600 0 0 0 6754 124 0 0 25 0 1 0 1796854555 136396800 28234 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33300 28234 145 145 0 33155 0 [pid=11237] vsize: 133200 Current children cumulated CPU time (s) 68.79 Current children cumulated vsize (Kb) 135324 [startup+80.0095 s] Raw data (loadavg): 0.98 0.92 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29624 0 0 0 7754 124 0 0 25 0 1 0 1796854555 136507392 28258 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33327 28258 145 145 0 33182 0 [pid=11237] vsize: 133308 Current children cumulated CPU time (s) 78.79 Current children cumulated vsize (Kb) 135432 [startup+90.0104 s] Raw data (loadavg): 0.98 0.92 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29634 0 0 0 8754 125 0 0 25 0 1 0 1796854555 136536064 28268 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33334 28268 145 145 0 33189 0 [pid=11237] vsize: 133336 Current children cumulated CPU time (s) 88.8 Current children cumulated vsize (Kb) 135460 [startup+100.011 s] Raw data (loadavg): 0.98 0.92 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29660 0 0 0 9754 125 0 0 25 0 1 0 1796854555 136622080 28294 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33355 28294 145 145 0 33210 0 [pid=11237] vsize: 133420 Current children cumulated CPU time (s) 98.8 Current children cumulated vsize (Kb) 135544 [startup+110.012 s] Raw data (loadavg): 0.99 0.92 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29680 0 0 0 10754 125 0 0 25 0 1 0 1796854555 136732672 28314 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33382 28314 145 145 0 33237 0 [pid=11237] vsize: 133528 Current children cumulated CPU time (s) 108.8 Current children cumulated vsize (Kb) 135652 [startup+120.013 s] Raw data (loadavg): 0.99 0.93 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29683 0 0 0 11754 125 0 0 25 0 1 0 1796854555 136744960 28317 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33385 28317 145 145 0 33240 0 [pid=11237] vsize: 133540 Current children cumulated CPU time (s) 118.8 Current children cumulated vsize (Kb) 135664 [startup+130.014 s] Raw data (loadavg): 0.99 0.93 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29693 0 0 0 12754 125 0 0 25 0 1 0 1796854555 136781824 28327 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33394 28327 145 145 0 33249 0 [pid=11237] vsize: 133576 Current children cumulated CPU time (s) 128.8 Current children cumulated vsize (Kb) 135700 [startup+140.015 s] Raw data (loadavg): 0.99 0.93 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29748 0 0 0 13753 125 0 0 25 0 1 0 1796854555 136998912 28382 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33447 28382 145 145 0 33302 0 [pid=11237] vsize: 133788 Current children cumulated CPU time (s) 138.79 Current children cumulated vsize (Kb) 135912 [startup+150.015 s] Raw data (loadavg): 0.99 0.93 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29773 0 0 0 14753 126 0 0 25 0 1 0 1796854555 137097216 28407 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33471 28407 145 145 0 33326 0 [pid=11237] vsize: 133884 Current children cumulated CPU time (s) 148.8 Current children cumulated vsize (Kb) 136008 [startup+160.015 s] Raw data (loadavg): 0.99 0.93 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29845 0 0 0 15751 126 0 0 25 0 1 0 1796854555 137388032 28479 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33542 28479 145 145 0 33397 0 [pid=11237] vsize: 134168 Current children cumulated CPU time (s) 158.78 Current children cumulated vsize (Kb) 136292 [startup+170.016 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29881 0 0 0 16751 126 0 0 25 0 1 0 1796854555 137527296 28515 4294967295 134512640 135094434 3221224432 3221223056 134557655 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33576 28515 145 145 0 33431 0 [pid=11237] vsize: 134304 Current children cumulated CPU time (s) 168.78 Current children cumulated vsize (Kb) 136428 [startup+180.016 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29904 0 0 0 17750 127 0 0 25 0 1 0 1796854555 137621504 28538 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33599 28538 145 145 0 33454 0 [pid=11237] vsize: 134396 Current children cumulated CPU time (s) 178.78 Current children cumulated vsize (Kb) 136520 [startup+190.017 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29957 0 0 0 18750 127 0 0 25 0 1 0 1796854555 137891840 28591 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33665 28591 145 145 0 33520 0 [pid=11237] vsize: 134660 Current children cumulated CPU time (s) 188.78 Current children cumulated vsize (Kb) 136784 [startup+200.018 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 29990 0 0 0 19749 127 0 0 25 0 1 0 1796854555 138022912 28624 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33697 28624 145 145 0 33552 0 [pid=11237] vsize: 134788 Current children cumulated CPU time (s) 198.77 Current children cumulated vsize (Kb) 136912 [startup+210.017 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30034 0 0 0 20749 128 0 0 25 0 1 0 1796854555 138199040 28668 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33740 28668 145 145 0 33595 0 [pid=11237] vsize: 134960 Current children cumulated CPU time (s) 208.78 Current children cumulated vsize (Kb) 137084 [startup+220.018 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30082 0 0 0 21748 128 0 0 25 0 1 0 1796854555 138391552 28716 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33787 28716 145 145 0 33642 0 [pid=11237] vsize: 135148 Current children cumulated CPU time (s) 218.77 Current children cumulated vsize (Kb) 137272 [startup+230.019 s] Raw data (loadavg): 0.99 0.94 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30158 0 0 0 22746 129 0 0 25 0 1 0 1796854555 138698752 28792 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33862 28792 145 145 0 33717 0 [pid=11237] vsize: 135448 Current children cumulated CPU time (s) 228.76 Current children cumulated vsize (Kb) 137572 [startup+240.02 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30224 0 0 0 23745 129 0 0 25 0 1 0 1796854555 138964992 28858 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33927 28858 145 145 0 33782 0 [pid=11237] vsize: 135708 Current children cumulated CPU time (s) 238.75 Current children cumulated vsize (Kb) 137832 [startup+250.021 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30284 0 0 0 24745 130 0 0 25 0 1 0 1796854555 139206656 28918 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 33986 28918 145 145 0 33841 0 [pid=11237] vsize: 135944 Current children cumulated CPU time (s) 248.76 Current children cumulated vsize (Kb) 138068 [startup+260.021 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30364 0 0 0 25743 130 0 0 25 0 1 0 1796854555 139530240 28998 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34065 28998 145 145 0 33920 0 [pid=11237] vsize: 136260 Current children cumulated CPU time (s) 258.74 Current children cumulated vsize (Kb) 138384 [startup+270.021 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30442 0 0 0 26742 131 0 0 25 0 1 0 1796854555 139845632 29076 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34142 29076 145 145 0 33997 0 [pid=11237] vsize: 136568 Current children cumulated CPU time (s) 268.74 Current children cumulated vsize (Kb) 138692 [startup+280.022 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30458 0 0 0 27742 131 0 0 25 0 1 0 1796854555 139907072 29092 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34157 29092 145 145 0 34012 0 [pid=11237] vsize: 136628 Current children cumulated CPU time (s) 278.74 Current children cumulated vsize (Kb) 138752 [startup+290.024 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30482 0 0 0 28742 131 0 0 25 0 1 0 1796854555 140001280 29116 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34180 29116 145 145 0 34035 0 [pid=11237] vsize: 136720 Current children cumulated CPU time (s) 288.74 Current children cumulated vsize (Kb) 138844 [startup+300.025 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30521 0 0 0 29742 131 0 0 25 0 1 0 1796854555 140156928 29155 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34218 29155 145 145 0 34073 0 [pid=11237] vsize: 136872 Current children cumulated CPU time (s) 298.74 Current children cumulated vsize (Kb) 138996 [startup+310.025 s] Raw data (loadavg): 0.99 0.95 0.92 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30563 0 0 0 30741 132 0 0 25 0 1 0 1796854555 140324864 29197 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34259 29197 145 145 0 34114 0 [pid=11237] vsize: 137036 Current children cumulated CPU time (s) 308.74 Current children cumulated vsize (Kb) 139160 [startup+320.026 s] Raw data (loadavg): 1.07 0.97 0.93 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30610 0 0 0 31740 133 0 0 25 0 1 0 1796854555 140513280 29244 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34305 29244 145 145 0 34160 0 [pid=11237] vsize: 137220 Current children cumulated CPU time (s) 318.74 Current children cumulated vsize (Kb) 139344 [startup+330.025 s] Raw data (loadavg): 1.06 0.97 0.93 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30686 0 0 0 32739 133 0 0 25 0 1 0 1796854555 140951552 29320 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34412 29320 145 145 0 34267 0 [pid=11237] vsize: 137648 Current children cumulated CPU time (s) 328.73 Current children cumulated vsize (Kb) 139772 [startup+340.026 s] Raw data (loadavg): 1.05 0.97 0.93 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30701 0 0 0 33739 133 0 0 25 0 1 0 1796854555 141008896 29335 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34426 29335 145 145 0 34281 0 [pid=11237] vsize: 137704 Current children cumulated CPU time (s) 338.73 Current children cumulated vsize (Kb) 139828 [startup+350.027 s] Raw data (loadavg): 1.12 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30759 0 0 0 34739 133 0 0 25 0 1 0 1796854555 141246464 29393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34484 29393 145 145 0 34339 0 [pid=11237] vsize: 137936 Current children cumulated CPU time (s) 348.73 Current children cumulated vsize (Kb) 140060 [startup+360.027 s] Raw data (loadavg): 1.10 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30829 0 0 0 35738 134 0 0 25 0 1 0 1796854555 141529088 29463 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34553 29463 145 145 0 34408 0 [pid=11237] vsize: 138212 Current children cumulated CPU time (s) 358.73 Current children cumulated vsize (Kb) 140336 [startup+370.028 s] Raw data (loadavg): 1.09 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30903 0 0 0 36736 134 0 0 25 0 1 0 1796854555 141828096 29537 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34626 29537 145 145 0 34481 0 [pid=11237] vsize: 138504 Current children cumulated CPU time (s) 368.71 Current children cumulated vsize (Kb) 140628 [startup+380.029 s] Raw data (loadavg): 1.07 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 30997 0 0 0 37734 136 0 0 25 0 1 0 1796854555 142209024 29631 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34719 29631 145 145 0 34574 0 [pid=11237] vsize: 138876 Current children cumulated CPU time (s) 378.71 Current children cumulated vsize (Kb) 141000 [startup+390.03 s] Raw data (loadavg): 1.06 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31062 0 0 0 38733 137 0 0 25 0 1 0 1796854555 142471168 29696 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 34783 29696 145 145 0 34638 0 [pid=11237] vsize: 139132 Current children cumulated CPU time (s) 388.71 Current children cumulated vsize (Kb) 141256 [startup+400.031 s] Raw data (loadavg): 1.05 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31158 0 0 0 39731 138 0 0 25 0 1 0 1796854555 142856192 29792 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 34877 29792 145 145 0 34732 0 [pid=11237] vsize: 139508 Current children cumulated CPU time (s) 398.7 Current children cumulated vsize (Kb) 141632 [startup+410.032 s] Raw data (loadavg): 1.04 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31278 0 0 0 40727 140 0 0 25 0 1 0 1796854555 143343616 29912 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 34996 29912 145 145 0 34851 0 [pid=11237] vsize: 139984 Current children cumulated CPU time (s) 408.68 Current children cumulated vsize (Kb) 142108 [startup+420.034 s] Raw data (loadavg): 1.04 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31358 0 0 0 41725 140 0 0 25 0 1 0 1796854555 143663104 29992 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 35074 29992 145 145 0 34929 0 [pid=11237] vsize: 140296 Current children cumulated CPU time (s) 418.66 Current children cumulated vsize (Kb) 142420 [startup+430.034 s] Raw data (loadavg): 1.03 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31497 0 0 0 42723 141 0 0 25 0 1 0 1796854555 144228352 30131 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35212 30131 145 145 0 35067 0 [pid=11237] vsize: 140848 Current children cumulated CPU time (s) 428.65 Current children cumulated vsize (Kb) 142972 [startup+440.036 s] Raw data (loadavg): 1.02 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31605 0 0 0 43720 143 0 0 25 0 1 0 1796854555 144666624 30239 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35319 30239 145 145 0 35174 0 [pid=11237] vsize: 141276 Current children cumulated CPU time (s) 438.64 Current children cumulated vsize (Kb) 143400 [startup+450.036 s] Raw data (loadavg): 1.02 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31724 0 0 0 44717 144 0 0 25 0 1 0 1796854555 145145856 30358 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35436 30358 145 145 0 35291 0 [pid=11237] vsize: 141744 Current children cumulated CPU time (s) 448.62 Current children cumulated vsize (Kb) 143868 [startup+460.037 s] Raw data (loadavg): 1.02 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31826 0 0 0 45715 146 0 0 25 0 1 0 1796854555 145559552 30460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35537 30460 145 145 0 35392 0 [pid=11237] vsize: 142148 Current children cumulated CPU time (s) 458.62 Current children cumulated vsize (Kb) 144272 [startup+470.039 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31909 0 0 0 46713 147 0 0 25 0 1 0 1796854555 145895424 30543 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35619 30543 145 145 0 35474 0 [pid=11237] vsize: 142476 Current children cumulated CPU time (s) 468.61 Current children cumulated vsize (Kb) 144600 [startup+480.04 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 31964 0 0 0 47712 147 0 0 25 0 1 0 1796854555 146116608 30598 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35673 30598 145 145 0 35528 0 [pid=11237] vsize: 142692 Current children cumulated CPU time (s) 478.6 Current children cumulated vsize (Kb) 144816 [startup+490.042 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32041 0 0 0 48711 148 0 0 25 0 1 0 1796854555 146427904 30675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35749 30675 145 145 0 35604 0 [pid=11237] vsize: 142996 Current children cumulated CPU time (s) 488.6 Current children cumulated vsize (Kb) 145120 [startup+500.043 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32101 0 0 0 49709 149 0 0 25 0 1 0 1796854555 146677760 30735 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35810 30735 145 145 0 35665 0 [pid=11237] vsize: 143240 Current children cumulated CPU time (s) 498.59 Current children cumulated vsize (Kb) 145364 [startup+510.043 s] Raw data (loadavg): 1.01 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32168 0 0 0 50707 150 0 0 25 0 1 0 1796854555 146952192 30802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35877 30802 145 145 0 35732 0 [pid=11237] vsize: 143508 Current children cumulated CPU time (s) 508.58 Current children cumulated vsize (Kb) 145632 [startup+520.044 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32237 0 0 0 51705 151 0 0 25 0 1 0 1796854555 147230720 30871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 35945 30871 145 145 0 35800 0 [pid=11237] vsize: 143780 Current children cumulated CPU time (s) 518.57 Current children cumulated vsize (Kb) 145904 [startup+530.046 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32300 0 0 0 52704 152 0 0 25 0 1 0 1796854555 147480576 30934 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36006 30934 145 145 0 35861 0 [pid=11237] vsize: 144024 Current children cumulated CPU time (s) 528.57 Current children cumulated vsize (Kb) 146148 [startup+540.048 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32339 0 0 0 53703 153 0 0 25 0 1 0 1796854555 147636224 30973 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36044 30973 145 145 0 35899 0 [pid=11237] vsize: 144176 Current children cumulated CPU time (s) 538.57 Current children cumulated vsize (Kb) 146300 [startup+550.049 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32382 0 0 0 54701 154 0 0 25 0 1 0 1796854555 147808256 31016 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36086 31016 145 145 0 35941 0 [pid=11237] vsize: 144344 Current children cumulated CPU time (s) 548.56 Current children cumulated vsize (Kb) 146468 [startup+560.05 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32435 0 0 0 55700 155 0 0 25 0 1 0 1796854555 148021248 31069 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36138 31069 145 145 0 35993 0 [pid=11237] vsize: 144552 Current children cumulated CPU time (s) 558.56 Current children cumulated vsize (Kb) 146676 [startup+570.052 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32492 0 0 0 56698 155 0 0 25 0 1 0 1796854555 148250624 31126 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36194 31126 145 145 0 36049 0 [pid=11237] vsize: 144776 Current children cumulated CPU time (s) 568.54 Current children cumulated vsize (Kb) 146900 [startup+580.052 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32583 0 0 0 57696 157 0 0 25 0 1 0 1796854555 148619264 31217 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36284 31217 145 145 0 36139 0 [pid=11237] vsize: 145136 Current children cumulated CPU time (s) 578.54 Current children cumulated vsize (Kb) 147260 [startup+590.054 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32619 0 0 0 58694 158 0 0 25 0 1 0 1796854555 148762624 31253 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36319 31253 145 145 0 36174 0 [pid=11237] vsize: 145276 Current children cumulated CPU time (s) 588.53 Current children cumulated vsize (Kb) 147400 [startup+600.056 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32675 0 0 0 59693 159 0 0 25 0 1 0 1796854555 148983808 31309 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36373 31309 145 145 0 36228 0 [pid=11237] vsize: 145492 Current children cumulated CPU time (s) 598.53 Current children cumulated vsize (Kb) 147616 [startup+610.057 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32724 0 0 0 60692 159 0 0 25 0 1 0 1796854555 149180416 31358 4294967295 134512640 135094434 3221224432 3221223104 134555765 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36421 31358 145 145 0 36276 0 [pid=11237] vsize: 145684 Current children cumulated CPU time (s) 608.52 Current children cumulated vsize (Kb) 147808 [startup+620.059 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32804 0 0 0 61690 160 0 0 25 0 1 0 1796854555 149762048 31438 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36563 31438 145 145 0 36418 0 [pid=11237] vsize: 146252 Current children cumulated CPU time (s) 618.51 Current children cumulated vsize (Kb) 148376 [startup+630.059 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32860 0 0 0 62688 161 0 0 25 0 1 0 1796854555 149987328 31494 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36618 31494 145 145 0 36473 0 [pid=11237] vsize: 146472 Current children cumulated CPU time (s) 628.5 Current children cumulated vsize (Kb) 148596 [startup+640.06 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32918 0 0 0 63687 162 0 0 25 0 1 0 1796854555 150220800 31552 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36675 31552 145 145 0 36530 0 [pid=11237] vsize: 146700 Current children cumulated CPU time (s) 638.5 Current children cumulated vsize (Kb) 148824 [startup+650.062 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 32963 0 0 0 64686 163 0 0 25 0 1 0 1796854555 150401024 31597 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36719 31597 145 145 0 36574 0 [pid=11237] vsize: 146876 Current children cumulated CPU time (s) 648.5 Current children cumulated vsize (Kb) 149000 [startup+660.063 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33028 0 0 0 65684 164 0 0 25 0 1 0 1796854555 150667264 31662 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36784 31662 145 145 0 36639 0 [pid=11237] vsize: 147136 Current children cumulated CPU time (s) 658.49 Current children cumulated vsize (Kb) 149260 [startup+670.065 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33109 0 0 0 66682 165 0 0 25 0 1 0 1796854555 150990848 31743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36863 31743 145 145 0 36718 0 [pid=11237] vsize: 147452 Current children cumulated CPU time (s) 668.48 Current children cumulated vsize (Kb) 149576 [startup+680.066 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33189 0 0 0 67680 167 0 0 25 0 1 0 1796854555 151318528 31823 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 36943 31823 145 145 0 36798 0 [pid=11237] vsize: 147772 Current children cumulated CPU time (s) 678.48 Current children cumulated vsize (Kb) 149896 [startup+690.067 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33271 0 0 0 68679 168 0 0 25 0 1 0 1796854555 151650304 31905 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37024 31905 145 145 0 36879 0 [pid=11237] vsize: 148096 Current children cumulated CPU time (s) 688.48 Current children cumulated vsize (Kb) 150220 [startup+700.068 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33336 0 0 0 69678 168 0 0 25 0 1 0 1796854555 151912448 31970 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37088 31970 145 145 0 36943 0 [pid=11237] vsize: 148352 Current children cumulated CPU time (s) 698.47 Current children cumulated vsize (Kb) 150476 [startup+710.069 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33413 0 0 0 70676 169 0 0 25 0 1 0 1796854555 152223744 32047 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37164 32047 145 145 0 37019 0 [pid=11237] vsize: 148656 Current children cumulated CPU time (s) 708.46 Current children cumulated vsize (Kb) 150780 [startup+720.071 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33492 0 0 0 71674 171 0 0 25 0 1 0 1796854555 152543232 32126 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37242 32126 145 145 0 37097 0 [pid=11237] vsize: 148968 Current children cumulated CPU time (s) 718.46 Current children cumulated vsize (Kb) 151092 [startup+730.072 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33566 0 0 0 72673 171 0 0 25 0 1 0 1796854555 152846336 32200 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37316 32200 145 145 0 37171 0 [pid=11237] vsize: 149264 Current children cumulated CPU time (s) 728.45 Current children cumulated vsize (Kb) 151388 [startup+740.074 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33636 0 0 0 73672 172 0 0 25 0 1 0 1796854555 153128960 32270 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37385 32270 145 145 0 37240 0 [pid=11237] vsize: 149540 Current children cumulated CPU time (s) 738.45 Current children cumulated vsize (Kb) 151664 [startup+750.074 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33709 0 0 0 74670 173 0 0 25 0 1 0 1796854555 153423872 32343 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37457 32343 145 145 0 37312 0 [pid=11237] vsize: 149828 Current children cumulated CPU time (s) 748.44 Current children cumulated vsize (Kb) 151952 [startup+760.074 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33785 0 0 0 75667 174 0 0 25 0 1 0 1796854555 153735168 32419 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37533 32419 145 145 0 37388 0 [pid=11237] vsize: 150132 Current children cumulated CPU time (s) 758.42 Current children cumulated vsize (Kb) 152256 [startup+770.076 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33842 0 0 0 76666 175 0 0 25 0 1 0 1796854555 153964544 32476 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37589 32476 145 145 0 37444 0 [pid=11237] vsize: 150356 Current children cumulated CPU time (s) 768.42 Current children cumulated vsize (Kb) 152480 [startup+780.077 s] Raw data (loadavg): 1.00 0.99 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33910 0 0 0 77664 176 0 0 25 0 1 0 1796854555 154243072 32544 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37657 32544 145 145 0 37512 0 [pid=11237] vsize: 150628 Current children cumulated CPU time (s) 778.41 Current children cumulated vsize (Kb) 152752 [startup+790.078 s] Raw data (loadavg): 1.07 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 33970 0 0 0 78662 177 0 0 25 0 1 0 1796854555 154484736 32604 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37716 32604 145 145 0 37571 0 [pid=11237] vsize: 150864 Current children cumulated CPU time (s) 788.4 Current children cumulated vsize (Kb) 152988 [startup+800.079 s] Raw data (loadavg): 1.06 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34035 0 0 0 79660 179 0 0 25 0 1 0 1796854555 154746880 32669 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37780 32669 145 145 0 37635 0 [pid=11237] vsize: 151120 Current children cumulated CPU time (s) 798.4 Current children cumulated vsize (Kb) 153244 [startup+810.08 s] Raw data (loadavg): 1.05 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34106 0 0 0 80659 180 0 0 25 0 1 0 1796854555 155037696 32740 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37851 32740 145 145 0 37706 0 [pid=11237] vsize: 151404 Current children cumulated CPU time (s) 808.4 Current children cumulated vsize (Kb) 153528 [startup+820.08 s] Raw data (loadavg): 1.04 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34206 0 0 0 81657 181 0 0 25 0 1 0 1796854555 155443200 32840 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 37950 32840 145 145 0 37805 0 [pid=11237] vsize: 151800 Current children cumulated CPU time (s) 818.39 Current children cumulated vsize (Kb) 153924 [startup+830.082 s] Raw data (loadavg): 1.04 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34301 0 0 0 82654 183 0 0 25 0 1 0 1796854555 155828224 32935 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 38044 32935 145 145 0 37899 0 [pid=11237] vsize: 152176 Current children cumulated CPU time (s) 828.38 Current children cumulated vsize (Kb) 154300 [startup+840.084 s] Raw data (loadavg): 1.03 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34416 0 0 0 83651 185 0 0 25 0 1 0 1796854555 156295168 33050 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 38158 33050 145 145 0 38013 0 [pid=11237] vsize: 152632 Current children cumulated CPU time (s) 838.37 Current children cumulated vsize (Kb) 154756 [startup+850.085 s] Raw data (loadavg): 1.02 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34517 0 0 0 84650 185 0 0 25 0 1 0 1796854555 156704768 33151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38258 33151 145 145 0 38113 0 [pid=11237] vsize: 153032 Current children cumulated CPU time (s) 848.36 Current children cumulated vsize (Kb) 155156 [startup+860.086 s] Raw data (loadavg): 1.02 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34591 0 0 0 85648 186 0 0 25 0 1 0 1796854555 157007872 33225 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38332 33225 145 145 0 38187 0 [pid=11237] vsize: 153328 Current children cumulated CPU time (s) 858.35 Current children cumulated vsize (Kb) 155452 [startup+870.087 s] Raw data (loadavg): 1.02 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34653 0 0 0 86647 186 0 0 25 0 1 0 1796854555 157257728 33287 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38393 33287 145 145 0 38248 0 [pid=11237] vsize: 153572 Current children cumulated CPU time (s) 868.34 Current children cumulated vsize (Kb) 155696 [startup+880.087 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34680 0 0 0 87647 187 0 0 25 0 1 0 1796854555 157364224 33314 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38419 33314 145 145 0 38274 0 [pid=11237] vsize: 153676 Current children cumulated CPU time (s) 878.35 Current children cumulated vsize (Kb) 155800 [startup+890.089 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34714 0 0 0 88647 187 0 0 25 0 1 0 1796854555 157503488 33348 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38453 33348 145 145 0 38308 0 [pid=11237] vsize: 153812 Current children cumulated CPU time (s) 888.35 Current children cumulated vsize (Kb) 155936 [startup+900.09 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34783 0 0 0 89645 187 0 0 25 0 1 0 1796854555 157782016 33417 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38521 33417 145 145 0 38376 0 [pid=11237] vsize: 154084 Current children cumulated CPU time (s) 898.33 Current children cumulated vsize (Kb) 156208 [startup+910.09 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34863 0 0 0 90643 188 0 0 25 0 1 0 1796854555 158105600 33497 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38600 33497 145 145 0 38455 0 [pid=11237] vsize: 154400 Current children cumulated CPU time (s) 908.32 Current children cumulated vsize (Kb) 156524 [startup+920.092 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 34944 0 0 0 91642 188 0 0 25 0 1 0 1796854555 158433280 33578 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11237/statm): 38680 33578 145 145 0 38535 0 [pid=11237] vsize: 154720 Current children cumulated CPU time (s) 918.31 Current children cumulated vsize (Kb) 156844 [startup+930.093 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35042 0 0 0 92640 189 0 0 25 0 1 0 1796854555 158830592 33676 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 38777 33676 145 145 0 38632 0 [pid=11237] vsize: 155108 Current children cumulated CPU time (s) 928.3 Current children cumulated vsize (Kb) 157232 [startup+940.093 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35139 0 0 0 93638 191 0 0 25 0 1 0 1796854555 159223808 33773 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 38873 33773 145 145 0 38728 0 [pid=11237] vsize: 155492 Current children cumulated CPU time (s) 938.3 Current children cumulated vsize (Kb) 157616 [startup+950.095 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35211 0 0 0 94636 192 0 0 25 0 1 0 1796854555 159514624 33845 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 38944 33845 145 145 0 38799 0 [pid=11237] vsize: 155776 Current children cumulated CPU time (s) 948.29 Current children cumulated vsize (Kb) 157900 [startup+960.096 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35269 0 0 0 95635 192 0 0 25 0 1 0 1796854555 159752192 33903 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39002 33903 145 145 0 38857 0 [pid=11237] vsize: 156008 Current children cumulated CPU time (s) 958.28 Current children cumulated vsize (Kb) 158132 [startup+970.097 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35349 0 0 0 96633 193 0 0 25 0 1 0 1796854555 160075776 33983 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39081 33983 145 145 0 38936 0 [pid=11237] vsize: 156324 Current children cumulated CPU time (s) 968.27 Current children cumulated vsize (Kb) 158448 [startup+980.098 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35435 0 0 0 97631 195 0 0 25 0 1 0 1796854555 160428032 34069 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39167 34069 145 145 0 39022 0 [pid=11237] vsize: 156668 Current children cumulated CPU time (s) 978.27 Current children cumulated vsize (Kb) 158792 [startup+990.1 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35525 0 0 0 98629 196 0 0 25 0 1 0 1796854555 160792576 34159 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39256 34159 145 145 0 39111 0 [pid=11237] vsize: 157024 Current children cumulated CPU time (s) 988.26 Current children cumulated vsize (Kb) 159148 [startup+1000.1 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35606 0 0 0 99627 197 0 0 25 0 1 0 1796854555 161120256 34240 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39336 34240 145 145 0 39191 0 [pid=11237] vsize: 157344 Current children cumulated CPU time (s) 998.25 Current children cumulated vsize (Kb) 159468 [startup+1010.1 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35691 0 0 0 100625 198 0 0 25 0 1 0 1796854555 161472512 34325 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39422 34325 145 145 0 39277 0 [pid=11237] vsize: 157688 Current children cumulated CPU time (s) 1008.24 Current children cumulated vsize (Kb) 159812 [startup+1020.1 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35771 0 0 0 101623 199 0 0 25 0 1 0 1796854555 161800192 34405 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39502 34405 145 145 0 39357 0 [pid=11237] vsize: 158008 Current children cumulated CPU time (s) 1018.23 Current children cumulated vsize (Kb) 160132 [startup+1030.1 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35881 0 0 0 102620 201 0 0 25 0 1 0 1796854555 162242560 34515 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39610 34515 145 145 0 39465 0 [pid=11237] vsize: 158440 Current children cumulated CPU time (s) 1028.22 Current children cumulated vsize (Kb) 160564 [startup+1040.1 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 35971 0 0 0 103618 202 0 0 25 0 1 0 1796854555 162611200 34605 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39700 34605 145 145 0 39555 0 [pid=11237] vsize: 158800 Current children cumulated CPU time (s) 1038.21 Current children cumulated vsize (Kb) 160924 [startup+1050.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36065 0 0 0 104615 204 0 0 25 0 1 0 1796854555 162992128 34699 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39793 34699 145 145 0 39648 0 [pid=11237] vsize: 159172 Current children cumulated CPU time (s) 1048.2 Current children cumulated vsize (Kb) 161296 [startup+1060.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36151 0 0 0 105612 205 0 0 25 0 1 0 1796854555 163340288 34785 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39878 34785 145 145 0 39733 0 [pid=11237] vsize: 159512 Current children cumulated CPU time (s) 1058.18 Current children cumulated vsize (Kb) 161636 [startup+1070.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36239 0 0 0 106610 206 0 0 25 0 1 0 1796854555 163696640 34873 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 39965 34873 145 145 0 39820 0 [pid=11237] vsize: 159860 Current children cumulated CPU time (s) 1068.17 Current children cumulated vsize (Kb) 161984 [startup+1080.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36340 0 0 0 107607 207 0 0 25 0 1 0 1796854555 164114432 34974 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40067 34974 145 145 0 39922 0 [pid=11237] vsize: 160268 Current children cumulated CPU time (s) 1078.15 Current children cumulated vsize (Kb) 162392 [startup+1090.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36442 0 0 0 108606 208 0 0 25 0 1 0 1796854555 164524032 35076 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40167 35076 145 145 0 40022 0 [pid=11237] vsize: 160668 Current children cumulated CPU time (s) 1088.15 Current children cumulated vsize (Kb) 162792 [startup+1100.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36533 0 0 0 109604 209 0 0 25 0 1 0 1796854555 164892672 35167 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40257 35167 145 145 0 40112 0 [pid=11237] vsize: 161028 Current children cumulated CPU time (s) 1098.14 Current children cumulated vsize (Kb) 163152 [startup+1110.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36617 0 0 0 110602 210 0 0 25 0 1 0 1796854555 165240832 35251 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40342 35251 145 145 0 40197 0 [pid=11237] vsize: 161368 Current children cumulated CPU time (s) 1108.13 Current children cumulated vsize (Kb) 163492 [startup+1120.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36700 0 0 0 111600 211 0 0 25 0 1 0 1796854555 165597184 35334 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40429 35334 145 145 0 40284 0 [pid=11237] vsize: 161716 Current children cumulated CPU time (s) 1118.12 Current children cumulated vsize (Kb) 163840 [startup+1130.11 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36779 0 0 0 112598 211 0 0 25 0 1 0 1796854555 165912576 35413 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40506 35413 145 145 0 40361 0 [pid=11237] vsize: 162024 Current children cumulated CPU time (s) 1128.1 Current children cumulated vsize (Kb) 164148 [startup+1140.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36860 0 0 0 113596 212 0 0 25 0 1 0 1796854555 166236160 35494 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40585 35494 145 145 0 40440 0 [pid=11237] vsize: 162340 Current children cumulated CPU time (s) 1138.09 Current children cumulated vsize (Kb) 164464 [startup+1150.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36923 0 0 0 114595 213 0 0 25 0 1 0 1796854555 166494208 35557 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40648 35557 145 145 0 40503 0 [pid=11237] vsize: 162592 Current children cumulated CPU time (s) 1148.09 Current children cumulated vsize (Kb) 164716 [startup+1160.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 36971 0 0 0 115594 214 0 0 25 0 1 0 1796854555 166699008 35605 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40698 35605 145 145 0 40553 0 [pid=11237] vsize: 162792 Current children cumulated CPU time (s) 1158.09 Current children cumulated vsize (Kb) 164916 [startup+1170.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 37012 0 0 0 116592 215 0 0 25 0 1 0 1796854555 166862848 35646 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40738 35646 145 145 0 40593 0 [pid=11237] vsize: 162952 Current children cumulated CPU time (s) 1168.08 Current children cumulated vsize (Kb) 165076 [startup+1180.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 37068 0 0 0 117591 216 0 0 25 0 1 0 1796854555 167088128 35702 4294967295 134512640 135094434 3221224432 3221223056 134557587 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40793 35702 145 145 0 40648 0 [pid=11237] vsize: 163172 Current children cumulated CPU time (s) 1178.08 Current children cumulated vsize (Kb) 165296 [startup+1190.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 37115 0 0 0 118590 217 0 0 25 0 1 0 1796854555 167272448 35749 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40838 35749 145 145 0 40693 0 [pid=11237] vsize: 163352 Current children cumulated CPU time (s) 1188.08 Current children cumulated vsize (Kb) 165476 [startup+1200.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 37156 0 0 0 119588 218 0 0 25 0 1 0 1796854555 167440384 35790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40879 35790 145 145 0 40734 0 [pid=11237] vsize: 163516 Current children cumulated CPU time (s) 1198.07 Current children cumulated vsize (Kb) 165640 [startup+1210.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 37253 0 0 0 120586 219 0 0 25 0 1 0 1796854555 167841792 35887 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40977 35887 145 145 0 40832 0 [pid=11237] vsize: 163908 Current children cumulated CPU time (s) 1208.06 Current children cumulated vsize (Kb) 166032 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 11237 Raw data (/proc/11233/stat): 11233 (minisat+_script) S 11232 11233 8263 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796854549 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11233/statm): 531 226 485 147 0 384 0 [pid=11233] vsize: 2124 Raw data (/proc/11237/stat): 11237 (minisat+_64-bit) R 11233 11233 8263 0 -1 0 37253 0 0 0 120586 219 0 0 25 0 1 0 1796854555 167841792 35887 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11237/statm): 40977 35887 145 145 0 40832 0 [pid=11237] vsize: 163908 Current children cumulated CPU time (s) 1208.06 Current children cumulated vsize (Kb) 166032 Sending SIGTERM to -11233 Sleeping 2 seconds One traced child (pid=11233) ended because it received signal 15 (SIGTERM) One traced child (pid=11237) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1208.13 CPU user time (s): 1205.86 CPU system time (s): 2.26766 CPU usage (%): 99.8294 Max. virtual memory (cumulated for all children) (Kb): 166032
ERROR: no interpretation found !