%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN544-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 : n027.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:52 PM UTC 2025 % Result : Satisfiable 23.15s 6.88s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SYN544-1 : TPTP v9.0.0. Released v2.1.0. % 0.00/0.10 % 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.09/0.29 % Computer : n027.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Wed Apr 9 07:58:20 EDT 2025 % 0.09/0.29 % CPUTime : % 23.15/6.88 % 23.15/6.88 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 23.15/6.88 % 23.15/6.88 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 23.37/6.90 %$ c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP9 > ssSkP8 > ssSkP7 > ssSkP6 > ssSkP5 > ssSkP4 > ssSkP3 > ssSkP2 > ssSkP1 > ssSkP0 > ndr1_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC9 > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC23 > ssSkC22 > ssSkC21 > ssSkC20 > ssSkC2 > ssSkC19 > ssSkC18 > ssSkC17 > ssSkC16 > ssSkC15 > ssSkC14 > ssSkC13 > ssSkC12 > ssSkC11 > ssSkC10 > ssSkC1 > ssSkC0 > ndr1_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a99 > a97 > a96 > a95 > a94 > a93 > a92 > a91 > a90 > a89 > a88 > a87 > a86 > a85 > a84 > a83 > a82 > a81 > a8 > a75 > a72 > a71 > a70 > a7 > a69 > a68 > a67 > a66 > a65 > a64 > a63 > a62 > a61 > a60 > a6 > a59 > a58 > a57 > a56 > a55 > a54 > a53 > a52 > a51 > a5 > a49 > a48 > a47 > a46 > a45 > a44 > a43 > a42 > a41 > a40 > a4 > a39 > a38 > a37 > a36 > a35 > a34 > a33 > a32 > a31 > a30 > a3 > a29 > a28 > a27 > a26 > a25 > a24 > a23 > a22 > a2 > a18 > a17 > a16 > a145 > a142 > a141 > a137 > a136 > a135 > a134 > a132 > a131 > a130 > a13 > a129 > a128 > a127 > a123 > a122 > a121 > a120 > a12 > a117 > a116 > a115 > a114 > a113 > a11 > a109 > a108 > a104 > a103 > a102 > a101 > a100 > a10 > a1 % 23.37/6.90 % 23.37/6.90 %Foreground sorts: % 23.37/6.90 % 23.37/6.90 % 23.37/6.90 %Background operators: % 23.37/6.90 % 23.37/6.90 % 23.37/6.90 %Foreground operators: % 23.37/6.90 tff(a99, type, a99: $i). % 23.37/6.90 tff(c7_0, type, c7_0: $o). % 23.37/6.90 tff(a1, type, a1: $i). % 23.37/6.90 tff(a94, type, a94: $i). % 23.37/6.90 tff(a68, type, a68: $i). % 23.37/6.90 tff(a101, type, a101: $i). % 23.37/6.90 tff(ssSkC8, type, ssSkC8: $o). % 23.37/6.90 tff(a100, type, a100: $i). % 23.37/6.90 tff(a108, type, a108: $i). % 23.37/6.90 tff(a89, type, a89: $i). % 23.37/6.90 tff(ssSkC7, type, ssSkC7: $o). % 23.37/6.90 tff(a64, type, a64: $i). % 23.37/6.90 tff(ssSkC21, type, ssSkC21: $o). % 23.37/6.90 tff(a3, type, a3: $i). % 23.37/6.90 tff(a97, type, a97: $i). % 23.37/6.90 tff(a32, type, a32: $i). % 23.37/6.90 tff(a35, type, a35: $i). % 23.37/6.90 tff(c4_0, type, c4_0: $o). % 23.37/6.90 tff(ssSkC10, type, ssSkC10: $o). % 23.37/6.90 tff(a47, type, a47: $i). % 23.37/6.90 tff(a34, type, a34: $i). % 23.37/6.90 tff(a69, type, a69: $i). % 23.37/6.90 tff(ssSkP0, type, ssSkP0: $i > $o). % 23.37/6.90 tff(a122, type, a122: $i). % 23.37/6.90 tff(a141, type, a141: $i). % 23.37/6.90 tff(a120, type, a120: $i). % 23.37/6.90 tff(ssSkC6, type, ssSkC6: $o). % 23.37/6.90 tff(a61, type, a61: $i). % 23.37/6.90 tff(c3_0, type, c3_0: $o). % 23.37/6.90 tff(a26, type, a26: $i). % 23.37/6.90 tff(ssSkP7, type, ssSkP7: $i > $o). % 23.37/6.90 tff(a103, type, a103: $i). % 23.37/6.90 tff(c1_2, type, c1_2: ($i * $i) > $o). % 23.37/6.90 tff(a60, type, a60: $i). % 23.37/6.90 tff(a40, type, a40: $i). % 23.37/6.90 tff(a113, type, a113: $i). % 23.37/6.90 tff(ssSkC23, type, ssSkC23: $o). % 23.37/6.90 tff(ssSkC3, type, ssSkC3: $o). % 23.37/6.90 tff(a130, type, a130: $i). % 23.37/6.90 tff(a36, type, a36: $i). % 23.37/6.90 tff(a75, type, a75: $i). % 23.37/6.90 tff(a62, type, a62: $i). % 23.37/6.90 tff(ssSkP2, type, ssSkP2: $i > $o). % 23.37/6.90 tff(a145, type, a145: $i). % 23.37/6.90 tff(ssSkC19, type, ssSkC19: $o). % 23.37/6.90 tff(a93, type, a93: $i). % 23.37/6.90 tff(a72, type, a72: $i). % 23.37/6.90 tff(a67, type, a67: $i). % 23.37/6.90 tff(a131, type, a131: $i). % 23.37/6.90 tff(a31, type, a31: $i). % 23.37/6.90 tff(a86, type, a86: $i). % 23.37/6.90 tff(a88, type, a88: $i). % 23.37/6.90 tff(c8_0, type, c8_0: $o). % 23.37/6.90 tff(a83, type, a83: $i). % 23.37/6.90 tff(a63, type, a63: $i). % 23.37/6.90 tff(a23, type, a23: $i). % 23.37/6.90 tff(a12, type, a12: $i). % 23.37/6.90 tff(a10, type, a10: $i). % 23.37/6.90 tff(ssSkC4, type, ssSkC4: $o). % 23.37/6.90 tff(a33, type, a33: $i). % 23.37/6.90 tff(a121, type, a121: $i). % 23.37/6.90 tff(a41, type, a41: $i). % 23.37/6.90 tff(a43, type, a43: $i). % 23.37/6.90 tff(a29, type, a29: $i). % 23.37/6.90 tff(a17, type, a17: $i). % 23.37/6.90 tff(a51, type, a51: $i). % 23.37/6.90 tff(a136, type, a136: $i). % 23.37/6.90 tff(c5_0, type, c5_0: $o). % 23.37/6.90 tff(a127, type, a127: $i). % 23.37/6.90 tff(ssSkC9, type, ssSkC9: $o). % 23.37/6.90 tff(ssSkP6, type, ssSkP6: $i > $o). % 23.37/6.90 tff(a142, type, a142: $i). % 23.37/6.90 tff(a28, type, a28: $i). % 23.37/6.90 tff(ssSkP8, type, ssSkP8: $i > $o). % 23.37/6.90 tff(a58, type, a58: $i). % 23.37/6.90 tff(c6_0, type, c6_0: $o). % 23.37/6.90 tff(a84, type, a84: $i). % 23.37/6.90 tff(a104, type, a104: $i). % 23.37/6.90 tff(c8_2, type, c8_2: ($i * $i) > $o). % 23.37/6.90 tff(a22, type, a22: $i). % 23.37/6.90 tff(a87, type, a87: $i). % 23.37/6.90 tff(ssSkC11, type, ssSkC11: $o). % 23.37/6.90 tff(a134, type, a134: $i). % 23.37/6.90 tff(ssSkC18, type, ssSkC18: $o). % 23.37/6.90 tff(ssSkC16, type, ssSkC16: $o). % 23.37/6.90 tff(a18, type, a18: $i). % 23.37/6.90 tff(a46, type, a46: $i). % 23.37/6.90 tff(ssSkP3, type, ssSkP3: $i > $o). % 23.37/6.90 tff(a7, type, a7: $i). % 23.37/6.90 tff(a11, type, a11: $i). % 23.37/6.90 tff(ssSkC17, type, ssSkC17: $o). % 23.37/6.90 tff(ssSkP9, type, ssSkP9: $i > $o). % 23.37/6.90 tff(a39, type, a39: $i). % 23.37/6.90 tff(a25, type, a25: $i). % 23.37/6.90 tff(c1_0, type, c1_0: $o). % 23.37/6.90 tff(a71, type, a71: $i). % 23.37/6.90 tff(c8_1, type, c8_1: $i > $o). % 23.37/6.90 tff(a53, type, a53: $i). % 23.37/6.90 tff(ssSkP4, type, ssSkP4: $i > $o). % 23.37/6.90 tff(a38, type, a38: $i). % 23.37/6.90 tff(c2_1, type, c2_1: $i > $o). % 23.37/6.90 tff(a129, type, a129: $i). % 23.37/6.90 tff(a2, type, a2: $i). % 23.37/6.90 tff(ndr1_1, type, ndr1_1: $i > $o). % 23.37/6.90 tff(ssSkC15, type, ssSkC15: $o). % 23.37/6.90 tff(c2_0, type, c2_0: $o). % 23.37/6.90 tff(c4_1, type, c4_1: $i > $o). % 23.37/6.90 tff(a45, type, a45: $i). % 23.37/6.90 tff(a6, type, a6: $i). % 23.37/6.90 tff(ssSkC12, type, ssSkC12: $o). % 23.37/6.90 tff(c6_2, type, c6_2: ($i * $i) > $o). % 23.37/6.90 tff(a90, type, a90: $i). % 23.37/6.90 tff(a52, type, a52: $i). % 23.37/6.90 tff(ssSkC20, type, ssSkC20: $o). % 23.37/6.90 tff(a123, type, a123: $i). % 23.37/6.90 tff(a116, type, a116: $i). % 23.37/6.90 tff(a66, type, a66: $i). % 23.37/6.90 tff(a92, type, a92: $i). % 23.37/6.90 tff(a57, type, a57: $i). % 23.37/6.90 tff(a4, type, a4: $i). % 23.37/6.90 tff(ndr1_0, type, ndr1_0: $o). % 23.37/6.90 tff(a48, type, a48: $i). % 23.37/6.90 tff(a44, type, a44: $i). % 23.37/6.90 tff(a117, type, a117: $i). % 23.37/6.90 tff(a42, type, a42: $i). % 23.37/6.90 tff(ssSkC14, type, ssSkC14: $o). % 23.37/6.90 tff(a85, type, a85: $i). % 23.37/6.90 tff(a30, type, a30: $i). % 23.37/6.90 tff(a56, type, a56: $i). % 23.37/6.90 tff(a54, type, a54: $i). % 23.37/6.90 tff(a137, type, a137: $i). % 23.37/6.90 tff(a49, type, a49: $i). % 23.37/6.90 tff(a5, type, a5: $i). % 23.37/6.90 tff(c1_1, type, c1_1: $i > $o). % 23.37/6.90 tff(a16, type, a16: $i). % 23.37/6.90 tff(a115, type, a115: $i). % 23.37/6.90 tff(a96, type, a96: $i). % 23.37/6.90 tff(ssSkC13, type, ssSkC13: $o). % 23.37/6.90 tff(a27, type, a27: $i). % 23.37/6.90 tff(ssSkC2, type, ssSkC2: $o). % 23.37/6.90 tff(c5_2, type, c5_2: ($i * $i) > $o). % 23.37/6.90 tff(a70, type, a70: $i). % 23.37/6.90 tff(a37, type, a37: $i). % 23.37/6.90 tff(c7_1, type, c7_1: $i > $o). % 23.37/6.90 tff(c6_1, type, c6_1: $i > $o). % 23.37/6.90 tff(a95, type, a95: $i). % 23.37/6.90 tff(a135, type, a135: $i). % 23.37/6.90 tff(ssSkC22, type, ssSkC22: $o). % 23.37/6.90 tff(c4_2, type, c4_2: ($i * $i) > $o). % 23.37/6.90 tff(a114, type, a114: $i). % 23.37/6.90 tff(ssSkC1, type, ssSkC1: $o). % 23.37/6.90 tff(a82, type, a82: $i). % 23.37/6.90 tff(ssSkP5, type, ssSkP5: $i > $o). % 23.37/6.90 tff(a55, type, a55: $i). % 23.37/6.90 tff(ssSkC0, type, ssSkC0: $o). % 23.37/6.90 tff(ssSkC5, type, ssSkC5: $o). % 23.37/6.90 tff(a8, type, a8: $i). % 23.37/6.90 tff(ssSkP1, type, ssSkP1: $i > $o). % 23.37/6.90 tff(a91, type, a91: $i). % 23.37/6.90 tff(c5_1, type, c5_1: $i > $o). % 23.37/6.90 tff(a13, type, a13: $i). % 23.37/6.90 tff(a81, type, a81: $i). % 23.37/6.90 tff(c7_2, type, c7_2: ($i * $i) > $o). % 23.37/6.90 tff(c3_2, type, c3_2: ($i * $i) > $o). % 23.37/6.90 tff(a24, type, a24: $i). % 23.37/6.90 tff(a109, type, a109: $i). % 23.37/6.90 tff(c2_2, type, c2_2: ($i * $i) > $o). % 23.37/6.90 tff(a102, type, a102: $i). % 23.37/6.90 tff(a65, type, a65: $i). % 23.37/6.90 tff(a128, type, a128: $i). % 23.37/6.90 tff(a59, type, a59: $i). % 23.37/6.90 tff(a132, type, a132: $i). % 23.37/6.90 tff(c3_1, type, c3_1: $i > $o). % 23.37/6.90 % 23.37/6.90 %Saturated clause set: % 23.37/6.91 tff(c_6054, plain, (![U_14]: (c7_1(U_14) | ~c2_2(U_14, a108) | ~c2_2(U_14, a94) | ssSkP7(U_14) | c1_1(U_14) | ~c6_1(U_14) | ~ndr1_1(U_14) | ~c3_2(U_14, a94) | ssSkP8(U_14)))). % 23.37/6.91 tff(c_5894, plain, (![U_601, V_602]: (c7_1(U_601) | ~c4_2(U_601, V_602) | c1_1(U_601) | c5_2(U_601, V_602) | ~c2_2(U_601, a108) | ~ndr1_1(U_601) | ~c2_2(U_601, V_602) | ssSkP7(U_601)))). % 23.37/6.91 tff(c_6041, plain, (![U_607]: (ssSkP8(U_607) | c7_1(U_607) | ~c4_2(U_607, a94) | c1_1(U_607) | ~c2_2(U_607, a108) | ~ndr1_1(U_607) | ~c2_2(U_607, a94) | ssSkP7(U_607)))). % 23.37/6.91 tff(c_5980, plain, (![U_17]: (~c2_2(U_17, a108) | c1_1(U_17) | ~c6_1(U_17) | ~c3_2(U_17, a108) | c7_1(U_17) | ~ndr1_1(U_17) | ssSkP7(U_17)))). % 23.37/6.91 tff(c_5979, plain, (![U_17]: (c1_1(U_17) | c7_1(U_17) | c8_1(U_17) | c2_2(U_17, a100) | ~ndr1_1(U_17) | ~c2_2(U_17, a108) | ssSkP7(U_17)))). % 23.37/6.91 tff(c_5978, plain, (![U_17]: (c1_1(U_17) | c7_1(U_17) | c8_1(U_17) | c4_2(U_17, a100) | ~ndr1_1(U_17) | ~c2_2(U_17, a108) | ssSkP7(U_17)))). % 23.37/6.91 tff(c_5960, plain, (![U_603]: (c7_1(U_603) | ~c4_2(U_603, a108) | c1_1(U_603) | ~ndr1_1(U_603) | ~c2_2(U_603, a108) | ssSkP7(U_603)))). % 23.37/6.91 tff(c_5754, plain, (![U_596]: (ssSkP8(U_596) | c2_1(U_596) | c6_1(U_596) | c7_1(U_596) | ~c4_2(U_596, a94) | c5_2(U_596, a67) | c1_1(U_596) | ~c2_2(U_596, a67) | ~ndr1_1(U_596) | ~c2_2(U_596, a94)))). % 23.37/6.91 tff(c_5566, plain, (![U_589, V_590]: (c2_1(U_589) | c6_1(U_589) | c7_1(U_589) | ~c4_2(U_589, V_590) | c5_2(U_589, a67) | c1_1(U_589) | c5_2(U_589, V_590) | ~c2_2(U_589, a67) | ~ndr1_1(U_589) | ~c2_2(U_589, V_590)))). % 23.37/6.91 tff(c_5651, plain, (![U_592]: (ssSkP8(U_592) | ssSkP3(U_592) | c7_1(U_592) | ~c4_2(U_592, a94) | c5_2(U_592, a22) | c1_1(U_592) | ~c2_2(U_592, a22) | ~ndr1_1(U_592) | ~c2_2(U_592, a94)))). % 23.37/6.91 tff(c_5586, plain, (![U_589]: (ssSkP3(U_589) | c7_1(U_589) | ~c4_2(U_589, a22) | c1_1(U_589) | ~ndr1_1(U_589) | ~c2_2(U_589, a22) | c5_2(U_589, a22)))). % 23.37/6.92 tff(c_5567, plain, (![U_589, V_590]: (ssSkP3(U_589) | c7_1(U_589) | ~c4_2(U_589, V_590) | c5_2(U_589, a22) | c1_1(U_589) | c5_2(U_589, V_590) | ~c2_2(U_589, a22) | ~ndr1_1(U_589) | ~c2_2(U_589, V_590)))). % 23.37/6.92 tff(c_5201, plain, (![U_247, V_248, W_546]: (c7_1(U_247) | ~c4_2(U_247, V_248) | c5_2(U_247, W_546) | c1_1(U_247) | c5_2(U_247, V_248) | ~c2_2(U_247, W_546) | ~ndr1_1(U_247) | ~c2_2(U_247, V_248) | c7_2(U_247, W_546)))). % 23.37/6.92 tff(c_5186, plain, (![U_579]: (ssSkP8(U_579) | ssSkP2(U_579) | c7_1(U_579) | ~c4_2(U_579, a94) | c5_2(U_579, a4) | c1_1(U_579) | ~c2_2(U_579, a4) | ~ndr1_1(U_579) | ~c2_2(U_579, a94)))). % 23.37/6.92 tff(c_5366, plain, (~c2_2(a90, a87))). % 23.37/6.92 tff(c_5104, plain, (![U_576, V_577]: (ssSkP2(U_576) | c7_1(U_576) | ~c4_2(U_576, V_577) | c5_2(U_576, a4) | c1_1(U_576) | c5_2(U_576, V_577) | ~c2_2(U_576, a4) | ~ndr1_1(U_576) | ~c2_2(U_576, V_577)))). % 23.37/6.92 tff(c_4828, plain, (c1_1(a24))). % 23.37/6.92 tff(c_4201, plain, (![U_553]: (c2_1(U_553) | c6_1(U_553) | c7_1(U_553) | ~c4_2(U_553, a87) | ~c2_2(U_553, a87) | c1_1(U_553) | c5_2(U_553, a67) | ~ndr1_1(U_553) | ~c2_2(U_553, a67) | ssSkP7(U_553)))). % 23.37/6.92 tff(c_4803, plain, (![U_569]: (c7_1(U_569) | ~c4_2(U_569, a87) | ~c2_2(U_569, a87) | c1_1(U_569) | ~ndr1_1(U_569) | ~c2_2(U_569, a108) | ssSkP7(U_569)))). % 23.37/6.92 tff(c_4236, plain, (![U_247, V_248]: (c7_1(U_247) | ~c4_2(U_247, V_248) | ssSkP7(U_247) | c1_1(U_247) | c5_2(U_247, V_248) | ~c2_2(U_247, a87) | ~ndr1_1(U_247) | ~c2_2(U_247, V_248) | c7_2(U_247, a87)))). % 23.37/6.92 tff(c_4428, plain, (~c3_2(a44, a94))). % 23.37/6.92 tff(c_4412, plain, (~c2_2(a44, a2))). % 23.37/6.92 tff(c_4204, plain, (![U_553]: (ssSkP2(U_553) | c7_1(U_553) | ~c4_2(U_553, a87) | ~c2_2(U_553, a87) | c1_1(U_553) | c5_2(U_553, a4) | ~ndr1_1(U_553) | ~c2_2(U_553, a4) | ssSkP7(U_553)))). % 23.37/6.92 tff(c_4289, plain, (![V_557]: (~c4_2(a44, V_557) | ~c2_2(a44, V_557)))). % 23.37/6.92 tff(c_2765, plain, (![U_247, V_248, W_249]: (c7_1(U_247) | c7_2(U_247, a87) | ~c4_2(U_247, V_248) | ssSkP7(U_247) | c1_1(U_247) | c7_2(U_247, W_249) | c5_2(U_247, V_248) | ~c2_2(U_247, W_249) | ~ndr1_1(U_247) | ~c2_2(U_247, V_248)))). % 23.37/6.92 tff(c_4202, plain, (![U_553]: (ssSkP3(U_553) | c7_1(U_553) | ~c4_2(U_553, a87) | ~c2_2(U_553, a87) | c1_1(U_553) | c5_2(U_553, a22) | ~ndr1_1(U_553) | ~c2_2(U_553, a22) | ssSkP7(U_553)))). % 23.37/6.92 tff(c_4001, plain, (![U_16, W_546]: (c7_1(U_16) | ~c4_2(U_16, a87) | ~c2_2(U_16, a87) | c1_1(U_16) | c5_2(U_16, W_546) | ~ndr1_1(U_16) | ~c2_2(U_16, W_546) | ssSkP7(U_16) | c7_2(U_16, W_546)))). % 23.37/6.92 tff(c_4138, plain, (~c2_2(a24, a87))). % 23.37/6.92 tff(c_3986, plain, (![U_76]: (c5_1(U_76) | ~c2_2(U_76, a56) | ~c1_2(U_76, a63) | ~c3_1(U_76) | ~c2_1(U_76) | ~ndr1_1(U_76) | ~c3_2(U_76, a63) | c6_1(U_76) | ~c7_1(U_76)))). % 23.37/6.92 tff(c_3936, plain, (![U_76]: (c5_1(U_76) | c3_2(U_76, a56) | ~c1_2(U_76, a63) | ~c3_1(U_76) | ~c2_1(U_76) | ~ndr1_1(U_76) | ~c3_2(U_76, a63) | c6_1(U_76) | ~c7_1(U_76)))). % 23.37/6.92 tff(c_2603, plain, (![U_247, V_248, V_487, W_249]: (c7_1(U_247) | c7_2(U_247, V_248) | ~c4_2(U_247, V_487) | ~c2_2(U_247, V_487) | ~c8_2(U_247, V_487) | c1_1(U_247) | c7_2(U_247, W_249) | c5_2(U_247, V_248) | ~c2_2(U_247, W_249) | ~ndr1_1(U_247) | ~c2_2(U_247, V_248)))). % 23.37/6.92 tff(c_3290, plain, (![U_508, V_509]: (c5_1(U_508) | c7_2(U_508, a56) | ~c1_2(U_508, V_509) | ~c4_2(U_508, V_509) | c5_2(U_508, V_509) | ~c3_1(U_508) | ~c2_1(U_508) | ~ndr1_1(U_508) | ~c3_2(U_508, V_509)))). % 23.37/6.92 tff(c_3288, plain, (![U_508, V_509]: (c5_1(U_508) | c3_2(U_508, a56) | ~c1_2(U_508, V_509) | ~c4_2(U_508, V_509) | c5_2(U_508, V_509) | ~c3_1(U_508) | ~c2_1(U_508) | ~ndr1_1(U_508) | ~c3_2(U_508, V_509)))). % 23.37/6.93 tff(c_3579, plain, (![U_522]: (c5_1(U_522) | ~c2_2(U_522, a56) | ~c1_2(U_522, a108) | c7_1(U_522) | c8_1(U_522) | c4_2(U_522, a100) | ~ndr1_1(U_522) | ~c2_2(U_522, a108) | ssSkP7(U_522)))). % 23.37/6.93 tff(c_3524, plain, (![U_519]: (c5_1(U_519) | c3_2(U_519, a56) | ~c1_2(U_519, a108) | c7_1(U_519) | c8_1(U_519) | c2_2(U_519, a100) | ~ndr1_1(U_519) | ~c2_2(U_519, a108) | ssSkP7(U_519)))). % 23.37/6.93 tff(c_3580, plain, (![U_522]: (c5_1(U_522) | c3_2(U_522, a56) | ~c1_2(U_522, a108) | c7_1(U_522) | c8_1(U_522) | c4_2(U_522, a100) | ~ndr1_1(U_522) | ~c2_2(U_522, a108) | ssSkP7(U_522)))). % 23.37/6.93 tff(c_3523, plain, (![U_519]: (c5_1(U_519) | ~c2_2(U_519, a56) | ~c1_2(U_519, a108) | c7_1(U_519) | c8_1(U_519) | c2_2(U_519, a100) | ~ndr1_1(U_519) | ~c2_2(U_519, a108) | ssSkP7(U_519)))). % 23.37/6.93 tff(c_3432, plain, (![U_17]: (c5_1(U_17) | ~c2_2(U_17, a56) | ~c1_2(U_17, a108) | c1_1(U_17) | ~c6_1(U_17) | ~c3_2(U_17, a108) | c7_1(U_17) | ~ndr1_1(U_17) | ssSkP7(U_17)))). % 23.37/6.93 tff(c_3327, plain, (![U_17]: (c5_1(U_17) | c3_2(U_17, a56) | ~c1_2(U_17, a108) | c1_1(U_17) | ~c6_1(U_17) | ~c3_2(U_17, a108) | c7_1(U_17) | ~ndr1_1(U_17) | ssSkP7(U_17)))). % 23.37/6.93 tff(c_3289, plain, (![U_508, V_509]: (c5_1(U_508) | ~c2_2(U_508, a56) | ~c1_2(U_508, V_509) | ~c4_2(U_508, V_509) | c5_2(U_508, V_509) | ~c3_1(U_508) | ~c2_1(U_508) | ~ndr1_1(U_508) | ~c3_2(U_508, V_509)))). % 23.37/6.93 tff(c_3656, plain, (![U_181]: (~c7_1(U_181) | ~ssSkP7(U_181) | c8_1(U_181) | c2_2(U_181, a100) | c4_2(U_181, a88) | ~ndr1_1(U_181) | ~c2_2(U_181, a88)))). % 23.37/6.93 tff(c_3694, plain, (~c2_2(a44, a88))). % 23.37/6.93 tff(c_3655, plain, (![U_179]: (~c7_1(U_179) | ~ssSkP7(U_179) | c8_1(U_179) | c5_2(U_179, a100) | c4_2(U_179, a88) | ~ndr1_1(U_179) | ~c2_2(U_179, a88)))). % 23.37/6.93 tff(c_3678, plain, (~c2_2(a35, a88))). % 23.37/6.93 tff(c_3657, plain, (![U_177]: (~c7_1(U_177) | ~ssSkP7(U_177) | c8_1(U_177) | c4_2(U_177, a100) | c4_2(U_177, a88) | ~ndr1_1(U_177) | ~c2_2(U_177, a88)))). % 23.37/6.93 tff(c_3661, plain, (~ssSkC9)). % 23.37/6.93 tff(c_3660, plain, (~c2_2(a44, a108))). % 23.37/6.93 tff(c_3659, plain, (~c2_2(a136, a88))). % 23.37/6.93 tff(c_3630, plain, (![U_357]: (~c7_1(U_357) | ~c7_2(U_357, a88) | ~ssSkP7(U_357)))). % 23.37/6.93 tff(c_3614, plain, (![U_17]: (c7_1(U_17) | c8_1(U_17) | c5_2(U_17, a100) | c4_2(U_17, a108) | ~ndr1_1(U_17) | ~c2_2(U_17, a108) | ssSkP7(U_17)))). % 23.37/6.93 tff(c_3595, plain, (![U_352]: (c1_2(U_352, a88) | ~c7_1(U_352) | ~ssSkP7(U_352)))). % 23.37/6.93 tff(c_3557, plain, (![U_17]: (c7_1(U_17) | c8_1(U_17) | c4_2(U_17, a100) | c4_2(U_17, a108) | ~ndr1_1(U_17) | ~c2_2(U_17, a108) | ssSkP7(U_17)))). % 23.37/6.93 tff(c_2051, plain, (![U_16]: (c5_1(U_16) | c7_2(U_16, a56) | ~c1_2(U_16, a108) | ~c4_2(U_16, a108) | c7_1(U_16) | ~ndr1_1(U_16) | ~c5_2(U_16, a87) | ssSkP7(U_16)))). % 23.37/6.93 tff(c_3501, plain, (~c7_1(a34))). % 23.37/6.93 tff(c_3497, plain, (~c7_1(a120))). % 23.37/6.93 tff(c_3450, plain, (![U_17]: (c7_1(U_17) | c8_1(U_17) | c2_2(U_17, a100) | c4_2(U_17, a108) | ~ndr1_1(U_17) | ~c2_2(U_17, a108) | ssSkP7(U_17)))). % 23.37/6.93 tff(c_3496, plain, (~c7_1(a65))). % 23.37/6.93 tff(c_3472, plain, (![U_3]: (~c7_1(U_3) | ndr1_1(U_3)))). % 23.37/6.93 tff(c_3427, plain, (![U_17]: (c5_1(U_17) | ~c2_2(U_17, a56) | ~c1_2(U_17, a108) | ~c4_2(U_17, a108) | c7_1(U_17) | ~ndr1_1(U_17) | ssSkP7(U_17)))). % 23.37/6.93 tff(c_3410, plain, (~c3_2(a52, a87))). % 23.37/6.93 tff(c_3409, plain, (~c2_1(a134))). % 23.37/6.93 tff(c_3284, plain, (![U_508, V_509]: (c1_1(U_508) | c4_2(U_508, V_509) | ~c6_1(U_508) | c5_2(U_508, V_509) | ~c3_1(U_508) | ~c2_1(U_508) | ~ndr1_1(U_508) | ~c3_2(U_508, V_509)))). % 23.37/6.93 tff(c_3244, plain, (![U_17]: (c5_1(U_17) | c3_2(U_17, a56) | ~c1_2(U_17, a108) | ~c4_2(U_17, a108) | c7_1(U_17) | ~ndr1_1(U_17) | ssSkP7(U_17)))). % 23.37/6.93 tff(c_3322, plain, (~c2_1(a90))). % 23.37/6.93 tff(c_3321, plain, (~c3_2(a27, a28))). % 23.37/6.93 tff(c_3295, plain, (![U_508]: (ssSkP3(U_508) | c5_2(U_508, a22) | ~c3_1(U_508) | ~c2_1(U_508) | ~ndr1_1(U_508) | ~c3_2(U_508, a22)))). % 23.37/6.93 tff(c_3305, plain, (~c3_2(a96, a97))). % 23.37/6.93 tff(c_3247, plain, (![U_332, V_333]: (c6_2(U_332, V_333) | c5_2(U_332, V_333) | ~c3_1(U_332) | ~c2_1(U_332) | ~ndr1_1(U_332) | ~c3_2(U_332, V_333)))). % 23.37/6.93 tff(c_3232, plain, (c1_1(a35))). % 23.37/6.93 tff(c_3231, plain, (~c3_2(a35, a94))). % 23.37/6.93 tff(c_3148, plain, (![U_134]: (~c4_2(a35, U_134) | ~c2_2(a35, U_134) | ~c1_2(a35, U_134)))). % 23.37/6.93 tff(c_3132, plain, (![V_487]: (~c4_2(a35, V_487) | ~c2_2(a35, V_487) | ~c8_2(a35, V_487)))). % 23.37/6.93 tff(c_3131, plain, (~c4_1(a34))). % 23.37/6.93 tff(c_3130, plain, (~c4_1(a18))). % 23.37/6.93 tff(c_3120, plain, (~c4_1(a52))). % 23.37/6.93 tff(c_3114, plain, (~c4_1(a51))). % 23.37/6.93 tff(c_3129, plain, (c3_1(a127))). % 23.37/6.93 tff(c_3128, plain, (~c4_1(a65))). % 23.37/6.93 tff(c_3068, plain, (![U_313]: (~c5_1(U_313) | ~c6_1(U_313) | ~c4_1(U_313)))). % 23.37/6.94 tff(c_3069, plain, (~c5_1(a127))). % 23.37/6.94 tff(c_3067, plain, (c6_1(a127))). % 23.37/6.94 tff(c_3062, plain, (c7_1(a127))). % 23.37/6.94 tff(c_3054, plain, (c8_1(a127))). % 23.37/6.94 tff(c_2408, plain, (![U_450]: (c4_1(U_450) | c7_1(U_450) | c1_2(U_450, a22) | ssSkP3(U_450) | c8_1(U_450) | c2_2(U_450, a100) | ~ndr1_1(U_450) | ~c2_2(U_450, a22)))). % 23.37/6.94 tff(c_2409, plain, (![U_438]: (c4_1(U_438) | c7_1(U_438) | c1_2(U_438, a22) | ssSkP3(U_438) | c8_1(U_438) | c4_2(U_438, a100) | ~ndr1_1(U_438) | ~c2_2(U_438, a22)))). % 23.37/6.94 tff(c_2445, plain, (![U_477]: (c5_1(U_477) | ~c2_2(U_477, a56) | ~c1_2(U_477, a94) | c1_1(U_477) | ~c6_1(U_477) | ~ndr1_1(U_477) | ~c3_2(U_477, a94) | ssSkP8(U_477)))). % 23.37/6.94 tff(c_2444, plain, (![U_477]: (c5_1(U_477) | c3_2(U_477, a56) | ~c1_2(U_477, a94) | c1_1(U_477) | ~c6_1(U_477) | ~ndr1_1(U_477) | ~c3_2(U_477, a94) | ssSkP8(U_477)))). % 23.37/6.94 tff(c_3040, plain, (c1_1(a60))). % 23.37/6.94 tff(c_3039, plain, (~c2_2(a60, a87))). % 23.37/6.94 tff(c_3021, plain, (![V_255]: (~c4_2(a60, V_255) | ~c2_2(a60, V_255) | ~c8_2(a60, V_255)))). % 23.37/6.94 tff(c_3018, plain, (~c2_2(a60, a108))). % 23.37/6.94 tff(c_3010, plain, (~c4_2(a60, a108))). % 23.37/6.94 tff(c_3008, plain, (~c3_2(a60, a108))). % 23.37/6.94 tff(c_3009, plain, (c3_2(a60, a62))). % 23.37/6.94 tff(c_2984, plain, (c6_2(a60, a108))). % 23.37/6.94 tff(c_2983, plain, (~c5_2(a60, a108))). % 23.37/6.94 tff(c_2957, plain, (~c7_2(a60, a108))). % 23.37/6.94 tff(c_2927, plain, (c8_2(a60, a61))). % 23.37/6.94 tff(c_2910, plain, (![U_17]: (c1_1(U_17) | c4_2(U_17, a108) | ~c6_1(U_17) | ~c3_2(U_17, a108) | c7_1(U_17) | ~ndr1_1(U_17) | ssSkP7(U_17)))). % 23.37/6.94 tff(c_2897, plain, (c5_2(a60, a61))). % 23.37/6.94 tff(c_2896, plain, (c1_1(a47))). % 23.37/6.94 tff(c_2895, plain, (c1_1(a136))). % 23.37/6.94 tff(c_2894, plain, (ssSkP4(a136))). % 23.37/6.94 tff(c_2890, plain, (~c2_2(a136, a57))). % 23.37/6.94 tff(c_2889, plain, (~c2_2(a136, a22))). % 23.37/6.94 tff(c_2847, plain, (![U_78]: (~c4_2(a136, U_78) | ~c2_2(a136, U_78) | c7_2(a136, U_78) | c3_2(a136, U_78)))). % 23.37/6.94 tff(c_2849, plain, (~c2_2(a136, a87))). % 23.37/6.94 tff(c_2831, plain, (![V_487]: (~c4_2(a136, V_487) | ~c2_2(a136, V_487) | ~c8_2(a136, V_487)))). % 23.37/6.94 tff(c_2830, plain, (~c4_2(a60, a62))). % 23.37/6.94 tff(c_2829, plain, (ssSkP8(a134))). % 23.37/6.94 tff(c_2825, plain, (~c2_2(a134, a94))). % 23.37/6.94 tff(c_2797, plain, (![V_248]: (~c4_2(a134, V_248) | c5_2(a134, V_248) | ~c2_2(a134, V_248)))). % 23.37/6.94 tff(c_2798, plain, (c2_2(a60, a62))). % 23.37/6.94 tff(c_2796, plain, (~c2_2(a134, a67))). % 23.37/6.94 tff(c_2795, plain, (~c3_2(a134, a94))). % 23.37/6.94 tff(c_2794, plain, (~c2_2(a134, a4))). % 23.37/6.94 tff(c_2778, plain, (![U_16]: (c7_1(U_16) | c7_2(U_16, a87) | ~ndr1_1(U_16) | ~c4_2(U_16, a87) | ~c2_2(U_16, a87) | ssSkP7(U_16)))). % 23.37/6.94 tff(c_2790, plain, (~c2_2(a134, a22))). % 23.37/6.94 tff(c_2791, plain, (~c2_2(a60, a61))). % 23.37/6.94 tff(c_2789, plain, (ssSkP4(a134))). % 23.37/6.94 tff(c_2785, plain, (~c2_2(a134, a57))). % 23.37/6.94 tff(c_2739, plain, (~c2_2(a134, a2))). % 23.37/6.94 tff(c_2616, plain, (![U_16, V_487]: (c7_1(U_16) | c7_2(U_16, a87) | ~ndr1_1(U_16) | ~c4_2(U_16, V_487) | ~c2_2(U_16, V_487) | ~c8_2(U_16, V_487) | ssSkP7(U_16)))). % 23.37/6.94 tff(c_2662, plain, (![V_130]: (~c4_2(a134, V_130) | ~c2_2(a134, V_130) | c1_2(a134, V_130)))). % 23.37/6.94 tff(c_2666, plain, (ndr1_1(a60))). % 23.37/6.94 tff(c_2665, plain, (~c2_2(a134, a87))). % 23.37/6.94 tff(c_2642, plain, (![V_487]: (~c4_2(a134, V_487) | ~c2_2(a134, V_487) | ~c8_2(a134, V_487)))). % 23.37/6.94 tff(c_2641, plain, (~c2_2(a47, a87))). % 23.37/6.94 tff(c_2623, plain, (![V_487]: (~c4_2(a47, V_487) | ~c2_2(a47, V_487) | ~c8_2(a47, V_487)))). % 23.37/6.94 tff(c_2585, plain, (![U_254, W_256, V_255]: (c7_1(U_254) | c7_2(U_254, W_256) | ~c8_2(U_254, W_256) | ~ndr1_1(U_254) | ~c4_2(U_254, V_255) | ~c2_2(U_254, V_255) | ~c8_2(U_254, V_255)))). % 23.37/6.94 tff(c_2584, plain, (~c2_2(a44, a115))). % 23.37/6.94 tff(c_2547, plain, (![U_481]: (~c8_1(U_481) | c1_1(U_481) | c5_2(U_481, a115) | ~ndr1_1(U_481) | ~c2_2(U_481, a115)))). % 23.37/6.94 tff(c_2553, plain, (~c2_2(a24, a115))). % 23.37/6.94 tff(c_2447, plain, (~c2_2(a35, a67))). % 23.37/6.94 tff(c_2449, plain, (![U_247, W_249, V_248]: (c1_1(U_247) | c7_2(U_247, W_249) | c8_2(U_247, V_248) | c5_2(U_247, V_248) | ~c2_2(U_247, W_249) | ~ndr1_1(U_247) | ~c2_2(U_247, V_248)))). % 23.37/6.94 tff(c_2446, plain, (~c1_2(a96, a97))). % 23.37/6.94 tff(c_2436, plain, (![U_14]: (c1_1(U_14) | c4_2(U_14, a94) | ~c6_1(U_14) | ~ndr1_1(U_14) | ~c3_2(U_14, a94) | ssSkP8(U_14)))). % 23.37/6.94 tff(c_2410, plain, (![U_264, V_265]: (c1_1(U_264) | c4_2(U_264, V_265) | ~c6_1(U_264) | ~ndr1_1(U_264) | ~c3_2(U_264, V_265) | ~c6_2(U_264, V_265)))). % 23.37/6.94 tff(c_2387, plain, (![U_471]: (ssSkP3(U_471) | c4_1(U_471) | c7_1(U_471) | c1_2(U_471, a22) | ~ndr1_1(U_471) | ~c4_2(U_471, a22)))). % 23.37/6.94 tff(c_2386, plain, (![U_471]: (ssSkP5(U_471) | c4_1(U_471) | c7_1(U_471) | c1_2(U_471, a69) | ~ndr1_1(U_471) | ~c4_2(U_471, a69)))). % 23.37/6.95 tff(c_2399, plain, (c7_2(a96, a97))). % 23.37/6.95 tff(c_2398, plain, (~c4_2(a96, a97))). % 23.37/6.95 tff(c_2397, plain, (c1_2(a24, a26))). % 23.37/6.95 tff(c_2343, plain, (![U_201, V_202]: (c4_1(U_201) | c7_1(U_201) | c1_2(U_201, V_202) | c6_2(U_201, V_202) | ~ndr1_1(U_201) | ~c4_2(U_201, V_202)))). % 23.37/6.95 tff(c_2340, plain, (~c6_2(a96, a97))). % 23.37/6.95 tff(c_2332, plain, (![U_17]: (c7_1(U_17) | c1_2(U_17, a108) | ~c3_1(U_17) | ~ndr1_1(U_17) | ~c3_2(U_17, a108) | ssSkP7(U_17)))). % 23.37/6.95 tff(c_2326, plain, (~c2_2(a44, a67))). % 23.37/6.95 tff(c_2231, plain, (![U_459]: (c2_1(U_459) | c6_1(U_459) | c8_1(U_459) | c5_2(U_459, a100) | c4_2(U_459, a67) | ~ndr1_1(U_459) | ~c2_2(U_459, a67)))). % 23.37/6.95 tff(c_2306, plain, (![U_466]: (c2_1(U_466) | c6_1(U_466) | c8_1(U_466) | c4_2(U_466, a100) | ~ndr1_1(U_466) | ~c2_2(U_466, a67)))). % 23.37/6.95 tff(c_2300, plain, (![U_464]: (c2_1(U_464) | c6_1(U_464) | c8_1(U_464) | c2_2(U_464, a100) | ~ndr1_1(U_464) | ~c2_2(U_464, a67)))). % 23.37/6.95 tff(c_2295, plain, (~c2_2(a35, a4))). % 23.37/6.95 tff(c_2294, plain, (ssSkP4(a35))). % 23.37/6.95 tff(c_2290, plain, (~c2_2(a35, a57))). % 23.37/6.95 tff(c_2287, plain, (~c2_2(a35, a22))). % 23.37/6.95 tff(c_2235, plain, (![U_459]: (ssSkP4(U_459) | c8_1(U_459) | c5_2(U_459, a100) | c4_2(U_459, a57) | ~ndr1_1(U_459) | ~c2_2(U_459, a57)))). % 23.37/6.95 tff(c_2270, plain, (~c2_2(a44, a4))). % 23.37/6.95 tff(c_2254, plain, (~c2_2(a44, a22))). % 23.37/6.95 tff(c_2234, plain, (![U_459]: (ssSkP2(U_459) | c8_1(U_459) | c5_2(U_459, a100) | c4_2(U_459, a4) | ~ndr1_1(U_459) | ~c2_2(U_459, a4)))). % 23.37/6.95 tff(c_2232, plain, (![U_459]: (ssSkP3(U_459) | c8_1(U_459) | c5_2(U_459, a100) | c4_2(U_459, a22) | ~ndr1_1(U_459) | ~c2_2(U_459, a22)))). % 23.37/6.95 tff(c_2181, plain, (![U_179, V_180]: (c8_1(U_179) | c5_2(U_179, a100) | c4_2(U_179, V_180) | c7_2(U_179, V_180) | ~ndr1_1(U_179) | ~c2_2(U_179, V_180)))). % 23.37/6.95 tff(c_2180, plain, (ndr1_1(a96))). % 23.37/6.95 tff(c_2178, plain, (![U_14]: (c5_1(U_14) | c3_2(U_14, a56) | ~ndr1_1(U_14) | ~c1_2(U_14, a94) | ~c4_2(U_14, a94) | ssSkP8(U_14)))). % 23.37/6.95 tff(c_2157, plain, (![U_204, V_205]: (c5_1(U_204) | c3_2(U_204, a56) | ~ndr1_1(U_204) | ~c6_2(U_204, V_205) | ~c1_2(U_204, V_205) | ~c4_2(U_204, V_205)))). % 23.37/6.95 tff(c_2156, plain, (c2_1(a96))). % 23.37/6.95 tff(c_2155, plain, (c1_1(a18))). % 23.37/6.95 tff(c_2136, plain, (![U_450]: (ssSkP4(U_450) | c8_1(U_450) | c2_2(U_450, a100) | c4_2(U_450, a57) | ~ndr1_1(U_450) | ~c2_2(U_450, a57)))). % 23.37/6.95 tff(c_2145, plain, (![U_453]: (ssSkP2(U_453) | c8_1(U_453) | c2_2(U_453, a100) | ~ndr1_1(U_453) | ~c2_2(U_453, a4)))). % 23.37/6.95 tff(c_2133, plain, (![U_450]: (ssSkP3(U_450) | c8_1(U_450) | c2_2(U_450, a100) | c4_2(U_450, a22) | ~ndr1_1(U_450) | ~c2_2(U_450, a22)))). % 23.37/6.95 tff(c_2082, plain, (![U_181, V_182]: (c8_1(U_181) | c2_2(U_181, a100) | c4_2(U_181, V_182) | c7_2(U_181, V_182) | ~ndr1_1(U_181) | ~c2_2(U_181, V_182)))). % 23.37/6.95 tff(c_2080, plain, (![U_14]: (c5_1(U_14) | ~c2_2(U_14, a56) | ~ndr1_1(U_14) | ~c1_2(U_14, a94) | ~c4_2(U_14, a94) | ssSkP8(U_14)))). % 23.37/6.95 tff(c_2059, plain, (![U_232, V_233]: (c5_1(U_232) | ~c2_2(U_232, a56) | ~ndr1_1(U_232) | ~c6_2(U_232, V_233) | ~c1_2(U_232, V_233) | ~c4_2(U_232, V_233)))). % 23.37/6.95 tff(c_2055, plain, (![U_14]: (c5_1(U_14) | c7_2(U_14, a56) | ~ndr1_1(U_14) | ~c1_2(U_14, a94) | ~c4_2(U_14, a94) | ssSkP8(U_14)))). % 23.37/6.95 tff(c_2057, plain, (~c4_2(a134, a108))). % 23.37/6.95 tff(c_2038, plain, (![U_206, V_207]: (c5_1(U_206) | c7_2(U_206, a56) | ~ndr1_1(U_206) | ~c6_2(U_206, V_207) | ~c1_2(U_206, V_207) | ~c4_2(U_206, V_207)))). % 23.37/6.95 tff(c_2037, plain, (ssSkP4(a44))). % 23.37/6.95 tff(c_2033, plain, (~c2_2(a44, a57))). % 23.37/6.95 tff(c_2009, plain, (![U_438]: (ssSkP4(U_438) | c8_1(U_438) | c4_2(U_438, a100) | c4_2(U_438, a57) | ~ndr1_1(U_438) | ~c2_2(U_438, a57)))). % 23.37/6.95 tff(c_2024, plain, (![U_441]: (ssSkP2(U_441) | c8_1(U_441) | c4_2(U_441, a100) | ~ndr1_1(U_441) | ~c2_2(U_441, a4)))). % 23.37/6.95 tff(c_2018, plain, (~c2_2(a35, a108))). % 23.37/6.95 tff(c_2019, plain, (ssSkC2)). % 23.37/6.95 tff(c_2017, plain, (~c2_2(a134, a108))). % 23.37/6.95 tff(c_2016, plain, (~c2_2(a136, a108))). % 23.37/6.95 tff(c_2006, plain, (![U_438]: (ssSkP3(U_438) | c8_1(U_438) | c4_2(U_438, a100) | c4_2(U_438, a22) | ~ndr1_1(U_438) | ~c2_2(U_438, a22)))). % 23.37/6.95 tff(c_2014, plain, (c4_2(a24, a26))). % 23.37/6.95 tff(c_2013, plain, (c3_1(a96))). % 23.37/6.95 tff(c_1955, plain, (![U_177, V_178]: (c8_1(U_177) | c4_2(U_177, a100) | c4_2(U_177, V_178) | c7_2(U_177, V_178) | ~ndr1_1(U_177) | ~c2_2(U_177, V_178)))). % 23.37/6.95 tff(c_1954, plain, (c6_1(a18))). % 23.37/6.95 tff(c_1934, plain, (![U_433]: (c2_1(U_433) | c6_1(U_433) | c7_1(U_433) | c1_2(U_433, a67) | ~c3_1(U_433) | ~ndr1_1(U_433) | ~c3_2(U_433, a67)))). % 23.37/6.95 tff(c_1938, plain, (![U_433]: (ssSkP4(U_433) | c7_1(U_433) | c1_2(U_433, a57) | ~c3_1(U_433) | ~ndr1_1(U_433) | ~c3_2(U_433, a57)))). % 23.37/6.95 tff(c_1951, plain, (~c3_2(a134, a108))). % 23.37/6.95 tff(c_1950, plain, (~c3_2(a35, a108))). % 23.37/6.95 tff(c_1949, plain, (~c3_2(a136, a108))). % 23.37/6.95 tff(c_1948, plain, (~c3_2(a24, a26))). % 23.37/6.95 tff(c_1935, plain, (![U_433]: (ssSkP3(U_433) | c7_1(U_433) | c1_2(U_433, a22) | ~c3_1(U_433) | ~ndr1_1(U_433) | ~c3_2(U_433, a22)))). % 23.37/6.95 tff(c_1946, plain, (ssSkP7(a35))). % 23.37/6.95 tff(c_1942, plain, (~c1_2(a35, a87))). % 23.37/6.95 tff(c_1886, plain, (![U_171, V_172]: (c7_1(U_171) | c1_2(U_171, V_172) | c7_2(U_171, V_172) | ~c3_1(U_171) | ~ndr1_1(U_171) | ~c3_2(U_171, V_172)))). % 23.37/6.95 tff(c_1885, plain, (~c1_2(a35, a57))). % 23.37/6.95 tff(c_1863, plain, (![U_134]: (~c5_2(a35, U_134) | ~c2_2(a35, U_134) | ~c1_2(a35, U_134)))). % 23.37/6.95 tff(c_1860, plain, (~c7_2(a35, a108))). % 23.37/6.95 tff(c_1859, plain, (~c5_2(a35, a108))). % 23.37/6.95 tff(c_1856, plain, (~c5_2(a136, a108))). % 23.37/6.95 tff(c_1855, plain, (c6_2(a136, a108))). % 23.37/6.95 tff(c_1854, plain, (~ssSkC18)). % 23.37/6.95 tff(c_1851, plain, (~c7_2(a136, a108))). % 23.37/6.95 tff(c_1842, plain, (ssSkC3)). % 23.37/6.95 tff(c_1841, plain, (ssSkP7(a90))). % 23.37/6.95 tff(c_1837, plain, (~c5_2(a90, a87))). % 23.37/6.95 tff(c_1827, plain, (![U_16]: (c7_1(U_16) | ~c7_2(U_16, a108) | ~ndr1_1(U_16) | ~c5_2(U_16, a87) | ssSkP7(U_16)))). % 23.37/6.95 tff(c_1834, plain, (~c7_2(a134, a108))). % 23.37/6.96 tff(c_1072, plain, (![U_165, V_166]: (c7_1(U_165) | ~c7_2(U_165, a108) | ~ndr1_1(U_165) | ~c8_2(U_165, V_166) | ~c5_2(U_165, V_166)))). % 23.37/6.96 tff(c_1791, plain, (~c5_1(a27))). % 23.37/6.96 tff(c_1790, plain, (~c5_1(a141))). % 23.37/6.96 tff(c_1789, plain, (~c5_1(a122))). % 23.37/6.96 tff(c_1782, plain, (c2_1(a52))). % 23.37/6.96 tff(c_1787, plain, (~c5_1(a117))). % 23.37/6.96 tff(c_1763, plain, (![V_146]: (c2_1(V_146) | ~c5_1(V_146) | ~c7_1(V_146)))). % 23.37/6.96 tff(c_1694, plain, (![U_17]: (c7_1(U_17) | ~c5_2(U_17, a108) | ~ndr1_1(U_17) | ssSkP7(U_17)))). % 23.37/6.96 tff(c_1628, plain, (![U_16]: (c7_1(U_16) | c6_2(U_16, a108) | ~ndr1_1(U_16) | ~c5_2(U_16, a87) | ssSkP7(U_16)))). % 23.37/6.96 tff(c_1680, plain, (~c5_2(a134, a108))). % 23.37/6.96 tff(c_1074, plain, (![U_163, V_164]: (c7_1(U_163) | ~c5_2(U_163, a108) | ~ndr1_1(U_163) | ~c8_2(U_163, V_164) | ~c5_2(U_163, V_164)))). % 23.37/6.96 tff(c_1638, plain, (c6_2(a134, a108))). % 23.37/6.96 tff(c_1637, plain, (~c5_2(a134, a135))). % 23.37/6.96 tff(c_1635, plain, (~c5_2(a47, a48))). % 23.37/6.96 tff(c_1080, plain, (![U_152, V_153]: (c7_1(U_152) | c6_2(U_152, a108) | ~ndr1_1(U_152) | ~c8_2(U_152, V_153) | ~c5_2(U_152, V_153)))). % 23.37/6.96 tff(c_1593, plain, (~c8_1(a134))). % 23.37/6.96 tff(c_1586, plain, (![V_130]: (c8_2(a134, V_130) | c1_2(a134, V_130)))). % 23.37/6.96 tff(c_1541, plain, (c6_1(a51))). % 23.37/6.96 tff(c_1540, plain, (~c8_1(a51))). % 23.37/6.96 tff(c_1528, plain, (~ndr1_1(a51))). % 23.37/6.96 tff(c_1527, plain, (ssSkP7(a52))). % 23.37/6.96 tff(c_1522, plain, (~c5_2(a52, a87))). % 23.37/6.96 tff(c_1473, plain, (![U_149]: (~c7_2(a52, U_149) | ~c8_2(a52, U_149) | ~c5_2(a52, U_149)))). % 23.37/6.96 tff(c_1514, plain, (~c8_1(a136))). % 23.37/6.96 tff(c_781, plain, (![U_78]: (c7_2(a136, U_78) | c3_2(a136, U_78) | c8_2(a136, U_78)))). % 23.37/6.96 tff(c_1507, plain, (~c1_2(a90, a94))). % 23.37/6.96 tff(c_1500, plain, (![U_148]: (~c6_2(a90, U_148) | ~c2_2(a90, U_148) | ~c1_2(a90, U_148)))). % 23.37/6.96 tff(c_1495, plain, (~c8_1(a65))). % 23.37/6.96 tff(c_1481, plain, (~ndr1_1(a65))). % 23.37/6.96 tff(c_1477, plain, (~c1_2(a35, a115))). % 23.37/6.96 tff(c_1475, plain, (![U_94]: (c6_1(U_94) | ~c7_1(U_94) | ~c2_2(U_94, a63)))). % 23.37/6.96 tff(c_1474, plain, (ndr1_1(a52))). % 23.37/6.96 tff(c_1447, plain, (![U_95]: (c6_1(U_95) | ~c7_1(U_95) | ~c5_2(U_95, a63)))). % 23.37/6.96 tff(c_1446, plain, (~ssSkC11)). % 23.37/6.96 tff(c_1438, plain, (![U_134]: (c8_2(a35, U_134) | ~c2_2(a35, U_134) | ~c1_2(a35, U_134)))). % 23.37/6.96 tff(c_1433, plain, (![U_74]: (c2_1(U_74) | c6_1(U_74) | ~c4_2(U_74, a67)))). % 23.37/6.96 tff(c_1430, plain, (![U_75]: (c2_1(U_75) | c6_1(U_75) | ~c7_2(U_75, a67)))). % 23.37/6.96 tff(c_1427, plain, (![U_76]: (c6_1(U_76) | c4_2(U_76, a63) | ~c7_1(U_76)))). % 23.37/6.96 tff(c_1425, plain, (c6_1(a120))). % 23.37/6.96 tff(c_1424, plain, (c6_1(a59))). % 23.37/6.96 tff(c_1423, plain, (~c7_1(a59))). % 23.37/6.96 tff(c_1422, plain, (~c8_1(a120))). % 23.37/6.96 tff(c_1410, plain, (~ndr1_1(a120))). % 23.37/6.96 tff(c_1408, plain, (~c8_1(a59))). % 23.37/6.96 tff(c_1395, plain, (c6_1(a113))). % 23.37/6.96 tff(c_1396, plain, (~ndr1_1(a59))). % 23.37/6.96 tff(c_1394, plain, (~c7_1(a113))). % 23.37/6.96 tff(c_1380, plain, (c6_1(a52))). % 23.37/6.96 tff(c_1381, plain, (~ndr1_1(a113))). % 23.37/6.96 tff(c_1379, plain, (c8_2(a134, a135))). % 23.37/6.96 tff(c_1378, plain, (c6_1(a27))). % 23.37/6.96 tff(c_1377, plain, (c6_1(a117))). % 23.37/6.96 tff(c_1373, plain, (c6_1(a122))). % 23.37/6.96 tff(c_1376, plain, (ssSkC5)). % 23.37/6.96 tff(c_1369, plain, (c6_1(a141))). % 23.37/6.96 tff(c_1348, plain, (~c7_1(a32))). % 23.37/6.96 tff(c_1349, plain, (![U_86]: (c4_1(U_86) | c6_1(U_86) | ~c8_1(U_86)))). % 23.37/6.96 tff(c_1336, plain, (c6_1(a34))). % 23.37/6.96 tff(c_1325, plain, (![U_51]: (c2_1(U_51) | c6_1(U_51) | ndr1_1(U_51)))). % 23.37/6.96 tff(c_1324, plain, (~c4_2(a134, a135))). % 23.37/6.96 tff(c_1323, plain, (c3_2(a134, a135))). % 23.37/6.96 tff(c_1322, plain, (ssSkC19)). % 23.37/6.96 tff(c_1319, plain, (~c4_2(a44, a87))). % 23.37/6.96 tff(c_1317, plain, (~c4_2(a44, a57))). % 23.37/6.96 tff(c_1318, plain, (c5_0)). % 23.37/6.96 tff(c_1316, plain, (~c4_2(a44, a69))). % 23.37/6.96 tff(c_1312, plain, (~c4_2(a44, a71))). % 23.37/6.96 tff(c_1315, plain, (~ssSkC17)). % 23.37/6.96 tff(c_1310, plain, (~c4_2(a44, a45))). % 23.37/6.96 tff(c_1311, plain, (ssSkC0)). % 23.37/6.96 tff(c_1282, plain, (![U_110]: (~c5_2(a44, U_110) | ~c4_2(a44, U_110)))). % 23.37/6.96 tff(c_1285, plain, (ndr1_1(a134))). % 23.37/6.96 tff(c_1275, plain, (~c1_1(a134))). % 23.37/6.96 tff(c_1273, plain, (~c8_1(a32))). % 23.37/6.97 tff(c_1269, plain, (~ndr1_1(a32))). % 23.37/6.97 tff(c_274, plain, (![U_29]: (ssSkP6(U_29) | ~c1_2(U_29, a71)))). % 23.37/6.97 tff(c_312, plain, (![U_39]: (ssSkP1(U_39) | ~c1_2(U_39, a2)))). % 23.37/6.97 tff(c_276, plain, (![U_30]: (ssSkP6(U_30) | ~c3_2(U_30, a71)))). % 23.37/6.97 tff(c_302, plain, (![U_34]: (ssSkP3(U_34) | ~c7_2(U_34, a22)))). % 23.37/6.97 tff(c_264, plain, (![U_27]: (ssSkP9(U_27) | ~c2_2(U_27, a101)))). % 23.37/6.97 tff(c_266, plain, (![U_28]: (ssSkP8(U_28) | ~c5_2(U_28, a94)))). % 23.37/6.97 tff(c_280, plain, (![U_32]: (ssSkP5(U_32) | ~c6_2(U_32, a69)))). % 23.37/6.97 tff(c_190, plain, (![U_23]: (ssSkP1(U_23) | c7_2(U_23, a2)))). % 23.37/6.97 tff(c_146, plain, (![U_18]: (ssSkP7(U_18) | c1_2(U_18, a87)))). % 23.37/6.97 tff(c_316, plain, (![U_41]: (ssSkP0(U_41) | ~c1_2(U_41, a1)))). % 23.37/6.97 tff(c_306, plain, (![U_36]: (ssSkP2(U_36) | ~c4_2(U_36, a4)))). % 23.37/6.97 tff(c_162, plain, (![U_22]: (ssSkP4(U_22) | c5_2(U_22, a57)))). % 23.37/6.97 tff(c_314, plain, (![U_40]: (ssSkP0(U_40) | ~c4_2(U_40, a1)))). % 23.37/6.97 tff(c_128, plain, (![U_12]: (ssSkP9(U_12) | c7_2(U_12, a101)))). % 23.37/6.97 tff(c_1245, plain, (ssSkC22)). % 23.37/6.97 tff(c_130, plain, (![U_13]: (ssSkP9(U_13) | c4_2(U_13, a101)))). % 23.37/6.97 tff(c_308, plain, (![U_37]: (ssSkP2(U_37) | ~c3_2(U_37, a4)))). % 23.37/6.97 tff(c_1110, plain, (![U_88]: (~c8_1(U_88) | ~c7_2(U_88, a115)))). % 23.37/6.97 tff(c_1241, plain, (ssSkC16)). % 23.37/6.97 tff(c_160, plain, (![U_21]: (ssSkP4(U_21) | c2_2(U_21, a57)))). % 23.37/6.97 tff(c_158, plain, (![U_20]: (ssSkP5(U_20) | c5_2(U_20, a69)))). % 23.37/6.97 tff(c_1092, plain, (![U_87]: (~c8_1(U_87) | ~c3_2(U_87, a115)))). % 23.37/6.97 tff(c_144, plain, (![U_17]: (ssSkP7(U_17) | c5_2(U_17, a87)))). % 23.37/6.97 tff(c_854, plain, (![U_89]: (~c8_1(U_89) | ~c8_2(U_89, a115)))). % 23.37/6.97 tff(c_310, plain, (![U_38]: (ssSkP2(U_38) | ~c7_2(U_38, a4)))). % 23.37/6.97 tff(c_156, plain, (![U_19]: (ssSkP6(U_19) | c5_2(U_19, a71)))). % 23.37/6.97 tff(c_282, plain, (![U_33]: (ssSkP4(U_33) | ~c7_2(U_33, a57)))). % 23.37/6.97 tff(c_1232, plain, (ssSkC1)). % 23.37/6.97 tff(c_142, plain, (![U_16]: (ssSkP7(U_16) | c8_2(U_16, a87)))). % 23.37/6.97 tff(c_304, plain, (![U_35]: (ssSkP3(U_35) | ~c6_2(U_35, a22)))). % 23.37/6.97 tff(c_278, plain, (![U_31]: (ssSkP5(U_31) | ~c1_2(U_31, a69)))). % 23.37/6.97 tff(c_134, plain, (![U_15]: (ssSkP8(U_15) | c2_2(U_15, a94)))). % 23.37/6.97 tff(c_132, plain, (![U_14]: (ssSkP8(U_14) | c6_2(U_14, a94)))). % 23.37/6.97 tff(c_192, plain, (![U_24]: (ssSkP1(U_24) | c4_2(U_24, a2)))). % 23.37/6.97 tff(c_1224, plain, (~c8_1(a34))). % 23.37/6.97 tff(c_1220, plain, (~ndr1_1(a34))). % 23.37/6.97 tff(c_1219, plain, (~c8_2(a44, a45))). % 23.37/6.97 tff(c_1218, plain, (c7_2(a90, a92))). % 23.37/6.97 tff(c_1217, plain, (~c1_2(a47, a49))). % 23.37/6.97 tff(c_1216, plain, (c5_2(a37, a38))). % 23.37/6.97 tff(c_1215, plain, (c1_2(a24, a25))). % 23.37/6.97 tff(c_1214, plain, (~c2_2(a83, a84))). % 23.37/6.97 tff(c_1213, plain, (c4_2(a37, a38))). % 23.37/6.97 tff(c_1212, plain, (c2_2(a24, a26))). % 23.37/6.97 tff(c_1211, plain, (c3_2(a90, a91))). % 23.37/6.97 tff(c_1210, plain, (c1_2(a90, a91))). % 23.37/6.97 tff(c_1209, plain, (c3_2(a24, a25))). % 23.37/6.97 tff(c_1208, plain, (c3_2(a37, a38))). % 23.37/6.97 tff(c_1207, plain, (c5_2(a44, a45))). % 23.37/6.97 tff(c_1206, plain, (~c1_2(a47, a48))). % 23.37/6.97 tff(c_1205, plain, (c5_2(a83, a84))). % 23.37/6.97 tff(c_1203, plain, (~ssSkC7)). % 23.37/6.97 tff(c_852, plain, (![U_58]: (ndr1_1(U_58) | ~c8_1(U_58)))). % 23.37/6.97 tff(c_1201, plain, (~c2_2(a47, a49))). % 23.37/6.97 tff(c_1200, plain, (~ssSkC10)). % 23.37/6.97 tff(c_1199, plain, (c2_2(a27, a28))). % 23.37/6.97 tff(c_1198, plain, (~c2_2(a35, a36))). % 23.37/6.97 tff(c_1197, plain, (~c2_2(a47, a48))). % 23.37/6.97 tff(c_1196, plain, (c8_2(a141, a142))). % 23.37/6.97 tff(c_1195, plain, (~c3_2(a141, a142))). % 23.37/6.97 tff(c_1194, plain, (c3_2(a83, a84))). % 23.37/6.97 tff(c_1192, plain, (~c3_2(a35, a36))). % 23.37/6.97 tff(c_1191, plain, (~c6_2(a27, a28))). % 23.37/6.97 tff(c_1184, plain, (c7_1(a52))). % 23.37/6.97 tff(c_1190, plain, (~ssSkC4)). % 23.37/6.97 tff(c_1185, plain, (c7_1(a141))). % 23.37/6.97 tff(c_1186, plain, (c7_1(a27))). % 23.37/6.97 tff(c_1188, plain, (c7_1(a117))). % 23.37/6.97 tff(c_1189, plain, (c7_2(a47, a49))). % 23.37/6.97 tff(c_1187, plain, (c7_1(a122))). % 23.37/6.97 tff(c_1050, plain, (![U_44]: (c7_1(U_44) | ~c8_1(U_44)))). % 23.37/6.97 tff(c_1167, plain, (~c6_2(a24, a25))). % 23.37/6.97 tff(c_1166, plain, (~c4_2(a90, a92))). % 23.37/6.97 tff(c_1165, plain, (~c7_2(a24, a26))). % 23.37/6.97 tff(c_44, plain, (![U_3]: (ssSkP7(U_3) | ndr1_1(U_3)))). % 23.37/6.97 tff(c_1163, plain, (~c6_2(a24, a26))). % 23.37/6.97 tff(c_1162, plain, (~ssSkC15)). % 23.37/6.97 tff(c_40, plain, (![U_2]: (ssSkP8(U_2) | ndr1_1(U_2)))). % 23.37/6.97 tff(c_48, plain, (![U_4]: (ssSkP6(U_4) | ndr1_1(U_4)))). % 23.37/6.97 tff(c_1158, plain, (~c4_2(a27, a28))). % 23.37/6.97 tff(c_1157, plain, (~c4_2(a35, a36))). % 23.37/6.97 tff(c_56, plain, (![U_6]: (ssSkP4(U_6) | ndr1_1(U_6)))). % 23.37/6.97 tff(c_78, plain, (![U_8]: (ssSkP2(U_8) | ndr1_1(U_8)))). % 23.37/6.97 tff(c_80, plain, (![U_9]: (ssSkP1(U_9) | ndr1_1(U_9)))). % 23.37/6.97 tff(c_76, plain, (![U_7]: (ssSkP3(U_7) | ndr1_1(U_7)))). % 23.37/6.97 tff(c_82, plain, (![U_10]: (ssSkP0(U_10) | ndr1_1(U_10)))). % 23.37/6.97 tff(c_1151, plain, (c8_2(a47, a48))). % 23.37/6.97 tff(c_1150, plain, (~c3_2(a90, a92))). % 23.37/6.97 tff(c_50, plain, (![U_5]: (ssSkP5(U_5) | ndr1_1(U_5)))). % 23.37/6.97 tff(c_38, plain, (![U_1]: (ssSkP9(U_1) | ndr1_1(U_1)))). % 23.37/6.97 tff(c_1147, plain, (~ssSkC12)). % 23.37/6.97 tff(c_1146, plain, (c8_1(a52))). % 23.37/6.97 tff(c_20, plain, (c5_2(a136, a137))). % 23.37/6.97 tff(c_1145, plain, (~c3_1(a83))). % 23.37/6.97 tff(c_1144, plain, (~c4_1(a35))). % 23.37/6.97 tff(c_1143, plain, (~c2_1(a24))). % 23.37/6.97 tff(c_16, plain, (c1_2(a136, a137))). % 23.37/6.97 tff(c_759, plain, (c5_2(a122, a123))). % 23.37/6.97 tff(c_1142, plain, (c5_1(a52))). % 23.37/6.97 tff(c_1141, plain, (ndr1_1(a47))). % 23.37/6.98 tff(c_753, plain, (~c3_2(a122, a123))). % 23.37/6.98 tff(c_1140, plain, (ndr1_1(a141))). % 23.37/6.98 tff(c_1139, plain, (~c6_1(a37))). % 23.37/6.98 tff(c_1138, plain, (~c4_1(a113))). % 23.37/6.98 tff(c_1137, plain, (c8_1(a141))). % 23.37/6.98 tff(c_1136, plain, (~ssSkC21)). % 23.37/6.98 tff(c_756, plain, (~c1_2(a122, a123))). % 23.37/6.98 tff(c_1135, plain, (c8_1(a27))). % 23.37/6.98 tff(c_1134, plain, (~c7_1(a83))). % 23.37/6.98 tff(c_18, plain, (c3_2(a136, a137))). % 23.37/6.98 tff(c_1133, plain, (ndr1_1(a37))). % 23.37/6.98 tff(c_1132, plain, (~c8_0)). % 23.37/6.98 tff(c_1131, plain, (ndr1_1(a90))). % 23.37/6.98 tff(c_1130, plain, (~c2_1(a44))). % 23.37/6.98 tff(c_1129, plain, (ndr1_1(a44))). % 23.37/6.98 tff(c_1128, plain, (ndr1_1(a83))). % 23.37/6.98 tff(c_1127, plain, (~c1_1(a37))). % 23.37/6.98 tff(c_1126, plain, (ndr1_1(a24))). % 23.37/6.98 tff(c_1125, plain, (~ssSkC14)). % 23.37/6.98 tff(c_1124, plain, (~c8_1(a113))). % 23.37/6.98 tff(c_1123, plain, (c6_1(a65))). % 23.37/6.98 tff(c_1122, plain, (c2_1(a32))). % 23.37/6.98 tff(c_1121, plain, (c5_1(a65))). % 23.37/6.98 tff(c_1120, plain, (ndr1_1(a35))). % 23.37/6.98 tff(c_1119, plain, (~c5_1(a120))). % 23.37/6.98 tff(c_1118, plain, (~c4_1(a141))). % 23.37/6.98 tff(c_1117, plain, (ndr1_1(a27))). % 23.37/6.98 tff(c_1116, plain, (~c1_0)). % 23.37/6.98 tff(c_1115, plain, (~c6_1(a47))). % 23.37/6.98 tff(c_754, plain, (ndr1_1(a122))). % 23.37/6.98 tff(c_761, plain, (~c7_1(a51))). % 23.37/6.98 tff(c_760, plain, (~c4_1(a59))). % 23.37/6.98 tff(c_777, plain, (c5_1(a51))). % 23.37/6.98 tff(c_750, plain, (c8_1(a122))). % 23.37/6.98 tff(c_746, plain, (~c1_1(a122))). % 23.37/6.98 tff(c_727, plain, (~c2_1(a117))). % 23.37/6.98 tff(c_747, plain, (c3_1(a59))). % 23.37/6.98 tff(c_8, plain, (ndr1_1(a136))). % 23.37/6.98 tff(c_10, plain, (c5_1(a136))). % 23.37/6.98 tff(c_732, plain, (c8_1(a117))). % 23.37/6.98 tff(c_2, plain, (ndr1_0)). % 23.37/6.98 tff(c_4, plain, (c6_0)). % 23.37/6.98 tff(c_783, plain, (c7_0)). % 23.37/6.98 tff(c_6, plain, (c4_0)). % 23.37/6.98 tff(c_12, plain, (~c2_0)). % 23.37/6.98 tff(c_14, plain, (~c3_0)). % 23.37/6.98 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 23.37/6.98 %------------------------------------------------------------------------------