Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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 | 15249 |
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.38 |
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 wulflinc4 THE 2005-04-21 05:05:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17159 boxname=wulflinc4 idbench=1320 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6f47095f2d417d23ced995954e641689 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-p0548.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-p0548.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-p0548.opb IDLAUNCH: 17159 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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 : 451.169 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: 745664 kB Buffers: 28208 kB Cached: 238284 kB SwapCached: 0 kB Active: 39492 kB Inactive: 229808 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 745412 kB SwapTotal: 2097136 kB SwapFree: 2096992 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6816 kB Slab: 14048 kB Committed_AS: 71672 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 05:25:31 (client local time) WITH STATUS 10 IN 1200.24 SECONDS stats: 17159 7 1200.24 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.85 0.97 0.91 2/54 418 Raw data (stat): 418 (runsolver) R 417 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484197167 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0007 s] Raw data (loadavg): 0.87 0.97 0.91 2/54 418 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 14009 0 0 0 967 31 0 0 25 0 1 0 484197167 65110016 13069 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0014 s] Raw data (loadavg): 0.89 0.97 0.91 2/54 418 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 22716 0 0 0 1946 51 0 0 25 0 1 0 484197167 91877376 21446 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.0019 s] Raw data (loadavg): 0.91 0.97 0.91 3/54 418 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 22776 0 0 0 2946 52 0 0 25 0 1 0 484197167 92057600 21506 4294967295 134512640 134672761 3221224544 3221223648 134560235 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.0021 s] Raw data (loadavg): 0.92 0.97 0.91 2/54 418 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 22830 0 0 0 3945 52 0 0 25 0 1 0 484197167 92327936 21560 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.003 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 418 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 22897 0 0 0 4945 52 0 0 25 0 1 0 484197167 92594176 21627 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22606 21627 603 41 0 22565 0 vsize: 90424 [startup+60.0036 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 22930 0 0 0 5946 52 0 0 25 0 1 0 484197167 92729344 21660 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22639 21660 603 41 0 22598 0 vsize: 90556 [startup+70.0037 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23011 0 0 0 6946 52 0 0 25 0 1 0 484197167 93061120 21741 4294967295 134512640 134672761 3221224544 3221223648 134560291 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.0046 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23089 0 0 0 7946 53 0 0 25 0 1 0 484197167 93454336 21819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22816 21819 603 41 0 22775 0 vsize: 91264 [startup+90.0051 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23126 0 0 0 8946 53 0 0 25 0 1 0 484197167 93585408 21856 4294967295 134512640 134672761 3221224544 3221223648 134560246 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.005 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23183 0 0 0 9946 53 0 0 25 0 1 0 484197167 93921280 21913 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22930 21913 603 41 0 22889 0 vsize: 91720 [startup+110.006 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23215 0 0 0 10946 53 0 0 25 0 1 0 484197167 94081024 21945 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22969 21945 603 41 0 22928 0 vsize: 91876 [startup+120.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23239 0 0 0 11945 53 0 0 25 0 1 0 484197167 94081024 21969 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22969 21969 603 41 0 22928 0 vsize: 91876 [startup+130.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23248 0 0 0 12946 53 0 0 25 0 1 0 484197167 94216192 21978 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21978 603 41 0 22961 0 vsize: 92008 [startup+140.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23253 0 0 0 13946 53 0 0 25 0 1 0 484197167 94216192 21983 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21983 603 41 0 22961 0 vsize: 92008 [startup+150.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23262 0 0 0 14946 53 0 0 25 0 1 0 484197167 94216192 21992 4294967295 134512640 134672761 3221224544 3221223648 134560412 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.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23266 0 0 0 15946 53 0 0 25 0 1 0 484197167 94216192 21996 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23002 21996 603 41 0 22961 0 vsize: 92008 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23267 0 0 0 16946 53 0 0 25 0 1 0 484197167 94216192 21997 4294967295 134512640 134672761 3221224544 3221223648 134560243 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.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23268 0 0 0 17946 53 0 0 25 0 1 0 484197167 94216192 21998 4294967295 134512640 134672761 3221224544 3221223648 134560235 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.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23275 0 0 0 18947 53 0 0 25 0 1 0 484197167 94351360 22005 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22005 603 41 0 22994 0 vsize: 92140 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23276 0 0 0 19947 53 0 0 25 0 1 0 484197167 94351360 22006 4294967295 134512640 134672761 3221224544 3221223648 134560260 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.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23279 0 0 0 20947 53 0 0 25 0 1 0 484197167 94351360 22009 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23283 0 0 0 21947 53 0 0 25 0 1 0 484197167 94351360 22013 4294967295 134512640 134672761 3221224544 3221223648 134560355 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.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23284 0 0 0 22947 53 0 0 25 0 1 0 484197167 94351360 22014 4294967295 134512640 134672761 3221224544 3221223648 134560291 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.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23286 0 0 0 23948 53 0 0 25 0 1 0 484197167 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.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23289 0 0 0 24948 53 0 0 25 0 1 0 484197167 94351360 22019 4294967295 134512640 134672761 3221224544 3221223648 134560361 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.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23290 0 0 0 25948 53 0 0 25 0 1 0 484197167 94351360 22020 4294967295 134512640 134672761 3221224544 3221223648 134560252 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.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23292 0 0 0 26948 53 0 0 25 0 1 0 484197167 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.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23293 0 0 0 27948 53 0 0 25 0 1 0 484197167 94351360 22023 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23296 0 0 0 28949 53 0 0 25 0 1 0 484197167 94351360 22026 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23298 0 0 0 29949 53 0 0 25 0 1 0 484197167 94351360 22028 4294967295 134512640 134672761 3221224544 3221223648 134560184 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.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23301 0 0 0 30949 53 0 0 25 0 1 0 484197167 94351360 22031 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22031 603 41 0 22994 0 vsize: 92140 [startup+320.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23302 0 0 0 31949 53 0 0 25 0 1 0 484197167 94351360 22032 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.017 s] Raw data (loadavg): 0.99 0.97 0.91 3/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23304 0 0 0 32949 53 0 0 25 0 1 0 484197167 94351360 22034 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22034 603 41 0 22994 0 vsize: 92140 [startup+340.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23308 0 0 0 33950 53 0 0 25 0 1 0 484197167 94351360 22038 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23035 22038 603 41 0 22994 0 vsize: 92140 [startup+350.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23310 0 0 0 34950 53 0 0 25 0 1 0 484197167 94486528 22040 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22040 603 41 0 23027 0 vsize: 92272 [startup+360.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23312 0 0 0 35950 53 0 0 25 0 1 0 484197167 94486528 22042 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22042 603 41 0 23027 0 vsize: 92272 [startup+370.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23314 0 0 0 36950 53 0 0 25 0 1 0 484197167 94486528 22044 4294967295 134512640 134672761 3221224544 3221223648 134559872 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.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23316 0 0 0 37950 54 0 0 25 0 1 0 484197167 94486528 22046 4294967295 134512640 134672761 3221224544 3221223648 134560402 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.019 s] Raw data (loadavg): 0.99 0.97 0.91 3/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23318 0 0 0 38951 54 0 0 25 0 1 0 484197167 94486528 22048 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22048 603 41 0 23027 0 vsize: 92272 [startup+400.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23321 0 0 0 39951 54 0 0 25 0 1 0 484197167 94486528 22051 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22051 603 41 0 23027 0 vsize: 92272 [startup+410.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23322 0 0 0 40951 54 0 0 25 0 1 0 484197167 94486528 22052 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22052 603 41 0 23027 0 vsize: 92272 [startup+420.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23331 0 0 0 41951 54 0 0 25 0 1 0 484197167 94486528 22061 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23068 22061 603 41 0 23027 0 vsize: 92272 [startup+430.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23368 0 0 0 42951 54 0 0 25 0 1 0 484197167 94621696 22098 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23101 22098 603 41 0 23060 0 vsize: 92404 [startup+440.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23434 0 0 0 43951 54 0 0 25 0 1 0 484197167 94887936 22164 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23166 22164 603 41 0 23125 0 vsize: 92664 [startup+450.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23482 0 0 0 44951 54 0 0 25 0 1 0 484197167 95154176 22212 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23231 22212 603 41 0 23190 0 vsize: 92924 [startup+460.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23496 0 0 0 45951 54 0 0 25 0 1 0 484197167 95154176 22226 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23231 22226 603 41 0 23190 0 vsize: 92924 [startup+470.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23500 0 0 0 46951 54 0 0 25 0 1 0 484197167 95154176 22230 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23231 22230 603 41 0 23190 0 vsize: 92924 [startup+480.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23505 0 0 0 47951 54 0 0 25 0 1 0 484197167 95154176 22235 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23231 22235 603 41 0 23190 0 vsize: 92924 [startup+490.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23509 0 0 0 48951 54 0 0 25 0 1 0 484197167 95289344 22239 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22239 603 41 0 23223 0 vsize: 93056 [startup+500.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23514 0 0 0 49952 54 0 0 25 0 1 0 484197167 95289344 22244 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22244 603 41 0 23223 0 vsize: 93056 [startup+510.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23519 0 0 0 50952 54 0 0 25 0 1 0 484197167 95289344 22249 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22249 603 41 0 23223 0 vsize: 93056 [startup+520.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23528 0 0 0 51952 54 0 0 25 0 1 0 484197167 95289344 22258 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23264 22258 603 41 0 23223 0 vsize: 93056 [startup+530.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23540 0 0 0 52952 55 0 0 25 0 1 0 484197167 95408128 22270 4294967295 134512640 134672761 3221224544 3221223648 134560150 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23293 22270 603 41 0 23252 0 vsize: 93172 [startup+540.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23572 0 0 0 53952 55 0 0 25 0 1 0 484197167 95543296 22302 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23326 22302 603 41 0 23285 0 vsize: 93304 [startup+550.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23594 0 0 0 54952 55 0 0 25 0 1 0 484197167 95543296 22324 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23326 22324 603 41 0 23285 0 vsize: 93304 [startup+560.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23598 0 0 0 55952 55 0 0 25 0 1 0 484197167 95543296 22328 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23614 0 0 0 56953 55 0 0 25 0 1 0 484197167 95666176 22344 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23356 22344 603 41 0 23315 0 vsize: 93424 [startup+580.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23649 0 0 0 57953 55 0 0 25 0 1 0 484197167 95801344 22379 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23389 22379 603 41 0 23348 0 vsize: 93556 [startup+590.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23740 0 0 0 58952 55 0 0 25 0 1 0 484197167 96206848 22470 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23488 22470 603 41 0 23447 0 vsize: 93952 [startup+600.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23808 0 0 0 59952 56 0 0 25 0 1 0 484197167 96477184 22538 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23554 22538 603 41 0 23513 0 vsize: 94216 [startup+610.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23816 0 0 0 60952 56 0 0 25 0 1 0 484197167 96477184 22546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23554 22546 603 41 0 23513 0 vsize: 94216 [startup+620.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 23942 0 0 0 61951 57 0 0 25 0 1 0 484197167 97013760 22672 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23685 22672 603 41 0 23644 0 vsize: 94740 [startup+630.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 24123 0 0 0 62951 57 0 0 25 0 1 0 484197167 97677312 22853 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23847 22853 603 41 0 23806 0 vsize: 95388 [startup+640.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 24282 0 0 0 63951 58 0 0 25 0 1 0 484197167 98353152 23012 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24012 23012 603 41 0 23971 0 vsize: 96048 [startup+650.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 24434 0 0 0 64950 58 0 0 25 0 1 0 484197167 99016704 23164 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24174 23164 603 41 0 24133 0 vsize: 96696 [startup+660.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 24582 0 0 0 65950 59 0 0 25 0 1 0 484197167 99553280 23312 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24305 23312 603 41 0 24264 0 vsize: 97220 [startup+670.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 24718 0 0 0 66950 59 0 0 25 0 1 0 484197167 100237312 23448 4294967295 134512640 134672761 3221224544 3221223648 134560390 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24472 23448 603 41 0 24431 0 vsize: 97888 [startup+680.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 24842 0 0 0 67950 59 0 0 25 0 1 0 484197167 100614144 23572 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24564 23572 603 41 0 24523 0 vsize: 98256 [startup+690.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25028 0 0 0 68949 60 0 0 25 0 1 0 484197167 101552128 23758 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24793 23758 603 41 0 24752 0 vsize: 99172 [startup+700.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25217 0 0 0 69949 60 0 0 25 0 1 0 484197167 102207488 23947 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24953 23947 603 41 0 24912 0 vsize: 99812 [startup+710.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25273 0 0 0 70949 61 0 0 25 0 1 0 484197167 102453248 24003 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25013 24003 603 41 0 24972 0 vsize: 100052 [startup+720.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25280 0 0 0 71949 61 0 0 25 0 1 0 484197167 102588416 24010 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25046 24010 603 41 0 25005 0 vsize: 100184 [startup+730.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25397 0 0 0 72949 61 0 0 25 0 1 0 484197167 102969344 24127 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25139 24127 603 41 0 25098 0 vsize: 100556 [startup+740.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25569 0 0 0 73949 61 0 0 25 0 1 0 484197167 103739392 24299 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25327 24299 603 41 0 25286 0 vsize: 101308 [startup+750.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25755 0 0 0 74949 62 0 0 25 0 1 0 484197167 104509440 24485 4294967295 134512640 134672761 3221224544 3221223728 134559298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25515 24485 603 41 0 25474 0 vsize: 102060 [startup+760.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 25964 0 0 0 75948 62 0 0 25 0 1 0 484197167 105316352 24694 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25712 24694 603 41 0 25671 0 vsize: 102848 [startup+770.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 26143 0 0 0 76948 63 0 0 25 0 1 0 484197167 106094592 24873 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25902 24873 603 41 0 25861 0 vsize: 103608 [startup+780.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 26332 0 0 0 77948 63 0 0 25 0 1 0 484197167 106868736 25062 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26091 25062 603 41 0 26050 0 vsize: 104364 [startup+790.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 26552 0 0 0 78947 64 0 0 25 0 1 0 484197167 107683840 25282 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26290 25282 603 41 0 26249 0 vsize: 105160 [startup+800.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 26775 0 0 0 79947 64 0 0 25 0 1 0 484197167 108634112 25505 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26522 25505 603 41 0 26481 0 vsize: 106088 [startup+810.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 26921 0 0 0 80947 65 0 0 25 0 1 0 484197167 109277184 25651 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26679 25651 603 41 0 26638 0 vsize: 106716 [startup+820.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27087 0 0 0 81947 65 0 0 25 0 1 0 484197167 109969408 25817 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26848 25817 603 41 0 26807 0 vsize: 107392 [startup+830.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27236 0 0 0 82946 65 0 0 25 0 1 0 484197167 110485504 25966 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26974 25966 603 41 0 26933 0 vsize: 107896 [startup+840.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27386 0 0 0 83947 65 0 0 25 0 1 0 484197167 111149056 26116 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27136 26116 603 41 0 27095 0 vsize: 108544 [startup+850.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27452 0 0 0 84946 66 0 0 25 0 1 0 484197167 111411200 26182 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27200 26182 603 41 0 27159 0 vsize: 108800 [startup+860.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27495 0 0 0 85946 66 0 0 25 0 1 0 484197167 111546368 26225 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27233 26225 603 41 0 27192 0 vsize: 108932 [startup+870.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27571 0 0 0 86946 66 0 0 25 0 1 0 484197167 111808512 26301 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27297 26301 603 41 0 27256 0 vsize: 109188 [startup+880.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27600 0 0 0 87946 67 0 0 25 0 1 0 484197167 111943680 26330 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27330 26330 603 41 0 27289 0 vsize: 109320 [startup+890.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27618 0 0 0 88946 67 0 0 25 0 1 0 484197167 112082944 26348 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27364 26348 603 41 0 27323 0 vsize: 109456 [startup+900.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27650 0 0 0 89946 67 0 0 25 0 1 0 484197167 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+910.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27713 0 0 0 90946 67 0 0 25 0 1 0 484197167 112492544 26443 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27464 26443 603 41 0 27423 0 vsize: 109856 [startup+920.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27725 0 0 0 91946 67 0 0 25 0 1 0 484197167 112492544 26455 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27464 26455 603 41 0 27423 0 vsize: 109856 [startup+930.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27738 0 0 0 92946 67 0 0 25 0 1 0 484197167 112492544 26468 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27464 26468 603 41 0 27423 0 vsize: 109856 [startup+940.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27760 0 0 0 93946 67 0 0 25 0 1 0 484197167 112611328 26490 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27493 26490 603 41 0 27452 0 vsize: 109972 [startup+950.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27787 0 0 0 94946 67 0 0 25 0 1 0 484197167 112742400 26517 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27525 26517 603 41 0 27484 0 vsize: 110100 [startup+960.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27812 0 0 0 95946 67 0 0 25 0 1 0 484197167 112873472 26542 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27557 26542 603 41 0 27516 0 vsize: 110228 [startup+970.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27823 0 0 0 96946 67 0 0 25 0 1 0 484197167 112873472 26553 4294967295 134512640 134672761 3221224544 3221223648 134560322 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27557 26553 603 41 0 27516 0 vsize: 110228 [startup+980.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27839 0 0 0 97947 67 0 0 25 0 1 0 484197167 112992256 26569 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27586 26569 603 41 0 27545 0 vsize: 110344 [startup+990.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27851 0 0 0 98947 67 0 0 25 0 1 0 484197167 112992256 26581 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27586 26581 603 41 0 27545 0 vsize: 110344 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27859 0 0 0 99947 67 0 0 25 0 1 0 484197167 112992256 26589 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27586 26589 603 41 0 27545 0 vsize: 110344 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27891 0 0 0 100947 67 0 0 25 0 1 0 484197167 113127424 26621 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27619 26621 603 41 0 27578 0 vsize: 110476 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27900 0 0 0 101947 67 0 0 25 0 1 0 484197167 113246208 26630 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27648 26630 603 41 0 27607 0 vsize: 110592 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27905 0 0 0 102948 67 0 0 25 0 1 0 484197167 113246208 26635 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27648 26635 603 41 0 27607 0 vsize: 110592 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 27912 0 0 0 103948 68 0 0 25 0 1 0 484197167 113246208 26642 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27648 26642 603 41 0 27607 0 vsize: 110592 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28000 0 0 0 104948 68 0 0 25 0 1 0 484197167 113647616 26730 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27746 26730 603 41 0 27705 0 vsize: 110984 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28021 0 0 0 105948 68 0 0 25 0 1 0 484197167 113647616 26751 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27746 26751 603 41 0 27705 0 vsize: 110984 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28051 0 0 0 106948 68 0 0 25 0 1 0 484197167 113778688 26781 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27778 26781 603 41 0 27737 0 vsize: 111112 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28070 0 0 0 107948 68 0 0 25 0 1 0 484197167 113909760 26800 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27810 26800 603 41 0 27769 0 vsize: 111240 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28103 0 0 0 108948 68 0 0 25 0 1 0 484197167 114044928 26833 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27843 26833 603 41 0 27802 0 vsize: 111372 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28122 0 0 0 109948 68 0 0 25 0 1 0 484197167 114044928 26852 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27843 26852 603 41 0 27802 0 vsize: 111372 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28123 0 0 0 110949 68 0 0 25 0 1 0 484197167 114176000 26853 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27875 26853 603 41 0 27834 0 vsize: 111500 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28180 0 0 0 111948 68 0 0 25 0 1 0 484197167 114438144 26910 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27939 26910 603 41 0 27898 0 vsize: 111756 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28242 0 0 0 112948 69 0 0 25 0 1 0 484197167 114692096 26972 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28001 26972 603 41 0 27960 0 vsize: 112004 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28258 0 0 0 113948 69 0 0 25 0 1 0 484197167 114827264 26988 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28034 26988 603 41 0 27993 0 vsize: 112136 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28265 0 0 0 114948 69 0 0 25 0 1 0 484197167 114827264 26995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28034 26995 603 41 0 27993 0 vsize: 112136 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28393 0 0 0 115948 69 0 0 25 0 1 0 484197167 115363840 27123 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28165 27123 603 41 0 28124 0 vsize: 112660 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28541 0 0 0 116948 70 0 0 25 0 1 0 484197167 115908608 27271 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28298 27271 603 41 0 28257 0 vsize: 113192 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 28810 0 0 0 117948 70 0 0 25 0 1 0 484197167 116977664 27540 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28559 27540 603 41 0 28518 0 vsize: 114236 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 29005 0 0 0 118948 70 0 0 25 0 1 0 484197167 117768192 27735 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28752 27735 603 41 0 28711 0 vsize: 115008 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 420 Raw data (stat): 418 (minisat+) R 417 5897 5896 0 -1 0 29042 0 0 0 119947 70 0 0 25 0 1 0 484197167 118034432 27772 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28817 27772 603 41 0 28776 0 vsize: 115268 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 420 Raw data (stat): 418 (minisat+) Z 417 5897 5896 0 -1 12 29045 0 0 0 119947 76 0 0 25 0 1 0 484197167 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.24 CPU user time (s): 1199.48 CPU system time (s): 0.763883 CPU usage (%): 100.012 Max. virtual memory (Kb): 115268 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####