%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV508-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/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 : n009.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:30:56 PM UTC 2025 % Result : Satisfiable 7.58s 2.76s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SWV508-1.040 : TPTP v9.0.0. Released v4.0.0. % 0.08/0.13 % 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.14/0.34 % Computer : n009.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 03:40:11 EDT 2025 % 0.14/0.34 % CPUTime : % 7.58/2.76 % 7.58/2.76 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.58/2.76 % 7.58/2.76 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.58/2.77 %$ store > sk > 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 > i_1490 > e_1492 > e_1491 > 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_1489 > a_1488 > a_1487 > a_1486 > a_1485 > a_1484 > a_1483 > a_1482 > a_1481 > a_1480 > a_1479 > a_1478 > a_1477 > a_1476 > a_1475 > a_1474 > a_1473 > a_1472 > a_1471 > a_1470 > a_1469 > a_1468 > a_1467 > a_1466 > a_1465 > a_1464 > a_1463 > a_1462 > a_1461 > a_1460 > a_1459 > a_1458 > a_1457 > a_1456 > a_1455 > a_1454 > a_1453 > a_1452 > a_1451 > a_1450 > a_1449 > a_1448 > a_1447 > a_1446 > a_1445 > a_1444 > a_1443 > a_1442 > a_1441 > a_1440 > a_1439 > 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 > a1 % 7.58/2.77 % 7.58/2.77 %Foreground sorts: % 7.58/2.77 % 7.58/2.77 % 7.58/2.77 %Background operators: % 7.58/2.77 % 7.58/2.77 % 7.58/2.77 %Foreground operators: % 7.58/2.77 tff(e29, type, e29: $i). % 7.58/2.77 tff(a1, type, a1: $i). % 7.58/2.77 tff(n22, type, n22: $i). % 7.58/2.77 tff(a_1468, type, a_1468: $i). % 7.58/2.77 tff(n27, type, n27: $i). % 7.58/2.77 tff(a_1424, type, a_1424: $i). % 7.58/2.77 tff(a_1456, type, a_1456: $i). % 7.58/2.77 tff(n16, type, n16: $i). % 7.58/2.77 tff(a_1453, type, a_1453: $i). % 7.58/2.77 tff(n12, type, n12: $i). % 7.58/2.77 tff(e1, type, e1: $i). % 7.58/2.77 tff(a_1442, type, a_1442: $i). % 7.58/2.77 tff(a_1460, type, a_1460: $i). % 7.58/2.77 tff(e8, type, e8: $i). % 7.58/2.77 tff(a_1449, type, a_1449: $i). % 7.58/2.77 tff(a_1452, type, a_1452: $i). % 7.58/2.77 tff(e21, type, e21: $i). % 7.58/2.77 tff(a_1489, type, a_1489: $i). % 7.58/2.77 tff(n24, type, n24: $i). % 7.58/2.77 tff(a_1431, type, a_1431: $i). % 7.58/2.77 tff(a_1475, type, a_1475: $i). % 7.58/2.77 tff(e15, type, e15: $i). % 7.58/2.77 tff(a_1446, type, a_1446: $i). % 7.58/2.77 tff(a_1415, type, a_1415: $i). % 7.58/2.77 tff(a_1464, type, a_1464: $i). % 7.58/2.77 tff(e33, type, e33: $i). % 7.58/2.77 tff(n35, type, n35: $i). % 7.58/2.77 tff(a_1459, type, a_1459: $i). % 7.58/2.77 tff(e40, type, e40: $i). % 7.58/2.77 tff(a_1412, type, a_1412: $i). % 7.58/2.77 tff(e18, type, e18: $i). % 7.58/2.77 tff(e38, type, e38: $i). % 7.58/2.77 tff(a_1437, type, a_1437: $i). % 7.58/2.77 tff(e24, type, e24: $i). % 7.58/2.77 tff(e31, type, e31: $i). % 7.58/2.77 tff(n33, type, n33: $i). % 7.58/2.77 tff(n36, type, n36: $i). % 7.58/2.77 tff(a_1432, type, a_1432: $i). % 7.58/2.77 tff(a_1429, type, a_1429: $i). % 7.58/2.77 tff(e39, type, e39: $i). % 7.58/2.77 tff(a_1486, type, a_1486: $i). % 7.58/2.77 tff(store, type, store: ($i * $i * $i) > $i). % 7.58/2.77 tff(n23, type, n23: $i). % 7.58/2.77 tff(n8, type, n8: $i). % 7.58/2.77 tff(a_1436, type, a_1436: $i). % 7.58/2.77 tff(e20, type, e20: $i). % 7.58/2.77 tff(e19, type, e19: $i). % 7.58/2.77 tff(e16, type, e16: $i). % 7.58/2.77 tff(n30, type, n30: $i). % 7.58/2.77 tff(a_1476, type, a_1476: $i). % 7.58/2.77 tff(a_1420, type, a_1420: $i). % 7.58/2.77 tff(e35, type, e35: $i). % 7.58/2.77 tff(a_1470, type, a_1470: $i). % 7.58/2.77 tff(e2, type, e2: $i). % 7.58/2.77 tff(n28, type, n28: $i). % 7.58/2.77 tff(a_1466, type, a_1466: $i). % 7.58/2.77 tff(n9, type, n9: $i). % 7.58/2.77 tff(a_1413, type, a_1413: $i). % 7.58/2.77 tff(a_1423, type, a_1423: $i). % 7.58/2.77 tff(e37, type, e37: $i). % 7.58/2.77 tff(e13, type, e13: $i). % 7.58/2.77 tff(n3, type, n3: $i). % 7.58/2.77 tff(a_1417, type, a_1417: $i). % 7.58/2.77 tff(a_1477, type, a_1477: $i). % 7.58/2.77 tff(a_1430, type, a_1430: $i). % 7.58/2.77 tff(e32, type, e32: $i). % 7.58/2.77 tff(e22, type, e22: $i). % 7.58/2.77 tff(n39, type, n39: $i). % 7.58/2.77 tff(a_1482, type, a_1482: $i). % 7.58/2.77 tff(a_1462, type, a_1462: $i). % 7.58/2.77 tff(a_1461, type, a_1461: $i). % 7.58/2.77 tff(e34, type, e34: $i). % 7.58/2.77 tff(n1, type, n1: $i). % 7.58/2.77 tff(a_1467, type, a_1467: $i). % 7.58/2.77 tff(a_1447, type, a_1447: $i). % 7.58/2.77 tff(e_1491, type, e_1491: $i). % 7.58/2.77 tff(a_1471, type, a_1471: $i). % 7.58/2.77 tff(a_1473, type, a_1473: $i). % 7.58/2.77 tff(n29, type, n29: $i). % 7.58/2.77 tff(e9, type, e9: $i). % 7.58/2.77 tff(n37, type, n37: $i). % 7.58/2.77 tff(a_1418, type, a_1418: $i). % 7.58/2.77 tff(n7, type, n7: $i). % 7.58/2.77 tff(e25, type, e25: $i). % 7.58/2.77 tff(i_1490, type, i_1490: $i). % 7.58/2.77 tff(e26, type, e26: $i). % 7.58/2.77 tff(a_1458, type, a_1458: $i). % 7.58/2.77 tff(n6, type, n6: $i). % 7.58/2.77 tff(a_1443, type, a_1443: $i). % 7.58/2.77 tff(e17, type, e17: $i). % 7.58/2.77 tff(n26, type, n26: $i). % 7.58/2.77 tff(e27, type, e27: $i). % 7.58/2.77 tff(e10, type, e10: $i). % 7.58/2.77 tff(e7, type, e7: $i). % 7.58/2.77 tff(a_1463, type, a_1463: $i). % 7.58/2.77 tff(a_1421, type, a_1421: $i). % 7.58/2.77 tff(n13, type, n13: $i). % 7.58/2.77 tff(a_1469, type, a_1469: $i). % 7.58/2.77 tff(a_1425, type, a_1425: $i). % 7.58/2.77 tff(a_1422, type, a_1422: $i). % 7.58/2.77 tff(sk, type, sk: ($i * $i) > $i). % 7.58/2.77 tff(a_1451, type, a_1451: $i). % 7.58/2.77 tff(e36, type, e36: $i). % 7.58/2.77 tff(a_1416, type, a_1416: $i). % 7.58/2.77 tff(a_1426, type, a_1426: $i). % 7.58/2.77 tff(n4, type, n4: $i). % 7.58/2.77 tff(n10, type, n10: $i). % 7.58/2.77 tff(n14, type, n14: $i). % 7.58/2.77 tff(n15, type, n15: $i). % 7.58/2.77 tff(a_1465, type, a_1465: $i). % 7.58/2.77 tff(n17, type, n17: $i). % 7.58/2.77 tff(n40, type, n40: $i). % 7.58/2.77 tff(e30, type, e30: $i). % 7.58/2.77 tff(select, type, select: ($i * $i) > $i). % 7.58/2.77 tff(a_1478, type, a_1478: $i). % 7.58/2.77 tff(a_1419, type, a_1419: $i). % 7.58/2.77 tff(n31, type, n31: $i). % 7.58/2.77 tff(a_1433, type, a_1433: $i). % 7.58/2.77 tff(a_1455, type, a_1455: $i). % 7.58/2.77 tff(a_1474, type, a_1474: $i). % 7.58/2.77 tff(a_1411, type, a_1411: $i). % 7.58/2.77 tff(n32, type, n32: $i). % 7.58/2.77 tff(a_1435, type, a_1435: $i). % 7.58/2.77 tff(a_1481, type, a_1481: $i). % 7.58/2.77 tff(a_1480, type, a_1480: $i). % 7.58/2.77 tff(n20, type, n20: $i). % 7.58/2.77 tff(e23, type, e23: $i). % 7.58/2.77 tff(n18, type, n18: $i). % 7.58/2.77 tff(n38, type, n38: $i). % 7.58/2.77 tff(a_1445, type, a_1445: $i). % 7.58/2.77 tff(e14, type, e14: $i). % 7.58/2.77 tff(a_1414, type, a_1414: $i). % 7.58/2.77 tff(a_1428, type, a_1428: $i). % 7.58/2.77 tff(a_1487, type, a_1487: $i). % 7.58/2.77 tff(a_1440, type, a_1440: $i). % 7.58/2.77 tff(a_1485, type, a_1485: $i). % 7.58/2.77 tff(a_1439, type, a_1439: $i). % 7.58/2.77 tff(n11, type, n11: $i). % 7.58/2.77 tff(a_1483, type, a_1483: $i). % 7.58/2.77 tff(a_1410, type, a_1410: $i). % 7.58/2.77 tff(a_1488, type, a_1488: $i). % 7.58/2.77 tff(e12, type, e12: $i). % 7.58/2.77 tff(e4, type, e4: $i). % 7.58/2.77 tff(e_1492, type, e_1492: $i). % 7.58/2.77 tff(a_1434, type, a_1434: $i). % 7.58/2.77 tff(n34, type, n34: $i). % 7.58/2.77 tff(a_1454, type, a_1454: $i). % 7.58/2.77 tff(a_1441, type, a_1441: $i). % 7.58/2.77 tff(a_1450, type, a_1450: $i). % 7.58/2.77 tff(a_1438, type, a_1438: $i). % 7.58/2.77 tff(e6, type, e6: $i). % 7.58/2.77 tff(n19, type, n19: $i). % 7.58/2.77 tff(a_1427, type, a_1427: $i). % 7.58/2.77 tff(a_1457, type, a_1457: $i). % 7.58/2.77 tff(n2, type, n2: $i). % 7.58/2.77 tff(e11, type, e11: $i). % 7.58/2.77 tff(a_1479, type, a_1479: $i). % 7.58/2.77 tff(a_1448, type, a_1448: $i). % 7.58/2.77 tff(e28, type, e28: $i). % 7.58/2.77 tff(n5, type, n5: $i). % 7.58/2.77 tff(a_1444, type, a_1444: $i). % 7.58/2.77 tff(e3, type, e3: $i). % 7.58/2.77 tff(a_1484, type, a_1484: $i). % 7.58/2.77 tff(n25, type, n25: $i). % 7.58/2.77 tff(e5, type, e5: $i). % 7.58/2.77 tff(n21, type, n21: $i). % 7.58/2.77 tff(a_1472, type, a_1472: $i). % 7.58/2.77 % 7.58/2.77 %Saturated clause set: % 7.58/2.77 tff(c_1868, plain, (![J_14]: (select(a_1428, J_14)=select(a_1427, J_14) | i_1490=J_14))). % 7.58/2.77 tff(c_2756, plain, (![J_14]: (select(a_1410, J_14)=select(a1, J_14) | i_1490=J_14))). % 7.58/2.77 tff(c_2754, plain, (![J_14]: (select(a_1449, J_14)=select(a_1448, J_14) | i_1490=J_14))). % 7.58/2.77 tff(c_2755, plain, (![J_14]: (select(a_1479, J_14)=select(a_1478, J_14) | i_1490=J_14))). % 7.58/2.77 tff(c_1867, plain, (![J_14]: (select(a_1489, J_14)=select(a_1488, J_14) | i_1490=J_14))). % 7.58/2.77 tff(c_2761, plain, (store(a_1448, i_1490, e1)=a_1449)). % 7.58/2.77 tff(c_2762, plain, (store(a_1478, i_1490, e1)=a_1479)). % 7.58/2.77 tff(c_2759, plain, (select(a_1410, i_1490)=e1)). % 7.58/2.77 tff(c_2786, plain, (e19!=e1)). % 7.58/2.77 tff(c_2781, plain, (e_1491=e1)). % 7.58/2.77 tff(c_2758, plain, (select(a_1449, i_1490)=e1)). % 7.58/2.77 tff(c_2760, plain, (store(a1, i_1490, e1)=a_1410)). % 7.58/2.77 tff(c_2757, plain, (select(a_1479, i_1490)=e1)). % 7.58/2.77 tff(c_2753, plain, (n1=i_1490)). % 7.58/2.77 tff(c_972, plain, (![J_14]: (select(a_1487, J_14)=select(a_1486, J_14) | n28=J_14))). % 7.58/2.77 tff(c_852, plain, (![J_14]: (select(a_1461, J_14)=select(a_1460, J_14) | n31=J_14))). % 7.58/2.77 tff(c_834, plain, (![J_14]: (select(a_1425, J_14)=select(a_1424, J_14) | n16=J_14))). % 7.58/2.77 tff(c_891, plain, (![J_14]: (select(a_1442, J_14)=select(a_1441, J_14) | n33=J_14))). % 7.58/2.77 tff(c_996, plain, (![J_14]: (select(a_1414, J_14)=select(a_1413, J_14) | n5=J_14))). % 7.58/2.77 tff(c_846, plain, (![J_14]: (select(a_1472, J_14)=select(a_1471, J_14) | n22=J_14))). % 7.58/2.77 tff(c_963, plain, (![J_14]: (select(a_1423, J_14)=select(a_1422, J_14) | n14=J_14))). % 7.58/2.77 tff(c_828, plain, (![J_14]: (select(a_1476, J_14)=select(a_1475, J_14) | n40=J_14))). % 7.58/2.77 tff(c_810, plain, (![J_14]: (select(a_1458, J_14)=select(a_1457, J_14) | n6=J_14))). % 7.58/2.77 tff(c_840, plain, (![J_14]: (select(a_1460, J_14)=select(a_1459, J_14) | n37=J_14))). % 7.58/2.77 tff(c_786, plain, (![J_14]: (select(a_1465, J_14)=select(a_1464, J_14) | n20=J_14))). % 7.58/2.78 tff(c_987, plain, (![J_14]: (select(a_1416, J_14)=select(a_1415, J_14) | n7=J_14))). % 7.58/2.78 tff(c_837, plain, (![J_14]: (select(a_1462, J_14)=select(a_1461, J_14) | n13=J_14))). % 7.58/2.78 tff(c_984, plain, (![J_14]: (select(a_1417, J_14)=select(a_1416, J_14) | n8=J_14))). % 7.58/2.78 tff(c_795, plain, (![J_14]: (select(a_1451, J_14)=select(a_1450, J_14) | n14=J_14))). % 7.58/2.78 tff(c_951, plain, (![J_14]: (select(a_1426, J_14)=select(a_1425, J_14) | n17=J_14))). % 7.58/2.78 tff(c_885, plain, (![J_14]: (select(a_1444, J_14)=select(a_1443, J_14) | n35=J_14))). % 7.58/2.78 tff(c_981, plain, (![J_14]: (select(a_1418, J_14)=select(a_1417, J_14) | n9=J_14))). % 7.58/2.78 tff(c_813, plain, (![J_14]: (select(a_1463, J_14)=select(a_1462, J_14) | n12=J_14))). % 7.58/2.78 tff(c_1005, plain, (![J_14]: (select(a_1412, J_14)=select(a_1411, J_14) | n3=J_14))). % 7.58/2.78 tff(c_897, plain, (![J_14]: (select(a_1440, J_14)=select(a_1439, J_14) | n31=J_14))). % 7.58/2.78 tff(c_777, plain, (![J_14]: (select(a_1454, J_14)=select(a_1453, J_14) | n25=J_14))). % 7.58/2.78 tff(c_792, plain, (![J_14]: (select(a_1457, J_14)=select(a_1456, J_14) | n32=J_14))). % 7.58/2.78 tff(c_903, plain, (![J_14]: (select(a_1439, J_14)=select(a_1438, J_14) | n30=J_14))). % 7.58/2.78 tff(c_804, plain, (![J_14]: (select(a_1466, J_14)=select(a_1465, J_14) | n35=J_14))). % 7.58/2.78 tff(c_855, plain, (![J_14]: (select(a_1470, J_14)=select(a_1469, J_14) | n27=J_14))). % 7.58/2.78 tff(c_876, plain, (![J_14]: (select(a_1446, J_14)=select(a_1445, J_14) | n37=J_14))). % 7.58/2.78 tff(c_933, plain, (![J_14]: (select(a_1431, J_14)=select(a_1430, J_14) | n22=J_14))). % 7.58/2.78 tff(c_966, plain, (![J_14]: (select(a_1422, J_14)=select(a_1421, J_14) | n13=J_14))). % 7.58/2.78 tff(c_960, plain, (![J_14]: (select(a_1485, J_14)=select(a_1484, J_14) | n15=J_14))). % 7.58/2.78 tff(c_798, plain, (![J_14]: (select(a_1469, J_14)=select(a_1468, J_14) | n21=J_14))). % 7.58/2.78 tff(c_849, plain, (![J_14]: (select(a_1471, J_14)=select(a_1470, J_14) | n10=J_14))). % 7.58/2.78 tff(c_978, plain, (![J_14]: (select(a_1419, J_14)=select(a_1418, J_14) | n10=J_14))). % 7.58/2.78 tff(c_801, plain, (![J_14]: (select(a_1467, J_14)=select(a_1466, J_14) | n23=J_14))). % 7.58/2.78 tff(c_975, plain, (![J_14]: (select(a_1420, J_14)=select(a_1419, J_14) | n11=J_14))). % 7.58/2.78 tff(c_924, plain, (![J_14]: (select(a_1433, J_14)=select(a_1432, J_14) | n24=J_14))). % 7.58/2.78 tff(c_831, plain, (![J_14]: (select(a_1475, J_14)=select(a_1474, J_14) | n2=J_14))). % 7.58/2.78 tff(c_825, plain, (![J_14]: (select(a_1477, J_14)=select(a_1476, J_14) | n38=J_14))). % 7.58/2.78 tff(c_954, plain, (![J_14]: (select(a_1474, J_14)=select(a_1473, J_14) | n33=J_14))). % 7.58/2.78 tff(c_882, plain, (![J_14]: (select(a_1480, J_14)=select(a_1479, J_14) | n9=J_14))). % 7.58/2.78 tff(c_939, plain, (![J_14]: (select(a_1429, J_14)=select(a_1428, J_14) | n20=J_14))). % 7.58/2.78 tff(c_906, plain, (![J_14]: (select(a_1438, J_14)=select(a_1437, J_14) | n29=J_14))). % 7.58/2.78 tff(c_927, plain, (![J_14]: (select(a_1432, J_14)=select(a_1431, J_14) | n23=J_14))). % 7.58/2.78 tff(c_948, plain, (![J_14]: (select(a_1427, J_14)=select(a_1426, J_14) | n18=J_14))). % 7.58/2.78 tff(c_783, plain, (![J_14]: (select(a_1453, J_14)=select(a_1452, J_14) | n11=J_14))). % 7.58/2.78 tff(c_789, plain, (![J_14]: (select(a_1452, J_14)=select(a_1451, J_14) | n24=J_14))). % 7.58/2.78 tff(c_1872, plain, (store(a_1488, i_1490, e19)=a_1489)). % 7.58/2.78 tff(c_879, plain, (![J_14]: (select(a_1445, J_14)=select(a_1444, J_14) | n36=J_14))). % 7.58/2.78 tff(c_1891, plain, (e_1492=e19)). % 7.58/2.78 tff(c_1870, plain, (select(a_1489, i_1490)=e19)). % 7.58/2.78 tff(c_1869, plain, (select(a_1428, i_1490)=e19)). % 7.58/2.78 tff(c_1871, plain, (store(a_1427, i_1490, e19)=a_1428)). % 7.58/2.78 tff(c_1866, plain, (n19=i_1490)). % 7.58/2.78 tff(c_936, plain, (![J_14]: (select(a_1478, J_14)=select(a_1477, J_14) | n39=J_14))). % 7.58/2.78 tff(c_957, plain, (![J_14]: (select(a_1424, J_14)=select(a_1423, J_14) | n15=J_14))). % 7.58/2.78 tff(c_993, plain, (![J_14]: (select(a_1415, J_14)=select(a_1414, J_14) | n6=J_14))). % 7.58/2.78 tff(c_1008, plain, (![J_14]: (select(a_1411, J_14)=select(a_1410, J_14) | n2=J_14))). % 7.58/2.78 tff(c_888, plain, (![J_14]: (select(a_1443, J_14)=select(a_1442, J_14) | n34=J_14))). % 7.58/2.78 tff(c_930, plain, (![J_14]: (select(a_1483, J_14)=select(a_1482, J_14) | n4=J_14))). % 7.58/2.78 tff(c_912, plain, (![J_14]: (select(a_1482, J_14)=select(a_1481, J_14) | n5=J_14))). % 7.58/2.78 tff(c_915, plain, (![J_14]: (select(a_1436, J_14)=select(a_1435, J_14) | n27=J_14))). % 7.58/2.78 tff(c_807, plain, (![J_14]: (select(a_1464, J_14)=select(a_1463, J_14) | n36=J_14))). % 7.58/2.78 tff(c_909, plain, (![J_14]: (select(a_1437, J_14)=select(a_1436, J_14) | n28=J_14))). % 7.58/2.78 tff(c_822, plain, (![J_14]: (select(a_1459, J_14)=select(a_1458, J_14) | n18=J_14))). % 7.58/2.78 tff(c_861, plain, (![J_14]: (select(a_1450, J_14)=select(a1, J_14) | n16=J_14))). % 7.58/2.78 tff(c_918, plain, (![J_14]: (select(a_1435, J_14)=select(a_1434, J_14) | n26=J_14))). % 7.58/2.78 tff(c_873, plain, (![J_14]: (select(a_1447, J_14)=select(a_1446, J_14) | n38=J_14))). % 7.58/2.78 tff(c_999, plain, (![J_14]: (select(a_1413, J_14)=select(a_1412, J_14) | n4=J_14))). % 7.58/2.78 tff(c_867, plain, (![J_14]: (select(a_1448, J_14)=select(a_1447, J_14) | n39=J_14))). % 7.58/2.78 tff(c_819, plain, (![J_14]: (select(a_1486, J_14)=select(a_1485, J_14) | n34=J_14))). % 7.58/2.78 tff(c_816, plain, (![J_14]: (select(a_1430, J_14)=select(a_1429, J_14) | n21=J_14))). % 7.58/2.78 tff(c_780, plain, (![J_14]: (select(a_1456, J_14)=select(a_1455, J_14) | n7=J_14))). % 7.58/2.78 tff(c_900, plain, (![J_14]: (select(a_1481, J_14)=select(a_1480, J_14) | n3=J_14))). % 7.58/2.78 tff(c_942, plain, (![J_14]: (select(a_1484, J_14)=select(a_1483, J_14) | n30=J_14))). % 7.58/2.78 tff(c_843, plain, (![J_14]: (select(a_1473, J_14)=select(a_1472, J_14) | n8=J_14))). % 7.58/2.78 tff(c_858, plain, (![J_14]: (select(a_1468, J_14)=select(a_1467, J_14) | n26=J_14))). % 7.58/2.78 tff(c_969, plain, (![J_14]: (select(a_1421, J_14)=select(a_1420, J_14) | n12=J_14))). % 7.58/2.79 tff(c_894, plain, (![J_14]: (select(a_1441, J_14)=select(a_1440, J_14) | n32=J_14))). % 7.58/2.79 tff(c_990, plain, (![J_14]: (select(a_1488, J_14)=select(a_1487, J_14) | n29=J_14))). % 7.58/2.79 tff(c_774, plain, (![J_14]: (select(a_1455, J_14)=select(a_1454, J_14) | n17=J_14))). % 7.58/2.79 tff(c_921, plain, (![J_14]: (select(a_1434, J_14)=select(a_1433, J_14) | n25=J_14))). % 7.58/2.79 tff(c_583, plain, (select(a_1460, n37)=e37)). % 7.58/2.79 tff(c_658, plain, (select(a_1436, n27)=e27)). % 7.58/2.79 tff(c_586, plain, (select(a_1473, n8)=e8)). % 7.58/2.79 tff(c_661, plain, (select(a_1435, n26)=e26)). % 7.58/2.79 tff(c_664, plain, (select(a_1434, n25)=e25)). % 7.58/2.79 tff(c_667, plain, (select(a_1433, n24)=e24)). % 7.58/2.79 tff(c_529, plain, (select(a_1465, n20)=e20)). % 7.58/2.79 tff(c_652, plain, (select(a_1437, n28)=e28)). % 7.58/2.79 tff(c_550, plain, (select(a_1464, n36)=e36)). % 7.58/2.79 tff(c_580, plain, (select(a_1462, n13)=e13)). % 7.58/2.79 tff(c_589, plain, (select(a_1472, n22)=e22)). % 7.58/2.79 tff(c_670, plain, (select(a_1432, n23)=e23)). % 7.58/2.79 tff(c_592, plain, (select(a_1471, n10)=e10)). % 7.58/2.79 tff(c_673, plain, (select(a_1483, n4)=e4)). % 7.58/2.79 tff(c_547, plain, (select(a_1466, n35)=e35)). % 7.58/2.79 tff(c_676, plain, (select(a_1431, n22)=e22)). % 7.58/2.79 tff(c_655, plain, (select(a_1482, n5)=e5)). % 7.58/2.79 tff(c_553, plain, (select(a_1458, n6)=e6)). % 7.58/2.79 tff(c_577, plain, (select(a_1425, n16)=e16)). % 7.58/2.79 tff(c_700, plain, (select(a_1424, n15)=e15)). % 7.58/2.79 tff(c_604, plain, (select(a_1450, n16)=e16)). % 7.58/2.79 tff(c_646, plain, (select(a_1439, n30)=e30)). % 7.58/2.79 tff(c_649, plain, (select(a_1438, n29)=e29)). % 7.58/2.79 tff(c_595, plain, (select(a_1461, n31)=e31)). % 7.58/2.79 tff(c_679, plain, (select(a_1478, n39)=e39)). % 7.58/2.79 tff(c_643, plain, (select(a_1481, n3)=e3)). % 7.58/2.79 tff(c_544, plain, (select(a_1467, n23)=e23)). % 7.58/2.79 tff(c_637, plain, (select(a_1441, n32)=e32)). % 7.58/2.79 tff(c_574, plain, (select(a_1475, n2)=e2)). % 7.58/2.79 tff(c_634, plain, (select(a_1442, n33)=e33)). % 7.58/2.79 tff(c_682, plain, (select(a_1429, n20)=e20)). % 7.58/2.79 tff(c_598, plain, (select(a_1470, n27)=e27)). % 7.58/2.79 tff(c_685, plain, (select(a_1484, n30)=e30)). % 7.58/2.79 tff(c_640, plain, (select(a_1440, n31)=e31)). % 7.58/2.79 tff(c_601, plain, (select(a_1468, n26)=e26)). % 7.58/2.79 tff(c_631, plain, (select(a_1443, n34)=e34)). % 7.58/2.79 tff(c_556, plain, (select(a_1463, n12)=e12)). % 7.58/2.79 tff(c_571, plain, (select(a_1476, n40)=e40)). % 7.58/2.79 tff(c_541, plain, (select(a_1469, n21)=e21)). % 7.58/2.79 tff(c_691, plain, (select(a_1427, n18)=e18)). % 7.58/2.79 tff(c_751, plain, (select(a_1411, n2)=e2)). % 7.58/2.79 tff(c_694, plain, (select(a_1426, n17)=e17)). % 7.58/2.79 tff(c_532, plain, (select(a_1452, n24)=e24)). % 7.58/2.79 tff(c_697, plain, (select(a_1474, n33)=e33)). % 7.58/2.79 tff(c_520, plain, (select(a_1454, n25)=e25)). % 7.58/2.79 tff(c_526, plain, (select(a_1453, n11)=e11)). % 7.58/2.79 tff(c_616, plain, (select(a_1447, n38)=e38)). % 7.58/2.79 tff(c_718, plain, (select(a_1420, n11)=e11)). % 7.58/2.79 tff(c_727, plain, (select(a_1417, n8)=e8)). % 7.58/2.79 tff(c_721, plain, (select(a_1419, n10)=e10)). % 7.58/2.79 tff(c_724, plain, (select(a_1418, n9)=e9)). % 7.58/2.79 tff(c_538, plain, (select(a_1451, n14)=e14)). % 7.58/2.79 tff(c_565, plain, (select(a_1459, n18)=e18)). % 7.58/2.79 tff(c_619, plain, (select(a_1446, n37)=e37)). % 7.58/2.79 tff(c_622, plain, (select(a_1445, n36)=e36)). % 7.58/2.79 tff(c_730, plain, (select(a_1416, n7)=e7)). % 7.58/2.79 tff(c_562, plain, (select(a_1486, n34)=e34)). % 7.58/2.79 tff(c_712, plain, (select(a_1421, n12)=e12)). % 7.58/2.79 tff(c_733, plain, (select(a_1488, n29)=e29)). % 7.58/2.79 tff(c_715, plain, (select(a_1487, n28)=e28)). % 7.58/2.79 tff(c_736, plain, (select(a_1415, n6)=e6)). % 7.58/2.79 tff(c_568, plain, (select(a_1477, n38)=e38)). % 7.58/2.79 tff(c_625, plain, (select(a_1480, n9)=e9)). % 7.58/2.79 tff(c_709, plain, (select(a_1422, n13)=e13)). % 7.58/2.79 tff(c_610, plain, (select(a_1448, n39)=e39)). % 7.58/2.79 tff(c_706, plain, (select(a_1423, n14)=e14)). % 7.58/2.79 tff(c_703, plain, (select(a_1485, n15)=e15)). % 7.58/2.79 tff(c_559, plain, (select(a_1430, n21)=e21)). % 7.58/2.79 tff(c_739, plain, (select(a_1414, n5)=e5)). % 7.58/2.79 tff(c_742, plain, (select(a_1413, n4)=e4)). % 7.58/2.79 tff(c_628, plain, (select(a_1444, n35)=e35)). % 7.58/2.79 tff(c_748, plain, (select(a_1412, n3)=e3)). % 7.58/2.79 tff(c_535, plain, (select(a_1457, n32)=e32)). % 7.58/2.79 tff(c_523, plain, (select(a_1456, n7)=e7)). % 7.58/2.79 tff(c_517, plain, (select(a_1455, n17)=e17)). % 7.58/2.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))). % 7.58/2.79 tff(c_2, plain, (![A_1, I_2, E_3]: (select(store(A_1, I_2, E_3), I_2)=E_3))). % 7.58/2.79 tff(c_96, plain, (store(a_1454, n17, e17)=a_1455)). % 7.58/2.79 tff(c_94, plain, (store(a_1453, n25, e25)=a_1454)). % 7.58/2.79 tff(c_98, plain, (store(a_1455, n7, e7)=a_1456)). % 7.58/2.79 tff(c_92, plain, (store(a_1452, n11, e11)=a_1453)). % 7.58/2.79 tff(c_116, plain, (store(a_1464, n20, e20)=a_1465)). % 7.58/2.79 tff(c_90, plain, (store(a_1451, n24, e24)=a_1452)). % 7.58/2.79 tff(c_100, plain, (store(a_1456, n32, e32)=a_1457)). % 7.58/2.79 tff(c_88, plain, (store(a_1450, n14, e14)=a_1451)). % 7.58/2.79 tff(c_124, plain, (store(a_1468, n21, e21)=a_1469)). % 7.58/2.79 tff(c_120, plain, (store(a_1466, n23, e23)=a_1467)). % 7.58/2.79 tff(c_118, plain, (store(a_1465, n35, e35)=a_1466)). % 7.58/2.79 tff(c_114, plain, (store(a_1463, n36, e36)=a_1464)). % 7.58/2.79 tff(c_102, plain, (store(a_1457, n6, e6)=a_1458)). % 7.58/2.79 tff(c_112, plain, (store(a_1462, n12, e12)=a_1463)). % 7.58/2.79 tff(c_46, plain, (store(a_1429, n21, e21)=a_1430)). % 7.58/2.79 tff(c_158, plain, (store(a_1485, n34, e34)=a_1486)). % 7.58/2.79 tff(c_104, plain, (store(a_1458, n18, e18)=a_1459)). % 7.58/2.79 tff(c_140, plain, (store(a_1476, n38, e38)=a_1477)). % 7.58/2.79 tff(c_138, plain, (store(a_1475, n40, e40)=a_1476)). % 7.58/2.79 tff(c_136, plain, (store(a_1474, n2, e2)=a_1475)). % 7.58/2.79 tff(c_36, plain, (store(a_1424, n16, e16)=a_1425)). % 7.58/2.79 tff(c_110, plain, (store(a_1461, n13, e13)=a_1462)). % 7.58/2.79 tff(c_106, plain, (store(a_1459, n37, e37)=a_1460)). % 7.58/2.79 tff(c_132, plain, (store(a_1472, n8, e8)=a_1473)). % 7.58/2.79 tff(c_130, plain, (store(a_1471, n22, e22)=a_1472)). % 7.58/2.79 tff(c_128, plain, (store(a_1470, n10, e10)=a_1471)). % 7.58/2.79 tff(c_108, plain, (store(a_1460, n31, e31)=a_1461)). % 7.58/2.80 tff(c_126, plain, (store(a_1469, n27, e27)=a_1470)). % 7.58/2.80 tff(c_122, plain, (store(a_1467, n26, e26)=a_1468)). % 7.58/2.80 tff(c_86, plain, (store(a1, n16, e16)=a_1450)). % 7.58/2.80 tff(c_82, plain, (store(a_1447, n39, e39)=a_1448)). % 7.58/2.80 tff(c_80, plain, (store(a_1446, n38, e38)=a_1447)). % 7.58/2.80 tff(c_78, plain, (store(a_1445, n37, e37)=a_1446)). % 7.58/2.80 tff(c_76, plain, (store(a_1444, n36, e36)=a_1445)). % 7.58/2.80 tff(c_146, plain, (store(a_1479, n9, e9)=a_1480)). % 7.58/2.80 tff(c_74, plain, (store(a_1443, n35, e35)=a_1444)). % 7.58/2.80 tff(c_72, plain, (store(a_1442, n34, e34)=a_1443)). % 7.58/2.80 tff(c_70, plain, (store(a_1441, n33, e33)=a_1442)). % 7.58/2.80 tff(c_68, plain, (store(a_1440, n32, e32)=a_1441)). % 7.58/2.80 tff(c_66, plain, (store(a_1439, n31, e31)=a_1440)). % 7.58/2.80 tff(c_148, plain, (store(a_1480, n3, e3)=a_1481)). % 7.58/2.80 tff(c_64, plain, (store(a_1438, n30, e30)=a_1439)). % 7.58/2.80 tff(c_62, plain, (store(a_1437, n29, e29)=a_1438)). % 7.58/2.80 tff(c_60, plain, (store(a_1436, n28, e28)=a_1437)). % 7.58/2.80 tff(c_150, plain, (store(a_1481, n5, e5)=a_1482)). % 7.58/2.80 tff(c_58, plain, (store(a_1435, n27, e27)=a_1436)). % 7.58/2.80 tff(c_56, plain, (store(a_1434, n26, e26)=a_1435)). % 7.58/2.80 tff(c_54, plain, (store(a_1433, n25, e25)=a_1434)). % 7.58/2.80 tff(c_52, plain, (store(a_1432, n24, e24)=a_1433)). % 7.58/2.80 tff(c_50, plain, (store(a_1431, n23, e23)=a_1432)). % 7.58/2.80 tff(c_152, plain, (store(a_1482, n4, e4)=a_1483)). % 7.58/2.80 tff(c_48, plain, (store(a_1430, n22, e22)=a_1431)). % 7.58/2.80 tff(c_142, plain, (store(a_1477, n39, e39)=a_1478)). % 7.58/2.80 tff(c_44, plain, (store(a_1428, n20, e20)=a_1429)). % 7.58/2.80 tff(c_154, plain, (store(a_1483, n30, e30)=a_1484)). % 7.58/2.80 tff(c_40, plain, (store(a_1426, n18, e18)=a_1427)). % 7.58/2.80 tff(c_38, plain, (store(a_1425, n17, e17)=a_1426)). % 7.58/2.80 tff(c_134, plain, (store(a_1473, n33, e33)=a_1474)). % 7.58/2.80 tff(c_34, plain, (store(a_1423, n15, e15)=a_1424)). % 7.58/2.80 tff(c_156, plain, (store(a_1484, n15, e15)=a_1485)). % 7.58/2.80 tff(c_32, plain, (store(a_1422, n14, e14)=a_1423)). % 7.58/2.80 tff(c_30, plain, (store(a_1421, n13, e13)=a_1422)). % 7.58/2.80 tff(c_28, plain, (store(a_1420, n12, e12)=a_1421)). % 7.58/2.80 tff(c_160, plain, (store(a_1486, n28, e28)=a_1487)). % 7.58/2.80 tff(c_26, plain, (store(a_1419, n11, e11)=a_1420)). % 7.58/2.80 tff(c_24, plain, (store(a_1418, n10, e10)=a_1419)). % 7.58/2.80 tff(c_22, plain, (store(a_1417, n9, e9)=a_1418)). % 7.58/2.80 tff(c_20, plain, (store(a_1416, n8, e8)=a_1417)). % 7.58/2.80 tff(c_18, plain, (store(a_1415, n7, e7)=a_1416)). % 7.58/2.80 tff(c_162, plain, (store(a_1487, n29, e29)=a_1488)). % 7.58/2.80 tff(c_16, plain, (store(a_1414, n6, e6)=a_1415)). % 7.58/2.80 tff(c_14, plain, (store(a_1413, n5, e5)=a_1414)). % 7.58/2.80 tff(c_12, plain, (store(a_1412, n4, e4)=a_1413)). % 7.58/2.80 tff(c_10, plain, (store(a_1411, n3, e3)=a_1412)). % 7.58/2.80 tff(c_8, plain, (store(a_1410, n2, e2)=a_1411)). % 7.58/2.80 tff(c_170, plain, (sk(a_1449, a_1489)=i_1490)). % 7.58/2.80 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.58/2.80 %------------------------------------------------------------------------------