%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : KRS009-1 : TPTP v9.0.0. Released v2.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 : n032.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:07:09 PM UTC 2025 % Result : Satisfiable 7.19s 2.78s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.09 % Problem : KRS009-1 : TPTP v9.0.0. Released v2.0.0. % 0.06/0.10 % 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.09/0.28 % Computer : n032.cluster.edu % 0.09/0.28 % Model : x86_64 x86_64 % 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.28 % Memory : 8042.1875MB % 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.28 % CPULimit : 300 % 0.09/0.28 % WCLimit : 300 % 0.09/0.28 % DateTime : Tue Apr 8 02:53:15 EDT 2025 % 0.09/0.28 % CPUTime : % 7.19/2.77 % 7.19/2.78 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.19/2.78 % 7.19/2.78 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.19/2.78 %$ t > s > r > p > equalish > t3least > s1most > r1most > p2least > p1most > e > d > c > a > #nlpp > u9r2 > u9r1 > u8r3 > u8r2 > u8r1 > u7r1 > u3r2 > u3r1 > u1r2 > u1r1 > u10r2 > u10r1 > exist % 7.19/2.78 % 7.19/2.78 %Foreground sorts: % 7.19/2.78 % 7.19/2.78 % 7.19/2.78 %Background operators: % 7.19/2.78 % 7.19/2.78 % 7.19/2.78 %Foreground operators: % 7.19/2.78 tff(s, type, s: ($i * $i) > $o). % 7.19/2.78 tff(u10r1, type, u10r1: $i > $i). % 7.19/2.78 tff(u9r1, type, u9r1: $i > $i). % 7.19/2.78 tff(s1most, type, s1most: $i > $o). % 7.19/2.78 tff(d, type, d: $i > $o). % 7.19/2.78 tff(p1most, type, p1most: $i > $o). % 7.19/2.78 tff(u3r1, type, u3r1: $i > $i). % 7.19/2.78 tff(u1r1, type, u1r1: $i > $i). % 7.19/2.78 tff(t3least, type, t3least: $i > $o). % 7.19/2.78 tff(r1most, type, r1most: $i > $o). % 7.19/2.78 tff(u3r2, type, u3r2: $i > $i). % 7.19/2.78 tff(u8r3, type, u8r3: $i > $i). % 7.19/2.78 tff(u9r2, type, u9r2: $i > $i). % 7.19/2.78 tff(u8r1, type, u8r1: $i > $i). % 7.19/2.78 tff(u8r2, type, u8r2: $i > $i). % 7.19/2.78 tff(c, type, c: $i > $o). % 7.19/2.78 tff(e, type, e: $i > $o). % 7.19/2.78 tff(u7r1, type, u7r1: $i > $i). % 7.19/2.78 tff(p, type, p: ($i * $i) > $o). % 7.19/2.78 tff(a, type, a: $i > $o). % 7.19/2.78 tff(t, type, t: ($i * $i) > $o). % 7.19/2.78 tff(exist, type, exist: $i). % 7.19/2.78 tff(equalish, type, equalish: ($i * $i) > $o). % 7.19/2.78 tff(u1r2, type, u1r2: $i > $i). % 7.19/2.78 tff(p2least, type, p2least: $i > $o). % 7.19/2.78 tff(r, type, r: ($i * $i) > $o). % 7.19/2.78 tff(u10r2, type, u10r2: $i > $i). % 7.19/2.78 % 7.19/2.78 %Saturated clause set: % 7.19/2.79 tff(c_1906, plain, (![X1_54, X1_312]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r1(X1_312)) | equalish(u10r2(X1_54), u10r1(X1_312)) | t3least(X1_312) | ~r(X1_312, u10r1(X1_54)) | ~r(X1_312, u10r2(X1_54)) | s1most(X1_312)))). % 7.19/2.79 tff(c_1203, plain, (![X1_35, X1_263]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r2(X1_263)) | equalish(u8r2(X1_35), u9r2(X1_263)) | t3least(X1_263) | ~s(X1_263, u8r1(X1_35)) | ~r(X1_263, u8r2(X1_35)) | r1most(X1_263)))). % 7.19/2.79 tff(c_702, plain, (![X1_54, X1_210]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r1(X1_210)) | equalish(u10r2(X1_54), u9r1(X1_210)) | t3least(X1_210) | ~s(X1_210, u10r1(X1_54)) | ~s(X1_210, u10r2(X1_54)) | r1most(X1_210)))). % 7.19/2.79 tff(c_1996, plain, (![X1_14, X1_317]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r2(X1_317)) | equalish(u3r2(X1_14), u10r2(X1_317)) | t3least(X1_317) | ~r(X1_317, u3r1(X1_14)) | ~s(X1_317, u3r2(X1_14)) | s1most(X1_317)))). % 7.19/2.79 tff(c_792, plain, (![X1_48, X1_216]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r2(X1_216)) | equalish(u9r2(X1_48), u10r2(X1_216)) | t3least(X1_216) | ~s(X1_216, u9r1(X1_48)) | ~r(X1_216, u9r2(X1_48)) | s1most(X1_216)))). % 7.19/2.79 tff(c_791, plain, (![X1_54, X1_216]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r2(X1_216)) | equalish(u10r2(X1_54), u10r2(X1_216)) | t3least(X1_216) | ~s(X1_216, u10r1(X1_54)) | ~r(X1_216, u10r2(X1_54)) | s1most(X1_216)))). % 7.19/2.79 tff(c_1463, plain, (![X1_35, X1_282]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r2(X1_282)) | equalish(u8r2(X1_35), u9r2(X1_282)) | t3least(X1_282) | ~r(X1_282, u8r1(X1_35)) | ~r(X1_282, u8r2(X1_35)) | r1most(X1_282)))). % 7.19/2.79 tff(c_1909, plain, (![X1_36, X1_312]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r1(X1_312)) | equalish(u8r3(X1_36), u10r1(X1_312)) | t3least(X1_312) | ~r(X1_312, u8r1(X1_36)) | ~r(X1_312, u8r3(X1_36)) | s1most(X1_312)))). % 7.19/2.79 tff(c_1554, plain, (![X1_36, X1_288]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r2(X1_288)) | equalish(u8r3(X1_36), u9r2(X1_288)) | t3least(X1_288) | ~r(X1_288, u8r1(X1_36)) | ~s(X1_288, u8r3(X1_36)) | r1most(X1_288)))). % 7.19/2.79 tff(c_981, plain, (![X1_54, X1_234]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r1(X1_234)) | equalish(u10r2(X1_54), u10r1(X1_234)) | t3least(X1_234) | ~s(X1_234, u10r1(X1_54)) | ~s(X1_234, u10r2(X1_54)) | s1most(X1_234)))). % 7.19/2.79 tff(c_605, plain, (![X1_54, X1_204]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r2(X1_204)) | equalish(u10r2(X1_54), u10r2(X1_204)) | t3least(X1_204) | ~s(X1_204, u10r1(X1_54)) | ~s(X1_204, u10r2(X1_54)) | s1most(X1_204)))). % 7.19/2.79 tff(c_1811, plain, (![X1_14, X1_306]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r2(X1_306)) | equalish(u3r2(X1_14), u10r2(X1_306)) | t3least(X1_306) | ~r(X1_306, u3r1(X1_14)) | ~r(X1_306, u3r2(X1_14)) | s1most(X1_306)))). % 7.19/2.79 tff(c_793, plain, (![X1_14, X1_216]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r2(X1_216)) | equalish(u3r2(X1_14), u10r2(X1_216)) | t3least(X1_216) | ~s(X1_216, u3r1(X1_14)) | ~r(X1_216, u3r2(X1_14)) | s1most(X1_216)))). % 7.19/2.79 tff(c_1548, plain, (![X1_3, X1_288]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r2(X1_288)) | equalish(u1r2(X1_3), u9r2(X1_288)) | t3least(X1_288) | ~r(X1_288, u1r1(X1_3)) | ~s(X1_288, u1r2(X1_3)) | r1most(X1_288)))). % 7.19/2.79 tff(c_1634, plain, (![X1_14, X1_291]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r1(X1_291)) | equalish(u3r2(X1_14), u9r1(X1_291)) | t3least(X1_291) | ~s(X1_291, u3r1(X1_14)) | ~r(X1_291, u3r2(X1_14)) | r1most(X1_291)))). % 7.19/2.79 tff(c_1201, plain, (![X1_3, X1_263]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r2(X1_263)) | equalish(u1r2(X1_3), u9r2(X1_263)) | t3least(X1_263) | ~s(X1_263, u1r1(X1_3)) | ~r(X1_263, u1r2(X1_3)) | r1most(X1_263)))). % 7.19/2.79 tff(c_700, plain, (![X1_37, X1_210]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r1(X1_210)) | equalish(u8r3(X1_37), u9r1(X1_210)) | t3least(X1_210) | ~s(X1_210, u8r2(X1_37)) | ~s(X1_210, u8r3(X1_37)) | r1most(X1_210)))). % 7.19/2.79 tff(c_876, plain, (![X1_14, X1_223]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r1(X1_223)) | equalish(u3r2(X1_14), u9r1(X1_223)) | t3least(X1_223) | ~r(X1_223, u3r1(X1_14)) | ~s(X1_223, u3r2(X1_14)) | r1most(X1_223)))). % 7.19/2.79 tff(c_1633, plain, (![X1_48, X1_291]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r1(X1_291)) | equalish(u9r2(X1_48), u9r1(X1_291)) | t3least(X1_291) | ~s(X1_291, u9r1(X1_48)) | ~r(X1_291, u9r2(X1_48)) | r1most(X1_291)))). % 7.19/2.79 tff(c_1726, plain, (![X1_48, X1_298]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r1(X1_298)) | equalish(u9r2(X1_48), u10r1(X1_298)) | t3least(X1_298) | ~r(X1_298, u9r1(X1_48)) | ~s(X1_298, u9r2(X1_48)) | s1most(X1_298)))). % 7.19/2.79 tff(c_608, plain, (![X1_36, X1_204]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r2(X1_204)) | equalish(u8r3(X1_36), u10r2(X1_204)) | t3least(X1_204) | ~s(X1_204, u8r1(X1_36)) | ~s(X1_204, u8r3(X1_36)) | s1most(X1_204)))). % 7.19/2.79 tff(c_1302, plain, (![X1_48, X1_269]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r1(X1_269)) | equalish(u9r2(X1_48), u10r1(X1_269)) | t3least(X1_269) | ~s(X1_269, u9r1(X1_48)) | ~r(X1_269, u9r2(X1_48)) | s1most(X1_269)))). % 7.19/2.80 tff(c_1629, plain, (![X1_3, X1_291]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r1(X1_291)) | equalish(u1r2(X1_3), u9r1(X1_291)) | t3least(X1_291) | ~s(X1_291, u1r1(X1_3)) | ~r(X1_291, u1r2(X1_3)) | r1most(X1_291)))). % 7.19/2.80 tff(c_1728, plain, (![X1_36, X1_298]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r1(X1_298)) | equalish(u8r3(X1_36), u10r1(X1_298)) | t3least(X1_298) | ~r(X1_298, u8r1(X1_36)) | ~s(X1_298, u8r3(X1_36)) | s1most(X1_298)))). % 7.19/2.80 tff(c_1723, plain, (![X1_37, X1_298]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r1(X1_298)) | equalish(u8r3(X1_37), u10r1(X1_298)) | t3least(X1_298) | ~r(X1_298, u8r2(X1_37)) | ~s(X1_298, u8r3(X1_37)) | s1most(X1_298)))). % 7.19/2.80 tff(c_874, plain, (![X1_54, X1_223]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r1(X1_223)) | equalish(u10r2(X1_54), u9r1(X1_223)) | t3least(X1_223) | ~r(X1_223, u10r1(X1_54)) | ~s(X1_223, u10r2(X1_54)) | r1most(X1_223)))). % 7.19/2.80 tff(c_606, plain, (![X1_48, X1_204]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r2(X1_204)) | equalish(u9r2(X1_48), u10r2(X1_204)) | t3least(X1_204) | ~s(X1_204, u9r1(X1_48)) | ~s(X1_204, u9r2(X1_48)) | s1most(X1_204)))). % 7.19/2.80 tff(c_1101, plain, (![X1_36, X1_249]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r1(X1_249)) | equalish(u8r3(X1_36), u9r1(X1_249)) | t3least(X1_249) | ~r(X1_249, u8r1(X1_36)) | ~r(X1_249, u8r3(X1_36)) | r1most(X1_249)))). % 7.19/2.80 tff(c_1461, plain, (![X1_3, X1_282]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r2(X1_282)) | equalish(u1r2(X1_3), u9r2(X1_282)) | t3least(X1_282) | ~r(X1_282, u1r1(X1_3)) | ~r(X1_282, u1r2(X1_3)) | r1most(X1_282)))). % 7.19/2.80 tff(c_1806, plain, (![X1_3, X1_306]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r2(X1_306)) | equalish(u1r2(X1_3), u10r2(X1_306)) | t3least(X1_306) | ~r(X1_306, u1r1(X1_3)) | ~r(X1_306, u1r2(X1_3)) | s1most(X1_306)))). % 7.19/2.80 tff(c_788, plain, (![X1_3, X1_216]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r2(X1_216)) | equalish(u1r2(X1_3), u10r2(X1_216)) | t3least(X1_216) | ~s(X1_216, u1r1(X1_3)) | ~r(X1_216, u1r2(X1_3)) | s1most(X1_216)))). % 7.19/2.80 tff(c_1725, plain, (![X1_54, X1_298]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r1(X1_298)) | equalish(u10r2(X1_54), u10r1(X1_298)) | t3least(X1_298) | ~r(X1_298, u10r1(X1_54)) | ~s(X1_298, u10r2(X1_54)) | s1most(X1_298)))). % 7.19/2.80 tff(c_603, plain, (![X1_37, X1_204]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r2(X1_204)) | equalish(u8r3(X1_37), u10r2(X1_204)) | t3least(X1_204) | ~s(X1_204, u8r2(X1_37)) | ~s(X1_204, u8r3(X1_37)) | s1most(X1_204)))). % 7.19/2.80 tff(c_1099, plain, (![X1_48, X1_249]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r1(X1_249)) | equalish(u9r2(X1_48), u9r1(X1_249)) | t3least(X1_249) | ~r(X1_249, u9r1(X1_48)) | ~r(X1_249, u9r2(X1_48)) | r1most(X1_249)))). % 7.19/2.80 tff(c_1907, plain, (![X1_48, X1_312]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r1(X1_312)) | equalish(u9r2(X1_48), u10r1(X1_312)) | t3least(X1_312) | ~r(X1_312, u9r1(X1_48)) | ~r(X1_312, u9r2(X1_48)) | s1most(X1_312)))). % 7.19/2.80 tff(c_1204, plain, (![X1_54, X1_263]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r2(X1_263)) | equalish(u10r2(X1_54), u9r2(X1_263)) | t3least(X1_263) | ~s(X1_263, u10r1(X1_54)) | ~r(X1_263, u10r2(X1_54)) | r1most(X1_263)))). % 7.19/2.80 tff(c_604, plain, (![X1_35, X1_204]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r2(X1_204)) | equalish(u8r2(X1_35), u10r2(X1_204)) | t3least(X1_204) | ~s(X1_204, u8r1(X1_35)) | ~s(X1_204, u8r2(X1_35)) | s1most(X1_204)))). % 7.19/2.80 tff(c_875, plain, (![X1_48, X1_223]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r1(X1_223)) | equalish(u9r2(X1_48), u9r1(X1_223)) | t3least(X1_223) | ~r(X1_223, u9r1(X1_48)) | ~s(X1_223, u9r2(X1_48)) | r1most(X1_223)))). % 7.19/2.80 tff(c_1997, plain, (![X1_36, X1_317]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r2(X1_317)) | equalish(u8r3(X1_36), u10r2(X1_317)) | t3least(X1_317) | ~r(X1_317, u8r1(X1_36)) | ~s(X1_317, u8r3(X1_36)) | s1most(X1_317)))). % 7.19/2.80 tff(c_1097, plain, (![X1_35, X1_249]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r1(X1_249)) | equalish(u8r2(X1_35), u9r1(X1_249)) | t3least(X1_249) | ~r(X1_249, u8r1(X1_35)) | ~r(X1_249, u8r2(X1_35)) | r1most(X1_249)))). % 7.19/2.80 tff(c_979, plain, (![X1_37, X1_234]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r1(X1_234)) | equalish(u8r3(X1_37), u10r1(X1_234)) | t3least(X1_234) | ~s(X1_234, u8r2(X1_37)) | ~s(X1_234, u8r3(X1_37)) | s1most(X1_234)))). % 7.19/2.80 tff(c_1631, plain, (![X1_35, X1_291]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r1(X1_291)) | equalish(u8r2(X1_35), u9r1(X1_291)) | t3least(X1_291) | ~s(X1_291, u8r1(X1_35)) | ~r(X1_291, u8r2(X1_35)) | r1most(X1_291)))). % 7.19/2.80 tff(c_1207, plain, (![X1_36, X1_263]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r2(X1_263)) | equalish(u8r3(X1_36), u9r2(X1_263)) | t3least(X1_263) | ~s(X1_263, u8r1(X1_36)) | ~r(X1_263, u8r3(X1_36)) | r1most(X1_263)))). % 7.19/2.80 tff(c_1376, plain, (![X1_35, X1_276]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r2(X1_276)) | equalish(u8r2(X1_35), u9r2(X1_276)) | t3least(X1_276) | ~s(X1_276, u8r1(X1_35)) | ~s(X1_276, u8r2(X1_35)) | r1most(X1_276)))). % 7.19/2.80 tff(c_1379, plain, (![X1_14, X1_276]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r2(X1_276)) | equalish(u3r2(X1_14), u9r2(X1_276)) | t3least(X1_276) | ~s(X1_276, u3r1(X1_14)) | ~s(X1_276, u3r2(X1_14)) | r1most(X1_276)))). % 7.19/2.80 tff(c_978, plain, (![X1_3, X1_234]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r1(X1_234)) | equalish(u1r2(X1_3), u10r1(X1_234)) | t3least(X1_234) | ~s(X1_234, u1r1(X1_3)) | ~s(X1_234, u1r2(X1_3)) | s1most(X1_234)))). % 7.19/2.80 tff(c_1377, plain, (![X1_54, X1_276]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r2(X1_276)) | equalish(u10r2(X1_54), u9r2(X1_276)) | t3least(X1_276) | ~s(X1_276, u10r1(X1_54)) | ~s(X1_276, u10r2(X1_54)) | r1most(X1_276)))). % 7.19/2.80 tff(c_607, plain, (![X1_14, X1_204]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r2(X1_204)) | equalish(u3r2(X1_14), u10r2(X1_204)) | t3least(X1_204) | ~s(X1_204, u3r1(X1_14)) | ~s(X1_204, u3r2(X1_14)) | s1most(X1_204)))). % 7.19/2.80 tff(c_701, plain, (![X1_35, X1_210]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r1(X1_210)) | equalish(u8r2(X1_35), u9r1(X1_210)) | t3least(X1_210) | ~s(X1_210, u8r1(X1_35)) | ~s(X1_210, u8r2(X1_35)) | r1most(X1_210)))). % 7.19/2.80 tff(c_1100, plain, (![X1_14, X1_249]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r1(X1_249)) | equalish(u3r2(X1_14), u9r1(X1_249)) | t3least(X1_249) | ~r(X1_249, u3r1(X1_14)) | ~r(X1_249, u3r2(X1_14)) | r1most(X1_249)))). % 7.19/2.80 tff(c_1380, plain, (![X1_36, X1_276]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r2(X1_276)) | equalish(u8r3(X1_36), u9r2(X1_276)) | t3least(X1_276) | ~s(X1_276, u8r1(X1_36)) | ~s(X1_276, u8r3(X1_36)) | r1most(X1_276)))). % 7.19/2.80 tff(c_1374, plain, (![X1_3, X1_276]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r2(X1_276)) | equalish(u1r2(X1_3), u9r2(X1_276)) | t3least(X1_276) | ~s(X1_276, u1r1(X1_3)) | ~s(X1_276, u1r2(X1_3)) | r1most(X1_276)))). % 7.19/2.80 tff(c_705, plain, (![X1_36, X1_210]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r1(X1_210)) | equalish(u8r3(X1_36), u9r1(X1_210)) | t3least(X1_210) | ~s(X1_210, u8r1(X1_36)) | ~s(X1_210, u8r3(X1_36)) | r1most(X1_210)))). % 7.19/2.80 tff(c_1464, plain, (![X1_54, X1_282]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r2(X1_282)) | equalish(u10r2(X1_54), u9r2(X1_282)) | t3least(X1_282) | ~r(X1_282, u10r1(X1_54)) | ~r(X1_282, u10r2(X1_54)) | r1most(X1_282)))). % 7.19/2.80 tff(c_703, plain, (![X1_48, X1_210]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r1(X1_210)) | equalish(u9r2(X1_48), u9r1(X1_210)) | t3least(X1_210) | ~s(X1_210, u9r1(X1_48)) | ~s(X1_210, u9r2(X1_48)) | r1most(X1_210)))). % 7.19/2.80 tff(c_1462, plain, (![X1_37, X1_282]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r2(X1_282)) | equalish(u8r3(X1_37), u9r2(X1_282)) | t3least(X1_282) | ~r(X1_282, u8r2(X1_37)) | ~r(X1_282, u8r3(X1_37)) | r1most(X1_282)))). % 7.19/2.80 tff(c_980, plain, (![X1_35, X1_234]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r1(X1_234)) | equalish(u8r2(X1_35), u10r1(X1_234)) | t3least(X1_234) | ~s(X1_234, u8r1(X1_35)) | ~s(X1_234, u8r2(X1_35)) | s1most(X1_234)))). % 7.19/2.80 tff(c_1995, plain, (![X1_48, X1_317]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r2(X1_317)) | equalish(u9r2(X1_48), u10r2(X1_317)) | t3least(X1_317) | ~r(X1_317, u9r1(X1_48)) | ~s(X1_317, u9r2(X1_48)) | s1most(X1_317)))). % 7.19/2.80 tff(c_877, plain, (![X1_36, X1_223]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r1(X1_223)) | equalish(u8r3(X1_36), u9r1(X1_223)) | t3least(X1_223) | ~r(X1_223, u8r1(X1_36)) | ~s(X1_223, u8r3(X1_36)) | r1most(X1_223)))). % 7.19/2.80 tff(c_1465, plain, (![X1_48, X1_282]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r2(X1_282)) | equalish(u9r2(X1_48), u9r2(X1_282)) | t3least(X1_282) | ~r(X1_282, u9r1(X1_48)) | ~r(X1_282, u9r2(X1_48)) | r1most(X1_282)))). % 7.19/2.80 tff(c_794, plain, (![X1_36, X1_216]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r2(X1_216)) | equalish(u8r3(X1_36), u10r2(X1_216)) | t3least(X1_216) | ~s(X1_216, u8r1(X1_36)) | ~r(X1_216, u8r3(X1_36)) | s1most(X1_216)))). % 7.19/2.80 tff(c_1904, plain, (![X1_37, X1_312]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r1(X1_312)) | equalish(u8r3(X1_37), u10r1(X1_312)) | t3least(X1_312) | ~r(X1_312, u8r2(X1_37)) | ~r(X1_312, u8r3(X1_37)) | s1most(X1_312)))). % 7.19/2.80 tff(c_699, plain, (![X1_3, X1_210]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r1(X1_210)) | equalish(u1r2(X1_3), u9r1(X1_210)) | t3least(X1_210) | ~s(X1_210, u1r1(X1_3)) | ~s(X1_210, u1r2(X1_3)) | r1most(X1_210)))). % 7.19/2.80 tff(c_1551, plain, (![X1_54, X1_288]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r2(X1_288)) | equalish(u10r2(X1_54), u9r2(X1_288)) | t3least(X1_288) | ~r(X1_288, u10r1(X1_54)) | ~s(X1_288, u10r2(X1_54)) | r1most(X1_288)))). % 7.19/2.80 tff(c_1552, plain, (![X1_48, X1_288]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r2(X1_288)) | equalish(u9r2(X1_48), u9r2(X1_288)) | t3least(X1_288) | ~r(X1_288, u9r1(X1_48)) | ~s(X1_288, u9r2(X1_48)) | r1most(X1_288)))). % 7.19/2.80 tff(c_1375, plain, (![X1_37, X1_276]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r2(X1_276)) | equalish(u8r3(X1_37), u9r2(X1_276)) | t3least(X1_276) | ~s(X1_276, u8r2(X1_37)) | ~s(X1_276, u8r3(X1_37)) | r1most(X1_276)))). % 7.19/2.80 tff(c_1550, plain, (![X1_35, X1_288]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r2(X1_288)) | equalish(u8r2(X1_35), u9r2(X1_288)) | t3least(X1_288) | ~r(X1_288, u8r1(X1_35)) | ~s(X1_288, u8r2(X1_35)) | r1most(X1_288)))). % 7.19/2.81 tff(c_1903, plain, (![X1_3, X1_312]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r1(X1_312)) | equalish(u1r2(X1_3), u10r1(X1_312)) | t3least(X1_312) | ~r(X1_312, u1r1(X1_3)) | ~r(X1_312, u1r2(X1_3)) | s1most(X1_312)))). % 7.19/2.81 tff(c_1549, plain, (![X1_37, X1_288]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r2(X1_288)) | equalish(u8r3(X1_37), u9r2(X1_288)) | t3least(X1_288) | ~r(X1_288, u8r2(X1_37)) | ~s(X1_288, u8r3(X1_37)) | r1most(X1_288)))). % 7.19/2.81 tff(c_1206, plain, (![X1_14, X1_263]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r2(X1_263)) | equalish(u3r2(X1_14), u9r2(X1_263)) | t3least(X1_263) | ~s(X1_263, u3r1(X1_14)) | ~r(X1_263, u3r2(X1_14)) | r1most(X1_263)))). % 7.19/2.81 tff(c_789, plain, (![X1_37, X1_216]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r2(X1_216)) | equalish(u8r3(X1_37), u10r2(X1_216)) | t3least(X1_216) | ~s(X1_216, u8r2(X1_37)) | ~r(X1_216, u8r3(X1_37)) | s1most(X1_216)))). % 7.19/2.81 tff(c_873, plain, (![X1_35, X1_223]: (~t3least(X1_35) | equalish(u8r1(X1_35), u9r1(X1_223)) | equalish(u8r2(X1_35), u9r1(X1_223)) | t3least(X1_223) | ~r(X1_223, u8r1(X1_35)) | ~s(X1_223, u8r2(X1_35)) | r1most(X1_223)))). % 7.19/2.81 tff(c_1635, plain, (![X1_36, X1_291]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r1(X1_291)) | equalish(u8r3(X1_36), u9r1(X1_291)) | t3least(X1_291) | ~s(X1_291, u8r1(X1_36)) | ~r(X1_291, u8r3(X1_36)) | r1most(X1_291)))). % 7.19/2.81 tff(c_1378, plain, (![X1_48, X1_276]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r2(X1_276)) | equalish(u9r2(X1_48), u9r2(X1_276)) | t3least(X1_276) | ~s(X1_276, u9r1(X1_48)) | ~s(X1_276, u9r2(X1_48)) | r1most(X1_276)))). % 7.19/2.81 tff(c_1632, plain, (![X1_54, X1_291]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r1(X1_291)) | equalish(u10r2(X1_54), u9r1(X1_291)) | t3least(X1_291) | ~s(X1_291, u10r1(X1_54)) | ~r(X1_291, u10r2(X1_54)) | r1most(X1_291)))). % 7.19/2.81 tff(c_602, plain, (![X1_3, X1_204]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r2(X1_204)) | equalish(u1r2(X1_3), u10r2(X1_204)) | t3least(X1_204) | ~s(X1_204, u1r1(X1_3)) | ~s(X1_204, u1r2(X1_3)) | s1most(X1_204)))). % 7.19/2.81 tff(c_1300, plain, (![X1_35, X1_269]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r1(X1_269)) | equalish(u8r2(X1_35), u10r1(X1_269)) | t3least(X1_269) | ~s(X1_269, u8r1(X1_35)) | ~r(X1_269, u8r2(X1_35)) | s1most(X1_269)))). % 7.19/2.81 tff(c_1809, plain, (![X1_54, X1_306]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r2(X1_306)) | equalish(u10r2(X1_54), u10r2(X1_306)) | t3least(X1_306) | ~r(X1_306, u10r1(X1_54)) | ~r(X1_306, u10r2(X1_54)) | s1most(X1_306)))). % 7.19/2.81 tff(c_1098, plain, (![X1_54, X1_249]: (s1most(X1_54) | equalish(u10r1(X1_54), u9r1(X1_249)) | equalish(u10r2(X1_54), u9r1(X1_249)) | t3least(X1_249) | ~r(X1_249, u10r1(X1_54)) | ~r(X1_249, u10r2(X1_54)) | r1most(X1_249)))). % 7.19/2.81 tff(c_1466, plain, (![X1_14, X1_282]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r2(X1_282)) | equalish(u3r2(X1_14), u9r2(X1_282)) | t3least(X1_282) | ~r(X1_282, u3r1(X1_14)) | ~r(X1_282, u3r2(X1_14)) | r1most(X1_282)))). % 7.19/2.81 tff(c_1205, plain, (![X1_48, X1_263]: (r1most(X1_48) | equalish(u9r1(X1_48), u9r2(X1_263)) | equalish(u9r2(X1_48), u9r2(X1_263)) | t3least(X1_263) | ~s(X1_263, u9r1(X1_48)) | ~r(X1_263, u9r2(X1_48)) | r1most(X1_263)))). % 7.19/2.81 tff(c_1727, plain, (![X1_14, X1_298]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r1(X1_298)) | equalish(u3r2(X1_14), u10r1(X1_298)) | t3least(X1_298) | ~r(X1_298, u3r1(X1_14)) | ~s(X1_298, u3r2(X1_14)) | s1most(X1_298)))). % 7.19/2.81 tff(c_790, plain, (![X1_35, X1_216]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r2(X1_216)) | equalish(u8r2(X1_35), u10r2(X1_216)) | t3least(X1_216) | ~s(X1_216, u8r1(X1_35)) | ~r(X1_216, u8r2(X1_35)) | s1most(X1_216)))). % 7.19/2.81 tff(c_1724, plain, (![X1_35, X1_298]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r1(X1_298)) | equalish(u8r2(X1_35), u10r1(X1_298)) | t3least(X1_298) | ~r(X1_298, u8r1(X1_35)) | ~s(X1_298, u8r2(X1_35)) | s1most(X1_298)))). % 7.19/2.81 tff(c_1202, plain, (![X1_37, X1_263]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r2(X1_263)) | equalish(u8r3(X1_37), u9r2(X1_263)) | t3least(X1_263) | ~s(X1_263, u8r2(X1_37)) | ~r(X1_263, u8r3(X1_37)) | r1most(X1_263)))). % 7.19/2.81 tff(c_1298, plain, (![X1_3, X1_269]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r1(X1_269)) | equalish(u1r2(X1_3), u10r1(X1_269)) | t3least(X1_269) | ~s(X1_269, u1r1(X1_3)) | ~r(X1_269, u1r2(X1_3)) | s1most(X1_269)))). % 7.19/2.81 tff(c_872, plain, (![X1_37, X1_223]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r1(X1_223)) | equalish(u8r3(X1_37), u9r1(X1_223)) | t3least(X1_223) | ~r(X1_223, u8r2(X1_37)) | ~s(X1_223, u8r3(X1_37)) | r1most(X1_223)))). % 7.19/2.81 tff(c_1722, plain, (![X1_3, X1_298]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r1(X1_298)) | equalish(u1r2(X1_3), u10r1(X1_298)) | t3least(X1_298) | ~r(X1_298, u1r1(X1_3)) | ~s(X1_298, u1r2(X1_3)) | s1most(X1_298)))). % 7.19/2.81 tff(c_1553, plain, (![X1_14, X1_288]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r2(X1_288)) | equalish(u3r2(X1_14), u9r2(X1_288)) | t3least(X1_288) | ~r(X1_288, u3r1(X1_14)) | ~s(X1_288, u3r2(X1_14)) | r1most(X1_288)))). % 7.19/2.81 tff(c_1301, plain, (![X1_54, X1_269]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r1(X1_269)) | equalish(u10r2(X1_54), u10r1(X1_269)) | t3least(X1_269) | ~s(X1_269, u10r1(X1_54)) | ~r(X1_269, u10r2(X1_54)) | s1most(X1_269)))). % 7.19/2.81 tff(c_1467, plain, (![X1_36, X1_282]: (~t3least(X1_36) | equalish(u8r1(X1_36), u9r2(X1_282)) | equalish(u8r3(X1_36), u9r2(X1_282)) | t3least(X1_282) | ~r(X1_282, u8r1(X1_36)) | ~r(X1_282, u8r3(X1_36)) | r1most(X1_282)))). % 7.19/2.81 tff(c_1994, plain, (![X1_54, X1_317]: (s1most(X1_54) | equalish(u10r1(X1_54), u10r2(X1_317)) | equalish(u10r2(X1_54), u10r2(X1_317)) | t3least(X1_317) | ~r(X1_317, u10r1(X1_54)) | ~s(X1_317, u10r2(X1_54)) | s1most(X1_317)))). % 7.19/2.81 tff(c_1810, plain, (![X1_48, X1_306]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r2(X1_306)) | equalish(u9r2(X1_48), u10r2(X1_306)) | t3least(X1_306) | ~r(X1_306, u9r1(X1_48)) | ~r(X1_306, u9r2(X1_48)) | s1most(X1_306)))). % 7.19/2.81 tff(c_1807, plain, (![X1_37, X1_306]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r2(X1_306)) | equalish(u8r3(X1_37), u10r2(X1_306)) | t3least(X1_306) | ~r(X1_306, u8r2(X1_37)) | ~r(X1_306, u8r3(X1_37)) | s1most(X1_306)))). % 7.19/2.81 tff(c_1812, plain, (![X1_36, X1_306]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r2(X1_306)) | equalish(u8r3(X1_36), u10r2(X1_306)) | t3least(X1_306) | ~r(X1_306, u8r1(X1_36)) | ~r(X1_306, u8r3(X1_36)) | s1most(X1_306)))). % 7.19/2.81 tff(c_984, plain, (![X1_36, X1_234]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r1(X1_234)) | equalish(u8r3(X1_36), u10r1(X1_234)) | t3least(X1_234) | ~s(X1_234, u8r1(X1_36)) | ~s(X1_234, u8r3(X1_36)) | s1most(X1_234)))). % 7.19/2.81 tff(c_1630, plain, (![X1_37, X1_291]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r1(X1_291)) | equalish(u8r3(X1_37), u9r1(X1_291)) | t3least(X1_291) | ~s(X1_291, u8r2(X1_37)) | ~r(X1_291, u8r3(X1_37)) | r1most(X1_291)))). % 7.19/2.81 tff(c_1299, plain, (![X1_37, X1_269]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r1(X1_269)) | equalish(u8r3(X1_37), u10r1(X1_269)) | t3least(X1_269) | ~s(X1_269, u8r2(X1_37)) | ~r(X1_269, u8r3(X1_37)) | s1most(X1_269)))). % 7.19/2.81 tff(c_982, plain, (![X1_48, X1_234]: (r1most(X1_48) | equalish(u9r1(X1_48), u10r1(X1_234)) | equalish(u9r2(X1_48), u10r1(X1_234)) | t3least(X1_234) | ~s(X1_234, u9r1(X1_48)) | ~s(X1_234, u9r2(X1_48)) | s1most(X1_234)))). % 7.19/2.81 tff(c_1096, plain, (![X1_37, X1_249]: (~t3least(X1_37) | equalish(u8r2(X1_37), u9r1(X1_249)) | equalish(u8r3(X1_37), u9r1(X1_249)) | t3least(X1_249) | ~r(X1_249, u8r2(X1_37)) | ~r(X1_249, u8r3(X1_37)) | r1most(X1_249)))). % 7.19/2.81 tff(c_1303, plain, (![X1_14, X1_269]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r1(X1_269)) | equalish(u3r2(X1_14), u10r1(X1_269)) | t3least(X1_269) | ~s(X1_269, u3r1(X1_14)) | ~r(X1_269, u3r2(X1_14)) | s1most(X1_269)))). % 7.19/2.81 tff(c_1808, plain, (![X1_35, X1_306]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r2(X1_306)) | equalish(u8r2(X1_35), u10r2(X1_306)) | t3least(X1_306) | ~r(X1_306, u8r1(X1_35)) | ~r(X1_306, u8r2(X1_35)) | s1most(X1_306)))). % 7.19/2.81 tff(c_983, plain, (![X1_14, X1_234]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r1(X1_234)) | equalish(u3r2(X1_14), u10r1(X1_234)) | t3least(X1_234) | ~s(X1_234, u3r1(X1_14)) | ~s(X1_234, u3r2(X1_14)) | s1most(X1_234)))). % 7.19/2.81 tff(c_1905, plain, (![X1_35, X1_312]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r1(X1_312)) | equalish(u8r2(X1_35), u10r1(X1_312)) | t3least(X1_312) | ~r(X1_312, u8r1(X1_35)) | ~r(X1_312, u8r2(X1_35)) | s1most(X1_312)))). % 7.19/2.81 tff(c_1304, plain, (![X1_36, X1_269]: (~t3least(X1_36) | equalish(u8r1(X1_36), u10r1(X1_269)) | equalish(u8r3(X1_36), u10r1(X1_269)) | t3least(X1_269) | ~s(X1_269, u8r1(X1_36)) | ~r(X1_269, u8r3(X1_36)) | s1most(X1_269)))). % 7.19/2.81 tff(c_704, plain, (![X1_14, X1_210]: (p1most(X1_14) | equalish(u3r1(X1_14), u9r1(X1_210)) | equalish(u3r2(X1_14), u9r1(X1_210)) | t3least(X1_210) | ~s(X1_210, u3r1(X1_14)) | ~s(X1_210, u3r2(X1_14)) | r1most(X1_210)))). % 7.19/2.81 tff(c_871, plain, (![X1_3, X1_223]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r1(X1_223)) | equalish(u1r2(X1_3), u9r1(X1_223)) | t3least(X1_223) | ~r(X1_223, u1r1(X1_3)) | ~s(X1_223, u1r2(X1_3)) | r1most(X1_223)))). % 7.19/2.81 tff(c_1993, plain, (![X1_35, X1_317]: (~t3least(X1_35) | equalish(u8r1(X1_35), u10r2(X1_317)) | equalish(u8r2(X1_35), u10r2(X1_317)) | t3least(X1_317) | ~r(X1_317, u8r1(X1_35)) | ~s(X1_317, u8r2(X1_35)) | s1most(X1_317)))). % 7.19/2.81 tff(c_1095, plain, (![X1_3, X1_249]: (~p2least(X1_3) | equalish(u1r1(X1_3), u9r1(X1_249)) | equalish(u1r2(X1_3), u9r1(X1_249)) | t3least(X1_249) | ~r(X1_249, u1r1(X1_3)) | ~r(X1_249, u1r2(X1_3)) | r1most(X1_249)))). % 7.19/2.81 tff(c_1991, plain, (![X1_3, X1_317]: (~p2least(X1_3) | equalish(u1r1(X1_3), u10r2(X1_317)) | equalish(u1r2(X1_3), u10r2(X1_317)) | t3least(X1_317) | ~r(X1_317, u1r1(X1_3)) | ~s(X1_317, u1r2(X1_3)) | s1most(X1_317)))). % 7.19/2.81 tff(c_1992, plain, (![X1_37, X1_317]: (~t3least(X1_37) | equalish(u8r2(X1_37), u10r2(X1_317)) | equalish(u8r3(X1_37), u10r2(X1_317)) | t3least(X1_317) | ~r(X1_317, u8r2(X1_37)) | ~s(X1_317, u8r3(X1_37)) | s1most(X1_317)))). % 7.19/2.81 tff(c_1908, plain, (![X1_14, X1_312]: (p1most(X1_14) | equalish(u3r1(X1_14), u10r1(X1_312)) | equalish(u3r2(X1_14), u10r1(X1_312)) | t3least(X1_312) | ~r(X1_312, u3r1(X1_14)) | ~r(X1_312, u3r2(X1_14)) | s1most(X1_312)))). % 7.19/2.81 tff(c_516, plain, (![X2_187, X1_56, X2_189]: (equalish(X2_187, u10r2(X1_56)) | equalish(X2_189, u10r2(X1_56)) | equalish(X2_189, X2_187) | t3least(X1_56) | ~r(X1_56, X2_187) | ~s(X1_56, X2_189) | s1most(X1_56)))). % 7.19/2.81 tff(c_1868, plain, (![X2_183, X1_55]: (equalish(X2_183, X2_183) | t3least(X1_55) | ~r(X1_55, X2_183) | s1most(X1_55) | equalish(X2_183, u10r1(X1_55))))). % 7.19/2.81 tff(c_508, plain, (![X2_183, X1_55, X2_185]: (equalish(X2_183, u10r1(X1_55)) | equalish(X2_185, u10r1(X1_55)) | equalish(X2_185, X2_183) | t3least(X1_55) | ~r(X1_55, X2_183) | ~r(X1_55, X2_185) | s1most(X1_55)))). % 7.19/2.81 tff(c_1781, plain, (![X2_183, X1_56]: (equalish(X2_183, X2_183) | t3least(X1_56) | ~r(X1_56, X2_183) | s1most(X1_56) | equalish(X2_183, u10r2(X1_56))))). % 7.19/2.81 tff(c_1779, plain, (![X1_56]: (t3least(X1_56) | ~r(X1_56, u10r2(X1_56)) | s1most(X1_56) | equalish(u10r2(X1_56), u10r2(X1_56))))). % 7.19/2.81 tff(c_509, plain, (![X2_183, X1_56, X2_185]: (equalish(X2_183, u10r2(X1_56)) | equalish(X2_185, u10r2(X1_56)) | equalish(X2_185, X2_183) | t3least(X1_56) | ~r(X1_56, X2_183) | ~r(X1_56, X2_185) | s1most(X1_56)))). % 7.19/2.81 tff(c_1740, plain, (![X1_303]: (equalish(u10r1(X1_303), u10r1(X1_303)) | t3least(X1_303) | ~r(X1_303, u10r1(X1_303)) | s1most(X1_303)))). % 7.19/2.81 tff(c_1732, plain, (![X2_300, X1_56]: (equalish(X2_300, u10r1(X1_56)) | equalish(u10r2(X1_56), X2_300) | t3least(X1_56) | ~r(X1_56, X2_300) | s1most(X1_56)))). % 7.19/2.81 tff(c_515, plain, (![X2_187, X1_55, X2_189]: (equalish(X2_187, u10r1(X1_55)) | equalish(X2_189, u10r1(X1_55)) | equalish(X2_189, X2_187) | t3least(X1_55) | ~r(X1_55, X2_187) | ~s(X1_55, X2_189) | s1most(X1_55)))). % 7.19/2.81 tff(c_1639, plain, (![X2_293, X1_50]: (equalish(X2_293, u9r1(X1_50)) | equalish(u9r2(X1_50), X2_293) | t3least(X1_50) | ~s(X1_50, X2_293) | r1most(X1_50)))). % 7.19/2.81 tff(c_488, plain, (![X2_171, X1_49, X2_173]: (equalish(X2_171, u9r1(X1_49)) | equalish(X2_173, u9r1(X1_49)) | equalish(X2_173, X2_171) | t3least(X1_49) | ~s(X1_49, X2_171) | ~r(X1_49, X2_173) | r1most(X1_49)))). % 7.19/2.81 tff(c_536, plain, (![X2_199, X1_50, X2_201]: (equalish(X2_199, u9r2(X1_50)) | equalish(X2_201, u9r2(X1_50)) | equalish(X2_201, X2_199) | t3least(X1_50) | ~r(X1_50, X2_199) | ~s(X1_50, X2_201) | r1most(X1_50)))). % 7.19/2.81 tff(c_1436, plain, (![X2_179, X1_50]: (equalish(X2_179, X2_179) | t3least(X1_50) | ~r(X1_50, X2_179) | r1most(X1_50) | equalish(X2_179, u9r2(X1_50))))). % 7.19/2.81 tff(c_1434, plain, (![X1_50]: (t3least(X1_50) | ~r(X1_50, u9r2(X1_50)) | r1most(X1_50) | equalish(u9r2(X1_50), u9r2(X1_50))))). % 7.19/2.81 tff(c_501, plain, (![X2_179, X1_50, X2_181]: (equalish(X2_179, u9r2(X1_50)) | equalish(X2_181, u9r2(X1_50)) | equalish(X2_181, X2_179) | t3least(X1_50) | ~r(X1_50, X2_179) | ~r(X1_50, X2_181) | r1most(X1_50)))). % 7.19/2.81 tff(c_1349, plain, (![X2_191, X1_50]: (equalish(X2_191, X2_191) | t3least(X1_50) | ~s(X1_50, X2_191) | r1most(X1_50) | equalish(X2_191, u9r2(X1_50))))). % 7.19/2.81 tff(c_1347, plain, (![X1_50]: (t3least(X1_50) | ~s(X1_50, u9r2(X1_50)) | r1most(X1_50) | equalish(u9r2(X1_50), u9r2(X1_50))))). % 7.19/2.81 tff(c_522, plain, (![X2_191, X1_50, X2_193]: (equalish(X2_191, u9r2(X1_50)) | equalish(X2_193, u9r2(X1_50)) | equalish(X2_193, X2_191) | t3least(X1_50) | ~s(X1_50, X2_191) | ~s(X1_50, X2_193) | r1most(X1_50)))). % 7.19/2.81 tff(c_1308, plain, (![X2_271, X1_56]: (equalish(X2_271, u10r1(X1_56)) | equalish(X2_271, u10r2(X1_56)) | t3least(X1_56) | ~r(X1_56, X2_271) | s1most(X1_56)))). % 7.19/2.81 tff(c_494, plain, (![X2_175, X1_55, X2_177]: (equalish(X2_175, u10r1(X1_55)) | equalish(X2_177, u10r1(X1_55)) | equalish(X2_177, X2_175) | t3least(X1_55) | ~s(X1_55, X2_175) | ~r(X1_55, X2_177) | s1most(X1_55)))). % 7.19/2.81 tff(c_487, plain, (![X2_171, X1_50, X2_173]: (equalish(X2_171, u9r2(X1_50)) | equalish(X2_173, u9r2(X1_50)) | equalish(X2_173, X2_171) | t3least(X1_50) | ~s(X1_50, X2_171) | ~r(X1_50, X2_173) | r1most(X1_50)))). % 7.19/2.81 tff(c_1128, plain, (![X2_258, X1_50]: (equalish(X2_258, u9r1(X1_50)) | equalish(u9r2(X1_50), X2_258) | t3least(X1_50) | ~r(X1_50, X2_258) | r1most(X1_50)))). % 7.19/2.81 tff(c_1123, plain, (![X2_254, X1_50]: (equalish(X2_254, u9r1(X1_50)) | equalish(X2_254, u9r2(X1_50)) | t3least(X1_50) | ~r(X1_50, X2_254) | r1most(X1_50)))). % 7.19/2.81 tff(c_1060, plain, (![X2_179, X1_49]: (equalish(X2_179, X2_179) | t3least(X1_49) | ~r(X1_49, X2_179) | r1most(X1_49) | equalish(X2_179, u9r1(X1_49))))). % 7.19/2.81 tff(c_1058, plain, (![X1_49]: (t3least(X1_49) | ~r(X1_49, u9r1(X1_49)) | r1most(X1_49) | equalish(u9r1(X1_49), u9r1(X1_49))))). % 7.19/2.81 tff(c_502, plain, (![X2_179, X1_49, X2_181]: (equalish(X2_179, u9r1(X1_49)) | equalish(X2_181, u9r1(X1_49)) | equalish(X2_181, X2_179) | t3least(X1_49) | ~r(X1_49, X2_179) | ~r(X1_49, X2_181) | r1most(X1_49)))). % 7.19/2.81 tff(c_1019, plain, (![X2_244, X1_56]: (equalish(X2_244, u10r1(X1_56)) | equalish(X2_244, u10r2(X1_56)) | t3least(X1_56) | ~s(X1_56, X2_244) | s1most(X1_56)))). % 7.19/2.81 tff(c_1007, plain, (![X2_240, X1_56]: (equalish(X2_240, u10r1(X1_56)) | equalish(u10r2(X1_56), X2_240) | t3least(X1_56) | ~s(X1_56, X2_240) | s1most(X1_56)))). % 7.19/2.81 tff(c_943, plain, (![X2_195, X1_55]: (equalish(X2_195, X2_195) | t3least(X1_55) | ~s(X1_55, X2_195) | s1most(X1_55) | equalish(X2_195, u10r1(X1_55))))). % 7.19/2.81 tff(c_941, plain, (![X1_55]: (t3least(X1_55) | ~s(X1_55, u10r1(X1_55)) | s1most(X1_55) | equalish(u10r1(X1_55), u10r1(X1_55))))). % 7.19/2.81 tff(c_529, plain, (![X2_195, X1_55, X2_197]: (equalish(X2_195, u10r1(X1_55)) | equalish(X2_197, u10r1(X1_55)) | equalish(X2_197, X2_195) | t3least(X1_55) | ~s(X1_55, X2_195) | ~s(X1_55, X2_197) | s1most(X1_55)))). % 7.19/2.81 tff(c_881, plain, (![X2_225, X1_50]: (equalish(X2_225, u9r1(X1_50)) | equalish(X2_225, u9r2(X1_50)) | t3least(X1_50) | ~s(X1_50, X2_225) | r1most(X1_50)))). % 7.19/2.81 tff(c_537, plain, (![X2_199, X1_49, X2_201]: (equalish(X2_199, u9r1(X1_49)) | equalish(X2_201, u9r1(X1_49)) | equalish(X2_201, X2_199) | t3least(X1_49) | ~r(X1_49, X2_199) | ~s(X1_49, X2_201) | r1most(X1_49)))). % 7.19/2.81 tff(c_495, plain, (![X2_175, X1_56, X2_177]: (equalish(X2_175, u10r2(X1_56)) | equalish(X2_177, u10r2(X1_56)) | equalish(X2_177, X2_175) | t3least(X1_56) | ~s(X1_56, X2_175) | ~r(X1_56, X2_177) | s1most(X1_56)))). % 7.19/2.81 tff(c_664, plain, (![X2_191, X1_49]: (equalish(X2_191, X2_191) | t3least(X1_49) | ~s(X1_49, X2_191) | r1most(X1_49) | equalish(X2_191, u9r1(X1_49))))). % 7.19/2.81 tff(c_662, plain, (![X1_49]: (t3least(X1_49) | ~s(X1_49, u9r1(X1_49)) | r1most(X1_49) | equalish(u9r1(X1_49), u9r1(X1_49))))). % 7.19/2.82 tff(c_523, plain, (![X2_191, X1_49, X2_193]: (equalish(X2_191, u9r1(X1_49)) | equalish(X2_193, u9r1(X1_49)) | equalish(X2_193, X2_191) | t3least(X1_49) | ~s(X1_49, X2_191) | ~s(X1_49, X2_193) | r1most(X1_49)))). % 7.19/2.82 tff(c_577, plain, (![X2_195, X1_56]: (equalish(X2_195, X2_195) | t3least(X1_56) | ~s(X1_56, X2_195) | s1most(X1_56) | equalish(X2_195, u10r2(X1_56))))). % 7.19/2.82 tff(c_575, plain, (![X1_56]: (t3least(X1_56) | ~s(X1_56, u10r2(X1_56)) | s1most(X1_56) | equalish(u10r2(X1_56), u10r2(X1_56))))). % 7.19/2.82 tff(c_530, plain, (![X2_195, X1_56, X2_197]: (equalish(X2_195, u10r2(X1_56)) | equalish(X2_197, u10r2(X1_56)) | equalish(X2_197, X2_195) | t3least(X1_56) | ~s(X1_56, X2_195) | ~s(X1_56, X2_197) | s1most(X1_56)))). % 7.19/2.82 tff(c_430, plain, (![X2_157, X2_158, X2_27, X1_26]: (equalish(X2_157, X2_158) | equalish(X2_27, X2_158) | equalish(X2_27, X2_157) | t3least(X1_26) | ~r(X1_26, X2_158) | ~r(X1_26, X2_157) | ~s(X1_26, X2_27)))). % 7.19/2.82 tff(c_478, plain, (![X2_169, X2_170, X2_27, X1_26]: (equalish(X2_169, X2_170) | equalish(X2_27, X2_170) | equalish(X2_27, X2_169) | t3least(X1_26) | ~s(X1_26, X2_170) | ~s(X1_26, X2_169) | ~s(X1_26, X2_27)))). % 7.19/2.82 tff(c_462, plain, (![X2_165, X2_166, X2_27, X1_26]: (equalish(X2_165, X2_166) | equalish(X2_27, X2_166) | equalish(X2_27, X2_165) | t3least(X1_26) | ~r(X1_26, X2_166) | ~s(X1_26, X2_165) | ~s(X1_26, X2_27)))). % 7.19/2.82 tff(c_446, plain, (![X2_161, X2_162, X2_27, X1_26]: (equalish(X2_161, X2_162) | equalish(X2_27, X2_162) | equalish(X2_27, X2_161) | t3least(X1_26) | ~s(X1_26, X2_162) | ~r(X1_26, X2_161) | ~s(X1_26, X2_27)))). % 7.19/2.82 tff(c_449, plain, (![X2_161, X2_162, X2_23, X1_22]: (equalish(X2_161, X2_162) | equalish(X2_23, X2_162) | equalish(X2_23, X2_161) | t3least(X1_22) | ~s(X1_22, X2_162) | ~r(X1_22, X2_161) | ~r(X1_22, X2_23)))). % 7.19/2.82 tff(c_433, plain, (![X2_157, X2_158, X2_23, X1_22]: (equalish(X2_157, X2_158) | equalish(X2_23, X2_158) | equalish(X2_23, X2_157) | t3least(X1_22) | ~r(X1_22, X2_158) | ~r(X1_22, X2_157) | ~r(X1_22, X2_23)))). % 7.19/2.82 tff(c_481, plain, (![X2_169, X2_170, X2_23, X1_22]: (equalish(X2_169, X2_170) | equalish(X2_23, X2_170) | equalish(X2_23, X2_169) | t3least(X1_22) | ~s(X1_22, X2_170) | ~s(X1_22, X2_169) | ~r(X1_22, X2_23)))). % 7.19/2.82 tff(c_465, plain, (![X2_165, X2_166, X2_23, X1_22]: (equalish(X2_165, X2_166) | equalish(X2_23, X2_166) | equalish(X2_23, X2_165) | t3least(X1_22) | ~r(X1_22, X2_166) | ~s(X1_22, X2_165) | ~r(X1_22, X2_23)))). % 7.19/2.82 tff(c_414, plain, (![X1_26, X4_153, X2_27, X2_154]: (~t(X1_26, X4_153) | equalish(X2_27, X2_154) | equalish(X4_153, X2_154) | equalish(X4_153, X2_27) | t3least(X1_26) | ~s(X1_26, X2_154) | ~s(X1_26, X2_27)))). % 7.19/2.82 tff(c_337, plain, (![X1_26, X4_143, X2_27, X2_144]: (~t(X1_26, X4_143) | equalish(X2_27, X2_144) | equalish(X4_143, X2_144) | equalish(X4_143, X2_27) | t3least(X1_26) | ~r(X1_26, X2_144) | ~s(X1_26, X2_27)))). % 7.19/2.82 tff(c_417, plain, (![X1_22, X4_153, X2_23, X2_154]: (~t(X1_22, X4_153) | equalish(X2_23, X2_154) | equalish(X4_153, X2_154) | equalish(X4_153, X2_23) | t3least(X1_22) | ~s(X1_22, X2_154) | ~r(X1_22, X2_23)))). % 7.19/2.82 tff(c_340, plain, (![X1_22, X4_143, X2_23, X2_144]: (~t(X1_22, X4_143) | equalish(X2_23, X2_144) | equalish(X4_143, X2_144) | equalish(X4_143, X2_23) | t3least(X1_22) | ~r(X1_22, X2_144) | ~r(X1_22, X2_23)))). % 7.19/2.82 tff(c_305, plain, (![X1_26, X3_133, X4_134, X2_27]: (~t(X1_26, X3_133) | ~t(X1_26, X4_134) | equalish(X3_133, X2_27) | equalish(X4_134, X2_27) | equalish(X4_134, X3_133) | t3least(X1_26) | ~s(X1_26, X2_27)))). % 7.19/2.82 tff(c_383, plain, (![X1_33]: (~s1most(X1_33) | ~r1most(X1_33) | ~t3least(X1_33) | e(X1_33)))). % 7.19/2.82 tff(c_380, plain, (![X1_148]: (a(X1_148)))). % 7.19/2.82 tff(c_358, plain, (![X1_146]: (d(X1_146) | c(X1_146)))). % 7.19/2.82 tff(c_349, plain, (![X1_145]: (c(X1_145) | p1most(X1_145)))). % 7.19/2.82 tff(c_321, plain, (![X1_16]: (p2least(X1_16) | p1most(X1_16)))). % 7.19/2.82 tff(c_308, plain, (![X1_22, X3_133, X4_134, X2_23]: (~t(X1_22, X3_133) | ~t(X1_22, X4_134) | equalish(X3_133, X2_23) | equalish(X4_134, X2_23) | equalish(X4_134, X3_133) | t3least(X1_22) | ~r(X1_22, X2_23)))). % 7.19/2.82 tff(c_288, plain, (![X1_70]: (~c(u10r2(X1_70)) | s1most(X1_70)))). % 7.19/2.82 tff(c_66, plain, (![X1_41, X2_44, X3_43, X4_42]: (~t(X1_41, X2_44) | ~t(X1_41, X3_43) | ~t(X1_41, X4_42) | equalish(X3_43, X2_44) | equalish(X4_42, X2_44) | equalish(X4_42, X3_43) | t3least(X1_41)))). % 7.19/2.82 tff(c_287, plain, (![X1_77]: (~c(u10r1(X1_77)) | s1most(X1_77)))). % 7.19/2.82 tff(c_275, plain, (![X1_9]: (~c(X1_9) | ~d(X1_9)))). % 7.19/2.82 tff(c_265, plain, (![X1_1]: (~p1most(X1_1) | ~c(X1_1)))). % 7.19/2.82 tff(c_260, plain, (![X1_5]: (~p1most(X1_5) | ~p2least(X1_5)))). % 7.19/2.82 tff(c_14, plain, (![X1_6, X2_8, X3_7]: (~p(X1_6, X2_8) | ~p(X1_6, X3_7) | equalish(X3_7, X2_8) | p2least(X1_6)))). % 7.19/2.82 tff(c_68, plain, (![X1_47, X2_46, X3_45]: (~r(X1_47, X2_46) | ~r(X1_47, X3_45) | ~r1most(X1_47) | equalish(X3_45, X2_46)))). % 7.19/2.82 tff(c_20, plain, (![X1_13, X2_12, X3_11]: (~p(X1_13, X2_12) | ~p(X1_13, X3_11) | ~p1most(X1_13) | equalish(X3_11, X2_12)))). % 7.19/2.82 tff(c_76, plain, (![X1_53, X2_52, X3_51]: (~s(X1_53, X2_52) | ~s(X1_53, X3_51) | ~s1most(X1_53) | equalish(X3_51, X2_52)))). % 7.19/2.82 tff(c_8, plain, (![X1_3]: (~equalish(u1r2(X1_3), u1r1(X1_3)) | ~p2least(X1_3)))). % 7.19/2.82 tff(c_58, plain, (![X1_37]: (~equalish(u8r3(X1_37), u8r2(X1_37)) | ~t3least(X1_37)))). % 7.19/2.82 tff(c_54, plain, (![X1_35]: (~equalish(u8r2(X1_35), u8r1(X1_35)) | ~t3least(X1_35)))). % 7.19/2.82 tff(c_78, plain, (![X1_54]: (~equalish(u10r2(X1_54), u10r1(X1_54)) | s1most(X1_54)))). % 7.19/2.82 tff(c_70, plain, (![X1_48]: (~equalish(u9r2(X1_48), u9r1(X1_48)) | r1most(X1_48)))). % 7.19/2.82 tff(c_22, plain, (![X1_14]: (~equalish(u3r2(X1_14), u3r1(X1_14)) | p1most(X1_14)))). % 7.19/2.82 tff(c_56, plain, (![X1_36]: (~equalish(u8r3(X1_36), u8r1(X1_36)) | ~t3least(X1_36)))). % 7.19/2.82 tff(c_153, plain, (![X1_91]: (c(u9r2(X1_91)) | r1most(X1_91)))). % 7.19/2.82 tff(c_74, plain, (![X1_50]: (r(X1_50, u9r2(X1_50)) | r1most(X1_50)))). % 7.19/2.82 tff(c_12, plain, (![X1_5]: (~p2least(X1_5) | p(X1_5, u1r2(X1_5))))). % 7.19/2.82 tff(c_64, plain, (![X1_40]: (~t3least(X1_40) | t(X1_40, u8r3(X1_40))))). % 7.19/2.82 tff(c_40, plain, (![X1_26, X2_27]: (~s(X1_26, X2_27) | t(X1_26, X2_27)))). % 7.19/2.82 tff(c_62, plain, (![X1_39]: (~t3least(X1_39) | t(X1_39, u8r2(X1_39))))). % 7.19/2.82 tff(c_60, plain, (![X1_38]: (~t3least(X1_38) | t(X1_38, u8r1(X1_38))))). % 7.19/2.82 tff(c_24, plain, (![X1_15]: (p(X1_15, u3r1(X1_15)) | p1most(X1_15)))). % 7.19/2.82 tff(c_125, plain, (![X1_78]: (c(u9r1(X1_78)) | r1most(X1_78)))). % 7.19/2.82 tff(c_120, plain, (![X1_77]: (d(u10r1(X1_77)) | s1most(X1_77)))). % 7.19/2.82 tff(c_72, plain, (![X1_49]: (r(X1_49, u9r1(X1_49)) | r1most(X1_49)))). % 7.19/2.82 tff(c_80, plain, (![X1_55]: (s(X1_55, u10r1(X1_55)) | s1most(X1_55)))). % 7.19/2.82 tff(c_10, plain, (![X1_4]: (~p2least(X1_4) | p(X1_4, u1r1(X1_4))))). % 7.19/2.82 tff(c_36, plain, (![X1_22, X2_23]: (~r(X1_22, X2_23) | t(X1_22, X2_23)))). % 7.19/2.82 tff(c_26, plain, (![X1_16]: (p(X1_16, u3r2(X1_16)) | p1most(X1_16)))). % 7.19/2.82 tff(c_106, plain, (![X1_70]: (d(u10r2(X1_70)) | s1most(X1_70)))). % 7.19/2.82 tff(c_82, plain, (![X1_56]: (s(X1_56, u10r2(X1_56)) | s1most(X1_56)))). % 7.19/2.82 tff(c_34, plain, (![X1_21, X2_20]: (~r(X1_21, X2_20) | c(X2_20)))). % 7.19/2.82 tff(c_38, plain, (![X1_25, X2_24]: (~s(X1_25, X2_24) | d(X2_24)))). % 7.19/2.82 tff(c_42, plain, (![X1_28]: (~e(X1_28) | s1most(X1_28)))). % 7.19/2.82 tff(c_4, plain, (![X1_1]: (~c(X1_1) | p2least(X1_1)))). % 7.19/2.82 tff(c_44, plain, (![X1_29]: (~e(X1_29) | r1most(X1_29)))). % 7.19/2.82 tff(c_6, plain, (![X1_2]: (~p2least(X1_2) | c(X1_2)))). % 7.19/2.82 tff(c_16, plain, (![X1_9]: (~d(X1_9) | p1most(X1_9)))). % 7.19/2.82 tff(c_18, plain, (![X1_10]: (~p1most(X1_10) | d(X1_10)))). % 7.19/2.82 tff(c_46, plain, (![X1_30]: (~e(X1_30) | t3least(X1_30)))). % 7.19/2.82 tff(c_2, plain, (e(exist))). % 7.19/2.82 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.19/2.82 %------------------------------------------------------------------------------