| Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-seba.opb |
| MD5SUM | 41b5898e0f1b65f739b9a89af7596ef6 |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 16290734500 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 7565 |
| Biggest coefficient in the objective function | 258342282854400 |
| Number of bits for the biggest coefficient in the objective function | 48 |
| Sum of the numbers in the objective function | 4664562894591719 |
| Number of bits of the sum of numbers in the objective function | 53 |
| Biggest number in a constraint | 258342282854400 |
| Number of bits of the biggest number in a constraint | 48 |
| Biggest sum of numbers in a constraint | 4664562894591719 |
| Number of bits of the biggest sum of numbers | 53 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1202.26 |
| Number of variables | 23376 |
| Total number of constraints | 1029 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 0 |
| Number of constraints which are nor clauses,nor cardinality constraints | 1029 |
| Minimum length of a constraint | 10 |
| Maximum length of a constraint | 496 |
LAUNCH ON wulflinc15 THE 2005-09-18 20:35:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2813 boxname=wulflinc15 idbench=469 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 41b5898e0f1b65f739b9a89af7596ef6 /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-seba.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-seba.opb IDLAUNCH: 2813 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 911680 kB Buffers: 33852 kB Cached: 59840 kB SwapCached: 692 kB Active: 58724 kB Inactive: 37540 kB HighTotal: 131008 kB HighFree: 68068 kB LowTotal: 903652 kB LowFree: 843612 kB SwapTotal: 2097136 kB SwapFree: 2095920 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 20948 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 20:55:41 (client local time) WITH STATUS 0 IN 1207.94 SECONDS stats: 2813 7 1207.94 0
c Parsing PB file... c PARSE ERROR! [line 1032] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 1421 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[1491]---> BDD-cost: 11 c ---[1490]---> BDD-cost: 11 c ---[1489]---> BDD-cost: 12 c ---[1488]---> BDD-cost: 15 c ---[1486]---> BDD-cost: 14 c ---[1485]---> BDD-cost: 11 c ---[1483]---> BDD-cost: 17 c ---[1482]---> BDD-cost: 18 c ---[1481]---> BDD-cost: 18 c ---[1480]---> BDD-cost: 17 c ---[1479]---> BDD-cost: 14 c ---[1478]---> BDD-cost: 16 c ---[1477]---> BDD-cost: 17 c ---[1476]---> BDD-cost: 18 c ---[1475]---> BDD-cost: 16 c ---[1474]---> BDD-cost: 17 c ---[1473]---> BDD-cost: 19 c ---[1472]---> BDD-cost: 13 c ---[1471]---> BDD-cost: 13 c ---[1470]---> BDD-cost: 13 c ---[1469]---> BDD-cost: 14 c ---[1467]---> BDD-cost: 16 c ---[1466]---> BDD-cost: 19 c ---[1465]---> BDD-cost: 19 c ---[1464]---> BDD-cost: 17 c ---[1463]---> BDD-cost: 18 c ---[1462]---> BDD-cost: 17 c ---[1461]---> BDD-cost: 14 c ---[1459]---> BDD-cost: 19 c ---[1458]---> BDD-cost: 13 c ---[1457]---> BDD-cost: 15 c ---[1456]---> BDD-cost: 14 c ---[1455]---> BDD-cost: 19 c ---[1454]---> BDD-cost: 18 c ---[1453]---> BDD-cost: 14 c ---[1451]---> BDD-cost: 17 c ---[1450]---> BDD-cost: 13 c ---[1449]---> BDD-cost: 14 c ---[1448]---> BDD-cost: 15 c ---[1447]---> BDD-cost: 12 c ---[1445]---> BDD-cost: 14 c ---[1443]---> BDD-cost: 15 c ---[1442]---> BDD-cost: 13 c ---[1441]---> BDD-cost: 16 c ---[1440]---> BDD-cost: 14 c ---[1439]---> BDD-cost: 14 c ---[1438]---> BDD-cost: 14 c ---[1437]---> BDD-cost: 15 c ---[1432]---> BDD-cost: 14 c ---[1431]---> BDD-cost: 15 c ---[1429]---> BDD-cost: 19 c ---[1428]---> BDD-cost: 19 c ---[1427]---> BDD-cost: 19 c ---[1425]---> BDD-cost: 11 c ---[1424]---> BDD-cost: 17 c ---[1423]---> BDD-cost: 16 c ---[1422]---> BDD-cost: 13 c ---[1421]---> BDD-cost: 17 c ---[1420]---> BDD-cost: 18 c ---[1419]---> BDD-cost: 18 c ---[1418]---> BDD-cost: 12 c ---[1417]---> BDD-cost: 17 c ---[1416]---> BDD-cost: 17 c ---[1415]---> BDD-cost: 14 c ---[1414]---> BDD-cost: 16 c ---[1413]---> BDD-cost: 13 c ---[1412]---> BDD-cost: 13 c ---[1411]---> BDD-cost: 16 c ---[1410]---> BDD-cost: 14 c ---[1406]---> BDD-cost: 19 c ---[1405]---> BDD-cost: 16 c ---[1404]---> BDD-cost: 11 c ---[1403]---> BDD-cost: 17 c ---[1401]---> BDD-cost: 14 c ---[1400]---> BDD-cost: 14 c ---[1399]---> BDD-cost: 13 c ---[1397]---> BDD-cost: 16 c ---[1396]---> BDD-cost: 11 c ---[1395]---> BDD-cost: 13 c ---[1394]---> BDD-cost: 18 c ---[1393]---> BDD-cost: 17 c ---[1392]---> BDD-cost: 16 c ---[1391]---> BDD-cost: 13 c ---[1390]---> BDD-cost: 13 c ---[1389]---> BDD-cost: 15 c ---[1388]---> BDD-cost: 14 c ---[1387]---> BDD-cost: 11 c ---[1386]---> BDD-cost: 16 c ---[1385]---> BDD-cost: 17 c ---[1384]---> BDD-cost: 15 c ---[1383]---> BDD-cost: 15 c ---[1382]---> BDD-cost: 15 c ---[1381]---> BDD-cost: 16 c ---[1380]---> BDD-cost: 8 c ---[1378]---> BDD-cost: 10 c ---[1377]---> BDD-cost: 15 c ---[1376]---> BDD-cost: 15 c ---[1375]---> BDD-cost: 14 c ---[1374]---> BDD-cost: 18 c ---[1373]---> BDD-cost: 11 c ---[1372]---> BDD-cost: 17 c ---[1371]---> BDD-cost: 18 c ---[1370]---> BDD-cost: 14 c ---[1369]---> BDD-cost: 15 c ---[1365]---> BDD-cost: 18 c ---[1364]---> BDD-cost: 19 c ---[1363]---> BDD-cost: 16 c ---[1362]---> BDD-cost: 14 c ---[1361]---> BDD-cost: 17 c ---[1359]---> BDD-cost: 15 c ---[1358]---> BDD-cost: 14 c ---[1357]---> BDD-cost: 15 c ---[1354]---> BDD-cost: 16 c ---[1352]---> BDD-cost: 13 c ---[1350]---> BDD-cost: 17 c ---[1349]---> BDD-cost: 15 c ---[1348]---> BDD-cost: 15 c ---[1347]---> BDD-cost: 15 c ---[1346]---> BDD-cost: 16 c ---[1343]---> BDD-cost: 14 c ---[1342]---> BDD-cost: 9 c ---[1341]---> BDD-cost: 14 c ---[1340]---> BDD-cost: 15 c ---[1339]---> BDD-cost: 14 c ---[1338]---> BDD-cost: 14 c ---[1337]---> BDD-cost: 14 c ---[1336]---> BDD-cost: 13 c ---[1335]---> BDD-cost: 15 c ---[1334]---> BDD-cost: 14 c ---[1333]---> BDD-cost: 14 c ---[1332]---> BDD-cost: 15 c ---[1331]---> BDD-cost: 15 c ---[1329]---> BDD-cost: 15 c ---[1328]---> BDD-cost: 12 c ---[1327]---> BDD-cost: 10 c ---[1326]---> BDD-cost: 14 c ---[1325]---> BDD-cost: 11 c ---[1324]---> BDD-cost: 15 c ---[1323]---> BDD-cost: 14 c ---[1322]---> BDD-cost: 11 c ---[1321]---> BDD-cost: 15 c ---[1320]---> BDD-cost: 18 c ---[1319]---> BDD-cost: 15 c ---[1317]---> BDD-cost: 12 c ---[1316]---> BDD-cost: 13 c ---[1315]---> BDD-cost: 11 c ---[1314]---> BDD-cost: 13 c ---[1313]---> BDD-cost: 13 c ---[1312]---> BDD-cost: 11 c ---[1311]---> BDD-cost: 18 c ---[1310]---> BDD-cost: 17 c ---[1308]---> BDD-cost: 13 c ---[1306]---> BDD-cost: 13 c ---[1305]---> BDD-cost: 17 c ---[1304]---> BDD-cost: 14 c ---[1303]---> BDD-cost: 15 c ---[1300]---> BDD-cost: 14 c ---[1297]---> BDD-cost: 16 c ---[1296]---> BDD-cost: 16 c ---[1295]---> BDD-cost: 13 c ---[1293]---> BDD-cost: 15 c ---[1290]---> BDD-cost: 10 c ---[1289]---> BDD-cost: 16 c ---[1288]---> BDD-cost: 18 c ---[1287]---> BDD-cost: 10 c ---[1286]---> BDD-cost: 17 c ---[1285]---> BDD-cost: 14 c ---[1284]---> BDD-cost: 14 c ---[1283]---> BDD-cost: 11 c ---[1281]---> BDD-cost: 11 c ---[1280]---> BDD-cost: 14 c ---[1278]---> BDD-cost: 16 c ---[1277]---> BDD-cost: 13 c ---[1276]---> BDD-cost: 16 c ---[1274]---> BDD-cost: 15 c ---[1271]---> BDD-cost: 15 c ---[1270]---> BDD-cost: 14 c ---[1268]---> BDD-cost: 11 c ---[1267]---> BDD-cost: 14 c ---[1266]---> BDD-cost: 15 c ---[1265]---> BDD-cost: 14 c ---[1264]---> BDD-cost: 12 c ---[1262]---> BDD-cost: 12 c ---[1261]---> BDD-cost: 13 c ---[1260]---> BDD-cost: 14 c ---[1259]---> BDD-cost: 16 c ---[1257]---> BDD-cost: 15 c ---[1256]---> BDD-cost: 17 c ---[1255]---> BDD-cost: 18 c ---[1253]---> BDD-cost: 17 c ---[1251]---> BDD-cost: 15 c ---[1249]---> BDD-cost: 9 c ---[1248]---> BDD-cost: 5 c ---[1247]---> BDD-cost: 9 c ---[1246]---> BDD-cost: 14 c ---[1245]---> BDD-cost: 15 c ---[1244]---> BDD-cost: 13 c ---[1243]---> BDD-cost: 15 c ---[1242]---> BDD-cost: 13 c ---[1241]---> BDD-cost: 12 c ---[1240]---> BDD-cost: 15 c ---[1239]---> BDD-cost: 13 c ---[1237]---> BDD-cost: 18 c ---[1236]---> BDD-cost: 17 c ---[1235]---> BDD-cost: 11 c ---[1234]---> BDD-cost: 15 c ---[1233]---> BDD-cost: 12 c ---[1232]---> BDD-cost: 14 c ---[1230]---> BDD-cost: 10 c ---[1229]---> BDD-cost: 10 c ---[1228]---> BDD-cost: 12 c ---[1227]---> BDD-cost: 15 c ---[1226]---> BDD-cost: 14 c ---[1224]---> BDD-cost: 14 c ---[1218]---> BDD-cost: 15 c ---[1216]---> BDD-cost: 17 c ---[1215]---> BDD-cost: 18 c ---[1214]---> BDD-cost: 16 c ---[1213]---> BDD-cost: 15 c ---[1212]---> BDD-cost: 17 c ---[1211]---> BDD-cost: 16 c ---[1210]---> BDD-cost: 14 c ---[1209]---> BDD-cost: 15 c ---[1207]---> BDD-cost: 15 c ---[1206]---> BDD-cost: 18 c ---[1205]---> BDD-cost: 9 c ---[1204]---> BDD-cost: 12 c ---[1203]---> BDD-cost: 13 c ---[1202]---> BDD-cost: 11 c ---[1201]---> BDD-cost: 15 c ---[1200]---> BDD-cost: 12 c ---[1199]---> BDD-cost: 11 c ---[1198]---> BDD-cost: 13 c ---[1197]---> BDD-cost: 13 c ---[1196]---> BDD-cost: 12 c ---[1195]---> BDD-cost: 13 c ---[1194]---> BDD-cost: 15 c ---[1191]---> BDD-cost: 13 c ---[1190]---> BDD-cost: 14 c ---[1189]---> BDD-cost: 12 c ---[1188]---> BDD-cost: 13 c ---[1187]---> BDD-cost: 13 c ---[1185]---> BDD-cost: 10 c ---[1184]---> BDD-cost: 13 c ---[1182]---> BDD-cost: 14 c ---[1181]---> BDD-cost: 14 c ---[1180]---> BDD-cost: 12 c ---[1178]---> BDD-cost: 6 c ---[1177]---> BDD-cost: 7 c ---[1175]---> BDD-cost: 12 c ---[1173]---> BDD-cost: 12 c ---[1172]---> BDD-cost: 19 c ---[1171]---> BDD-cost: 18 c ---[1170]---> BDD-cost: 18 c ---[1169]---> BDD-cost: 12 c ---[1168]---> BDD-cost: 10 c ---[1165]---> BDD-cost: 9 c ---[1161]---> BDD-cost: 16 c ---[1160]---> BDD-cost: 11 c ---[1157]---> BDD-cost: 10 c ---[1156]---> BDD-cost: 9 c ---[1155]---> BDD-cost: 10 c ---[1154]---> BDD-cost: 12 c ---[1149]---> BDD-cost: 11 c ---[1148]---> BDD-cost: 14 c ---[1147]---> BDD-cost: 18 c ---[1145]---> BDD-cost: 12 c ---[1144]---> BDD-cost: 15 c ---[1143]---> BDD-cost: 11 c ---[1142]---> BDD-cost: 17 c ---[1141]---> BDD-cost: 12 c ---[1140]---> BDD-cost: 10 c ---[1139]---> BDD-cost: 11 c ---[1138]---> BDD-cost: 12 c ---[1137]---> BDD-cost: 13 c ---[1135]---> BDD-cost: 15 c ---[1134]---> BDD-cost: 14 c ---[1133]---> BDD-cost: 19 c ---[1132]---> BDD-cost: 13 c ---[1131]---> BDD-cost: 14 c ---[1130]---> BDD-cost: 13 c ---[1128]---> BDD-cost: 13 c ---[1127]---> BDD-cost: 10 c ---[1125]---> BDD-cost: 17 c ---[1124]---> BDD-cost: 15 c ---[1123]---> BDD-cost: 13 c ---[1122]---> BDD-cost: 12 c ---[1121]---> BDD-cost: 10 c ---[1120]---> BDD-cost: 13 c ---[1117]---> BDD-cost: 12 c ---[1116]---> BDD-cost: 12 c ---[1115]---> BDD-cost: 14 c ---[1114]---> BDD-cost: 13 c ---[1112]---> BDD-cost: 12 c ---[1111]---> BDD-cost: 13 c ---[1110]---> BDD-cost: 13 c ---[1109]---> BDD-cost: 11 c ---[1108]---> BDD-cost: 15 c ---[1107]---> BDD-cost: 13 c ---[1106]---> BDD-cost: 15 c ---[1105]---> BDD-cost: 12 c ---[1104]---> BDD-cost: 11 c ---[1103]---> BDD-cost: 9 c ---[1102]---> BDD-cost: 12 c ---[1101]---> BDD-cost: 14 c ---[1100]---> BDD-cost: 13 c ---[1099]---> BDD-cost: 15 c ---[1098]---> BDD-cost: 14 c ---[1096]---> BDD-cost: 13 c ---[1094]---> BDD-cost: 11 c ---[1092]---> BDD-cost: 14 c ---[1090]---> BDD-cost: 14 c ---[1088]---> BDD-cost: 9 c ---[1086]---> BDD-cost: 13 c ---[1085]---> BDD-cost: 7 c ---[1084]---> BDD-cost: 11 c ---[1083]---> BDD-cost: 12 c ---[1081]---> BDD-cost: 12 c ---[1080]---> BDD-cost: 6 c ---[1079]---> BDD-cost: 10 c ---[1077]---> BDD-cost: 11 c ---[1076]---> BDD-cost: 15 c ---[1075]---> BDD-cost: 13 c ---[1073]---> BDD-cost: 13 c ---[1071]---> BDD-cost: 10 c ---[1070]---> BDD-cost: 7 c ---[1069]---> BDD-cost: 17 c ---[1068]---> BDD-cost: 18 c ---[1067]---> BDD-cost: 16 c ---[1066]---> BDD-cost: 12 c ---[1065]---> BDD-cost: 18 c ---[1064]---> BDD-cost: 14 c ---[1063]---> BDD-cost: 14 c ---[1062]---> BDD-cost: 17 c ---[1048]---> BDD-cost: 17 c ---[1047]---> BDD-cost: 15 c ---[1046]---> BDD-cost: 15 c ---[1045]---> BDD-cost: 16 c ---[1042]---> BDD-cost: 11 c ---[1041]---> BDD-cost: 16 c ---[1039]---> BDD-cost: 15 c ---[1038]---> BDD-cost: 17 c ---[1037]---> BDD-cost: 15 c ---[1036]---> BDD-cost: 13 c ---[1035]---> BDD-cost: 12 c ---[1034]---> BDD-cost: 12 c ---[1028]---> BDD-cost: 8 c ---[1027]---> BDD-cost: 15 c ---[1026]---> BDD-cost: 12 c ---[1025]---> BDD-cost: 13 c ---[1024]---> BDD-cost: 16 c ---[1023]---> BDD-cost: 16 c ---[1022]---> BDD-cost: 14 c ---[1021]---> BDD-cost: 14 c ---[1016]---> BDD-cost: 13 c ---[1015]---> BDD-cost: 13 c ---[1014]---> BDD-cost: 14 c ---[1013]---> BDD-cost: 11 c ---[1012]---> BDD-cost: 8 c ---[1008]---> BDD-cost: 13 c ---[1007]---> BDD-cost: 11 c ---[1006]---> BDD-cost: 11 c ---[1005]---> BDD-cost: 13 c ---[ 999]---> BDD-cost: 13 c ---[ 998]---> BDD-cost: 12 c ---[ 997]---> BDD-cost: 14 c ---[ 996]---> BDD-cost: 14 c ---[ 995]---> BDD-cost: 14 c ---[ 994]---> BDD-cost: 18 c ---[ 993]---> BDD-cost: 19 c ---[ 992]---> BDD-cost: 11 c ---[ 991]---> BDD-cost: 16 c ---[ 985]---> Sorter-cost: 295 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 984]---> BDD-cost: 63 c ---[ 983]---> BDD-cost: 58 c ---[ 982]---> BDD-cost: 68 c ---[ 981]---> BDD-cost: 58 c ---[ 980]---> BDD-cost: 73 c ---[ 979]---> BDD-cost: 63 c ---[ 977]---> BDD-cost: 112 c ---[ 975]---> Sorter-cost: 580 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 973]---> Sorter-cost: 1398 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 971]---> Sorter-cost: 1039 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 969]---> Sorter-cost: 485 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 967]---> Adder-cost: 438 maxlim: 630756 bits: 21/20 c ---[ 965]---> Sorter-cost: 771 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 963]---> BDD-cost: 180 c ---[ 961]---> Sorter-cost: 836 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 959]---> Adder-cost: 394 maxlim: 13189095 bits: 25/24 c ---[ 957]---> Sorter-cost: 1499 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 955]---> Sorter-cost: 2907 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 953]---> Sorter-cost: 1456 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 951]---> BDD-cost: 180 c ---[ 949]---> BDD-cost: 176 c ---[ 947]---> Sorter-cost: 2763 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 945]---> BDD-cost: 194 c ---[ 943]---> Adder-cost: 290 maxlim: 221175 bits: 19/18 c ---[ 941]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 939]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 937]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 935]---> Adder-cost: 308 maxlim: 212978 bits: 19/18 c ---[ 933]---> Adder-cost: 690 maxlim: 11435964 bits: 25/24 c ---[ 931]---> Adder-cost: 574 maxlim: 11042750 bits: 25/24 c ---[ 929]---> Adder-cost: 428 maxlim: 11042750 bits: 25/24 c ---[ 927]---> Adder-cost: 1000 maxlim: 75267630 bits: 28/27 c ---[ 925]---> Adder-cost: 622 maxlim: 75267630 bits: 28/27 c ---[ 923]---> Adder-cost: 379 maxlim: 1867758 bits: 22/21 c ---[ 921]---> Adder-cost: 576 maxlim: 10944429 bits: 25/24 c ---[ 919]---> Adder-cost: 488 maxlim: 10944429 bits: 25/24 c ---[ 917]---> Adder-cost: 372 maxlim: 9502666 bits: 25/24 c ---[ 915]---> Adder-cost: 666 maxlim: 1277895 bits: 22/21 c ---[ 913]---> Adder-cost: 672 maxlim: 1298372 bits: 22/21 c ---[ 911]---> Adder-cost: 289 maxlim: 229360 bits: 19/18 c ---[ 909]---> Adder-cost: 357 maxlim: 3243968 bits: 23/22 c ---[ 907]---> BDD-cost: 184 c ---[ 905]---> Adder-cost: 248 maxlim: 1621984 bits: 22/21 c ---[ 903]---> Sorter-cost: 3144 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 901]---> Adder-cost: 248 maxlim: 1621984 bits: 22/21 c ---[ 899]---> Sorter-cost: 892 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 897]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 895]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 893]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 891]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 889]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 887]---> Adder-cost: 571 maxlim: 937938 bits: 21/20 c ---[ 885]---> Adder-cost: 312 maxlim: 630756 bits: 21/20 c ---[ 883]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 881]---> BDD-cost: 157 c ---[ 879]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 877]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 875]---> Sorter-cost: 1796 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 873]---> Adder-cost: 297 maxlim: 483299 bits: 20/19 c ---[ 871]---> Adder-cost: 1024 maxlim: 3616609 bits: 23/22 c ---[ 869]---> Sorter-cost: 727 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 867]---> BDD-cost: 178 c ---[ 865]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 863]---> Sorter-cost: 772 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 861]---> Sorter-cost: 2894 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 859]---> BDD-cost: 191 c ---[ 857]---> BDD-cost: 185 c ---[ 855]---> Sorter-cost: 1076 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 853]---> Adder-cost: 323 maxlim: 491490 bits: 20/19 c ---[ 851]---> Adder-cost: 763 maxlim: 946134 bits: 21/20 c ---[ 849]---> Adder-cost: 589 maxlim: 937947 bits: 21/20 c ---[ 847]---> Adder-cost: 463 maxlim: 946134 bits: 21/20 c ---[ 845]---> Adder-cost: 896 maxlim: 2404242 bits: 23/22 c ---[ 843]---> Adder-cost: 564 maxlim: 2404242 bits: 23/22 c ---[ 841]---> Adder-cost: 747 maxlim: 2002861 bits: 22/21 c ---[ 839]---> BDD-cost: 171 c ---[ 837]---> Adder-cost: 799 maxlim: 3952477 bits: 23/22 c ---[ 835]---> BDD-cost: 180 c ---[ 833]---> Adder-cost: 319 maxlim: 315378 bits: 20/19 c ---[ 831]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 829]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 827]---> Sorter-cost: 2256 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 825]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 823]---> Adder-cost: 574 maxlim: 5406679 bits: 24/23 c ---[ 821]---> Adder-cost: 336 maxlim: 4358094 bits: 24/23 c ---[ 819]---> Adder-cost: 417 maxlim: 3932115 bits: 23/22 c ---[ 817]---> Adder-cost: 366 maxlim: 5210052 bits: 24/23 c ---[ 815]---> Adder-cost: 300 maxlim: 3932115 bits: 23/22 c ---[ 813]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 811]---> Adder-cost: 316 maxlim: 2523024 bits: 23/22 c ---[ 809]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 807]---> Sorter-cost: 2419 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 805]---> BDD-cost: 144 c ---[ 803]---> Sorter-cost: 2290 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 801]---> Sorter-cost: 2382 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 799]---> Adder-cost: 428 maxlim: 589803 bits: 21/20 c ---[ 797]---> Sorter-cost: 2382 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 795]---> Sorter-cost: 2303 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 793]---> BDD-cost: 170 c ---[ 791]---> Adder-cost: 284 maxlim: 589803 bits: 21/20 c ---[ 789]---> BDD-cost: 162 c ---[ 787]---> Sorter-cost: 1911 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 785]---> Sorter-cost: 2309 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 783]---> Sorter-cost: 2309 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 781]---> Sorter-cost: 2303 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 779]---> Sorter-cost: 2378 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 777]---> Sorter-cost: 2391 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 775]---> Adder-cost: 474 maxlim: 1376207 bits: 22/21 c ---[ 773]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 771]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 769]---> Adder-cost: 348 maxlim: 348145 bits: 20/19 c ---[ 767]---> Sorter-cost: 1522 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 765]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 763]---> Adder-cost: 264 maxlim: 294901 bits: 20/19 c ---[ 761]---> Adder-cost: 440 maxlim: 860142 bits: 21/20 c ---[ 759]---> Adder-cost: 312 maxlim: 630756 bits: 21/20 c ---[ 757]---> Adder-cost: 936 maxlim: 3665754 bits: 23/22 c ---[ 755]---> Adder-cost: 558 maxlim: 3350376 bits: 23/22 c ---[ 753]---> Adder-cost: 1460 maxlim: 22264803 bits: 26/25 c ---[ 751]---> Adder-cost: 1416 maxlim: 32160271 bits: 26/25 c ---[ 749]---> Adder-cost: 508 maxlim: 2408335 bits: 23/22 c ---[ 747]---> Adder-cost: 870 maxlim: 2297747 bits: 23/22 c ---[ 745]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 743]---> BDD-cost: 136 c ---[ 741]---> Adder-cost: 988 maxlim: 6663881 bits: 24/23 c ---[ 739]---> Adder-cost: 1102 maxlim: 4853526 bits: 24/23 c ---[ 737]---> Adder-cost: 624 maxlim: 4853526 bits: 24/23 c ---[ 735]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 733]---> Adder-cost: 588 maxlim: 2219934 bits: 23/22 c ---[ 731]---> Adder-cost: 269 maxlim: 241654 bits: 19/18 c ---[ 729]---> Adder-cost: 453 maxlim: 954326 bits: 21/20 c ---[ 727]---> Adder-cost: 540 maxlim: 622557 bits: 21/20 c ---[ 725]---> Adder-cost: 322 maxlim: 298995 bits: 20/19 c ---[ 723]---> Adder-cost: 376 maxlim: 1269690 bits: 22/21 c ---[ 721]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 719]---> Adder-cost: 550 maxlim: 851920 bits: 21/20 c ---[ 717]---> Adder-cost: 1144 maxlim: 9559638 bits: 25/24 c ---[ 715]---> Adder-cost: 264 maxlim: 294901 bits: 20/19 c ---[ 713]---> Adder-cost: 492 maxlim: 565220 bits: 21/20 c ---[ 711]---> Adder-cost: 643 maxlim: 1900460 bits: 22/21 c ---[ 709]---> Adder-cost: 522 maxlim: 827354 bits: 21/20 c ---[ 707]---> Adder-cost: 350 maxlim: 401390 bits: 20/19 c ---[ 705]---> Adder-cost: 311 maxlim: 229364 bits: 19/18 c ---[ 703]---> Adder-cost: 650 maxlim: 1617842 bits: 22/21 c ---[ 701]---> Adder-cost: 306 maxlim: 458729 bits: 20/19 c ---[ 699]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 697]---> Adder-cost: 211 maxlim: 241654 bits: 19/18 c ---[ 695]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 693]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 691]---> BDD-cost: 153 c ---[ 689]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 687]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 685]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 683]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 681]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 679]---> Sorter-cost: 686 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 677]---> Adder-cost: 264 maxlim: 294901 bits: 20/19 c ---[ 675]---> Adder-cost: 268 maxlim: 303092 bits: 20/19 c ---[ 673]---> Adder-cost: 264 maxlim: 294901 bits: 20/19 c ---[ 671]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 669]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 667]---> Adder-cost: 202 maxlim: 151542 bits: 19/18 c ---[ 665]---> Sorter-cost: 451 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 663]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 661]---> Sorter-cost: 523 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 659]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 657]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 655]---> Sorter-cost: 805 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 653]---> Adder-cost: 312 maxlim: 630756 bits: 21/20 c ---[ 651]---> Sorter-cost: 2035 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 649]---> BDD-cost: 166 c ---[ 647]---> Adder-cost: 314 maxlim: 630756 bits: 21/20 c ---[ 645]---> Sorter-cost: 1649 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 643]---> Sorter-cost: 1649 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 641]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 639]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 637]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 635]---> Sorter-cost: 1417 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 633]---> Sorter-cost: 1465 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 631]---> Sorter-cost: 1456 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 629]---> Sorter-cost: 1481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 627]---> Sorter-cost: 1332 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 625]---> Sorter-cost: 1805 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 623]---> BDD-cost: 139 c ---[ 621]---> Adder-cost: 773 maxlim: 1978278 bits: 22/21 c ---[ 619]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 617]---> BDD-cost: 153 c ---[ 615]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 613]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 611]---> Sorter-cost: 1626 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 609]---> Adder-cost: 432 maxlim: 679905 bits: 21/20 c ---[ 607]---> Adder-cost: 464 maxlim: 1617842 bits: 22/21 c ---[ 605]---> Adder-cost: 228 maxlim: 176120 bits: 19/18 c ---[ 603]---> Adder-cost: 230 maxlim: 135159 bits: 19/18 c ---[ 601]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 599]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 597]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 595]---> Sorter-cost: 1626 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 593]---> Adder-cost: 564 maxlim: 2404242 bits: 23/22 c ---[ 591]---> BDD-cost: 184 c ---[ 589]---> Adder-cost: 208 maxlim: 217080 bits: 19/18 c ---[ 587]---> Sorter-cost: 673 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 585]---> BDD-cost: 144 c ---[ 583]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 581]---> BDD-cost: 137 c ---[ 577]---> Sorter-cost: 1517 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 575]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 573]---> Adder-cost: 282 maxlim: 204787 bits: 19/18 c ---[ 571]---> BDD-cost: 154 c ---[ 569]---> Adder-cost: 208 maxlim: 217080 bits: 19/18 c ---[ 567]---> Adder-cost: 342 maxlim: 651240 bits: 21/20 c ---[ 565]---> Adder-cost: 398 maxlim: 1085400 bits: 22/21 c ---[ 563]---> Sorter-cost: 2902 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 561]---> BDD-cost: 148 c ---[ 559]---> Sorter-cost: 2580 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 557]---> Sorter-cost: 2595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 555]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 553]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 551]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 549]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 547]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 545]---> Sorter-cost: 2399 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 543]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 541]---> Sorter-cost: 955 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 539]---> Sorter-cost: 1853 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 537]---> BDD-cost: 140 c ---[ 535]---> BDD-cost: 144 c ---[ 533]---> Sorter-cost: 2604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 531]---> Sorter-cost: 2597 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 529]---> BDD-cost: 162 c ---[ 527]---> Sorter-cost: 1837 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 525]---> Sorter-cost: 3432 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 523]---> Adder-cost: 278 maxlim: 397296 bits: 20/19 c ---[ 521]---> Adder-cost: 357 maxlim: 815073 bits: 21/20 c ---[ 519]---> Sorter-cost: 1776 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 517]---> Adder-cost: 268 maxlim: 434160 bits: 20/19 c ---[ 515]---> Sorter-cost: 1626 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 513]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 511]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 509]---> Sorter-cost: 481 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 507]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 505]---> Adder-cost: 312 maxlim: 651240 bits: 21/20 c ---[ 503]---> Sorter-cost: 1818 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 501]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 499]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 497]---> Sorter-cost: 1399 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 495]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 493]---> Sorter-cost: 2347 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 491]---> Adder-cost: 533 maxlim: 1855383 bits: 22/21 c ---[ 489]---> Adder-cost: 343 maxlim: 1765273 bits: 22/21 c ---[ 487]---> Adder-cost: 424 maxlim: 675801 bits: 21/20 c ---[ 485]---> Sorter-cost: 1388 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 483]---> Adder-cost: 637 maxlim: 1978257 bits: 22/21 c ---[ 481]---> Sorter-cost: 2160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 479]---> BDD-cost: 139 c ---[ 477]---> Sorter-cost: 556 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 475]---> Sorter-cost: 605 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 473]---> Sorter-cost: 1132 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 471]---> BDD-cost: 135 c ---[ 469]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 467]---> BDD-cost: 134 c ---[ 465]---> Sorter-cost: 1742 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 463]---> Sorter-cost: 1772 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 461]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 459]---> Sorter-cost: 775 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 457]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 455]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 453]---> Adder-cost: 392 maxlim: 1490858 bits: 22/21 c ---[ 451]---> Adder-cost: 406 maxlim: 1216443 bits: 22/21 c ---[ 449]---> Adder-cost: 375 maxlim: 634841 bits: 21/20 c ---[ 447]---> Adder-cost: 325 maxlim: 622558 bits: 21/20 c ---[ 445]---> Adder-cost: 313 maxlim: 421865 bits: 20/19 c ---[ 443]---> Adder-cost: 330 maxlim: 1187770 bits: 22/21 c ---[ 441]---> Adder-cost: 486 maxlim: 1470379 bits: 22/21 c ---[ 439]---> Adder-cost: 508 maxlim: 1503149 bits: 22/21 c ---[ 437]---> Adder-cost: 326 maxlim: 1839001 bits: 22/21 c ---[ 435]---> Adder-cost: 688 maxlim: 2338712 bits: 23/22 c ---[ 433]---> Adder-cost: 775 maxlim: 2064295 bits: 22/21 c ---[ 431]---> Sorter-cost: 1193 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 429]---> Sorter-cost: 527 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 427]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 425]---> Sorter-cost: 941 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 423]---> Sorter-cost: 1153 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 421]---> Sorter-cost: 2179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 419]---> Sorter-cost: 2138 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 417]---> Sorter-cost: 542 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 415]---> Sorter-cost: 1103 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 413]---> Sorter-cost: 1103 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 411]---> Sorter-cost: 1150 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 409]---> Sorter-cost: 2475 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 405]---> Sorter-cost: 532 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 403]---> Sorter-cost: 2597 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 401]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 399]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 397]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 395]---> Sorter-cost: 460 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 393]---> Sorter-cost: 1439 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 391]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 389]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 387]---> BDD-cost: 153 c ---[ 385]---> Sorter-cost: 1467 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 383]---> BDD-cost: 109 c ---[ 381]---> BDD-cost: 112 c ---[ 379]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 377]---> BDD-cost: 125 c ---[ 375]---> Sorter-cost: 825 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 373]---> BDD-cost: 126 c ---[ 371]---> Sorter-cost: 1918 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 369]---> Adder-cost: 631 maxlim: 1662901 bits: 22/21 c ---[ 367]---> Adder-cost: 685 maxlim: 1654711 bits: 22/21 c ---[ 365]---> Sorter-cost: 2303 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 363]---> BDD-cost: 110 c ---[ 361]---> BDD-cost: 104 c ---[ 359]---> BDD-cost: 112 c ---[ 357]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 355]---> Sorter-cost: 796 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 353]---> BDD-cost: 114 c ---[ 351]---> Sorter-cost: 565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 349]---> Sorter-cost: 916 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 347]---> BDD-cost: 126 c ---[ 345]---> Sorter-cost: 812 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 343]---> Sorter-cost: 2303 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 341]---> Sorter-cost: 801 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 339]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 337]---> Sorter-cost:12307 Base: 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 335]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 333]---> Adder-cost: 270 maxlim: 278517 bits: 20/19 c ---[ 331]---> Adder-cost: 488 maxlim: 868314 bits: 21/20 c ---[ 329]---> Sorter-cost: 824 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 327]---> Adder-cost: 319 maxlim: 315378 bits: 20/19 c ---[ 325]---> Sorter-cost: 3287 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 323]---> Sorter-cost: 565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 321]---> Sorter-cost: 1090 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 319]---> Sorter-cost: 1090 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 317]---> Adder-cost: 532 maxlim: 15809908 bits: 25/24 c ---[ 315]---> Sorter-cost: 775 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 313]---> Sorter-cost: 1621 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 311]---> Sorter-cost: 1615 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 309]---> Adder-cost: 523 maxlim: 3952477 bits: 23/22 c ---[ 307]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 305]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 303]---> Sorter-cost: 592 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 301]---> Adder-cost: 217 maxlim: 249847 bits: 19/18 c ---[ 299]---> Sorter-cost: 831 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 297]---> Sorter-cost: 654 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 295]---> Adder-cost: 820 maxlim: 2379666 bits: 23/22 c ---[ 293]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 291]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 289]---> Sorter-cost: 1610 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 287]---> Sorter-cost: 1350 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 285]---> Sorter-cost: 1103 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 281]---> Sorter-cost: 1103 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 279]---> Sorter-cost: 1103 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 277]---> Sorter-cost: 2217 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 275]---> Sorter-cost: 2179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 273]---> Adder-cost: 226 maxlim: 159735 bits: 19/18 c ---[ 271]---> BDD-cost: 148 c ---[ 269]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 267]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 265]---> Sorter-cost: 540 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 263]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 261]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 259]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 257]---> Sorter-cost: 2179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 255]---> Sorter-cost: 1350 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 253]---> Sorter-cost: 508 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 251]---> Sorter-cost: 1626 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 249]---> Sorter-cost: 2574 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 247]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 245]---> Sorter-cost: 2466 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 243]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 241]---> Sorter-cost: 638 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 239]---> Sorter-cost: 627 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 237]---> Sorter-cost: 1673 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 235]---> Sorter-cost: 2376 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 233]---> BDD-cost: 139 c ---[ 231]---> BDD-cost: 114 c ---[ 229]---> BDD-cost: 110 c ---[ 227]---> Sorter-cost: 2303 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 225]---> Sorter-cost: 1151 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 223]---> Sorter-cost: 589 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 221]---> BDD-cost: 131 c ---[ 219]---> Sorter-cost: 1060 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 217]---> Sorter-cost: 1350 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 213]---> BDD-cost: 112 c ---[ 211]---> Sorter-cost: 2179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 209]---> Sorter-cost: 980 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 207]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 205]---> BDD-cost: 149 c ---[ 203]---> BDD-cost: 153 c ---[ 201]---> Sorter-cost: 499 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> BDD-cost: 100 c ---[ 197]---> Adder-cost: 564 maxlim: 2404242 bits: 23/22 c ---[ 195]---> BDD-cost: 180 c ---[ 193]---> BDD-cost: 180 c ---[ 191]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 189]---> Adder-cost: 476 maxlim: 3350376 bits: 23/22 c ---[ 187]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 185]---> Adder-cost: 319 maxlim: 315378 bits: 20/19 c ---[ 183]---> Adder-cost: 319 maxlim: 315378 bits: 20/19 c ---[ 181]---> Sorter-cost: 754 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 177]---> Sorter-cost: 2179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 175]---> Sorter-cost: 1077 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 173]---> Adder-cost: 812 maxlim: 19782745 bits: 26/25 c ---[ 171]---> Sorter-cost: 677 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 167]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 165]---> Adder-cost: 314 maxlim: 315378 bits: 20/19 c ---[ 163]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 161]---> BDD-cost: 152 c ---[ 157]---> BDD-cost: 157 c ---[ 155]---> BDD-cost: 161 c ---[ 153]---> BDD-cost: 157 c ---[ 151]---> Sorter-cost: 2239 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> Sorter-cost: 884 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 145]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> Adder-cost: 314 maxlim: 630756 bits: 21/20 c ---[ 139]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 137]---> BDD-cost: 153 c ---[ 135]---> Adder-cost: 259 maxlim: 253936 bits: 19/18 c ---[ 133]---> Adder-cost: 269 maxlim: 233462 bits: 19/18 c ---[ 131]---> Adder-cost: 523 maxlim: 3952477 bits: 23/22 c ---[ 129]---> Adder-cost: 606 maxlim: 2441111 bits: 23/22 c ---[ 127]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 125]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 123]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 121]---> Sorter-cost: 1639 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 117]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 115]---> Sorter-cost: 1060 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 518 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> Sorter-cost: 489 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 893 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 1090 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 1138 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 3209 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 99]---> Adder-cost: 312 maxlim: 315378 bits: 20/19 c ---[ 97]---> Sorter-cost: 2578 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 95]---> BDD-cost: 148 c ---[ 93]---> Sorter-cost: 771 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> Adder-cost: 529 maxlim: 15809908 bits: 25/24 c ---[ 89]---> Sorter-cost: 2160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 87]---> Adder-cost: 312 maxlim: 1425399 bits: 22/21 c ---[ 79]---> Adder-cost: 342 maxlim: 255984 bits: 19/18 c ---[ 76]---> BDD-cost: 38 c ---[ 75]---> BDD-cost: 44 c ---[ 73]---> BDD-cost: 47 c ---[ 72]---> BDD-cost: 43 c ---[ 71]---> Sorter-cost: 1367 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> BDD-cost: 9 c ---[ 69]---> BDD-cost: 9 c ---[ 68]---> BDD-cost: 14 c ---[ 67]---> BDD-cost: 15 c ---[ 66]---> BDD-cost: 12 c ---[ 65]---> BDD-cost: 13 c ---[ 64]---> BDD-cost: 13 c ---[ 63]---> BDD-cost: 16 c ---[ 62]---> BDD-cost: 14 c ---[ 61]---> BDD-cost: 16 c ---[ 60]---> BDD-cost: 15 c ---[ 59]---> BDD-cost: 14 c ---[ 58]---> BDD-cost: 11 c ---[ 57]---> BDD-cost: 11 c ---[ 56]---> BDD-cost: 9 c ---[ 55]---> BDD-cost: 14 c ---[ 54]---> BDD-cost: 10 c ---[ 53]---> BDD-cost: 17 c ---[ 52]---> BDD-cost: 13 c ---[ 51]---> BDD-cost: 11 c ---[ 50]---> BDD-cost: 12 c ---[ 49]---> BDD-cost: 13 c ---[ 48]---> BDD-cost: 12 c ---[ 47]---> BDD-cost: 14 c ---[ 46]---> BDD-cost: 14 c ---[ 45]---> BDD-cost: 10 c ---[ 44]---> BDD-cost: 9 c ---[ 43]---> BDD-cost: 10 c ---[ 42]---> BDD-cost: 14 c ---[ 41]---> BDD-cost: 9 c ---[ 40]---> BDD-cost: 5 c ---[ 39]---> BDD-cost: 13 c ---[ 38]---> BDD-cost: 12 c ---[ 37]---> BDD-cost: 11 c ---[ 36]---> BDD-cost: 11 c ---[ 35]---> BDD-cost: 11 c ---[ 34]---> BDD-cost: 12 c ---[ 33]---> BDD-cost: 12 c ---[ 32]---> BDD-cost: 10 c ---[ 31]---> BDD-cost: 6 c ---[ 30]---> BDD-cost: 13 c ---[ 29]---> BDD-cost: 6 c ---[ 28]---> BDD-cost: 11 c ---[ 27]---> BDD-cost: 11 c ---[ 26]---> BDD-cost: 7 c ---[ 25]---> BDD-cost: 9 c ---[ 24]---> BDD-cost: 11 c ---[ 23]---> BDD-cost: 10 c ---[ 22]---> BDD-cost: 10 c ---[ 21]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 9 c ---[ 19]---> BDD-cost: 7 c ---[ 18]---> BDD-cost: 12 c ---[ 17]---> BDD-cost: 11 c ---[ 16]---> BDD-cost: 17 c ---[ 15]---> BDD-cost: 11 c ---[ 14]---> BDD-cost: 10 c ---[ 13]---> BDD-cost: 11 c ---[ 12]---> BDD-cost: 6 c ---[ 11]---> BDD-cost: 7 c ---[ 10]---> BDD-cost: 11 c ---[ 9]---> BDD-cost: 13 c ---[ 8]---> BDD-cost: 8 c ---[ 7]---> BDD-cost: 8 c ---[ 6]---> BDD-cost: 9 c ---[ 5]---> BDD-cost: 8 c ---[ 4]---> BDD-cost: 14 c ---[ 3]---> BDD-cost: 10 c ---[ 2]---> BDD-cost: 104 c ---[ 1]---> BDD-cost: 35 c ---[ 0]---> BDD-cost: 32 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1380421 3915776 | 460140 0 0 nan | 0.000 % | c | 100 | 1379860 3914524 | 506154 98 520 5.3 | 6.468 % | c | 250 | 1379860 3914524 | 556769 248 1235 5.0 | 6.468 % | c | 475 | 1379858 3914520 | 612446 472 2616 5.5 | 6.468 % | c | 812 | 1379802 3914396 | 673690 797 4172 5.2 | 6.472 % | c | 1318 | 1374309 3901930 | 741060 1269 7253 5.7 | 6.835 % | c | 2077 | 1372944 3898833 | 815166 1984 12268 6.2 | 6.926 % | c | 3216 | 1372699 3898273 | 896682 3118 23460 7.5 | 6.943 % | c | 4924 | 1372683 3898237 | 986350 4824 49805 10.3 | 6.944 % | c | 7488 | 1372563 3897968 | 1084986 7384 86865 11.8 | 6.952 % | c | 11333 | 1372549 3897937 | 1193484 11227 188541 16.8 | 6.953 % | c | 17102 | 1372549 3897937 | 1312833 16996 382799 22.5 | 6.953 % | c | 25751 | 1372539 3897915 | 1444116 25640 700797 27.3 | 6.954 % | c | 38725 | 1372539 3897915 | 1588528 38614 1550487 40.2 | 6.954 % | c | 58186 | 1371650 3895931 | 1747380 58058 2822182 48.6 | 7.008 % |
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/12307/stat): 12307 (minisat+_script) R 12306 12307 31778 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1785941805 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/12307/statm): 174 3 169 147 0 27 0 [pid=12307] 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=12308 New process pid=12309 New process pid=12310 execve syscall for /bin/sed executable One traced child (pid=12309) exited with status: 0 open syscall for file /etc/ld.so.preload 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/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=12310) exited with status: 0 One traced child (pid=12308) exited with status: 0 New process pid=12311 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-seba.opb One traced child (pid=12311) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=12312 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-seba.opb [startup+10.0042 s] Raw data (loadavg): 0.95 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 3631 0 3 0 931 21 0 0 25 0 1 0 1785941812 15646720 3571 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 3820 3571 162 162 0 3658 0 [pid=12312] vsize: 15280 Current children cumulated CPU time (s) 9.54 Current children cumulated vsize (Kb) 17408 [startup+20.005 s] Raw data (loadavg): 0.96 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 3843 0 3 0 1930 22 0 0 25 0 1 0 1785941812 16265216 3646 4294967295 134512640 135167914 3221224448 3221220940 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 3971 3646 162 162 0 3809 0 [pid=12312] vsize: 15884 Current children cumulated CPU time (s) 19.54 Current children cumulated vsize (Kb) 18012 [startup+30.0068 s] Raw data (loadavg): 0.96 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 3843 0 3 0 2930 22 0 0 25 0 1 0 1785941812 16265216 3646 4294967295 134512640 135167914 3221224448 3221220760 134694458 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 3971 3646 162 162 0 3809 0 [pid=12312] vsize: 15884 Current children cumulated CPU time (s) 29.54 Current children cumulated vsize (Kb) 18012 [startup+40.0077 s] Raw data (loadavg): 0.97 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 3843 0 3 0 3930 22 0 0 25 0 1 0 1785941812 16265216 3646 4294967295 134512640 135167914 3221224448 3221221580 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 3971 3646 162 162 0 3809 0 [pid=12312] vsize: 15884 Current children cumulated CPU time (s) 39.54 Current children cumulated vsize (Kb) 18012 [startup+50.0085 s] Raw data (loadavg): 0.97 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 3859 0 3 0 4930 23 0 0 25 0 1 0 1785941812 16265216 3662 4294967295 134512640 135167914 3221224448 3221220928 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 3971 3662 162 162 0 3809 0 [pid=12312] vsize: 15884 Current children cumulated CPU time (s) 49.55 Current children cumulated vsize (Kb) 18012 [startup+60.0093 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 3859 0 3 0 5929 23 0 0 25 0 1 0 1785941812 16265216 3662 4294967295 134512640 135167914 3221224448 3221221372 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 3971 3662 162 162 0 3809 0 [pid=12312] vsize: 15884 Current children cumulated CPU time (s) 59.54 Current children cumulated vsize (Kb) 18012 [startup+70.0101 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 4094 0 3 0 6928 24 0 0 25 0 1 0 1785941812 16760832 3814 4294967295 134512640 135167914 3221224448 3221222256 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4092 3814 162 162 0 3930 0 [pid=12312] vsize: 16368 Current children cumulated CPU time (s) 69.54 Current children cumulated vsize (Kb) 18496 [startup+80.012 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 4309 0 3 0 7926 26 0 0 25 0 1 0 1785941812 18116608 4029 4294967295 134512640 135167914 3221224448 3221220512 134723229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4423 4029 162 162 0 4261 0 [pid=12312] vsize: 17692 Current children cumulated CPU time (s) 79.54 Current children cumulated vsize (Kb) 19820 [startup+90.0128 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 4352 0 3 0 8926 26 0 0 25 0 1 0 1785941812 18219008 4072 4294967295 134512640 135167914 3221224448 3221222112 134843030 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4448 4072 162 162 0 4286 0 [pid=12312] vsize: 17792 Current children cumulated CPU time (s) 89.54 Current children cumulated vsize (Kb) 19920 [startup+100.014 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5005 0 3 0 9922 29 0 0 25 0 1 0 1785941812 19750912 4560 4294967295 134512640 135167914 3221224448 3221220656 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4822 4560 162 162 0 4660 0 [pid=12312] vsize: 19288 Current children cumulated CPU time (s) 99.53 Current children cumulated vsize (Kb) 21416 [startup+110.015 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5005 0 3 0 10922 29 0 0 25 0 1 0 1785941812 19750912 4560 4294967295 134512640 135167914 3221224448 3221221440 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4822 4560 162 162 0 4660 0 [pid=12312] vsize: 19288 Current children cumulated CPU time (s) 109.53 Current children cumulated vsize (Kb) 21416 [startup+120.016 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5005 0 3 0 11922 29 0 0 25 0 1 0 1785941812 19750912 4560 4294967295 134512640 135167914 3221224448 3221221616 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4822 4560 162 162 0 4660 0 [pid=12312] vsize: 19288 Current children cumulated CPU time (s) 119.53 Current children cumulated vsize (Kb) 21416 [startup+130.017 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5005 0 3 0 12922 30 0 0 25 0 1 0 1785941812 19750912 4560 4294967295 134512640 135167914 3221224448 3221221712 134845921 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4822 4560 162 162 0 4660 0 [pid=12312] vsize: 19288 Current children cumulated CPU time (s) 129.54 Current children cumulated vsize (Kb) 21416 [startup+140.018 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5050 0 3 0 13921 30 0 0 25 0 1 0 1785941812 19869696 4605 4294967295 134512640 135167914 3221224448 3221221932 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4851 4605 162 162 0 4689 0 [pid=12312] vsize: 19404 Current children cumulated CPU time (s) 139.53 Current children cumulated vsize (Kb) 21532 [startup+150.019 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5050 0 3 0 14921 30 0 0 25 0 1 0 1785941812 19869696 4605 4294967295 134512640 135167914 3221224448 3221221968 134522732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4851 4605 162 162 0 4689 0 [pid=12312] vsize: 19404 Current children cumulated CPU time (s) 149.53 Current children cumulated vsize (Kb) 21532 [startup+160.02 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5061 0 3 0 15920 31 0 0 25 0 1 0 1785941812 19890176 4616 4294967295 134512640 135167914 3221224448 3221221976 134722513 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4856 4616 162 162 0 4694 0 [pid=12312] vsize: 19424 Current children cumulated CPU time (s) 159.53 Current children cumulated vsize (Kb) 21552 [startup+170.02 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5076 0 3 0 16920 31 0 0 25 0 1 0 1785941812 19931136 4631 4294967295 134512640 135167914 3221224448 3221222336 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 4866 4631 162 162 0 4704 0 [pid=12312] vsize: 19464 Current children cumulated CPU time (s) 169.53 Current children cumulated vsize (Kb) 21592 [startup+180.022 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 5105 0 3 0 17919 32 0 0 25 0 1 0 1785941812 21606400 4660 4294967295 134512640 135167914 3221224448 3221222688 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 5275 4660 162 162 0 5113 0 [pid=12312] vsize: 21100 Current children cumulated CPU time (s) 179.53 Current children cumulated vsize (Kb) 23228 [startup+190.023 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 6054 0 3 0 18915 36 0 0 25 0 1 0 1785941812 23666688 5279 4294967295 134512640 135167914 3221224448 3221222300 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 5778 5279 162 162 0 5616 0 [pid=12312] vsize: 23112 Current children cumulated CPU time (s) 189.53 Current children cumulated vsize (Kb) 25240 [startup+200.023 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 6487 0 3 0 19912 37 0 0 25 0 1 0 1785941812 24780800 5712 4294967295 134512640 135167914 3221224448 3221182868 134697403 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 6050 5712 162 162 0 5888 0 [pid=12312] vsize: 24200 Current children cumulated CPU time (s) 199.51 Current children cumulated vsize (Kb) 26328 [startup+210.024 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 6792 0 3 0 20910 39 0 0 25 0 1 0 1785941812 28721152 6017 4294967295 134512640 135167914 3221224448 3221222668 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 7012 6017 162 162 0 6850 0 [pid=12312] vsize: 28048 Current children cumulated CPU time (s) 209.51 Current children cumulated vsize (Kb) 30176 [startup+220.024 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 7139 0 3 0 21907 40 0 0 25 0 1 0 1785941812 29618176 6364 4294967295 134512640 135167914 3221224448 3221222400 134523428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 7231 6364 162 162 0 7069 0 [pid=12312] vsize: 28924 Current children cumulated CPU time (s) 219.49 Current children cumulated vsize (Kb) 31052 [startup+230.025 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 8840 0 3 0 22901 44 0 0 25 0 1 0 1785941812 33304576 7406 4294967295 134512640 135167914 3221224448 3221203680 134845903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 8131 7406 162 162 0 7969 0 [pid=12312] vsize: 32524 Current children cumulated CPU time (s) 229.47 Current children cumulated vsize (Kb) 34652 [startup+240.026 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 9359 0 3 0 23895 47 0 0 25 0 1 0 1785941812 34660352 7925 4294967295 134512640 135167914 3221224448 3221177216 134843406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 8462 7925 162 162 0 8300 0 [pid=12312] vsize: 33848 Current children cumulated CPU time (s) 239.44 Current children cumulated vsize (Kb) 35976 [startup+250.027 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 18180 0 3 0 24823 84 0 0 17 0 1 0 1785941812 80867328 16699 4294967295 134512640 135167914 3221224448 3221191024 134854320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12312/statm): 19743 16699 162 162 0 19581 0 [pid=12312] vsize: 78972 Current children cumulated CPU time (s) 249.09 Current children cumulated vsize (Kb) 81100 [startup+260.028 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37018 0 3 0 25650 167 0 0 25 0 1 0 1785941812 159404032 35537 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 38917 35537 162 162 0 38755 0 [pid=12312] vsize: 155668 Current children cumulated CPU time (s) 258.19 Current children cumulated vsize (Kb) 157796 [startup+270.029 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37239 0 3 0 26648 168 0 0 25 0 1 0 1785941812 160104448 35758 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39088 35758 162 162 0 38926 0 [pid=12312] vsize: 156352 Current children cumulated CPU time (s) 268.18 Current children cumulated vsize (Kb) 158480 [startup+280.029 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37254 0 3 0 27648 169 0 0 25 0 1 0 1785941812 160165888 35773 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39103 35773 162 162 0 38941 0 [pid=12312] vsize: 156412 Current children cumulated CPU time (s) 278.19 Current children cumulated vsize (Kb) 158540 [startup+290.03 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37272 0 3 0 28648 169 0 0 25 0 1 0 1785941812 160239616 35791 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39121 35791 162 162 0 38959 0 [pid=12312] vsize: 156484 Current children cumulated CPU time (s) 288.19 Current children cumulated vsize (Kb) 158612 [startup+300.031 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37294 0 3 0 29647 169 0 0 25 0 1 0 1785941812 160333824 35813 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39144 35813 162 162 0 38982 0 [pid=12312] vsize: 156576 Current children cumulated CPU time (s) 298.18 Current children cumulated vsize (Kb) 158704 [startup+310.032 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37333 0 3 0 30647 169 0 0 25 0 1 0 1785941812 160493568 35852 4294967295 134512640 135167914 3221224448 3221223120 134562224 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39183 35852 162 162 0 39021 0 [pid=12312] vsize: 156732 Current children cumulated CPU time (s) 308.18 Current children cumulated vsize (Kb) 158860 [startup+320.033 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37384 0 3 0 31647 170 0 0 25 0 1 0 1785941812 160600064 35903 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39209 35903 162 162 0 39047 0 [pid=12312] vsize: 156836 Current children cumulated CPU time (s) 318.19 Current children cumulated vsize (Kb) 158964 [startup+330.034 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37415 0 3 0 32646 170 0 0 25 0 1 0 1785941812 160718848 35934 4294967295 134512640 135167914 3221224448 3221223108 134567743 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39238 35934 162 162 0 39076 0 [pid=12312] vsize: 156952 Current children cumulated CPU time (s) 328.18 Current children cumulated vsize (Kb) 159080 [startup+340.035 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37438 0 3 0 33646 170 0 0 25 0 1 0 1785941812 160813056 35957 4294967295 134512640 135167914 3221224448 3221223120 134562352 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39261 35957 162 162 0 39099 0 [pid=12312] vsize: 157044 Current children cumulated CPU time (s) 338.18 Current children cumulated vsize (Kb) 159172 [startup+350.036 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37459 0 3 0 34646 170 0 0 25 0 1 0 1785941812 160923648 35978 4294967295 134512640 135167914 3221224448 3221223120 134562306 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39288 35978 162 162 0 39126 0 [pid=12312] vsize: 157152 Current children cumulated CPU time (s) 348.18 Current children cumulated vsize (Kb) 159280 [startup+360.037 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37510 0 3 0 35645 171 0 0 25 0 1 0 1785941812 161124352 36029 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39337 36029 162 162 0 39175 0 [pid=12312] vsize: 157348 Current children cumulated CPU time (s) 358.18 Current children cumulated vsize (Kb) 159476 [startup+370.038 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37562 0 3 0 36644 171 0 0 25 0 1 0 1785941812 161333248 36081 4294967295 134512640 135167914 3221224448 3221223152 134562891 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39388 36081 162 162 0 39226 0 [pid=12312] vsize: 157552 Current children cumulated CPU time (s) 368.17 Current children cumulated vsize (Kb) 159680 [startup+380.039 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37626 0 3 0 37644 171 0 0 25 0 1 0 1785941812 161587200 36145 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39450 36145 162 162 0 39288 0 [pid=12312] vsize: 157800 Current children cumulated CPU time (s) 378.17 Current children cumulated vsize (Kb) 159928 [startup+390.039 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37794 0 3 0 38641 173 0 0 25 0 1 0 1785941812 162328576 36313 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39631 36313 162 162 0 39469 0 [pid=12312] vsize: 158524 Current children cumulated CPU time (s) 388.16 Current children cumulated vsize (Kb) 160652 [startup+400.039 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37829 0 3 0 39640 173 0 0 25 0 1 0 1785941812 162463744 36348 4294967295 134512640 135167914 3221224448 3221223108 134567705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39664 36348 162 162 0 39502 0 [pid=12312] vsize: 158656 Current children cumulated CPU time (s) 398.15 Current children cumulated vsize (Kb) 160784 [startup+410.04 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37890 0 3 0 40640 174 0 0 25 0 1 0 1785941812 162709504 36409 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39724 36409 162 162 0 39562 0 [pid=12312] vsize: 158896 Current children cumulated CPU time (s) 408.16 Current children cumulated vsize (Kb) 161024 [startup+420.041 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 37945 0 3 0 41639 174 0 0 25 0 1 0 1785941812 162930688 36464 4294967295 134512640 135167914 3221224448 3221223184 134559379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39778 36464 162 162 0 39616 0 [pid=12312] vsize: 159112 Current children cumulated CPU time (s) 418.15 Current children cumulated vsize (Kb) 161240 [startup+430.042 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38003 0 3 0 42638 175 0 0 25 0 1 0 1785941812 163164160 36522 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39835 36522 162 162 0 39673 0 [pid=12312] vsize: 159340 Current children cumulated CPU time (s) 428.15 Current children cumulated vsize (Kb) 161468 [startup+440.043 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38080 0 3 0 43637 175 0 0 25 0 1 0 1785941812 163471360 36599 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39910 36599 162 162 0 39748 0 [pid=12312] vsize: 159640 Current children cumulated CPU time (s) 438.14 Current children cumulated vsize (Kb) 161768 [startup+450.043 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38153 0 3 0 44635 175 0 0 25 0 1 0 1785941812 163766272 36672 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 39982 36672 162 162 0 39820 0 [pid=12312] vsize: 159928 Current children cumulated CPU time (s) 448.12 Current children cumulated vsize (Kb) 162056 [startup+460.045 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38199 0 3 0 45634 176 0 0 25 0 1 0 1785941812 163950592 36718 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40027 36718 162 162 0 39865 0 [pid=12312] vsize: 160108 Current children cumulated CPU time (s) 458.12 Current children cumulated vsize (Kb) 162236 [startup+470.046 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38220 0 3 0 46634 176 0 0 25 0 1 0 1785941812 164032512 36739 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40047 36739 162 162 0 39885 0 [pid=12312] vsize: 160188 Current children cumulated CPU time (s) 468.12 Current children cumulated vsize (Kb) 162316 [startup+480.048 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38245 0 3 0 47634 176 0 0 25 0 1 0 1785941812 164134912 36764 4294967295 134512640 135167914 3221224448 3221223152 134562540 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40072 36764 162 162 0 39910 0 [pid=12312] vsize: 160288 Current children cumulated CPU time (s) 478.12 Current children cumulated vsize (Kb) 162416 [startup+490.049 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38324 0 3 0 48632 177 0 0 25 0 1 0 1785941812 164450304 36843 4294967295 134512640 135167914 3221224448 3221223168 134560230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40149 36843 162 162 0 39987 0 [pid=12312] vsize: 160596 Current children cumulated CPU time (s) 488.11 Current children cumulated vsize (Kb) 162724 [startup+500.048 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38444 0 3 0 49630 178 0 0 25 0 1 0 1785941812 164937728 36963 4294967295 134512640 135167914 3221224448 3221223088 134562178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40268 36963 162 162 0 40106 0 [pid=12312] vsize: 161072 Current children cumulated CPU time (s) 498.1 Current children cumulated vsize (Kb) 163200 [startup+510.049 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38588 0 3 0 50628 179 0 0 25 0 1 0 1785941812 165523456 37107 4294967295 134512640 135167914 3221224448 3221223168 134560493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40411 37107 162 162 0 40249 0 [pid=12312] vsize: 161644 Current children cumulated CPU time (s) 508.09 Current children cumulated vsize (Kb) 163772 [startup+520.05 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38771 0 3 0 51625 179 0 0 25 0 1 0 1785941812 166273024 37290 4294967295 134512640 135167914 3221224448 3221223168 134560230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40594 37290 162 162 0 40432 0 [pid=12312] vsize: 162376 Current children cumulated CPU time (s) 518.06 Current children cumulated vsize (Kb) 164504 [startup+530.052 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38834 0 3 0 52625 180 0 0 25 0 1 0 1785941812 166658048 37353 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40688 37353 162 162 0 40526 0 [pid=12312] vsize: 162752 Current children cumulated CPU time (s) 528.07 Current children cumulated vsize (Kb) 164880 [startup+540.053 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38897 0 3 0 53624 180 0 0 25 0 1 0 1785941812 166912000 37416 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40750 37416 162 162 0 40588 0 [pid=12312] vsize: 163000 Current children cumulated CPU time (s) 538.06 Current children cumulated vsize (Kb) 165128 [startup+550.053 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 38973 0 3 0 54623 181 0 0 25 0 1 0 1785941812 167219200 37492 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40825 37492 162 162 0 40663 0 [pid=12312] vsize: 163300 Current children cumulated CPU time (s) 548.06 Current children cumulated vsize (Kb) 165428 [startup+560.054 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39045 0 3 0 55622 182 0 0 25 0 1 0 1785941812 167505920 37564 4294967295 134512640 135167914 3221224448 3221223120 134562370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40895 37564 162 162 0 40733 0 [pid=12312] vsize: 163580 Current children cumulated CPU time (s) 558.06 Current children cumulated vsize (Kb) 165708 [startup+570.055 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39120 0 3 0 56621 182 0 0 25 0 1 0 1785941812 167809024 37639 4294967295 134512640 135167914 3221224448 3221223120 134562260 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 40969 37639 162 162 0 40807 0 [pid=12312] vsize: 163876 Current children cumulated CPU time (s) 568.05 Current children cumulated vsize (Kb) 166004 [startup+580.056 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39163 0 3 0 57619 183 0 0 25 0 1 0 1785941812 167985152 37682 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41012 37682 162 162 0 40850 0 [pid=12312] vsize: 164048 Current children cumulated CPU time (s) 578.04 Current children cumulated vsize (Kb) 166176 [startup+590.057 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39189 0 3 0 58619 183 0 0 25 0 1 0 1785941812 168091648 37708 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41038 37708 162 162 0 40876 0 [pid=12312] vsize: 164152 Current children cumulated CPU time (s) 588.04 Current children cumulated vsize (Kb) 166280 [startup+600.058 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39254 0 3 0 59618 184 0 0 25 0 1 0 1785941812 168353792 37773 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41102 37773 162 162 0 40940 0 [pid=12312] vsize: 164408 Current children cumulated CPU time (s) 598.04 Current children cumulated vsize (Kb) 166536 [startup+610.058 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39323 0 3 0 60616 185 0 0 25 0 1 0 1785941812 168632320 37842 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41170 37842 162 162 0 41008 0 [pid=12312] vsize: 164680 Current children cumulated CPU time (s) 608.03 Current children cumulated vsize (Kb) 166808 [startup+620.059 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39406 0 3 0 61615 185 0 0 25 0 1 0 1785941812 168968192 37925 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41252 37925 162 162 0 41090 0 [pid=12312] vsize: 165008 Current children cumulated CPU time (s) 618.02 Current children cumulated vsize (Kb) 167136 [startup+630.061 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39497 0 3 0 62613 187 0 0 25 0 1 0 1785941812 169336832 38016 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41342 38016 162 162 0 41180 0 [pid=12312] vsize: 165368 Current children cumulated CPU time (s) 628.02 Current children cumulated vsize (Kb) 167496 [startup+640.062 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39605 0 3 0 63611 188 0 0 25 0 1 0 1785941812 169775104 38124 4294967295 134512640 135167914 3221224448 3221223168 134560230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41449 38124 162 162 0 41287 0 [pid=12312] vsize: 165796 Current children cumulated CPU time (s) 638.01 Current children cumulated vsize (Kb) 167924 [startup+650.063 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39698 0 3 0 64610 188 0 0 25 0 1 0 1785941812 170147840 38217 4294967295 134512640 135167914 3221224448 3221223152 134562782 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41540 38217 162 162 0 41378 0 [pid=12312] vsize: 166160 Current children cumulated CPU time (s) 648 Current children cumulated vsize (Kb) 168288 [startup+660.064 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39796 0 3 0 65608 189 0 0 25 0 1 0 1785941812 170545152 38315 4294967295 134512640 135167914 3221224448 3221223168 134560230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41637 38315 162 162 0 41475 0 [pid=12312] vsize: 166548 Current children cumulated CPU time (s) 657.99 Current children cumulated vsize (Kb) 168676 [startup+670.064 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39892 0 3 0 66607 190 0 0 25 0 1 0 1785941812 170938368 38411 4294967295 134512640 135167914 3221224448 3221223120 134562373 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41733 38411 162 162 0 41571 0 [pid=12312] vsize: 166932 Current children cumulated CPU time (s) 667.99 Current children cumulated vsize (Kb) 169060 [startup+680.065 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 39981 0 3 0 67605 190 0 0 25 0 1 0 1785941812 171302912 38500 4294967295 134512640 135167914 3221224448 3221223140 134562696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41822 38500 162 162 0 41660 0 [pid=12312] vsize: 167288 Current children cumulated CPU time (s) 677.97 Current children cumulated vsize (Kb) 169416 [startup+690.066 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40074 0 3 0 68604 191 0 0 25 0 1 0 1785941812 171683840 38593 4294967295 134512640 135167914 3221224448 3221223168 134560973 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 41915 38593 162 162 0 41753 0 [pid=12312] vsize: 167660 Current children cumulated CPU time (s) 687.97 Current children cumulated vsize (Kb) 169788 [startup+700.067 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40168 0 3 0 69602 192 0 0 25 0 1 0 1785941812 172064768 38687 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42008 38687 162 162 0 41846 0 [pid=12312] vsize: 168032 Current children cumulated CPU time (s) 697.96 Current children cumulated vsize (Kb) 170160 [startup+710.068 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40268 0 3 0 70601 192 0 0 25 0 1 0 1785941812 172466176 38787 4294967295 134512640 135167914 3221224448 3221223152 134563051 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42106 38787 162 162 0 41944 0 [pid=12312] vsize: 168424 Current children cumulated CPU time (s) 707.95 Current children cumulated vsize (Kb) 170552 [startup+720.068 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40315 0 3 0 71600 193 0 0 25 0 1 0 1785941812 172654592 38834 4294967295 134512640 135167914 3221224448 3221223028 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42152 38834 162 162 0 41990 0 [pid=12312] vsize: 168608 Current children cumulated CPU time (s) 717.95 Current children cumulated vsize (Kb) 170736 [startup+730.069 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40371 0 3 0 72599 193 0 0 25 0 1 0 1785941812 172879872 38890 4294967295 134512640 135167914 3221224448 3221223152 134562891 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42207 38890 162 162 0 42045 0 [pid=12312] vsize: 168828 Current children cumulated CPU time (s) 727.94 Current children cumulated vsize (Kb) 170956 [startup+740.07 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40427 0 3 0 73598 193 0 0 25 0 1 0 1785941812 173109248 38946 4294967295 134512640 135167914 3221224448 3221223152 134562531 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42263 38946 162 162 0 42101 0 [pid=12312] vsize: 169052 Current children cumulated CPU time (s) 737.93 Current children cumulated vsize (Kb) 171180 [startup+750.071 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40502 0 3 0 74596 194 0 0 25 0 1 0 1785941812 173408256 39021 4294967295 134512640 135167914 3221224448 3221223152 134562815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42336 39021 162 162 0 42174 0 [pid=12312] vsize: 169344 Current children cumulated CPU time (s) 747.92 Current children cumulated vsize (Kb) 171472 [startup+760.072 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40535 0 3 0 75596 194 0 0 25 0 1 0 1785941812 173539328 39054 4294967295 134512640 135167914 3221224448 3221223152 134562682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42368 39054 162 162 0 42206 0 [pid=12312] vsize: 169472 Current children cumulated CPU time (s) 757.92 Current children cumulated vsize (Kb) 171600 [startup+770.073 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40579 0 3 0 76595 195 0 0 25 0 1 0 1785941812 173719552 39098 4294967295 134512640 135167914 3221224448 3221223120 134562221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42412 39098 162 162 0 42250 0 [pid=12312] vsize: 169648 Current children cumulated CPU time (s) 767.92 Current children cumulated vsize (Kb) 171776 [startup+780.074 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40609 0 3 0 77595 195 0 0 25 0 1 0 1785941812 173838336 39128 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42441 39128 162 162 0 42279 0 [pid=12312] vsize: 169764 Current children cumulated CPU time (s) 777.92 Current children cumulated vsize (Kb) 171892 [startup+790.075 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40640 0 3 0 78594 196 0 0 25 0 1 0 1785941812 173973504 39159 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42474 39159 162 162 0 42312 0 [pid=12312] vsize: 169896 Current children cumulated CPU time (s) 787.92 Current children cumulated vsize (Kb) 172024 [startup+800.076 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40665 0 3 0 79593 197 0 0 25 0 1 0 1785941812 174075904 39184 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42499 39184 162 162 0 42337 0 [pid=12312] vsize: 169996 Current children cumulated CPU time (s) 797.92 Current children cumulated vsize (Kb) 172124 [startup+810.078 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40688 0 3 0 80593 197 0 0 25 0 1 0 1785941812 174170112 39207 4294967295 134512640 135167914 3221224448 3221223016 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42522 39207 162 162 0 42360 0 [pid=12312] vsize: 170088 Current children cumulated CPU time (s) 807.92 Current children cumulated vsize (Kb) 172216 [startup+820.079 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40720 0 3 0 81593 197 0 0 25 0 1 0 1785941812 174297088 39239 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42553 39239 162 162 0 42391 0 [pid=12312] vsize: 170212 Current children cumulated CPU time (s) 817.92 Current children cumulated vsize (Kb) 172340 [startup+830.081 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40754 0 3 0 82592 197 0 0 25 0 1 0 1785941812 174436352 39273 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42587 39273 162 162 0 42425 0 [pid=12312] vsize: 170348 Current children cumulated CPU time (s) 827.91 Current children cumulated vsize (Kb) 172476 [startup+840.081 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40788 0 3 0 83592 197 0 0 25 0 1 0 1785941812 174571520 39307 4294967295 134512640 135167914 3221224448 3221223120 134562370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42620 39307 162 162 0 42458 0 [pid=12312] vsize: 170480 Current children cumulated CPU time (s) 837.91 Current children cumulated vsize (Kb) 172608 [startup+850.082 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40825 0 3 0 84592 197 0 0 25 0 1 0 1785941812 174723072 39344 4294967295 134512640 135167914 3221224448 3221223120 134562352 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42657 39344 162 162 0 42495 0 [pid=12312] vsize: 170628 Current children cumulated CPU time (s) 847.91 Current children cumulated vsize (Kb) 172756 [startup+860.083 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40855 0 3 0 85592 198 0 0 25 0 1 0 1785941812 174845952 39374 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42687 39374 162 162 0 42525 0 [pid=12312] vsize: 170748 Current children cumulated CPU time (s) 857.92 Current children cumulated vsize (Kb) 172876 [startup+870.084 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40878 0 3 0 86591 198 0 0 25 0 1 0 1785941812 174936064 39397 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42709 39397 162 162 0 42547 0 [pid=12312] vsize: 170836 Current children cumulated CPU time (s) 867.91 Current children cumulated vsize (Kb) 172964 [startup+880.086 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40902 0 3 0 87591 198 0 0 25 0 1 0 1785941812 175034368 39421 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42733 39421 162 162 0 42571 0 [pid=12312] vsize: 170932 Current children cumulated CPU time (s) 877.91 Current children cumulated vsize (Kb) 173060 [startup+890.086 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40932 0 3 0 88591 198 0 0 25 0 1 0 1785941812 175157248 39451 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42763 39451 162 162 0 42601 0 [pid=12312] vsize: 171052 Current children cumulated CPU time (s) 887.91 Current children cumulated vsize (Kb) 173180 [startup+900.087 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40953 0 3 0 89591 198 0 0 25 0 1 0 1785941812 175239168 39472 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42783 39472 162 162 0 42621 0 [pid=12312] vsize: 171132 Current children cumulated CPU time (s) 897.91 Current children cumulated vsize (Kb) 173260 [startup+910.088 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 40982 0 3 0 90590 198 0 0 25 0 1 0 1785941812 175357952 39501 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42812 39501 162 162 0 42650 0 [pid=12312] vsize: 171248 Current children cumulated CPU time (s) 907.9 Current children cumulated vsize (Kb) 173376 [startup+920.089 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41016 0 3 0 91590 199 0 0 25 0 1 0 1785941812 175497216 39535 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42846 39535 162 162 0 42684 0 [pid=12312] vsize: 171384 Current children cumulated CPU time (s) 917.91 Current children cumulated vsize (Kb) 173512 [startup+930.091 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41050 0 3 0 92590 199 0 0 25 0 1 0 1785941812 175632384 39569 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42879 39569 162 162 0 42717 0 [pid=12312] vsize: 171516 Current children cumulated CPU time (s) 927.91 Current children cumulated vsize (Kb) 173644 [startup+940.092 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41079 0 3 0 93590 199 0 0 25 0 1 0 1785941812 175751168 39598 4294967295 134512640 135167914 3221224448 3221223152 134562869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42908 39598 162 162 0 42746 0 [pid=12312] vsize: 171632 Current children cumulated CPU time (s) 937.91 Current children cumulated vsize (Kb) 173760 [startup+950.092 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41127 0 3 0 94589 200 0 0 25 0 1 0 1785941812 175943680 39646 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42955 39646 162 162 0 42793 0 [pid=12312] vsize: 171820 Current children cumulated CPU time (s) 947.91 Current children cumulated vsize (Kb) 173948 [startup+960.093 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41164 0 3 0 95588 200 0 0 25 0 1 0 1785941812 176095232 39683 4294967295 134512640 135167914 3221224448 3221223152 134562531 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 42992 39683 162 162 0 42830 0 [pid=12312] vsize: 171968 Current children cumulated CPU time (s) 957.9 Current children cumulated vsize (Kb) 174096 [startup+970.094 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41207 0 3 0 96587 201 0 0 25 0 1 0 1785941812 176271360 39726 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43035 39726 162 162 0 42873 0 [pid=12312] vsize: 172140 Current children cumulated CPU time (s) 967.9 Current children cumulated vsize (Kb) 174268 [startup+980.095 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41254 0 3 0 97587 201 0 0 25 0 1 0 1785941812 176721920 39773 4294967295 134512640 135167914 3221224448 3221223088 134561550 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43145 39773 162 162 0 42983 0 [pid=12312] vsize: 172580 Current children cumulated CPU time (s) 977.9 Current children cumulated vsize (Kb) 174708 [startup+990.096 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41298 0 3 0 98587 201 0 0 25 0 1 0 1785941812 176902144 39817 4294967295 134512640 135167914 3221224448 3221223120 134562352 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43189 39817 162 162 0 43027 0 [pid=12312] vsize: 172756 Current children cumulated CPU time (s) 987.9 Current children cumulated vsize (Kb) 174884 [startup+1000.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41327 0 3 0 99586 202 0 0 25 0 1 0 1785941812 177020928 39846 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43218 39846 162 162 0 43056 0 [pid=12312] vsize: 172872 Current children cumulated CPU time (s) 997.9 Current children cumulated vsize (Kb) 175000 [startup+1010.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41354 0 3 0 100586 202 0 0 25 0 1 0 1785941812 177127424 39873 4294967295 134512640 135167914 3221224448 3221223132 134562216 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43244 39873 162 162 0 43082 0 [pid=12312] vsize: 172976 Current children cumulated CPU time (s) 1007.9 Current children cumulated vsize (Kb) 175104 [startup+1020.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41381 0 3 0 101586 202 0 0 25 0 1 0 1785941812 177238016 39900 4294967295 134512640 135167914 3221224448 3221223120 134562221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43271 39900 162 162 0 43109 0 [pid=12312] vsize: 173084 Current children cumulated CPU time (s) 1017.9 Current children cumulated vsize (Kb) 175212 [startup+1030.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41405 0 3 0 102585 202 0 0 25 0 1 0 1785941812 177336320 39924 4294967295 134512640 135167914 3221224448 3221223120 134562252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43295 39924 162 162 0 43133 0 [pid=12312] vsize: 173180 Current children cumulated CPU time (s) 1027.89 Current children cumulated vsize (Kb) 175308 [startup+1040.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41436 0 3 0 103585 203 0 0 25 0 1 0 1785941812 177459200 39955 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43325 39955 162 162 0 43163 0 [pid=12312] vsize: 173300 Current children cumulated CPU time (s) 1037.9 Current children cumulated vsize (Kb) 175428 [startup+1050.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41465 0 3 0 104585 203 0 0 25 0 1 0 1785941812 177577984 39984 4294967295 134512640 135167914 3221224448 3221223152 134562479 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43354 39984 162 162 0 43192 0 [pid=12312] vsize: 173416 Current children cumulated CPU time (s) 1047.9 Current children cumulated vsize (Kb) 175544 [startup+1060.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41494 0 3 0 105585 203 0 0 25 0 1 0 1785941812 177696768 40013 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43383 40013 162 162 0 43221 0 [pid=12312] vsize: 173532 Current children cumulated CPU time (s) 1057.9 Current children cumulated vsize (Kb) 175660 [startup+1070.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41523 0 3 0 106585 203 0 0 25 0 1 0 1785941812 177815552 40042 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43412 40042 162 162 0 43250 0 [pid=12312] vsize: 173648 Current children cumulated CPU time (s) 1067.9 Current children cumulated vsize (Kb) 175776 [startup+1080.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41556 0 3 0 107585 204 0 0 25 0 1 0 1785941812 177946624 40075 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43444 40075 162 162 0 43282 0 [pid=12312] vsize: 173776 Current children cumulated CPU time (s) 1077.91 Current children cumulated vsize (Kb) 175904 [startup+1090.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41594 0 3 0 108584 204 0 0 25 0 1 0 1785941812 178102272 40113 4294967295 134512640 135167914 3221224448 3221223152 134562905 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43482 40113 162 162 0 43320 0 [pid=12312] vsize: 173928 Current children cumulated CPU time (s) 1087.9 Current children cumulated vsize (Kb) 176056 [startup+1100.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41631 0 3 0 109583 204 0 0 25 0 1 0 1785941812 178249728 40150 4294967295 134512640 135167914 3221224448 3221223120 134562347 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43518 40150 162 162 0 43356 0 [pid=12312] vsize: 174072 Current children cumulated CPU time (s) 1097.89 Current children cumulated vsize (Kb) 176200 [startup+1110.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41662 0 3 0 110583 205 0 0 25 0 1 0 1785941812 178376704 40181 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43549 40181 162 162 0 43387 0 [pid=12312] vsize: 174196 Current children cumulated CPU time (s) 1107.9 Current children cumulated vsize (Kb) 176324 [startup+1120.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41698 0 3 0 111582 205 0 0 25 0 1 0 1785941812 178524160 40217 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43585 40217 162 162 0 43423 0 [pid=12312] vsize: 174340 Current children cumulated CPU time (s) 1117.89 Current children cumulated vsize (Kb) 176468 [startup+1130.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41726 0 3 0 112582 205 0 0 25 0 1 0 1785941812 178638848 40245 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43613 40245 162 162 0 43451 0 [pid=12312] vsize: 174452 Current children cumulated CPU time (s) 1127.89 Current children cumulated vsize (Kb) 176580 [startup+1140.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41759 0 3 0 113582 205 0 0 25 0 1 0 1785941812 178769920 40278 4294967295 134512640 135167914 3221224448 3221223088 134561482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43645 40278 162 162 0 43483 0 [pid=12312] vsize: 174580 Current children cumulated CPU time (s) 1137.89 Current children cumulated vsize (Kb) 176708 [startup+1150.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41792 0 3 0 114581 205 0 0 25 0 1 0 1785941812 178905088 40311 4294967295 134512640 135167914 3221224448 3221223152 134562562 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43678 40311 162 162 0 43516 0 [pid=12312] vsize: 174712 Current children cumulated CPU time (s) 1147.88 Current children cumulated vsize (Kb) 176840 [startup+1160.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41826 0 3 0 115580 206 0 0 25 0 1 0 1785941812 179044352 40345 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43712 40345 162 162 0 43550 0 [pid=12312] vsize: 174848 Current children cumulated CPU time (s) 1157.88 Current children cumulated vsize (Kb) 176976 [startup+1170.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41867 0 3 0 116579 206 0 0 25 0 1 0 1785941812 179208192 40386 4294967295 134512640 135167914 3221224448 3221223184 134559402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43752 40386 162 162 0 43590 0 [pid=12312] vsize: 175008 Current children cumulated CPU time (s) 1167.87 Current children cumulated vsize (Kb) 177136 [startup+1180.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41905 0 3 0 117579 206 0 0 25 0 1 0 1785941812 179363840 40424 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43790 40424 162 162 0 43628 0 [pid=12312] vsize: 175160 Current children cumulated CPU time (s) 1177.87 Current children cumulated vsize (Kb) 177288 [startup+1190.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41936 0 3 0 118579 206 0 0 25 0 1 0 1785941812 179490816 40455 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43821 40455 162 162 0 43659 0 [pid=12312] vsize: 175284 Current children cumulated CPU time (s) 1187.87 Current children cumulated vsize (Kb) 177412 [startup+1200.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 41970 0 3 0 119578 207 0 0 25 0 1 0 1785941812 179625984 40489 4294967295 134512640 135167914 3221224448 3221223152 134562493 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43854 40489 162 162 0 43692 0 [pid=12312] vsize: 175416 Current children cumulated CPU time (s) 1197.87 Current children cumulated vsize (Kb) 177544 [startup+1210.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 42000 0 3 0 120578 207 0 0 25 0 1 0 1785941812 179748864 40519 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43884 40519 162 162 0 43722 0 [pid=12312] vsize: 175536 Current children cumulated CPU time (s) 1207.87 Current children cumulated vsize (Kb) 177664 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 12312 Raw data (/proc/12307/stat): 12307 (minisat+_script) S 12306 12307 31778 0 -1 0 314 332 0 0 0 1 0 1 20 0 1 0 1785941805 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12307/statm): 532 234 485 147 0 385 0 [pid=12307] vsize: 2128 Raw data (/proc/12312/stat): 12312 (minisat+_bignum) R 12307 12307 31778 0 -1 0 42000 0 3 0 120578 207 0 0 25 0 1 0 1785941812 179748864 40519 4294967295 134512640 135167914 3221224448 3221223152 134562533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12312/statm): 43884 40519 162 162 0 43722 0 [pid=12312] vsize: 175536 Current children cumulated CPU time (s) 1207.87 Current children cumulated vsize (Kb) 177664 Sending SIGTERM to -12307 Sleeping 2 seconds One traced child (pid=12307) ended because it received signal 15 (SIGTERM) One traced child (pid=12312) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1207.94 CPU user time (s): 1205.79 CPU system time (s): 2.15067 CPU usage (%): 99.813 Max. virtual memory (cumulated for all children) (Kb): 177664
ERROR: no interpretation found !