%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV534-1.010 : TPTP v9.0.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:31:04 PM UTC 2025 % Result : Satisfiable 15.67s 5.39s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV534-1.010 : TPTP v9.0.0. Released v4.0.0. % 0.03/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.32 % Computer : n007.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Wed Apr 9 03:55:09 EDT 2025 % 0.13/0.32 % CPUTime : % 15.67/5.39 % 15.67/5.39 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.67/5.40 % 15.67/5.40 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.67/5.41 %$ store > select > #nlpp > i9 > i8 > i7 > i6 > i5 > i4 > i3 > i2 > i1 > i0 > e_1319 > e_1317 > e_1315 > e_1313 > e_1311 > e_1309 > e_1306 > e_1304 > e_1302 > e_1300 > e_1298 > e_1296 > e_1294 > e_1292 > e_1290 > e_1288 > e_1286 > e_1282 > e_1280 > e_1278 > e_1276 > e_1274 > e_1272 > e_1269 > e_1267 > e_1265 > e_1263 > e_1261 > e_1259 > e_1257 > e_1255 > e_1253 > e_1251 > e_1249 > e_1247 > e_1245 > a_1320 > a_1318 > a_1316 > a_1314 > a_1312 > a_1310 > a_1308 > a_1307 > a_1305 > a_1303 > a_1301 > a_1299 > a_1297 > a_1295 > a_1293 > a_1291 > a_1289 > a_1287 > a_1285 > a_1284 > a_1283 > a_1281 > a_1279 > a_1277 > a_1275 > a_1273 > a_1271 > a_1270 > a_1268 > a_1266 > a_1264 > a_1262 > a_1260 > a_1258 > a_1256 > a_1254 > a_1252 > a_1250 > a_1248 > a_1246 > a1 % 15.67/5.41 % 15.67/5.41 %Foreground sorts: % 15.67/5.41 % 15.67/5.41 % 15.67/5.41 %Background operators: % 15.67/5.41 % 15.67/5.41 % 15.67/5.41 %Foreground operators: % 15.67/5.41 tff(a1, type, a1: $i). % 15.67/5.41 tff(e_1319, type, e_1319: $i). % 15.67/5.41 tff(e_1257, type, e_1257: $i). % 15.67/5.41 tff(e_1253, type, e_1253: $i). % 15.67/5.41 tff(a_1308, type, a_1308: $i). % 15.67/5.41 tff(a_1287, type, a_1287: $i). % 15.67/5.41 tff(e_1317, type, e_1317: $i). % 15.67/5.41 tff(e_1306, type, e_1306: $i). % 15.67/5.41 tff(e_1251, type, e_1251: $i). % 15.67/5.41 tff(e_1265, type, e_1265: $i). % 15.67/5.41 tff(e_1298, type, e_1298: $i). % 15.67/5.41 tff(e_1259, type, e_1259: $i). % 15.67/5.41 tff(a_1284, type, a_1284: $i). % 15.67/5.41 tff(a_1291, type, a_1291: $i). % 15.67/5.41 tff(e_1288, type, e_1288: $i). % 15.67/5.41 tff(a_1270, type, a_1270: $i). % 15.67/5.41 tff(a_1289, type, a_1289: $i). % 15.67/5.41 tff(a_1293, type, a_1293: $i). % 15.67/5.41 tff(a_1248, type, a_1248: $i). % 15.67/5.41 tff(e_1313, type, e_1313: $i). % 15.67/5.41 tff(e_1261, type, e_1261: $i). % 15.67/5.41 tff(e_1247, type, e_1247: $i). % 15.67/5.41 tff(e_1290, type, e_1290: $i). % 15.67/5.41 tff(a_1303, type, a_1303: $i). % 15.67/5.41 tff(store, type, store: ($i * $i * $i) > $i). % 15.67/5.41 tff(a_1271, type, a_1271: $i). % 15.67/5.41 tff(e_1249, type, e_1249: $i). % 15.67/5.41 tff(a_1307, type, a_1307: $i). % 15.67/5.41 tff(a_1254, type, a_1254: $i). % 15.67/5.41 tff(e_1296, type, e_1296: $i). % 15.67/5.41 tff(e_1280, type, e_1280: $i). % 15.67/5.41 tff(a_1312, type, a_1312: $i). % 15.67/5.41 tff(e_1315, type, e_1315: $i). % 15.67/5.41 tff(a_1250, type, a_1250: $i). % 15.67/5.41 tff(e_1300, type, e_1300: $i). % 15.67/5.41 tff(e_1309, type, e_1309: $i). % 15.67/5.41 tff(e_1292, type, e_1292: $i). % 15.67/5.41 tff(a_1246, type, a_1246: $i). % 15.67/5.41 tff(a_1295, type, a_1295: $i). % 15.67/5.41 tff(a_1256, type, a_1256: $i). % 15.67/5.41 tff(e_1286, type, e_1286: $i). % 15.67/5.41 tff(a_1301, type, a_1301: $i). % 15.67/5.41 tff(a_1314, type, a_1314: $i). % 15.67/5.41 tff(a_1281, type, a_1281: $i). % 15.67/5.41 tff(a_1283, type, a_1283: $i). % 15.67/5.41 tff(a_1275, type, a_1275: $i). % 15.67/5.41 tff(e_1304, type, e_1304: $i). % 15.67/5.41 tff(a_1310, type, a_1310: $i). % 15.67/5.41 tff(a_1285, type, a_1285: $i). % 15.67/5.41 tff(a_1258, type, a_1258: $i). % 15.67/5.41 tff(i8, type, i8: $i). % 15.67/5.41 tff(a_1262, type, a_1262: $i). % 15.67/5.41 tff(a_1318, type, a_1318: $i). % 15.67/5.41 tff(i9, type, i9: $i). % 15.67/5.41 tff(a_1273, type, a_1273: $i). % 15.67/5.41 tff(e_1267, type, e_1267: $i). % 15.67/5.41 tff(a_1320, type, a_1320: $i). % 15.67/5.41 tff(i7, type, i7: $i). % 15.67/5.41 tff(i1, type, i1: $i). % 15.67/5.41 tff(i2, type, i2: $i). % 15.67/5.41 tff(a_1264, type, a_1264: $i). % 15.67/5.41 tff(e_1311, type, e_1311: $i). % 15.67/5.41 tff(a_1299, type, a_1299: $i). % 15.67/5.41 tff(a_1268, type, a_1268: $i). % 15.67/5.41 tff(e_1263, type, e_1263: $i). % 15.67/5.41 tff(select, type, select: ($i * $i) > $i). % 15.67/5.41 tff(a_1305, type, a_1305: $i). % 15.67/5.41 tff(a_1277, type, a_1277: $i). % 15.67/5.41 tff(e_1255, type, e_1255: $i). % 15.67/5.41 tff(e_1245, type, e_1245: $i). % 15.67/5.41 tff(a_1297, type, a_1297: $i). % 15.67/5.41 tff(e_1269, type, e_1269: $i). % 15.67/5.41 tff(a_1266, type, a_1266: $i). % 15.67/5.41 tff(i0, type, i0: $i). % 15.67/5.41 tff(a_1252, type, a_1252: $i). % 15.67/5.41 tff(a_1316, type, a_1316: $i). % 15.67/5.41 tff(a_1279, type, a_1279: $i). % 15.67/5.41 tff(i5, type, i5: $i). % 15.67/5.41 tff(e_1272, type, e_1272: $i). % 15.67/5.41 tff(a_1260, type, a_1260: $i). % 15.67/5.41 tff(i4, type, i4: $i). % 15.67/5.41 tff(e_1278, type, e_1278: $i). % 15.67/5.41 tff(e_1282, type, e_1282: $i). % 15.67/5.41 tff(e_1274, type, e_1274: $i). % 15.67/5.41 tff(i3, type, i3: $i). % 15.67/5.41 tff(e_1302, type, e_1302: $i). % 15.67/5.41 tff(e_1276, type, e_1276: $i). % 15.67/5.41 tff(e_1294, type, e_1294: $i). % 15.67/5.41 tff(i6, type, i6: $i). % 15.67/5.41 % 15.67/5.41 %Saturated clause set: % 15.76/5.41 tff(c_8575, plain, (![J_14]: (select(a_1277, J_14)=select(a_1275, J_14) | i0=J_14))). % 15.76/5.41 tff(c_9377, plain, (store(a_1318, i0, e_1247)=a_1320)). % 15.76/5.41 tff(c_9293, plain, (store(a_1312, i0, e_1245)=a_1314)). % 15.76/5.41 tff(c_9292, plain, (store(a_1316, i4, e_1245)=a_1318)). % 15.76/5.41 tff(c_9297, plain, (store(a_1314, i0, e_1245)=a_1316)). % 15.76/5.41 tff(c_9302, plain, (store(a_1310, i0, e_1245)=a_1312)). % 15.76/5.41 tff(c_9392, plain, (store(a_1291, i4, e_1247)=a_1293)). % 15.76/5.41 tff(c_9390, plain, (store(a_1297, i0, e_1247)=a_1299)). % 15.76/5.41 tff(c_9314, plain, (store(a_1303, i0, e_1245)=a_1305)). % 15.76/5.41 tff(c_10476, plain, (![J_5]: (select(a_1254, J_5)=select(a_1252, J_5) | i4=J_5))). % 15.76/5.42 tff(c_9303, plain, (store(a_1305, i0, e_1245)=a_1307)). % 15.76/5.42 tff(c_9391, plain, (store(a_1295, i0, e_1247)=a_1297)). % 15.76/5.42 tff(c_9389, plain, (store(a_1299, i0, e_1247)=a_1301)). % 15.76/5.42 tff(c_9388, plain, (store(a_1301, i4, e_1247)=a_1303)). % 15.76/5.42 tff(c_9304, plain, (store(a_1307, i0, e_1245)=a_1308)). % 15.76/5.42 tff(c_9301, plain, (store(a_1308, i0, e_1245)=a_1310)). % 15.76/5.42 tff(c_9704, plain, (store(a_1275, i0, e_1245)=a_1277)). % 15.76/5.42 tff(c_9705, plain, (store(a_1277, i0, e_1245)=a_1279)). % 15.76/5.42 tff(c_9703, plain, (store(a_1281, i0, e_1245)=a_1283)). % 15.76/5.42 tff(c_9702, plain, (store(a_1279, i0, e_1245)=a_1281)). % 15.76/5.42 tff(c_9963, plain, (store(a_1260, i0, e_1247)=a_1262)). % 15.76/5.42 tff(c_9962, plain, (store(a_1262, i0, e_1247)=a_1264)). % 15.76/5.42 tff(c_9965, plain, (store(a_1264, i4, e_1247)=a_1266)). % 15.76/5.42 tff(c_9716, plain, (store(a_1268, i0, e_1245)=a_1270)). % 15.76/5.42 tff(c_9966, plain, (store(a_1252, i4, e_1247)=a_1254)). % 15.76/5.42 tff(c_9718, plain, (store(a_1266, i0, e_1245)=a_1268)). % 15.76/5.42 tff(c_9714, plain, (store(a_1271, i0, e_1245)=a_1273)). % 15.76/5.42 tff(c_9715, plain, (store(a_1273, i0, e_1245)=a_1275)). % 15.76/5.42 tff(c_9717, plain, (store(a_1270, i0, e_1245)=a_1271)). % 15.76/5.42 tff(c_9964, plain, (store(a_1258, i0, e_1247)=a_1260)). % 15.76/5.42 tff(c_10231, plain, (![J_5]: (select(a_1320, J_5)=select(a_1318, J_5) | i0=J_5))). % 15.76/5.42 tff(c_9383, plain, (select(a_1314, i4)=e_1247)). % 15.76/5.42 tff(c_9381, plain, (select(a_1307, i4)=e_1247)). % 15.76/5.42 tff(c_9385, plain, (select(a_1316, i4)=e_1247)). % 15.76/5.42 tff(c_9380, plain, (select(a_1312, i4)=e_1247)). % 15.76/5.42 tff(c_9379, plain, (select(a_1308, i4)=e_1247)). % 15.76/5.42 tff(c_9384, plain, (select(a_1320, i0)=e_1247)). % 15.76/5.42 tff(c_9378, plain, (select(a_1310, i4)=e_1247)). % 15.76/5.42 tff(c_9386, plain, (select(a_1305, i4)=e_1247)). % 15.76/5.42 tff(c_9969, plain, (select(a_1260, i0)=e_1247)). % 15.76/5.42 tff(c_9970, plain, (select(a_1262, i0)=e_1247)). % 15.76/5.42 tff(c_9976, plain, (select(a_1254, i4)=e_1247)). % 15.76/5.42 tff(c_9968, plain, (select(a_1264, i0)=e_1247)). % 15.76/5.42 tff(c_9967, plain, (select(a_1266, i4)=e_1247)). % 15.76/5.42 tff(c_9971, plain, (select(a_1256, i4)=e_1247)). % 15.76/5.42 tff(c_9977, plain, (select(a_1252, i0)=e_1247)). % 15.76/5.42 tff(c_9961, plain, (select(a_1250, i0)=e_1247)). % 15.76/5.42 tff(c_9974, plain, (e_1261=e_1247)). % 15.76/5.42 tff(c_9975, plain, (e_1259=e_1247)). % 15.76/5.42 tff(c_9973, plain, (e_1265=e_1247)). % 15.76/5.42 tff(c_9987, plain, (![J_5]: (select(a_1293, J_5)=select(a_1291, J_5) | i4=J_5))). % 15.76/5.42 tff(c_9972, plain, (e_1263=e_1247)). % 15.76/5.42 tff(c_9953, plain, (e_1253=e_1247)). % 15.76/5.42 tff(c_8014, plain, (![J_14]: (select(a_1250, J_14)=select(a_1248, J_14) | i4=J_14))). % 15.82/5.42 tff(c_9707, plain, (select(a_1281, i0)=e_1245)). % 15.82/5.42 tff(c_9708, plain, (select(a_1277, i0)=e_1245)). % 15.82/5.42 tff(c_9709, plain, (select(a_1279, i0)=e_1245)). % 15.82/5.42 tff(c_9706, plain, (select(a_1283, i0)=e_1245)). % 15.82/5.42 tff(c_9722, plain, (select(a_1270, i0)=e_1245)). % 15.82/5.42 tff(c_9719, plain, (select(a_1275, i0)=e_1245)). % 15.82/5.42 tff(c_9720, plain, (select(a_1273, i0)=e_1245)). % 15.82/5.42 tff(c_9721, plain, (select(a_1271, i0)=e_1245)). % 15.82/5.42 tff(c_9727, plain, (select(a_1268, i0)=e_1245)). % 15.82/5.42 tff(c_9713, plain, (select(a_1262, i4)=e_1245)). % 15.82/5.42 tff(c_9791, plain, (select(a_1260, i4)=e_1245)). % 15.82/5.42 tff(c_9711, plain, (e_1280=e_1245)). % 15.82/5.42 tff(c_9712, plain, (e_1278=e_1245)). % 15.82/5.43 tff(c_8001, plain, (![J_14]: (select(a_1318, J_14)=select(a_1316, J_14) | i4=J_14))). % 15.82/5.43 tff(c_9710, plain, (e_1282=e_1245)). % 15.82/5.43 tff(c_9724, plain, (e_1274=e_1245)). % 15.82/5.43 tff(c_9725, plain, (e_1272=e_1245)). % 15.82/5.43 tff(c_9723, plain, (e_1276=e_1245)). % 15.82/5.43 tff(c_9726, plain, (e_1269=e_1245)). % 15.82/5.43 tff(c_9728, plain, (select(a_1264, i4)=e_1245)). % 15.82/5.43 tff(c_9697, plain, (e_1267=e_1245)). % 15.82/5.43 tff(c_2426, plain, (![J_14]: (select(a_1262, J_14)=select(a_1260, J_14) | i0=J_14))). % 15.82/5.43 tff(c_9295, plain, (select(a_1318, i4)=e_1245)). % 15.82/5.43 tff(c_9296, plain, (select(a_1314, i0)=e_1245)). % 15.82/5.43 tff(c_9298, plain, (select(a_1316, i0)=e_1245)). % 15.82/5.43 tff(c_9382, plain, (select(a_1285, i0)=e_1247)). % 15.82/5.43 tff(c_9393, plain, (select(a_1287, i0)=e_1247)). % 15.82/5.43 tff(c_9395, plain, (select(a_1301, i0)=e_1247)). % 15.82/5.43 tff(c_9305, plain, (select(a_1312, i0)=e_1245)). % 15.82/5.43 tff(c_9306, plain, (select(a_1310, i0)=e_1245)). % 15.82/5.43 tff(c_9307, plain, (select(a_1308, i0)=e_1245)). % 15.82/5.43 tff(c_9396, plain, (select(a_1297, i0)=e_1247)). % 15.82/5.43 tff(c_9394, plain, (select(a_1303, i4)=e_1247)). % 15.82/5.43 tff(c_9313, plain, (select(a_1305, i0)=e_1245)). % 15.82/5.43 tff(c_9294, plain, (select(a_1299, i4)=e_1245)). % 15.82/5.43 tff(c_9402, plain, (select(a_1293, i4)=e_1247)). % 15.82/5.43 tff(c_9308, plain, (select(a_1307, i0)=e_1245)). % 15.82/5.43 tff(c_9397, plain, (select(a_1299, i0)=e_1247)). % 15.82/5.43 tff(c_9403, plain, (select(a_1289, i0)=e_1247)). % 15.82/5.43 tff(c_9438, plain, (select(a_1297, i4)=e_1245)). % 15.82/5.43 tff(c_9387, plain, (e_1319=e_1247)). % 15.82/5.43 tff(c_9300, plain, (e_1315=e_1245)). % 15.82/5.43 tff(c_9299, plain, (e_1317=e_1245)). % 15.82/5.43 tff(c_9401, plain, (e_1296=e_1247)). % 15.82/5.43 tff(c_9400, plain, (e_1298=e_1247)). % 15.82/5.43 tff(c_9399, plain, (e_1300=e_1247)). % 15.82/5.43 tff(c_9398, plain, (e_1302=e_1247)). % 15.82/5.43 tff(c_9347, plain, (e_1292=e_1247)). % 15.82/5.43 tff(c_9310, plain, (e_1311=e_1245)). % 15.82/5.43 tff(c_9315, plain, (select(a_1301, i4)=e_1245)). % 15.82/5.43 tff(c_9311, plain, (e_1309=e_1245)). % 15.82/5.43 tff(c_9312, plain, (e_1306=e_1245)). % 15.82/5.43 tff(c_9309, plain, (e_1313=e_1245)). % 15.82/5.43 tff(c_9321, plain, (![J_14]: (select(a_1285, J_14)=select(a_1284, J_14) | i4=J_14))). % 15.82/5.43 tff(c_9287, plain, (e_1304=e_1245)). % 15.82/5.43 tff(c_1072, plain, (![J_14]: (select(a_1299, J_14)=select(a_1297, J_14) | i0=J_14))). % 15.82/5.43 tff(c_1898, plain, (![J_14]: (select(a_1283, J_14)=select(a_1281, J_14) | i0=J_14))). % 15.82/5.43 tff(c_1073, plain, (![J_14]: (select(a_1273, J_14)=select(a_1271, J_14) | i0=J_14))). % 15.82/5.43 tff(c_1896, plain, (![J_14]: (select(a_1268, J_14)=select(a_1266, J_14) | i0=J_14))). % 15.82/5.43 tff(c_9175, plain, (![J_14]: (select(a_1246, J_14)=select(a1, J_14) | i4=J_14))). % 15.82/5.43 tff(c_9157, plain, (![J_14]: (select(a_1297, J_14)=select(a_1295, J_14) | i0=J_14))). % 15.82/5.43 tff(c_9112, plain, (![J_5]: (select(a_1314, J_5)=select(a_1312, J_5) | i0=J_5))). % 15.82/5.43 tff(c_9076, plain, (![J_14]: (select(a_1281, J_14)=select(a_1279, J_14) | i0=J_14))). % 15.82/5.43 tff(c_9003, plain, (![J_5]: (select(a_1287, J_5)=select(a_1285, J_5) | i4=J_5))). % 15.82/5.43 tff(c_8963, plain, (![J_5]: (select(a_1291, J_5)=select(a_1289, J_5) | i0=J_5))). % 15.82/5.43 tff(c_613, plain, (![J_14]: (select(a_1307, J_14)=select(a_1305, J_14) | i0=J_14))). % 15.82/5.43 tff(c_8825, plain, (![J_14]: (select(a_1312, J_14)=select(a_1310, J_14) | i0=J_14))). % 15.82/5.43 tff(c_8782, plain, (![J_14]: (select(a_1310, J_14)=select(a_1308, J_14) | i0=J_14))). % 15.82/5.43 tff(c_8696, plain, (![J_14]: (select(a_1301, J_14)=select(a_1299, J_14) | i0=J_14))). % 15.82/5.43 tff(c_8609, plain, (![J_14]: (select(a_1252, J_14)=select(a_1250, J_14) | i4=J_14))). % 15.82/5.44 tff(c_8569, plain, (i3=i0)). % 15.82/5.44 tff(c_7992, plain, (store(a_1248, i4, e_1245)=a_1250)). % 15.82/5.44 tff(c_7991, plain, (store(a_1250, i4, e_1245)=a_1252)). % 15.82/5.44 tff(c_8517, plain, (![J_14]: (select(a_1260, J_14)=select(a_1258, J_14) | i0=J_14))). % 15.82/5.44 tff(c_8407, plain, (![J_14]: (select(a_1284, J_14)=select(a1, J_14) | i0=J_14))). % 15.82/5.44 tff(c_8002, plain, (store(a_1287, i4, e_1245)=a_1289)). % 15.82/5.44 tff(c_8009, plain, (store(a_1284, i4, e_1245)=a_1285)). % 15.82/5.44 tff(c_8005, plain, (store(a1, i4, e_1245)=a_1246)). % 15.82/5.44 tff(c_8015, plain, (store(a_1285, i4, e_1245)=a_1287)). % 15.82/5.44 tff(c_682, plain, (![J_14]: (select(a_1316, J_14)=select(a_1314, J_14) | i0=J_14))). % 15.82/5.44 tff(c_7995, plain, (select(a_1248, i4)=e_1245)). % 15.82/5.44 tff(c_7996, plain, (select(a_1252, i4)=e_1245)). % 15.82/5.44 tff(c_7997, plain, (select(a_1250, i4)=e_1245)). % 15.82/5.44 tff(c_8211, plain, (![J_14]: (select(a_1289, J_14)=select(a_1287, J_14) | i4=J_14))). % 15.82/5.44 tff(c_8011, plain, (select(a_1246, i4)=e_1245)). % 15.82/5.44 tff(c_8008, plain, (select(a_1289, i4)=e_1245)). % 15.82/5.44 tff(c_661, plain, (![J_14]: (select(a_1279, J_14)=select(a_1277, J_14) | i0=J_14))). % 15.82/5.44 tff(c_8012, plain, (select(a1, i4)=e_1247)). % 15.82/5.44 tff(c_8010, plain, (select(a_1285, i4)=e_1245)). % 15.82/5.44 tff(c_8062, plain, (![J_14]: (select(a_1275, J_14)=select(a_1273, J_14) | i0=J_14))). % 15.82/5.44 tff(c_8016, plain, (select(a_1287, i4)=e_1245)). % 15.82/5.44 tff(c_7998, plain, (i4!=i0)). % 15.82/5.44 tff(c_8013, plain, (i8=i4)). % 15.82/5.44 tff(c_7970, plain, (i6=i4)). % 15.82/5.44 tff(c_7624, plain, (store(a_1254, i0, e_1245)=a_1256)). % 15.82/5.44 tff(c_7892, plain, (store(a_1293, i4, e_1245)=a_1295)). % 15.82/5.44 tff(c_7891, plain, (select(a_1295, i4)=e_1245)). % 15.82/5.44 tff(c_7890, plain, (select(a_1293, i0)=e_1245)). % 15.82/5.44 tff(c_7884, plain, (e_1294=e_1245)). % 15.82/5.44 tff(c_7789, plain, (store(a_1256, i4, e_1245)=a_1258)). % 15.82/5.44 tff(c_7730, plain, (![J_14]: (select(a_1256, J_14)=select(a_1254, J_14) | i0=J_14))). % 15.82/5.44 tff(c_7625, plain, (select(a_1256, i0)=e_1245)). % 15.82/5.44 tff(c_7622, plain, (select(a_1258, i4)=e_1245)). % 15.82/5.44 tff(c_7629, plain, (e_1251=e_1245)). % 15.82/5.44 tff(c_7628, plain, (e_1255=e_1245)). % 15.82/5.44 tff(c_673, plain, (![J_14]: (select(a_1303, J_14)=select(a_1301, J_14) | i4=J_14))). % 15.82/5.44 tff(c_7623, plain, (e_1257=e_1245)). % 15.82/5.44 tff(c_7620, plain, (e_1249=e_1245)). % 15.82/5.44 tff(c_703, plain, (![J_14]: (select(a_1295, J_14)=select(a_1293, J_14) | i4=J_14))). % 15.82/5.44 tff(c_2445, plain, (store(a1, i0, e_1247)=a_1284)). % 15.82/5.44 tff(c_2568, plain, (![J_14]: (select(a_1248, J_14)=select(a_1246, J_14) | i0=J_14))). % 15.82/5.44 tff(c_2447, plain, (store(a_1246, i0, e_1247)=a_1248)). % 15.82/5.44 tff(c_2443, plain, (select(a_1248, i0)=e_1247)). % 15.82/5.44 tff(c_2442, plain, (select(a_1284, i0)=e_1247)). % 15.82/5.44 tff(c_649, plain, (![J_14]: (select(a_1271, J_14)=select(a_1270, J_14) | i0=J_14))). % 15.82/5.44 tff(c_2440, plain, (i9=i0)). % 15.82/5.44 tff(c_2449, plain, (select(a1, i0)=e_1245)). % 15.82/5.44 tff(c_2425, plain, (i7=i0)). % 15.82/5.44 tff(c_2400, plain, (![J_14]: (select(a_1264, J_14)=select(a_1262, J_14) | i0=J_14))). % 15.82/5.44 tff(c_1893, plain, (store(a_1289, i0, e_1245)=a_1291)). % 15.82/5.44 tff(c_625, plain, (![J_14]: (select(a_1266, J_14)=select(a_1264, J_14) | i4=J_14))). % 15.82/5.44 tff(c_1895, plain, (select(a_1291, i0)=e_1245)). % 15.82/5.44 tff(c_1945, plain, (![J_14]: (select(a_1305, J_14)=select(a_1303, J_14) | i0=J_14))). % 15.82/5.44 tff(c_1891, plain, (i5=i0)). % 15.82/5.44 tff(c_1546, plain, (e_1290=e_1245)). % 15.82/5.44 tff(c_1538, plain, (e_1288=e_1245)). % 15.82/5.44 tff(c_616, plain, (![J_14]: (select(a_1258, J_14)=select(a_1256, J_14) | i4=J_14))). % 15.82/5.44 tff(c_1260, plain, (i2=i0)). % 15.82/5.44 tff(c_1071, plain, (i1=i0)). % 15.82/5.44 tff(c_658, plain, (![J_14]: (select(a_1308, J_14)=select(a_1307, J_14) | i0=J_14))). % 15.82/5.44 tff(c_688, plain, (![J_14]: (select(a_1270, J_14)=select(a_1268, J_14) | i0=J_14))). % 15.82/5.44 tff(c_773, plain, (e_1286=e_1245)). % 15.82/5.44 tff(c_4, plain, (![A_6, I_4, E_7, J_5]: (select(store(A_6, I_4, E_7), J_5)=select(A_6, J_5) | J_5=I_4))). % 15.82/5.44 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 15.82/5.44 tff(c_158, plain, (a_1320!=a_1283)). % 15.82/5.44 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.82/5.44 %------------------------------------------------------------------------------