%------------------------------------------------------------------------------ % 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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n026.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 : Satisfiable 7.96s 2.66s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYN539-1 : TPTP v9.0.0. Released v2.1.0. % 0.03/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n026.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Apr 9 07:57:53 EDT 2025 % 0.13/0.33 % CPUTime : % 7.96/2.66 % 7.96/2.66 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.96/2.66 % 7.96/2.66 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.02/2.67 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP3 > ssSkP2 > ssSkP1 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > 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 > a605 > a604 > a603 > a602 > a601 > a600 > a599 > a598 > a597 > a596 > a595 > a594 > a593 > a592 > a591 > a590 > a589 > a588 > a587 % 8.02/2.67 % 8.02/2.67 %Foreground sorts: % 8.02/2.67 % 8.02/2.67 % 8.02/2.67 %Background operators: % 8.02/2.67 % 8.02/2.67 % 8.02/2.67 %Foreground operators: % 8.02/2.67 tff(a601, type, a601: $i). % 8.02/2.67 tff(ssSkC7, type, ssSkC7: $o). % 8.02/2.67 tff(a600, type, a600: $i). % 8.02/2.67 tff(c4_0, type, c4_0: $o). % 8.02/2.67 tff(ssSkP0, type, ssSkP0: $i > $o). % 8.02/2.67 tff(ssSkC6, type, ssSkC6: $o). % 8.02/2.67 tff(c3_0, type, c3_0: $o). % 8.02/2.67 tff(a594, type, a594: $i). % 8.02/2.67 tff(c1_2, type, c1_2: ($i * $i) > $o). % 8.02/2.67 tff(ssSkC3, type, ssSkC3: $o). % 8.02/2.67 tff(a627, type, a627: $i). % 8.02/2.67 tff(a624, type, a624: $i). % 8.02/2.67 tff(a613, type, a613: $i). % 8.02/2.67 tff(ssSkP2, type, ssSkP2: $i > $o). % 8.02/2.67 tff(a628, type, a628: $i). % 8.02/2.67 tff(a629, type, a629: $i). % 8.02/2.67 tff(a620, type, a620: $i). % 8.02/2.67 tff(a596, type, a596: $i). % 8.02/2.67 tff(a619, type, a619: $i). % 8.02/2.67 tff(ssSkC4, type, ssSkC4: $o). % 8.02/2.67 tff(a621, type, a621: $i). % 8.02/2.67 tff(c5_0, type, c5_0: $o). % 8.02/2.67 tff(a616, type, a616: $i). % 8.02/2.67 tff(a599, type, a599: $i). % 8.02/2.67 tff(a638, type, a638: $i). % 8.02/2.67 tff(a602, type, a602: $i). % 8.02/2.67 tff(a626, type, a626: $i). % 8.02/2.67 tff(a617, type, a617: $i). % 8.02/2.67 tff(a636, type, a636: $i). % 8.02/2.67 tff(a605, type, a605: $i). % 8.02/2.67 tff(a611, type, a611: $i). % 8.02/2.67 tff(a598, type, a598: $i). % 8.02/2.67 tff(a614, type, a614: $i). % 8.02/2.67 tff(ssSkP3, type, ssSkP3: $i > $o). % 8.02/2.67 tff(a612, type, a612: $i). % 8.02/2.67 tff(a589, type, a589: $i). % 8.02/2.67 tff(c1_0, type, c1_0: $o). % 8.02/2.67 tff(c2_1, type, c2_1: $i > $o). % 8.02/2.67 tff(ndr1_1, type, ndr1_1: $i > $o). % 8.02/2.67 tff(c2_0, type, c2_0: $o). % 8.02/2.67 tff(c4_1, type, c4_1: $i > $o). % 8.02/2.67 tff(a597, type, a597: $i). % 8.02/2.67 tff(a591, type, a591: $i). % 8.02/2.67 tff(a593, type, a593: $i). % 8.02/2.67 tff(a609, type, a609: $i). % 8.02/2.67 tff(a603, type, a603: $i). % 8.02/2.67 tff(a630, type, a630: $i). % 8.02/2.67 tff(a587, type, a587: $i). % 8.02/2.67 tff(a610, type, a610: $i). % 8.02/2.67 tff(a622, type, a622: $i). % 8.02/2.67 tff(a588, type, a588: $i). % 8.02/2.67 tff(a595, type, a595: $i). % 8.02/2.67 tff(ndr1_0, type, ndr1_0: $o). % 8.02/2.67 tff(a618, type, a618: $i). % 8.02/2.67 tff(a615, type, a615: $i). % 8.02/2.67 tff(c1_1, type, c1_1: $i > $o). % 8.02/2.67 tff(ssSkC2, type, ssSkC2: $o). % 8.02/2.67 tff(a625, type, a625: $i). % 8.02/2.67 tff(c5_2, type, c5_2: ($i * $i) > $o). % 8.02/2.67 tff(a634, type, a634: $i). % 8.02/2.67 tff(a631, type, a631: $i). % 8.02/2.67 tff(a608, type, a608: $i). % 8.02/2.67 tff(a632, type, a632: $i). % 8.02/2.67 tff(a590, type, a590: $i). % 8.02/2.67 tff(c4_2, type, c4_2: ($i * $i) > $o). % 8.02/2.67 tff(a623, type, a623: $i). % 8.02/2.67 tff(a639, type, a639: $i). % 8.02/2.67 tff(ssSkC1, type, ssSkC1: $o). % 8.02/2.67 tff(ssSkC0, type, ssSkC0: $o). % 8.02/2.67 tff(ssSkC5, type, ssSkC5: $o). % 8.02/2.67 tff(ssSkP1, type, ssSkP1: $i > $o). % 8.02/2.67 tff(c5_1, type, c5_1: $i > $o). % 8.02/2.67 tff(c3_2, type, c3_2: ($i * $i) > $o). % 8.02/2.67 tff(a637, type, a637: $i). % 8.02/2.67 tff(c2_2, type, c2_2: ($i * $i) > $o). % 8.02/2.67 tff(a604, type, a604: $i). % 8.02/2.67 tff(a592, type, a592: $i). % 8.02/2.67 tff(a633, type, a633: $i). % 8.02/2.67 tff(a635, type, a635: $i). % 8.02/2.67 tff(c3_1, type, c3_1: $i > $o). % 8.02/2.67 % 8.02/2.67 %Saturated clause set: % 8.02/2.68 tff(c_1100, plain, (![U_10, V_213]: (c2_2(U_10, V_213) | ~c1_1(U_10) | c2_1(U_10) | c3_2(U_10, V_213) | ~c3_2(U_10, a632) | ~c1_2(U_10, V_213) | c2_2(U_10, a636) | c1_2(U_10, a599) | ~ndr1_1(U_10) | ~c2_2(U_10, a595) | ssSkP0(U_10)))). % 8.02/2.68 tff(c_1102, plain, (![U_10, V_213]: (c2_2(U_10, V_213) | ~c1_1(U_10) | c2_1(U_10) | c3_2(U_10, V_213) | ~c3_2(U_10, a632) | ~c1_2(U_10, V_213) | c1_2(U_10, a599) | ~c3_2(U_10, a636) | ~ndr1_1(U_10) | ~c2_2(U_10, a595) | ssSkP0(U_10)))). % 8.02/2.68 tff(c_1049, plain, (![U_10, V_207]: (c2_2(U_10, V_207) | ~c1_1(U_10) | c2_1(U_10) | c3_2(U_10, V_207) | ~c2_2(U_10, a632) | ~c1_2(U_10, V_207) | c1_2(U_10, a599) | ~c3_2(U_10, a636) | ~ndr1_1(U_10) | ~c2_2(U_10, a595) | ssSkP0(U_10)))). % 8.02/2.68 tff(c_1047, plain, (![U_10, V_207]: (c2_2(U_10, V_207) | ~c1_1(U_10) | c2_1(U_10) | c3_2(U_10, V_207) | ~c2_2(U_10, a632) | ~c1_2(U_10, V_207) | c2_2(U_10, a636) | c1_2(U_10, a599) | ~ndr1_1(U_10) | ~c2_2(U_10, a595) | ssSkP0(U_10)))). % 8.02/2.68 tff(c_913, plain, (![U_10, V_196]: (c2_2(U_10, V_196) | c4_2(U_10, V_196) | ~c3_1(U_10) | ~c1_1(U_10) | c1_2(U_10, a599) | ~c3_2(U_10, a636) | ~ndr1_1(U_10) | ~c2_2(U_10, a595) | ssSkP0(U_10)))). % 8.02/2.68 tff(c_993, plain, (![U_201, V_191]: (c2_2(U_201, V_191) | c4_2(U_201, V_191) | ~c3_1(U_201) | ~c1_1(U_201) | c2_2(U_201, a636) | c1_2(U_201, a599) | ~ndr1_1(U_201) | ~c2_2(U_201, a595) | ssSkP0(U_201)))). % 8.02/2.68 tff(c_1354, plain, (![U_229]: (~c1_1(U_229) | c3_1(U_229) | ~c5_1(U_229) | c2_2(U_229, a636) | c1_2(U_229, a599) | ~ndr1_1(U_229) | ~c2_2(U_229, a595) | ssSkP0(U_229)))). % 8.02/2.68 tff(c_796, plain, (![U_188]: (c2_2(U_188, a639) | ~c1_1(U_188) | c3_1(U_188) | ~c5_1(U_188) | c1_2(U_188, a599) | ~c3_2(U_188, a636) | ~ndr1_1(U_188) | ~c2_2(U_188, a595) | ssSkP0(U_188)))). % 8.02/2.68 tff(c_1305, plain, (![U_225]: (c1_2(U_225, a603) | ~c3_2(U_225, a636) | ~c2_2(U_225, a603) | ~c1_1(U_225) | ~c1_2(U_225, a595) | ~ndr1_1(U_225) | ssSkP2(U_225)))). % 8.02/2.68 tff(c_755, plain, (![U_7, V_187]: (c1_2(U_7, a603) | c4_2(U_7, V_187) | ~c3_2(U_7, a636) | ~c2_2(U_7, V_187) | ~c1_1(U_7) | ~c1_2(U_7, a595) | ~ndr1_1(U_7) | ssSkP2(U_7)))). % 8.02/2.68 tff(c_1234, plain, (![U_222]: (c2_2(U_222, a636) | c1_2(U_222, a603) | ~c2_2(U_222, a603) | ~c1_1(U_222) | ~c1_2(U_222, a595) | ~ndr1_1(U_222) | ssSkP2(U_222)))). % 8.02/2.68 tff(c_937, plain, (![U_7, V_200]: (c2_2(U_7, a636) | c1_2(U_7, a603) | c4_2(U_7, V_200) | ~c2_2(U_7, V_200) | ~c1_1(U_7) | ~c1_2(U_7, a595) | ~ndr1_1(U_7) | ssSkP2(U_7)))). % 8.02/2.68 tff(c_695, plain, (![U_83, V_84]: (c1_1(U_83) | c4_2(U_83, a617) | c2_2(U_83, V_84) | c2_1(U_83) | c3_2(U_83, V_84) | ~c2_2(U_83, a632) | ~ndr1_1(U_83) | ~c1_2(U_83, V_84)))). % 8.02/2.68 tff(c_731, plain, (![U_182, V_183]: (c1_1(U_182) | c4_2(U_182, a617) | c2_2(U_182, V_183) | c2_1(U_182) | c3_2(U_182, V_183) | ~c3_2(U_182, a632) | ~ndr1_1(U_182) | ~c1_2(U_182, V_183)))). % 8.02/2.68 tff(c_655, plain, (![U_83, V_84]: (c1_1(U_83) | c2_2(U_83, V_84) | ~c1_2(U_83, a617) | c2_1(U_83) | c3_2(U_83, V_84) | ~c2_2(U_83, a632) | ~ndr1_1(U_83) | ~c1_2(U_83, V_84)))). % 8.02/2.68 tff(c_732, plain, (![U_182, V_183]: (c1_1(U_182) | c2_2(U_182, V_183) | ~c1_2(U_182, a617) | c2_1(U_182) | c3_2(U_182, V_183) | ~c3_2(U_182, a632) | ~ndr1_1(U_182) | ~c1_2(U_182, V_183)))). % 8.02/2.68 tff(c_734, plain, (![U_182, V_183]: (c2_2(U_182, V_183) | ~c1_1(U_182) | ~c4_2(U_182, a595) | c2_1(U_182) | c3_2(U_182, V_183) | ~c3_2(U_182, a632) | ~ndr1_1(U_182) | ~c1_2(U_182, V_183)))). % 8.02/2.68 tff(c_625, plain, (![U_172, V_173]: (c2_2(U_172, V_173) | ~c1_1(U_172) | ~c1_2(U_172, a595) | c2_1(U_172) | c3_2(U_172, V_173) | ~c2_2(U_172, a632) | ~ndr1_1(U_172) | ~c1_2(U_172, V_173)))). % 8.02/2.68 tff(c_733, plain, (![U_182, V_183]: (c2_2(U_182, V_183) | ~c1_1(U_182) | ~c1_2(U_182, a595) | c2_1(U_182) | c3_2(U_182, V_183) | ~c3_2(U_182, a632) | ~ndr1_1(U_182) | ~c1_2(U_182, V_183)))). % 8.02/2.68 tff(c_626, plain, (![U_172, V_173]: (c2_2(U_172, V_173) | ~c1_1(U_172) | ~c4_2(U_172, a595) | c2_1(U_172) | c3_2(U_172, V_173) | ~c2_2(U_172, a632) | ~ndr1_1(U_172) | ~c1_2(U_172, V_173)))). % 8.02/2.68 tff(c_1034, plain, (c1_0)). % 8.02/2.68 tff(c_797, plain, (![U_188]: (c2_2(U_188, a603) | ~c1_1(U_188) | ssSkP2(U_188) | c1_2(U_188, a599) | ~c3_2(U_188, a636) | ~ndr1_1(U_188) | ~c2_2(U_188, a595) | ssSkP0(U_188)))). % 8.02/2.68 tff(c_995, plain, (![U_201]: (c2_2(U_201, a603) | ~c1_1(U_201) | ssSkP2(U_201) | c2_2(U_201, a636) | c1_2(U_201, a599) | ~ndr1_1(U_201) | ~c2_2(U_201, a595) | ssSkP0(U_201)))). % 8.02/2.68 tff(c_1008, plain, (![U_201]: (ssSkP2(U_201) | c2_2(U_201, a636) | c1_2(U_201, a599) | ~ndr1_1(U_201) | ~c2_2(U_201, a603) | ssSkP0(U_201)))). % 8.02/2.68 tff(c_945, plain, (![U_10, V_200]: (c2_2(U_10, a636) | c1_2(U_10, a599) | c4_2(U_10, V_200) | ~ndr1_1(U_10) | ~c2_2(U_10, V_200) | ssSkP0(U_10)))). % 8.02/2.68 tff(c_948, plain, (c2_2(a588, a636))). % 8.02/2.68 tff(c_924, plain, (![U_119, W_121, V_120]: (c2_2(U_119, a636) | c1_2(U_119, W_121) | c4_2(U_119, V_120) | ~c2_2(U_119, W_121) | ~ndr1_1(U_119) | ~c2_2(U_119, V_120)))). % 8.02/2.68 tff(c_810, plain, (![U_188]: (ssSkP2(U_188) | c1_2(U_188, a599) | ~c3_2(U_188, a636) | ~ndr1_1(U_188) | ~c2_2(U_188, a603) | ssSkP0(U_188)))). % 8.02/2.68 tff(c_921, plain, (~c5_1(a605))). % 8.02/2.68 tff(c_916, plain, (~ndr1_1(a605))). % 8.02/2.68 tff(c_846, plain, (![U_190, V_191]: (c2_2(U_190, V_191) | ~c4_2(U_190, a595) | c4_2(U_190, V_191) | ~c3_1(U_190) | ~c1_1(U_190) | ~ndr1_1(U_190)))). % 8.02/2.68 tff(c_845, plain, (![U_190, V_191]: (c2_2(U_190, V_191) | ~c1_2(U_190, a595) | c4_2(U_190, V_191) | ~c3_1(U_190) | ~c1_1(U_190) | ~ndr1_1(U_190)))). % 8.02/2.68 tff(c_847, plain, (![U_190]: (ssSkP0(U_190) | c4_2(U_190, a599) | ~c3_1(U_190) | ~c1_1(U_190) | ~ndr1_1(U_190)))). % 8.02/2.68 tff(c_823, plain, (![U_91, V_92]: (c4_2(U_91, V_92) | c5_2(U_91, V_92) | ~c3_1(U_91) | ~c1_1(U_91) | ~ndr1_1(U_91)))). % 8.02/2.68 tff(c_825, plain, (~c2_2(a624, a595))). % 8.02/2.68 tff(c_824, plain, (~c2_2(a637, a638))). % 8.02/2.69 tff(c_820, plain, (~c2_2(a608, a609))). % 8.02/2.69 tff(c_819, plain, (~c2_2(a608, a595))). % 8.02/2.69 tff(c_763, plain, (![U_10, V_187]: (c1_2(U_10, a599) | c4_2(U_10, V_187) | ~c3_2(U_10, a636) | ~ndr1_1(U_10) | ~c2_2(U_10, V_187) | ssSkP0(U_10)))). % 8.02/2.69 tff(c_764, plain, (~c3_2(a588, a636))). % 8.02/2.69 tff(c_742, plain, (![U_133, W_135, V_134]: (c1_2(U_133, W_135) | c4_2(U_133, V_134) | ~c3_2(U_133, a636) | ~c2_2(U_133, W_135) | ~ndr1_1(U_133) | ~c2_2(U_133, V_134)))). % 8.02/2.69 tff(c_735, plain, (![U_182]: (ssSkP0(U_182) | c2_1(U_182) | c3_2(U_182, a599) | ~c3_2(U_182, a632) | ~ndr1_1(U_182) | ~c1_2(U_182, a599)))). % 8.02/2.69 tff(c_713, plain, (![U_85, V_86]: (c2_1(U_85) | c5_2(U_85, V_86) | c3_2(U_85, V_86) | ~c3_2(U_85, a632) | ~ndr1_1(U_85) | ~c1_2(U_85, V_86)))). % 8.02/2.69 tff(c_701, plain, (![U_7]: (c1_1(U_7) | c4_2(U_7, a617) | c2_2(U_7, a603) | ~ndr1_1(U_7) | ~c1_2(U_7, a603) | ssSkP2(U_7)))). % 8.02/2.69 tff(c_675, plain, (![U_89, V_90]: (c1_1(U_89) | c4_2(U_89, a617) | c2_2(U_89, V_90) | ~ndr1_1(U_89) | ~c1_2(U_89, V_90) | ~c5_2(U_89, V_90)))). % 8.02/2.69 tff(c_661, plain, (![U_7]: (c1_1(U_7) | c2_2(U_7, a603) | ~c1_2(U_7, a617) | ~ndr1_1(U_7) | ~c1_2(U_7, a603) | ssSkP2(U_7)))). % 8.02/2.69 tff(c_672, plain, (~c1_2(a608, a609))). % 8.02/2.69 tff(c_669, plain, (~c1_2(a624, a626))). % 8.02/2.69 tff(c_668, plain, (~c1_2(a588, a591))). % 8.02/2.69 tff(c_635, plain, (![U_98, V_99]: (c1_1(U_98) | c2_2(U_98, V_99) | ~c1_2(U_98, a617) | ~ndr1_1(U_98) | ~c1_2(U_98, V_99) | ~c5_2(U_98, V_99)))). % 8.02/2.69 tff(c_632, plain, (![U_174]: (ssSkP0(U_174) | c2_1(U_174) | ~c2_2(U_174, a632) | ~ndr1_1(U_174) | ~c1_2(U_174, a599)))). % 8.02/2.69 tff(c_613, plain, (![U_83, V_84]: (c2_1(U_83) | c5_2(U_83, V_84) | c3_2(U_83, V_84) | ~c2_2(U_83, a632) | ~ndr1_1(U_83) | ~c1_2(U_83, V_84)))). % 8.02/2.69 tff(c_608, plain, (ssSkC5)). % 8.02/2.69 tff(c_534, plain, (![U_20]: (c2_2(U_20, a639) | ~c1_1(U_20) | ~c4_2(U_20, a595) | ~ndr1_1(U_20) | c3_1(U_20) | ~c5_1(U_20)))). % 8.02/2.69 tff(c_588, plain, (![U_169]: (~c1_1(U_169) | ~c1_2(U_169, a595) | ~ndr1_1(U_169) | c3_1(U_169) | ~c5_1(U_169)))). % 8.02/2.69 tff(c_591, plain, (~ssSkC7)). % 8.02/2.69 tff(c_567, plain, (![U_7]: (c2_2(U_7, a603) | ~c1_1(U_7) | ~c1_2(U_7, a595) | ~ndr1_1(U_7) | ssSkP2(U_7)))). % 8.02/2.69 tff(c_535, plain, (![U_7]: (c2_2(U_7, a603) | ~c1_1(U_7) | ~c4_2(U_7, a595) | ~ndr1_1(U_7) | ssSkP2(U_7)))). % 8.02/2.69 tff(c_579, plain, (~c1_2(a608, a595))). % 8.02/2.69 tff(c_578, plain, (~c1_2(a624, a595))). % 8.02/2.69 tff(c_575, plain, (~c4_2(a608, a595))). % 8.02/2.69 tff(c_574, plain, (~c1_2(a588, a595))). % 8.02/2.69 tff(c_545, plain, (![U_81, V_82]: (c2_2(U_81, V_82) | ~c1_1(U_81) | ~c1_2(U_81, a595) | ~ndr1_1(U_81) | ~c5_2(U_81, V_82)))). % 8.02/2.69 tff(c_543, plain, (~c4_2(a624, a595))). % 8.02/2.69 tff(c_542, plain, (~c4_2(a588, a595))). % 8.02/2.69 tff(c_513, plain, (![U_79, V_80]: (c2_2(U_79, V_80) | ~c1_1(U_79) | ~c4_2(U_79, a595) | ~ndr1_1(U_79) | ~c5_2(U_79, V_80)))). % 8.02/2.69 tff(c_509, plain, (ssSkC4)). % 8.02/2.69 tff(c_506, plain, (~c5_1(a592))). % 8.02/2.69 tff(c_500, plain, (~ndr1_1(a592))). % 8.02/2.69 tff(c_493, plain, (~c1_2(a588, a589))). % 8.02/2.69 tff(c_494, plain, (~ndr1_1(a593))). % 8.02/2.69 tff(c_490, plain, (c1_2(a588, a590))). % 8.02/2.69 tff(c_487, plain, (~c2_2(a588, a591))). % 8.02/2.69 tff(c_484, plain, (c5_2(a588, a591))). % 8.02/2.69 tff(c_481, plain, (c3_2(a588, a589))). % 8.02/2.69 tff(c_478, plain, (c2_2(a588, a589))). % 8.02/2.69 tff(c_471, plain, (~c4_2(a588, a590))). % 8.02/2.69 tff(c_468, plain, (c2_2(a588, a590))). % 8.02/2.69 tff(c_447, plain, (ndr1_1(a588))). % 8.02/2.69 tff(c_439, plain, (![U_27]: (c3_1(U_27) | ~c5_1(U_27) | ~c1_2(U_27, a639)))). % 8.02/2.69 tff(c_435, plain, (![U_28]: (c3_1(U_28) | ~c5_1(U_28) | ~c2_2(U_28, a639)))). % 8.02/2.69 tff(c_424, plain, (![U_20]: (c3_1(U_20) | c5_2(U_20, a639) | ~c5_1(U_20)))). % 8.02/2.69 tff(c_417, plain, (c2_0)). % 8.02/2.69 tff(c_414, plain, (ssSkC3)). % 8.02/2.69 tff(c_407, plain, (ssSkC2)). % 8.02/2.69 tff(c_403, plain, (![U_17]: (c3_1(U_17) | ndr1_1(U_17) | ~c5_1(U_17)))). % 8.02/2.69 tff(c_120, plain, (![U_11]: (ssSkP3(U_11) | ~c2_2(U_11, a621)))). % 8.02/2.69 tff(c_128, plain, (![U_14]: (ssSkP0(U_14) | ~c3_2(U_14, a599)))). % 8.02/2.69 tff(c_70, plain, (![U_5]: (ssSkP3(U_5) | c1_2(U_5, a621)))). % 8.02/2.69 tff(c_82, plain, (![U_10]: (ssSkP0(U_10) | c2_2(U_10, a599)))). % 8.02/2.69 tff(c_80, plain, (![U_9]: (ssSkP1(U_9) | c3_2(U_9, a602)))). % 8.02/2.69 tff(c_126, plain, (![U_13]: (ssSkP1(U_13) | ~c2_2(U_13, a602)))). % 8.02/2.69 tff(c_124, plain, (![U_12]: (ssSkP2(U_12) | ~c4_2(U_12, a603)))). % 8.02/2.69 tff(c_130, plain, (![U_15]: (ssSkP0(U_15) | ~c5_2(U_15, a599)))). % 8.02/2.69 tff(c_72, plain, (![U_6]: (ssSkP3(U_6) | c4_2(U_6, a621)))). % 8.02/2.69 tff(c_78, plain, (![U_8]: (ssSkP2(U_8) | c3_2(U_8, a603)))). % 8.02/2.69 tff(c_76, plain, (![U_7]: (ssSkP2(U_7) | c5_2(U_7, a603)))). % 8.02/2.69 tff(c_387, plain, (c4_2(a624, a626))). % 8.02/2.69 tff(c_386, plain, (c5_2(a624, a626))). % 8.02/2.69 tff(c_384, plain, (c5_2(a608, a609))). % 8.02/2.69 tff(c_385, plain, (~c4_2(a637, a638))). % 8.02/2.69 tff(c_382, plain, (c3_2(a624, a625))). % 8.02/2.69 tff(c_32, plain, (![U_1]: (ssSkP3(U_1) | ndr1_1(U_1)))). % 8.02/2.69 tff(c_380, plain, (~c3_2(a624, a626))). % 8.02/2.69 tff(c_377, plain, (~c4_2(a608, a609))). % 8.02/2.69 tff(c_379, plain, (~ssSkC6)). % 8.02/2.69 tff(c_376, plain, (~c2_2(a624, a625))). % 8.02/2.70 tff(c_38, plain, (![U_3]: (ssSkP1(U_3) | ndr1_1(U_3)))). % 8.02/2.70 tff(c_373, plain, (~ssSkC0)). % 8.02/2.70 tff(c_40, plain, (![U_4]: (ssSkP0(U_4) | ndr1_1(U_4)))). % 8.02/2.70 tff(c_372, plain, (c1_2(a637, a638))). % 8.02/2.70 tff(c_36, plain, (![U_2]: (ssSkP2(U_2) | ndr1_1(U_2)))). % 8.02/2.70 tff(c_370, plain, (~c1_2(a624, a625))). % 8.02/2.70 tff(c_369, plain, (~c3_1(a637))). % 8.02/2.70 tff(c_368, plain, (c2_1(a593))). % 8.02/2.70 tff(c_366, plain, (ndr1_1(a624))). % 8.02/2.70 tff(c_365, plain, (ndr1_1(a608))). % 8.02/2.70 tff(c_364, plain, (c5_1(a587))). % 8.02/2.70 tff(c_363, plain, (~c3_0)). % 8.02/2.70 tff(c_361, plain, (~c2_1(a637))). % 8.02/2.70 tff(c_360, plain, (~c3_1(a592))). % 8.02/2.70 tff(c_359, plain, (c3_1(a587))). % 8.02/2.70 tff(c_358, plain, (c5_1(a619))). % 8.02/2.70 tff(c_357, plain, (~c2_1(a616))). % 8.02/2.70 tff(c_356, plain, (c1_1(a619))). % 8.02/2.70 tff(c_355, plain, (c1_1(a616))). % 8.02/2.70 tff(c_353, plain, (c4_1(a619))). % 8.02/2.70 tff(c_352, plain, (~c4_1(a620))). % 8.02/2.70 tff(c_351, plain, (~c3_1(a616))). % 8.02/2.70 tff(c_350, plain, (~c2_1(a634))). % 8.02/2.70 tff(c_349, plain, (~c5_1(a593))). % 8.02/2.70 tff(c_348, plain, (~c4_1(a592))). % 8.02/2.70 tff(c_347, plain, (ndr1_1(a637))). % 8.02/2.70 tff(c_346, plain, (c2_1(a587))). % 8.02/2.70 tff(c_336, plain, (ndr1_0)). % 8.02/2.70 tff(c_335, plain, (~c4_0)). % 8.02/2.70 tff(c_2, plain, (c5_0)). % 8.02/2.70 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.02/2.70 %------------------------------------------------------------------------------