Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0548.opb |
MD5SUM | 6f47095f2d417d23ced995954e641689 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 14938 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 416 |
Biggest coefficient in the objective function | 11000 |
Number of bits for the biggest coefficient in the objective function | 14 |
Sum of the numbers in the objective function | 96797 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 11000 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 96797 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1236.51 |
Number of variables | 548 |
Total number of constraints | 724 |
Number of constraints which are clauses | 40 |
Number of constraints which are cardinality constraints (but not clauses) | 550 |
Number of constraints which are nor clauses,nor cardinality constraints | 134 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 143 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-21 09:04:05 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12167 boxname=wulflinc11 idbench=936 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6f47095f2d417d23ced995954e641689 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0548.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0548.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p0548.opb IDLAUNCH: 12167 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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: 759760 kB Buffers: 29436 kB Cached: 224748 kB SwapCached: 0 kB Active: 100276 kB Inactive: 156700 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 759508 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6816 kB Slab: 12296 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 09:24:08 (client local time) WITH STATUS 10 IN 1200.26 SECONDS stats: 12167 7 1200.26 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 156 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ssss.s..ssss........................................ c ---[ 164]---> BDD-cost: 12 c ---[ 163]---> BDD-cost: 46 c ---[ 162]---> BDD-cost: 27 c ---[ 161]---> BDD-cost: 8 c ---[ 160]---> BDD-cost: 48 c ---[ 159]---> BDD-cost: 7 c ---[ 157]---> BDD-cost: 75 c ---[ 156]---> BDD-cost: 23 c ---[ 154]---> BDD-cost: 54 c ---[ 153]---> BDD-cost: 8 c ---[ 152]---> BDD-cost: 105 c ---[ 151]---> BDD-cost: 104 c ---[ 150]---> BDD-cost: 120 c ---[ 149]---> BDD-cost: 79 c ---[ 148]---> BDD-cost: 19 c ---[ 147]---> BDD-cost: 115 c ---[ 146]---> BDD-cost: 107 c ---[ 145]---> BDD-cost: 11 c ---[ 144]---> BDD-cost: 55 c ---[ 143]---> BDD-cost: 87 c ---[ 142]---> BDD-cost: 54 c ---[ 141]---> BDD-cost: 164 c ---[ 140]---> BDD-cost: 151 c ---[ 139]---> BDD-cost: 31 c ---[ 138]---> BDD-cost: 26 c ---[ 136]---> BDD-cost: 28 c ---[ 135]---> BDD-cost: 77 c ---[ 134]---> BDD-cost: 153 c ---[ 133]---> BDD-cost: 109 c ---[ 131]---> BDD-cost: 137 c ---[ 130]---> BDD-cost: 6 c ---[ 129]---> BDD-cost: 56 c ---[ 128]---> BDD-cost: 23 c ---[ 127]---> BDD-cost: 7 c ---[ 126]---> BDD-cost: 32 c ---[ 125]---> BDD-cost: 15 c ---[ 123]---> BDD-cost: 14 c ---[ 121]---> BDD-cost: 10 c ---[ 120]---> BDD-cost: 19 c ---[ 119]---> BDD-cost: 12 c ---[ 118]---> BDD-cost: 9 c ---[ 117]---> BDD-cost: 24 c ---[ 116]---> BDD-cost: 11 c ---[ 115]---> BDD-cost: 9 c ---[ 114]---> BDD-cost: 29 c ---[ 112]---> BDD-cost: 6 c ---[ 111]---> BDD-cost: 21 c ---[ 110]---> BDD-cost: 29 c ---[ 109]---> BDD-cost: 51 c ---[ 107]---> BDD-cost: 8 c ---[ 106]---> BDD-cost: 35 c ---[ 105]---> BDD-cost: 24 c ---[ 104]---> BDD-cost: 12 c ---[ 103]---> BDD-cost: 16 c ---[ 102]---> BDD-cost: 29 c ---[ 101]---> BDD-cost: 13 c ---[ 100]---> BDD-cost: 49 c ---[ 99]---> BDD-cost: 60 c ---[ 98]---> BDD-cost: 7 c ---[ 97]---> BDD-cost: 12 c ---[ 96]---> BDD-cost: 9 c ---[ 95]---> BDD-cost: 16 c ---[ 93]---> BDD-cost: 68 c ---[ 92]---> BDD-cost: 78 c ---[ 91]---> BDD-cost: 47 c ---[ 90]---> BDD-cost: 13 c ---[ 89]---> BDD-cost: 68 c ---[ 88]---> BDD-cost: 8 c ---[ 87]---> BDD-cost: 20 c ---[ 86]---> BDD-cost: 18 c ---[ 83]---> BDD-cost: 10 c ---[ 81]---> BDD-cost: 12 c ---[ 80]---> BDD-cost:142726 c ---[ 79]---> BDD-cost: 1478 c ---[ 78]---> BDD-cost: 1140 c ---[ 77]---> BDD-cost: 2534 c ---[ 76]---> BDD-cost: 37 c ---[ 75]---> BDD-cost: 3 c ---[ 73]---> BDD-cost: 3 c ---[ 71]---> BDD-cost: 3 c ---[ 69]---> BDD-cost: 3 c ---[ 67]---> BDD-cost: 3 c ---[ 61]---> BDD-cost: 3 c ---[ 59]---> BDD-cost: 3 c ---[ 57]---> BDD-cost: 3 c ---[ 55]---> BDD-cost: 3 c ---[ 53]---> BDD-cost: 3 c ---[ 47]---> BDD-cost: 3 c ---[ 41]---> BDD-cost: 3 c ---[ 33]---> BDD-cost: 3 c ---[ 31]---> BDD-cost: 3 c ---[ 29]---> BDD-cost: 3 c ---[ 27]---> BDD-cost: 3 c ---[ 25]---> BDD-cost: 3 c ---[ 23]---> BDD-cost: 3 c ---[ 21]---> BDD-cost: 3 c ---[ 19]---> BDD-cost: 3 c ---[ 17]---> BDD-cost: 3 c ---[ 15]---> BDD-cost: 3 c ---[ 13]---> BDD-cost: 49 c ---[ 12]---> BDD-cost: 49 c ---[ 11]---> BDD-cost: 26 c ---[ 10]---> BDD-cost: 5 c ---[ 9]---> BDD-cost: 7 c ---[ 8]---> BDD-cost: 9 c ---[ 7]---> BDD-cost: 11 c ---[ 6]---> BDD-cost: 5 c ---[ 5]---> BDD-cost: 20 c ---[ 4]---> BDD-cost: 4 c ---[ 3]---> BDD-cost: 2 c ---[ 2]---> BDD-cost: 9 c ---[ 1]---> BDD-cost: 2 c ---[ 0]---> BDD-cost: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 444846 1328425 | 148282 0 0 nan | 0.000 % | c | 101 | 441209 1318476 | 163110 98 5432 55.4 | 0.424 % | c | 251 | 441209 1318476 | 179421 248 21498 86.7 | 0.424 % | c | 476 | 441209 1318476 | 197363 473 28197 59.6 | 0.424 % | c | 813 | 438913 1313060 | 217099 798 37190 46.6 | 1.091 % | c ============================================================================== c [1mFound solution: 47049[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:108445 Base: 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 838 | 736455 2007125 | 245485 807 37347 46.3 | 1.091 % | c | 938 | 736455 2007125 | 270033 907 38571 42.5 | 1.054 % | c | 1090 | 736455 2007125 | 297036 1059 39109 36.9 | 1.054 % | c | 1315 | 736455 2007125 | 326740 1284 41364 32.2 | 1.054 % | c | 1654 | 736439 2007089 | 359414 1622 43195 26.6 | 1.056 % | c | 2160 | 736028 2005916 | 395356 2119 93991 44.4 | 1.113 % | c | 2920 | 735716 2004989 | 434891 2873 145416 50.6 | 1.155 % | c | 4059 | 735701 2004944 | 478380 4010 168919 42.1 | 1.157 % | c | 5767 | 735701 2004944 | 526218 5718 198094 34.6 | 1.157 % | c | 8330 | 735614 2004683 | 578840 8278 442134 53.4 | 1.168 % | c | 12175 | 720208 1958823 | 636724 11694 979186 83.7 | 3.194 % | c | 17943 | 719276 1956027 | 700397 17400 2513961 144.5 | 3.317 % | c | 26593 | 711392 1932375 | 770437 25708 4843896 188.4 | 4.337 % | c | 39571 | 699563 1896888 | 847480 37844 6277713 165.9 | 5.897 % | c c *** TERMINATED *** s SATISFIABLE v C1001_bit0 -C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 C1008_bit0 -C1010_bit0 -C1011_bit0 C1012_bit0 -C1013_bit0 -C1014_bit0 -C1015_bit0 -C1016_bit0 C1019_bit0 C1021_bit0 C1022_bit0 -C1023_bit0 -C1024_bit0 -C1025_bit0 -C1026_bit0 C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 -C1034_bit0 -C1035_bit0 -C1038_bit0 -C1040_bit0 C1041_bit0 C1042_bit0 -C1043_bit0 -C1044_bit0 -C1045_bit0 -C1046_bit0 C1049_bit0 C1051_bit0 -C1052_bit0 -C1053_bit0 -C1054_bit0 -C1055_bit0 -C1058_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 -C1063_bit0 -C1064_bit0 -C1066_bit0 -C1067_bit0 -C1068_bit0 -C1069_bit0 -C1070_bit0 -C1072_bit0 -C1073_bit0 -C1074_bit0 -C1075_bit0 -C1076_bit0 -C1077_bit0 -C1079_bit0 C1080_bit0 -C1081_bit0 -C1082_bit0 -C1083_bit0 -C1084_bit0 C1087_bit0 -C1089_bit0 -C1090_bit0 C1091_bit0 C1092_bit0 -C1093_bit0 -C1094_bit0 -C1095_bit0 C1098_bit0 -C1100_bit0 C1101_bit0 C1102_bit0 -C1103_bit0 -C1104_bit0 -C1105_bit0 -C1108_bit0 -C1109_bit0 C1110_bit0 -C1111_bit0 C1112_bit0 C1113_bit0 -C1114_bit0 C1117_bit0 C1119_bit0 C1120_bit0 C1121_bit0 C1122_bit0 -C1123_bit0 -C1124_bit0 -C1125_bit0 C1128_bit0 -C1130_bit0 -C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1137_bit0 -C1139_bit0 -C1140_bit0 -C1141_bit0 -C1142_bit0 -C1143_bit0 -C1145_bit0 -C1146_bit0 -C1147_bit0 -C1148_bit0 -C1149_bit0 -C1151_bit0 -C1152_bit0 -C1153_bit0 -C1154_bit0 -C1155_bit0 -C1156_bit0 -C1158_bit0 -C1159_bit0 C1160_bit0 -C1161_bit0 -C1162_bit0 -C1163_bit0 -C1164_bit0 C1167_bit0 -C1168_bit0 C1169_bit0 C1170_bit0 C1171_bit0 C1172_bit0 C1173_bit0 -C1174_bit0 -C1175_bit0 -C1176_bit0 -C1179_bit0 -C1180_bit0 -C1181_bit0 -C1182_bit0 -C1183_bit0 -C1184_bit0 -C1185_bit0 C1186_bit0 -C1187_bit0 -C1188_bit0 -C1191_bit0 C1192_bit0 C1193_bit0 C1194_bit0 C1195_bit0 C1196_bit0 C1197_bit0 C1198_bit0 C1199_bit0 -C1200_bit0 -C1201_bit0 -C1202_bit0 C1205_bit0 -C1206_bit0 C1207_bit0 -C1208_bit0 C1209_bit0 C1210_bit0 -C1211_bit0 -C1212_bit0 -C1213_bit0 -C1214_bit0 C1215_bit0 C1216_bit0 -C1217_bit0 -C1218_bit0 C1219_bit0 -C1220_bit0 -C1221_bit0 -C1224_bit0 C1225_bit0 -C1226_bit0 -C1227_bit0 -C1228_bit0 -C1229_bit0 C1230_bit0 -C1231_bit0 -C1232_bit0 -C1233_bit0 -C1236_bit0 -C1237_bit0 -C1238_bit0 -C1239_bit0 C1240_bit0 C1241_bit0 -C1242_bit0 -C1243_bit0 -C1244_bit0 -C1245_bit0 -C1246_bit0 -C1249_bit0 -C1250_bit0 -C1251_bit0 -C1252_bit0 -C1253_bit0 C1254_bit0 C1255_bit0 -C1256_bit0 -C1257_bit0 -C1258_bit0 -C1259_bit0 -C1262_bit0 -C1263_bit0 -C1264_bit0 -C1265_bit0 C1266_bit0 C1267_bit0 -C1268_bit0 -C1269_bit0 C1270_bit0 -C1271_bit0 -C1272_bit0 -C1273_bit0 -C1276_bit0 -C1277_bit0 C1278_bit0 C1279_bit0 -C1280_bit0 C1281_bit0 -C1282_bit0 C1283_bit0 -C1284_bit0 -C1285_bit0 -C1286_bit0 C1289_bit0 -C1290_bit0 -C1291_bit0 -C1292_bit0 -C1293_bit0 C1294_bit0 -C1295_bit0 -C1296_bit0 C1297_bit0 -C1298_bit0 C1299_bit0 C1300_bit0 C1303_bit0 -C1304_bit0 C1305_bit0 C1306_bit0 -C1307_bit0 C1308_bit0 C1309_bit0 -C1310_bit0 C1311_bit0 -C1312_bit0 -C1313_bit0 -C1314_bit0 -C1316_bit0 -C1317_bit0 C1318_bit0 C1319_bit0 C1320_bit0 C1321_bit0 C1322_bit0 C1323_bit0 -C1324_bit0 -C1325_bit0 -C1326_bit0 -C1327_bit0 C1328_bit0 -C1329_bit0 -C1330_bit0 C1331_bit0 -C1332_bit0 C1333_bit0 C1334_bit0 C1335_bit0 -C1336_bit0 C1337_bit0 -C1338_bit0 -C1339_bit0 -C1340_bit0 C1342_bit0 -C1343_bit0 -C1344_bit0 -C1345_bit0 C1346_bit0 -C1347_bit0 -C1348_bit0 -C1349_bit0 C1351_bit0 -C1352_bit0 C1353_bit0 -C1354_bit0 C1355_bit0 -C1356_bit0 -C1357_bit0 -C1358_bit0 C1359_bit0 -C1361_bit0 -C1362_bit0 -C1363_bit0 -C1364_bit0 -C1365_bit0 C1366_bit0 C1367_bit0 -C1368_bit0 -C1369_bit0 -C1370_bit0 -C1371_bit0 C1374_bit0 -C1375_bit0 C1376_bit0 C1377_bit0 -C1378_bit0 C1379_bit0 -C1380_bit0 C1381_bit0 -C1382_bit0 -C1383_bit0 -C1384_bit0 -C1387_bit0 -C1388_bit0 C1389_bit0 C1390_bit0 C1391_bit0 -C1392_bit0 C1393_bit0 -C1394_bit0 -C1395_bit0 -C1396_bit0 C1399_bit0 C1400_bit0 C1401_bit0 C1402_bit0 C1403_bit0 -C1404_bit0 -C1405_bit0 C1406_bit0 -C1407_bit0 -C1408_bit0 -C1409_bit0 C1412_bit0 -C1413_bit0 -C1414_bit0 C1415_bit0 -C1416_bit0 -C1417_bit0 C1418_bit0 -C1419_bit0 -C1420_bit0 -C1421_bit0 -C14#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (runsolver) R 31445 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485630909 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0005 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 14009 0 0 0 971 27 0 0 25 0 1 0 485630909 65110016 13069 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15896 13069 603 41 0 15855 0 vsize: 63584 [startup+20.0012 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 22716 0 0 0 1951 47 0 0 25 0 1 0 485630909 91877376 21446 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22431 21446 603 41 0 22390 0 vsize: 89724 [startup+30.0016 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 22776 0 0 0 2951 47 0 0 25 0 1 0 485630909 92057600 21506 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22475 21506 603 41 0 22434 0 vsize: 89900 [startup+40.0018 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 22830 0 0 0 3950 47 0 0 25 0 1 0 485630909 92327936 21560 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22541 21560 603 41 0 22500 0 vsize: 90164 [startup+50.0025 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 22894 0 0 0 4950 48 0 0 25 0 1 0 485630909 92594176 21624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22606 21624 603 41 0 22565 0 vsize: 90424 [startup+60.002 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 22927 0 0 0 5950 48 0 0 25 0 1 0 485630909 92594176 21657 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22606 21657 603 41 0 22565 0 vsize: 90424 [startup+70.0031 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23011 0 0 0 6950 48 0 0 25 0 1 0 485630909 93061120 21741 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22720 21741 603 41 0 22679 0 vsize: 90880 [startup+80.0038 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23083 0 0 0 7950 49 0 0 25 0 1 0 485630909 93323264 21813 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22784 21813 603 41 0 22743 0 vsize: 91136 [startup+90.0033 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31446 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23126 0 0 0 8950 49 0 0 25 0 1 0 485630909 93585408 21856 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22848 21856 603 41 0 22807 0 vsize: 91392 [startup+100.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23182 0 0 0 9950 49 0 0 25 0 1 0 485630909 93921280 21912 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22930 21912 603 41 0 22889 0 vsize: 91720 [startup+110.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23213 0 0 0 10951 49 0 0 25 0 1 0 485630909 94081024 21943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22969 21943 603 41 0 22928 0 vsize: 91876 [startup+120.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23224 0 0 0 11951 49 0 0 25 0 1 0 485630909 94081024 21954 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22969 21954 603 41 0 22928 0 vsize: 91876 [startup+130.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23246 0 0 0 12951 49 0 0 25 0 1 0 485630909 94216192 21976 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21976 603 41 0 22961 0 vsize: 92008 [startup+140.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23251 0 0 0 13951 49 0 0 25 0 1 0 485630909 94216192 21981 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21981 603 41 0 22961 0 vsize: 92008 [startup+150.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23262 0 0 0 14951 49 0 0 25 0 1 0 485630909 94216192 21992 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21992 603 41 0 22961 0 vsize: 92008 [startup+160.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23266 0 0 0 15950 49 0 0 25 0 1 0 485630909 94216192 21996 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23002 21996 603 41 0 22961 0 vsize: 92008 [startup+170.006 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23267 0 0 0 16950 49 0 0 25 0 1 0 485630909 94216192 21997 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21997 603 41 0 22961 0 vsize: 92008 [startup+180.006 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23268 0 0 0 17950 49 0 0 25 0 1 0 485630909 94216192 21998 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21998 603 41 0 22961 0 vsize: 92008 [startup+190.007 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23273 0 0 0 18951 49 0 0 25 0 1 0 485630909 94216192 22003 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 22003 603 41 0 22961 0 vsize: 92008 [startup+200.007 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23276 0 0 0 19951 49 0 0 25 0 1 0 485630909 94351360 22006 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22006 603 41 0 22994 0 vsize: 92140 [startup+210.007 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23279 0 0 0 20951 49 0 0 25 0 1 0 485630909 94351360 22009 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22009 603 41 0 22994 0 vsize: 92140 [startup+220.008 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23283 0 0 0 21951 49 0 0 25 0 1 0 485630909 94351360 22013 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22013 603 41 0 22994 0 vsize: 92140 [startup+230.009 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23284 0 0 0 22952 49 0 0 25 0 1 0 485630909 94351360 22014 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22014 603 41 0 22994 0 vsize: 92140 [startup+240.008 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23286 0 0 0 23952 49 0 0 25 0 1 0 485630909 94351360 22016 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22016 603 41 0 22994 0 vsize: 92140 [startup+250.009 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23289 0 0 0 24952 49 0 0 25 0 1 0 485630909 94351360 22019 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22019 603 41 0 22994 0 vsize: 92140 [startup+260.009 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23290 0 0 0 25952 49 0 0 25 0 1 0 485630909 94351360 22020 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22020 603 41 0 22994 0 vsize: 92140 [startup+270.01 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23292 0 0 0 26952 49 0 0 25 0 1 0 485630909 94351360 22022 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22022 603 41 0 22994 0 vsize: 92140 [startup+280.011 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23293 0 0 0 27953 49 0 0 25 0 1 0 485630909 94351360 22023 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22023 603 41 0 22994 0 vsize: 92140 [startup+290.011 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23296 0 0 0 28953 49 0 0 25 0 1 0 485630909 94351360 22026 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22026 603 41 0 22994 0 vsize: 92140 [startup+300.012 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23298 0 0 0 29953 49 0 0 25 0 1 0 485630909 94351360 22028 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22028 603 41 0 22994 0 vsize: 92140 [startup+310.012 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23299 0 0 0 30953 49 0 0 25 0 1 0 485630909 94351360 22029 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22029 603 41 0 22994 0 vsize: 92140 [startup+320.013 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23302 0 0 0 31953 49 0 0 25 0 1 0 485630909 94351360 22032 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22032 603 41 0 22994 0 vsize: 92140 [startup+330.013 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23303 0 0 0 32954 49 0 0 25 0 1 0 485630909 94351360 22033 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22033 603 41 0 22994 0 vsize: 92140 [startup+340.012 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23306 0 0 0 33954 49 0 0 25 0 1 0 485630909 94351360 22036 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22036 603 41 0 22994 0 vsize: 92140 [startup+350.013 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23309 0 0 0 34954 49 0 0 25 0 1 0 485630909 94486528 22039 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22039 603 41 0 23027 0 vsize: 92272 [startup+360.014 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23310 0 0 0 35954 49 0 0 25 0 1 0 485630909 94486528 22040 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22040 603 41 0 23027 0 vsize: 92272 [startup+370.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23314 0 0 0 36954 49 0 0 25 0 1 0 485630909 94486528 22044 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22044 603 41 0 23027 0 vsize: 92272 [startup+380.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23316 0 0 0 37955 49 0 0 25 0 1 0 485630909 94486528 22046 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22046 603 41 0 23027 0 vsize: 92272 [startup+390.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23317 0 0 0 38955 49 0 0 25 0 1 0 485630909 94486528 22047 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22047 603 41 0 23027 0 vsize: 92272 [startup+400.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23319 0 0 0 39955 49 0 0 25 0 1 0 485630909 94486528 22049 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22049 603 41 0 23027 0 vsize: 92272 [startup+410.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23321 0 0 0 40955 49 0 0 25 0 1 0 485630909 94486528 22051 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22051 603 41 0 23027 0 vsize: 92272 [startup+420.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23325 0 0 0 41955 49 0 0 25 0 1 0 485630909 94486528 22055 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22055 603 41 0 23027 0 vsize: 92272 [startup+430.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23344 0 0 0 42955 50 0 0 25 0 1 0 485630909 94621696 22074 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23101 22074 603 41 0 23060 0 vsize: 92404 [startup+440.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23426 0 0 0 43956 50 0 0 25 0 1 0 485630909 94887936 22156 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23166 22156 603 41 0 23125 0 vsize: 92664 [startup+450.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23452 0 0 0 44956 50 0 0 25 0 1 0 485630909 95019008 22182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23198 22182 603 41 0 23157 0 vsize: 92792 [startup+460.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23494 0 0 0 45956 50 0 0 25 0 1 0 485630909 95154176 22224 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23231 22224 603 41 0 23190 0 vsize: 92924 [startup+470.019 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23499 0 0 0 46956 50 0 0 25 0 1 0 485630909 95154176 22229 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23231 22229 603 41 0 23190 0 vsize: 92924 [startup+480.019 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23503 0 0 0 47956 50 0 0 25 0 1 0 485630909 95154176 22233 4294967295 134512640 134672761 3221224544 3221223648 134560390 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23231 22233 603 41 0 23190 0 vsize: 92924 [startup+490.019 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23508 0 0 0 48956 50 0 0 25 0 1 0 485630909 95289344 22238 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22238 603 41 0 23223 0 vsize: 93056 [startup+500.019 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23513 0 0 0 49956 50 0 0 25 0 1 0 485630909 95289344 22243 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22243 603 41 0 23223 0 vsize: 93056 [startup+510.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23516 0 0 0 50957 50 0 0 25 0 1 0 485630909 95289344 22246 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22246 603 41 0 23223 0 vsize: 93056 [startup+520.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23523 0 0 0 51957 50 0 0 25 0 1 0 485630909 95289344 22253 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22253 603 41 0 23223 0 vsize: 93056 [startup+530.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23537 0 0 0 52957 50 0 0 25 0 1 0 485630909 95289344 22267 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22267 603 41 0 23223 0 vsize: 93056 [startup+540.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23544 0 0 0 53957 50 0 0 25 0 1 0 485630909 95408128 22274 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23293 22274 603 41 0 23252 0 vsize: 93172 [startup+550.021 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23587 0 0 0 54957 50 0 0 25 0 1 0 485630909 95543296 22317 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23326 22317 603 41 0 23285 0 vsize: 93304 [startup+560.021 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23598 0 0 0 55957 50 0 0 25 0 1 0 485630909 95543296 22328 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23326 22328 603 41 0 23285 0 vsize: 93304 [startup+570.022 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23604 0 0 0 56958 50 0 0 25 0 1 0 485630909 95666176 22334 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23356 22334 603 41 0 23315 0 vsize: 93424 [startup+580.022 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23625 0 0 0 57958 50 0 0 25 0 1 0 485630909 95666176 22355 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23356 22355 603 41 0 23315 0 vsize: 93424 [startup+590.022 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23650 0 0 0 58958 50 0 0 25 0 1 0 485630909 95801344 22380 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23389 22380 603 41 0 23348 0 vsize: 93556 [startup+600.023 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23754 0 0 0 59958 51 0 0 25 0 1 0 485630909 96206848 22484 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23488 22484 603 41 0 23447 0 vsize: 93952 [startup+610.022 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23811 0 0 0 60957 51 0 0 25 0 1 0 485630909 96477184 22541 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23554 22541 603 41 0 23513 0 vsize: 94216 [startup+620.023 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 23872 0 0 0 61957 52 0 0 25 0 1 0 485630909 96747520 22602 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23620 22602 603 41 0 23579 0 vsize: 94480 [startup+630.024 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 24030 0 0 0 62956 52 0 0 25 0 1 0 485630909 97419264 22760 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23784 22760 603 41 0 23743 0 vsize: 95136 [startup+640.023 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 24173 0 0 0 63956 53 0 0 25 0 1 0 485630909 97943552 22903 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23912 22903 603 41 0 23871 0 vsize: 95648 [startup+650.024 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 24335 0 0 0 64955 53 0 0 25 0 1 0 485630909 98615296 23065 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24076 23065 603 41 0 24035 0 vsize: 96304 [startup+660.024 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 24499 0 0 0 65955 54 0 0 25 0 1 0 485630909 99282944 23229 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24239 23229 603 41 0 24198 0 vsize: 96956 [startup+670.024 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 24624 0 0 0 66955 54 0 0 25 0 1 0 485630909 99823616 23354 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24371 23354 603 41 0 24330 0 vsize: 97484 [startup+680.024 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 24772 0 0 0 67955 54 0 0 25 0 1 0 485630909 100352000 23502 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24500 23502 603 41 0 24459 0 vsize: 98000 [startup+690.025 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 24907 0 0 0 68955 55 0 0 25 0 1 0 485630909 101015552 23637 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24662 23637 603 41 0 24621 0 vsize: 98648 [startup+700.025 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 25086 0 0 0 69955 55 0 0 25 0 1 0 485630909 101687296 23816 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24826 23816 603 41 0 24785 0 vsize: 99304 [startup+710.025 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 25270 0 0 0 70955 55 0 0 25 0 1 0 485630909 102453248 24000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25013 24000 603 41 0 24972 0 vsize: 100052 [startup+720.025 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 25277 0 0 0 71955 55 0 0 25 0 1 0 485630909 102453248 24007 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25013 24007 603 41 0 24972 0 vsize: 100052 [startup+730.026 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 25330 0 0 0 72955 55 0 0 25 0 1 0 485630909 102723584 24060 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25079 24060 603 41 0 25038 0 vsize: 100316 [startup+740.026 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 25443 0 0 0 73955 56 0 0 25 0 1 0 485630909 103231488 24173 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25203 24173 603 41 0 25162 0 vsize: 100812 [startup+750.027 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 25620 0 0 0 74954 56 0 0 25 0 1 0 485630909 103858176 24350 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25356 24350 603 41 0 25315 0 vsize: 101424 [startup+760.027 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 25807 0 0 0 75954 57 0 0 25 0 1 0 485630909 104644608 24537 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25548 24537 603 41 0 25507 0 vsize: 102192 [startup+770.027 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 26014 0 0 0 76954 57 0 0 25 0 1 0 485630909 105570304 24744 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25774 24744 603 41 0 25733 0 vsize: 103096 [startup+780.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 26180 0 0 0 77954 58 0 0 25 0 1 0 485630909 106233856 24910 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25936 24910 603 41 0 25895 0 vsize: 103744 [startup+790.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 26369 0 0 0 78954 58 0 0 25 0 1 0 485630909 107003904 25099 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26124 25099 603 41 0 26083 0 vsize: 104496 [startup+800.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 26593 0 0 0 79953 58 0 0 25 0 1 0 485630909 107970560 25323 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26360 25323 603 41 0 26319 0 vsize: 105440 [startup+810.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 26795 0 0 0 80953 59 0 0 25 0 1 0 485630909 108769280 25525 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26555 25525 603 41 0 26514 0 vsize: 106220 [startup+820.027 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 26954 0 0 0 81953 59 0 0 25 0 1 0 485630909 109408256 25684 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26711 25684 603 41 0 26670 0 vsize: 106844 [startup+830.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27110 0 0 0 82953 59 0 0 25 0 1 0 485630909 109969408 25840 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26848 25840 603 41 0 26807 0 vsize: 107392 [startup+840.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27262 0 0 0 83953 60 0 0 25 0 1 0 485630909 110608384 25992 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27004 25992 603 41 0 26963 0 vsize: 108016 [startup+850.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27406 0 0 0 84953 60 0 0 25 0 1 0 485630909 111271936 26136 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27166 26136 603 41 0 27125 0 vsize: 108664 [startup+860.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27460 0 0 0 85953 60 0 0 25 0 1 0 485630909 111411200 26190 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27200 26190 603 41 0 27159 0 vsize: 108800 [startup+870.028 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27519 0 0 0 86953 60 0 0 25 0 1 0 485630909 111677440 26249 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27265 26249 603 41 0 27224 0 vsize: 109060 [startup+880.029 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27577 0 0 0 87952 61 0 0 25 0 1 0 485630909 111943680 26307 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27330 26307 603 41 0 27289 0 vsize: 109320 [startup+890.029 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27600 0 0 0 88952 61 0 0 25 0 1 0 485630909 111943680 26330 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27330 26330 603 41 0 27289 0 vsize: 109320 [startup+900.029 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27627 0 0 0 89953 61 0 0 25 0 1 0 485630909 112082944 26357 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27364 26357 603 41 0 27323 0 vsize: 109456 [startup+910.029 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27650 0 0 0 90953 61 0 0 25 0 1 0 485630909 112214016 26380 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27396 26380 603 41 0 27355 0 vsize: 109584 [startup+920.029 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27716 0 0 0 91953 61 0 0 25 0 1 0 485630909 112492544 26446 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27464 26446 603 41 0 27423 0 vsize: 109856 [startup+930.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27727 0 0 0 92953 61 0 0 25 0 1 0 485630909 112492544 26457 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27464 26457 603 41 0 27423 0 vsize: 109856 [startup+940.029 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27741 0 0 0 93953 61 0 0 25 0 1 0 485630909 112627712 26471 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27497 26471 603 41 0 27456 0 vsize: 109988 [startup+950.029 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27760 0 0 0 94953 61 0 0 25 0 1 0 485630909 112611328 26490 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27493 26490 603 41 0 27452 0 vsize: 109972 [startup+960.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27793 0 0 0 95953 61 0 0 25 0 1 0 485630909 112742400 26523 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27525 26523 603 41 0 27484 0 vsize: 110100 [startup+970.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27812 0 0 0 96953 61 0 0 25 0 1 0 485630909 112873472 26542 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27557 26542 603 41 0 27516 0 vsize: 110228 [startup+980.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27823 0 0 0 97953 61 0 0 25 0 1 0 485630909 112873472 26553 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27557 26553 603 41 0 27516 0 vsize: 110228 [startup+990.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27839 0 0 0 98954 61 0 0 25 0 1 0 485630909 112992256 26569 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27586 26569 603 41 0 27545 0 vsize: 110344 [startup+1000.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27851 0 0 0 99954 61 0 0 25 0 1 0 485630909 112992256 26581 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27586 26581 603 41 0 27545 0 vsize: 110344 [startup+1010.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27859 0 0 0 100954 61 0 0 25 0 1 0 485630909 112992256 26589 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27586 26589 603 41 0 27545 0 vsize: 110344 [startup+1020.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27891 0 0 0 101954 61 0 0 25 0 1 0 485630909 113127424 26621 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27619 26621 603 41 0 27578 0 vsize: 110476 [startup+1030.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27900 0 0 0 102954 62 0 0 25 0 1 0 485630909 113246208 26630 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27648 26630 603 41 0 27607 0 vsize: 110592 [startup+1040.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27905 0 0 0 103954 62 0 0 25 0 1 0 485630909 113246208 26635 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27648 26635 603 41 0 27607 0 vsize: 110592 [startup+1050.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27909 0 0 0 104954 62 0 0 25 0 1 0 485630909 113246208 26639 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27648 26639 603 41 0 27607 0 vsize: 110592 [startup+1060.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 27990 0 0 0 105954 62 0 0 25 0 1 0 485630909 113512448 26720 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27713 26720 603 41 0 27672 0 vsize: 110852 [startup+1070.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28021 0 0 0 106954 62 0 0 25 0 1 0 485630909 113647616 26751 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27746 26751 603 41 0 27705 0 vsize: 110984 [startup+1080.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28049 0 0 0 107954 62 0 0 25 0 1 0 485630909 113778688 26779 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27778 26779 603 41 0 27737 0 vsize: 111112 [startup+1090.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28068 0 0 0 108954 62 0 0 25 0 1 0 485630909 113909760 26798 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27810 26798 603 41 0 27769 0 vsize: 111240 [startup+1100.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28103 0 0 0 109955 62 0 0 25 0 1 0 485630909 114044928 26833 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27843 26833 603 41 0 27802 0 vsize: 111372 [startup+1110.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28122 0 0 0 110955 62 0 0 25 0 1 0 485630909 114044928 26852 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27843 26852 603 41 0 27802 0 vsize: 111372 [startup+1120.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28123 0 0 0 111955 63 0 0 25 0 1 0 485630909 114176000 26853 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27875 26853 603 41 0 27834 0 vsize: 111500 [startup+1130.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28180 0 0 0 112955 63 0 0 25 0 1 0 485630909 114438144 26910 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27939 26910 603 41 0 27898 0 vsize: 111756 [startup+1140.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28242 0 0 0 113955 63 0 0 25 0 1 0 485630909 114692096 26972 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28001 26972 603 41 0 27960 0 vsize: 112004 [startup+1150.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28257 0 0 0 114955 63 0 0 25 0 1 0 485630909 114827264 26987 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28034 26987 603 41 0 27993 0 vsize: 112136 [startup+1160.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28265 0 0 0 115955 63 0 0 25 0 1 0 485630909 114827264 26995 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28034 26995 603 41 0 27993 0 vsize: 112136 [startup+1170.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28366 0 0 0 116955 63 0 0 25 0 1 0 485630909 115232768 27096 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28133 27096 603 41 0 28092 0 vsize: 112532 [startup+1180.03 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28488 0 0 0 117955 63 0 0 25 0 1 0 485630909 115773440 27218 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28265 27218 603 41 0 28224 0 vsize: 113060 [startup+1190.04 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 28753 0 0 0 118955 64 0 0 25 0 1 0 485630909 116842496 27483 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28526 27483 603 41 0 28485 0 vsize: 114104 [startup+1200.04 s] Raw data (loadavg): 0.99 1.00 0.97 2/54 31448 Raw data (stat): 31446 (minisat+) R 31445 32461 32460 0 -1 0 29004 0 0 0 119955 65 0 0 25 0 1 0 485630909 117768192 27734 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28752 27734 603 41 0 28711 0 vsize: 115008 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 1.00 0.97 1/54 31448 Raw data (stat): 31446 (minisat+) Z 31445 32461 32460 0 -1 12 29007 0 0 0 119955 71 0 0 25 0 1 0 485630909 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.1 CPU time (s): 1200.26 CPU user time (s): 1199.55 CPU system time (s): 0.710891 CPU usage (%): 100.013 Max. virtual memory (Kb): 115008 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####