%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN539+1 : TPTP v9.0.0. Released v2.1.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 10:03:51 PM UTC 2025 % Result : CounterSatisfiable 8.53s 2.88s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN539+1 : TPTP v9.0.0. Released v2.1.0. % 0.12/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.12/0.34 % Computer : n018.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 07:57:47 EDT 2025 % 0.12/0.34 % CPUTime : % 8.53/2.88 % 8.53/2.88 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.53/2.88 % 8.53/2.88 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.53/2.89 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a639 > a638 > a637 > a636 > a635 > a634 > a633 > a632 > a631 > a630 > a629 > a628 > a627 > a626 > a625 > a624 > a623 > a622 > a621 > a620 > a619 > a618 > a617 > a616 > a615 > a614 > a613 > a612 > a611 > a610 > a609 > a608 > a607 > a606 > a605 > a604 > a603 > a602 > a601 > a600 > a599 > a598 > a597 > a596 > a595 > a594 > a593 > a592 > a591 > a590 > a589 > a588 > a587 % 8.53/2.89 % 8.53/2.89 %Foreground sorts: % 8.53/2.89 % 8.53/2.89 % 8.53/2.89 %Background operators: % 8.53/2.89 % 8.53/2.89 % 8.53/2.89 %Foreground operators: % 8.53/2.89 tff(a601, type, a601: $i). % 8.53/2.89 tff(a600, type, a600: $i). % 8.53/2.89 tff(c4_0, type, c4_0: $o). % 8.53/2.89 tff(c3_0, type, c3_0: $o). % 8.53/2.89 tff(a594, type, a594: $i). % 8.53/2.89 tff(c1_2, type, c1_2: ($i * $i) > $o). % 8.53/2.89 tff(a627, type, a627: $i). % 8.53/2.89 tff(a624, type, a624: $i). % 8.53/2.89 tff(a613, type, a613: $i). % 8.53/2.89 tff(a628, type, a628: $i). % 8.53/2.89 tff(a629, type, a629: $i). % 8.53/2.89 tff(a620, type, a620: $i). % 8.53/2.89 tff(a596, type, a596: $i). % 8.53/2.89 tff(a619, type, a619: $i). % 8.53/2.89 tff(a621, type, a621: $i). % 8.53/2.89 tff(c5_0, type, c5_0: $o). % 8.53/2.89 tff(a616, type, a616: $i). % 8.53/2.89 tff(a599, type, a599: $i). % 8.53/2.89 tff(a638, type, a638: $i). % 8.53/2.89 tff(a602, type, a602: $i). % 8.53/2.89 tff(a606, type, a606: $i). % 8.53/2.89 tff(a626, type, a626: $i). % 8.53/2.89 tff(a617, type, a617: $i). % 8.53/2.89 tff(a636, type, a636: $i). % 8.53/2.89 tff(a605, type, a605: $i). % 8.53/2.89 tff(a611, type, a611: $i). % 8.53/2.89 tff(a598, type, a598: $i). % 8.53/2.89 tff(a614, type, a614: $i). % 8.53/2.89 tff(a612, type, a612: $i). % 8.53/2.89 tff(a589, type, a589: $i). % 8.53/2.89 tff(c1_0, type, c1_0: $o). % 8.53/2.89 tff(c2_1, type, c2_1: $i > $o). % 8.53/2.89 tff(ndr1_1, type, ndr1_1: $i > $o). % 8.53/2.89 tff(c2_0, type, c2_0: $o). % 8.53/2.89 tff(c4_1, type, c4_1: $i > $o). % 8.53/2.89 tff(a597, type, a597: $i). % 8.53/2.89 tff(a591, type, a591: $i). % 8.53/2.89 tff(a593, type, a593: $i). % 8.53/2.89 tff(a609, type, a609: $i). % 8.53/2.89 tff(a603, type, a603: $i). % 8.53/2.89 tff(a630, type, a630: $i). % 8.53/2.89 tff(a587, type, a587: $i). % 8.53/2.89 tff(a610, type, a610: $i). % 8.53/2.89 tff(a622, type, a622: $i). % 8.53/2.89 tff(a588, type, a588: $i). % 8.53/2.89 tff(a595, type, a595: $i). % 8.53/2.89 tff(ndr1_0, type, ndr1_0: $o). % 8.53/2.89 tff(a618, type, a618: $i). % 8.53/2.89 tff(a615, type, a615: $i). % 8.53/2.89 tff(c1_1, type, c1_1: $i > $o). % 8.53/2.89 tff(a607, type, a607: $i). % 8.53/2.89 tff(a625, type, a625: $i). % 8.53/2.89 tff(c5_2, type, c5_2: ($i * $i) > $o). % 8.53/2.89 tff(a634, type, a634: $i). % 8.53/2.89 tff(a631, type, a631: $i). % 8.53/2.89 tff(a608, type, a608: $i). % 8.53/2.89 tff(a632, type, a632: $i). % 8.53/2.89 tff(a590, type, a590: $i). % 8.53/2.89 tff(c4_2, type, c4_2: ($i * $i) > $o). % 8.53/2.89 tff(a623, type, a623: $i). % 8.53/2.89 tff(a639, type, a639: $i). % 8.53/2.89 tff(c5_1, type, c5_1: $i > $o). % 8.53/2.89 tff(c3_2, type, c3_2: ($i * $i) > $o). % 8.53/2.89 tff(a637, type, a637: $i). % 8.53/2.89 tff(c2_2, type, c2_2: ($i * $i) > $o). % 8.53/2.89 tff(a604, type, a604: $i). % 8.53/2.89 tff(a592, type, a592: $i). % 8.53/2.89 tff(a633, type, a633: $i). % 8.53/2.89 tff(a635, type, a635: $i). % 8.53/2.89 tff(c3_1, type, c3_1: $i > $o). % 8.53/2.89 % 8.53/2.89 %Saturated clause set: % 8.53/2.89 tff(c_2678, plain, (![X15_159, X16_160]: (c4_1(X15_159) | c2_2(X15_159, X16_160) | ~c2_1(X15_159) | c1_2(X15_159, a627) | ~c3_2(X15_159, X16_160) | ~c1_2(X15_159, X16_160) | ~c3_1(X15_159) | ~ndr1_1(X15_159) | ~c1_1(X15_159)))). % 8.53/2.89 tff(c_2625, plain, (![X15_26, X16_28]: (c1_2(X15_26, a627) | ~c3_2(X15_26, X16_28) | ~c1_2(X15_26, X16_28) | ~c3_1(X15_26) | c4_2(X15_26, X16_28) | ~ndr1_1(X15_26) | ~c1_1(X15_26)))). % 8.53/2.89 tff(c_2602, plain, (![X35_50, X36_52]: (c1_2(X35_50, a627) | ~c3_2(X35_50, X36_52) | ~c1_2(X35_50, X36_52) | ~c5_2(X35_50, X36_52) | ~ndr1_1(X35_50) | ~c3_1(X35_50)))). % 8.53/2.89 tff(c_2526, plain, (![X15_149, X16_150]: (c4_1(X15_149) | c2_2(X15_149, X16_150) | ~c2_1(X15_149) | ~c2_2(X15_149, a627) | ~c3_2(X15_149, X16_150) | ~c1_2(X15_149, X16_150) | ~c3_1(X15_149) | ~ndr1_1(X15_149) | ~c1_1(X15_149)))). % 8.53/2.89 tff(c_2473, plain, (![X15_145, X16_146]: (c4_1(X15_145) | ~c1_2(X15_145, X16_146) | ~c2_1(X15_145) | c2_2(X15_145, X16_146) | c1_2(X15_145, a595) | ~c3_1(X15_145) | ~ndr1_1(X15_145) | ~c1_1(X15_145)))). % 8.53/2.89 tff(c_2415, plain, (![X15_141, X16_142]: (c4_1(X15_141) | ~c1_2(X15_141, X16_142) | ~c2_1(X15_141) | ~c1_2(X15_141, a595) | c2_2(X15_141, X16_142) | ~c3_1(X15_141) | ~ndr1_1(X15_141) | ~c1_1(X15_141)))). % 8.53/2.89 tff(c_2280, plain, (![X15_134, X16_135]: (~c2_2(X15_134, a627) | ~c3_2(X15_134, X16_135) | ~c1_2(X15_134, X16_135) | ~c3_1(X15_134) | c4_2(X15_134, X16_135) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2333, plain, (![X15_136]: (c2_2(X15_136, a622) | ~c2_2(X15_136, a621) | ~c2_1(X15_136) | c1_2(X15_136, a595) | ~c3_1(X15_136) | ~ndr1_1(X15_136) | ~c1_1(X15_136)))). % 8.53/2.89 tff(c_2334, plain, (![X15_136]: (c2_2(X15_136, a622) | c1_2(X15_136, a621) | ~c2_1(X15_136) | c1_2(X15_136, a595) | ~c3_1(X15_136) | ~ndr1_1(X15_136) | ~c1_1(X15_136)))). % 8.53/2.89 tff(c_2432, plain, (![X15_134, X16_144]: (c2_2(X15_134, X16_144) | c4_2(X15_134, X16_144) | c1_2(X15_134, a595) | ~c3_1(X15_134) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2288, plain, (![X15_134, X16_135]: (~c4_2(X15_134, a595) | c2_2(X15_134, X16_135) | ~c3_1(X15_134) | c4_2(X15_134, X16_135) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2289, plain, (![X15_134, X16_135]: (~c1_2(X15_134, a595) | c2_2(X15_134, X16_135) | ~c3_1(X15_134) | c4_2(X15_134, X16_135) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2286, plain, (![X15_134]: (c2_2(X15_134, a600) | c2_1(X15_134) | ~c3_1(X15_134) | c4_2(X15_134, a599) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2287, plain, (![X15_134]: (~c3_2(X15_134, a600) | c2_1(X15_134) | ~c3_1(X15_134) | c4_2(X15_134, a599) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2285, plain, (![X15_134]: (c1_2(X15_134, a600) | c2_1(X15_134) | ~c3_1(X15_134) | c4_2(X15_134, a599) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2284, plain, (![X15_134, X16_135]: (c1_2(X15_134, X16_135) | ~c3_1(X15_134) | c4_2(X15_134, X16_135) | ~ndr1_1(X15_134) | ~c1_1(X15_134)))). % 8.53/2.89 tff(c_2290, plain, (~c1_1(a629))). % 8.53/2.89 tff(c_2251, plain, (![X15_26, X16_28]: (~c3_1(X15_26) | c4_2(X15_26, X16_28) | c5_2(X15_26, X16_28) | ~ndr1_1(X15_26) | ~c1_1(X15_26)))). % 8.53/2.89 tff(c_2246, plain, (~c2_1(a596))). % 8.53/2.90 tff(c_2204, plain, (![X2_10]: (~c1_2(a596, X2_10) | ~c4_2(a596, X2_10) | c3_2(a596, X2_10)))). % 8.53/2.90 tff(c_1788, plain, (~c3_1(a608))). % 8.53/2.90 tff(c_1787, plain, (~c1_1(a608))). % 8.53/2.90 tff(c_1761, plain, (c5_2(a608, a609))). % 8.53/2.90 tff(c_1759, plain, (~c4_2(a608, a609))). % 8.53/2.90 tff(c_1629, plain, (![X29_42]: (c4_1(X29_42) | ~c1_2(X29_42, a621) | c2_2(X29_42, a621) | ~c4_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1628, plain, (![X29_42]: (c4_1(X29_42) | ~c1_2(X29_42, a621) | c2_2(X29_42, a621) | ~c1_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1755, plain, (c1_1(a594))). % 8.53/2.90 tff(c_1753, plain, (c3_2(a624, a625))). % 8.53/2.90 tff(c_1749, plain, (~c1_2(a624, a625))). % 8.53/2.90 tff(c_1746, plain, (~c1_1(a624))). % 8.53/2.90 tff(c_1721, plain, (c5_2(a624, a626))). % 8.53/2.90 tff(c_1716, plain, (~c3_2(a624, a626))). % 8.53/2.90 tff(c_1710, plain, (~c2_1(a624))). % 8.53/2.90 tff(c_1701, plain, (c4_2(a624, a626))). % 8.53/2.90 tff(c_1697, plain, (ndr1_1(a608))). % 8.53/2.90 tff(c_1696, plain, (~c2_2(a629, a630))). % 8.53/2.90 tff(c_1671, plain, (![X35_50, X36_52]: (~c2_2(X35_50, a627) | ~c3_2(X35_50, X36_52) | ~c1_2(X35_50, X36_52) | ~c5_2(X35_50, X36_52) | ~ndr1_1(X35_50) | ~c3_1(X35_50)))). % 8.53/2.90 tff(c_1674, plain, (~c5_2(a629, a630))). % 8.53/2.90 tff(c_1669, plain, (~c2_2(a624, a625))). % 8.53/2.90 tff(c_1659, plain, (ndr1_1(a624))). % 8.53/2.90 tff(c_1650, plain, (ndr1_1(a629))). % 8.53/2.90 tff(c_1647, plain, (~c2_1(a629))). % 8.53/2.90 tff(c_1643, plain, (c3_1(a629))). % 8.53/2.90 tff(c_1635, plain, (![X29_104]: (c4_1(X29_104) | ~c1_2(X29_104, a621) | ~ndr1_1(X29_104) | ~c1_2(X29_104, a622) | ~c2_1(X29_104)))). % 8.53/2.90 tff(c_1605, plain, (![X30_43, X31_45]: (c4_1(X30_43) | ~c4_2(X30_43, X31_45) | ~c1_2(X30_43, X31_45) | c2_2(X30_43, X31_45) | ~ndr1_1(X30_43) | ~c2_1(X30_43)))). % 8.53/2.90 tff(c_1602, plain, (c1_2(a596, a598))). % 8.53/2.90 tff(c_1598, plain, (c2_2(a596, a598))). % 8.53/2.90 tff(c_1586, plain, (![X3_11]: (~c3_2(X3_11, a599) | ~c3_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1582, plain, (![X3_11]: (c2_2(X3_11, a599) | ~c3_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1577, plain, (~c2_1(a634))). % 8.53/2.90 tff(c_1569, plain, (![X29_42]: (~c1_1(X29_42) | c1_2(X29_42, a622) | c4_2(X29_42, a622) | ~ndr1_1(X29_42) | c1_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1573, plain, (![X3_11]: (c2_2(X3_11, a599) | c1_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1568, plain, (![X29_42]: (~c1_1(X29_42) | c1_2(X29_42, a622) | c4_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c2_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1567, plain, (![X29_42]: (~c1_1(X29_42) | c1_2(X29_42, a622) | c4_2(X29_42, a622) | ~ndr1_1(X29_42) | c4_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1549, plain, (![X6_14, X7_16]: (~c1_1(X6_14) | ~c5_2(X6_14, X7_16) | c1_2(X6_14, X7_16) | c4_2(X6_14, X7_16) | ~ndr1_1(X6_14)))). % 8.53/2.90 tff(c_1547, plain, (~c2_2(a596, a597))). % 8.53/2.90 tff(c_1544, plain, (~c1_2(a596, a597))). % 8.53/2.90 tff(c_1541, plain, (~c4_2(a596, a598))). % 8.53/2.90 tff(c_1538, plain, (![X3_11]: (~c5_2(X3_11, a599) | c1_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1536, plain, (~c1_1(a596))). % 8.53/2.90 tff(c_1522, plain, (![X3_11]: (~c3_2(X3_11, a599) | c1_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1520, plain, (c5_2(a596, a597))). % 8.53/2.90 tff(c_1517, plain, (![X3_11]: (c2_2(X3_11, a599) | c2_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1514, plain, (![X3_11]: (~c3_2(X3_11, a599) | c2_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1511, plain, (![X3_11]: (~c5_2(X3_11, a599) | c2_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1509, plain, (ndr1_1(a593))). % 8.53/2.90 tff(c_1451, plain, (![X29_42]: (~c4_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | ~c2_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1452, plain, (![X29_42]: (~c4_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | c1_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1489, plain, (![X3_11]: (~c5_2(X3_11, a599) | ~c3_2(X3_11, a600) | c2_1(X3_11)))). % 8.53/2.90 tff(c_1438, plain, (![X29_42]: (~c1_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | ~c2_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1437, plain, (![X29_42]: (~c1_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | c4_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1439, plain, (![X29_42]: (~c1_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | c1_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1450, plain, (![X29_42]: (~c4_2(X29_42, a595) | c2_2(X29_42, a622) | ~ndr1_1(X29_42) | ~c1_1(X29_42) | c4_2(X29_42, a621) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1476, plain, (~c3_1(a593))). % 8.53/2.90 tff(c_1472, plain, (~c5_1(a593))). % 8.53/2.90 tff(c_1463, plain, (ndr1_1(a596))). % 8.53/2.90 tff(c_1460, plain, (c4_1(a594))). % 8.53/2.90 tff(c_1457, plain, (c2_1(a593))). % 8.53/2.90 tff(c_1455, plain, (![X21_33]: (c5_1(X21_33) | ~c3_1(X21_33)))). % 8.53/2.90 tff(c_1244, plain, (![X_4, Y_6]: (~c4_2(X_4, a595) | ~c5_2(X_4, Y_6) | c2_2(X_4, Y_6) | ~ndr1_1(X_4) | ~c1_1(X_4)))). % 8.53/2.90 tff(c_1246, plain, (![X_4, Y_6]: (~c1_2(X_4, a595) | ~c5_2(X_4, Y_6) | c2_2(X_4, Y_6) | ~ndr1_1(X_4) | ~c1_1(X_4)))). % 8.53/2.90 tff(c_1422, plain, (![X29_42]: (c4_2(X29_42, a621) | c5_2(X29_42, a622) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1402, plain, (![X29_42]: (~c2_2(X29_42, a621) | c5_2(X29_42, a622) | ~c2_1(X29_42)))). % 8.53/2.90 tff(c_1385, plain, (ndr1_1(a592))). % 8.53/2.90 tff(c_1371, plain, (![X29_42]: (~c2_2(X29_42, a621) | ~c1_2(X29_42, a622) | ~c2_1(X29_42)))). % 8.53/2.91 tff(c_1368, plain, (![X29_42]: (c4_2(X29_42, a621) | ~c1_2(X29_42, a622) | ~c2_1(X29_42)))). % 8.53/2.91 tff(c_1354, plain, (![X3_11]: (ndr1_1(X3_11) | c2_1(X3_11)))). % 8.53/2.91 tff(c_1351, plain, (![X29_42]: (c1_2(X29_42, a621) | ~c1_2(X29_42, a622) | ~c2_1(X29_42)))). % 8.53/2.91 tff(c_1339, plain, (![X29_42]: (c1_2(X29_42, a621) | c5_2(X29_42, a622) | ~c2_1(X29_42)))). % 8.53/2.91 tff(c_1323, plain, (~c4_2(a613, a614))). % 8.53/2.91 tff(c_1315, plain, (~c3_2(a613, a614))). % 8.53/2.91 tff(c_1312, plain, (c1_2(a613, a614))). % 8.53/2.91 tff(c_1305, plain, (ndr1_1(a613))). % 8.53/2.91 tff(c_1300, plain, (![X29_42]: (ndr1_1(X29_42) | ~c2_1(X29_42)))). % 8.53/2.91 tff(c_1294, plain, (~c3_1(a613))). % 8.53/2.91 tff(c_1291, plain, (~c3_1(a592))). % 8.53/2.91 tff(c_1290, plain, (~c4_1(a592))). % 8.53/2.91 tff(c_1279, plain, (~c2_0)). % 8.53/2.91 tff(c_1271, plain, (c3_0)). % 8.53/2.91 tff(c_1270, plain, (c4_1(a619))). % 8.53/2.91 tff(c_1269, plain, (c1_1(a631))). % 8.53/2.91 tff(c_1267, plain, (c5_1(a619))). % 8.53/2.91 tff(c_1264, plain, (~c2_1(a637))). % 8.53/2.91 tff(c_1262, plain, (c1_1(a619))). % 8.53/2.91 tff(c_1259, plain, (~c1_0)). % 8.53/2.91 tff(c_1258, plain, (~c3_1(a637))). % 8.53/2.91 tff(c_1257, plain, (~c3_1(a631))). % 8.53/2.91 tff(c_1255, plain, (c4_0)). % 8.53/2.91 tff(c_2, plain, (c5_0)). % 8.53/2.91 tff(c_692, plain, (ndr1_0)). % 8.53/2.91 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.53/2.91 %------------------------------------------------------------------------------