%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV533-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n020.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 11.25s 3.76s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV533-1.010 : TPTP v9.0.0. Released v4.0.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 03:54:34 EDT 2025 % 0.13/0.34 % CPUTime : % 11.25/3.76 % 11.25/3.76 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.25/3.76 % 11.25/3.76 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.25/3.77 %$ store > select > #nlpp > i9 > i8 > i7 > i6 > i5 > i4 > i3 > i2 > i1 > i0 > e_1318 > e_1316 > e_1314 > e_1312 > e_1310 > e_1308 > e_1305 > e_1303 > e_1301 > e_1299 > e_1297 > e_1295 > e_1293 > e_1291 > e_1289 > e_1287 > e_1285 > e_1281 > e_1279 > e_1277 > e_1275 > e_1273 > e_1271 > e_1268 > e_1266 > e_1264 > e_1262 > e_1260 > e_1258 > e_1256 > e_1254 > e_1252 > e_1250 > e_1248 > e_1246 > e_1244 > a_1319 > a_1317 > a_1315 > a_1313 > a_1311 > a_1309 > a_1307 > a_1306 > a_1304 > a_1302 > a_1300 > a_1298 > a_1296 > a_1294 > a_1292 > a_1290 > a_1288 > a_1286 > a_1284 > a_1283 > a_1282 > a_1280 > a_1278 > a_1276 > a_1274 > a_1272 > a_1270 > a_1269 > a_1267 > a_1265 > a_1263 > a_1261 > a_1259 > a_1257 > a_1255 > a_1253 > a_1251 > a_1249 > a_1247 > a_1245 > a1 % 11.25/3.77 % 11.25/3.77 %Foreground sorts: % 11.25/3.77 % 11.25/3.77 % 11.25/3.77 %Background operators: % 11.25/3.77 % 11.25/3.77 % 11.25/3.77 %Foreground operators: % 11.25/3.77 tff(e_1256, type, e_1256: $i). % 11.25/3.77 tff(a1, type, a1: $i). % 11.25/3.77 tff(e_1244, type, e_1244: $i). % 11.25/3.77 tff(e_1281, type, e_1281: $i). % 11.25/3.77 tff(a_1304, type, a_1304: $i). % 11.25/3.77 tff(e_1301, type, e_1301: $i). % 11.25/3.77 tff(a_1292, type, a_1292: $i). % 11.25/3.77 tff(a_1257, type, a_1257: $i). % 11.25/3.77 tff(a_1282, type, a_1282: $i). % 11.25/3.77 tff(a_1278, type, a_1278: $i). % 11.25/3.77 tff(a_1284, type, a_1284: $i). % 11.25/3.77 tff(e_1271, type, e_1271: $i). % 11.25/3.77 tff(e_1287, type, e_1287: $i). % 11.25/3.77 tff(a_1306, type, a_1306: $i). % 11.25/3.77 tff(a_1270, type, a_1270: $i). % 11.25/3.77 tff(e_1310, type, e_1310: $i). % 11.25/3.77 tff(a_1255, type, a_1255: $i). % 11.25/3.77 tff(a_1265, type, a_1265: $i). % 11.25/3.77 tff(a_1311, type, a_1311: $i). % 11.25/3.77 tff(e_1303, type, e_1303: $i). % 11.25/3.77 tff(a_1269, type, a_1269: $i). % 11.25/3.77 tff(a_1313, type, a_1313: $i). % 11.25/3.77 tff(e_1258, type, e_1258: $i). % 11.25/3.77 tff(e_1312, type, e_1312: $i). % 11.25/3.77 tff(a_1294, type, a_1294: $i). % 11.25/3.77 tff(a_1290, type, a_1290: $i). % 11.25/3.77 tff(store, type, store: ($i * $i * $i) > $i). % 11.25/3.77 tff(e_1318, type, e_1318: $i). % 11.25/3.77 tff(e_1248, type, e_1248: $i). % 11.25/3.77 tff(a_1307, type, a_1307: $i). % 11.25/3.77 tff(e_1275, type, e_1275: $i). % 11.25/3.77 tff(a_1300, type, a_1300: $i). % 11.25/3.77 tff(a_1280, type, a_1280: $i). % 11.25/3.77 tff(a_1245, type, a_1245: $i). % 11.25/3.77 tff(e_1268, type, e_1268: $i). % 11.25/3.77 tff(e_1277, type, e_1277: $i). % 11.25/3.77 tff(a_1272, type, a_1272: $i). % 11.25/3.77 tff(e_1264, type, e_1264: $i). % 11.25/3.77 tff(a_1253, type, a_1253: $i). % 11.25/3.77 tff(e_1246, type, e_1246: $i). % 11.25/3.77 tff(e_1297, type, e_1297: $i). % 11.25/3.77 tff(a_1302, type, a_1302: $i). % 11.25/3.77 tff(e_1279, type, e_1279: $i). % 11.25/3.77 tff(a_1276, type, a_1276: $i). % 11.25/3.77 tff(e_1254, type, e_1254: $i). % 11.25/3.77 tff(a_1298, type, a_1298: $i). % 11.25/3.77 tff(e_1291, type, e_1291: $i). % 11.25/3.77 tff(a_1283, type, a_1283: $i). % 11.25/3.77 tff(a_1247, type, a_1247: $i). % 11.25/3.77 tff(e_1250, type, e_1250: $i). % 11.25/3.77 tff(i8, type, i8: $i). % 11.25/3.77 tff(e_1266, type, e_1266: $i). % 11.25/3.77 tff(i9, type, i9: $i). % 11.25/3.77 tff(e_1314, type, e_1314: $i). % 11.25/3.77 tff(a_1259, type, a_1259: $i). % 11.25/3.77 tff(e_1316, type, e_1316: $i). % 11.25/3.77 tff(i7, type, i7: $i). % 11.25/3.77 tff(i1, type, i1: $i). % 11.25/3.77 tff(a_1249, type, a_1249: $i). % 11.25/3.77 tff(i2, type, i2: $i). % 11.25/3.77 tff(select, type, select: ($i * $i) > $i). % 11.25/3.77 tff(a_1309, type, a_1309: $i). % 11.25/3.77 tff(a_1315, type, a_1315: $i). % 11.25/3.77 tff(a_1319, type, a_1319: $i). % 11.25/3.77 tff(a_1251, type, a_1251: $i). % 11.25/3.77 tff(e_1289, type, e_1289: $i). % 11.25/3.77 tff(e_1262, type, e_1262: $i). % 11.25/3.77 tff(a_1286, type, a_1286: $i). % 11.25/3.77 tff(e_1305, type, e_1305: $i). % 11.25/3.77 tff(a_1274, type, a_1274: $i). % 11.25/3.77 tff(a_1288, type, a_1288: $i). % 11.25/3.77 tff(a_1317, type, a_1317: $i). % 11.25/3.77 tff(e_1295, type, e_1295: $i). % 11.25/3.77 tff(e_1299, type, e_1299: $i). % 11.25/3.77 tff(i0, type, i0: $i). % 11.25/3.77 tff(a_1296, type, a_1296: $i). % 11.25/3.77 tff(a_1261, type, a_1261: $i). % 11.25/3.77 tff(i5, type, i5: $i). % 11.25/3.77 tff(e_1252, type, e_1252: $i). % 11.25/3.77 tff(e_1273, type, e_1273: $i). % 11.25/3.77 tff(a_1267, type, a_1267: $i). % 11.25/3.77 tff(i4, type, i4: $i). % 11.25/3.77 tff(e_1260, type, e_1260: $i). % 11.25/3.77 tff(a_1263, type, a_1263: $i). % 11.25/3.77 tff(e_1293, type, e_1293: $i). % 11.25/3.77 tff(e_1308, type, e_1308: $i). % 11.25/3.77 tff(i3, type, i3: $i). % 11.25/3.77 tff(e_1285, type, e_1285: $i). % 11.25/3.77 tff(i6, type, i6: $i). % 11.25/3.77 % 11.25/3.77 %Saturated clause set: % 11.25/3.77 tff(c_7841, plain, (![J_5]: (select(a_1319, J_5)=select(a_1317, J_5) | i0=J_5))). % 11.25/3.77 tff(c_6594, plain, (![J_14]: (select(a_1276, J_14)=select(a_1274, J_14) | i0=J_14))). % 11.25/3.77 tff(c_2452, plain, (![J_14]: (select(a_1300, J_14)=select(a_1298, J_14) | i0=J_14))). % 11.25/3.77 tff(c_2861, plain, (![J_14]: (select(a_1257, J_14)=select(a_1255, J_14) | i0=J_14))). % 11.25/3.77 tff(c_2458, plain, (![J_14]: (select(a_1283, J_14)=select(a1, J_14) | i0=J_14))). % 11.25/3.77 tff(c_7739, plain, (![J_14]: (select(a_1280, J_14)=select(a_1278, J_14) | i0=J_14))). % 11.25/3.77 tff(c_7628, plain, (store(a_1290, i6, e_1246)=a_1292)). % 11.25/3.77 tff(c_1899, plain, (![J_14]: (select(a_1282, J_14)=select(a_1280, J_14) | i0=J_14))). % 11.25/3.77 tff(c_7626, plain, (select(a_1286, i0)=e_1246)). % 11.25/3.77 tff(c_7629, plain, (select(a_1292, i6)=e_1246)). % 11.25/3.77 tff(c_7627, plain, (select(a_1288, i0)=e_1246)). % 11.25/3.77 tff(c_7649, plain, (![J_5]: (select(a_1313, J_5)=select(a_1311, J_5) | i0=J_5))). % 11.25/3.77 tff(c_7625, plain, (select(a_1284, i0)=e_1246)). % 11.25/3.77 tff(c_7619, plain, (e_1291=e_1246)). % 11.25/3.77 tff(c_1463, plain, (![J_14]: (select(a_1284, J_14)=select(a_1283, J_14) | i6=J_14))). % 11.25/3.77 tff(c_1072, plain, (![J_14]: (select(a_1298, J_14)=select(a_1296, J_14) | i0=J_14))). % 11.25/3.77 tff(c_1073, plain, (![J_14]: (select(a_1272, J_14)=select(a_1270, J_14) | i0=J_14))). % 11.25/3.77 tff(c_1464, plain, (![J_14]: (select(a_1245, J_14)=select(a1, J_14) | i6=J_14))). % 11.25/3.77 tff(c_7521, plain, (![J_14]: (select(a_1296, J_14)=select(a_1294, J_14) | i0=J_14))). % 11.25/3.77 tff(c_6916, plain, (store(a_1280, i0, e_1244)=a_1282)). % 11.25/3.77 tff(c_1897, plain, (![J_14]: (select(a_1267, J_14)=select(a_1265, J_14) | i0=J_14))). % 11.25/3.77 tff(c_6915, plain, (store(a_1278, i0, e_1244)=a_1280)). % 11.25/3.77 tff(c_6737, plain, (store(a_1315, i0, e_1244)=a_1317)). % 11.25/3.77 tff(c_6736, plain, (store(a_1317, i0, e_1244)=a_1319)). % 11.25/3.77 tff(c_6352, plain, (store(a_1253, i0, e_1244)=a_1255)). % 11.25/3.77 tff(c_6517, plain, (store(a_1292, i0, e_1244)=a_1294)). % 11.25/3.78 tff(c_6354, plain, (store(a_1249, i6, e_1244)=a_1251)). % 11.25/3.78 tff(c_6850, plain, (store(a_1251, i6, e_1246)=a_1253)). % 11.25/3.78 tff(c_7397, plain, (store(a_1311, i0, e_1244)=a_1313)). % 11.25/3.78 tff(c_7385, plain, (store(a_1307, i0, e_1244)=a_1309)). % 11.25/3.78 tff(c_7373, plain, (store(a_1259, i0, e_1244)=a_1261)). % 11.25/3.78 tff(c_7361, plain, (store(a_1309, i0, e_1244)=a_1311)). % 11.25/3.78 tff(c_7349, plain, (store(a_1304, i0, e_1244)=a_1306)). % 11.25/3.78 tff(c_7337, plain, (store(a_1306, i0, e_1244)=a_1307)). % 11.25/3.78 tff(c_7324, plain, (store(a_1257, i0, e_1244)=a_1259)). % 11.25/3.78 tff(c_7312, plain, (store(a_1261, i0, e_1244)=a_1263)). % 11.25/3.78 tff(c_7300, plain, (store(a_1255, i0, e_1244)=a_1257)). % 11.25/3.78 tff(c_1893, plain, (![J_14]: (select(a_1317, J_14)=select(a_1315, J_14) | i0=J_14))). % 11.25/3.78 tff(c_7269, plain, (store(a_1300, i0, e_1244)=a_1302)). % 11.25/3.78 tff(c_7257, plain, (store(a_1270, i0, e_1244)=a_1272)). % 11.25/3.78 tff(c_7245, plain, (store(a_1274, i0, e_1244)=a_1276)). % 11.25/3.78 tff(c_7233, plain, (store(a_1272, i0, e_1244)=a_1274)). % 11.25/3.78 tff(c_7221, plain, (store(a_1302, i0, e_1244)=a_1304)). % 11.25/3.78 tff(c_7208, plain, (store(a_1267, i0, e_1244)=a_1269)). % 11.25/3.78 tff(c_7196, plain, (store(a_1298, i0, e_1244)=a_1300)). % 11.25/3.78 tff(c_7184, plain, (store(a_1269, i0, e_1244)=a_1270)). % 11.25/3.78 tff(c_7171, plain, (store(a_1265, i0, e_1244)=a_1267)). % 11.25/3.78 tff(c_7159, plain, (store(a_1296, i0, e_1244)=a_1298)). % 11.25/3.78 tff(c_7147, plain, (store(a_1263, i0, e_1244)=a_1265)). % 11.25/3.78 tff(c_7135, plain, (store(a_1294, i0, e_1244)=a_1296)). % 11.25/3.78 tff(c_6738, plain, (select(a_1317, i0)=e_1244)). % 11.25/3.78 tff(c_6918, plain, (select(a_1280, i0)=e_1244)). % 11.25/3.78 tff(c_6917, plain, (select(a_1282, i0)=e_1244)). % 11.25/3.78 tff(c_6739, plain, (select(a_1319, i0)=e_1244)). % 11.25/3.78 tff(c_6336, plain, (select(a_1259, i0)=e_1244)). % 11.25/3.78 tff(c_6355, plain, (select(a_1251, i6)=e_1244)). % 11.25/3.78 tff(c_6520, plain, (select(a_1292, i0)=e_1244)). % 11.25/3.78 tff(c_6955, plain, (select(a_1278, i0)=e_1244)). % 11.25/3.78 tff(c_6338, plain, (select(a_1269, i0)=e_1244)). % 11.25/3.78 tff(c_6341, plain, (select(a_1267, i0)=e_1244)). % 11.25/3.78 tff(c_7021, plain, (![J_5]: (select(a_1290, J_5)=select(a_1288, J_5) | i0=J_5))). % 11.25/3.78 tff(c_6339, plain, (select(a_1270, i0)=e_1244)). % 11.25/3.78 tff(c_6340, plain, (select(a_1265, i0)=e_1244)). % 11.25/3.78 tff(c_6331, plain, (select(a_1261, i0)=e_1244)). % 11.25/3.78 tff(c_6353, plain, (select(a_1255, i0)=e_1244)). % 11.25/3.78 tff(c_6851, plain, (select(a_1253, i6)=e_1246)). % 11.25/3.78 tff(c_6922, plain, (store(a_1276, i0, e_1244)=a_1278)). % 11.25/3.78 tff(c_6507, plain, (select(a_1298, i0)=e_1244)). % 11.25/3.78 tff(c_6920, plain, (e_1279=e_1244)). % 11.25/3.78 tff(c_661, plain, (![J_14]: (select(a_1278, J_14)=select(a_1276, J_14) | i0=J_14))). % 11.25/3.78 tff(c_6919, plain, (e_1281=e_1244)). % 11.25/3.78 tff(c_6900, plain, (e_1277=e_1244)). % 11.25/3.78 tff(c_6332, plain, (select(a_1274, i0)=e_1244)). % 11.25/3.78 tff(c_6849, plain, (select(a_1251, i0)=e_1246)). % 11.25/3.78 tff(c_6871, plain, (select(a_1249, i0)=e_1246)). % 11.25/3.78 tff(c_6784, plain, (select(a_1315, i0)=e_1244)). % 11.25/3.78 tff(c_6844, plain, (e_1252=e_1246)). % 11.25/3.78 tff(c_6816, plain, (![J_14]: (select(a_1251, J_14)=select(a_1249, J_14) | i6=J_14))). % 11.25/3.78 tff(c_6335, plain, (select(a_1257, i0)=e_1244)). % 11.25/3.78 tff(c_6807, plain, (select(a_1276, i0)=e_1244)). % 11.25/3.78 tff(c_6504, plain, (select(a_1306, i0)=e_1244)). % 11.25/3.78 tff(c_6333, plain, (select(a_1272, i0)=e_1244)). % 11.25/3.78 tff(c_6743, plain, (store(a_1313, i0, e_1244)=a_1315)). % 11.25/3.78 tff(c_6337, plain, (select(a_1263, i0)=e_1244)). % 11.25/3.78 tff(c_6740, plain, (e_1316=e_1244)). % 11.25/3.78 tff(c_6741, plain, (e_1318=e_1244)). % 11.25/3.78 tff(c_6748, plain, (![J_14]: (select(a_1265, J_14)=select(a_1263, J_14) | i0=J_14))). % 11.25/3.78 tff(c_6721, plain, (e_1314=e_1244)). % 11.25/3.78 tff(c_6501, plain, (select(a_1311, i0)=e_1244)). % 11.25/3.78 tff(c_6506, plain, (select(a_1300, i0)=e_1244)). % 11.25/3.78 tff(c_6358, plain, (select(a_1247, i6)=e_1244)). % 11.25/3.78 tff(c_6499, plain, (select(a_1309, i0)=e_1244)). % 11.25/3.78 tff(c_6505, plain, (select(a_1302, i0)=e_1244)). % 11.25/3.78 tff(c_6511, plain, (select(a_1294, i0)=e_1244)). % 11.25/3.78 tff(c_6659, plain, (select(a_1313, i0)=e_1244)). % 11.25/3.78 tff(c_6649, plain, (![J_14]: (select(a_1261, J_14)=select(a_1259, J_14) | i0=J_14))). % 11.25/3.78 tff(c_6503, plain, (select(a_1304, i0)=e_1244)). % 11.25/3.78 tff(c_6502, plain, (select(a_1307, i0)=e_1244)). % 11.25/3.78 tff(c_6592, plain, (i3=i0)). % 11.25/3.78 tff(c_6508, plain, (select(a_1296, i0)=e_1244)). % 11.25/3.78 tff(c_6572, plain, (![J_14]: (select(a_1302, J_14)=select(a_1300, J_14) | i0=J_14))). % 11.25/3.78 tff(c_6514, plain, (e_1301=e_1244)). % 11.25/3.78 tff(c_6515, plain, (e_1303=e_1244)). % 11.25/3.78 tff(c_6512, plain, (e_1308=e_1244)). % 11.25/3.78 tff(c_6510, plain, (e_1312=e_1244)). % 11.25/3.78 tff(c_6513, plain, (e_1305=e_1244)). % 11.25/3.78 tff(c_6516, plain, (e_1299=e_1244)). % 11.25/3.78 tff(c_6518, plain, (e_1297=e_1244)). % 11.25/3.78 tff(c_6519, plain, (e_1295=e_1244)). % 11.25/3.78 tff(c_6529, plain, (![J_14]: (select(a_1259, J_14)=select(a_1257, J_14) | i0=J_14))). % 11.25/3.78 tff(c_6509, plain, (e_1310=e_1244)). % 11.25/3.78 tff(c_6498, plain, (e_1293=e_1244)). % 11.25/3.78 tff(c_6415, plain, (select(a_1249, i6)=e_1244)). % 11.25/3.78 tff(c_6356, plain, (e_1254=e_1244)). % 11.25/3.78 tff(c_6357, plain, (e_1250=e_1244)). % 11.25/3.78 tff(c_6351, plain, (e_1256=e_1244)). % 11.25/3.78 tff(c_6439, plain, (![J_14]: (select(a_1294, J_14)=select(a_1292, J_14) | i0=J_14))). % 11.25/3.78 tff(c_6350, plain, (e_1258=e_1244)). % 11.25/3.79 tff(c_6349, plain, (e_1273=e_1244)). % 11.25/3.79 tff(c_6348, plain, (e_1268=e_1244)). % 11.25/3.79 tff(c_6347, plain, (e_1262=e_1244)). % 11.25/3.79 tff(c_6346, plain, (e_1266=e_1244)). % 11.25/3.79 tff(c_6360, plain, (store(a_1247, i6, e_1244)=a_1249)). % 11.25/3.79 tff(c_6342, plain, (e_1260=e_1244)). % 11.25/3.79 tff(c_6343, plain, (e_1264=e_1244)). % 11.25/3.79 tff(c_6344, plain, (e_1271=e_1244)). % 11.25/3.79 tff(c_6369, plain, (![J_14]: (select(a_1288, J_14)=select(a_1286, J_14) | i6=J_14))). % 11.25/3.79 tff(c_6345, plain, (e_1275=e_1244)). % 11.25/3.79 tff(c_6330, plain, (i6!=i0)). % 11.25/3.79 tff(c_6329, plain, (e_1248=e_1244)). % 11.25/3.79 tff(c_3298, plain, (![J_14]: (select(a_1292, J_14)=select(a_1290, J_14) | i6=J_14))). % 11.25/3.79 tff(c_613, plain, (![J_14]: (select(a_1306, J_14)=select(a_1304, J_14) | i0=J_14))). % 11.25/3.79 tff(c_3087, plain, (![J_14]: (select(a_1247, J_14)=select(a_1245, J_14) | i0=J_14))). % 11.25/3.79 tff(c_3039, plain, (![J_14]: (select(a_1311, J_14)=select(a_1309, J_14) | i0=J_14))). % 11.25/3.79 tff(c_649, plain, (![J_14]: (select(a_1270, J_14)=select(a_1269, J_14) | i0=J_14))). % 11.25/3.79 tff(c_2896, plain, (![J_14]: (select(a_1274, J_14)=select(a_1272, J_14) | i0=J_14))). % 11.25/3.79 tff(c_2854, plain, (i4=i0)). % 11.25/3.79 tff(c_2763, plain, (![J_14]: (select(a_1255, J_14)=select(a_1253, J_14) | i0=J_14))). % 11.25/3.79 tff(c_2474, plain, (store(a_1245, i0, e_1246)=a_1247)). % 11.25/3.79 tff(c_643, plain, (![J_14]: (select(a_1286, J_14)=select(a_1284, J_14) | i6=J_14))). % 11.25/3.79 tff(c_2472, plain, (store(a1, i0, e_1246)=a_1283)). % 11.25/3.79 tff(c_682, plain, (![J_14]: (select(a_1315, J_14)=select(a_1313, J_14) | i0=J_14))). % 11.25/3.79 tff(c_2470, plain, (select(a_1247, i0)=e_1246)). % 11.25/3.79 tff(c_2469, plain, (select(a_1283, i0)=e_1246)). % 11.25/3.79 tff(c_2519, plain, (![J_14]: (select(a_1263, J_14)=select(a_1261, J_14) | i0=J_14))). % 11.25/3.79 tff(c_2467, plain, (i9=i0)). % 11.25/3.79 tff(c_2476, plain, (select(a1, i0)=e_1244)). % 11.25/3.79 tff(c_2451, plain, (i7=i0)). % 11.25/3.79 tff(c_2303, plain, (![J_14]: (select(a_1304, J_14)=select(a_1302, J_14) | i0=J_14))). % 11.25/3.79 tff(c_1894, plain, (store(a_1288, i0, e_1244)=a_1290)). % 11.25/3.79 tff(c_2195, plain, (![J_14]: (select(a_1309, J_14)=select(a_1307, J_14) | i0=J_14))). % 11.25/3.79 tff(c_1896, plain, (select(a_1290, i0)=e_1244)). % 11.25/3.79 tff(c_2114, plain, (![J_14]: (select(a_1253, J_14)=select(a_1251, J_14) | i6=J_14))). % 11.25/3.79 tff(c_1891, plain, (i5=i0)). % 11.25/3.79 tff(c_1683, plain, (store(a_1286, i6, e_1244)=a_1288)). % 11.25/3.79 tff(c_1472, plain, (store(a1, i6, e_1244)=a_1245)). % 11.25/3.79 tff(c_1543, plain, (select(a_1288, i6)=e_1244)). % 11.25/3.79 tff(c_1546, plain, (e_1289=e_1244)). % 11.25/3.79 tff(c_1475, plain, (store(a_1283, i6, e_1244)=a_1284)). % 11.25/3.79 tff(c_1538, plain, (e_1287=e_1244)). % 11.25/3.79 tff(c_1468, plain, (select(a_1284, i6)=e_1244)). % 11.25/3.79 tff(c_1465, plain, (select(a_1245, i6)=e_1244)). % 11.25/3.79 tff(c_1478, plain, (select(a1, i6)=e_1246)). % 11.25/3.79 tff(c_1462, plain, (i8=i6)). % 11.25/3.79 tff(c_1260, plain, (i2=i0)). % 11.25/3.79 tff(c_1071, plain, (i1=i0)). % 11.25/3.79 tff(c_658, plain, (![J_14]: (select(a_1307, J_14)=select(a_1306, J_14) | i0=J_14))). % 11.25/3.79 tff(c_679, plain, (![J_14]: (select(a_1249, J_14)=select(a_1247, J_14) | i6=J_14))). % 11.25/3.79 tff(c_688, plain, (![J_14]: (select(a_1269, J_14)=select(a_1267, J_14) | i0=J_14))). % 11.25/3.79 tff(c_778, plain, (store(a_1284, i6, e_1244)=a_1286)). % 11.25/3.79 tff(c_831, plain, (select(a_1286, i6)=e_1244)). % 11.25/3.79 tff(c_773, plain, (e_1285=e_1244)). % 11.25/3.79 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))). % 11.25/3.79 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 11.25/3.79 tff(c_158, plain, (a_1319!=a_1282)). % 11.25/3.79 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.25/3.79 %------------------------------------------------------------------------------