%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN418+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 : n017.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:31 PM UTC 2025 % Result : CounterSatisfiable 20.25s 6.73s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.13 % Problem : SYN418+1 : TPTP v9.0.0. Released v2.1.0. % 0.10/0.14 % 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.14/0.34 % Computer : n017.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 07:23:40 EDT 2025 % 0.14/0.34 % CPUTime : % 20.25/6.73 % 20.25/6.73 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.25/6.73 % 20.25/6.73 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.25/6.74 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ndr1_0 > c9_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > c10_0 > a99 > a98 > a97 > a96 > a95 > a94 > a93 > a92 > a91 > a90 > a9 > a89 > a88 > a87 > a86 > a85 > a84 > a83 > a82 > a81 > a80 > a8 > a79 > a78 > a77 > a76 > a75 > a74 > a73 > a72 > a71 > a70 > a7 > a69 > a68 > a67 > a66 > a65 > a64 > a63 > a62 > a61 > a60 > a6 > a59 > a58 > a57 > a56 > a55 > a54 > a53 > a52 > a51 > a50 > 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 > a21 > a20 > a2 > a19 > a18 > a17 > a16 > a15 > a146 > a145 > a144 > a143 > a142 > a141 > a140 > a14 > a139 > a138 > a137 > a136 > a135 > a134 > a133 > a132 > a131 > a130 > a13 > a129 > a128 > a127 > a126 > a125 > a124 > a123 > a122 > a121 > a120 > a12 > a119 > a118 > a117 > a116 > a115 > a114 > a113 > a112 > a111 > a110 > a11 > a109 > a108 > a107 > a106 > a105 > a104 > a103 > a102 > a101 > a100 > a10 > a1 % 20.25/6.74 % 20.25/6.74 %Foreground sorts: % 20.25/6.74 % 20.25/6.74 % 20.25/6.74 %Background operators: % 20.25/6.74 % 20.25/6.74 % 20.25/6.74 %Foreground operators: % 20.25/6.74 tff(a99, type, a99: $i). % 20.25/6.74 tff(a143, type, a143: $i). % 20.25/6.74 tff(c7_0, type, c7_0: $o). % 20.25/6.74 tff(a1, type, a1: $i). % 20.25/6.74 tff(a94, type, a94: $i). % 20.25/6.74 tff(a68, type, a68: $i). % 20.25/6.74 tff(a101, type, a101: $i). % 20.25/6.74 tff(a100, type, a100: $i). % 20.25/6.74 tff(a108, type, a108: $i). % 20.25/6.74 tff(a89, type, a89: $i). % 20.25/6.74 tff(a64, type, a64: $i). % 20.25/6.74 tff(a112, type, a112: $i). % 20.25/6.74 tff(a3, type, a3: $i). % 20.25/6.74 tff(a97, type, a97: $i). % 20.25/6.74 tff(a32, type, a32: $i). % 20.25/6.74 tff(a35, type, a35: $i). % 20.25/6.74 tff(c4_0, type, c4_0: $o). % 20.25/6.74 tff(a47, type, a47: $i). % 20.25/6.74 tff(a73, type, a73: $i). % 20.25/6.74 tff(a34, type, a34: $i). % 20.25/6.74 tff(a146, type, a146: $i). % 20.25/6.74 tff(a69, type, a69: $i). % 20.25/6.74 tff(a124, type, a124: $i). % 20.25/6.74 tff(a122, type, a122: $i). % 20.25/6.74 tff(a141, type, a141: $i). % 20.25/6.74 tff(a120, type, a120: $i). % 20.25/6.74 tff(a61, type, a61: $i). % 20.25/6.74 tff(c3_0, type, c3_0: $o). % 20.25/6.74 tff(a140, type, a140: $i). % 20.25/6.74 tff(a26, type, a26: $i). % 20.25/6.74 tff(a138, type, a138: $i). % 20.25/6.74 tff(a103, type, a103: $i). % 20.25/6.74 tff(c1_2, type, c1_2: ($i * $i) > $o). % 20.25/6.74 tff(a60, type, a60: $i). % 20.25/6.74 tff(a40, type, a40: $i). % 20.25/6.74 tff(a113, type, a113: $i). % 20.25/6.74 tff(a130, type, a130: $i). % 20.25/6.74 tff(a36, type, a36: $i). % 20.25/6.74 tff(a75, type, a75: $i). % 20.25/6.74 tff(a62, type, a62: $i). % 20.25/6.74 tff(a15, type, a15: $i). % 20.25/6.74 tff(a145, type, a145: $i). % 20.25/6.74 tff(a119, type, a119: $i). % 20.25/6.74 tff(a93, type, a93: $i). % 20.25/6.74 tff(a107, type, a107: $i). % 20.25/6.74 tff(a72, type, a72: $i). % 20.25/6.74 tff(a67, type, a67: $i). % 20.25/6.74 tff(a131, type, a131: $i). % 20.25/6.74 tff(a31, type, a31: $i). % 20.25/6.74 tff(a86, type, a86: $i). % 20.25/6.74 tff(a88, type, a88: $i). % 20.25/6.74 tff(c8_0, type, c8_0: $o). % 20.25/6.74 tff(a83, type, a83: $i). % 20.25/6.74 tff(a63, type, a63: $i). % 20.25/6.74 tff(a23, type, a23: $i). % 20.25/6.74 tff(a12, type, a12: $i). % 20.25/6.74 tff(a10, type, a10: $i). % 20.25/6.74 tff(a126, type, a126: $i). % 20.25/6.74 tff(a110, type, a110: $i). % 20.25/6.74 tff(a78, type, a78: $i). % 20.25/6.74 tff(a33, type, a33: $i). % 20.25/6.74 tff(a121, type, a121: $i). % 20.25/6.74 tff(a41, type, a41: $i). % 20.25/6.74 tff(a43, type, a43: $i). % 20.25/6.74 tff(a29, type, a29: $i). % 20.25/6.74 tff(a17, type, a17: $i). % 20.25/6.74 tff(a74, type, a74: $i). % 20.25/6.74 tff(a51, type, a51: $i). % 20.25/6.74 tff(a136, type, a136: $i). % 20.25/6.74 tff(a125, type, a125: $i). % 20.25/6.74 tff(c5_0, type, c5_0: $o). % 20.25/6.74 tff(a127, type, a127: $i). % 20.25/6.74 tff(a98, type, a98: $i). % 20.25/6.74 tff(a111, type, a111: $i). % 20.25/6.74 tff(a142, type, a142: $i). % 20.25/6.74 tff(a28, type, a28: $i). % 20.25/6.74 tff(a58, type, a58: $i). % 20.25/6.74 tff(c6_0, type, c6_0: $o). % 20.25/6.74 tff(a84, type, a84: $i). % 20.25/6.74 tff(a104, type, a104: $i). % 20.25/6.74 tff(c8_2, type, c8_2: ($i * $i) > $o). % 20.25/6.74 tff(a14, type, a14: $i). % 20.25/6.74 tff(a22, type, a22: $i). % 20.25/6.74 tff(a87, type, a87: $i). % 20.25/6.74 tff(a134, type, a134: $i). % 20.25/6.74 tff(a139, type, a139: $i). % 20.25/6.74 tff(a77, type, a77: $i). % 20.25/6.74 tff(a18, type, a18: $i). % 20.25/6.74 tff(a46, type, a46: $i). % 20.25/6.74 tff(a7, type, a7: $i). % 20.25/6.74 tff(a11, type, a11: $i). % 20.25/6.74 tff(a118, type, a118: $i). % 20.25/6.74 tff(a76, type, a76: $i). % 20.25/6.74 tff(a39, type, a39: $i). % 20.25/6.74 tff(a25, type, a25: $i). % 20.25/6.74 tff(c1_0, type, c1_0: $o). % 20.25/6.74 tff(a71, type, a71: $i). % 20.25/6.74 tff(c8_1, type, c8_1: $i > $o). % 20.25/6.74 tff(a53, type, a53: $i). % 20.25/6.74 tff(a38, type, a38: $i). % 20.25/6.74 tff(a50, type, a50: $i). % 20.25/6.74 tff(a105, type, a105: $i). % 20.25/6.74 tff(c2_1, type, c2_1: $i > $o). % 20.25/6.74 tff(a9, type, a9: $i). % 20.25/6.74 tff(a129, type, a129: $i). % 20.25/6.74 tff(a2, type, a2: $i). % 20.25/6.74 tff(ndr1_1, type, ndr1_1: $i > $o). % 20.25/6.74 tff(c2_0, type, c2_0: $o). % 20.25/6.74 tff(c4_1, type, c4_1: $i > $o). % 20.25/6.74 tff(c9_1, type, c9_1: $i > $o). % 20.25/6.74 tff(c10_1, type, c10_1: $i > $o). % 20.25/6.74 tff(a45, type, a45: $i). % 20.25/6.74 tff(c10_0, type, c10_0: $o). % 20.25/6.74 tff(a6, type, a6: $i). % 20.25/6.74 tff(c6_2, type, c6_2: ($i * $i) > $o). % 20.25/6.74 tff(a90, type, a90: $i). % 20.25/6.74 tff(a52, type, a52: $i). % 20.25/6.74 tff(a80, type, a80: $i). % 20.25/6.74 tff(a21, type, a21: $i). % 20.25/6.74 tff(a123, type, a123: $i). % 20.25/6.74 tff(a116, type, a116: $i). % 20.25/6.74 tff(a20, type, a20: $i). % 20.25/6.74 tff(a66, type, a66: $i). % 20.25/6.74 tff(a92, type, a92: $i). % 20.25/6.74 tff(a79, type, a79: $i). % 20.25/6.74 tff(a57, type, a57: $i). % 20.25/6.74 tff(a4, type, a4: $i). % 20.25/6.74 tff(ndr1_0, type, ndr1_0: $o). % 20.25/6.74 tff(a48, type, a48: $i). % 20.25/6.74 tff(a44, type, a44: $i). % 20.25/6.74 tff(a117, type, a117: $i). % 20.25/6.74 tff(a42, type, a42: $i). % 20.25/6.74 tff(c9_2, type, c9_2: ($i * $i) > $o). % 20.25/6.74 tff(c10_2, type, c10_2: ($i * $i) > $o). % 20.25/6.74 tff(a85, type, a85: $i). % 20.25/6.74 tff(a30, type, a30: $i). % 20.25/6.74 tff(a56, type, a56: $i). % 20.25/6.74 tff(a54, type, a54: $i). % 20.25/6.74 tff(a137, type, a137: $i). % 20.25/6.74 tff(a133, type, a133: $i). % 20.25/6.74 tff(a49, type, a49: $i). % 20.25/6.74 tff(a5, type, a5: $i). % 20.25/6.74 tff(c1_1, type, c1_1: $i > $o). % 20.25/6.74 tff(a16, type, a16: $i). % 20.25/6.74 tff(a115, type, a115: $i). % 20.25/6.74 tff(a19, type, a19: $i). % 20.25/6.74 tff(a96, type, a96: $i). % 20.25/6.74 tff(a27, type, a27: $i). % 20.25/6.74 tff(c5_2, type, c5_2: ($i * $i) > $o). % 20.25/6.74 tff(a70, type, a70: $i). % 20.25/6.74 tff(a37, type, a37: $i). % 20.25/6.74 tff(c9_0, type, c9_0: $o). % 20.25/6.74 tff(c7_1, type, c7_1: $i > $o). % 20.25/6.74 tff(c6_1, type, c6_1: $i > $o). % 20.25/6.74 tff(a95, type, a95: $i). % 20.25/6.74 tff(a135, type, a135: $i). % 20.25/6.74 tff(c4_2, type, c4_2: ($i * $i) > $o). % 20.25/6.74 tff(a114, type, a114: $i). % 20.25/6.74 tff(a82, type, a82: $i). % 20.25/6.74 tff(a55, type, a55: $i). % 20.25/6.74 tff(a8, type, a8: $i). % 20.25/6.74 tff(a144, type, a144: $i). % 20.25/6.74 tff(a106, type, a106: $i). % 20.25/6.74 tff(a91, type, a91: $i). % 20.25/6.74 tff(c5_1, type, c5_1: $i > $o). % 20.25/6.74 tff(a13, type, a13: $i). % 20.25/6.74 tff(a81, type, a81: $i). % 20.25/6.74 tff(c7_2, type, c7_2: ($i * $i) > $o). % 20.25/6.74 tff(c3_2, type, c3_2: ($i * $i) > $o). % 20.25/6.74 tff(a24, type, a24: $i). % 20.25/6.74 tff(a109, type, a109: $i). % 20.25/6.74 tff(c2_2, type, c2_2: ($i * $i) > $o). % 20.25/6.74 tff(a102, type, a102: $i). % 20.25/6.74 tff(a65, type, a65: $i). % 20.25/6.74 tff(a128, type, a128: $i). % 20.25/6.74 tff(a59, type, a59: $i). % 20.25/6.74 tff(a132, type, a132: $i). % 20.25/6.74 tff(c3_1, type, c3_1: $i > $o). % 20.25/6.74 % 20.25/6.74 %Saturated clause set: % 20.25/6.75 tff(c_10036, plain, (![X119_236, X26_537, X25_538]: (c3_2(X119_236, X26_537) | c5_2(X119_236, X26_537) | ~c4_2(X119_236, X26_537) | ~c5_2(X119_236, X25_538) | c10_2(X119_236, X25_538) | ~c2_2(X119_236, X25_538) | ~c6_1(X119_236) | c4_1(X119_236) | ~c10_2(X119_236, a131) | c2_2(X119_236, a89) | ~c6_2(X119_236, a89) | ~c6_2(X119_236, a39) | ~c7_2(X119_236, a39) | ~ndr1_1(X119_236)))). % 20.25/6.75 tff(c_10038, plain, (![X119_230, X26_537, X25_538]: (c3_2(X119_230, X26_537) | c5_2(X119_230, X26_537) | ~c4_2(X119_230, X26_537) | ~c5_2(X119_230, X25_538) | c10_2(X119_230, X25_538) | ~c2_2(X119_230, X25_538) | ~c6_1(X119_230) | c4_1(X119_230) | c2_2(X119_230, a131) | c2_2(X119_230, a89) | ~c6_2(X119_230, a89) | ~c6_2(X119_230, a39) | ~c7_2(X119_230, a39) | ~ndr1_1(X119_230)))). % 20.25/6.75 tff(c_10037, plain, (![X119_224, X26_537, X25_538]: (c3_2(X119_224, X26_537) | c5_2(X119_224, X26_537) | ~c4_2(X119_224, X26_537) | ~c5_2(X119_224, X25_538) | c10_2(X119_224, X25_538) | ~c2_2(X119_224, X25_538) | ~c6_1(X119_224) | c4_1(X119_224) | ~c1_2(X119_224, a131) | c2_2(X119_224, a89) | ~c6_2(X119_224, a89) | ~c6_2(X119_224, a39) | ~c7_2(X119_224, a39) | ~ndr1_1(X119_224)))). % 20.25/6.75 tff(c_10043, plain, (![X119_168, X26_537, X25_538, X121_172]: (c3_2(X119_168, X26_537) | c5_2(X119_168, X26_537) | ~c4_2(X119_168, X26_537) | ~c5_2(X119_168, X25_538) | c10_2(X119_168, X25_538) | ~c2_2(X119_168, X25_538) | ~c10_2(X119_168, a131) | c2_2(X119_168, X121_172) | c9_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, a39) | ~c7_2(X119_168, a39) | ~ndr1_1(X119_168)))). % 20.25/6.75 tff(c_10049, plain, (![X119_168, X26_537, X25_538, X121_172]: (c3_2(X119_168, X26_537) | c5_2(X119_168, X26_537) | ~c4_2(X119_168, X26_537) | ~c5_2(X119_168, X25_538) | c10_2(X119_168, X25_538) | ~c2_2(X119_168, X25_538) | ~c1_2(X119_168, a131) | c2_2(X119_168, X121_172) | c9_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, a39) | ~c7_2(X119_168, a39) | ~ndr1_1(X119_168)))). % 20.25/6.75 tff(c_10046, plain, (![X119_168, X26_537, X25_538, X121_172]: (c3_2(X119_168, X26_537) | c5_2(X119_168, X26_537) | ~c4_2(X119_168, X26_537) | ~c5_2(X119_168, X25_538) | c10_2(X119_168, X25_538) | ~c2_2(X119_168, X25_538) | c2_2(X119_168, a131) | c2_2(X119_168, X121_172) | c9_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, a39) | ~c7_2(X119_168, a39) | ~ndr1_1(X119_168)))). % 20.25/6.75 tff(c_10105, plain, (![X24_39, X26_43, X25_42]: (c2_2(X24_39, a39) | c3_2(X24_39, X26_43) | c5_2(X24_39, X26_43) | ~c4_2(X24_39, X26_43) | ~c5_2(X24_39, X25_42) | c10_2(X24_39, X25_42) | ~c2_2(X24_39, X25_42) | ~ndr1_1(X24_39)))). % 20.25/6.75 tff(c_10102, plain, (~c2_2(a3, a4))). % 20.25/6.75 tff(c_10101, plain, (~c2_2(a119, a120))). % 20.25/6.75 tff(c_10089, plain, (![X24_39, X26_43, X25_42]: (~c3_2(X24_39, a39) | c3_2(X24_39, X26_43) | c5_2(X24_39, X26_43) | ~c4_2(X24_39, X26_43) | ~c5_2(X24_39, X25_42) | c10_2(X24_39, X25_42) | ~c2_2(X24_39, X25_42) | ~ndr1_1(X24_39)))). % 20.25/6.75 tff(c_10062, plain, (~c7_2(a3, a39))). % 20.25/6.75 tff(c_10061, plain, (~c7_2(a119, a39))). % 20.25/6.75 tff(c_9988, plain, (![X24_39, X26_43, X25_42]: (~c9_2(X24_39, a39) | c3_2(X24_39, X26_43) | c5_2(X24_39, X26_43) | ~c4_2(X24_39, X26_43) | ~c5_2(X24_39, X25_42) | c10_2(X24_39, X25_42) | ~c2_2(X24_39, X25_42) | ~ndr1_1(X24_39)))). % 20.25/6.75 tff(c_9974, plain, (c2_2(a37, a38))). % 20.25/6.75 tff(c_8789, plain, (![X121_338, X119_168, X120_340, X121_172, X120_171]: (c7_2(X119_168, X121_338) | c8_2(X119_168, X121_338) | c4_1(X119_168) | c1_2(X119_168, X121_172) | c2_2(X119_168, X121_338) | ~c6_2(X119_168, X121_338) | ~c6_2(X119_168, X120_340) | c9_2(X119_168, X120_340) | ~c7_2(X119_168, X120_340) | c2_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.75 tff(c_8864, plain, (![X119_168, X121_342, X120_344, X121_172, X120_171]: (c7_2(X119_168, X121_342) | c8_2(X119_168, X121_342) | c4_1(X119_168) | c1_2(X119_168, X121_172) | c2_2(X119_168, X121_342) | ~c6_2(X119_168, X121_342) | ~c6_2(X119_168, X120_344) | c9_2(X119_168, X120_344) | ~c7_2(X119_168, X120_344) | ~c10_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.75 tff(c_9948, plain, (~c1_2(a37, a131))). % 20.25/6.75 tff(c_8948, plain, (![X119_168, X121_172, X121_346, X120_348, X120_171]: (c7_2(X119_168, X121_346) | c8_2(X119_168, X121_346) | c4_1(X119_168) | c1_2(X119_168, X121_172) | c2_2(X119_168, X121_346) | ~c6_2(X119_168, X121_346) | ~c6_2(X119_168, X120_348) | c9_2(X119_168, X120_348) | ~c7_2(X119_168, X120_348) | ~c1_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.75 tff(c_7768, plain, (![X119_247, X17_31, X16_30, X120_248]: (~c10_2(X119_247, X17_31) | ~c1_2(X119_247, X17_31) | c9_2(X119_247, X17_31) | c1_2(X119_247, X16_30) | c3_2(X119_247, X16_30) | c9_2(X119_247, X16_30) | c10_2(X119_247, X120_248) | ~c1_2(X119_247, X120_248) | ~c6_1(X119_247) | c4_1(X119_247) | c2_2(X119_247, a131) | c2_2(X119_247, a89) | ~c6_2(X119_247, a89) | ~c6_2(X119_247, X120_248) | ~c7_2(X119_247, X120_248) | ~ndr1_1(X119_247)))). % 20.25/6.75 tff(c_7894, plain, (![X119_253, X17_31, X16_30, X121_254]: (~c10_2(X119_253, X17_31) | ~c1_2(X119_253, X17_31) | c9_2(X119_253, X17_31) | c1_2(X119_253, X16_30) | c3_2(X119_253, X16_30) | c9_2(X119_253, X16_30) | c10_2(X119_253, X121_254) | ~c1_2(X119_253, X121_254) | ~c6_1(X119_253) | c4_1(X119_253) | c2_2(X119_253, a131) | c2_2(X119_253, X121_254) | ~c6_2(X119_253, X121_254) | ~c6_2(X119_253, a89) | ~c7_2(X119_253, a89) | ~ndr1_1(X119_253)))). % 20.25/6.75 tff(c_7810, plain, (![X119_249, X17_31, X16_30, X120_250]: (~c10_2(X119_249, X17_31) | ~c1_2(X119_249, X17_31) | c9_2(X119_249, X17_31) | c1_2(X119_249, X16_30) | c3_2(X119_249, X16_30) | c9_2(X119_249, X16_30) | c10_2(X119_249, X120_250) | ~c1_2(X119_249, X120_250) | ~c6_1(X119_249) | c4_1(X119_249) | ~c1_2(X119_249, a131) | c2_2(X119_249, a89) | ~c6_2(X119_249, a89) | ~c6_2(X119_249, X120_250) | ~c7_2(X119_249, X120_250) | ~ndr1_1(X119_249)))). % 20.25/6.75 tff(c_7852, plain, (![X119_251, X17_31, X16_30, X120_252]: (~c10_2(X119_251, X17_31) | ~c1_2(X119_251, X17_31) | c9_2(X119_251, X17_31) | c1_2(X119_251, X16_30) | c3_2(X119_251, X16_30) | c9_2(X119_251, X16_30) | c10_2(X119_251, X120_252) | ~c1_2(X119_251, X120_252) | ~c6_1(X119_251) | c4_1(X119_251) | ~c10_2(X119_251, a131) | c2_2(X119_251, a89) | ~c6_2(X119_251, a89) | ~c6_2(X119_251, X120_252) | ~c7_2(X119_251, X120_252) | ~ndr1_1(X119_251)))). % 20.25/6.75 tff(c_7680, plain, (![X119_242, X17_31, X16_30, X121_243]: (~c10_2(X119_242, X17_31) | ~c1_2(X119_242, X17_31) | c9_2(X119_242, X17_31) | c1_2(X119_242, X16_30) | c3_2(X119_242, X16_30) | c9_2(X119_242, X16_30) | c10_2(X119_242, X121_243) | ~c1_2(X119_242, X121_243) | ~c6_1(X119_242) | c4_1(X119_242) | ~c10_2(X119_242, a131) | c2_2(X119_242, X121_243) | ~c6_2(X119_242, X121_243) | ~c6_2(X119_242, a89) | ~c7_2(X119_242, a89) | ~ndr1_1(X119_242)))). % 20.25/6.75 tff(c_7725, plain, (![X119_245, X17_31, X16_30, X121_246]: (~c10_2(X119_245, X17_31) | ~c1_2(X119_245, X17_31) | c9_2(X119_245, X17_31) | c1_2(X119_245, X16_30) | c3_2(X119_245, X16_30) | c9_2(X119_245, X16_30) | c10_2(X119_245, X121_246) | ~c1_2(X119_245, X121_246) | ~c6_1(X119_245) | c4_1(X119_245) | ~c1_2(X119_245, a131) | c2_2(X119_245, X121_246) | ~c6_2(X119_245, X121_246) | ~c6_2(X119_245, a89) | ~c7_2(X119_245, a89) | ~ndr1_1(X119_245)))). % 20.25/6.75 tff(c_7253, plain, (![X17_31, X121_225, X16_30, X120_226, X119_224]: (~c10_2(X119_224, X17_31) | ~c1_2(X119_224, X17_31) | c9_2(X119_224, X17_31) | c1_2(X119_224, X16_30) | c3_2(X119_224, X16_30) | c9_2(X119_224, X16_30) | c10_2(X119_224, X121_225) | ~c1_2(X119_224, X121_225) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | c9_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.76 tff(c_7271, plain, (![X17_31, X121_225, X16_30, X120_226, X119_224]: (~c10_2(X119_224, X17_31) | ~c1_2(X119_224, X17_31) | c9_2(X119_224, X17_31) | c1_2(X119_224, X16_30) | c3_2(X119_224, X16_30) | c9_2(X119_224, X16_30) | c10_2(X119_224, X120_226) | ~c1_2(X119_224, X120_226) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | c9_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.76 tff(c_7426, plain, (![X17_31, X16_30, X121_231, X120_232, X119_230]: (~c10_2(X119_230, X17_31) | ~c1_2(X119_230, X17_31) | c9_2(X119_230, X17_31) | c1_2(X119_230, X16_30) | c3_2(X119_230, X16_30) | c9_2(X119_230, X16_30) | c10_2(X119_230, X120_232) | ~c1_2(X119_230, X120_232) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | c9_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.76 tff(c_7576, plain, (![X119_236, X17_31, X16_30, X120_238, X121_237]: (~c10_2(X119_236, X17_31) | ~c1_2(X119_236, X17_31) | c9_2(X119_236, X17_31) | c1_2(X119_236, X16_30) | c3_2(X119_236, X16_30) | c9_2(X119_236, X16_30) | c10_2(X119_236, X120_238) | ~c1_2(X119_236, X120_238) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | c9_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.76 tff(c_9694, plain, (~c1_2(a37, a38))). % 20.25/6.76 tff(c_7408, plain, (![X17_31, X16_30, X121_231, X120_232, X119_230]: (~c10_2(X119_230, X17_31) | ~c1_2(X119_230, X17_31) | c9_2(X119_230, X17_31) | c1_2(X119_230, X16_30) | c3_2(X119_230, X16_30) | c9_2(X119_230, X16_30) | c10_2(X119_230, X121_231) | ~c1_2(X119_230, X121_231) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | c9_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.76 tff(c_9682, plain, (~c10_2(a37, a131))). % 20.25/6.76 tff(c_7558, plain, (![X119_236, X17_31, X16_30, X120_238, X121_237]: (~c10_2(X119_236, X17_31) | ~c1_2(X119_236, X17_31) | c9_2(X119_236, X17_31) | c1_2(X119_236, X16_30) | c3_2(X119_236, X16_30) | c9_2(X119_236, X16_30) | c10_2(X119_236, X121_237) | ~c1_2(X119_236, X121_237) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | c9_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.76 tff(c_9668, plain, (~c7_2(a37, a89))). % 20.25/6.76 tff(c_9577, plain, (c6_2(a37, a38))). % 20.25/6.76 tff(c_8947, plain, (![X119_168, X121_346, X120_171, X120_348]: (c7_2(X119_168, X121_346) | c8_2(X119_168, X121_346) | c4_1(X119_168) | c1_2(X119_168, X120_171) | c2_2(X119_168, X121_346) | ~c6_2(X119_168, X121_346) | ~c6_2(X119_168, X120_348) | c9_2(X119_168, X120_348) | ~c7_2(X119_168, X120_348) | ~c1_2(X119_168, a131) | c2_2(X119_168, X120_171) | ~c6_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.76 tff(c_9541, plain, (c4_2(a37, a38))). % 20.25/6.76 tff(c_9539, plain, (~c3_1(a37))). % 20.25/6.76 tff(c_9540, plain, (c6_1(a37))). % 20.25/6.76 tff(c_9530, plain, (~c7_1(a37))). % 20.25/6.76 tff(c_9523, plain, (~c3_2(a37, a38))). % 20.25/6.76 tff(c_8788, plain, (![X119_168, X121_338, X121_172, X120_340]: (c7_2(X119_168, X121_338) | c8_2(X119_168, X121_338) | c4_1(X119_168) | c1_2(X119_168, X121_172) | c2_2(X119_168, X121_338) | ~c6_2(X119_168, X121_338) | ~c6_2(X119_168, X120_340) | c9_2(X119_168, X120_340) | ~c7_2(X119_168, X120_340) | c2_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c7_2(X119_168, X121_172) | ~ndr1_1(X119_168)))). % 20.25/6.76 tff(c_9487, plain, (~c6_2(a3, a5))). % 20.25/6.76 tff(c_8863, plain, (![X119_168, X121_342, X121_172, X120_344]: (c7_2(X119_168, X121_342) | c8_2(X119_168, X121_342) | c4_1(X119_168) | c1_2(X119_168, X121_172) | c2_2(X119_168, X121_342) | ~c6_2(X119_168, X121_342) | ~c6_2(X119_168, X120_344) | c9_2(X119_168, X120_344) | ~c7_2(X119_168, X120_344) | ~c10_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c7_2(X119_168, X121_172) | ~ndr1_1(X119_168)))). % 20.25/6.76 tff(c_7726, plain, (![X119_245, X121_246, X35_58]: (~c8_2(X119_245, a43) | ~c3_2(X119_245, X121_246) | ~c4_2(X119_245, X121_246) | c2_2(X119_245, X35_58) | c4_2(X119_245, X35_58) | ~c3_2(X119_245, X35_58) | ~c6_1(X119_245) | c4_1(X119_245) | ~c1_2(X119_245, a131) | c2_2(X119_245, X121_246) | ~c6_2(X119_245, X121_246) | ~c6_2(X119_245, a89) | ~c7_2(X119_245, a89) | ~ndr1_1(X119_245)))). % 20.25/6.76 tff(c_7682, plain, (![X119_242, X121_243, X35_58]: (c1_2(X119_242, a43) | ~c3_2(X119_242, X121_243) | ~c4_2(X119_242, X121_243) | c2_2(X119_242, X35_58) | c4_2(X119_242, X35_58) | ~c3_2(X119_242, X35_58) | ~c6_1(X119_242) | c4_1(X119_242) | ~c10_2(X119_242, a131) | c2_2(X119_242, X121_243) | ~c6_2(X119_242, X121_243) | ~c6_2(X119_242, a89) | ~c7_2(X119_242, a89) | ~ndr1_1(X119_242)))). % 20.25/6.76 tff(c_7896, plain, (![X119_253, X121_254, X35_58]: (c1_2(X119_253, a43) | ~c3_2(X119_253, X121_254) | ~c4_2(X119_253, X121_254) | c2_2(X119_253, X35_58) | c4_2(X119_253, X35_58) | ~c3_2(X119_253, X35_58) | ~c6_1(X119_253) | c4_1(X119_253) | c2_2(X119_253, a131) | c2_2(X119_253, X121_254) | ~c6_2(X119_253, X121_254) | ~c6_2(X119_253, a89) | ~c7_2(X119_253, a89) | ~ndr1_1(X119_253)))). % 20.25/6.76 tff(c_7813, plain, (![X119_249, X120_250, X35_58]: (c10_2(X119_249, a43) | ~c3_2(X119_249, X120_250) | ~c4_2(X119_249, X120_250) | c2_2(X119_249, X35_58) | c4_2(X119_249, X35_58) | ~c3_2(X119_249, X35_58) | ~c6_1(X119_249) | c4_1(X119_249) | ~c1_2(X119_249, a131) | c2_2(X119_249, a89) | ~c6_2(X119_249, a89) | ~c6_2(X119_249, X120_250) | ~c7_2(X119_249, X120_250) | ~ndr1_1(X119_249)))). % 20.25/6.76 tff(c_7897, plain, (![X119_253, X121_254, X35_58]: (c10_2(X119_253, a43) | ~c3_2(X119_253, X121_254) | ~c4_2(X119_253, X121_254) | c2_2(X119_253, X35_58) | c4_2(X119_253, X35_58) | ~c3_2(X119_253, X35_58) | ~c6_1(X119_253) | c4_1(X119_253) | c2_2(X119_253, a131) | c2_2(X119_253, X121_254) | ~c6_2(X119_253, X121_254) | ~c6_2(X119_253, a89) | ~c7_2(X119_253, a89) | ~ndr1_1(X119_253)))). % 20.25/6.76 tff(c_7683, plain, (![X119_242, X121_243, X35_58]: (c10_2(X119_242, a43) | ~c3_2(X119_242, X121_243) | ~c4_2(X119_242, X121_243) | c2_2(X119_242, X35_58) | c4_2(X119_242, X35_58) | ~c3_2(X119_242, X35_58) | ~c6_1(X119_242) | c4_1(X119_242) | ~c10_2(X119_242, a131) | c2_2(X119_242, X121_243) | ~c6_2(X119_242, X121_243) | ~c6_2(X119_242, a89) | ~c7_2(X119_242, a89) | ~ndr1_1(X119_242)))). % 20.25/6.76 tff(c_7770, plain, (![X119_247, X120_248, X35_58]: (c1_2(X119_247, a43) | ~c3_2(X119_247, X120_248) | ~c4_2(X119_247, X120_248) | c2_2(X119_247, X35_58) | c4_2(X119_247, X35_58) | ~c3_2(X119_247, X35_58) | ~c6_1(X119_247) | c4_1(X119_247) | c2_2(X119_247, a131) | c2_2(X119_247, a89) | ~c6_2(X119_247, a89) | ~c6_2(X119_247, X120_248) | ~c7_2(X119_247, X120_248) | ~ndr1_1(X119_247)))). % 20.25/6.76 tff(c_7853, plain, (![X119_251, X120_252, X35_58]: (~c8_2(X119_251, a43) | ~c3_2(X119_251, X120_252) | ~c4_2(X119_251, X120_252) | c2_2(X119_251, X35_58) | c4_2(X119_251, X35_58) | ~c3_2(X119_251, X35_58) | ~c6_1(X119_251) | c4_1(X119_251) | ~c10_2(X119_251, a131) | c2_2(X119_251, a89) | ~c6_2(X119_251, a89) | ~c6_2(X119_251, X120_252) | ~c7_2(X119_251, X120_252) | ~ndr1_1(X119_251)))). % 20.25/6.76 tff(c_7728, plain, (![X119_245, X121_246, X35_58]: (c10_2(X119_245, a43) | ~c3_2(X119_245, X121_246) | ~c4_2(X119_245, X121_246) | c2_2(X119_245, X35_58) | c4_2(X119_245, X35_58) | ~c3_2(X119_245, X35_58) | ~c6_1(X119_245) | c4_1(X119_245) | ~c1_2(X119_245, a131) | c2_2(X119_245, X121_246) | ~c6_2(X119_245, X121_246) | ~c6_2(X119_245, a89) | ~c7_2(X119_245, a89) | ~ndr1_1(X119_245)))). % 20.25/6.76 tff(c_7771, plain, (![X119_247, X120_248, X35_58]: (c10_2(X119_247, a43) | ~c3_2(X119_247, X120_248) | ~c4_2(X119_247, X120_248) | c2_2(X119_247, X35_58) | c4_2(X119_247, X35_58) | ~c3_2(X119_247, X35_58) | ~c6_1(X119_247) | c4_1(X119_247) | c2_2(X119_247, a131) | c2_2(X119_247, a89) | ~c6_2(X119_247, a89) | ~c6_2(X119_247, X120_248) | ~c7_2(X119_247, X120_248) | ~ndr1_1(X119_247)))). % 20.25/6.76 tff(c_7769, plain, (![X119_247, X120_248, X35_58]: (~c8_2(X119_247, a43) | ~c3_2(X119_247, X120_248) | ~c4_2(X119_247, X120_248) | c2_2(X119_247, X35_58) | c4_2(X119_247, X35_58) | ~c3_2(X119_247, X35_58) | ~c6_1(X119_247) | c4_1(X119_247) | c2_2(X119_247, a131) | c2_2(X119_247, a89) | ~c6_2(X119_247, a89) | ~c6_2(X119_247, X120_248) | ~c7_2(X119_247, X120_248) | ~ndr1_1(X119_247)))). % 20.25/6.76 tff(c_7895, plain, (![X119_253, X121_254, X35_58]: (~c8_2(X119_253, a43) | ~c3_2(X119_253, X121_254) | ~c4_2(X119_253, X121_254) | c2_2(X119_253, X35_58) | c4_2(X119_253, X35_58) | ~c3_2(X119_253, X35_58) | ~c6_1(X119_253) | c4_1(X119_253) | c2_2(X119_253, a131) | c2_2(X119_253, X121_254) | ~c6_2(X119_253, X121_254) | ~c6_2(X119_253, a89) | ~c7_2(X119_253, a89) | ~ndr1_1(X119_253)))). % 20.25/6.76 tff(c_7855, plain, (![X119_251, X120_252, X35_58]: (c10_2(X119_251, a43) | ~c3_2(X119_251, X120_252) | ~c4_2(X119_251, X120_252) | c2_2(X119_251, X35_58) | c4_2(X119_251, X35_58) | ~c3_2(X119_251, X35_58) | ~c6_1(X119_251) | c4_1(X119_251) | ~c10_2(X119_251, a131) | c2_2(X119_251, a89) | ~c6_2(X119_251, a89) | ~c6_2(X119_251, X120_252) | ~c7_2(X119_251, X120_252) | ~ndr1_1(X119_251)))). % 20.25/6.76 tff(c_7727, plain, (![X119_245, X121_246, X35_58]: (c1_2(X119_245, a43) | ~c3_2(X119_245, X121_246) | ~c4_2(X119_245, X121_246) | c2_2(X119_245, X35_58) | c4_2(X119_245, X35_58) | ~c3_2(X119_245, X35_58) | ~c6_1(X119_245) | c4_1(X119_245) | ~c1_2(X119_245, a131) | c2_2(X119_245, X121_246) | ~c6_2(X119_245, X121_246) | ~c6_2(X119_245, a89) | ~c7_2(X119_245, a89) | ~ndr1_1(X119_245)))). % 20.25/6.76 tff(c_7811, plain, (![X119_249, X120_250, X35_58]: (~c8_2(X119_249, a43) | ~c3_2(X119_249, X120_250) | ~c4_2(X119_249, X120_250) | c2_2(X119_249, X35_58) | c4_2(X119_249, X35_58) | ~c3_2(X119_249, X35_58) | ~c6_1(X119_249) | c4_1(X119_249) | ~c1_2(X119_249, a131) | c2_2(X119_249, a89) | ~c6_2(X119_249, a89) | ~c6_2(X119_249, X120_250) | ~c7_2(X119_249, X120_250) | ~ndr1_1(X119_249)))). % 20.25/6.76 tff(c_7681, plain, (![X119_242, X121_243, X35_58]: (~c8_2(X119_242, a43) | ~c3_2(X119_242, X121_243) | ~c4_2(X119_242, X121_243) | c2_2(X119_242, X35_58) | c4_2(X119_242, X35_58) | ~c3_2(X119_242, X35_58) | ~c6_1(X119_242) | c4_1(X119_242) | ~c10_2(X119_242, a131) | c2_2(X119_242, X121_243) | ~c6_2(X119_242, X121_243) | ~c6_2(X119_242, a89) | ~c7_2(X119_242, a89) | ~ndr1_1(X119_242)))). % 20.25/6.76 tff(c_7812, plain, (![X119_249, X120_250, X35_58]: (c1_2(X119_249, a43) | ~c3_2(X119_249, X120_250) | ~c4_2(X119_249, X120_250) | c2_2(X119_249, X35_58) | c4_2(X119_249, X35_58) | ~c3_2(X119_249, X35_58) | ~c6_1(X119_249) | c4_1(X119_249) | ~c1_2(X119_249, a131) | c2_2(X119_249, a89) | ~c6_2(X119_249, a89) | ~c6_2(X119_249, X120_250) | ~c7_2(X119_249, X120_250) | ~ndr1_1(X119_249)))). % 20.25/6.76 tff(c_7854, plain, (![X119_251, X120_252, X35_58]: (c1_2(X119_251, a43) | ~c3_2(X119_251, X120_252) | ~c4_2(X119_251, X120_252) | c2_2(X119_251, X35_58) | c4_2(X119_251, X35_58) | ~c3_2(X119_251, X35_58) | ~c6_1(X119_251) | c4_1(X119_251) | ~c10_2(X119_251, a131) | c2_2(X119_251, a89) | ~c6_2(X119_251, a89) | ~c6_2(X119_251, X120_252) | ~c7_2(X119_251, X120_252) | ~ndr1_1(X119_251)))). % 20.25/6.76 tff(c_7618, plain, (![X119_239, X17_31, X16_30, X121_240]: (~c10_2(X119_239, X17_31) | ~c1_2(X119_239, X17_31) | c9_2(X119_239, X17_31) | c1_2(X119_239, X16_30) | c3_2(X119_239, X16_30) | c9_2(X119_239, X16_30) | c10_2(X119_239, X121_240) | ~c1_2(X119_239, X121_240) | ~c10_2(X119_239, a131) | c2_2(X119_239, X121_240) | ~c6_2(X119_239, X121_240) | ~c7_2(X119_239, X121_240) | ~ndr1_1(X119_239)))). % 20.25/6.76 tff(c_7468, plain, (![X119_233, X17_31, X16_30, X121_234]: (~c10_2(X119_233, X17_31) | ~c1_2(X119_233, X17_31) | c9_2(X119_233, X17_31) | c1_2(X119_233, X16_30) | c3_2(X119_233, X16_30) | c9_2(X119_233, X16_30) | c10_2(X119_233, X121_234) | ~c1_2(X119_233, X121_234) | c2_2(X119_233, a131) | c2_2(X119_233, X121_234) | ~c6_2(X119_233, X121_234) | ~c7_2(X119_233, X121_234) | ~ndr1_1(X119_233)))). % 20.25/6.76 tff(c_9143, plain, (~c6_2(a35, a36))). % 20.25/6.76 tff(c_7314, plain, (![X119_227, X17_31, X16_30, X120_228]: (~c10_2(X119_227, X17_31) | ~c1_2(X119_227, X17_31) | c9_2(X119_227, X17_31) | c1_2(X119_227, X16_30) | c3_2(X119_227, X16_30) | c9_2(X119_227, X16_30) | c10_2(X119_227, X120_228) | ~c1_2(X119_227, X120_228) | ~c1_2(X119_227, a131) | c2_2(X119_227, X120_228) | ~c6_2(X119_227, X120_228) | ~c7_2(X119_227, X120_228) | ~ndr1_1(X119_227)))). % 20.25/6.76 tff(c_7561, plain, (![X119_236, X121_237, X35_58, X120_238]: (c10_2(X119_236, a43) | ~c3_2(X119_236, X121_237) | ~c4_2(X119_236, X121_237) | c2_2(X119_236, X35_58) | c4_2(X119_236, X35_58) | ~c3_2(X119_236, X35_58) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | c9_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.76 tff(c_7272, plain, (![X119_224, X120_226, X35_58, X121_225]: (~c8_2(X119_224, a43) | ~c3_2(X119_224, X120_226) | ~c4_2(X119_224, X120_226) | c2_2(X119_224, X35_58) | c4_2(X119_224, X35_58) | ~c3_2(X119_224, X35_58) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | c9_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.76 tff(c_7256, plain, (![X119_224, X121_225, X35_58, X120_226]: (c10_2(X119_224, a43) | ~c3_2(X119_224, X121_225) | ~c4_2(X119_224, X121_225) | c2_2(X119_224, X35_58) | c4_2(X119_224, X35_58) | ~c3_2(X119_224, X35_58) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | c9_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.76 tff(c_9064, plain, (~c1_2(a53, a131))). % 20.25/6.76 tff(c_7255, plain, (![X119_224, X121_225, X35_58, X120_226]: (c1_2(X119_224, a43) | ~c3_2(X119_224, X121_225) | ~c4_2(X119_224, X121_225) | c2_2(X119_224, X35_58) | c4_2(X119_224, X35_58) | ~c3_2(X119_224, X35_58) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | c9_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.76 tff(c_7410, plain, (![X119_230, X121_231, X35_58, X120_232]: (c1_2(X119_230, a43) | ~c3_2(X119_230, X121_231) | ~c4_2(X119_230, X121_231) | c2_2(X119_230, X35_58) | c4_2(X119_230, X35_58) | ~c3_2(X119_230, X35_58) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | c9_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.76 tff(c_7274, plain, (![X119_224, X120_226, X35_58, X121_225]: (c10_2(X119_224, a43) | ~c3_2(X119_224, X120_226) | ~c4_2(X119_224, X120_226) | c2_2(X119_224, X35_58) | c4_2(X119_224, X35_58) | ~c3_2(X119_224, X35_58) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | c9_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.76 tff(c_9020, plain, (c2_2(a53, a131))). % 20.25/6.76 tff(c_7411, plain, (![X119_230, X121_231, X35_58, X120_232]: (c10_2(X119_230, a43) | ~c3_2(X119_230, X121_231) | ~c4_2(X119_230, X121_231) | c2_2(X119_230, X35_58) | c4_2(X119_230, X35_58) | ~c3_2(X119_230, X35_58) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | c9_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_7560, plain, (![X119_236, X121_237, X35_58, X120_238]: (c1_2(X119_236, a43) | ~c3_2(X119_236, X121_237) | ~c4_2(X119_236, X121_237) | c2_2(X119_236, X35_58) | c4_2(X119_236, X35_58) | ~c3_2(X119_236, X35_58) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | c9_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_7273, plain, (![X119_224, X120_226, X35_58, X121_225]: (c1_2(X119_224, a43) | ~c3_2(X119_224, X120_226) | ~c4_2(X119_224, X120_226) | c2_2(X119_224, X35_58) | c4_2(X119_224, X35_58) | ~c3_2(X119_224, X35_58) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | c9_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.77 tff(c_7254, plain, (![X119_224, X121_225, X35_58, X120_226]: (~c8_2(X119_224, a43) | ~c3_2(X119_224, X121_225) | ~c4_2(X119_224, X121_225) | c2_2(X119_224, X35_58) | c4_2(X119_224, X35_58) | ~c3_2(X119_224, X35_58) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, X120_226) | c9_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.77 tff(c_8970, plain, (~c1_2(a45, a131))). % 20.25/6.77 tff(c_8465, plain, (![X119_168, X121_172, X112_318, X120_171]: (c7_2(X119_168, X121_172) | c8_2(X119_168, X121_172) | c4_1(X119_168) | c2_2(X119_168, X112_318) | c1_2(X119_168, X112_318) | ~c9_2(X119_168, X112_318) | ~c1_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.77 tff(c_8892, plain, (~c10_2(a45, a131))). % 20.25/6.77 tff(c_8459, plain, (![X119_168, X121_172, X112_318, X120_171]: (c7_2(X119_168, X121_172) | c8_2(X119_168, X121_172) | c4_1(X119_168) | c2_2(X119_168, X112_318) | c1_2(X119_168, X112_318) | ~c9_2(X119_168, X112_318) | ~c10_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.77 tff(c_8814, plain, (c2_2(a45, a131))). % 20.25/6.77 tff(c_8462, plain, (![X119_168, X121_172, X112_318, X120_171]: (c7_2(X119_168, X121_172) | c8_2(X119_168, X121_172) | c4_1(X119_168) | c2_2(X119_168, X112_318) | c1_2(X119_168, X112_318) | ~c9_2(X119_168, X112_318) | c2_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.77 tff(c_8688, plain, (![X119_224, X121_326, X121_225]: (c7_2(X119_224, X121_326) | c8_2(X119_224, X121_326) | c1_2(X119_224, X121_225) | c2_2(X119_224, X121_326) | ~c6_2(X119_224, X121_326) | ~c6_1(X119_224) | c4_1(X119_224) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, a89) | ~c7_2(X119_224, a89) | ~ndr1_1(X119_224)))). % 20.25/6.77 tff(c_8608, plain, (![X119_230, X121_323, X121_231]: (c7_2(X119_230, X121_323) | c8_2(X119_230, X121_323) | c1_2(X119_230, X121_231) | c2_2(X119_230, X121_323) | ~c6_2(X119_230, X121_323) | ~c6_1(X119_230) | c4_1(X119_230) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, a89) | ~c7_2(X119_230, a89) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_8535, plain, (![X119_236, X121_320, X121_237]: (c7_2(X119_236, X121_320) | c8_2(X119_236, X121_320) | c1_2(X119_236, X121_237) | c2_2(X119_236, X121_320) | ~c6_2(X119_236, X121_320) | ~c6_1(X119_236) | c4_1(X119_236) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, a89) | ~c7_2(X119_236, a89) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_8456, plain, (![X119_224, X121_225, X112_318]: (c7_2(X119_224, X121_225) | c8_2(X119_224, X121_225) | c2_2(X119_224, X112_318) | c1_2(X119_224, X112_318) | ~c9_2(X119_224, X112_318) | ~c6_1(X119_224) | c4_1(X119_224) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, a89) | ~c7_2(X119_224, a89) | ~ndr1_1(X119_224)))). % 20.25/6.77 tff(c_8452, plain, (![X119_230, X121_231, X112_318]: (c7_2(X119_230, X121_231) | c8_2(X119_230, X121_231) | c2_2(X119_230, X112_318) | c1_2(X119_230, X112_318) | ~c9_2(X119_230, X112_318) | ~c6_1(X119_230) | c4_1(X119_230) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, a89) | ~c7_2(X119_230, a89) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_8565, plain, (~c7_2(a45, a89))). % 20.25/6.77 tff(c_8457, plain, (![X119_236, X121_237, X112_318]: (c7_2(X119_236, X121_237) | c8_2(X119_236, X121_237) | c2_2(X119_236, X112_318) | c1_2(X119_236, X112_318) | ~c9_2(X119_236, X112_318) | ~c6_1(X119_236) | c4_1(X119_236) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, a89) | ~c7_2(X119_236, a89) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_8488, plain, (ndr1_1(a37))). % 20.25/6.77 tff(c_8487, plain, (~c5_1(a37))). % 20.25/6.77 tff(c_8486, plain, (c4_1(a53))). % 20.25/6.77 tff(c_8485, plain, (c4_1(a143))). % 20.25/6.77 tff(c_8484, plain, (c4_1(a19))). % 20.25/6.77 tff(c_8483, plain, (c4_1(a139))). % 20.25/6.77 tff(c_8410, plain, (![X111_156, X113_160, X112_159]: (c7_2(X111_156, X113_160) | ~c9_2(X111_156, X113_160) | c8_2(X111_156, X113_160) | c4_1(X111_156) | c2_2(X111_156, X112_159) | c1_2(X111_156, X112_159) | ~c9_2(X111_156, X112_159) | ~ndr1_1(X111_156)))). % 20.25/6.77 tff(c_8409, plain, (~c10_2(a71, a72))). % 20.25/6.77 tff(c_8408, plain, (~c6_2(a71, a72))). % 20.25/6.77 tff(c_8347, plain, (c7_2(a71, a72))). % 20.25/6.77 tff(c_8346, plain, (~c8_2(a53, a43))). % 20.25/6.77 tff(c_8345, plain, (c4_2(a71, a72))). % 20.25/6.77 tff(c_8344, plain, (c6_1(a9))). % 20.25/6.77 tff(c_8336, plain, (~c7_1(a9))). % 20.25/6.77 tff(c_8335, plain, (~c3_1(a68))). % 20.25/6.77 tff(c_8327, plain, (c6_1(a68))). % 20.25/6.77 tff(c_8332, plain, (~c3_1(a71))). % 20.25/6.77 tff(c_8328, plain, (~c8_1(a71))). % 20.25/6.77 tff(c_8319, plain, (~c7_1(a68))). % 20.25/6.77 tff(c_8318, plain, (~c3_1(a3))). % 20.25/6.77 tff(c_8315, plain, (c6_1(a3))). % 20.25/6.77 tff(c_8307, plain, (~c7_1(a3))). % 20.25/6.77 tff(c_8269, plain, (![X_5, Y_7]: (~c1_2(X_5, Y_7) | ~c10_2(X_5, Y_7) | c3_2(X_5, Y_7) | ~ndr1_1(X_5) | ~c7_1(X_5) | c10_1(X_5)))). % 20.25/6.77 tff(c_7409, plain, (![X119_230, X121_231, X35_58, X120_232]: (~c8_2(X119_230, a43) | ~c3_2(X119_230, X121_231) | ~c4_2(X119_230, X121_231) | c2_2(X119_230, X35_58) | c4_2(X119_230, X35_58) | ~c3_2(X119_230, X35_58) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | c9_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_7578, plain, (![X119_236, X120_238, X35_58, X121_237]: (c1_2(X119_236, a43) | ~c3_2(X119_236, X120_238) | ~c4_2(X119_236, X120_238) | c2_2(X119_236, X35_58) | c4_2(X119_236, X35_58) | ~c3_2(X119_236, X35_58) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | c9_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_7577, plain, (![X119_236, X120_238, X35_58, X121_237]: (~c8_2(X119_236, a43) | ~c3_2(X119_236, X120_238) | ~c4_2(X119_236, X120_238) | c2_2(X119_236, X35_58) | c4_2(X119_236, X35_58) | ~c3_2(X119_236, X35_58) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | c9_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_7428, plain, (![X119_230, X120_232, X35_58, X121_231]: (c1_2(X119_230, a43) | ~c3_2(X119_230, X120_232) | ~c4_2(X119_230, X120_232) | c2_2(X119_230, X35_58) | c4_2(X119_230, X35_58) | ~c3_2(X119_230, X35_58) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | c9_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_8182, plain, (ndr1_1(a71))). % 20.25/6.77 tff(c_7427, plain, (![X119_230, X120_232, X35_58, X121_231]: (~c8_2(X119_230, a43) | ~c3_2(X119_230, X120_232) | ~c4_2(X119_230, X120_232) | c2_2(X119_230, X35_58) | c4_2(X119_230, X35_58) | ~c3_2(X119_230, X35_58) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | c9_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_7429, plain, (![X119_230, X120_232, X35_58, X121_231]: (c10_2(X119_230, a43) | ~c3_2(X119_230, X120_232) | ~c4_2(X119_230, X120_232) | c2_2(X119_230, X35_58) | c4_2(X119_230, X35_58) | ~c3_2(X119_230, X35_58) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | c9_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_8129, plain, (~c2_1(a71))). % 20.25/6.77 tff(c_8128, plain, (~c10_2(a53, a131))). % 20.25/6.77 tff(c_7559, plain, (![X119_236, X121_237, X35_58, X120_238]: (~c8_2(X119_236, a43) | ~c3_2(X119_236, X121_237) | ~c4_2(X119_236, X121_237) | c2_2(X119_236, X35_58) | c4_2(X119_236, X35_58) | ~c3_2(X119_236, X35_58) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | c9_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_7579, plain, (![X119_236, X120_238, X35_58, X121_237]: (c10_2(X119_236, a43) | ~c3_2(X119_236, X120_238) | ~c4_2(X119_236, X120_238) | c2_2(X119_236, X35_58) | c4_2(X119_236, X35_58) | ~c3_2(X119_236, X35_58) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | c9_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_8092, plain, (~c3_2(a9, a10))). % 20.25/6.77 tff(c_8091, plain, (c2_2(a9, a10))). % 20.25/6.77 tff(c_7316, plain, (![X119_227, X120_228, X35_58]: (c1_2(X119_227, a43) | ~c3_2(X119_227, X120_228) | ~c4_2(X119_227, X120_228) | c2_2(X119_227, X35_58) | c4_2(X119_227, X35_58) | ~c3_2(X119_227, X35_58) | ~c1_2(X119_227, a131) | c2_2(X119_227, X120_228) | ~c6_2(X119_227, X120_228) | ~c7_2(X119_227, X120_228) | ~ndr1_1(X119_227)))). % 20.25/6.77 tff(c_7471, plain, (![X119_233, X121_234, X35_58]: (c10_2(X119_233, a43) | ~c3_2(X119_233, X121_234) | ~c4_2(X119_233, X121_234) | c2_2(X119_233, X35_58) | c4_2(X119_233, X35_58) | ~c3_2(X119_233, X35_58) | c2_2(X119_233, a131) | c2_2(X119_233, X121_234) | ~c6_2(X119_233, X121_234) | ~c7_2(X119_233, X121_234) | ~ndr1_1(X119_233)))). % 20.25/6.77 tff(c_7470, plain, (![X119_233, X121_234, X35_58]: (c1_2(X119_233, a43) | ~c3_2(X119_233, X121_234) | ~c4_2(X119_233, X121_234) | c2_2(X119_233, X35_58) | c4_2(X119_233, X35_58) | ~c3_2(X119_233, X35_58) | c2_2(X119_233, a131) | c2_2(X119_233, X121_234) | ~c6_2(X119_233, X121_234) | ~c7_2(X119_233, X121_234) | ~ndr1_1(X119_233)))). % 20.25/6.77 tff(c_7315, plain, (![X119_227, X120_228, X35_58]: (~c8_2(X119_227, a43) | ~c3_2(X119_227, X120_228) | ~c4_2(X119_227, X120_228) | c2_2(X119_227, X35_58) | c4_2(X119_227, X35_58) | ~c3_2(X119_227, X35_58) | ~c1_2(X119_227, a131) | c2_2(X119_227, X120_228) | ~c6_2(X119_227, X120_228) | ~c7_2(X119_227, X120_228) | ~ndr1_1(X119_227)))). % 20.25/6.77 tff(c_7619, plain, (![X119_239, X121_240, X35_58]: (~c8_2(X119_239, a43) | ~c3_2(X119_239, X121_240) | ~c4_2(X119_239, X121_240) | c2_2(X119_239, X35_58) | c4_2(X119_239, X35_58) | ~c3_2(X119_239, X35_58) | ~c10_2(X119_239, a131) | c2_2(X119_239, X121_240) | ~c6_2(X119_239, X121_240) | ~c7_2(X119_239, X121_240) | ~ndr1_1(X119_239)))). % 20.25/6.77 tff(c_7317, plain, (![X119_227, X120_228, X35_58]: (c10_2(X119_227, a43) | ~c3_2(X119_227, X120_228) | ~c4_2(X119_227, X120_228) | c2_2(X119_227, X35_58) | c4_2(X119_227, X35_58) | ~c3_2(X119_227, X35_58) | ~c1_2(X119_227, a131) | c2_2(X119_227, X120_228) | ~c6_2(X119_227, X120_228) | ~c7_2(X119_227, X120_228) | ~ndr1_1(X119_227)))). % 20.25/6.77 tff(c_7972, plain, (~c6_2(a9, a10))). % 20.25/6.77 tff(c_7469, plain, (![X119_233, X121_234, X35_58]: (~c8_2(X119_233, a43) | ~c3_2(X119_233, X121_234) | ~c4_2(X119_233, X121_234) | c2_2(X119_233, X35_58) | c4_2(X119_233, X35_58) | ~c3_2(X119_233, X35_58) | c2_2(X119_233, a131) | c2_2(X119_233, X121_234) | ~c6_2(X119_233, X121_234) | ~c7_2(X119_233, X121_234) | ~ndr1_1(X119_233)))). % 20.25/6.77 tff(c_7620, plain, (![X119_239, X121_240, X35_58]: (c1_2(X119_239, a43) | ~c3_2(X119_239, X121_240) | ~c4_2(X119_239, X121_240) | c2_2(X119_239, X35_58) | c4_2(X119_239, X35_58) | ~c3_2(X119_239, X35_58) | ~c10_2(X119_239, a131) | c2_2(X119_239, X121_240) | ~c6_2(X119_239, X121_240) | ~c7_2(X119_239, X121_240) | ~ndr1_1(X119_239)))). % 20.25/6.77 tff(c_7941, plain, (~c6_2(a90, a91))). % 20.25/6.77 tff(c_7621, plain, (![X119_239, X121_240, X35_58]: (c10_2(X119_239, a43) | ~c3_2(X119_239, X121_240) | ~c4_2(X119_239, X121_240) | c2_2(X119_239, X35_58) | c4_2(X119_239, X35_58) | ~c3_2(X119_239, X35_58) | ~c10_2(X119_239, a131) | c2_2(X119_239, X121_240) | ~c6_2(X119_239, X121_240) | ~c7_2(X119_239, X121_240) | ~ndr1_1(X119_239)))). % 20.25/6.77 tff(c_7430, plain, (![X119_230, X121_231]: (~c6_1(X119_230) | c4_1(X119_230) | c2_2(X119_230, a131) | c2_2(X119_230, X121_231) | c9_2(X119_230, X121_231) | ~c6_2(X119_230, X121_231) | ~c6_2(X119_230, a89) | ~c7_2(X119_230, a89) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_7562, plain, (![X119_236, X120_238]: (~c6_1(X119_236) | c4_1(X119_236) | ~c10_2(X119_236, a131) | c2_2(X119_236, a89) | ~c6_2(X119_236, a89) | ~c6_2(X119_236, X120_238) | c9_2(X119_236, X120_238) | ~c7_2(X119_236, X120_238) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_7257, plain, (![X119_224, X120_226]: (~c6_1(X119_224) | c4_1(X119_224) | ~c1_2(X119_224, a131) | c2_2(X119_224, a89) | ~c6_2(X119_224, a89) | ~c6_2(X119_224, X120_226) | c9_2(X119_224, X120_226) | ~c7_2(X119_224, X120_226) | ~ndr1_1(X119_224)))). % 20.25/6.77 tff(c_7412, plain, (![X119_230, X120_232]: (~c6_1(X119_230) | c4_1(X119_230) | c2_2(X119_230, a131) | c2_2(X119_230, a89) | ~c6_2(X119_230, a89) | ~c6_2(X119_230, X120_232) | c9_2(X119_230, X120_232) | ~c7_2(X119_230, X120_232) | ~ndr1_1(X119_230)))). % 20.25/6.77 tff(c_7275, plain, (![X119_224, X121_225]: (~c6_1(X119_224) | c4_1(X119_224) | ~c1_2(X119_224, a131) | c2_2(X119_224, X121_225) | c9_2(X119_224, X121_225) | ~c6_2(X119_224, X121_225) | ~c6_2(X119_224, a89) | ~c7_2(X119_224, a89) | ~ndr1_1(X119_224)))). % 20.25/6.77 tff(c_7698, plain, (![X68_99]: (~c7_2(a73, X68_99) | ~c10_2(a73, X68_99) | c5_2(a73, X68_99)))). % 20.25/6.77 tff(c_7580, plain, (![X119_236, X121_237]: (~c6_1(X119_236) | c4_1(X119_236) | ~c10_2(X119_236, a131) | c2_2(X119_236, X121_237) | c9_2(X119_236, X121_237) | ~c6_2(X119_236, X121_237) | ~c6_2(X119_236, a89) | ~c7_2(X119_236, a89) | ~ndr1_1(X119_236)))). % 20.25/6.77 tff(c_7622, plain, (![X119_239]: (~c6_1(X119_239) | c4_1(X119_239) | ~c10_2(X119_239, a131) | c2_2(X119_239, a89) | ~c6_2(X119_239, a89) | ~c7_2(X119_239, a89) | ~ndr1_1(X119_239)))). % 20.25/6.77 tff(c_7646, plain, (ndr1_1(a73))). % 20.25/6.78 tff(c_7507, plain, (![X119_168, X121_172]: (~c10_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c7_2(X119_168, X121_172) | ~ndr1_1(X119_168) | c9_2(X119_168, X121_172)))). % 20.25/6.78 tff(c_7486, plain, (![X119_168, X121_172, X120_171]: (~c10_2(X119_168, a131) | c2_2(X119_168, X121_172) | c9_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.78 tff(c_7472, plain, (![X119_233]: (~c6_1(X119_233) | c4_1(X119_233) | c2_2(X119_233, a131) | c2_2(X119_233, a89) | ~c6_2(X119_233, a89) | ~c7_2(X119_233, a89) | ~ndr1_1(X119_233)))). % 20.25/6.78 tff(c_7357, plain, (![X119_168, X121_172]: (c2_2(X119_168, a131) | c2_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c7_2(X119_168, X121_172) | ~ndr1_1(X119_168) | c9_2(X119_168, X121_172)))). % 20.25/6.78 tff(c_7334, plain, (![X119_168, X121_172, X120_171]: (c2_2(X119_168, a131) | c2_2(X119_168, X121_172) | c9_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.78 tff(c_7318, plain, (![X119_227]: (~c6_1(X119_227) | c4_1(X119_227) | ~c1_2(X119_227, a131) | c2_2(X119_227, a89) | ~c6_2(X119_227, a89) | ~c7_2(X119_227, a89) | ~ndr1_1(X119_227)))). % 20.25/6.78 tff(c_7335, plain, (~c7_2(a7, a8))). % 20.25/6.78 tff(c_7333, plain, (~c6_2(a139, a141))). % 20.25/6.78 tff(c_7332, plain, (~c7_2(a139, a141))). % 20.25/6.78 tff(c_7203, plain, (![X119_168, X120_171]: (~c1_2(X119_168, a131) | c2_2(X119_168, X120_171) | ~c6_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168) | c9_2(X119_168, X120_171)))). % 20.25/6.78 tff(c_7288, plain, (~c6_2(a112, a113))). % 20.25/6.78 tff(c_7189, plain, (![X119_168, X121_172, X120_171]: (~c1_2(X119_168, a131) | c2_2(X119_168, X121_172) | c9_2(X119_168, X121_172) | ~c6_2(X119_168, X121_172) | ~c6_2(X119_168, X120_171) | c9_2(X119_168, X120_171) | ~c7_2(X119_168, X120_171) | ~ndr1_1(X119_168)))). % 20.25/6.78 tff(c_7186, plain, (~c3_1(a9))). % 20.25/6.78 tff(c_7187, plain, (ndr1_1(a9))). % 20.25/6.78 tff(c_7182, plain, (~c8_1(a9))). % 20.25/6.78 tff(c_7180, plain, (~c1_2(a53, a54))). % 20.25/6.78 tff(c_7179, plain, (~c1_2(a19, a20))). % 20.25/6.78 tff(c_7178, plain, (~c1_2(a139, a140))). % 20.25/6.78 tff(c_7176, plain, (~c6_1(a41))). % 20.25/6.78 tff(c_7171, plain, (~ndr1_1(a41))). % 20.25/6.78 tff(c_7169, plain, (~c1_2(a45, a48))). % 20.25/6.78 tff(c_7168, plain, (~c1_2(a143, a144))). % 20.25/6.78 tff(c_7140, plain, (![X14_25, X17_31, X16_30, X15_29]: (~c10_2(X14_25, X17_31) | ~c1_2(X14_25, X17_31) | c9_2(X14_25, X17_31) | c1_2(X14_25, X16_30) | c3_2(X14_25, X16_30) | c9_2(X14_25, X16_30) | ~c9_2(X14_25, X15_29) | c10_2(X14_25, X15_29) | ~c1_2(X14_25, X15_29) | ~ndr1_1(X14_25)))). % 20.25/6.78 tff(c_7110, plain, (![X34_55, X36_59, X35_58]: (~c8_2(X34_55, a43) | ~c3_2(X34_55, X36_59) | ~c9_2(X34_55, X36_59) | ~c4_2(X34_55, X36_59) | c2_2(X34_55, X35_58) | c4_2(X34_55, X35_58) | ~c3_2(X34_55, X35_58) | ~ndr1_1(X34_55)))). % 20.25/6.78 tff(c_7107, plain, (~c2_2(a143, a144))). % 20.25/6.78 tff(c_7106, plain, (~c3_1(a73))). % 20.25/6.78 tff(c_7098, plain, (![X54_215]: (c7_1(X54_215) | c5_1(X54_215) | ~c3_1(X54_215)))). % 20.25/6.78 tff(c_7100, plain, (~c3_1(a136))). % 20.25/6.78 tff(c_7099, plain, (~c3_1(a35))). % 20.25/6.78 tff(c_7097, plain, (~c3_1(a56))). % 20.25/6.78 tff(c_7083, plain, (![X54_80]: (c8_1(X54_80) | ~c3_1(X54_80)))). % 20.25/6.78 tff(c_7075, plain, (~c4_2(a143, a144))). % 20.25/6.78 tff(c_7039, plain, (~c4_2(a45, a48))). % 20.25/6.78 tff(c_7042, plain, (![X34_55, X36_59, X35_58]: (c1_2(X34_55, a43) | ~c3_2(X34_55, X36_59) | ~c9_2(X34_55, X36_59) | ~c4_2(X34_55, X36_59) | c2_2(X34_55, X35_58) | c4_2(X34_55, X35_58) | ~c3_2(X34_55, X35_58) | ~ndr1_1(X34_55)))). % 20.25/6.78 tff(c_7012, plain, (![X34_55, X36_59, X35_58]: (c10_2(X34_55, a43) | ~c3_2(X34_55, X36_59) | ~c9_2(X34_55, X36_59) | ~c4_2(X34_55, X36_59) | c2_2(X34_55, X35_58) | c4_2(X34_55, X35_58) | ~c3_2(X34_55, X35_58) | ~ndr1_1(X34_55)))). % 20.25/6.78 tff(c_7009, plain, (c6_1(a73))). % 20.25/6.78 tff(c_7005, plain, (~c7_1(a73))). % 20.25/6.78 tff(c_7004, plain, (~c4_1(a73))). % 20.25/6.78 tff(c_7001, plain, (~c10_1(a41))). % 20.25/6.78 tff(c_6975, plain, (c4_2(a90, a91))). % 20.25/6.78 tff(c_6972, plain, (~c7_2(a68, a69))). % 20.25/6.78 tff(c_6952, plain, (~c2_2(a90, a91))). % 20.25/6.78 tff(c_6949, plain, (~c3_2(a68, a69))). % 20.25/6.78 tff(c_6947, plain, (c7_2(a90, a91))). % 20.25/6.78 tff(c_6944, plain, (~c5_2(a68, a69))). % 20.25/6.78 tff(c_6938, plain, (~c10_2(a81, a82))). % 20.25/6.78 tff(c_6935, plain, (![X85_122]: (c10_2(X85_122, a89) | ~c6_1(X85_122) | c4_1(X85_122)))). % 20.25/6.78 tff(c_6925, plain, (~c1_2(a81, a82))). % 20.25/6.78 tff(c_6918, plain, (~c8_1(a56))). % 20.25/6.78 tff(c_6915, plain, (c2_1(a68))). % 20.25/6.78 tff(c_6910, plain, (![X85_122]: (~c9_2(X85_122, a89) | ~c6_1(X85_122) | c4_1(X85_122)))). % 20.25/6.78 tff(c_6904, plain, (c3_2(a81, a82))). % 20.25/6.78 tff(c_6900, plain, (~c1_1(a56))). % 20.25/6.78 tff(c_6894, plain, (c4_1(a68))). % 20.25/6.78 tff(c_6892, plain, (ndr1_1(a90))). % 20.25/6.78 tff(c_6888, plain, (ndr1_1(a68))). % 20.25/6.78 tff(c_6886, plain, (~c4_1(a90))). % 20.25/6.78 tff(c_6882, plain, (![X85_122]: (c4_2(X85_122, a89) | ~c6_1(X85_122) | c4_1(X85_122)))). % 20.25/6.78 tff(c_6873, plain, (~c1_1(a81))). % 20.25/6.78 tff(c_6865, plain, (~c2_2(a112, a113))). % 20.25/6.78 tff(c_6864, plain, (~c6_1(a59))). % 20.25/6.78 tff(c_6861, plain, (c4_1(a18))). % 20.25/6.78 tff(c_6833, plain, (![X85_122]: (ndr1_1(X85_122) | ~c6_1(X85_122) | c4_1(X85_122)))). % 20.25/6.78 tff(c_6836, plain, (~c4_2(a112, a113))). % 20.25/6.78 tff(c_6825, plain, (~c9_1(a81))). % 20.25/6.78 tff(c_6823, plain, (ndr1_1(a81))). % 20.25/6.78 tff(c_6819, plain, (~c9_2(a112, a113))). % 20.25/6.78 tff(c_6804, plain, (c6_1(a112))). % 20.25/6.78 tff(c_6797, plain, (~c2_2(a45, a47))). % 20.25/6.78 tff(c_6796, plain, (~c2_2(a35, a36))). % 20.25/6.78 tff(c_6794, plain, (~c2_2(a45, a46))). % 20.25/6.78 tff(c_6761, plain, (![X106_150, X107_152]: (c5_1(X106_150) | c7_1(X106_150) | c10_2(X106_150, X107_152) | c4_2(X106_150, X107_152) | ~c2_2(X106_150, X107_152) | ~ndr1_1(X106_150)))). % 20.25/6.78 tff(c_6757, plain, (ndr1_1(a112))). % 20.25/6.78 tff(c_6752, plain, (~c3_1(a112))). % 20.25/6.78 tff(c_6744, plain, (![X134_188]: (c7_1(X134_188) | c6_1(X134_188)))). % 20.25/6.78 tff(c_6732, plain, (~ndr1_1(a59))). % 20.25/6.78 tff(c_6689, plain, (~ndr1_1(a66))). % 20.25/6.78 tff(c_6660, plain, (~ndr1_1(a18))). % 20.25/6.78 tff(c_6639, plain, (![X48_73]: (c7_2(a53, X48_73) | ~c10_2(a53, X48_73) | c4_2(a53, X48_73)))). % 20.25/6.78 tff(c_6636, plain, (![X47_72]: (c6_2(a53, X47_72) | ~c3_2(a53, X47_72) | c1_2(a53, X47_72)))). % 20.25/6.78 tff(c_6618, plain, (~c4_2(a45, a47))). % 20.25/6.78 tff(c_6608, plain, (~ndr1_1(a127))). % 20.25/6.78 tff(c_6588, plain, (~c1_2(a45, a47))). % 20.25/6.78 tff(c_6587, plain, (c3_2(a45, a47))). % 20.25/6.78 tff(c_6585, plain, (~c8_2(a45, a46))). % 20.25/6.78 tff(c_6584, plain, (~c10_2(a45, a46))). % 20.25/6.78 tff(c_6557, plain, (~c4_2(a45, a46))). % 20.25/6.78 tff(c_6515, plain, (~c2_2(a45, a48))). % 20.25/6.78 tff(c_6502, plain, (c9_2(a45, a48))). % 20.25/6.78 tff(c_6501, plain, (c7_2(a45, a48))). % 20.25/6.78 tff(c_6497, plain, (~c8_2(a139, a140))). % 20.25/6.78 tff(c_6472, plain, (~c6_2(a87, a88))). % 20.25/6.78 tff(c_6464, plain, (c1_2(a139, a141))). % 20.25/6.78 tff(c_6453, plain, (~c9_2(a87, a88))). % 20.25/6.78 tff(c_6446, plain, (~c3_2(a139, a140))). % 20.25/6.78 tff(c_6442, plain, (c9_2(a139, a140))). % 20.25/6.78 tff(c_6439, plain, (~c9_2(a139, a141))). % 20.25/6.78 tff(c_6436, plain, (ndr1_1(a45))). % 20.25/6.78 tff(c_6429, plain, (~c1_2(a119, a120))). % 20.25/6.78 tff(c_6422, plain, (c5_2(a119, a120))). % 20.25/6.78 tff(c_6412, plain, (~c1_1(a87))). % 20.25/6.78 tff(c_6410, plain, (c4_1(a66))). % 20.25/6.78 tff(c_6400, plain, (ndr1_1(a87))). % 20.25/6.78 tff(c_6396, plain, (~c3_2(a3, a5))). % 20.25/6.78 tff(c_6393, plain, (~c9_1(a66))). % 20.25/6.78 tff(c_6390, plain, (c5_2(a3, a4))). % 20.25/6.79 tff(c_6387, plain, (c10_1(a119))). % 20.25/6.79 tff(c_6384, plain, (c7_2(a3, a5))). % 20.25/6.79 tff(c_6382, plain, (~c6_1(a119))). % 20.25/6.79 tff(c_6380, plain, (c1_2(a3, a4))). % 20.25/6.79 tff(c_6377, plain, (ndr1_1(a119))). % 20.25/6.79 tff(c_6375, plain, (~c1_2(a3, a5))). % 20.25/6.79 tff(c_6374, plain, (ndr1_1(a139))). % 20.25/6.79 tff(c_6372, plain, (~c2_1(a139))). % 20.25/6.79 tff(c_6370, plain, (~c3_2(a3, a4))). % 20.25/6.79 tff(c_6329, plain, (c5_1(a7))). % 20.25/6.79 tff(c_6323, plain, (![X95_135]: (c7_1(X95_135) | c5_1(X95_135) | ~c8_1(X95_135)))). % 20.25/6.79 tff(c_6304, plain, (ndr1_1(a3))). % 20.25/6.79 tff(c_6294, plain, (~c1_1(a3))). % 20.25/6.79 tff(c_6258, plain, (c2_2(a19, a20))). % 20.25/6.79 tff(c_6249, plain, (c9_2(a19, a20))). % 20.25/6.79 tff(c_6233, plain, (~c4_2(a35, a36))). % 20.25/6.79 tff(c_6230, plain, (~c9_1(a59))). % 20.25/6.79 tff(c_6214, plain, (~c4_2(a19, a20))). % 20.25/6.79 tff(c_6210, plain, (c7_2(a35, a36))). % 20.25/6.79 tff(c_6193, plain, (c8_2(a35, a36))). % 20.25/6.79 tff(c_6181, plain, (c2_2(a19, a21))). % 20.25/6.79 tff(c_6174, plain, (~c8_2(a19, a21))). % 20.25/6.79 tff(c_6128, plain, (~c2_2(a102, a103))). % 20.25/6.79 tff(c_6119, plain, (~c4_2(a102, a103))). % 20.25/6.79 tff(c_6111, plain, (~c6_2(a102, a103))). % 20.25/6.79 tff(c_6085, plain, (~c8_1(a35))). % 20.25/6.79 tff(c_6084, plain, (ndr1_1(a19))). % 20.25/6.79 tff(c_6071, plain, (c7_1(a19))). % 20.25/6.79 tff(c_6063, plain, (ndr1_1(a35))). % 20.25/6.79 tff(c_6062, plain, (~c5_1(a31))). % 20.25/6.79 tff(c_6058, plain, (c2_1(a35))). % 20.25/6.79 tff(c_6057, plain, (~c1_2(a7, a8))). % 20.25/6.79 tff(c_6056, plain, (c9_2(a53, a54))). % 20.25/6.79 tff(c_6050, plain, (c2_2(a7, a8))). % 20.25/6.79 tff(c_6043, plain, (c10_1(a102))). % 20.25/6.79 tff(c_6035, plain, (c3_1(a18))). % 20.25/6.79 tff(c_6032, plain, (c4_1(a102))). % 20.25/6.79 tff(c_6029, plain, (c6_1(a18))). % 20.25/6.79 tff(c_6018, plain, (ndr1_1(a102))). % 20.25/6.79 tff(c_6010, plain, (~c5_2(a136, a137))). % 20.25/6.79 tff(c_6003, plain, (~c3_1(a16))). % 20.25/6.79 tff(c_5999, plain, (~c3_2(a53, a54))). % 20.25/6.79 tff(c_5997, plain, (~c5_2(a143, a144))). % 20.25/6.79 tff(c_5994, plain, (~c9_1(a121))). % 20.25/6.79 tff(c_5986, plain, (~c6_1(a121))). % 20.25/6.79 tff(c_5984, plain, (c9_2(a143, a144))). % 20.25/6.79 tff(c_5981, plain, (~c10_2(a143, a144))). % 20.25/6.79 tff(c_5980, plain, (~c10_2(a136, a137))). % 20.25/6.79 tff(c_5978, plain, (c2_2(a136, a137))). % 20.25/6.79 tff(c_5976, plain, (~c10_1(a121))). % 20.25/6.79 tff(c_5974, plain, (c4_1(a126))). % 20.25/6.79 tff(c_5970, plain, (c6_1(a126))). % 20.25/6.79 tff(c_5962, plain, (~c9_2(a7, a8))). % 20.25/6.79 tff(c_5952, plain, (ndr1_1(a7))). % 20.25/6.79 tff(c_5947, plain, (~c9_0)). % 20.25/6.79 tff(c_5945, plain, (ndr1_1(a143))). % 20.25/6.79 tff(c_5940, plain, (c10_1(a7))). % 20.25/6.79 tff(c_5933, plain, (ndr1_1(a53))). % 20.25/6.79 tff(c_5925, plain, (c8_1(a7))). % 20.25/6.79 tff(c_5921, plain, (~c6_1(a6))). % 20.25/6.79 tff(c_5920, plain, (c1_1(a143))). % 20.25/6.79 tff(c_5918, plain, (c4_1(a127))). % 20.25/6.79 tff(c_5915, plain, (ndr1_1(a136))). % 20.25/6.79 tff(c_5913, plain, (c7_1(a136))). % 20.25/6.79 tff(c_5906, plain, (~c8_1(a136))). % 20.25/6.79 tff(c_5904, plain, (~c10_0)). % 20.25/6.79 tff(c_5901, plain, (~c4_1(a6))). % 20.25/6.79 tff(c_5899, plain, (~c2_1(a127))). % 20.25/6.79 tff(c_5890, plain, (c8_0)). % 20.25/6.79 tff(c_5889, plain, (~c7_0)). % 20.25/6.79 tff(c_5888, plain, (~c6_0)). % 20.25/6.79 tff(c_5885, plain, (~c4_0)). % 20.25/6.79 tff(c_5882, plain, (c1_0)). % 20.25/6.79 tff(c_5879, plain, (~c3_0)). % 20.25/6.79 tff(c_5876, plain, (c2_0)). % 20.25/6.79 tff(c_5875, plain, (c5_0)). % 20.25/6.79 tff(c_3734, plain, (ndr1_0)). % 20.53/6.79 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.53/6.79 %------------------------------------------------------------------------------