%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MSC014-10 : TPTP v9.0.0. Released v7.5.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 : n018.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 07:45:09 PM UTC 2025 % Result : Satisfiable 17.82s 7.93s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : MSC014-10 : TPTP v9.0.0. Released v7.5.0. % 0.04/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.13/0.36 % Computer : n018.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 300 % 0.13/0.36 % DateTime : Tue Apr 8 07:57:32 EDT 2025 % 0.13/0.36 % CPUTime : % 17.82/7.93 % 17.82/7.93 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.82/7.93 % 17.82/7.93 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.82/7.94 %$ f > sK1_exists_f_Z > ifeq2 > ifeq > equalish > #nlpp > true > n1 > n0 > b > a % 17.82/7.94 % 17.82/7.94 %Foreground sorts: % 17.82/7.94 % 17.82/7.94 % 17.82/7.94 %Background operators: % 17.82/7.94 % 17.82/7.94 % 17.82/7.94 %Foreground operators: % 17.82/7.94 tff(a, type, a: $i). % 17.82/7.94 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 17.82/7.94 tff(b, type, b: $i). % 17.82/7.94 tff(n1, type, n1: $i). % 17.82/7.94 tff(equalish, type, equalish: ($i * $i) > $i). % 17.82/7.94 tff(n0, type, n0: $i). % 17.82/7.94 tff(sK1_exists_f_Z, type, sK1_exists_f_Z: ($i * $i * $i * $i) > $i). % 17.82/7.94 tff(true, type, true: $i). % 17.82/7.94 tff(f, type, f: ($i * $i * $i * $i * $i) > $i). % 17.82/7.94 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 17.82/7.94 % 17.82/7.94 %Saturated clause set: % 17.82/7.94 tff(c_27218, plain, (![X1_1485, X2_1486, X3_1487, X4_1488]: (ifeq2(f(X1_1485, X2_1486, X3_1487, X4_1488, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(X1_1485, n0), true)=true))). % 17.82/7.94 tff(c_27100, plain, (![X1_1477, X2_1478, X3_1479, X4_1480]: (ifeq2(f(X1_1477, X2_1478, X3_1479, X4_1480, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(X3_1479, n0), true)=true))). % 17.82/7.94 tff(c_26958, plain, (![X1_1469, X2_1470, X3_1471, X4_1472]: (ifeq2(f(X1_1469, X2_1470, X3_1471, X4_1472, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(X2_1470, n0), true)=true))). % 17.82/7.94 tff(c_26828, plain, (![X1_1461, X2_1462, X3_1463, X4_1464]: (ifeq2(f(X1_1461, X2_1462, X3_1463, X4_1464, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(X1_1461, n0), true)=true))). % 17.82/7.94 tff(c_26741, plain, (![X1_1453, X2_1454, X3_1455, X4_1456]: (ifeq2(f(X1_1453, X2_1454, X3_1455, X4_1456, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(X4_1456, n1), true)=true))). % 17.82/7.94 tff(c_26616, plain, (![X1_1445, X2_1446, X3_1447, X4_1448]: (ifeq2(f(X1_1445, X2_1446, X3_1447, X4_1448, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(X2_1446, n0), true)=true))). % 17.82/7.94 tff(c_26498, plain, (![X1_1437, X2_1438, X3_1439, X4_1440]: (ifeq2(f(X1_1437, X2_1438, X3_1439, X4_1440, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(X4_1440, n0), true)=true))). % 17.82/7.94 tff(c_26392, plain, (![X1_1429, X2_1430, X3_1431, X4_1432]: (ifeq2(f(X1_1429, X2_1430, X3_1431, X4_1432, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(X3_1431, n0), true)=true))). % 17.82/7.94 tff(c_26262, plain, (![X1_1421, X2_1422, X3_1423, X4_1424]: (ifeq2(f(X1_1421, X2_1422, X3_1423, X4_1424, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(X2_1422, n0), true)=true))). % 17.82/7.95 tff(c_26156, plain, (![X1_1413, X2_1414, X3_1415, X4_1416]: (ifeq2(f(X1_1413, X2_1414, X3_1415, X4_1416, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(X3_1415, n0), true)=true))). % 17.82/7.95 tff(c_26026, plain, (![X1_1405, X2_1406, X3_1407, X4_1408]: (ifeq2(f(X1_1405, X2_1406, X3_1407, X4_1408, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(X1_1405, n1), true)=true))). % 17.82/7.95 tff(c_25908, plain, (![X1_1397, X2_1398, X3_1399, X4_1400]: (ifeq2(f(X1_1397, X2_1398, X3_1399, X4_1400, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(X2_1398, n1), true)=true))). % 17.82/7.95 tff(c_25778, plain, (![X1_1389, X2_1390, X3_1391, X4_1392]: (ifeq2(f(X1_1389, X2_1390, X3_1391, X4_1392, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(X1_1389, n1), true)=true))). % 17.82/7.95 tff(c_25672, plain, (![X1_1381, X2_1382, X3_1383, X4_1384]: (ifeq2(f(X1_1381, X2_1382, X3_1383, X4_1384, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(X2_1382, n0), true)=true))). % 17.82/7.95 tff(c_25553, plain, (![X1_1373, X2_1374, X3_1375, X4_1376]: (ifeq2(f(X1_1373, X2_1374, X3_1375, X4_1376, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(X2_1374, n1), true)=true))). % 17.82/7.95 tff(c_25436, plain, (![X1_1365, X2_1366, X3_1367, X4_1368]: (ifeq2(f(X1_1365, X2_1366, X3_1367, X4_1368, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(X4_1368, n0), true)=true))). % 17.82/7.95 tff(c_25318, plain, (![X1_1357, X2_1358, X3_1359, X4_1360]: (ifeq2(f(X1_1357, X2_1358, X3_1359, X4_1360, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(X4_1360, n0), true)=true))). % 17.82/7.95 tff(c_25107, plain, (![X1_1345, X2_1346, X3_1347, X4_1348]: (ifeq2(f(X1_1345, X2_1346, X3_1347, X4_1348, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(X4_1348, n1), true)=true))). % 17.82/7.95 tff(c_25058, plain, (![X1_1341, X2_1342, X3_1343, X4_1344]: (ifeq2(f(X1_1341, X2_1342, X3_1343, X4_1344, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(X2_1342, n1), true)=true))). % 17.82/7.95 tff(c_24940, plain, (![X1_1333, X2_1334, X3_1335, X4_1336]: (ifeq2(f(X1_1333, X2_1334, X3_1335, X4_1336, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(X1_1333, n0), true)=true))). % 17.82/7.95 tff(c_24834, plain, (![X1_1325, X2_1326, X3_1327, X4_1328]: (ifeq2(f(X1_1325, X2_1326, X3_1327, X4_1328, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(X1_1325, n0), true)=true))). % 17.82/7.95 tff(c_24716, plain, (![X1_1317, X2_1318, X3_1319, X4_1320]: (ifeq2(f(X1_1317, X2_1318, X3_1319, X4_1320, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(X3_1319, n0), true)=true))). % 17.82/7.95 tff(c_24586, plain, (![X1_1309, X2_1310, X3_1311, X4_1312]: (ifeq2(f(X1_1309, X2_1310, X3_1311, X4_1312, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(X1_1309, n1), true)=true))). % 17.82/7.95 tff(c_24456, plain, (![X1_1301, X2_1302, X3_1303, X4_1304]: (ifeq2(f(X1_1301, X2_1302, X3_1303, X4_1304, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(X4_1304, n0), true)=true))). % 17.82/7.95 tff(c_24325, plain, (![X1_1293, X2_1294, X3_1295, X4_1296]: (ifeq2(f(X1_1293, X2_1294, X3_1295, X4_1296, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(X1_1293, n0), true)=true))). % 17.82/7.95 tff(c_24208, plain, (![X1_1285, X2_1286, X3_1287, X4_1288]: (ifeq2(f(X1_1285, X2_1286, X3_1287, X4_1288, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(X3_1287, n1), true)=true))). % 17.82/7.95 tff(c_24090, plain, (![X1_1277, X2_1278, X3_1279, X4_1280]: (ifeq2(f(X1_1277, X2_1278, X3_1279, X4_1280, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(X2_1278, n0), true)=true))). % 17.82/7.95 tff(c_23895, plain, (![X1_1265, X2_1266, X3_1267, X4_1268]: (ifeq2(f(X1_1265, X2_1266, X3_1267, X4_1268, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(X2_1266, n1), true)=true))). % 17.82/7.95 tff(c_23854, plain, (![X1_1261, X2_1262, X3_1263, X4_1264]: (ifeq2(f(X1_1261, X2_1262, X3_1263, X4_1264, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(X2_1262, n0), true)=true))). % 17.82/7.95 tff(c_23736, plain, (![X1_1253, X2_1254, X3_1255, X4_1256]: (ifeq2(f(X1_1253, X2_1254, X3_1255, X4_1256, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(X4_1256, n1), true)=true))). % 17.82/7.95 tff(c_23618, plain, (![X1_1245, X2_1246, X3_1247, X4_1248]: (ifeq2(f(X1_1245, X2_1246, X3_1247, X4_1248, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(X4_1248, n0), true)=true))). % 17.82/7.95 tff(c_23512, plain, (![X1_1237, X2_1238, X3_1239, X4_1240]: (ifeq2(f(X1_1237, X2_1238, X3_1239, X4_1240, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(X2_1238, n0), true)=true))). % 17.82/7.95 tff(c_23406, plain, (![X1_1229, X2_1230, X3_1231, X4_1232]: (ifeq2(f(X1_1229, X2_1230, X3_1231, X4_1232, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(X3_1231, n1), true)=true))). % 17.82/7.95 tff(c_23276, plain, (![X1_1221, X2_1222, X3_1223, X4_1224]: (ifeq2(f(X1_1221, X2_1222, X3_1223, X4_1224, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(X3_1223, n1), true)=true))). % 17.82/7.95 tff(c_23145, plain, (![X1_1213, X2_1214, X3_1215, X4_1216]: (ifeq2(f(X1_1213, X2_1214, X3_1215, X4_1216, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(X1_1213, n1), true)=true))). % 17.82/7.95 tff(c_23028, plain, (![X1_1205, X2_1206, X3_1207, X4_1208]: (ifeq2(f(X1_1205, X2_1206, X3_1207, X4_1208, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(X4_1208, n1), true)=true))). % 17.82/7.95 tff(c_22910, plain, (![X1_1197, X2_1198, X3_1199, X4_1200]: (ifeq2(f(X1_1197, X2_1198, X3_1199, X4_1200, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(X3_1199, n1), true)=true))). % 17.82/7.95 tff(c_22723, plain, (![X1_1185, X2_1186, X3_1187, X4_1188]: (ifeq2(f(X1_1185, X2_1186, X3_1187, X4_1188, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(X3_1187, n0), true)=true))). % 17.82/7.95 tff(c_22686, plain, (![X1_1181, X2_1182, X3_1183, X4_1184]: (ifeq2(f(X1_1181, X2_1182, X3_1183, X4_1184, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(X3_1183, n0), true)=true))). % 17.82/7.95 tff(c_22568, plain, (![X1_1173, X2_1174, X3_1175, X4_1176]: (ifeq2(f(X1_1173, X2_1174, X3_1175, X4_1176, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(X1_1173, n1), true)=true))). % 17.82/7.95 tff(c_22462, plain, (![X1_1165, X2_1166, X3_1167, X4_1168]: (ifeq2(f(X1_1165, X2_1166, X3_1167, X4_1168, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(X4_1168, n1), true)=true))). % 17.82/7.95 tff(c_22356, plain, (![X1_1157, X2_1158, X3_1159, X4_1160]: (ifeq2(f(X1_1157, X2_1158, X3_1159, X4_1160, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(X4_1160, n1), true)=true))). % 17.82/7.95 tff(c_22250, plain, (![X1_1149, X2_1150, X3_1151, X4_1152]: (ifeq2(f(X1_1149, X2_1150, X3_1151, X4_1152, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(X3_1151, n1), true)=true))). % 17.82/7.95 tff(c_22144, plain, (![X1_1141, X2_1142, X3_1143, X4_1144]: (ifeq2(f(X1_1141, X2_1142, X3_1143, X4_1144, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(X2_1142, n1), true)=true))). % 17.82/7.95 tff(c_22025, plain, (![X1_1133, X2_1134, X3_1135, X4_1136]: (ifeq2(f(X1_1133, X2_1134, X3_1135, X4_1136, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(X4_1136, n1), true)=true))). % 17.82/7.95 tff(c_21920, plain, (![X1_1125, X2_1126, X3_1127, X4_1128]: (ifeq2(f(X1_1125, X2_1126, X3_1127, X4_1128, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(X1_1125, n0), true)=true))). % 17.82/7.95 tff(c_21814, plain, (![X1_1117, X2_1118, X3_1119, X4_1120]: (ifeq2(f(X1_1117, X2_1118, X3_1119, X4_1120, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(X4_1120, n0), true)=true))). % 17.82/7.96 tff(c_21639, plain, (![X1_1105, X2_1106, X3_1107, X4_1108]: (ifeq2(f(X1_1105, X2_1106, X3_1107, X4_1108, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(X4_1108, n0), true)=true))). % 17.82/7.96 tff(c_21602, plain, (![X1_1101, X2_1102, X3_1103, X4_1104]: (ifeq2(f(X1_1101, X2_1102, X3_1103, X4_1104, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(X3_1103, n0), true)=true))). % 17.82/7.96 tff(c_21496, plain, (![X1_1093, X2_1094, X3_1095, X4_1096]: (ifeq2(f(X1_1093, X2_1094, X3_1095, X4_1096, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(X1_1093, n0), true)=true))). % 17.82/7.96 tff(c_21390, plain, (![X1_1085, X2_1086, X3_1087, X4_1088]: (ifeq2(f(X1_1085, X2_1086, X3_1087, X4_1088, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(X4_1088, n1), true)=true))). % 17.82/7.96 tff(c_21284, plain, (![X1_1077, X2_1078, X3_1079, X4_1080]: (ifeq2(f(X1_1077, X2_1078, X3_1079, X4_1080, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(X2_1078, n1), true)=true))). % 17.82/7.96 tff(c_21175, plain, (![X1_1069, X2_1070, X3_1071, X4_1072]: (ifeq2(f(X1_1069, X2_1070, X3_1071, X4_1072, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(X3_1071, n0), true)=true))). % 17.82/7.96 tff(c_21068, plain, (![X1_1061, X2_1062, X3_1063, X4_1064]: (ifeq2(f(X1_1061, X2_1062, X3_1063, X4_1064, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(X1_1061, n0), true)=true))). % 17.82/7.96 tff(c_20947, plain, (![X1_1053, X2_1054, X3_1055, X4_1056]: (ifeq2(f(X1_1053, X2_1054, X3_1055, X4_1056, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(X4_1056, n0), true)=true))). % 17.82/7.96 tff(c_20834, plain, (![X1_1045, X2_1046, X3_1047, X4_1048]: (ifeq2(f(X1_1045, X2_1046, X3_1047, X4_1048, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(X3_1047, n1), true)=true))). % 17.82/7.96 tff(c_20721, plain, (![X1_1037, X2_1038, X3_1039, X4_1040]: (ifeq2(f(X1_1037, X2_1038, X3_1039, X4_1040, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(X1_1037, n1), true)=true))). % 17.82/7.96 tff(c_20608, plain, (![X1_1029, X2_1030, X3_1031, X4_1032]: (ifeq2(f(X1_1029, X2_1030, X3_1031, X4_1032, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(X1_1029, n1), true)=true))). % 17.82/7.96 tff(c_20495, plain, (![X1_1021, X2_1022, X3_1023, X4_1024]: (ifeq2(f(X1_1021, X2_1022, X3_1023, X4_1024, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(X2_1022, n1), true)=true))). % 17.82/7.96 tff(c_20382, plain, (![X1_1013, X2_1014, X3_1015, X4_1016]: (ifeq2(f(X1_1013, X2_1014, X3_1015, X4_1016, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(X2_1014, n1), true)=true))). % 17.82/7.96 tff(c_20257, plain, (![X1_1005, X2_1006, X3_1007, X4_1008]: (ifeq2(f(X1_1005, X2_1006, X3_1007, X4_1008, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(X3_1007, n1), true)=true))). % 17.82/7.96 tff(c_20144, plain, (![X1_997, X2_998, X3_999, X4_1000]: (ifeq2(f(X1_997, X2_998, X3_999, X4_1000, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(X1_997, n1), true)=true))). % 17.82/7.96 tff(c_745, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.96 tff(c_619, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.96 tff(c_740, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.96 tff(c_621, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.96 tff(c_617, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.96 tff(c_19657, plain, (![X1_957, X2_958, X3_959, X4_960]: (ifeq2(f(X1_957, X2_958, X3_959, X4_960, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(X2_958, n0), true)=true))). % 17.82/7.96 tff(c_19730, plain, (![Y1_31, Y4_968, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y4_968, Y3_30, Y4_37, sK1_exists_f_Z(n0, n0, n0, n0)), true, true, true)=true))). % 17.82/7.96 tff(c_623, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n0, n0, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.96 tff(c_746, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.96 tff(c_19565, plain, (![Y1_31, Y1_949, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y1_949, Y3_30, Y4_37, sK1_exists_f_Z(n0, n0, n0, n1)), true, true, true)=true))). % 17.82/7.96 tff(c_742, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n0, n0, n1)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.96 tff(c_6875, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.96 tff(c_1320, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.96 tff(c_3205, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.96 tff(c_3206, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.96 tff(c_3120, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.96 tff(c_5517, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.96 tff(c_3118, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.96 tff(c_4492, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.96 tff(c_4494, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.96 tff(c_6780, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.96 tff(c_11434, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.96 tff(c_11433, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.96 tff(c_5518, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.96 tff(c_18496, plain, (![X1_853, X2_854, X3_855, X4_856]: (ifeq2(f(X1_853, X2_854, X3_855, X4_856, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(X3_855, n1), true)=true))). % 17.82/7.96 tff(c_13128, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.96 tff(c_3208, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.96 tff(c_2232, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.96 tff(c_11334, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.96 tff(c_13132, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.97 tff(c_4496, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.97 tff(c_10450, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.97 tff(c_6879, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.97 tff(c_1324, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.97 tff(c_6783, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.97 tff(c_5424, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.97 tff(c_5421, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.97 tff(c_6880, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.97 tff(c_13126, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.97 tff(c_8788, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.97 tff(c_2228, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.97 tff(c_8784, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.97 tff(c_5522, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.97 tff(c_18042, plain, (![Y1_31, Y1_809, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y1_809, Y3_30, Y4_37, sK1_exists_f_Z(n1, n0, n1, n1)), true, true, true)=true))). % 17.82/7.97 tff(c_6876, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n0, n1, n1)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.97 tff(c_8786, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.97 tff(c_6778, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.97 tff(c_11437, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.97 tff(c_2230, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.97 tff(c_1319, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.97 tff(c_17752, plain, (![Y2_782, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y2_782, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n1, n0, n0)), true, true, true)=true))). % 17.82/7.97 tff(c_4490, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n1, n0, n0)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.97 tff(c_17656, plain, (![Y1_31, Y4_776, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y4_776, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n0, n1)), true, true, true)=true))). % 17.82/7.97 tff(c_11438, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n1, n0, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.97 tff(c_3122, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.97 tff(c_10455, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.97 tff(c_17468, plain, (![Y1_31, Y4_760, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y4_760, Y3_30, Y4_37, sK1_exists_f_Z(n1, n0, n1, n0)), true, true, true)=true))). % 17.82/7.97 tff(c_3210, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n0, n1, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.97 tff(c_5422, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.97 tff(c_11328, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.97 tff(c_17306, plain, (![Y1_31, Y3_743, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y3_743, Y3_30, Y4_37, sK1_exists_f_Z(n1, n0, n0, n1)), true, true, true)=true))). % 17.82/7.97 tff(c_1323, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n0, n0, n1)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.97 tff(c_11330, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(n0, Y1_40), true)=true))). % 17.82/7.97 tff(c_17170, plain, (![Y1_31, Y4_732, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y4_732, Y3_30, Y4_37, sK1_exists_f_Z(n0, n0, n1, n1)), true, true, true)=true))). % 17.82/7.97 tff(c_6784, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n0, n0, n1, n1)), true, equalish(n1, Y4_19), true)=true))). % 17.82/7.97 tff(c_17082, plain, (![Y2_722, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y2_722, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n0, n0, n0)), true, true, true)=true))). % 17.82/7.97 tff(c_2227, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n1, n0, n0, n0)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.97 tff(c_16985, plain, (![Y1_31, Y3_715, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y3_715, Y3_30, Y4_37, sK1_exists_f_Z(n0, n1, n0, n1)), true, true, true)=true))). % 17.82/7.97 tff(c_11333, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n1, n0, n1)), true, equalish(n0, Y3_21), true)=true))). % 17.82/7.97 tff(c_16893, plain, (![Y1_31, Y3_707, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y3_707, Y3_30, Y4_37, sK1_exists_f_Z(n0, n1, n1, n1)), true, true, true)=true))). % 17.82/7.97 tff(c_13131, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n0, n1, n1, n1)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.97 tff(c_16800, plain, (![Y1_31, Y3_699, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y3_699, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n1, n0)), true, true, true)=true))). % 17.82/7.97 tff(c_5520, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n1, n1, n0)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.97 tff(c_10454, plain, (![Y1_22, Y2_25, Y3_21, Y4_28]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(n1, Y3_21), true)=true))). % 17.82/7.97 tff(c_16669, plain, (![Y2_686, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y2_686, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n1, n1, n0)), true, true, true)=true))). % 17.82/7.97 tff(c_8782, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n1, n1, n0)), true, equalish(n1, Y2_34), true)=true))). % 17.82/7.97 tff(c_16572, plain, (![Y1_31, Y4_680, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y4_680, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n0, n0)), true, true, true)=true))). % 17.82/7.97 tff(c_5426, plain, (![Y1_13, Y2_16, Y3_12, Y4_19]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, sK1_exists_f_Z(n1, n1, n0, n0)), true, equalish(n0, Y4_19), true)=true))). % 17.82/7.97 tff(c_16480, plain, (![Y1_31, Y1_669, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y1_669, Y3_30, Y4_37, sK1_exists_f_Z(n1, n1, n1, n1)), true, true, true)=true))). % 17.82/7.97 tff(c_10451, plain, (![Y1_40, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n1, n1, n1, n1)), true, equalish(n1, Y1_40), true)=true))). % 17.82/7.97 tff(c_16391, plain, (![Y2_662, Y2_43, Y3_39, Y4_46]: (ifeq2(f(Y2_662, Y2_43, Y3_39, Y4_46, sK1_exists_f_Z(n0, n0, n1, n0)), true, true, true)=true))). % 17.82/7.97 tff(c_3116, plain, (![Y1_31, Y2_34, Y3_30, Y4_37]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, sK1_exists_f_Z(n0, n0, n1, n0)), true, equalish(n0, Y2_34), true)=true))). % 17.82/7.97 tff(c_3397, plain, (![X4_267]: (ifeq2(equalish(X4_267, X4_267), true, f(n1, n1, n0, X4_267, sK1_exists_f_Z(n1, n1, n0, X4_267)), true)=true))). % 17.82/7.97 tff(c_5307, plain, (![X3_340]: (ifeq2(equalish(X3_340, X3_340), true, f(n1, n0, X3_340, n1, sK1_exists_f_Z(n1, n0, X3_340, n1)), true)=true))). % 17.82/7.97 tff(c_12913, plain, (![X3_591]: (ifeq2(equalish(X3_591, X3_591), true, f(n1, n1, X3_591, n1, sK1_exists_f_Z(n1, n1, X3_591, n1)), true)=true))). % 17.82/7.97 tff(c_8391, plain, (![X4_449]: (ifeq2(equalish(X4_449, X4_449), true, f(n0, n0, n1, X4_449, sK1_exists_f_Z(n0, n0, n1, X4_449)), true)=true))). % 17.82/7.97 tff(c_3011, plain, (![X3_255]: (ifeq2(equalish(X3_255, X3_255), true, f(n1, n0, X3_255, n0, sK1_exists_f_Z(n1, n0, X3_255, n0)), true)=true))). % 17.82/7.97 tff(c_6208, plain, (![X4_373]: (ifeq2(equalish(X4_373, X4_373), true, f(n1, n0, n1, X4_373, sK1_exists_f_Z(n1, n0, n1, X4_373)), true)=true))). % 17.82/7.97 tff(c_11122, plain, (![X3_532]: (ifeq2(equalish(X3_532, X3_532), true, f(n0, n1, X3_532, n1, sK1_exists_f_Z(n0, n1, X3_532, n1)), true)=true))). % 17.82/7.97 tff(c_8546, plain, (![X4_452]: (ifeq2(equalish(X4_452, X4_452), true, f(n0, n1, n0, X4_452, sK1_exists_f_Z(n0, n1, n0, X4_452)), true)=true))). % 17.82/7.97 tff(c_3398, plain, (![X4_267]: (ifeq2(equalish(X4_267, X4_267), true, f(n1, n1, n1, X4_267, sK1_exists_f_Z(n1, n1, n1, X4_267)), true)=true))). % 17.82/7.97 tff(c_3010, plain, (![X3_255]: (ifeq2(equalish(X3_255, X3_255), true, f(n0, n0, X3_255, n0, sK1_exists_f_Z(n0, n0, X3_255, n0)), true)=true))). % 17.82/7.97 tff(c_8547, plain, (![X4_452]: (ifeq2(equalish(X4_452, X4_452), true, f(n0, n1, n1, X4_452, sK1_exists_f_Z(n0, n1, n1, X4_452)), true)=true))). % 17.82/7.97 tff(c_10257, plain, (![X2_501]: (ifeq2(equalish(X2_501, X2_501), true, f(n1, X2_501, n0, n1, sK1_exists_f_Z(n1, X2_501, n0, n1)), true)=true))). % 17.82/7.97 tff(c_508, plain, (![X4_152]: (ifeq2(equalish(X4_152, X4_152), true, f(n1, n0, n0, X4_152, sK1_exists_f_Z(n1, n0, n0, X4_152)), true)=true))). % 17.82/7.97 tff(c_14709, plain, (![X3_643]: (ifeq2(equalish(X3_643, X3_643), true, f(n0, n1, X3_643, n0, sK1_exists_f_Z(n0, n1, X3_643, n0)), true)=true))). % 17.82/7.97 tff(c_2866, plain, (![X3_252, X2_253, X1_254]: (ifeq2(equalish(X3_252, X3_252), true, ifeq2(equalish(X2_253, X2_253), true, ifeq2(equalish(X1_254, X1_254), true, f(X1_254, X2_253, X3_252, n0, sK1_exists_f_Z(X1_254, X2_253, X3_252, n0)), true), true), true)=true))). % 17.82/7.97 tff(c_2468, plain, (![X3_236, X2_237, X1_238]: (ifeq2(equalish(X3_236, X3_236), true, ifeq2(equalish(X2_237, X2_237), true, ifeq2(equalish(X1_238, X1_238), true, f(X1_238, X2_237, X3_236, n1, sK1_exists_f_Z(X1_238, X2_237, X3_236, n1)), true), true), true)=true))). % 17.82/7.97 tff(c_14391, plain, (![X2_638]: (ifeq2(equalish(X2_638, X2_638), true, f(n0, X2_638, n1, n1, sK1_exists_f_Z(n0, X2_638, n1, n1)), true)=true))). % 17.82/7.97 tff(c_13994, plain, (![X1_627]: (ifeq2(equalish(X1_627, X1_627), true, f(X1_627, n1, n0, n0, sK1_exists_f_Z(X1_627, n1, n0, n0)), true)=true))). % 17.82/7.97 tff(c_13764, plain, (![X1_622]: (ifeq2(equalish(X1_622, X1_622), true, f(X1_622, n1, n1, n0, sK1_exists_f_Z(X1_622, n1, n1, n0)), true)=true))). % 17.82/7.97 tff(c_13013, plain, (![X1_596]: (ifeq2(equalish(X1_596, X1_596), true, f(X1_596, n1, n1, n1, sK1_exists_f_Z(X1_596, n1, n1, n1)), true)=true))). % 17.82/7.98 tff(c_13024, plain, (f(n0, n1, n1, n1, sK1_exists_f_Z(n0, n1, n1, n1))=true)). % 17.82/7.98 tff(c_2500, plain, (![X3_236, X2_237]: (ifeq2(equalish(X3_236, X3_236), true, ifeq2(equalish(X2_237, X2_237), true, f(n1, X2_237, X3_236, n1, sK1_exists_f_Z(n1, X2_237, X3_236, n1)), true), true)=true))). % 17.82/7.98 tff(c_12302, plain, (![X2_578]: (ifeq2(equalish(X2_578, X2_578), true, f(n0, X2_578, n0, n1, sK1_exists_f_Z(n0, X2_578, n0, n1)), true)=true))). % 17.82/7.98 tff(c_2931, plain, (![X3_252, X2_253]: (ifeq2(equalish(X3_252, X3_252), true, ifeq2(equalish(X2_253, X2_253), true, f(n1, X2_253, X3_252, n0, sK1_exists_f_Z(n1, X2_253, X3_252, n0)), true), true)=true))). % 17.82/7.98 tff(c_11212, plain, (![X1_537]: (ifeq2(equalish(X1_537, X1_537), true, f(X1_537, n1, n0, n1, sK1_exists_f_Z(X1_537, n1, n0, n1)), true)=true))). % 17.82/7.98 tff(c_11227, plain, (f(n1, n1, n0, n1, sK1_exists_f_Z(n1, n1, n0, n1))=true)). % 17.82/7.98 tff(c_11226, plain, (f(n0, n1, n0, n1, sK1_exists_f_Z(n0, n1, n0, n1))=true)). % 17.82/7.98 tff(c_2499, plain, (![X3_236, X1_238]: (ifeq2(equalish(X3_236, X3_236), true, ifeq2(equalish(X1_238, X1_238), true, f(X1_238, n1, X3_236, n1, sK1_exists_f_Z(X1_238, n1, X3_236, n1)), true), true)=true))). % 17.82/7.98 tff(c_10337, plain, (![X2_506]: (ifeq2(equalish(X2_506, X2_506), true, f(n1, X2_506, n1, n1, sK1_exists_f_Z(n1, X2_506, n1, n1)), true)=true))). % 17.82/7.98 tff(c_10356, plain, (f(n1, n1, n1, n1, sK1_exists_f_Z(n1, n1, n1, n1))=true)). % 17.82/7.98 tff(c_2495, plain, (![X2_237, X1_238]: (ifeq2(equalish(X2_237, X2_237), true, ifeq2(equalish(X1_238, X1_238), true, f(X1_238, X2_237, n0, n1, sK1_exists_f_Z(X1_238, X2_237, n0, n1)), true), true)=true))). % 17.82/7.98 tff(c_9969, plain, (![X2_497]: (ifeq2(equalish(X2_497, X2_497), true, f(n1, X2_497, n1, n0, sK1_exists_f_Z(n1, X2_497, n1, n0)), true)=true))). % 17.82/7.98 tff(c_2498, plain, (![X2_237, X1_238]: (ifeq2(equalish(X2_237, X2_237), true, ifeq2(equalish(X1_238, X1_238), true, f(X1_238, X2_237, n1, n1, sK1_exists_f_Z(X1_238, X2_237, n1, n1)), true), true)=true))). % 17.82/7.98 tff(c_1572, plain, (![X4_198, X1_200]: (ifeq2(equalish(X4_198, X4_198), true, ifeq2(equalish(X1_200, X1_200), true, f(X1_200, n1, n1, X4_198, sK1_exists_f_Z(X1_200, n1, n1, X4_198)), true), true)=true))). % 17.82/7.98 tff(c_9585, plain, (![X3_487]: (ifeq2(equalish(X3_487, X3_487), true, f(n0, n0, X3_487, n1, sK1_exists_f_Z(n0, n0, X3_487, n1)), true)=true))). % 17.82/7.98 tff(c_2497, plain, (![X3_236, X2_237]: (ifeq2(equalish(X3_236, X3_236), true, ifeq2(equalish(X2_237, X2_237), true, f(n0, X2_237, X3_236, n1, sK1_exists_f_Z(n0, X2_237, X3_236, n1)), true), true)=true))). % 17.82/7.98 tff(c_8662, plain, (![X2_456]: (ifeq2(equalish(X2_456, X2_456), true, f(n0, X2_456, n1, n0, sK1_exists_f_Z(n0, X2_456, n1, n0)), true)=true))). % 17.82/7.98 tff(c_8685, plain, (f(n0, n1, n1, n0, sK1_exists_f_Z(n0, n1, n1, n0))=true)). % 17.82/7.98 tff(c_2929, plain, (![X2_253, X1_254]: (ifeq2(equalish(X2_253, X2_253), true, ifeq2(equalish(X1_254, X1_254), true, f(X1_254, X2_253, n1, n0, sK1_exists_f_Z(X1_254, X2_253, n1, n0)), true), true)=true))). % 17.82/7.98 tff(c_1993, plain, (![X4_214, X3_215]: (ifeq2(equalish(X4_214, X4_214), true, ifeq2(equalish(X3_215, X3_215), true, f(n0, n1, X3_215, X4_214, sK1_exists_f_Z(n0, n1, X3_215, X4_214)), true), true)=true))). % 17.82/7.98 tff(c_8196, plain, (![X2_445]: (ifeq2(equalish(X2_445, X2_445), true, f(n1, X2_445, n0, n0, sK1_exists_f_Z(n1, X2_445, n0, n0)), true)=true))). % 17.82/7.98 tff(c_656, plain, (![X4_155, X2_156]: (ifeq2(equalish(X4_155, X4_155), true, ifeq2(equalish(X2_156, X2_156), true, f(n0, X2_156, n1, X4_155, sK1_exists_f_Z(n0, X2_156, n1, X4_155)), true), true)=true))). % 17.82/7.98 tff(c_2928, plain, (![X3_252, X2_253]: (ifeq2(equalish(X3_252, X3_252), true, ifeq2(equalish(X2_253, X2_253), true, f(n0, X2_253, X3_252, n0, sK1_exists_f_Z(n0, X2_253, X3_252, n0)), true), true)=true))). % 17.82/7.98 tff(c_1032, plain, (![X4_173, X3_174]: (ifeq2(equalish(X4_173, X4_173), true, ifeq2(equalish(X3_174, X3_174), true, f(n0, n0, X3_174, X4_173, sK1_exists_f_Z(n0, n0, X3_174, X4_173)), true), true)=true))). % 17.82/7.98 tff(c_6687, plain, (![X1_392]: (ifeq2(equalish(X1_392, X1_392), true, f(X1_392, n0, n1, n1, sK1_exists_f_Z(X1_392, n0, n1, n1)), true)=true))). % 17.82/7.98 tff(c_655, plain, (![X4_155, X1_157]: (ifeq2(equalish(X4_155, X4_155), true, ifeq2(equalish(X1_157, X1_157), true, f(X1_157, n0, n1, X4_155, sK1_exists_f_Z(X1_157, n0, n1, X4_155)), true), true)=true))). % 17.82/7.98 tff(c_6697, plain, (f(n1, n0, n1, n1, sK1_exists_f_Z(n1, n0, n1, n1))=true)). % 17.82/7.98 tff(c_6696, plain, (f(n0, n0, n1, n1, sK1_exists_f_Z(n0, n0, n1, n1))=true)). % 17.82/7.98 tff(c_1570, plain, (![X4_198, X1_200]: (ifeq2(equalish(X4_198, X4_198), true, ifeq2(equalish(X1_200, X1_200), true, f(X1_200, n1, n0, X4_198, sK1_exists_f_Z(X1_200, n1, n0, X4_198)), true), true)=true))). % 17.82/7.98 tff(c_1034, plain, (![X4_173, X3_174]: (ifeq2(equalish(X4_173, X4_173), true, ifeq2(equalish(X3_174, X3_174), true, f(n1, n0, X3_174, X4_173, sK1_exists_f_Z(n1, n0, X3_174, X4_173)), true), true)=true))). % 17.82/7.98 tff(c_5321, plain, (![X3_342]: (ifeq2(equalish(X3_342, X3_342), true, f(n1, n1, X3_342, n0, sK1_exists_f_Z(n1, n1, X3_342, n0)), true)=true))). % 17.82/7.98 tff(c_477, plain, (![X4_149, X2_150]: (ifeq2(equalish(X4_149, X4_149), true, ifeq2(equalish(X2_150, X2_150), true, f(n1, X2_150, n0, X4_149, sK1_exists_f_Z(n1, X2_150, n0, X4_149)), true), true)=true))). % 17.82/7.98 tff(c_5331, plain, (f(n1, n1, n1, n0, sK1_exists_f_Z(n1, n1, n1, n0))=true)). % 17.82/7.98 tff(c_5330, plain, (f(n1, n1, n0, n0, sK1_exists_f_Z(n1, n1, n0, n0))=true)). % 17.82/7.98 tff(c_2496, plain, (![X3_236, X1_238]: (ifeq2(equalish(X3_236, X3_236), true, ifeq2(equalish(X1_238, X1_238), true, f(X1_238, n0, X3_236, n1, sK1_exists_f_Z(X1_238, n0, X3_236, n1)), true), true)=true))). % 17.82/7.98 tff(c_2926, plain, (![X2_253, X1_254]: (ifeq2(equalish(X2_253, X2_253), true, ifeq2(equalish(X1_254, X1_254), true, f(X1_254, X2_253, n0, n0, sK1_exists_f_Z(X1_254, X2_253, n0, n0)), true), true)=true))). % 17.82/7.98 tff(c_4392, plain, (![X2_310]: (ifeq2(equalish(X2_310, X2_310), true, f(n0, X2_310, n0, n0, sK1_exists_f_Z(n0, X2_310, n0, n0)), true)=true))). % 17.82/7.98 tff(c_2055, plain, (![X4_217, X2_219]: (ifeq2(equalish(X4_217, X4_217), true, ifeq2(equalish(X2_219, X2_219), true, f(n1, X2_219, n1, X4_217, sK1_exists_f_Z(n1, X2_219, n1, X4_217)), true), true)=true))). % 17.82/7.98 tff(c_4405, plain, (f(n0, n1, n0, n0, sK1_exists_f_Z(n0, n1, n0, n0))=true)). % 17.82/7.98 tff(c_2930, plain, (![X3_252, X1_254]: (ifeq2(equalish(X3_252, X3_252), true, ifeq2(equalish(X1_254, X1_254), true, f(X1_254, n1, X3_252, n0, sK1_exists_f_Z(X1_254, n1, X3_252, n0)), true), true)=true))). % 17.82/7.98 tff(c_1990, plain, (![X4_214, X2_216]: (ifeq2(equalish(X4_214, X4_214), true, ifeq2(equalish(X2_216, X2_216), true, f(n0, X2_216, n0, X4_214, sK1_exists_f_Z(n0, X2_216, n0, X4_214)), true), true)=true))). % 17.82/7.98 tff(c_3025, plain, (![X1_257]: (ifeq2(equalish(X1_257, X1_257), true, f(X1_257, n0, n1, n0, sK1_exists_f_Z(X1_257, n0, n1, n0)), true)=true))). % 17.82/7.98 tff(c_2056, plain, (![X4_217, X3_218]: (ifeq2(equalish(X4_217, X4_217), true, ifeq2(equalish(X3_218, X3_218), true, f(n1, n1, X3_218, X4_217, sK1_exists_f_Z(n1, n1, X3_218, X4_217)), true), true)=true))). % 17.82/7.98 tff(c_3035, plain, (f(n1, n0, n1, n0, sK1_exists_f_Z(n1, n0, n1, n0))=true)). % 17.82/7.98 tff(c_3034, plain, (f(n0, n0, n1, n0, sK1_exists_f_Z(n0, n0, n1, n0))=true)). % 17.82/7.98 tff(c_2927, plain, (![X3_252, X1_254]: (ifeq2(equalish(X3_252, X3_252), true, ifeq2(equalish(X1_254, X1_254), true, f(X1_254, n0, X3_252, n0, sK1_exists_f_Z(X1_254, n0, X3_252, n0)), true), true)=true))). % 17.82/7.98 tff(c_2126, plain, (![X1_223]: (ifeq2(equalish(X1_223, X1_223), true, f(X1_223, n0, n0, n0, sK1_exists_f_Z(X1_223, n0, n0, n0)), true)=true))). % 17.82/7.98 tff(c_2149, plain, (f(n1, n0, n0, n0, sK1_exists_f_Z(n1, n0, n0, n0))=true)). % 17.82/7.98 tff(c_443, plain, (![X4_145, X3_146, X2_147]: (ifeq2(equalish(X4_145, X4_145), true, ifeq2(equalish(X3_146, X3_146), true, ifeq2(equalish(X2_147, X2_147), true, f(n1, X2_147, X3_146, X4_145, sK1_exists_f_Z(n1, X2_147, X3_146, X4_145)), true), true), true)=true))). % 17.82/7.98 tff(c_440, plain, (![X4_145, X3_146, X2_147]: (ifeq2(equalish(X4_145, X4_145), true, ifeq2(equalish(X3_146, X3_146), true, ifeq2(equalish(X2_147, X2_147), true, f(n0, X2_147, X3_146, X4_145, sK1_exists_f_Z(n0, X2_147, X3_146, X4_145)), true), true), true)=true))). % 17.82/7.98 tff(c_1226, plain, (![X1_185]: (ifeq2(equalish(X1_185, X1_185), true, f(X1_185, n0, n0, n1, sK1_exists_f_Z(X1_185, n0, n0, n1)), true)=true))). % 17.82/7.98 tff(c_442, plain, (![X4_145, X3_146, X1_148]: (ifeq2(equalish(X4_145, X4_145), true, ifeq2(equalish(X3_146, X3_146), true, ifeq2(equalish(X1_148, X1_148), true, f(X1_148, n1, X3_146, X4_145, sK1_exists_f_Z(X1_148, n1, X3_146, X4_145)), true), true), true)=true))). % 17.82/7.98 tff(c_1245, plain, (f(n1, n0, n0, n1, sK1_exists_f_Z(n1, n0, n0, n1))=true)). % 17.82/7.98 tff(c_439, plain, (![X4_145, X3_146, X1_148]: (ifeq2(equalish(X4_145, X4_145), true, ifeq2(equalish(X3_146, X3_146), true, ifeq2(equalish(X1_148, X1_148), true, f(X1_148, n0, X3_146, X4_145, sK1_exists_f_Z(X1_148, n0, X3_146, X4_145)), true), true), true)=true))). % 17.82/7.98 tff(c_663, plain, (f(n0, n0, n0, n1, sK1_exists_f_Z(n0, n0, n0, n1))=true)). % 17.82/7.98 tff(c_441, plain, (![X4_145, X2_147, X1_148]: (ifeq2(equalish(X4_145, X4_145), true, ifeq2(equalish(X2_147, X2_147), true, ifeq2(equalish(X1_148, X1_148), true, f(X1_148, X2_147, n1, X4_145, sK1_exists_f_Z(X1_148, X2_147, n1, X4_145)), true), true), true)=true))). % 17.82/7.98 tff(c_540, plain, (f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))=true)). % 17.82/7.98 tff(c_507, plain, (![X4_152]: (ifeq2(equalish(X4_152, X4_152), true, f(n0, n0, n0, X4_152, sK1_exists_f_Z(n0, n0, n0, X4_152)), true)=true))). % 17.82/7.98 tff(c_474, plain, (![X4_149, X1_151]: (ifeq2(equalish(X4_149, X4_149), true, ifeq2(equalish(X1_151, X1_151), true, f(X1_151, n0, n0, X4_149, sK1_exists_f_Z(X1_151, n0, n0, X4_149)), true), true)=true))). % 17.82/7.98 tff(c_438, plain, (![X4_145, X2_147, X1_148]: (ifeq2(equalish(X4_145, X4_145), true, ifeq2(equalish(X2_147, X2_147), true, ifeq2(equalish(X1_148, X1_148), true, f(X1_148, X2_147, n0, X4_145, sK1_exists_f_Z(X1_148, X2_147, n0, X4_145)), true), true), true)=true))). % 17.82/7.98 tff(c_10, plain, (![X4_7, X3_8, X2_9, X1_10]: (ifeq2(equalish(X4_7, X4_7), true, ifeq2(equalish(X3_8, X3_8), true, ifeq2(equalish(X2_9, X2_9), true, ifeq2(equalish(X1_10, X1_10), true, f(X1_10, X2_9, X3_8, X4_7, sK1_exists_f_Z(X1_10, X2_9, X3_8, X4_7)), true), true), true), true)=true))). % 17.82/7.98 tff(c_246, plain, (![X4_122, X3_121, X1_117, Y3_115, Y1_118, Z_116, Y4_120]: (ifeq2(f(Y1_118, n0, Y3_115, Y4_120, Z_116), true, ifeq2(f(X1_117, n0, X3_121, X4_122, Z_116), true, true, true), true)=true))). % 17.82/7.98 tff(c_249, plain, (![X4_122, X3_121, X1_117, Y3_115, Y1_118, Z_116, Y4_120]: (ifeq2(f(Y1_118, n1, Y3_115, Y4_120, Z_116), true, ifeq2(f(X1_117, n1, X3_121, X4_122, Z_116), true, true, true), true)=true))). % 17.82/7.98 tff(c_175, plain, (![X4_100, Y3_99, Y2_103, Y4_107, Z_102, X3_104, X2_106]: (ifeq2(f(n1, Y2_103, Y3_99, Y4_107, Z_102), true, ifeq2(f(n1, X2_106, X3_104, X4_100, Z_102), true, true, true), true)=true))). % 17.82/7.98 tff(c_16, plain, (![X2_35, X3_29, Z_32, Y3_30, X4_36, Y1_31, Y4_37, Y2_34, X1_33]: (ifeq2(f(Y1_31, Y2_34, Y3_30, Y4_37, Z_32), true, ifeq2(f(X1_33, X2_35, X3_29, X4_36, Z_32), true, equalish(X2_35, Y2_34), true), true)=true))). % 17.82/7.98 tff(c_172, plain, (![X4_100, Y3_99, Y2_103, Y4_107, Z_102, X3_104, X2_106]: (ifeq2(f(n0, Y2_103, Y3_99, Y4_107, Z_102), true, ifeq2(f(n0, X2_106, X3_104, X4_100, Z_102), true, true, true), true)=true))). % 17.82/7.98 tff(c_18, plain, (![Y4_46, X2_44, X1_42, Y2_43, Y3_39, X3_38, X4_45, Y1_40, Z_41]: (ifeq2(f(Y1_40, Y2_43, Y3_39, Y4_46, Z_41), true, ifeq2(f(X1_42, X2_44, X3_38, X4_45, Z_41), true, equalish(X1_42, Y1_40), true), true)=true))). % 17.82/7.98 tff(c_95, plain, (![Y1_71, Z_76, X4_69, Y2_72, X2_75, X1_77, Y4_74]: (ifeq2(f(Y1_71, Y2_72, n1, Y4_74, Z_76), true, ifeq2(f(X1_77, X2_75, n1, X4_69, Z_76), true, true, true), true)=true))). % 17.82/7.98 tff(c_92, plain, (![Y1_71, Z_76, X4_69, Y2_72, X2_75, X1_77, Y4_74]: (ifeq2(f(Y1_71, Y2_72, n0, Y4_74, Z_76), true, ifeq2(f(X1_77, X2_75, n0, X4_69, Z_76), true, true, true), true)=true))). % 17.82/7.98 tff(c_69, plain, (![Z_58, X1_53, X3_54, Y2_61, X2_60, Y3_59, Y1_55]: (ifeq2(f(Y1_55, Y2_61, Y3_59, n1, Z_58), true, ifeq2(f(X1_53, X2_60, X3_54, n1, Z_58), true, true, true), true)=true))). % 17.82/7.98 tff(c_14, plain, (![X4_27, Y2_25, X1_24, Y4_28, Y1_22, Z_23, Y3_21, X3_20, X2_26]: (ifeq2(f(Y1_22, Y2_25, Y3_21, Y4_28, Z_23), true, ifeq2(f(X1_24, X2_26, X3_20, X4_27, Z_23), true, equalish(X3_20, Y3_21), true), true)=true))). % 17.82/7.98 tff(c_66, plain, (![Z_58, X1_53, X3_54, Y2_61, X2_60, Y3_59, Y1_55]: (ifeq2(f(Y1_55, Y2_61, Y3_59, n0, Z_58), true, ifeq2(f(X1_53, X2_60, X3_54, n0, Z_58), true, true, true), true)=true))). % 17.82/7.98 tff(c_12, plain, (![Y3_12, Y4_19, X3_11, Y2_16, X2_17, Z_14, X1_15, Y1_13, X4_18]: (ifeq2(f(Y1_13, Y2_16, Y3_12, Y4_19, Z_14), true, ifeq2(f(X1_15, X2_17, X3_11, X4_18, Z_14), true, equalish(X4_18, Y4_19), true), true)=true))). % 17.82/7.98 tff(c_20, plain, (ifeq(equalish(n0, n1), true, a, b)=b)). % 17.82/7.98 tff(c_22, plain, (ifeq(equalish(n1, n0), true, a, b)=b)). % 17.82/7.98 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq2(A_1, A_1, B_2, C_3)=B_2))). % 17.82/7.98 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq(A_4, A_4, B_5, C_6)=B_5))). % 17.82/7.98 tff(c_6, plain, (equalish(n0, n0)=true)). % 17.82/7.98 tff(c_8, plain, (equalish(n1, n1)=true)). % 17.82/7.98 tff(c_24, plain, (b!=a)). % 17.82/7.98 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.82/7.98 %------------------------------------------------------------------------------