%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV499-1.040 : 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 : n012.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 : Thu Apr 10 02:51:32 AM UTC 2025 % Result : Satisfiable 6.94s 2.62s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV499-1.040 : TPTP v9.0.0. Released v4.0.0. % 0.03/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.14/0.35 % Computer : n012.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Apr 9 22:24:44 EDT 2025 % 0.14/0.35 % CPUTime : % 6.94/2.62 % 6.94/2.62 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.94/2.62 % 6.94/2.62 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.94/2.64 %$ store > select > #nlpp > n9 > n8 > n7 > n6 > n5 > n40 > n4 > n39 > n38 > n37 > n36 > n35 > n34 > n33 > n32 > n31 > n30 > n3 > n29 > n28 > n27 > n26 > n25 > n24 > n23 > n22 > n21 > n20 > n2 > n19 > n18 > n17 > n16 > n15 > n14 > n13 > n12 > n11 > n10 > n1 > e9 > e8 > e7 > e6 > e5 > e40 > e4 > e39 > e38 > e37 > e36 > e35 > e34 > e33 > e32 > e31 > e30 > e3 > e29 > e28 > e27 > e26 > e25 > e24 > e23 > e22 > e21 > e20 > e2 > e19 > e18 > e17 > e16 > e15 > e14 > e13 > e12 > e11 > e10 > e1 > a_1438 > a_1437 > a_1436 > a_1435 > a_1434 > a_1433 > a_1432 > a_1431 > a_1430 > a_1429 > a_1428 > a_1427 > a_1426 > a_1425 > a_1424 > a_1423 > a_1422 > a_1421 > a_1420 > a_1419 > a_1418 > a_1417 > a_1416 > a_1415 > a_1414 > a_1413 > a_1412 > a_1411 > a_1410 > a_1409 > a_1408 > a_1407 > a_1406 > a_1405 > a_1404 > a_1403 > a_1402 > a_1401 > a_1400 > a_1399 > a_1398 > a_1397 > a_1396 > a_1395 > a_1394 > a_1393 > a_1392 > a_1391 > a_1390 > a_1389 > a_1388 > a_1387 > a_1386 > a_1385 > a_1384 > a_1383 > a_1382 > a_1381 > a_1380 > a_1379 > a_1378 > a_1377 > a_1376 > a_1375 > a_1374 > a_1373 > a_1372 > a_1371 > a_1370 > a_1369 > a_1368 > a_1367 > a_1366 > a_1365 > a_1364 > a_1363 > a_1362 > a_1361 > a_1360 > a_1359 > a1 % 6.94/2.64 % 6.94/2.64 %Foreground sorts: % 6.94/2.64 % 6.94/2.64 % 6.94/2.64 %Background operators: % 6.94/2.64 % 6.94/2.64 % 6.94/2.64 %Foreground operators: % 6.94/2.64 tff(e29, type, e29: $i). % 6.94/2.64 tff(a1, type, a1: $i). % 6.94/2.64 tff(a_1407, type, a_1407: $i). % 6.94/2.64 tff(n22, type, n22: $i). % 6.94/2.64 tff(a_1361, type, a_1361: $i). % 6.94/2.64 tff(n27, type, n27: $i). % 6.94/2.64 tff(a_1424, type, a_1424: $i). % 6.94/2.64 tff(a_1387, type, a_1387: $i). % 6.94/2.64 tff(a_1366, type, a_1366: $i). % 6.94/2.64 tff(n16, type, n16: $i). % 6.94/2.64 tff(n12, type, n12: $i). % 6.94/2.64 tff(e1, type, e1: $i). % 6.94/2.64 tff(e8, type, e8: $i). % 6.94/2.64 tff(e21, type, e21: $i). % 6.94/2.64 tff(n24, type, n24: $i). % 6.94/2.64 tff(a_1391, type, a_1391: $i). % 6.94/2.64 tff(a_1399, type, a_1399: $i). % 6.94/2.64 tff(a_1386, type, a_1386: $i). % 6.94/2.64 tff(a_1431, type, a_1431: $i). % 6.94/2.64 tff(e15, type, e15: $i). % 6.94/2.64 tff(a_1370, type, a_1370: $i). % 6.94/2.64 tff(a_1415, type, a_1415: $i). % 6.94/2.64 tff(a_1363, type, a_1363: $i). % 6.94/2.64 tff(e33, type, e33: $i). % 6.94/2.64 tff(n35, type, n35: $i). % 6.94/2.64 tff(a_1390, type, a_1390: $i). % 6.94/2.64 tff(e40, type, e40: $i). % 6.94/2.64 tff(a_1395, type, a_1395: $i). % 6.94/2.64 tff(a_1412, type, a_1412: $i). % 6.94/2.64 tff(e18, type, e18: $i). % 6.94/2.64 tff(e38, type, e38: $i). % 6.94/2.64 tff(a_1362, type, a_1362: $i). % 6.94/2.64 tff(a_1437, type, a_1437: $i). % 6.94/2.64 tff(e24, type, e24: $i). % 6.94/2.64 tff(e31, type, e31: $i). % 6.94/2.64 tff(n33, type, n33: $i). % 6.94/2.64 tff(n36, type, n36: $i). % 6.94/2.64 tff(a_1432, type, a_1432: $i). % 6.94/2.64 tff(a_1429, type, a_1429: $i). % 6.94/2.64 tff(e39, type, e39: $i). % 6.94/2.64 tff(store, type, store: ($i * $i * $i) > $i). % 6.94/2.64 tff(n23, type, n23: $i). % 6.94/2.64 tff(n8, type, n8: $i). % 6.94/2.64 tff(a_1436, type, a_1436: $i). % 6.94/2.64 tff(e20, type, e20: $i). % 6.94/2.64 tff(e19, type, e19: $i). % 6.94/2.64 tff(e16, type, e16: $i). % 6.94/2.64 tff(n30, type, n30: $i). % 6.94/2.64 tff(a_1364, type, a_1364: $i). % 6.94/2.64 tff(a_1420, type, a_1420: $i). % 6.94/2.64 tff(a_1406, type, a_1406: $i). % 6.94/2.64 tff(e35, type, e35: $i). % 6.94/2.64 tff(a_1383, type, a_1383: $i). % 6.94/2.64 tff(a_1393, type, a_1393: $i). % 6.94/2.64 tff(e2, type, e2: $i). % 6.94/2.64 tff(a_1367, type, a_1367: $i). % 6.94/2.64 tff(n28, type, n28: $i). % 6.94/2.64 tff(n9, type, n9: $i). % 6.94/2.64 tff(a_1413, type, a_1413: $i). % 6.94/2.64 tff(a_1379, type, a_1379: $i). % 6.94/2.64 tff(a_1423, type, a_1423: $i). % 6.94/2.64 tff(a_1402, type, a_1402: $i). % 6.94/2.64 tff(e37, type, e37: $i). % 6.94/2.64 tff(e13, type, e13: $i). % 6.94/2.64 tff(n3, type, n3: $i). % 6.94/2.64 tff(a_1417, type, a_1417: $i). % 6.94/2.64 tff(a_1403, type, a_1403: $i). % 6.94/2.64 tff(a_1430, type, a_1430: $i). % 6.94/2.64 tff(e32, type, e32: $i). % 6.94/2.64 tff(e22, type, e22: $i). % 6.94/2.64 tff(n39, type, n39: $i). % 6.94/2.64 tff(a_1359, type, a_1359: $i). % 6.94/2.64 tff(e34, type, e34: $i). % 6.94/2.64 tff(n1, type, n1: $i). % 6.94/2.64 tff(a_1385, type, a_1385: $i). % 6.94/2.64 tff(n29, type, n29: $i). % 6.94/2.64 tff(e9, type, e9: $i). % 6.94/2.64 tff(a_1396, type, a_1396: $i). % 6.94/2.64 tff(n37, type, n37: $i). % 6.94/2.64 tff(a_1418, type, a_1418: $i). % 6.94/2.64 tff(n7, type, n7: $i). % 6.94/2.64 tff(e25, type, e25: $i). % 6.94/2.64 tff(a_1376, type, a_1376: $i). % 6.94/2.64 tff(e26, type, e26: $i). % 6.94/2.64 tff(n6, type, n6: $i). % 6.94/2.64 tff(e17, type, e17: $i). % 6.94/2.64 tff(a_1388, type, a_1388: $i). % 6.94/2.64 tff(n26, type, n26: $i). % 6.94/2.64 tff(e27, type, e27: $i). % 6.94/2.64 tff(e10, type, e10: $i). % 6.94/2.64 tff(e7, type, e7: $i). % 6.94/2.64 tff(a_1421, type, a_1421: $i). % 6.94/2.64 tff(n13, type, n13: $i). % 6.94/2.64 tff(a_1372, type, a_1372: $i). % 6.94/2.64 tff(a_1425, type, a_1425: $i). % 6.94/2.64 tff(a_1422, type, a_1422: $i). % 6.94/2.64 tff(a_1404, type, a_1404: $i). % 6.94/2.64 tff(a_1405, type, a_1405: $i). % 6.94/2.64 tff(a_1394, type, a_1394: $i). % 6.94/2.64 tff(e36, type, e36: $i). % 6.94/2.64 tff(a_1389, type, a_1389: $i). % 6.94/2.64 tff(a_1416, type, a_1416: $i). % 6.94/2.64 tff(a_1426, type, a_1426: $i). % 6.94/2.64 tff(n4, type, n4: $i). % 6.94/2.64 tff(a_1381, type, a_1381: $i). % 6.94/2.64 tff(a_1380, type, a_1380: $i). % 6.94/2.64 tff(n10, type, n10: $i). % 6.94/2.64 tff(n14, type, n14: $i). % 6.94/2.64 tff(n15, type, n15: $i). % 6.94/2.64 tff(n17, type, n17: $i). % 6.94/2.64 tff(n40, type, n40: $i). % 6.94/2.64 tff(a_1382, type, a_1382: $i). % 6.94/2.64 tff(e30, type, e30: $i). % 6.94/2.64 tff(select, type, select: ($i * $i) > $i). % 6.94/2.64 tff(a_1369, type, a_1369: $i). % 6.94/2.64 tff(a_1419, type, a_1419: $i). % 6.94/2.64 tff(n31, type, n31: $i). % 6.94/2.64 tff(a_1368, type, a_1368: $i). % 6.94/2.64 tff(a_1433, type, a_1433: $i). % 6.94/2.64 tff(a_1384, type, a_1384: $i). % 6.94/2.64 tff(a_1401, type, a_1401: $i). % 6.94/2.64 tff(a_1411, type, a_1411: $i). % 6.94/2.64 tff(n32, type, n32: $i). % 6.94/2.64 tff(a_1435, type, a_1435: $i). % 6.94/2.64 tff(n20, type, n20: $i). % 6.94/2.64 tff(e23, type, e23: $i). % 6.94/2.64 tff(n18, type, n18: $i). % 6.94/2.64 tff(n38, type, n38: $i). % 6.94/2.64 tff(e14, type, e14: $i). % 6.94/2.64 tff(a_1414, type, a_1414: $i). % 6.94/2.64 tff(a_1428, type, a_1428: $i). % 6.94/2.64 tff(n11, type, n11: $i). % 6.94/2.64 tff(a_1400, type, a_1400: $i). % 6.94/2.64 tff(a_1410, type, a_1410: $i). % 6.94/2.64 tff(e12, type, e12: $i). % 6.94/2.64 tff(e4, type, e4: $i). % 6.94/2.64 tff(a_1434, type, a_1434: $i). % 6.94/2.64 tff(a_1365, type, a_1365: $i). % 6.94/2.64 tff(n34, type, n34: $i). % 6.94/2.64 tff(a_1409, type, a_1409: $i). % 6.94/2.64 tff(a_1397, type, a_1397: $i). % 6.94/2.64 tff(a_1374, type, a_1374: $i). % 6.94/2.64 tff(a_1398, type, a_1398: $i). % 6.94/2.64 tff(a_1438, type, a_1438: $i). % 6.94/2.64 tff(a_1375, type, a_1375: $i). % 6.94/2.64 tff(a_1371, type, a_1371: $i). % 6.94/2.64 tff(e6, type, e6: $i). % 6.94/2.64 tff(n19, type, n19: $i). % 6.94/2.64 tff(a_1377, type, a_1377: $i). % 6.94/2.64 tff(a_1427, type, a_1427: $i). % 6.94/2.64 tff(n2, type, n2: $i). % 6.94/2.64 tff(e11, type, e11: $i). % 6.94/2.64 tff(e28, type, e28: $i). % 6.94/2.64 tff(n5, type, n5: $i). % 6.94/2.64 tff(e3, type, e3: $i). % 6.94/2.64 tff(n25, type, n25: $i). % 6.94/2.64 tff(a_1378, type, a_1378: $i). % 6.94/2.64 tff(e5, type, e5: $i). % 6.94/2.64 tff(a_1360, type, a_1360: $i). % 6.94/2.64 tff(a_1392, type, a_1392: $i). % 6.94/2.64 tff(a_1408, type, a_1408: $i). % 6.94/2.64 tff(n21, type, n21: $i). % 6.94/2.64 tff(a_1373, type, a_1373: $i). % 6.94/2.64 % 6.94/2.64 %Saturated clause set: % 6.94/2.64 tff(c_795, plain, (![J_14]: (select(a_1404, J_14)=select(a_1403, J_14) | n17=J_14))). % 6.94/2.64 tff(c_948, plain, (![J_14]: (select(a_1421, J_14)=select(a_1420, J_14) | n22=J_14))). % 6.94/2.64 tff(c_840, plain, (![J_14]: (select(a_1419, J_14)=select(a_1418, J_14) | n27=J_14))). % 6.94/2.64 tff(c_813, plain, (![J_14]: (select(a_1376, J_14)=select(a_1375, J_14) | n18=J_14))). % 6.94/2.64 tff(c_807, plain, (![J_14]: (select(a_1405, J_14)=select(a_1404, J_14) | n7=J_14))). % 6.94/2.64 tff(c_966, plain, (![J_14]: (select(a_1367, J_14)=select(a_1366, J_14) | n9=J_14))). % 6.94/2.64 tff(c_888, plain, (![J_14]: (select(a_1388, J_14)=select(a_1387, J_14) | n30=J_14))). % 6.94/2.64 tff(c_972, plain, (![J_14]: (select(a_1365, J_14)=select(a_1364, J_14) | n7=J_14))). % 6.94/2.64 tff(c_975, plain, (![J_14]: (select(a_1434, J_14)=select(a_1433, J_14) | n15=J_14))). % 6.94/2.64 tff(c_915, plain, (![J_14]: (select(a_1429, J_14)=select(a_1428, J_14) | n9=J_14))). % 6.94/2.64 tff(c_900, plain, (![J_14]: (select(a_1385, J_14)=select(a_1384, J_14) | n27=J_14))). % 6.94/2.64 tff(c_789, plain, (![J_14]: (select(a_1397, J_14)=select(a_1396, J_14) | n39=J_14))). % 6.94/2.64 tff(c_876, plain, (![J_14]: (select(a_1391, J_14)=select(a_1390, J_14) | n33=J_14))). % 6.94/2.64 tff(c_894, plain, (![J_14]: (select(a_1386, J_14)=select(a_1385, J_14) | n28=J_14))). % 6.94/2.64 tff(c_849, plain, (![J_14]: (select(a_1416, J_14)=select(a_1415, J_14) | n23=J_14))). % 6.94/2.64 tff(c_837, plain, (![J_14]: (select(a_1407, J_14)=select(a_1406, J_14) | n6=J_14))). % 6.94/2.64 tff(c_906, plain, (![J_14]: (select(a_1383, J_14)=select(a_1382, J_14) | n25=J_14))). % 6.94/2.64 tff(c_855, plain, (![J_14]: (select(a_1425, J_14)=select(a_1424, J_14) | n40=J_14))). % 6.94/2.64 tff(c_831, plain, (![J_14]: (select(a_1408, J_14)=select(a_1407, J_14) | n18=J_14))). % 6.94/2.64 tff(c_828, plain, (![J_14]: (select(a_1372, J_14)=select(a_1371, J_14) | n14=J_14))). % 6.94/2.64 tff(c_897, plain, (![J_14]: (select(a_1428, J_14)=select(a_1427, J_14) | n1=J_14))). % 6.94/2.64 tff(c_819, plain, (![J_14]: (select(a_1423, J_14)=select(a_1422, J_14) | n33=J_14))). % 6.94/2.64 tff(c_777, plain, (![J_14]: (select(a_1403, J_14)=select(a_1402, J_14) | n25=J_14))). % 6.94/2.64 tff(c_921, plain, (![J_14]: (select(a_1379, J_14)=select(a_1378, J_14) | n21=J_14))). % 6.94/2.64 tff(c_798, plain, (![J_14]: (select(a_1413, J_14)=select(a_1412, J_14) | n36=J_14))). % 6.94/2.64 tff(c_1002, plain, (![J_14]: (select(a_1438, J_14)=select(a_1437, J_14) | n19=J_14))). % 6.94/2.64 tff(c_882, plain, (![J_14]: (select(a_1389, J_14)=select(a_1388, J_14) | n31=J_14))). % 6.94/2.64 tff(c_801, plain, (![J_14]: (select(a_1412, J_14)=select(a_1411, J_14) | n12=J_14))). % 6.94/2.64 tff(c_861, plain, (![J_14]: (select(a_1395, J_14)=select(a_1394, J_14) | n37=J_14))). % 6.94/2.64 tff(c_924, plain, (![J_14]: (select(a_1378, J_14)=select(a_1377, J_14) | n20=J_14))). % 6.94/2.64 tff(c_792, plain, (![J_14]: (select(a_1415, J_14)=select(a_1414, J_14) | n35=J_14))). % 6.94/2.64 tff(c_816, plain, (![J_14]: (select(a_1432, J_14)=select(a_1431, J_14) | n4=J_14))). % 6.94/2.64 tff(c_810, plain, (![J_14]: (select(a_1409, J_14)=select(a_1408, J_14) | n37=J_14))). % 6.94/2.64 tff(c_951, plain, (![J_14]: (select(a_1371, J_14)=select(a_1370, J_14) | n13=J_14))). % 6.94/2.64 tff(c_942, plain, (![J_14]: (select(a_1373, J_14)=select(a_1372, J_14) | n15=J_14))). % 6.94/2.65 tff(c_852, plain, (![J_14]: (select(a_1414, J_14)=select(a_1413, J_14) | n20=J_14))). % 6.94/2.65 tff(c_867, plain, (![J_14]: (select(a_1426, J_14)=select(a_1425, J_14) | n38=J_14))). % 6.94/2.65 tff(c_891, plain, (![J_14]: (select(a_1387, J_14)=select(a_1386, J_14) | n29=J_14))). % 6.94/2.65 tff(c_969, plain, (![J_14]: (select(a_1366, J_14)=select(a_1365, J_14) | n8=J_14))). % 6.94/2.65 tff(c_963, plain, (![J_14]: (select(a_1368, J_14)=select(a_1367, J_14) | n10=J_14))). % 6.94/2.65 tff(c_927, plain, (![J_14]: (select(a_1430, J_14)=select(a_1429, J_14) | n3=J_14))). % 6.94/2.65 tff(c_780, plain, (![J_14]: (select(a_1410, J_14)=select(a_1409, J_14) | n31=J_14))). % 6.94/2.65 tff(c_786, plain, (![J_14]: (select(a_1398, J_14)=select(a_1397, J_14) | n40=J_14))). % 6.94/2.65 tff(c_936, plain, (![J_14]: (select(a_1375, J_14)=select(a_1374, J_14) | n17=J_14))). % 6.94/2.65 tff(c_834, plain, (![J_14]: (select(a_1420, J_14)=select(a_1419, J_14) | n10=J_14))). % 6.94/2.65 tff(c_858, plain, (![J_14]: (select(a_1396, J_14)=select(a_1395, J_14) | n38=J_14))). % 6.94/2.65 tff(c_984, plain, (![J_14]: (select(a_1362, J_14)=select(a_1361, J_14) | n4=J_14))). % 6.94/2.65 tff(c_960, plain, (![J_14]: (select(a_1369, J_14)=select(a_1368, J_14) | n11=J_14))). % 6.94/2.65 tff(c_996, plain, (![J_14]: (select(a_1359, J_14)=select(a1, J_14) | n1=J_14))). % 6.94/2.65 tff(c_987, plain, (![J_14]: (select(a_1435, J_14)=select(a_1434, J_14) | n34=J_14))). % 6.94/2.65 tff(c_990, plain, (![J_14]: (select(a_1361, J_14)=select(a_1360, J_14) | n3=J_14))). % 6.94/2.65 tff(c_981, plain, (![J_14]: (select(a_1363, J_14)=select(a_1362, J_14) | n5=J_14))). % 6.94/2.65 tff(c_885, plain, (![J_14]: (select(a_1427, J_14)=select(a_1426, J_14) | n39=J_14))). % 6.94/2.65 tff(c_939, plain, (![J_14]: (select(a_1374, J_14)=select(a_1373, J_14) | n16=J_14))). % 6.94/2.65 tff(c_978, plain, (![J_14]: (select(a_1364, J_14)=select(a_1363, J_14) | n6=J_14))). % 6.94/2.65 tff(c_909, plain, (![J_14]: (select(a_1382, J_14)=select(a_1381, J_14) | n24=J_14))). % 6.94/2.65 tff(c_957, plain, (![J_14]: (select(a_1433, J_14)=select(a_1432, J_14) | n30=J_14))). % 6.94/2.65 tff(c_765, plain, (![J_14]: (select(a_1437, J_14)=select(a_1436, J_14) | n29=J_14))). % 6.94/2.65 tff(c_768, plain, (![J_14]: (select(a_1402, J_14)=select(a_1401, J_14) | n11=J_14))). % 6.94/2.65 tff(c_771, plain, (![J_14]: (select(a_1401, J_14)=select(a_1400, J_14) | n24=J_14))). % 6.94/2.65 tff(c_774, plain, (![J_14]: (select(a_1400, J_14)=select(a_1399, J_14) | n14=J_14))). % 6.94/2.65 tff(c_912, plain, (![J_14]: (select(a_1381, J_14)=select(a_1380, J_14) | n23=J_14))). % 6.94/2.65 tff(c_954, plain, (![J_14]: (select(a_1370, J_14)=select(a_1369, J_14) | n12=J_14))). % 6.94/2.65 tff(c_825, plain, (![J_14]: (select(a_1406, J_14)=select(a_1405, J_14) | n32=J_14))). % 6.94/2.65 tff(c_864, plain, (![J_14]: (select(a_1394, J_14)=select(a_1393, J_14) | n36=J_14))). % 6.94/2.65 tff(c_918, plain, (![J_14]: (select(a_1380, J_14)=select(a_1379, J_14) | n22=J_14))). % 6.94/2.65 tff(c_930, plain, (![J_14]: (select(a_1377, J_14)=select(a_1376, J_14) | n19=J_14))). % 6.94/2.65 tff(c_993, plain, (![J_14]: (select(a_1360, J_14)=select(a_1359, J_14) | n2=J_14))). % 6.94/2.65 tff(c_870, plain, (![J_14]: (select(a_1393, J_14)=select(a_1392, J_14) | n35=J_14))). % 6.94/2.65 tff(c_822, plain, (![J_14]: (select(a_1422, J_14)=select(a_1421, J_14) | n8=J_14))). % 6.94/2.65 tff(c_783, plain, (![J_14]: (select(a_1399, J_14)=select(a1, J_14) | n16=J_14))). % 6.94/2.65 tff(c_846, plain, (![J_14]: (select(a_1417, J_14)=select(a_1416, J_14) | n26=J_14))). % 6.94/2.65 tff(c_945, plain, (![J_14]: (select(a_1431, J_14)=select(a_1430, J_14) | n5=J_14))). % 6.94/2.65 tff(c_999, plain, (![J_14]: (select(a_1436, J_14)=select(a_1435, J_14) | n28=J_14))). % 6.94/2.65 tff(c_873, plain, (![J_14]: (select(a_1392, J_14)=select(a_1391, J_14) | n34=J_14))). % 6.94/2.65 tff(c_804, plain, (![J_14]: (select(a_1411, J_14)=select(a_1410, J_14) | n13=J_14))). % 6.94/2.65 tff(c_879, plain, (![J_14]: (select(a_1390, J_14)=select(a_1389, J_14) | n32=J_14))). % 6.94/2.65 tff(c_843, plain, (![J_14]: (select(a_1418, J_14)=select(a_1417, J_14) | n21=J_14))). % 6.94/2.65 tff(c_903, plain, (![J_14]: (select(a_1384, J_14)=select(a_1383, J_14) | n26=J_14))). % 6.94/2.65 tff(c_933, plain, (![J_14]: (select(a_1424, J_14)=select(a_1423, J_14) | n2=J_14))). % 6.94/2.65 tff(c_643, plain, (select(a_1381, n23)=e23)). % 6.94/2.65 tff(c_532, plain, (select(a_1412, n12)=e12)). % 6.94/2.65 tff(c_571, plain, (select(a_1419, n27)=e27)). % 6.94/2.65 tff(c_640, plain, (select(a_1382, n24)=e24)). % 6.94/2.65 tff(c_529, plain, (select(a_1413, n36)=e36)). % 6.94/2.65 tff(c_649, plain, (select(a_1380, n22)=e22)). % 6.94/2.65 tff(c_511, plain, (select(a_1410, n31)=e31)). % 6.94/2.65 tff(c_652, plain, (select(a_1379, n21)=e21)). % 6.94/2.65 tff(c_574, plain, (select(a_1418, n21)=e21)). % 6.94/2.65 tff(c_655, plain, (select(a_1378, n20)=e20)). % 6.94/2.65 tff(c_568, plain, (select(a_1407, n6)=e6)). % 6.94/2.65 tff(c_658, plain, (select(a_1430, n3)=e3)). % 6.94/2.65 tff(c_586, plain, (select(a_1425, n40)=e40)). % 6.94/2.65 tff(c_646, plain, (select(a_1429, n9)=e9)). % 6.94/2.65 tff(c_535, plain, (select(a_1411, n13)=e13)). % 6.94/2.65 tff(c_631, plain, (select(a_1385, n27)=e27)). % 6.94/2.65 tff(c_577, plain, (select(a_1417, n26)=e26)). % 6.94/2.65 tff(c_637, plain, (select(a_1383, n25)=e25)). % 6.94/2.65 tff(c_565, plain, (select(a_1420, n10)=e10)). % 6.94/2.65 tff(c_661, plain, (select(a_1377, n19)=e19)). % 6.94/2.65 tff(c_682, plain, (select(a_1371, n13)=e13)). % 6.94/2.65 tff(c_562, plain, (select(a_1408, n18)=e18)). % 6.94/2.65 tff(c_634, plain, (select(a_1384, n26)=e26)). % 6.94/2.65 tff(c_664, plain, (select(a_1424, n2)=e2)). % 6.94/2.65 tff(c_625, plain, (select(a_1386, n28)=e28)). % 6.94/2.65 tff(c_580, plain, (select(a_1416, n23)=e23)). % 6.94/2.65 tff(c_559, plain, (select(a_1372, n14)=e14)). % 6.94/2.65 tff(c_667, plain, (select(a_1375, n17)=e17)). % 6.94/2.65 tff(c_670, plain, (select(a_1374, n16)=e16)). % 6.94/2.65 tff(c_628, plain, (select(a_1428, n1)=e1)). % 6.94/2.65 tff(c_538, plain, (select(a_1405, n7)=e7)). % 6.94/2.66 tff(c_583, plain, (select(a_1414, n20)=e20)). % 6.94/2.66 tff(c_673, plain, (select(a_1373, n15)=e15)). % 6.94/2.66 tff(c_526, plain, (select(a_1404, n17)=e17)). % 6.94/2.66 tff(c_619, plain, (select(a_1388, n30)=e30)). % 6.94/2.66 tff(c_556, plain, (select(a_1406, n32)=e32)). % 6.94/2.66 tff(c_616, plain, (select(a_1427, n39)=e39)). % 6.94/2.66 tff(c_622, plain, (select(a_1387, n29)=e29)). % 6.94/2.66 tff(c_676, plain, (select(a_1431, n5)=e5)). % 6.94/2.66 tff(c_514, plain, (select(a_1399, n16)=e16)). % 6.94/2.66 tff(c_679, plain, (select(a_1421, n22)=e22)). % 6.94/2.66 tff(c_613, plain, (select(a_1389, n31)=e31)). % 6.94/2.66 tff(c_502, plain, (select(a_1401, n24)=e24)). % 6.94/2.66 tff(c_553, plain, (select(a_1422, n8)=e8)). % 6.94/2.66 tff(c_523, plain, (select(a_1415, n35)=e35)). % 6.94/2.66 tff(c_508, plain, (select(a_1403, n25)=e25)). % 6.94/2.66 tff(c_610, plain, (select(a_1390, n32)=e32)). % 6.94/2.66 tff(c_700, plain, (select(a_1366, n8)=e8)). % 6.94/2.66 tff(c_598, plain, (select(a_1426, n38)=e38)). % 6.94/2.66 tff(c_703, plain, (select(a_1365, n7)=e7)). % 6.94/2.66 tff(c_706, plain, (select(a_1434, n15)=e15)). % 6.94/2.66 tff(c_520, plain, (select(a_1397, n39)=e39)). % 6.94/2.66 tff(c_547, plain, (select(a_1432, n4)=e4)). % 6.94/2.66 tff(c_697, plain, (select(a_1367, n9)=e9)). % 6.94/2.66 tff(c_544, plain, (select(a_1376, n18)=e18)). % 6.94/2.66 tff(c_694, plain, (select(a_1368, n10)=e10)). % 6.94/2.66 tff(c_601, plain, (select(a_1393, n35)=e35)). % 6.94/2.66 tff(c_595, plain, (select(a_1394, n36)=e36)). % 6.94/2.66 tff(c_709, plain, (select(a_1364, n6)=e6)). % 6.94/2.66 tff(c_712, plain, (select(a_1363, n5)=e5)). % 6.94/2.66 tff(c_604, plain, (select(a_1392, n34)=e34)). % 6.94/2.66 tff(c_691, plain, (select(a_1369, n11)=e11)). % 6.94/2.66 tff(c_715, plain, (select(a_1362, n4)=e4)). % 6.94/2.66 tff(c_592, plain, (select(a_1395, n37)=e37)). % 6.94/2.66 tff(c_688, plain, (select(a_1433, n30)=e30)). % 6.94/2.66 tff(c_589, plain, (select(a_1396, n38)=e38)). % 6.94/2.66 tff(c_541, plain, (select(a_1409, n37)=e37)). % 6.94/2.66 tff(c_718, plain, (select(a_1435, n34)=e34)). % 6.94/2.66 tff(c_550, plain, (select(a_1423, n33)=e33)). % 6.94/2.66 tff(c_685, plain, (select(a_1370, n12)=e12)). % 6.94/2.66 tff(c_607, plain, (select(a_1391, n33)=e33)). % 6.94/2.66 tff(c_721, plain, (select(a_1361, n3)=e3)). % 6.94/2.66 tff(c_724, plain, (select(a_1360, n2)=e2)). % 6.94/2.66 tff(c_517, plain, (select(a_1398, n40)=e40)). % 6.94/2.66 tff(c_505, plain, (select(a_1400, n14)=e14)). % 6.94/2.66 tff(c_499, plain, (select(a_1402, n11)=e11)). % 6.94/2.66 tff(c_727, plain, (select(a_1359, n1)=e1)). % 6.94/2.66 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))). % 6.94/2.66 tff(c_730, plain, (select(a_1436, n28)=e28)). % 6.94/2.66 tff(c_733, plain, (select(a_1438, n19)=e19)). % 6.94/2.66 tff(c_496, plain, (select(a_1437, n29)=e29)). % 6.94/2.66 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 6.94/2.66 tff(c_162, plain, (store(a_1436, n29, e29)=a_1437)). % 6.94/2.66 tff(c_92, plain, (store(a_1401, n11, e11)=a_1402)). % 6.94/2.66 tff(c_90, plain, (store(a_1400, n24, e24)=a_1401)). % 6.94/2.66 tff(c_88, plain, (store(a_1399, n14, e14)=a_1400)). % 6.94/2.66 tff(c_94, plain, (store(a_1402, n25, e25)=a_1403)). % 6.94/2.66 tff(c_108, plain, (store(a_1409, n31, e31)=a_1410)). % 6.94/2.66 tff(c_86, plain, (store(a1, n16, e16)=a_1399)). % 6.94/2.66 tff(c_84, plain, (store(a_1397, n40, e40)=a_1398)). % 6.94/2.66 tff(c_82, plain, (store(a_1396, n39, e39)=a_1397)). % 6.94/2.66 tff(c_118, plain, (store(a_1414, n35, e35)=a_1415)). % 6.94/2.66 tff(c_96, plain, (store(a_1403, n17, e17)=a_1404)). % 6.94/2.66 tff(c_114, plain, (store(a_1412, n36, e36)=a_1413)). % 6.94/2.66 tff(c_112, plain, (store(a_1411, n12, e12)=a_1412)). % 6.94/2.66 tff(c_110, plain, (store(a_1410, n13, e13)=a_1411)). % 6.94/2.66 tff(c_98, plain, (store(a_1404, n7, e7)=a_1405)). % 6.94/2.66 tff(c_106, plain, (store(a_1408, n37, e37)=a_1409)). % 6.94/2.66 tff(c_40, plain, (store(a_1375, n18, e18)=a_1376)). % 6.94/2.66 tff(c_152, plain, (store(a_1431, n4, e4)=a_1432)). % 6.94/2.66 tff(c_134, plain, (store(a_1422, n33, e33)=a_1423)). % 6.94/2.66 tff(c_132, plain, (store(a_1421, n8, e8)=a_1422)). % 6.94/2.66 tff(c_100, plain, (store(a_1405, n32, e32)=a_1406)). % 6.94/2.66 tff(c_32, plain, (store(a_1371, n14, e14)=a_1372)). % 6.94/2.66 tff(c_104, plain, (store(a_1407, n18, e18)=a_1408)). % 6.94/2.66 tff(c_128, plain, (store(a_1419, n10, e10)=a_1420)). % 6.94/2.66 tff(c_102, plain, (store(a_1406, n6, e6)=a_1407)). % 6.94/2.66 tff(c_126, plain, (store(a_1418, n27, e27)=a_1419)). % 6.94/2.66 tff(c_124, plain, (store(a_1417, n21, e21)=a_1418)). % 6.94/2.66 tff(c_122, plain, (store(a_1416, n26, e26)=a_1417)). % 6.94/2.66 tff(c_120, plain, (store(a_1415, n23, e23)=a_1416)). % 6.94/2.66 tff(c_116, plain, (store(a_1413, n20, e20)=a_1414)). % 6.94/2.66 tff(c_138, plain, (store(a_1424, n40, e40)=a_1425)). % 6.94/2.66 tff(c_80, plain, (store(a_1395, n38, e38)=a_1396)). % 6.94/2.66 tff(c_78, plain, (store(a_1394, n37, e37)=a_1395)). % 6.94/2.66 tff(c_76, plain, (store(a_1393, n36, e36)=a_1394)). % 6.94/2.66 tff(c_140, plain, (store(a_1425, n38, e38)=a_1426)). % 6.94/2.66 tff(c_74, plain, (store(a_1392, n35, e35)=a_1393)). % 6.94/2.66 tff(c_72, plain, (store(a_1391, n34, e34)=a_1392)). % 6.94/2.66 tff(c_70, plain, (store(a_1390, n33, e33)=a_1391)). % 6.94/2.66 tff(c_68, plain, (store(a_1389, n32, e32)=a_1390)). % 6.94/2.66 tff(c_66, plain, (store(a_1388, n31, e31)=a_1389)). % 6.94/2.66 tff(c_142, plain, (store(a_1426, n39, e39)=a_1427)). % 6.94/2.66 tff(c_64, plain, (store(a_1387, n30, e30)=a_1388)). % 6.94/2.66 tff(c_62, plain, (store(a_1386, n29, e29)=a_1387)). % 6.94/2.66 tff(c_60, plain, (store(a_1385, n28, e28)=a_1386)). % 6.94/2.66 tff(c_144, plain, (store(a_1427, n1, e1)=a_1428)). % 6.94/2.66 tff(c_58, plain, (store(a_1384, n27, e27)=a_1385)). % 6.94/2.66 tff(c_56, plain, (store(a_1383, n26, e26)=a_1384)). % 6.94/2.66 tff(c_54, plain, (store(a_1382, n25, e25)=a_1383)). % 6.94/2.66 tff(c_52, plain, (store(a_1381, n24, e24)=a_1382)). % 6.94/2.66 tff(c_50, plain, (store(a_1380, n23, e23)=a_1381)). % 6.94/2.66 tff(c_146, plain, (store(a_1428, n9, e9)=a_1429)). % 6.94/2.66 tff(c_48, plain, (store(a_1379, n22, e22)=a_1380)). % 6.94/2.66 tff(c_46, plain, (store(a_1378, n21, e21)=a_1379)). % 6.94/2.66 tff(c_44, plain, (store(a_1377, n20, e20)=a_1378)). % 6.94/2.66 tff(c_148, plain, (store(a_1429, n3, e3)=a_1430)). % 6.94/2.66 tff(c_42, plain, (store(a_1376, n19, e19)=a_1377)). % 6.94/2.66 tff(c_136, plain, (store(a_1423, n2, e2)=a_1424)). % 6.94/2.67 tff(c_38, plain, (store(a_1374, n17, e17)=a_1375)). % 6.94/2.67 tff(c_36, plain, (store(a_1373, n16, e16)=a_1374)). % 6.94/2.67 tff(c_34, plain, (store(a_1372, n15, e15)=a_1373)). % 6.94/2.67 tff(c_150, plain, (store(a_1430, n5, e5)=a_1431)). % 6.94/2.67 tff(c_130, plain, (store(a_1420, n22, e22)=a_1421)). % 6.94/2.67 tff(c_30, plain, (store(a_1370, n13, e13)=a_1371)). % 6.94/2.67 tff(c_28, plain, (store(a_1369, n12, e12)=a_1370)). % 6.94/2.67 tff(c_154, plain, (store(a_1432, n30, e30)=a_1433)). % 6.94/2.67 tff(c_26, plain, (store(a_1368, n11, e11)=a_1369)). % 6.94/2.67 tff(c_24, plain, (store(a_1367, n10, e10)=a_1368)). % 6.94/2.67 tff(c_22, plain, (store(a_1366, n9, e9)=a_1367)). % 6.94/2.67 tff(c_20, plain, (store(a_1365, n8, e8)=a_1366)). % 6.94/2.67 tff(c_18, plain, (store(a_1364, n7, e7)=a_1365)). % 6.94/2.67 tff(c_156, plain, (store(a_1433, n15, e15)=a_1434)). % 6.94/2.67 tff(c_16, plain, (store(a_1363, n6, e6)=a_1364)). % 6.94/2.67 tff(c_14, plain, (store(a_1362, n5, e5)=a_1363)). % 6.94/2.67 tff(c_12, plain, (store(a_1361, n4, e4)=a_1362)). % 6.94/2.67 tff(c_158, plain, (store(a_1434, n34, e34)=a_1435)). % 6.94/2.67 tff(c_10, plain, (store(a_1360, n3, e3)=a_1361)). % 6.94/2.67 tff(c_8, plain, (store(a_1359, n2, e2)=a_1360)). % 6.94/2.67 tff(c_6, plain, (store(a1, n1, e1)=a_1359)). % 6.94/2.67 tff(c_160, plain, (store(a_1435, n28, e28)=a_1436)). % 6.94/2.67 tff(c_164, plain, (store(a_1437, n19, e19)=a_1438)). % 6.94/2.67 tff(c_166, plain, (a_1438!=a_1398)). % 6.94/2.67 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.94/2.67 %------------------------------------------------------------------------------