%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV538-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 : n023.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:06 PM UTC 2025 % Result : Satisfiable 17.35s 6.47s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWV538-1.010 : TPTP v9.0.0. Released v4.0.0. % 0.04/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 : n023.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:56:24 EDT 2025 % 0.13/0.34 % CPUTime : % 17.35/6.47 % 17.35/6.47 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.35/6.47 % 17.35/6.47 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.35/6.48 %$ store > sk > select > #nlpp > i_1372 > i9 > i8 > i7 > i6 > i5 > i4 > i3 > i2 > i1 > i0 > e_1374 > e_1373 > e_1370 > e_1368 > e_1366 > e_1364 > e_1362 > e_1360 > e_1357 > e_1355 > e_1353 > e_1351 > e_1349 > e_1347 > e_1345 > e_1343 > e_1341 > e_1339 > e_1337 > e_1333 > e_1331 > e_1329 > e_1327 > e_1325 > e_1323 > e_1320 > e_1318 > e_1316 > e_1314 > e_1312 > e_1310 > e_1308 > e_1306 > e_1304 > e_1302 > e_1300 > e_1298 > e_1296 > a_1371 > a_1369 > a_1367 > a_1365 > a_1363 > a_1361 > a_1359 > a_1358 > a_1356 > a_1354 > a_1352 > a_1350 > a_1348 > a_1346 > a_1344 > a_1342 > a_1340 > a_1338 > a_1336 > a_1335 > a_1334 > a_1332 > a_1330 > a_1328 > a_1326 > a_1324 > a_1322 > a_1321 > a_1319 > a_1317 > a_1315 > a_1313 > a_1311 > a_1309 > a_1307 > a_1305 > a_1303 > a_1301 > a_1299 > a_1297 > a1 % 17.35/6.48 % 17.35/6.48 %Foreground sorts: % 17.35/6.48 % 17.35/6.48 % 17.35/6.48 %Background operators: % 17.35/6.48 % 17.35/6.48 % 17.35/6.48 %Foreground operators: % 17.35/6.48 tff(a1, type, a1: $i). % 17.35/6.48 tff(a_1361, type, a_1361: $i). % 17.35/6.48 tff(a_1356, type, a_1356: $i). % 17.35/6.48 tff(e_1351, type, e_1351: $i). % 17.35/6.48 tff(a_1328, type, a_1328: $i). % 17.35/6.48 tff(e_1360, type, e_1360: $i). % 17.35/6.48 tff(a_1338, type, a_1338: $i). % 17.35/6.48 tff(e_1306, type, e_1306: $i). % 17.35/6.48 tff(e_1368, type, e_1368: $i). % 17.35/6.48 tff(a_1350, type, a_1350: $i). % 17.35/6.48 tff(e_1349, type, e_1349: $i). % 17.35/6.48 tff(e_1329, type, e_1329: $i). % 17.35/6.48 tff(e_1298, type, e_1298: $i). % 17.35/6.48 tff(a_1352, type, a_1352: $i). % 17.35/6.48 tff(a_1363, type, a_1363: $i). % 17.35/6.48 tff(a_1321, type, a_1321: $i). % 17.35/6.48 tff(a_1326, type, a_1326: $i). % 17.35/6.48 tff(a_1354, type, a_1354: $i). % 17.35/6.48 tff(e_1310, type, e_1310: $i). % 17.35/6.48 tff(e_1333, type, e_1333: $i). % 17.35/6.48 tff(a_1311, type, a_1311: $i). % 17.35/6.48 tff(a_1342, type, a_1342: $i). % 17.35/6.48 tff(a_1313, type, a_1313: $i). % 17.35/6.48 tff(a_1303, type, a_1303: $i). % 17.35/6.48 tff(e_1312, type, e_1312: $i). % 17.35/6.48 tff(store, type, store: ($i * $i * $i) > $i). % 17.35/6.48 tff(e_1318, type, e_1318: $i). % 17.35/6.48 tff(a_1307, type, a_1307: $i). % 17.35/6.48 tff(e_1296, type, e_1296: $i). % 17.35/6.48 tff(e_1353, type, e_1353: $i). % 17.35/6.48 tff(e_1357, type, e_1357: $i). % 17.35/6.48 tff(a_1336, type, a_1336: $i). % 17.35/6.48 tff(a_1367, type, a_1367: $i). % 17.35/6.48 tff(a_1335, type, a_1335: $i). % 17.35/6.48 tff(e_1355, type, e_1355: $i). % 17.35/6.48 tff(e_1300, type, e_1300: $i). % 17.35/6.48 tff(a_1348, type, a_1348: $i). % 17.35/6.48 tff(a_1359, type, a_1359: $i). % 17.35/6.48 tff(e_1364, type, e_1364: $i). % 17.35/6.48 tff(a_1301, type, a_1301: $i). % 17.35/6.48 tff(e_1323, type, e_1323: $i). % 17.35/6.48 tff(a_1324, type, a_1324: $i). % 17.35/6.48 tff(e_1304, type, e_1304: $i). % 17.35/6.48 tff(a_1358, type, a_1358: $i). % 17.35/6.48 tff(i8, type, i8: $i). % 17.35/6.48 tff(i9, type, i9: $i). % 17.35/6.48 tff(e_1314, type, e_1314: $i). % 17.35/6.48 tff(e_1347, type, e_1347: $i). % 17.35/6.48 tff(sk, type, sk: ($i * $i) > $i). % 17.35/6.48 tff(a_1322, type, a_1322: $i). % 17.35/6.48 tff(e_1316, type, e_1316: $i). % 17.35/6.48 tff(i7, type, i7: $i). % 17.35/6.48 tff(e_1366, type, e_1366: $i). % 17.35/6.48 tff(e_1374, type, e_1374: $i). % 17.35/6.48 tff(i1, type, i1: $i). % 17.35/6.48 tff(a_1344, type, a_1344: $i). % 17.35/6.48 tff(i2, type, i2: $i). % 17.35/6.48 tff(a_1299, type, a_1299: $i). % 17.35/6.48 tff(e_1343, type, e_1343: $i). % 17.35/6.48 tff(select, type, select: ($i * $i) > $i). % 17.35/6.48 tff(e_1345, type, e_1345: $i). % 17.35/6.48 tff(a_1309, type, a_1309: $i). % 17.35/6.48 tff(a_1330, type, a_1330: $i). % 17.35/6.48 tff(a_1305, type, a_1305: $i). % 17.35/6.48 tff(a_1369, type, a_1369: $i). % 17.35/6.48 tff(a_1334, type, a_1334: $i). % 17.35/6.48 tff(e_1370, type, e_1370: $i). % 17.35/6.48 tff(a_1315, type, a_1315: $i). % 17.35/6.48 tff(a_1319, type, a_1319: $i). % 17.35/6.48 tff(e_1339, type, e_1339: $i). % 17.35/6.48 tff(e_1362, type, e_1362: $i). % 17.35/6.48 tff(a_1340, type, a_1340: $i). % 17.35/6.48 tff(e_1320, type, e_1320: $i). % 17.35/6.48 tff(e_1337, type, e_1337: $i). % 17.35/6.48 tff(e_1373, type, e_1373: $i). % 17.35/6.48 tff(a_1317, type, a_1317: $i). % 17.35/6.48 tff(a_1365, type, a_1365: $i). % 17.35/6.48 tff(e_1341, type, e_1341: $i). % 17.35/6.48 tff(a_1297, type, a_1297: $i). % 17.35/6.48 tff(i0, type, i0: $i). % 17.35/6.48 tff(a_1346, type, a_1346: $i). % 17.35/6.48 tff(a_1371, type, a_1371: $i). % 17.35/6.48 tff(e_1331, type, e_1331: $i). % 17.35/6.48 tff(i5, type, i5: $i). % 17.35/6.48 tff(i4, type, i4: $i). % 17.35/6.48 tff(e_1325, type, e_1325: $i). % 17.35/6.48 tff(i_1372, type, i_1372: $i). % 17.35/6.48 tff(e_1308, type, e_1308: $i). % 17.35/6.48 tff(e_1327, type, e_1327: $i). % 17.35/6.48 tff(i3, type, i3: $i). % 17.35/6.48 tff(e_1302, type, e_1302: $i). % 17.35/6.48 tff(a_1332, type, a_1332: $i). % 17.35/6.48 tff(i6, type, i6: $i). % 17.35/6.48 % 17.35/6.48 %Saturated clause set: % 17.35/6.48 tff(c_18535, plain, (![J_14]: (select(a_1365, J_14)=select(a_1363, J_14) | i0=J_14))). % 17.35/6.48 tff(c_19464, plain, (store(a_1367, i0, e_1296)=a_1369)). % 17.35/6.48 tff(c_19461, plain, (select(a_1361, i4)=e_1296)). % 17.35/6.48 tff(c_19460, plain, (select(a_1359, i4)=e_1296)). % 17.35/6.48 tff(c_19462, plain, (select(a_1363, i4)=e_1296)). % 17.35/6.48 tff(c_19466, plain, (select(a_1367, i4)=e_1296)). % 17.35/6.48 tff(c_19508, plain, (![J_5]: (select(a_1350, J_5)=select(a_1311, J_5) | i0=J_5))). % 17.35/6.48 tff(c_19463, plain, (select(a_1365, i4)=e_1296)). % 17.35/6.48 tff(c_19465, plain, (select(a_1369, i0)=e_1296)). % 17.35/6.48 tff(c_19473, plain, (select(a_1358, i4)=e_1296)). % 17.35/6.48 tff(c_19455, plain, (e_1368=e_1296)). % 17.35/6.48 tff(c_19392, plain, (store(a_1330, i4, e_1296)=a_1332)). % 17.35/6.48 tff(c_19380, plain, (store(a_1332, i4, e_1296)=a_1334)). % 17.35/6.48 tff(c_18895, plain, (store(a_1315, i4, e_1296)=a_1317)). % 17.35/6.48 tff(c_18885, plain, (store(a_1317, i4, e_1296)=a_1319)). % 17.35/6.48 tff(c_18886, plain, (store(a_1354, i4, e_1296)=a_1356)). % 17.35/6.48 tff(c_18888, plain, (store(a_1350, i4, e_1296)=a_1352)). % 17.35/6.48 tff(c_18887, plain, (store(a_1352, i4, e_1296)=a_1354)). % 17.35/6.48 tff(c_18901, plain, (store(a_1311, i4, e_1296)=a_1313)). % 17.35/6.48 tff(c_19291, plain, (select(a_1330, i4)=e_1296)). % 17.35/6.48 tff(c_19277, plain, (select(a_1332, i4)=e_1296)). % 17.35/6.48 tff(c_19262, plain, (select(a_1324, i4)=e_1296)). % 17.35/6.48 tff(c_19249, plain, (select(a_1326, i4)=e_1296)). % 17.35/6.48 tff(c_19234, plain, (select(a_1322, i4)=e_1296)). % 17.35/6.48 tff(c_19221, plain, (select(a_1328, i4)=e_1296)). % 17.35/6.48 tff(c_19201, plain, (![J_5]: (select(a_1328, J_5)=select(a_1326, J_5) | i0=J_5))). % 17.35/6.48 tff(c_19188, plain, (select(a_1334, i4)=e_1296)). % 17.35/6.48 tff(c_19176, plain, (select(a1, i0)=e_1302)). % 17.35/6.48 tff(c_19155, plain, (![J_14]: (select(a_1297, J_14)=select(a1, J_14) | i4=J_14))). % 17.35/6.48 tff(c_18897, plain, (select(a_1317, i4)=e_1296)). % 17.35/6.48 tff(c_18896, plain, (select(a_1319, i4)=e_1296)). % 17.35/6.48 tff(c_18891, plain, (select(a_1356, i4)=e_1296)). % 17.35/6.48 tff(c_18890, plain, (select(a_1354, i4)=e_1296)). % 17.35/6.48 tff(c_18898, plain, (select(a_1315, i4)=e_1296)). % 17.35/6.48 tff(c_18902, plain, (select(a_1313, i4)=e_1296)). % 17.35/6.48 tff(c_18903, plain, (select(a_1311, i0)=e_1296)). % 17.35/6.48 tff(c_18889, plain, (select(a_1352, i4)=e_1296)). % 17.35/6.48 tff(c_2067, plain, (![J_14]: (select(a_1369, J_14)=select(a_1367, J_14) | i0=J_14))). % 17.35/6.48 tff(c_18884, plain, (select(a_1309, i0)=e_1296)). % 17.35/6.48 tff(c_18883, plain, (select(a_1307, i0)=e_1296)). % 17.35/6.49 tff(c_18878, plain, (select(a_1305, i0)=e_1296)). % 17.35/6.49 tff(c_18970, plain, (select(a_1321, i4)=e_1296)). % 17.35/6.49 tff(c_18953, plain, (select(a_1303, i0)=e_1296)). % 17.35/6.49 tff(c_18880, plain, (e_1373=e_1296)). % 17.35/6.49 tff(c_18879, plain, (e_1302!=e_1296)). % 17.35/6.49 tff(c_18939, plain, (![J_14]: (select(a_1332, J_14)=select(a_1330, J_14) | i4=J_14))). % 17.35/6.49 tff(c_18882, plain, (e_1331=e_1296)). % 17.35/6.49 tff(c_18881, plain, (e_1333=e_1296)). % 17.35/6.49 tff(c_18893, plain, (e_1355=e_1296)). % 17.35/6.49 tff(c_18892, plain, (e_1353=e_1296)). % 17.35/6.49 tff(c_18894, plain, (e_1351=e_1296)). % 17.35/6.49 tff(c_18899, plain, (e_1318=e_1296)). % 17.35/6.49 tff(c_18900, plain, (e_1316=e_1296)). % 17.35/6.49 tff(c_18873, plain, (e_1312=e_1296)). % 17.35/6.49 tff(c_18822, plain, (![J_5]: (select(a_1307, J_5)=select(a_1305, J_5) | i4=J_5))). % 17.35/6.49 tff(c_18793, plain, (![J_5]: (select(a_1301, J_5)=select(a_1299, J_5) | i0=J_5))). % 17.35/6.49 tff(c_18728, plain, (![J_14]: (select(a_1305, J_14)=select(a_1303, J_14) | i4=J_14))). % 17.35/6.49 tff(c_18681, plain, (![J_14]: (select(a_1326, J_14)=select(a_1324, J_14) | i0=J_14))). % 17.35/6.49 tff(c_18563, plain, (store(a_1369, i4, e_1302)=a_1371)). % 17.35/6.49 tff(c_18567, plain, (store(a_1365, i0, e_1302)=a_1367)). % 17.35/6.49 tff(c_18531, plain, (store(a_1363, i0, e_1302)=a_1365)). % 17.35/6.49 tff(c_18532, plain, (store(a_1326, i0, e_1302)=a_1328)). % 17.35/6.49 tff(c_18533, plain, (select(a_1365, i0)=e_1302)). % 17.35/6.49 tff(c_18564, plain, (select(a_1371, i4)=e_1302)). % 17.35/6.49 tff(c_18566, plain, (select(a_1367, i0)=e_1302)). % 17.35/6.49 tff(c_18545, plain, (select(a_1330, i0)=e_1302)). % 17.35/6.49 tff(c_18584, plain, (![J_14]: (select(a_1371, J_14)=select(a_1369, J_14) | i4=J_14))). % 17.35/6.49 tff(c_18534, plain, (select(a_1328, i0)=e_1302)). % 17.35/6.49 tff(c_18562, plain, (e_1374=e_1302)). % 17.35/6.49 tff(c_18565, plain, (e_1370=e_1302)). % 17.35/6.49 tff(c_18540, plain, (e_1366=e_1302)). % 17.35/6.49 tff(c_18546, plain, (store(a_1328, i0, e_1302)=a_1330)). % 17.35/6.49 tff(c_18539, plain, (e_1329=e_1302)). % 17.35/6.49 tff(c_18530, plain, (i3=i0)). % 17.35/6.49 tff(c_18504, plain, (![J_14]: (select(a_1363, J_14)=select(a_1361, J_14) | i0=J_14))). % 17.35/6.49 tff(c_18109, plain, (store(a_1359, i0, e_1302)=a_1361)). % 17.35/6.49 tff(c_18110, plain, (store(a_1361, i0, e_1302)=a_1363)). % 17.35/6.49 tff(c_18420, plain, (sk(a_1334, a_1371)=i4)). % 17.35/6.49 tff(c_18437, plain, (![J_14]: (select(a_1303, J_14)=select(a_1301, J_14) | i4=J_14))). % 17.35/6.49 tff(c_18417, plain, (i_1372=i4)). % 17.35/6.49 tff(c_17626, plain, (store(a_1322, i0, e_1302)=a_1324)). % 17.35/6.49 tff(c_18364, plain, (![J_14]: (select(a_1313, J_14)=select(a_1311, J_14) | i4=J_14))). % 17.35/6.49 tff(c_17624, plain, (store(a_1324, i0, e_1302)=a_1326)). % 17.35/6.49 tff(c_18120, plain, (store(a_1356, i0, e_1302)=a_1358)). % 17.35/6.49 tff(c_655, plain, (![J_14]: (select(a_1321, J_14)=select(a_1319, J_14) | i0=J_14))). % 17.35/6.49 tff(c_18114, plain, (select(a_1363, i0)=e_1302)). % 17.35/6.49 tff(c_18115, plain, (select(a_1361, i0)=e_1302)). % 17.35/6.49 tff(c_18108, plain, (select(a_1354, i0)=e_1302)). % 17.35/6.49 tff(c_18118, plain, (select(a_1359, i0)=e_1302)). % 17.35/6.49 tff(c_18121, plain, (store(a_1358, i0, e_1302)=a_1359)). % 17.35/6.49 tff(c_18119, plain, (select(a_1358, i0)=e_1302)). % 17.35/6.49 tff(c_18122, plain, (select(a_1356, i0)=e_1302)). % 17.35/6.49 tff(c_18107, plain, (select(a_1352, i0)=e_1302)). % 17.35/6.49 tff(c_18140, plain, (![J_14]: (select(a_1334, J_14)=select(a_1332, J_14) | i4=J_14))). % 17.35/6.49 tff(c_18117, plain, (e_1362=e_1302)). % 17.35/6.49 tff(c_18116, plain, (e_1360=e_1302)). % 17.35/6.49 tff(c_18113, plain, (e_1364=e_1302)). % 17.35/6.49 tff(c_18102, plain, (e_1357=e_1302)). % 17.35/6.49 tff(c_18079, plain, (![J_14]: (select(a_1352, J_14)=select(a_1350, J_14) | i4=J_14))). % 17.35/6.49 tff(c_18009, plain, (store(a_1311, i0, e_1302)=a_1350)). % 17.45/6.49 tff(c_17992, plain, (a_1348=a_1311)). % 17.45/6.49 tff(c_17635, plain, (store(a_1319, i0, e_1302)=a_1321)). % 17.45/6.49 tff(c_17989, plain, (a_1346=a_1309)). % 17.45/6.49 tff(c_754, plain, (![J_14]: (select(a_1309, J_14)=select(a_1307, J_14) | i4=J_14))). % 17.45/6.49 tff(c_17939, plain, (a_1344=a_1307)). % 17.45/6.49 tff(c_17926, plain, (a_1342=a_1305)). % 17.45/6.49 tff(c_17923, plain, (a_1340=a_1303)). % 17.45/6.49 tff(c_17883, plain, (store(a_1299, i0, e_1296)=a_1301)). % 17.45/6.49 tff(c_17184, plain, (store(a_1313, i0, e_1302)=a_1315)). % 17.45/6.49 tff(c_17882, plain, (a_1338=a_1301)). % 17.45/6.49 tff(c_17771, plain, (![J_14]: (select(a_1315, J_14)=select(a_1313, J_14) | i0=J_14))). % 17.45/6.49 tff(c_17627, plain, (select(a_1326, i0)=e_1302)). % 17.45/6.49 tff(c_17629, plain, (select(a_1324, i0)=e_1302)). % 17.45/6.49 tff(c_17633, plain, (select(a_1322, i0)=e_1302)). % 17.45/6.49 tff(c_17636, plain, (store(a_1321, i0, e_1302)=a_1322)). % 17.45/6.49 tff(c_17543, plain, (select(a_1297, i0)=e_1302)). % 17.45/6.49 tff(c_17634, plain, (select(a_1321, i0)=e_1302)). % 17.45/6.49 tff(c_709, plain, (![J_14]: (select(a_1322, J_14)=select(a_1321, J_14) | i0=J_14))). % 17.45/6.49 tff(c_17448, plain, (select(a_1350, i0)=e_1302)). % 17.45/6.49 tff(c_17667, plain, (select(a_1317, i0)=e_1302)). % 17.45/6.49 tff(c_17631, plain, (e_1325=e_1302)). % 17.45/6.49 tff(c_17632, plain, (e_1323=e_1302)). % 17.45/6.49 tff(c_17630, plain, (e_1327=e_1302)). % 17.45/6.49 tff(c_17637, plain, (select(a_1319, i0)=e_1302)). % 17.45/6.50 tff(c_17619, plain, (e_1320=e_1302)). % 17.45/6.50 tff(c_17516, plain, (![J_14]: (select(a_1299, J_14)=select(a_1297, J_14) | i4=J_14))). % 17.45/6.50 tff(c_17449, plain, (e_1349=e_1302)). % 17.45/6.50 tff(c_17461, plain, (e_1345=e_1302)). % 17.45/6.50 tff(c_17463, plain, (e_1341=e_1302)). % 17.45/6.50 tff(c_17476, plain, (![J_14]: (select(a_1319, J_14)=select(a_1317, J_14) | i4=J_14))). % 17.45/6.50 tff(c_17462, plain, (e_1343=e_1302)). % 17.45/6.50 tff(c_17455, plain, (e_1347=e_1302)). % 17.45/6.50 tff(c_17442, plain, (e_1339=e_1302)). % 17.45/6.50 tff(c_17438, plain, (a_1336=a_1299)). % 17.45/6.50 tff(c_736, plain, (![J_14]: (select(a_1330, J_14)=select(a_1328, J_14) | i0=J_14))). % 17.45/6.50 tff(c_17357, plain, (store(a_1297, i4, e_1296)=a_1299)). % 17.45/6.50 tff(c_17185, plain, (select(a_1315, i0)=e_1302)). % 17.45/6.50 tff(c_17334, plain, (select(a_1301, i0)=e_1296)). % 17.45/6.50 tff(c_17233, plain, (select(a_1299, i4)=e_1296)). % 17.45/6.50 tff(c_17267, plain, (![J_14]: (select(a_1324, J_14)=select(a_1322, J_14) | i0=J_14))). % 17.45/6.50 tff(c_17232, plain, (e_1300=e_1296)). % 17.45/6.50 tff(c_17238, plain, (a_1335=a_1297)). % 17.45/6.50 tff(c_17227, plain, (e_1298=e_1296)). % 17.45/6.50 tff(c_17175, plain, (select(a1, i4)=e_1296)). % 17.45/6.50 tff(c_17178, plain, (e_1314=e_1302)). % 17.45/6.50 tff(c_17163, plain, (i7=i4)). % 17.45/6.50 tff(c_17119, plain, (i4!=i0)). % 17.45/6.50 tff(c_1807, plain, (store(a_1301, i4, e_1302)=a_1303)). % 17.45/6.50 tff(c_2352, plain, (store(a_1309, i4, e_1302)=a_1311)). % 17.45/6.50 tff(c_1805, plain, (store(a_1303, i4, e_1302)=a_1305)). % 17.45/6.50 tff(c_2309, plain, (![J_14]: (select(a_1311, J_14)=select(a_1309, J_14) | i4=J_14))). % 17.45/6.50 tff(c_1806, plain, (store(a1, i4, e_1296)=a_1297)). % 17.45/6.50 tff(c_2198, plain, (![J_14]: (select(a_1361, J_14)=select(a_1359, J_14) | i0=J_14))). % 17.45/6.50 tff(c_1820, plain, (store(a_1305, i4, e_1302)=a_1307)). % 17.45/6.50 tff(c_2077, plain, (select(a_1299, i0)=e_1302)). % 17.45/6.50 tff(c_2101, plain, (![J_14]: (select(a_1356, J_14)=select(a_1354, J_14) | i4=J_14))). % 17.45/6.50 tff(c_2066, plain, (i6=i0)). % 17.45/6.50 tff(c_1811, plain, (select(a_1297, i4)=e_1296)). % 17.45/6.50 tff(c_1809, plain, (select(a_1305, i4)=e_1302)). % 17.45/6.50 tff(c_1813, plain, (select(a_1303, i4)=e_1302)). % 17.45/6.50 tff(c_700, plain, (![J_14]: (select(a_1354, J_14)=select(a_1352, J_14) | i4=J_14))). % 17.45/6.50 tff(c_1950, plain, (select(a_1311, i4)=e_1302)). % 17.45/6.50 tff(c_733, plain, (![J_14]: (select(a_1367, J_14)=select(a_1365, J_14) | i0=J_14))). % 17.45/6.50 tff(c_1880, plain, (e_1310=e_1302)). % 17.45/6.50 tff(c_1824, plain, (select(a_1307, i4)=e_1302)). % 17.45/6.50 tff(c_1802, plain, (i9=i4)). % 17.45/6.50 tff(c_1818, plain, (i8=i4)). % 17.45/6.50 tff(c_1790, plain, (i5=i4)). % 17.45/6.50 tff(c_1632, plain, (store(a_1307, i4, e_1302)=a_1309)). % 17.45/6.50 tff(c_682, plain, (![J_14]: (select(a_1317, J_14)=select(a_1315, J_14) | i4=J_14))). % 17.45/6.50 tff(c_1631, plain, (select(a_1309, i4)=e_1302)). % 17.45/6.50 tff(c_1619, plain, (e_1308=e_1302)). % 17.45/6.50 tff(c_706, plain, (![J_14]: (select(a_1358, J_14)=select(a_1356, J_14) | i0=J_14))). % 17.45/6.50 tff(c_1490, plain, (e_1304=e_1302)). % 17.45/6.50 tff(c_1162, plain, (i1=i0)). % 17.45/6.50 tff(c_1017, plain, (i2=i0)). % 17.45/6.50 tff(c_712, plain, (![J_14]: (select(a_1359, J_14)=select(a_1358, J_14) | i0=J_14))). % 17.45/6.50 tff(c_840, plain, (e_1337=e_1296)). % 17.45/6.50 tff(c_765, plain, (e_1306=e_1302)). % 17.45/6.50 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))). % 17.45/6.50 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 17.45/6.50 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.45/6.50 %------------------------------------------------------------------------------