%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN545+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 : n029.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 : CounterSatisfiable 33.24s 17.83s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN545+1 : TPTP v9.0.0. Released v2.1.0. % 0.11/0.13 % 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 : n029.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.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Apr 9 07:59:04 EDT 2025 % 0.14/0.35 % CPUTime : % 33.24/17.83 % 33.24/17.83 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.24/17.84 % 33.24/17.84 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.33/17.85 %$ c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ndr1_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ndr1_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a297 > a296 > a295 > a294 > a293 > a292 > a291 > a290 > a289 > a288 > a287 > a286 > a285 > a284 > a283 > a282 > a281 > a280 > a279 > a278 > a277 > a276 > a275 > a274 > a273 > a272 > a271 > a270 > a269 > a268 > a267 > a266 > a265 > a264 > a263 > a262 > a261 > a260 > a259 > a258 > a257 > a256 > a255 > a254 > a253 > a252 > a251 > a250 > a249 > a248 > a247 > a246 > a245 > a244 > a243 > a242 > a241 > a240 > a239 > a238 > a237 > a236 > a235 > a234 > a233 > a232 > a231 > a230 > a229 > a228 > a227 > a226 > a225 > a224 > a223 > a222 > a221 > a220 > a219 > a218 > a217 > a216 > a215 > a214 > a213 > a212 > a211 > a210 > a209 > a208 > a207 > a206 > a205 > a204 > a203 > a202 > a201 > a200 > a199 > a198 > a197 > a196 > a195 > a194 > a193 > a192 > a191 > a190 > a189 > a188 > a187 > a186 > a185 > a184 > a183 > a182 > a181 > a180 > a179 > a178 > a177 > a176 > a175 > a174 > a173 > a172 > a171 > a170 > a169 > a168 > a167 > a166 > a165 > a164 > a163 > a162 > a161 > a160 > a159 > a158 > a157 > a156 > a155 > a154 > a153 > a152 > a151 > a150 > a149 > a148 > a147 % 33.33/17.85 % 33.33/17.85 %Foreground sorts: % 33.33/17.85 % 33.33/17.85 % 33.33/17.85 %Background operators: % 33.33/17.85 % 33.33/17.85 % 33.33/17.85 %Foreground operators: % 33.33/17.85 tff(a230, type, a230: $i). % 33.33/17.85 tff(a229, type, a229: $i). % 33.33/17.85 tff(a254, type, a254: $i). % 33.33/17.85 tff(c7_0, type, c7_0: $o). % 33.33/17.85 tff(a242, type, a242: $i). % 33.33/17.85 tff(a281, type, a281: $i). % 33.33/17.85 tff(a149, type, a149: $i). % 33.33/17.85 tff(a257, type, a257: $i). % 33.33/17.85 tff(a206, type, a206: $i). % 33.33/17.85 tff(a178, type, a178: $i). % 33.33/17.85 tff(a169, type, a169: $i). % 33.33/17.85 tff(a292, type, a292: $i). % 33.33/17.85 tff(c4_0, type, c4_0: $o). % 33.33/17.85 tff(a217, type, a217: $i). % 33.33/17.85 tff(a207, type, a207: $i). % 33.33/17.85 tff(a280, type, a280: $i). % 33.33/17.85 tff(a297, type, a297: $i). % 33.33/17.85 tff(a290, type, a290: $i). % 33.33/17.85 tff(a167, type, a167: $i). % 33.33/17.85 tff(a198, type, a198: $i). % 33.33/17.85 tff(a215, type, a215: $i). % 33.33/17.85 tff(a249, type, a249: $i). % 33.33/17.85 tff(a201, type, a201: $i). % 33.33/17.85 tff(c3_0, type, c3_0: $o). % 33.33/17.85 tff(a211, type, a211: $i). % 33.33/17.85 tff(a213, type, a213: $i). % 33.33/17.85 tff(c1_2, type, c1_2: ($i * $i) > $o). % 33.33/17.85 tff(a272, type, a272: $i). % 33.33/17.85 tff(a200, type, a200: $i). % 33.33/17.85 tff(a233, type, a233: $i). % 33.33/17.85 tff(a192, type, a192: $i). % 33.33/17.85 tff(a157, type, a157: $i). % 33.33/17.85 tff(a264, type, a264: $i). % 33.33/17.85 tff(a185, type, a185: $i). % 33.33/17.85 tff(a284, type, a284: $i). % 33.33/17.85 tff(a147, type, a147: $i). % 33.33/17.85 tff(a171, type, a171: $i). % 33.33/17.85 tff(a295, type, a295: $i). % 33.33/17.85 tff(a194, type, a194: $i). % 33.33/17.85 tff(a161, type, a161: $i). % 33.33/17.85 tff(a214, type, a214: $i). % 33.33/17.85 tff(a285, type, a285: $i). % 33.33/17.85 tff(a184, type, a184: $i). % 33.33/17.85 tff(a204, type, a204: $i). % 33.33/17.85 tff(a266, type, a266: $i). % 33.33/17.85 tff(a232, type, a232: $i). % 33.33/17.85 tff(a153, type, a153: $i). % 33.33/17.85 tff(c8_0, type, c8_0: $o). % 33.33/17.85 tff(a269, type, a269: $i). % 33.33/17.85 tff(a174, type, a174: $i). % 33.33/17.85 tff(a166, type, a166: $i). % 33.33/17.85 tff(a286, type, a286: $i). % 33.33/17.85 tff(a237, type, a237: $i). % 33.33/17.85 tff(a176, type, a176: $i). % 33.33/17.85 tff(a183, type, a183: $i). % 33.33/17.85 tff(a248, type, a248: $i). % 33.33/17.85 tff(a165, type, a165: $i). % 33.33/17.85 tff(a291, type, a291: $i). % 33.33/17.85 tff(a283, type, a283: $i). % 33.33/17.85 tff(a238, type, a238: $i). % 33.33/17.85 tff(a228, type, a228: $i). % 33.33/17.85 tff(a293, type, a293: $i). % 33.33/17.85 tff(a179, type, a179: $i). % 33.33/17.85 tff(a294, type, a294: $i). % 33.33/17.85 tff(c5_0, type, c5_0: $o). % 33.33/17.85 tff(a180, type, a180: $i). % 33.33/17.85 tff(a173, type, a173: $i). % 33.33/17.85 tff(a268, type, a268: $i). % 33.33/17.85 tff(a261, type, a261: $i). % 33.33/17.85 tff(a163, type, a163: $i). % 33.33/17.85 tff(a245, type, a245: $i). % 33.33/17.85 tff(c6_0, type, c6_0: $o). % 33.33/17.85 tff(a154, type, a154: $i). % 33.33/17.85 tff(a235, type, a235: $i). % 33.33/17.85 tff(c8_2, type, c8_2: ($i * $i) > $o). % 33.33/17.85 tff(a270, type, a270: $i). % 33.33/17.85 tff(a210, type, a210: $i). % 33.33/17.85 tff(a187, type, a187: $i). % 33.33/17.85 tff(a278, type, a278: $i). % 33.33/17.85 tff(a222, type, a222: $i). % 33.33/17.85 tff(a220, type, a220: $i). % 33.33/17.85 tff(a227, type, a227: $i). % 33.33/17.85 tff(a265, type, a265: $i). % 33.33/17.85 tff(a251, type, a251: $i). % 33.33/17.85 tff(a236, type, a236: $i). % 33.33/17.85 tff(a275, type, a275: $i). % 33.33/17.85 tff(a205, type, a205: $i). % 33.33/17.85 tff(a246, type, a246: $i). % 33.33/17.85 tff(a193, type, a193: $i). % 33.33/17.85 tff(a160, type, a160: $i). % 33.33/17.85 tff(a196, type, a196: $i). % 33.33/17.85 tff(a218, type, a218: $i). % 33.33/17.85 tff(a282, type, a282: $i). % 33.33/17.85 tff(a273, type, a273: $i). % 33.33/17.85 tff(c1_0, type, c1_0: $o). % 33.33/17.85 tff(a240, type, a240: $i). % 33.33/17.85 tff(c8_1, type, c8_1: $i > $o). % 33.33/17.85 tff(a203, type, a203: $i). % 33.33/17.85 tff(a172, type, a172: $i). % 33.33/17.85 tff(a234, type, a234: $i). % 33.33/17.85 tff(a151, type, a151: $i). % 33.33/17.85 tff(a250, type, a250: $i). % 33.33/17.85 tff(a267, type, a267: $i). % 33.33/17.85 tff(a189, type, a189: $i). % 33.33/17.85 tff(c2_1, type, c2_1: $i > $o). % 33.33/17.85 tff(a219, type, a219: $i). % 33.33/17.85 tff(a258, type, a258: $i). % 33.33/17.85 tff(a191, type, a191: $i). % 33.33/17.85 tff(ndr1_1, type, ndr1_1: $i > $o). % 33.33/17.85 tff(c2_0, type, c2_0: $o). % 33.33/17.85 tff(c4_1, type, c4_1: $i > $o). % 33.33/17.85 tff(a277, type, a277: $i). % 33.33/17.85 tff(a274, type, a274: $i). % 33.33/17.85 tff(a223, type, a223: $i). % 33.33/17.85 tff(a271, type, a271: $i). % 33.33/17.85 tff(a252, type, a252: $i). % 33.33/17.85 tff(a159, type, a159: $i). % 33.33/17.85 tff(a186, type, a186: $i). % 33.33/17.85 tff(a243, type, a243: $i). % 33.33/17.85 tff(a158, type, a158: $i). % 33.33/17.85 tff(c6_2, type, c6_2: ($i * $i) > $o). % 33.33/17.85 tff(a260, type, a260: $i). % 33.33/17.85 tff(a212, type, a212: $i). % 33.33/17.85 tff(a195, type, a195: $i). % 33.33/17.85 tff(a263, type, a263: $i). % 33.33/17.85 tff(a188, type, a188: $i). % 33.33/17.85 tff(a175, type, a175: $i). % 33.33/17.85 tff(a289, type, a289: $i). % 33.33/17.85 tff(a202, type, a202: $i). % 33.33/17.85 tff(a226, type, a226: $i). % 33.33/17.85 tff(ndr1_0, type, ndr1_0: $o). % 33.33/17.85 tff(a288, type, a288: $i). % 33.33/17.85 tff(a287, type, a287: $i). % 33.33/17.85 tff(a155, type, a155: $i). % 33.33/17.85 tff(a197, type, a197: $i). % 33.33/17.85 tff(a241, type, a241: $i). % 33.33/17.85 tff(a231, type, a231: $i). % 33.33/17.85 tff(a224, type, a224: $i). % 33.33/17.85 tff(a177, type, a177: $i). % 33.33/17.85 tff(a150, type, a150: $i). % 33.33/17.85 tff(a255, type, a255: $i). % 33.33/17.85 tff(a182, type, a182: $i). % 33.33/17.85 tff(a208, type, a208: $i). % 33.33/17.85 tff(a253, type, a253: $i). % 33.33/17.85 tff(c1_1, type, c1_1: $i > $o). % 33.33/17.85 tff(a170, type, a170: $i). % 33.33/17.85 tff(a156, type, a156: $i). % 33.33/17.85 tff(c5_2, type, c5_2: ($i * $i) > $o). % 33.33/17.85 tff(a190, type, a190: $i). % 33.33/17.85 tff(a225, type, a225: $i). % 33.33/17.85 tff(a148, type, a148: $i). % 33.33/17.85 tff(a216, type, a216: $i). % 33.33/17.85 tff(c7_1, type, c7_1: $i > $o). % 33.33/17.85 tff(c6_1, type, c6_1: $i > $o). % 33.33/17.85 tff(c4_2, type, c4_2: ($i * $i) > $o). % 33.33/17.85 tff(a259, type, a259: $i). % 33.33/17.85 tff(a276, type, a276: $i). % 33.33/17.85 tff(a262, type, a262: $i). % 33.33/17.85 tff(a239, type, a239: $i). % 33.33/17.85 tff(a164, type, a164: $i). % 33.33/17.85 tff(a247, type, a247: $i). % 33.33/17.85 tff(a279, type, a279: $i). % 33.33/17.85 tff(a209, type, a209: $i). % 33.33/17.85 tff(a296, type, a296: $i). % 33.33/17.85 tff(c5_1, type, c5_1: $i > $o). % 33.33/17.85 tff(a221, type, a221: $i). % 33.33/17.85 tff(c7_2, type, c7_2: ($i * $i) > $o). % 33.33/17.85 tff(c3_2, type, c3_2: ($i * $i) > $o). % 33.33/17.85 tff(c2_2, type, c2_2: ($i * $i) > $o). % 33.33/17.85 tff(a181, type, a181: $i). % 33.33/17.85 tff(a162, type, a162: $i). % 33.33/17.85 tff(a168, type, a168: $i). % 33.33/17.85 tff(a244, type, a244: $i). % 33.33/17.85 tff(a199, type, a199: $i). % 33.33/17.85 tff(a152, type, a152: $i). % 33.33/17.85 tff(c3_1, type, c3_1: $i > $o). % 33.33/17.85 tff(a256, type, a256: $i). % 33.33/17.85 % 33.33/17.85 %Saturated clause set: % 33.33/17.85 tff(c_15962, plain, (![X77_1271, X39_1270, V_1272, X40_1273, X40_762, V_4]: (~c5_2(X39_1270, X77_1271) | c4_2(X39_1270, V_4) | c3_2(X39_1270, V_4) | ~c3_2(X39_1270, X40_762) | c4_2(X39_1270, X40_762) | ~c1_2(X39_1270, X40_762) | c4_2(X39_1270, a152) | ~c1_2(X39_1270, a152) | ~c6_2(X39_1270, X77_1271) | c4_2(X39_1270, X77_1271) | c4_2(X39_1270, a264) | c4_2(X39_1270, V_1272) | c3_2(X39_1270, V_1272) | c7_1(X39_1270) | c4_2(X39_1270, X40_1273) | ~c6_2(X39_1270, a147) | c4_2(X39_1270, a147) | c5_2(X39_1270, X40_1273) | ~c1_2(X39_1270, X40_1273) | ~c5_1(X39_1270) | ~c3_2(X39_1270, a264) | ~c6_1(X39_1270) | c1_1(X39_1270) | c5_2(X39_1270, a263) | ~c1_2(X39_1270, a263) | ~ndr1_1(X39_1270) | c8_1(X39_1270)))). % 33.33/17.85 tff(c_15971, plain, (![X77_1271, X39_1270, V_1272, X40_340, X40_1273, V_4]: (~c5_2(X39_1270, X77_1271) | c4_2(X39_1270, V_4) | c3_2(X39_1270, V_4) | c4_2(X39_1270, X40_340) | c5_2(X39_1270, X40_340) | ~c1_2(X39_1270, X40_340) | c4_2(X39_1270, a152) | ~c1_2(X39_1270, a152) | ~c6_2(X39_1270, X77_1271) | c4_2(X39_1270, X77_1271) | c4_2(X39_1270, a264) | c4_2(X39_1270, V_1272) | c3_2(X39_1270, V_1272) | c7_1(X39_1270) | c4_2(X39_1270, X40_1273) | ~c6_2(X39_1270, a147) | c4_2(X39_1270, a147) | c5_2(X39_1270, X40_1273) | ~c1_2(X39_1270, X40_1273) | ~c5_1(X39_1270) | ~c3_2(X39_1270, a264) | ~c6_1(X39_1270) | c1_1(X39_1270) | c5_2(X39_1270, a263) | ~c1_2(X39_1270, a263) | ~ndr1_1(X39_1270) | c8_1(X39_1270)))). % 33.33/17.85 tff(c_15969, plain, (![X77_1271, X39_1270, V_1272, X40_1273, X4_431, V_4]: (~c5_2(X39_1270, X77_1271) | c4_2(X39_1270, V_4) | c3_2(X39_1270, V_4) | ~c5_2(X39_1270, X4_431) | c7_2(X39_1270, X4_431) | ~c3_2(X39_1270, X4_431) | c4_2(X39_1270, a152) | ~c1_2(X39_1270, a152) | ~c6_2(X39_1270, X77_1271) | c4_2(X39_1270, X77_1271) | c4_2(X39_1270, a264) | c4_2(X39_1270, V_1272) | c3_2(X39_1270, V_1272) | c7_1(X39_1270) | c4_2(X39_1270, X40_1273) | ~c6_2(X39_1270, a147) | c4_2(X39_1270, a147) | c5_2(X39_1270, X40_1273) | ~c1_2(X39_1270, X40_1273) | ~c5_1(X39_1270) | ~c3_2(X39_1270, a264) | ~c6_1(X39_1270) | c1_1(X39_1270) | c5_2(X39_1270, a263) | ~c1_2(X39_1270, a263) | ~ndr1_1(X39_1270) | c8_1(X39_1270)))). % 33.33/17.86 tff(c_15626, plain, (![X141_1243, V_1245, X77_1244, X40_1246, X40_762, V_4]: (~c5_2(X141_1243, X77_1244) | c4_2(X141_1243, V_4) | c3_2(X141_1243, V_4) | ~c3_2(X141_1243, X40_762) | c4_2(X141_1243, X40_762) | ~c1_2(X141_1243, X40_762) | c4_2(X141_1243, a152) | ~c1_2(X141_1243, a152) | ~c6_2(X141_1243, X77_1244) | c4_2(X141_1243, X77_1244) | c4_2(X141_1243, a264) | c4_2(X141_1243, V_1245) | c3_2(X141_1243, V_1245) | c7_1(X141_1243) | c4_2(X141_1243, X40_1246) | ~c6_2(X141_1243, a147) | c4_2(X141_1243, a147) | c1_1(X141_1243) | c5_2(X141_1243, X40_1246) | ~c1_2(X141_1243, X40_1246) | c8_1(X141_1243) | ~c5_1(X141_1243) | ~c3_2(X141_1243, a264) | ~ndr1_1(X141_1243) | ~c5_2(X141_1243, a263) | ~c6_1(X141_1243)))). % 33.33/17.86 tff(c_15344, plain, (![X40_1238, X141_1235, X40_762, V_1237, V_4, X77_1236]: (~c5_2(X141_1235, X77_1236) | c4_2(X141_1235, V_4) | c3_2(X141_1235, V_4) | ~c3_2(X141_1235, X40_762) | c4_2(X141_1235, X40_762) | ~c1_2(X141_1235, X40_762) | c4_2(X141_1235, a152) | ~c1_2(X141_1235, a152) | ~c6_2(X141_1235, X77_1236) | c4_2(X141_1235, X77_1236) | c4_2(X141_1235, a264) | c4_2(X141_1235, V_1237) | c3_2(X141_1235, V_1237) | c7_1(X141_1235) | c4_2(X141_1235, X40_1238) | ~c6_2(X141_1235, a147) | c4_2(X141_1235, a147) | c1_1(X141_1235) | c5_2(X141_1235, X40_1238) | ~c1_2(X141_1235, X40_1238) | c8_1(X141_1235) | ~c5_1(X141_1235) | ~c3_2(X141_1235, a264) | ~ndr1_1(X141_1235) | c4_2(X141_1235, a263) | ~c6_1(X141_1235)))). % 33.33/17.86 tff(c_15351, plain, (![X40_1238, X4_431, X141_1235, V_1237, V_4, X77_1236]: (~c5_2(X141_1235, X77_1236) | c4_2(X141_1235, V_4) | c3_2(X141_1235, V_4) | ~c5_2(X141_1235, X4_431) | c7_2(X141_1235, X4_431) | ~c3_2(X141_1235, X4_431) | c4_2(X141_1235, a152) | ~c1_2(X141_1235, a152) | ~c6_2(X141_1235, X77_1236) | c4_2(X141_1235, X77_1236) | c4_2(X141_1235, a264) | c4_2(X141_1235, V_1237) | c3_2(X141_1235, V_1237) | c7_1(X141_1235) | c4_2(X141_1235, X40_1238) | ~c6_2(X141_1235, a147) | c4_2(X141_1235, a147) | c1_1(X141_1235) | c5_2(X141_1235, X40_1238) | ~c1_2(X141_1235, X40_1238) | c8_1(X141_1235) | ~c5_1(X141_1235) | ~c3_2(X141_1235, a264) | ~ndr1_1(X141_1235) | c4_2(X141_1235, a263) | ~c6_1(X141_1235)))). % 33.33/17.86 tff(c_15353, plain, (![X40_1238, X40_340, X141_1235, V_1237, V_4, X77_1236]: (~c5_2(X141_1235, X77_1236) | c4_2(X141_1235, V_4) | c3_2(X141_1235, V_4) | c4_2(X141_1235, X40_340) | c5_2(X141_1235, X40_340) | ~c1_2(X141_1235, X40_340) | c4_2(X141_1235, a152) | ~c1_2(X141_1235, a152) | ~c6_2(X141_1235, X77_1236) | c4_2(X141_1235, X77_1236) | c4_2(X141_1235, a264) | c4_2(X141_1235, V_1237) | c3_2(X141_1235, V_1237) | c7_1(X141_1235) | c4_2(X141_1235, X40_1238) | ~c6_2(X141_1235, a147) | c4_2(X141_1235, a147) | c1_1(X141_1235) | c5_2(X141_1235, X40_1238) | ~c1_2(X141_1235, X40_1238) | c8_1(X141_1235) | ~c5_1(X141_1235) | ~c3_2(X141_1235, a264) | ~ndr1_1(X141_1235) | c4_2(X141_1235, a263) | ~c6_1(X141_1235)))). % 33.33/17.86 tff(c_15633, plain, (![X141_1243, V_1245, X77_1244, X4_431, X40_1246, V_4]: (~c5_2(X141_1243, X77_1244) | c4_2(X141_1243, V_4) | c3_2(X141_1243, V_4) | ~c5_2(X141_1243, X4_431) | c7_2(X141_1243, X4_431) | ~c3_2(X141_1243, X4_431) | c4_2(X141_1243, a152) | ~c1_2(X141_1243, a152) | ~c6_2(X141_1243, X77_1244) | c4_2(X141_1243, X77_1244) | c4_2(X141_1243, a264) | c4_2(X141_1243, V_1245) | c3_2(X141_1243, V_1245) | c7_1(X141_1243) | c4_2(X141_1243, X40_1246) | ~c6_2(X141_1243, a147) | c4_2(X141_1243, a147) | c1_1(X141_1243) | c5_2(X141_1243, X40_1246) | ~c1_2(X141_1243, X40_1246) | c8_1(X141_1243) | ~c5_1(X141_1243) | ~c3_2(X141_1243, a264) | ~ndr1_1(X141_1243) | ~c5_2(X141_1243, a263) | ~c6_1(X141_1243)))). % 33.33/17.86 tff(c_15635, plain, (![X141_1243, V_1245, X77_1244, X40_340, X40_1246, V_4]: (~c5_2(X141_1243, X77_1244) | c4_2(X141_1243, V_4) | c3_2(X141_1243, V_4) | c4_2(X141_1243, X40_340) | c5_2(X141_1243, X40_340) | ~c1_2(X141_1243, X40_340) | c4_2(X141_1243, a152) | ~c1_2(X141_1243, a152) | ~c6_2(X141_1243, X77_1244) | c4_2(X141_1243, X77_1244) | c4_2(X141_1243, a264) | c4_2(X141_1243, V_1245) | c3_2(X141_1243, V_1245) | c7_1(X141_1243) | c4_2(X141_1243, X40_1246) | ~c6_2(X141_1243, a147) | c4_2(X141_1243, a147) | c1_1(X141_1243) | c5_2(X141_1243, X40_1246) | ~c1_2(X141_1243, X40_1246) | c8_1(X141_1243) | ~c5_1(X141_1243) | ~c3_2(X141_1243, a264) | ~ndr1_1(X141_1243) | ~c5_2(X141_1243, a263) | ~c6_1(X141_1243)))). % 33.33/17.86 tff(c_15024, plain, (![X40_1177, V_1176, X39_1175, X40_340, V_4]: (~c5_2(X39_1175, a152) | c4_2(X39_1175, V_4) | c3_2(X39_1175, V_4) | c4_2(X39_1175, X40_340) | c5_2(X39_1175, X40_340) | ~c1_2(X39_1175, X40_340) | c4_2(X39_1175, a264) | c4_2(X39_1175, V_1176) | c3_2(X39_1175, V_1176) | c4_2(X39_1175, a152) | ~c1_2(X39_1175, a152) | ~c3_2(X39_1175, X40_1177) | c7_1(X39_1175) | c4_2(X39_1175, X40_1177) | ~c6_2(X39_1175, a147) | c4_2(X39_1175, a147) | ~c1_2(X39_1175, X40_1177) | ~c5_1(X39_1175) | ~c3_2(X39_1175, a264) | ~c6_1(X39_1175) | c1_1(X39_1175) | c5_2(X39_1175, a263) | ~c1_2(X39_1175, a263) | ~ndr1_1(X39_1175) | c8_1(X39_1175)))). % 33.33/17.86 tff(c_15019, plain, (![X40_1177, V_1176, X39_1175, X40_762, V_4]: (~c5_2(X39_1175, a152) | c4_2(X39_1175, V_4) | c3_2(X39_1175, V_4) | ~c3_2(X39_1175, X40_762) | c4_2(X39_1175, X40_762) | ~c1_2(X39_1175, X40_762) | c4_2(X39_1175, a264) | c4_2(X39_1175, V_1176) | c3_2(X39_1175, V_1176) | c4_2(X39_1175, a152) | ~c1_2(X39_1175, a152) | ~c3_2(X39_1175, X40_1177) | c7_1(X39_1175) | c4_2(X39_1175, X40_1177) | ~c6_2(X39_1175, a147) | c4_2(X39_1175, a147) | ~c1_2(X39_1175, X40_1177) | ~c5_1(X39_1175) | ~c3_2(X39_1175, a264) | ~c6_1(X39_1175) | c1_1(X39_1175) | c5_2(X39_1175, a263) | ~c1_2(X39_1175, a263) | ~ndr1_1(X39_1175) | c8_1(X39_1175)))). % 33.33/17.86 tff(c_13631, plain, (![X39_937, V_938, X40_939, X40_762, V_4]: (~c5_2(X39_937, a152) | c4_2(X39_937, V_4) | c3_2(X39_937, V_4) | c4_2(X39_937, a152) | ~c1_2(X39_937, a152) | ~c3_2(X39_937, X40_762) | c4_2(X39_937, X40_762) | ~c1_2(X39_937, X40_762) | c4_2(X39_937, a264) | c4_2(X39_937, V_938) | c3_2(X39_937, V_938) | c7_1(X39_937) | c4_2(X39_937, X40_939) | ~c6_2(X39_937, a147) | c4_2(X39_937, a147) | c5_2(X39_937, X40_939) | ~c1_2(X39_937, X40_939) | ~c5_1(X39_937) | ~c3_2(X39_937, a264) | ~c6_1(X39_937) | c1_1(X39_937) | c5_2(X39_937, a263) | ~c1_2(X39_937, a263) | ~ndr1_1(X39_937) | c8_1(X39_937)))). % 33.33/17.86 tff(c_14758, plain, (![X40_1075, X141_1073, V_1074, X40_762, V_4]: (~c5_2(X141_1073, a152) | c4_2(X141_1073, V_4) | c3_2(X141_1073, V_4) | ~c3_2(X141_1073, X40_762) | c4_2(X141_1073, X40_762) | ~c1_2(X141_1073, X40_762) | c4_2(X141_1073, a264) | c4_2(X141_1073, V_1074) | c3_2(X141_1073, V_1074) | c4_2(X141_1073, a152) | ~c1_2(X141_1073, a152) | ~c3_2(X141_1073, X40_1075) | c7_1(X141_1073) | c4_2(X141_1073, X40_1075) | ~c6_2(X141_1073, a147) | c4_2(X141_1073, a147) | c1_1(X141_1073) | ~c1_2(X141_1073, X40_1075) | c8_1(X141_1073) | ~c5_1(X141_1073) | ~c3_2(X141_1073, a264) | ~ndr1_1(X141_1073) | c4_2(X141_1073, a263) | ~c6_1(X141_1073)))). % 33.33/17.86 tff(c_14834, plain, (![V_1077, X40_1078, X40_762, X141_1076, V_4]: (~c5_2(X141_1076, a152) | c4_2(X141_1076, V_4) | c3_2(X141_1076, V_4) | ~c3_2(X141_1076, X40_762) | c4_2(X141_1076, X40_762) | ~c1_2(X141_1076, X40_762) | c4_2(X141_1076, a264) | c4_2(X141_1076, V_1077) | c3_2(X141_1076, V_1077) | c4_2(X141_1076, a152) | ~c1_2(X141_1076, a152) | ~c3_2(X141_1076, X40_1078) | c7_1(X141_1076) | c4_2(X141_1076, X40_1078) | ~c6_2(X141_1076, a147) | c4_2(X141_1076, a147) | c1_1(X141_1076) | ~c1_2(X141_1076, X40_1078) | c8_1(X141_1076) | ~c5_1(X141_1076) | ~c3_2(X141_1076, a264) | ~ndr1_1(X141_1076) | ~c5_2(X141_1076, a263) | ~c6_1(X141_1076)))). % 33.33/17.86 tff(c_14839, plain, (![V_1077, X40_340, X40_1078, X141_1076, V_4]: (~c5_2(X141_1076, a152) | c4_2(X141_1076, V_4) | c3_2(X141_1076, V_4) | c4_2(X141_1076, X40_340) | c5_2(X141_1076, X40_340) | ~c1_2(X141_1076, X40_340) | c4_2(X141_1076, a264) | c4_2(X141_1076, V_1077) | c3_2(X141_1076, V_1077) | c4_2(X141_1076, a152) | ~c1_2(X141_1076, a152) | ~c3_2(X141_1076, X40_1078) | c7_1(X141_1076) | c4_2(X141_1076, X40_1078) | ~c6_2(X141_1076, a147) | c4_2(X141_1076, a147) | c1_1(X141_1076) | ~c1_2(X141_1076, X40_1078) | c8_1(X141_1076) | ~c5_1(X141_1076) | ~c3_2(X141_1076, a264) | ~ndr1_1(X141_1076) | ~c5_2(X141_1076, a263) | ~c6_1(X141_1076)))). % 33.33/17.86 tff(c_14763, plain, (![X40_1075, X141_1073, V_1074, X40_340, V_4]: (~c5_2(X141_1073, a152) | c4_2(X141_1073, V_4) | c3_2(X141_1073, V_4) | c4_2(X141_1073, X40_340) | c5_2(X141_1073, X40_340) | ~c1_2(X141_1073, X40_340) | c4_2(X141_1073, a264) | c4_2(X141_1073, V_1074) | c3_2(X141_1073, V_1074) | c4_2(X141_1073, a152) | ~c1_2(X141_1073, a152) | ~c3_2(X141_1073, X40_1075) | c7_1(X141_1073) | c4_2(X141_1073, X40_1075) | ~c6_2(X141_1073, a147) | c4_2(X141_1073, a147) | c1_1(X141_1073) | ~c1_2(X141_1073, X40_1075) | c8_1(X141_1073) | ~c5_1(X141_1073) | ~c3_2(X141_1073, a264) | ~ndr1_1(X141_1073) | c4_2(X141_1073, a263) | ~c6_1(X141_1073)))). % 33.33/17.86 tff(c_13289, plain, (![X40_749, V_909, V_748, X40_910, X141_191]: (~c5_2(X141_191, a152) | c4_2(X141_191, V_909) | c3_2(X141_191, V_909) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c3_2(X141_191, X40_910) | c4_2(X141_191, X40_910) | ~c1_2(X141_191, X40_910) | c4_2(X141_191, a264) | c4_2(X141_191, V_748) | c3_2(X141_191, V_748) | c7_1(X141_191) | c4_2(X141_191, X40_749) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | c5_2(X141_191, X40_749) | ~c1_2(X141_191, X40_749) | c8_1(X141_191) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.33/17.86 tff(c_13288, plain, (![X40_749, V_909, V_748, X40_910, X141_191]: (~c5_2(X141_191, a152) | c4_2(X141_191, V_909) | c3_2(X141_191, V_909) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c3_2(X141_191, X40_910) | c4_2(X141_191, X40_910) | ~c1_2(X141_191, X40_910) | c4_2(X141_191, a264) | c4_2(X141_191, V_748) | c3_2(X141_191, V_748) | c7_1(X141_191) | c4_2(X141_191, X40_749) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | c5_2(X141_191, X40_749) | ~c1_2(X141_191, X40_749) | c8_1(X141_191) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.33/17.86 tff(c_13636, plain, (![X39_937, V_938, X40_939, X40_340, V_4]: (c4_2(X39_937, a152) | ~c5_2(X39_937, a152) | c4_2(X39_937, V_4) | c3_2(X39_937, V_4) | c4_2(X39_937, X40_340) | c5_2(X39_937, X40_340) | ~c1_2(X39_937, X40_340) | c4_2(X39_937, a264) | c4_2(X39_937, V_938) | c3_2(X39_937, V_938) | c7_1(X39_937) | c4_2(X39_937, X40_939) | ~c6_2(X39_937, a147) | c4_2(X39_937, a147) | c5_2(X39_937, X40_939) | ~c1_2(X39_937, X40_939) | ~c5_1(X39_937) | ~c3_2(X39_937, a264) | ~c6_1(X39_937) | c1_1(X39_937) | c5_2(X39_937, a263) | ~c1_2(X39_937, a263) | ~ndr1_1(X39_937) | c8_1(X39_937)))). % 33.33/17.87 tff(c_13127, plain, (![V_894, X40_895, X4_896, X3_893, V_4]: (c4_2(X3_893, X4_896) | c4_2(X3_893, V_4) | c3_2(X3_893, V_4) | c4_2(X3_893, a264) | ~c1_2(X3_893, a264) | ~c6_1(X3_893) | c5_2(X3_893, a263) | ~c1_2(X3_893, a263) | c4_2(X3_893, a152) | ~c5_2(X3_893, a152) | c4_2(X3_893, V_894) | c3_2(X3_893, V_894) | c7_1(X3_893) | c4_2(X3_893, X40_895) | ~c6_2(X3_893, a147) | c4_2(X3_893, a147) | c1_1(X3_893) | c5_2(X3_893, X40_895) | ~c1_2(X3_893, X40_895) | c8_1(X3_893) | ~c5_1(X3_893) | ~c5_2(X3_893, X4_896) | ~c3_2(X3_893, X4_896) | ~ndr1_1(X3_893)))). % 33.33/17.87 tff(c_13287, plain, (![X40_540, X3_12, V_909, X40_910, V_539, X4_14]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_909) | c3_2(X3_12, V_909) | ~c1_2(X3_12, a152) | ~c3_2(X3_12, X40_910) | c4_2(X3_12, X40_910) | ~c1_2(X3_12, X40_910) | c4_2(X3_12, a152) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c7_1(X3_12) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.33/17.87 tff(c_15022, plain, (![X39_1175, V_4, V_1176, X40_1177]: (~c5_2(X39_1175, a152) | c4_2(X39_1175, V_4) | c3_2(X39_1175, V_4) | ~c1_2(X39_1175, a264) | c4_2(X39_1175, a264) | c4_2(X39_1175, V_1176) | c3_2(X39_1175, V_1176) | c4_2(X39_1175, a152) | ~c1_2(X39_1175, a152) | ~c3_2(X39_1175, X40_1177) | c7_1(X39_1175) | c4_2(X39_1175, X40_1177) | ~c6_2(X39_1175, a147) | c4_2(X39_1175, a147) | ~c1_2(X39_1175, X40_1177) | ~c5_1(X39_1175) | ~c3_2(X39_1175, a264) | ~c6_1(X39_1175) | c1_1(X39_1175) | c5_2(X39_1175, a263) | ~c1_2(X39_1175, a263) | ~ndr1_1(X39_1175) | c8_1(X39_1175)))). % 33.33/17.87 tff(c_12637, plain, (![V_859, X141_858, X40_860, X40_340, V_4]: (c4_2(X141_858, a152) | ~c5_2(X141_858, a152) | c4_2(X141_858, V_4) | c3_2(X141_858, V_4) | c4_2(X141_858, X40_340) | c5_2(X141_858, X40_340) | ~c1_2(X141_858, X40_340) | c4_2(X141_858, a264) | c4_2(X141_858, V_859) | c3_2(X141_858, V_859) | c7_1(X141_858) | c4_2(X141_858, X40_860) | ~c6_2(X141_858, a147) | c4_2(X141_858, a147) | c1_1(X141_858) | c5_2(X141_858, X40_860) | ~c1_2(X141_858, X40_860) | c8_1(X141_858) | ~c5_1(X141_858) | ~c3_2(X141_858, a264) | ~ndr1_1(X141_858) | c4_2(X141_858, a263) | ~c6_1(X141_858)))). % 33.33/17.87 tff(c_12458, plain, (![X141_855, V_856, X40_857, X40_340, V_4]: (c4_2(X141_855, a152) | ~c5_2(X141_855, a152) | c4_2(X141_855, V_4) | c3_2(X141_855, V_4) | c4_2(X141_855, X40_340) | c5_2(X141_855, X40_340) | ~c1_2(X141_855, X40_340) | c4_2(X141_855, a264) | c4_2(X141_855, V_856) | c3_2(X141_855, V_856) | c7_1(X141_855) | c4_2(X141_855, X40_857) | ~c6_2(X141_855, a147) | c4_2(X141_855, a147) | c1_1(X141_855) | c5_2(X141_855, X40_857) | ~c1_2(X141_855, X40_857) | c8_1(X141_855) | ~c5_1(X141_855) | ~c3_2(X141_855, a264) | ~ndr1_1(X141_855) | ~c5_2(X141_855, a263) | ~c6_1(X141_855)))). % 33.33/17.87 tff(c_13132, plain, (![V_894, X40_895, X4_896, X3_893, V_4]: (c4_2(X3_893, X4_896) | c4_2(X3_893, V_4) | c3_2(X3_893, V_4) | c4_2(X3_893, a264) | ~c1_2(X3_893, a264) | ~c5_2(X3_893, a263) | ~c6_1(X3_893) | c4_2(X3_893, a152) | ~c5_2(X3_893, a152) | c4_2(X3_893, V_894) | c3_2(X3_893, V_894) | c7_1(X3_893) | c4_2(X3_893, X40_895) | ~c6_2(X3_893, a147) | c4_2(X3_893, a147) | c1_1(X3_893) | c5_2(X3_893, X40_895) | ~c1_2(X3_893, X40_895) | c8_1(X3_893) | ~c5_1(X3_893) | ~c5_2(X3_893, X4_896) | ~c3_2(X3_893, X4_896) | ~ndr1_1(X3_893)))). % 33.45/17.87 tff(c_14841, plain, (![X141_1076, V_4, V_1077, X40_1078]: (~c5_2(X141_1076, a152) | c4_2(X141_1076, V_4) | c3_2(X141_1076, V_4) | ~c1_2(X141_1076, a264) | c4_2(X141_1076, a264) | c4_2(X141_1076, V_1077) | c3_2(X141_1076, V_1077) | c4_2(X141_1076, a152) | ~c1_2(X141_1076, a152) | ~c3_2(X141_1076, X40_1078) | c7_1(X141_1076) | c4_2(X141_1076, X40_1078) | ~c6_2(X141_1076, a147) | c4_2(X141_1076, a147) | c1_1(X141_1076) | ~c1_2(X141_1076, X40_1078) | c8_1(X141_1076) | ~c5_1(X141_1076) | ~c3_2(X141_1076, a264) | ~ndr1_1(X141_1076) | ~c5_2(X141_1076, a263) | ~c6_1(X141_1076)))). % 33.45/17.87 tff(c_14764, plain, (![X141_1073, V_4, V_1074, X40_1075]: (~c5_2(X141_1073, a152) | c4_2(X141_1073, V_4) | c3_2(X141_1073, V_4) | ~c1_2(X141_1073, a264) | c4_2(X141_1073, a264) | c4_2(X141_1073, V_1074) | c3_2(X141_1073, V_1074) | c4_2(X141_1073, a152) | ~c1_2(X141_1073, a152) | ~c3_2(X141_1073, X40_1075) | c7_1(X141_1073) | c4_2(X141_1073, X40_1075) | ~c6_2(X141_1073, a147) | c4_2(X141_1073, a147) | c1_1(X141_1073) | ~c1_2(X141_1073, X40_1075) | c8_1(X141_1073) | ~c5_1(X141_1073) | ~c3_2(X141_1073, a264) | ~ndr1_1(X141_1073) | c4_2(X141_1073, a263) | ~c6_1(X141_1073)))). % 33.45/17.87 tff(c_15976, plain, (![X39_1270, X77_1271, V_1272, X40_1273]: (c4_1(X39_1270) | c1_2(X39_1270, X77_1271) | c2_2(X39_1270, X77_1271) | c4_2(X39_1270, a152) | ~c1_2(X39_1270, a152) | ~c6_2(X39_1270, X77_1271) | c4_2(X39_1270, X77_1271) | c4_2(X39_1270, a264) | c4_2(X39_1270, V_1272) | c3_2(X39_1270, V_1272) | c7_1(X39_1270) | c4_2(X39_1270, X40_1273) | ~c6_2(X39_1270, a147) | c4_2(X39_1270, a147) | c5_2(X39_1270, X40_1273) | ~c1_2(X39_1270, X40_1273) | ~c5_1(X39_1270) | ~c3_2(X39_1270, a264) | ~c6_1(X39_1270) | c1_1(X39_1270) | c5_2(X39_1270, a263) | ~c1_2(X39_1270, a263) | ~ndr1_1(X39_1270) | c8_1(X39_1270)))). % 33.45/17.87 tff(c_13131, plain, (![V_894, X40_895, X4_896, X3_893, V_4]: (c4_2(X3_893, X4_896) | c4_2(X3_893, V_4) | c3_2(X3_893, V_4) | c4_2(X3_893, a264) | ~c1_2(X3_893, a264) | c4_2(X3_893, a263) | ~c6_1(X3_893) | c4_2(X3_893, a152) | ~c5_2(X3_893, a152) | c4_2(X3_893, V_894) | c3_2(X3_893, V_894) | c7_1(X3_893) | c4_2(X3_893, X40_895) | ~c6_2(X3_893, a147) | c4_2(X3_893, a147) | c1_1(X3_893) | c5_2(X3_893, X40_895) | ~c1_2(X3_893, X40_895) | c8_1(X3_893) | ~c5_1(X3_893) | ~c5_2(X3_893, X4_896) | ~c3_2(X3_893, X4_896) | ~ndr1_1(X3_893)))). % 33.45/17.87 tff(c_15640, plain, (![X141_1243, X77_1244, V_1245, X40_1246]: (c4_1(X141_1243) | c1_2(X141_1243, X77_1244) | c2_2(X141_1243, X77_1244) | c4_2(X141_1243, a152) | ~c1_2(X141_1243, a152) | ~c6_2(X141_1243, X77_1244) | c4_2(X141_1243, X77_1244) | c4_2(X141_1243, a264) | c4_2(X141_1243, V_1245) | c3_2(X141_1243, V_1245) | c7_1(X141_1243) | c4_2(X141_1243, X40_1246) | ~c6_2(X141_1243, a147) | c4_2(X141_1243, a147) | c1_1(X141_1243) | c5_2(X141_1243, X40_1246) | ~c1_2(X141_1243, X40_1246) | c8_1(X141_1243) | ~c5_1(X141_1243) | ~c3_2(X141_1243, a264) | ~ndr1_1(X141_1243) | ~c5_2(X141_1243, a263) | ~c6_1(X141_1243)))). % 33.45/17.87 tff(c_12230, plain, (![X3_841, X4_843, V_4, V_842]: (c4_2(X3_841, X4_843) | c4_2(X3_841, V_4) | c3_2(X3_841, V_4) | c4_2(X3_841, a264) | ~c1_2(X3_841, a264) | ~c6_1(X3_841) | c1_1(X3_841) | c5_2(X3_841, a263) | ~c1_2(X3_841, a263) | c8_1(X3_841) | ~c5_2(X3_841, a152) | c4_2(X3_841, V_842) | c3_2(X3_841, V_842) | c7_1(X3_841) | c4_2(X3_841, a152) | ~c1_2(X3_841, a152) | ~c6_2(X3_841, a147) | c4_2(X3_841, a147) | ~c5_1(X3_841) | ~c5_2(X3_841, X4_843) | ~c3_2(X3_841, X4_843) | ~ndr1_1(X3_841)))). % 33.45/17.87 tff(c_13130, plain, (![V_894, X40_895, X4_896, X3_893, X40_340, V_4]: (c4_2(X3_893, X4_896) | c4_2(X3_893, V_4) | c3_2(X3_893, V_4) | c4_2(X3_893, X40_340) | c5_2(X3_893, X40_340) | ~c1_2(X3_893, X40_340) | c4_2(X3_893, a152) | ~c5_2(X3_893, a152) | c4_2(X3_893, V_894) | c3_2(X3_893, V_894) | c7_1(X3_893) | c4_2(X3_893, X40_895) | ~c6_2(X3_893, a147) | c4_2(X3_893, a147) | c1_1(X3_893) | c5_2(X3_893, X40_895) | ~c1_2(X3_893, X40_895) | c8_1(X3_893) | ~c5_1(X3_893) | ~c5_2(X3_893, X4_896) | ~c3_2(X3_893, X4_896) | ~ndr1_1(X3_893)))). % 33.45/17.87 tff(c_13634, plain, (![X39_937, V_4, V_938, X40_939]: (c4_2(X39_937, a152) | ~c5_2(X39_937, a152) | c4_2(X39_937, V_4) | c3_2(X39_937, V_4) | ~c1_2(X39_937, a264) | c4_2(X39_937, a264) | c4_2(X39_937, V_938) | c3_2(X39_937, V_938) | c7_1(X39_937) | c4_2(X39_937, X40_939) | ~c6_2(X39_937, a147) | c4_2(X39_937, a147) | c5_2(X39_937, X40_939) | ~c1_2(X39_937, X40_939) | ~c5_1(X39_937) | ~c3_2(X39_937, a264) | ~c6_1(X39_937) | c1_1(X39_937) | c5_2(X39_937, a263) | ~c1_2(X39_937, a263) | ~ndr1_1(X39_937) | c8_1(X39_937)))). % 33.45/17.87 tff(c_15358, plain, (![X141_1235, X77_1236, V_1237, X40_1238]: (c4_1(X141_1235) | c1_2(X141_1235, X77_1236) | c2_2(X141_1235, X77_1236) | c4_2(X141_1235, a152) | ~c1_2(X141_1235, a152) | ~c6_2(X141_1235, X77_1236) | c4_2(X141_1235, X77_1236) | c4_2(X141_1235, a264) | c4_2(X141_1235, V_1237) | c3_2(X141_1235, V_1237) | c7_1(X141_1235) | c4_2(X141_1235, X40_1238) | ~c6_2(X141_1235, a147) | c4_2(X141_1235, a147) | c1_1(X141_1235) | c5_2(X141_1235, X40_1238) | ~c1_2(X141_1235, X40_1238) | c8_1(X141_1235) | ~c5_1(X141_1235) | ~c3_2(X141_1235, a264) | ~ndr1_1(X141_1235) | c4_2(X141_1235, a263) | ~c6_1(X141_1235)))). % 33.45/17.87 tff(c_13643, plain, (![X39_937, X77_112, V_938, X40_939]: (c4_2(X39_937, a152) | ~c1_2(X39_937, a152) | ~c6_2(X39_937, X77_112) | c4_2(X39_937, X77_112) | c7_2(X39_937, X77_112) | c4_2(X39_937, a264) | c4_2(X39_937, V_938) | c3_2(X39_937, V_938) | c7_1(X39_937) | c4_2(X39_937, X40_939) | ~c6_2(X39_937, a147) | c4_2(X39_937, a147) | c5_2(X39_937, X40_939) | ~c1_2(X39_937, X40_939) | ~c5_1(X39_937) | ~c3_2(X39_937, a264) | ~c6_1(X39_937) | c1_1(X39_937) | c5_2(X39_937, a263) | ~c1_2(X39_937, a263) | ~ndr1_1(X39_937) | c8_1(X39_937)))). % 33.45/17.87 tff(c_13813, plain, (![X39_585, X40_962, V_961, X40_586, X77_587]: (~c5_2(X39_585, X77_587) | c4_2(X39_585, V_961) | c3_2(X39_585, V_961) | ~c3_2(X39_585, X40_962) | c4_2(X39_585, X40_962) | ~c6_2(X39_585, a147) | c4_2(X39_585, a147) | ~c1_2(X39_585, X40_962) | c4_1(X39_585) | c1_2(X39_585, a152) | c2_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585)))). % 33.45/17.87 tff(c_13829, plain, (![X77_306, X40_962, V_961, X39_58, X40_60]: (~c5_2(X39_58, X77_306) | c4_2(X39_58, V_961) | c3_2(X39_58, V_961) | c4_1(X39_58) | c1_2(X39_58, a152) | c2_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_962) | c4_2(X39_58, X40_962) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_962) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.87 tff(c_13139, plain, (![V_894, X40_895, X4_896, X3_893, X77_112]: (c4_2(X3_893, X4_896) | ~c1_2(X3_893, X4_896) | ~c6_2(X3_893, X77_112) | c4_2(X3_893, X77_112) | c7_2(X3_893, X77_112) | c4_2(X3_893, a152) | ~c5_2(X3_893, a152) | c4_2(X3_893, V_894) | c3_2(X3_893, V_894) | c7_1(X3_893) | c4_2(X3_893, X40_895) | ~c6_2(X3_893, a147) | c4_2(X3_893, a147) | c1_1(X3_893) | c5_2(X3_893, X40_895) | ~c1_2(X3_893, X40_895) | c8_1(X3_893) | ~c5_1(X3_893) | ~c5_2(X3_893, X4_896) | ~c3_2(X3_893, X4_896) | ~ndr1_1(X3_893)))). % 33.45/17.87 tff(c_12638, plain, (![X141_858, V_4, V_859, X40_860]: (c4_2(X141_858, a152) | ~c5_2(X141_858, a152) | c4_2(X141_858, V_4) | c3_2(X141_858, V_4) | ~c1_2(X141_858, a264) | c4_2(X141_858, a264) | c4_2(X141_858, V_859) | c3_2(X141_858, V_859) | c7_1(X141_858) | c4_2(X141_858, X40_860) | ~c6_2(X141_858, a147) | c4_2(X141_858, a147) | c1_1(X141_858) | c5_2(X141_858, X40_860) | ~c1_2(X141_858, X40_860) | c8_1(X141_858) | ~c5_1(X141_858) | ~c3_2(X141_858, a264) | ~ndr1_1(X141_858) | c4_2(X141_858, a263) | ~c6_1(X141_858)))). % 33.45/17.87 tff(c_12460, plain, (![X141_855, V_4, V_856, X40_857]: (c4_2(X141_855, a152) | ~c5_2(X141_855, a152) | c4_2(X141_855, V_4) | c3_2(X141_855, V_4) | ~c1_2(X141_855, a264) | c4_2(X141_855, a264) | c4_2(X141_855, V_856) | c3_2(X141_855, V_856) | c7_1(X141_855) | c4_2(X141_855, X40_857) | ~c6_2(X141_855, a147) | c4_2(X141_855, a147) | c1_1(X141_855) | c5_2(X141_855, X40_857) | ~c1_2(X141_855, X40_857) | c8_1(X141_855) | ~c5_1(X141_855) | ~c3_2(X141_855, a264) | ~ndr1_1(X141_855) | ~c5_2(X141_855, a263) | ~c6_1(X141_855)))). % 33.45/17.87 tff(c_12465, plain, (![X141_855, X77_112, V_856, X40_857]: (c4_2(X141_855, a152) | ~c1_2(X141_855, a152) | ~c6_2(X141_855, X77_112) | c4_2(X141_855, X77_112) | c7_2(X141_855, X77_112) | c4_2(X141_855, a264) | c4_2(X141_855, V_856) | c3_2(X141_855, V_856) | c7_1(X141_855) | c4_2(X141_855, X40_857) | ~c6_2(X141_855, a147) | c4_2(X141_855, a147) | c1_1(X141_855) | c5_2(X141_855, X40_857) | ~c1_2(X141_855, X40_857) | c8_1(X141_855) | ~c5_1(X141_855) | ~c3_2(X141_855, a264) | ~ndr1_1(X141_855) | ~c5_2(X141_855, a263) | ~c6_1(X141_855)))). % 33.45/17.87 tff(c_14587, plain, (![X3_1057, X4_1059, V_4, V_1058]: (c4_2(X3_1057, X4_1059) | c4_2(X3_1057, V_4) | c3_2(X3_1057, V_4) | c4_2(X3_1057, a152) | ~c5_2(X3_1057, a152) | c4_2(X3_1057, V_1058) | c3_2(X3_1057, V_1058) | c7_1(X3_1057) | c4_2(X3_1057, a264) | ~c1_2(X3_1057, a264) | ~c6_2(X3_1057, a147) | c4_2(X3_1057, a147) | ~c6_1(X3_1057) | c1_1(X3_1057) | c5_2(X3_1057, a263) | ~c1_2(X3_1057, a263) | c8_1(X3_1057) | ~c5_1(X3_1057) | ~c5_2(X3_1057, X4_1059) | ~c3_2(X3_1057, X4_1059) | ~ndr1_1(X3_1057)))). % 33.45/17.87 tff(c_12644, plain, (![X141_858, X77_112, V_859, X40_860]: (c4_2(X141_858, a152) | ~c1_2(X141_858, a152) | ~c6_2(X141_858, X77_112) | c4_2(X141_858, X77_112) | c7_2(X141_858, X77_112) | c4_2(X141_858, a264) | c4_2(X141_858, V_859) | c3_2(X141_858, V_859) | c7_1(X141_858) | c4_2(X141_858, X40_860) | ~c6_2(X141_858, a147) | c4_2(X141_858, a147) | c1_1(X141_858) | c5_2(X141_858, X40_860) | ~c1_2(X141_858, X40_860) | c8_1(X141_858) | ~c5_1(X141_858) | ~c3_2(X141_858, a264) | ~ndr1_1(X141_858) | c4_2(X141_858, a263) | ~c6_1(X141_858)))). % 33.45/17.87 tff(c_14688, plain, (![X39_1067, V_1068, X40_1069]: (c4_1(X39_1067) | c1_2(X39_1067, a152) | c2_2(X39_1067, a152) | c4_2(X39_1067, a264) | c4_2(X39_1067, V_1068) | c3_2(X39_1067, V_1068) | ~c3_2(X39_1067, a152) | ~c3_2(X39_1067, X40_1069) | c7_1(X39_1067) | c4_2(X39_1067, X40_1069) | ~c6_2(X39_1067, a147) | c4_2(X39_1067, a147) | ~c1_2(X39_1067, X40_1069) | ~c5_1(X39_1067) | ~c3_2(X39_1067, a264) | ~c6_1(X39_1067) | c1_1(X39_1067) | c5_2(X39_1067, a263) | ~c1_2(X39_1067, a263) | ~ndr1_1(X39_1067) | c8_1(X39_1067)))). % 33.45/17.87 tff(c_14595, plain, (![X3_1057, X4_1059, V_1058]: (c4_1(X3_1057) | c1_2(X3_1057, X4_1059) | c2_2(X3_1057, X4_1059) | c4_2(X3_1057, a152) | ~c5_2(X3_1057, a152) | c4_2(X3_1057, V_1058) | c3_2(X3_1057, V_1058) | c7_1(X3_1057) | c4_2(X3_1057, a264) | ~c1_2(X3_1057, a264) | ~c6_2(X3_1057, a147) | c4_2(X3_1057, a147) | ~c6_1(X3_1057) | c1_1(X3_1057) | c5_2(X3_1057, a263) | ~c1_2(X3_1057, a263) | c8_1(X3_1057) | ~c5_1(X3_1057) | ~c5_2(X3_1057, X4_1059) | ~c3_2(X3_1057, X4_1059) | ~ndr1_1(X3_1057)))). % 33.45/17.87 tff(c_14463, plain, (![X39_1054, X4_1056, V_1055]: (c4_1(X39_1054) | c1_2(X39_1054, X4_1056) | c2_2(X39_1054, X4_1056) | c4_2(X39_1054, a264) | ~c5_2(X39_1054, a264) | c4_2(X39_1054, V_1055) | c3_2(X39_1054, V_1055) | c7_1(X39_1054) | c4_2(X39_1054, a152) | ~c1_2(X39_1054, a152) | ~c6_2(X39_1054, a147) | c4_2(X39_1054, a147) | ~c5_1(X39_1054) | ~c5_2(X39_1054, X4_1056) | ~c3_2(X39_1054, X4_1056) | ~c6_1(X39_1054) | c1_1(X39_1054) | c5_2(X39_1054, a263) | ~c1_2(X39_1054, a263) | ~ndr1_1(X39_1054) | c8_1(X39_1054)))). % 33.45/17.87 tff(c_11786, plain, (![X141_821, X4_823, X77_112, V_822]: (c4_2(X141_821, X4_823) | ~c1_2(X141_821, X4_823) | ~c6_2(X141_821, X77_112) | c4_2(X141_821, X77_112) | c7_2(X141_821, X77_112) | c4_2(X141_821, a264) | ~c5_2(X141_821, a264) | c4_2(X141_821, V_822) | c3_2(X141_821, V_822) | c7_1(X141_821) | c4_2(X141_821, a152) | ~c1_2(X141_821, a152) | ~c6_2(X141_821, a147) | c4_2(X141_821, a147) | ~c5_1(X141_821) | ~c5_2(X141_821, X4_823) | ~c3_2(X141_821, X4_823) | ~ndr1_1(X141_821) | ~c5_2(X141_821, a263) | ~c6_1(X141_821)))). % 33.45/17.87 tff(c_11897, plain, (![X141_824, X4_826, X77_112, V_825]: (c4_2(X141_824, X4_826) | ~c1_2(X141_824, X4_826) | ~c6_2(X141_824, X77_112) | c4_2(X141_824, X77_112) | c7_2(X141_824, X77_112) | c4_2(X141_824, a264) | ~c5_2(X141_824, a264) | c4_2(X141_824, V_825) | c3_2(X141_824, V_825) | c7_1(X141_824) | c4_2(X141_824, a152) | ~c1_2(X141_824, a152) | ~c6_2(X141_824, a147) | c4_2(X141_824, a147) | ~c5_1(X141_824) | ~c5_2(X141_824, X4_826) | ~c3_2(X141_824, X4_826) | ~ndr1_1(X141_824) | c4_2(X141_824, a263) | ~c6_1(X141_824)))). % 33.45/17.87 tff(c_13290, plain, (![X3_12, V_909, V_703, X40_910, X4_704]: (c4_2(X3_12, X4_704) | c4_2(X3_12, V_909) | c3_2(X3_12, V_909) | ~c3_2(X3_12, X40_910) | c4_2(X3_12, X40_910) | c1_1(X3_12) | ~c1_2(X3_12, X40_910) | c8_1(X3_12) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_703) | c3_2(X3_12, V_703) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_704) | ~c3_2(X3_12, X4_704) | ~ndr1_1(X3_12)))). % 33.45/17.87 tff(c_13318, plain, (![V_909, X77_306, X40_910, X39_58, X40_60]: (~c5_2(X39_58, X77_306) | c4_2(X39_58, V_909) | c3_2(X39_58, V_909) | c4_2(X39_58, a152) | ~c1_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_910) | c4_2(X39_58, X40_910) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_910) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.87 tff(c_13297, plain, (![X39_585, V_909, X40_910, X40_586, X77_112]: (~c5_2(X39_585, X77_112) | c4_2(X39_585, V_909) | c3_2(X39_585, V_909) | ~c3_2(X39_585, X40_910) | c4_2(X39_585, X40_910) | ~c6_2(X39_585, a147) | c4_2(X39_585, a147) | ~c1_2(X39_585, X40_910) | c4_2(X39_585, a152) | ~c1_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_112) | c4_2(X39_585, X77_112) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585)))). % 33.45/17.88 tff(c_10856, plain, (![X39_761, X4_431, X40_762, V_4, X77_763]: (~c5_2(X39_761, X77_763) | c4_2(X39_761, V_4) | c3_2(X39_761, V_4) | ~c6_2(X39_761, a147) | c4_2(X39_761, a147) | ~c5_2(X39_761, X4_431) | c7_2(X39_761, X4_431) | ~c3_2(X39_761, X4_431) | c4_2(X39_761, a152) | ~c1_2(X39_761, a152) | ~c5_1(X39_761) | ~c3_2(X39_761, X40_762) | c7_1(X39_761) | c4_2(X39_761, X40_762) | ~c6_2(X39_761, X77_763) | c4_2(X39_761, X77_763) | c1_1(X39_761) | ~c1_2(X39_761, X40_762) | ~ndr1_1(X39_761) | c8_1(X39_761)))). % 33.45/17.88 tff(c_11324, plain, (![V_787, X39_58, X77_439, X40_788, X40_60]: (~c5_2(X39_58, X77_439) | c4_2(X39_58, V_787) | c3_2(X39_58, V_787) | ~c3_2(X39_58, a152) | ~c3_2(X39_58, X40_788) | c4_2(X39_58, X40_788) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_788) | c7_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_439) | c4_2(X39_58, X77_439) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_12233, plain, (![X4_843, X3_841, X40_340, V_842, V_4]: (c4_2(X3_841, X4_843) | c4_2(X3_841, V_4) | c3_2(X3_841, V_4) | c4_2(X3_841, X40_340) | c1_1(X3_841) | c5_2(X3_841, X40_340) | ~c1_2(X3_841, X40_340) | c8_1(X3_841) | ~c5_2(X3_841, a152) | c4_2(X3_841, V_842) | c3_2(X3_841, V_842) | c7_1(X3_841) | c4_2(X3_841, a152) | ~c1_2(X3_841, a152) | ~c6_2(X3_841, a147) | c4_2(X3_841, a147) | ~c5_1(X3_841) | ~c5_2(X3_841, X4_843) | ~c3_2(X3_841, X4_843) | ~ndr1_1(X3_841)))). % 33.45/17.88 tff(c_14215, plain, (![X39_243, V_1020, X40_1021]: (c4_2(X39_243, a264) | c4_2(X39_243, V_1020) | c3_2(X39_243, V_1020) | c4_2(X39_243, a152) | ~c1_2(X39_243, a152) | ~c3_2(X39_243, X40_1021) | c7_1(X39_243) | c4_2(X39_243, X40_1021) | ~c6_2(X39_243, a147) | c4_2(X39_243, a147) | ~c1_2(X39_243, X40_1021) | c7_2(X39_243, a152) | ~c5_1(X39_243) | ~c3_2(X39_243, a264) | ~c6_1(X39_243) | c1_1(X39_243) | c5_2(X39_243, a263) | ~c1_2(X39_243, a263) | ~ndr1_1(X39_243) | c8_1(X39_243)))). % 33.45/17.88 tff(c_11228, plain, (![V_779, X77_781, X44_66, X39_778, X40_780]: (~c5_2(X39_778, X77_781) | c6_1(X39_778) | ~c8_2(X39_778, X44_66) | ~c6_2(X39_778, X44_66) | c5_2(X39_778, X44_66) | ~c3_2(X39_778, a147) | c4_2(X39_778, a152) | ~c5_2(X39_778, a152) | c4_2(X39_778, V_779) | c3_2(X39_778, V_779) | ~c5_1(X39_778) | ~c3_2(X39_778, X40_780) | c7_1(X39_778) | c4_2(X39_778, X40_780) | ~c6_2(X39_778, X77_781) | c4_2(X39_778, X77_781) | c1_1(X39_778) | ~c1_2(X39_778, X40_780) | ~ndr1_1(X39_778) | c8_1(X39_778)))). % 33.45/17.88 tff(c_11109, plain, (![V_775, X40_776, X77_777, X39_774, X44_66]: (~c5_2(X39_774, X77_777) | c6_1(X39_774) | ~c8_2(X39_774, X44_66) | ~c6_2(X39_774, X44_66) | c5_2(X39_774, X44_66) | c5_2(X39_774, a147) | c4_2(X39_774, a152) | ~c5_2(X39_774, a152) | c4_2(X39_774, V_775) | c3_2(X39_774, V_775) | ~c5_1(X39_774) | ~c3_2(X39_774, X40_776) | c7_1(X39_774) | c4_2(X39_774, X40_776) | ~c6_2(X39_774, X77_777) | c4_2(X39_774, X77_777) | c1_1(X39_774) | ~c1_2(X39_774, X40_776) | ~ndr1_1(X39_774) | c8_1(X39_774)))). % 33.45/17.88 tff(c_13145, plain, (![V_894, X40_895, X4_896, X3_893, X44_66]: (c6_1(X3_893) | ~c8_2(X3_893, X44_66) | ~c6_2(X3_893, X44_66) | c5_2(X3_893, X44_66) | c4_2(X3_893, a152) | ~c5_2(X3_893, a152) | c4_2(X3_893, V_894) | c3_2(X3_893, V_894) | c7_1(X3_893) | c4_2(X3_893, X40_895) | ~c6_2(X3_893, a147) | c4_2(X3_893, a147) | c1_1(X3_893) | c5_2(X3_893, X40_895) | ~c1_2(X3_893, X40_895) | c8_1(X3_893) | ~c5_1(X3_893) | ~c5_2(X3_893, X4_896) | ~c3_2(X3_893, X4_896) | ~ndr1_1(X3_893)))). % 33.45/17.88 tff(c_14351, plain, (![X39_58, V_1052, X40_1053]: (c4_2(X39_58, a264) | ~c5_2(X39_58, a264) | c4_2(X39_58, V_1052) | c3_2(X39_58, V_1052) | c4_1(X39_58) | c1_2(X39_58, a152) | c2_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_1053) | c7_1(X39_58) | c4_2(X39_58, X40_1053) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_1053) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_14038, plain, (![X141_980, V_981, X40_982]: (c4_1(X141_980) | c1_2(X141_980, a152) | c2_2(X141_980, a152) | c4_2(X141_980, a264) | c4_2(X141_980, V_981) | c3_2(X141_980, V_981) | ~c3_2(X141_980, a152) | ~c3_2(X141_980, X40_982) | c7_1(X141_980) | c4_2(X141_980, X40_982) | ~c6_2(X141_980, a147) | c4_2(X141_980, a147) | c1_1(X141_980) | ~c1_2(X141_980, X40_982) | c8_1(X141_980) | ~c5_1(X141_980) | ~c3_2(X141_980, a264) | ~ndr1_1(X141_980) | ~c5_2(X141_980, a263) | ~c6_1(X141_980)))). % 33.45/17.88 tff(c_13964, plain, (![X141_977, V_978, X40_979]: (c4_1(X141_977) | c1_2(X141_977, a152) | c2_2(X141_977, a152) | c4_2(X141_977, a264) | c4_2(X141_977, V_978) | c3_2(X141_977, V_978) | ~c3_2(X141_977, a152) | ~c3_2(X141_977, X40_979) | c7_1(X141_977) | c4_2(X141_977, X40_979) | ~c6_2(X141_977, a147) | c4_2(X141_977, a147) | c1_1(X141_977) | ~c1_2(X141_977, X40_979) | c8_1(X141_977) | ~c5_1(X141_977) | ~c3_2(X141_977, a264) | ~ndr1_1(X141_977) | c4_2(X141_977, a263) | ~c6_1(X141_977)))). % 33.45/17.88 tff(c_13640, plain, (![X39_937, V_938, X40_939]: (c4_1(X39_937) | c1_2(X39_937, a152) | c2_2(X39_937, a152) | c4_2(X39_937, a264) | c4_2(X39_937, V_938) | c3_2(X39_937, V_938) | c7_1(X39_937) | c4_2(X39_937, X40_939) | ~c6_2(X39_937, a147) | c4_2(X39_937, a147) | c5_2(X39_937, X40_939) | ~c1_2(X39_937, X40_939) | ~c5_1(X39_937) | ~c3_2(X39_937, a264) | ~c6_1(X39_937) | c1_1(X39_937) | c5_2(X39_937, a263) | ~c1_2(X39_937, a263) | ~ndr1_1(X39_937) | c8_1(X39_937)))). % 33.45/17.88 tff(c_12235, plain, (![X3_841, X4_843, V_4, V_842]: (c4_2(X3_841, X4_843) | c4_2(X3_841, V_4) | c3_2(X3_841, V_4) | c4_2(X3_841, a264) | ~c1_2(X3_841, a264) | ~c5_2(X3_841, a263) | ~c6_1(X3_841) | ~c5_2(X3_841, a152) | c4_2(X3_841, V_842) | c3_2(X3_841, V_842) | c7_1(X3_841) | c4_2(X3_841, a152) | ~c1_2(X3_841, a152) | ~c6_2(X3_841, a147) | c4_2(X3_841, a147) | ~c5_1(X3_841) | ~c5_2(X3_841, X4_843) | ~c3_2(X3_841, X4_843) | ~ndr1_1(X3_841)))). % 33.45/17.88 tff(c_12234, plain, (![X3_841, X4_843, V_4, V_842]: (c4_2(X3_841, X4_843) | c4_2(X3_841, V_4) | c3_2(X3_841, V_4) | c4_2(X3_841, a264) | ~c1_2(X3_841, a264) | c4_2(X3_841, a263) | ~c6_1(X3_841) | ~c5_2(X3_841, a152) | c4_2(X3_841, V_842) | c3_2(X3_841, V_842) | c7_1(X3_841) | c4_2(X3_841, a152) | ~c1_2(X3_841, a152) | ~c6_2(X3_841, a147) | c4_2(X3_841, a147) | ~c5_1(X3_841) | ~c5_2(X3_841, X4_843) | ~c3_2(X3_841, X4_843) | ~ndr1_1(X3_841)))). % 33.45/17.88 tff(c_10132, plain, (![V_703, X77_306, X4_704, X39_58, X40_60]: (~c5_2(X39_58, X77_306) | c4_2(X39_58, V_703) | c3_2(X39_58, V_703) | c4_2(X39_58, a152) | ~c1_2(X39_58, a152) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c5_1(X39_58) | ~c5_2(X39_58, X4_704) | c7_2(X39_58, X4_704) | ~c3_2(X39_58, X4_704) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_10466, plain, (![X3_12, X4_14, V_752]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_752) | c3_2(X3_12, V_752) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c6_1(X3_12) | c1_1(X3_12) | c5_2(X3_12, a263) | ~c1_2(X3_12, a263) | c8_1(X3_12) | c4_1(X3_12) | c1_2(X3_12, a152) | c2_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.88 tff(c_13303, plain, (![X39_58, V_909, X40_910, X40_60]: (~c5_2(X39_58, a152) | c4_2(X39_58, V_909) | c3_2(X39_58, V_909) | ~c1_2(X39_58, a152) | ~c3_2(X39_58, X40_910) | c4_2(X39_58, X40_910) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_910) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, a152) | c4_2(X39_58, a152) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_10983, plain, (![X77_306, V_772, X39_58, X40_773, X40_60]: (~c5_2(X39_58, X77_306) | c4_2(X39_58, V_772) | c3_2(X39_58, V_772) | ~c4_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_773) | c4_2(X39_58, X40_773) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_773) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_11337, plain, (![V_787, X77_306, X39_58, X40_788, X40_60]: (~c5_2(X39_58, X77_306) | c4_2(X39_58, V_787) | c3_2(X39_58, V_787) | ~c3_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_788) | c4_2(X39_58, X40_788) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_788) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_11320, plain, (![V_787, X77_436, X39_58, X40_788, X40_60]: (~c5_2(X39_58, X77_436) | c4_2(X39_58, V_787) | c3_2(X39_58, V_787) | ~c3_2(X39_58, X40_788) | c4_2(X39_58, X40_788) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_788) | ~c3_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_436) | c4_2(X39_58, X77_436) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_11322, plain, (![X39_58, V_787, X40_788, X40_60]: (~c5_2(X39_58, a152) | c4_2(X39_58, V_787) | c3_2(X39_58, V_787) | ~c3_2(X39_58, a152) | ~c3_2(X39_58, X40_788) | c4_2(X39_58, X40_788) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_788) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, a152) | c4_2(X39_58, a152) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_10965, plain, (![X77_428, V_772, X39_58, X40_773, X40_60]: (~c5_2(X39_58, X77_428) | c4_2(X39_58, V_772) | c3_2(X39_58, V_772) | ~c3_2(X39_58, X40_773) | c4_2(X39_58, X40_773) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_773) | ~c4_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_428) | c4_2(X39_58, X77_428) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_11103, plain, (![V_775, X40_776, X77_777, X39_774, X77_112]: (~c1_2(X39_774, X77_777) | ~c6_2(X39_774, X77_112) | c4_2(X39_774, X77_112) | c7_2(X39_774, X77_112) | c5_2(X39_774, a147) | c4_2(X39_774, a152) | ~c5_2(X39_774, a152) | c4_2(X39_774, V_775) | c3_2(X39_774, V_775) | ~c5_1(X39_774) | ~c3_2(X39_774, X40_776) | c7_1(X39_774) | c4_2(X39_774, X40_776) | ~c6_2(X39_774, X77_777) | c4_2(X39_774, X77_777) | c1_1(X39_774) | ~c1_2(X39_774, X40_776) | ~ndr1_1(X39_774) | c8_1(X39_774)))). % 33.45/17.88 tff(c_8881, plain, (![X39_585, X40_586, X40_340, X77_587, V_4]: (~c5_2(X39_585, X77_587) | c4_2(X39_585, V_4) | c3_2(X39_585, V_4) | c4_2(X39_585, X40_340) | ~c6_2(X39_585, a147) | c4_2(X39_585, a147) | c5_2(X39_585, X40_340) | ~c1_2(X39_585, X40_340) | c7_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585)))). % 33.45/17.88 tff(c_11222, plain, (![V_779, X77_781, X39_778, X77_112, X40_780]: (~c1_2(X39_778, X77_781) | ~c6_2(X39_778, X77_112) | c4_2(X39_778, X77_112) | c7_2(X39_778, X77_112) | ~c3_2(X39_778, a147) | c4_2(X39_778, a152) | ~c5_2(X39_778, a152) | c4_2(X39_778, V_779) | c3_2(X39_778, V_779) | ~c5_1(X39_778) | ~c3_2(X39_778, X40_780) | c7_1(X39_778) | c4_2(X39_778, X40_780) | ~c6_2(X39_778, X77_781) | c4_2(X39_778, X77_781) | c1_1(X39_778) | ~c1_2(X39_778, X40_780) | ~ndr1_1(X39_778) | c8_1(X39_778)))). % 33.45/17.88 tff(c_14221, plain, (![X141_191, V_1020, X40_1021]: (c4_2(X141_191, a264) | c4_2(X141_191, V_1020) | c3_2(X141_191, V_1020) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c3_2(X141_191, X40_1021) | c7_1(X141_191) | c4_2(X141_191, X40_1021) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_1021) | c8_1(X141_191) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.88 tff(c_14220, plain, (![X141_191, V_1020, X40_1021]: (c4_2(X141_191, a264) | c4_2(X141_191, V_1020) | c3_2(X141_191, V_1020) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c3_2(X141_191, X40_1021) | c7_1(X141_191) | c4_2(X141_191, X40_1021) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_1021) | c8_1(X141_191) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.88 tff(c_14158, plain, (![X39_58, V_984, X40_985]: (c4_2(X39_58, a264) | ~c5_2(X39_58, a264) | c4_2(X39_58, V_984) | c3_2(X39_58, V_984) | c4_2(X39_58, a152) | ~c1_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_985) | c7_1(X39_58) | c4_2(X39_58, X40_985) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_985) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_13190, plain, (![X39_243, V_905, X40_906]: (c4_2(X39_243, a264) | c4_2(X39_243, V_905) | c3_2(X39_243, V_905) | ~c3_2(X39_243, a152) | ~c3_2(X39_243, X40_906) | c7_1(X39_243) | c4_2(X39_243, X40_906) | ~c6_2(X39_243, a147) | c4_2(X39_243, a147) | ~c1_2(X39_243, X40_906) | c7_2(X39_243, a152) | ~c5_1(X39_243) | ~c3_2(X39_243, a264) | ~c6_1(X39_243) | c1_1(X39_243) | c5_2(X39_243, a263) | ~c1_2(X39_243, a263) | ~ndr1_1(X39_243) | c8_1(X39_243)))). % 33.45/17.88 tff(c_13444, plain, (![X39_930, V_4, V_931]: (c4_2(X39_930, a152) | ~c5_2(X39_930, a152) | c4_2(X39_930, V_4) | c3_2(X39_930, V_4) | c4_2(X39_930, V_931) | c3_2(X39_930, V_931) | c7_1(X39_930) | c4_2(X39_930, a264) | ~c1_2(X39_930, a264) | ~c6_2(X39_930, a147) | c4_2(X39_930, a147) | ~c5_1(X39_930) | ~c3_2(X39_930, a264) | ~c6_1(X39_930) | c1_1(X39_930) | c5_2(X39_930, a263) | ~c1_2(X39_930, a263) | ~ndr1_1(X39_930) | c8_1(X39_930)))). % 33.45/17.88 tff(c_13135, plain, (![X3_893, X4_896, V_894, X40_895]: (c4_1(X3_893) | c1_2(X3_893, X4_896) | c2_2(X3_893, X4_896) | c4_2(X3_893, a152) | ~c5_2(X3_893, a152) | c4_2(X3_893, V_894) | c3_2(X3_893, V_894) | c7_1(X3_893) | c4_2(X3_893, X40_895) | ~c6_2(X3_893, a147) | c4_2(X3_893, a147) | c1_1(X3_893) | c5_2(X3_893, X40_895) | ~c1_2(X3_893, X40_895) | c8_1(X3_893) | ~c5_1(X3_893) | ~c5_2(X3_893, X4_896) | ~c3_2(X3_893, X4_896) | ~ndr1_1(X3_893)))). % 33.45/17.88 tff(c_10478, plain, (![X3_12, V_752, X4_14]: (c4_2(X3_12, a152) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_752) | c3_2(X3_12, V_752) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c6_1(X3_12) | c1_1(X3_12) | c5_2(X3_12, a263) | ~c1_2(X3_12, a263) | c8_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.88 tff(c_11692, plain, (![X39_58, V_819, X4_820]: (c4_2(X39_58, a264) | ~c5_2(X39_58, a264) | c4_2(X39_58, V_819) | c3_2(X39_58, V_819) | c7_1(X39_58) | c4_2(X39_58, a152) | ~c1_2(X39_58, a152) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c5_1(X39_58) | ~c5_2(X39_58, X4_820) | c7_2(X39_58, X4_820) | ~c3_2(X39_58, X4_820) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.88 tff(c_13841, plain, (![X141_191, V_961, X40_962]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_961) | c3_2(X141_191, V_961) | c4_1(X141_191) | c1_2(X141_191, a152) | c2_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_962) | c7_1(X141_191) | c4_2(X141_191, X40_962) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_962) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.88 tff(c_13839, plain, (![X141_191, V_961, X40_962]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_961) | c3_2(X141_191, V_961) | c4_1(X141_191) | c1_2(X141_191, a152) | c2_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_962) | c7_1(X141_191) | c4_2(X141_191, X40_962) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_962) | ~ndr1_1(X141_191) | c8_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.88 tff(c_13840, plain, (![X141_191, V_961, X40_962]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_961) | c3_2(X141_191, V_961) | c4_1(X141_191) | c1_2(X141_191, a152) | c2_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_962) | c7_1(X141_191) | c4_2(X141_191, X40_962) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_962) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.88 tff(c_12641, plain, (![X141_858, V_859, X40_860]: (c4_1(X141_858) | c1_2(X141_858, a152) | c2_2(X141_858, a152) | c4_2(X141_858, a264) | c4_2(X141_858, V_859) | c3_2(X141_858, V_859) | c7_1(X141_858) | c4_2(X141_858, X40_860) | ~c6_2(X141_858, a147) | c4_2(X141_858, a147) | c1_1(X141_858) | c5_2(X141_858, X40_860) | ~c1_2(X141_858, X40_860) | c8_1(X141_858) | ~c5_1(X141_858) | ~c3_2(X141_858, a264) | ~ndr1_1(X141_858) | c4_2(X141_858, a263) | ~c6_1(X141_858)))). % 33.45/17.88 tff(c_12462, plain, (![X141_855, V_856, X40_857]: (c4_1(X141_855) | c1_2(X141_855, a152) | c2_2(X141_855, a152) | c4_2(X141_855, a264) | c4_2(X141_855, V_856) | c3_2(X141_855, V_856) | c7_1(X141_855) | c4_2(X141_855, X40_857) | ~c6_2(X141_855, a147) | c4_2(X141_855, a147) | c1_1(X141_855) | c5_2(X141_855, X40_857) | ~c1_2(X141_855, X40_857) | c8_1(X141_855) | ~c5_1(X141_855) | ~c3_2(X141_855, a264) | ~ndr1_1(X141_855) | ~c5_2(X141_855, a263) | ~c6_1(X141_855)))). % 33.45/17.88 tff(c_11568, plain, (![X3_815, X4_817, V_4, V_816]: (c4_2(X3_815, X4_817) | c4_2(X3_815, V_4) | c3_2(X3_815, V_4) | c4_2(X3_815, a152) | ~c5_2(X3_815, a152) | c4_2(X3_815, V_816) | c3_2(X3_815, V_816) | c7_1(X3_815) | c4_2(X3_815, a264) | ~c1_2(X3_815, a264) | ~c6_2(X3_815, a147) | c4_2(X3_815, a147) | ~c5_2(X3_815, a263) | ~c6_1(X3_815) | ~c5_1(X3_815) | ~c5_2(X3_815, X4_817) | ~c3_2(X3_815, X4_817) | ~ndr1_1(X3_815)))). % 33.45/17.88 tff(c_11461, plain, (![X3_812, X4_814, V_4, V_813]: (c4_2(X3_812, X4_814) | c4_2(X3_812, V_4) | c3_2(X3_812, V_4) | c4_2(X3_812, a152) | ~c5_2(X3_812, a152) | c4_2(X3_812, V_813) | c3_2(X3_812, V_813) | c7_1(X3_812) | c4_2(X3_812, a264) | ~c1_2(X3_812, a264) | ~c6_2(X3_812, a147) | c4_2(X3_812, a147) | c4_2(X3_812, a263) | ~c6_1(X3_812) | ~c5_1(X3_812) | ~c5_2(X3_812, X4_814) | ~c3_2(X3_812, X4_814) | ~ndr1_1(X3_812)))). % 33.45/17.88 tff(c_10123, plain, (![X3_12, V_703, X77_306, X4_704, X4_14]: (~c5_2(X3_12, X77_306) | c4_2(X3_12, V_703) | c3_2(X3_12, V_703) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, X4_704) | c7_2(X3_12, X4_704) | ~c3_2(X3_12, X4_704) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.88 tff(c_13307, plain, (![X3_12, V_909, X40_910, X4_14]: (c4_2(X3_12, V_909) | c3_2(X3_12, V_909) | ~c3_2(X3_12, X40_910) | c4_2(X3_12, X40_910) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | ~c1_2(X3_12, X40_910) | c8_1(X3_12) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X4_14) | c4_2(X3_12, X4_14) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.88 tff(c_13325, plain, (![X3_12, X4_14, V_909, X40_910]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_909) | c3_2(X3_12, V_909) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c3_2(X3_12, X40_910) | c7_1(X3_12) | c4_2(X3_12, X40_910) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | ~c1_2(X3_12, X40_910) | c8_1(X3_12) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.88 tff(c_11227, plain, (![V_779, X77_781, X39_778, X40_780, V_4]: (~c5_2(X39_778, X77_781) | c4_2(X39_778, V_4) | c3_2(X39_778, V_4) | ~c3_2(X39_778, a147) | c4_2(X39_778, a152) | ~c5_2(X39_778, a152) | c4_2(X39_778, V_779) | c3_2(X39_778, V_779) | ~c5_1(X39_778) | ~c3_2(X39_778, X40_780) | c7_1(X39_778) | c4_2(X39_778, X40_780) | ~c6_2(X39_778, X77_781) | c4_2(X39_778, X77_781) | c1_1(X39_778) | ~c1_2(X39_778, X40_780) | ~ndr1_1(X39_778) | c8_1(X39_778)))). % 33.45/17.88 tff(c_11106, plain, (![V_775, X40_776, X77_777, X39_774, V_4]: (~c5_2(X39_774, X77_777) | c4_2(X39_774, V_4) | c3_2(X39_774, V_4) | c5_2(X39_774, a147) | c4_2(X39_774, a152) | ~c5_2(X39_774, a152) | c4_2(X39_774, V_775) | c3_2(X39_774, V_775) | ~c5_1(X39_774) | ~c3_2(X39_774, X40_776) | c7_1(X39_774) | c4_2(X39_774, X40_776) | ~c6_2(X39_774, X77_777) | c4_2(X39_774, X77_777) | c1_1(X39_774) | ~c1_2(X39_774, X40_776) | ~ndr1_1(X39_774) | c8_1(X39_774)))). % 33.45/17.88 tff(c_8936, plain, (![X39_588, V_4, X40_340, X40_589]: (~c5_2(X39_588, a152) | c4_2(X39_588, V_4) | c3_2(X39_588, V_4) | c4_2(X39_588, X40_340) | ~c6_2(X39_588, a147) | c4_2(X39_588, a147) | c5_2(X39_588, X40_340) | ~c1_2(X39_588, X40_340) | ~c5_1(X39_588) | ~c3_2(X39_588, X40_589) | c7_1(X39_588) | c4_2(X39_588, X40_589) | ~c6_2(X39_588, a152) | c4_2(X39_588, a152) | c1_1(X39_588) | ~c1_2(X39_588, X40_589) | ~ndr1_1(X39_588) | c8_1(X39_588)))). % 33.45/17.88 tff(c_11465, plain, (![X3_812, X4_814, V_813]: (c4_1(X3_812) | c1_2(X3_812, X4_814) | c2_2(X3_812, X4_814) | c4_2(X3_812, a152) | ~c5_2(X3_812, a152) | c4_2(X3_812, V_813) | c3_2(X3_812, V_813) | c7_1(X3_812) | c4_2(X3_812, a264) | ~c1_2(X3_812, a264) | ~c6_2(X3_812, a147) | c4_2(X3_812, a147) | c4_2(X3_812, a263) | ~c6_1(X3_812) | ~c5_1(X3_812) | ~c5_2(X3_812, X4_814) | ~c3_2(X3_812, X4_814) | ~ndr1_1(X3_812)))). % 33.45/17.88 tff(c_11893, plain, (![X141_824, X4_826, V_825]: (c4_1(X141_824) | c1_2(X141_824, X4_826) | c2_2(X141_824, X4_826) | c4_2(X141_824, a264) | ~c5_2(X141_824, a264) | c4_2(X141_824, V_825) | c3_2(X141_824, V_825) | c7_1(X141_824) | c4_2(X141_824, a152) | ~c1_2(X141_824, a152) | ~c6_2(X141_824, a147) | c4_2(X141_824, a147) | ~c5_1(X141_824) | ~c5_2(X141_824, X4_826) | ~c3_2(X141_824, X4_826) | ~ndr1_1(X141_824) | c4_2(X141_824, a263) | ~c6_1(X141_824)))). % 33.45/17.88 tff(c_11782, plain, (![X141_821, X4_823, V_822]: (c4_1(X141_821) | c1_2(X141_821, X4_823) | c2_2(X141_821, X4_823) | c4_2(X141_821, a264) | ~c5_2(X141_821, a264) | c4_2(X141_821, V_822) | c3_2(X141_821, V_822) | c7_1(X141_821) | c4_2(X141_821, a152) | ~c1_2(X141_821, a152) | ~c6_2(X141_821, a147) | c4_2(X141_821, a147) | ~c5_1(X141_821) | ~c5_2(X141_821, X4_823) | ~c3_2(X141_821, X4_823) | ~ndr1_1(X141_821) | ~c5_2(X141_821, a263) | ~c6_1(X141_821)))). % 33.45/17.88 tff(c_11571, plain, (![X3_815, X4_817, V_816]: (c4_1(X3_815) | c1_2(X3_815, X4_817) | c2_2(X3_815, X4_817) | c4_2(X3_815, a152) | ~c5_2(X3_815, a152) | c4_2(X3_815, V_816) | c3_2(X3_815, V_816) | c7_1(X3_815) | c4_2(X3_815, a264) | ~c1_2(X3_815, a264) | ~c6_2(X3_815, a147) | c4_2(X3_815, a147) | ~c5_2(X3_815, a263) | ~c6_1(X3_815) | ~c5_1(X3_815) | ~c5_2(X3_815, X4_817) | ~c3_2(X3_815, X4_817) | ~ndr1_1(X3_815)))). % 33.45/17.88 tff(c_13328, plain, (![X141_191, V_909, X40_910]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_909) | c3_2(X141_191, V_909) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_910) | c7_1(X141_191) | c4_2(X141_191, X40_910) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_910) | ~ndr1_1(X141_191) | c8_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.88 tff(c_13329, plain, (![X141_191, V_909, X40_910]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_909) | c3_2(X141_191, V_909) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_910) | c7_1(X141_191) | c4_2(X141_191, X40_910) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_910) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_13330, plain, (![X141_191, V_909, X40_910]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_909) | c3_2(X141_191, V_909) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_910) | c7_1(X141_191) | c4_2(X141_191, X40_910) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_910) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_13196, plain, (![X141_191, V_905, X40_906]: (c4_2(X141_191, a264) | c4_2(X141_191, V_905) | c3_2(X141_191, V_905) | ~c3_2(X141_191, a152) | ~c3_2(X141_191, X40_906) | c7_1(X141_191) | c4_2(X141_191, X40_906) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_906) | c8_1(X141_191) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_13195, plain, (![X141_191, V_905, X40_906]: (c4_2(X141_191, a264) | c4_2(X141_191, V_905) | c3_2(X141_191, V_905) | ~c3_2(X141_191, a152) | ~c3_2(X141_191, X40_906) | c7_1(X141_191) | c4_2(X141_191, X40_906) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_906) | c8_1(X141_191) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_12889, plain, (![X39_58, V_887, X40_888]: (c4_2(X39_58, a264) | ~c5_2(X39_58, a264) | c4_2(X39_58, V_887) | c3_2(X39_58, V_887) | ~c4_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_888) | c7_1(X39_58) | c4_2(X39_58, X40_888) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_888) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.89 tff(c_12765, plain, (![X39_58, V_868, X40_869]: (c4_2(X39_58, a264) | ~c5_2(X39_58, a264) | c4_2(X39_58, V_868) | c3_2(X39_58, V_868) | ~c3_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_869) | c7_1(X39_58) | c4_2(X39_58, X40_869) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c1_2(X39_58, X40_869) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.89 tff(c_13823, plain, (![X3_12, X4_14, V_961, X40_962]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_961) | c3_2(X3_12, V_961) | ~c3_2(X3_12, X40_962) | c7_1(X3_12) | c4_2(X3_12, X40_962) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | ~c1_2(X3_12, X40_962) | c8_1(X3_12) | c4_1(X3_12) | c1_2(X3_12, a152) | c2_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_12276, plain, (![X158_209, X159_211, V_849, X4_850]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | ~c5_2(X158_209, a152) | c4_2(X158_209, V_849) | c3_2(X158_209, V_849) | c7_1(X158_209) | c4_2(X158_209, a152) | ~c1_2(X158_209, a152) | ~c6_2(X158_209, a147) | c4_2(X158_209, a147) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_850) | ~c3_2(X158_209, X4_850) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.89 tff(c_9024, plain, (![X39_592, W_5, V_4, X40_593]: (~c7_2(X39_592, W_5) | c4_2(X39_592, W_5) | ~c5_2(X39_592, W_5) | c4_2(X39_592, V_4) | c3_2(X39_592, V_4) | c4_1(X39_592) | c1_2(X39_592, a152) | c2_2(X39_592, a152) | ~c5_1(X39_592) | ~c3_2(X39_592, X40_593) | c7_1(X39_592) | c4_2(X39_592, X40_593) | ~c6_2(X39_592, a147) | c4_2(X39_592, a147) | c1_1(X39_592) | ~c1_2(X39_592, X40_593) | ~ndr1_1(X39_592) | c8_1(X39_592)))). % 33.45/17.89 tff(c_11099, plain, (![X39_774, X77_777, V_775, X40_776]: (c4_1(X39_774) | c1_2(X39_774, X77_777) | c2_2(X39_774, X77_777) | c5_2(X39_774, a147) | c4_2(X39_774, a152) | ~c5_2(X39_774, a152) | c4_2(X39_774, V_775) | c3_2(X39_774, V_775) | ~c5_1(X39_774) | ~c3_2(X39_774, X40_776) | c7_1(X39_774) | c4_2(X39_774, X40_776) | ~c6_2(X39_774, X77_777) | c4_2(X39_774, X77_777) | c1_1(X39_774) | ~c1_2(X39_774, X40_776) | ~ndr1_1(X39_774) | c8_1(X39_774)))). % 33.45/17.89 tff(c_11218, plain, (![X39_778, X77_781, V_779, X40_780]: (c4_1(X39_778) | c1_2(X39_778, X77_781) | c2_2(X39_778, X77_781) | ~c3_2(X39_778, a147) | c4_2(X39_778, a152) | ~c5_2(X39_778, a152) | c4_2(X39_778, V_779) | c3_2(X39_778, V_779) | ~c5_1(X39_778) | ~c3_2(X39_778, X40_780) | c7_1(X39_778) | c4_2(X39_778, X40_780) | ~c6_2(X39_778, X77_781) | c4_2(X39_778, X77_781) | c1_1(X39_778) | ~c1_2(X39_778, X40_780) | ~ndr1_1(X39_778) | c8_1(X39_778)))). % 33.45/17.89 tff(c_8245, plain, (![X3_12, V_539, X40_540, X4_14]: (c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X4_14) | c4_2(X3_12, X4_14) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_12242, plain, (![X3_841, X4_843, X77_112, V_842]: (c4_2(X3_841, X4_843) | ~c1_2(X3_841, X4_843) | ~c6_2(X3_841, X77_112) | c4_2(X3_841, X77_112) | c7_2(X3_841, X77_112) | ~c5_2(X3_841, a152) | c4_2(X3_841, V_842) | c3_2(X3_841, V_842) | c7_1(X3_841) | c4_2(X3_841, a152) | ~c1_2(X3_841, a152) | ~c6_2(X3_841, a147) | c4_2(X3_841, a147) | ~c5_1(X3_841) | ~c5_2(X3_841, X4_843) | ~c3_2(X3_841, X4_843) | ~ndr1_1(X3_841)))). % 33.45/17.89 tff(c_10481, plain, (![X3_12, X4_14, V_752]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_752) | c3_2(X3_12, V_752) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c6_1(X3_12) | c1_1(X3_12) | c5_2(X3_12, a263) | ~c1_2(X3_12, a263) | c8_1(X3_12) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_10374, plain, (![X39_243, V_748, X40_749]: (c4_2(X39_243, a264) | c4_2(X39_243, V_748) | c3_2(X39_243, V_748) | c7_1(X39_243) | c4_2(X39_243, X40_749) | ~c6_2(X39_243, a147) | c4_2(X39_243, a147) | c5_2(X39_243, X40_749) | ~c1_2(X39_243, X40_749) | c7_2(X39_243, a152) | ~c5_1(X39_243) | ~c3_2(X39_243, a264) | ~c6_1(X39_243) | c1_1(X39_243) | c5_2(X39_243, a263) | ~c1_2(X39_243, a263) | ~ndr1_1(X39_243) | c8_1(X39_243)))). % 33.45/17.89 tff(c_10480, plain, (![X3_12, X4_14, V_752]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_752) | c3_2(X3_12, V_752) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c6_1(X3_12) | c1_1(X3_12) | c5_2(X3_12, a263) | ~c1_2(X3_12, a263) | c8_1(X3_12) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_13450, plain, (![X39_930, V_931]: (c4_1(X39_930) | c1_2(X39_930, a152) | c2_2(X39_930, a152) | c4_2(X39_930, V_931) | c3_2(X39_930, V_931) | c7_1(X39_930) | c4_2(X39_930, a264) | ~c1_2(X39_930, a264) | ~c6_2(X39_930, a147) | c4_2(X39_930, a147) | ~c5_1(X39_930) | ~c3_2(X39_930, a264) | ~c6_1(X39_930) | c1_1(X39_930) | c5_2(X39_930, a263) | ~c1_2(X39_930, a263) | ~ndr1_1(X39_930) | c8_1(X39_930)))). % 33.45/17.89 tff(c_13393, plain, (![X39_243, V_929]: (c4_2(X39_243, V_929) | c3_2(X39_243, V_929) | c7_1(X39_243) | c4_2(X39_243, a264) | ~c1_2(X39_243, a264) | ~c6_2(X39_243, a147) | c4_2(X39_243, a147) | c7_2(X39_243, a152) | ~c5_1(X39_243) | ~c3_2(X39_243, a264) | ~c6_1(X39_243) | c1_1(X39_243) | c5_2(X39_243, a263) | ~c1_2(X39_243, a263) | ~ndr1_1(X39_243) | c8_1(X39_243)))). % 33.45/17.89 tff(c_10479, plain, (![X3_12, X4_14, V_752]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_752) | c3_2(X3_12, V_752) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c6_1(X3_12) | c1_1(X3_12) | c5_2(X3_12, a263) | ~c1_2(X3_12, a263) | c8_1(X3_12) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_8250, plain, (![X3_12, X4_14, V_539, X40_540]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c7_1(X3_12) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | c4_1(X3_12) | c1_2(X3_12, a152) | c2_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_9026, plain, (![X39_592, X77_594, X44_66, X40_593]: (~c5_2(X39_592, X77_594) | c6_1(X39_592) | ~c8_2(X39_592, X44_66) | ~c6_2(X39_592, X44_66) | c5_2(X39_592, X44_66) | c4_1(X39_592) | c1_2(X39_592, a152) | c2_2(X39_592, a152) | ~c5_1(X39_592) | ~c3_2(X39_592, X40_593) | c7_1(X39_592) | c4_2(X39_592, X40_593) | ~c6_2(X39_592, X77_594) | c4_2(X39_592, X77_594) | c1_1(X39_592) | ~c1_2(X39_592, X40_593) | ~ndr1_1(X39_592) | c8_1(X39_592)))). % 33.45/17.89 tff(c_8256, plain, (![X40_540, X77_306, V_539, X39_58, X40_60]: (~c5_2(X39_58, X77_306) | c4_2(X39_58, V_539) | c3_2(X39_58, V_539) | c4_2(X39_58, X40_540) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | c5_2(X39_58, X40_540) | ~c1_2(X39_58, X40_540) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.89 tff(c_8029, plain, (![X3_12, V_511, X4_14]: (c4_2(X3_12, V_511) | c3_2(X3_12, V_511) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, a263) | ~c6_1(X3_12) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X4_14) | c4_2(X3_12, X4_14) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_10871, plain, (![X39_761, W_5, V_4, X40_762]: (~c7_2(X39_761, W_5) | c4_2(X39_761, W_5) | ~c5_2(X39_761, W_5) | c4_2(X39_761, V_4) | c3_2(X39_761, V_4) | c4_2(X39_761, a152) | ~c1_2(X39_761, a152) | ~c5_1(X39_761) | ~c3_2(X39_761, X40_762) | c7_1(X39_761) | c4_2(X39_761, X40_762) | ~c6_2(X39_761, a147) | c4_2(X39_761, a147) | c1_1(X39_761) | ~c1_2(X39_761, X40_762) | ~ndr1_1(X39_761) | c8_1(X39_761)))). % 33.45/17.89 tff(c_11344, plain, (![X3_12, X4_14, V_787, X40_788]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_787) | c3_2(X3_12, V_787) | ~c3_2(X3_12, a152) | ~c3_2(X3_12, X40_788) | c7_1(X3_12) | c4_2(X3_12, X40_788) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | ~c1_2(X3_12, X40_788) | c8_1(X3_12) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_8116, plain, (![X3_12, X4_14, V_518]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_518) | c3_2(X3_12, V_518) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c4_2(X3_12, a263) | ~c6_1(X3_12) | c4_1(X3_12) | c1_2(X3_12, a152) | c2_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_8034, plain, (![X3_12, X4_14, V_511]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_511) | c3_2(X3_12, V_511) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, a263) | ~c6_1(X3_12) | c4_1(X3_12) | c1_2(X3_12, a152) | c2_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_8262, plain, (![X3_12, V_539, X40_540, X4_14]: (c4_2(X3_12, a152) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c7_1(X3_12) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_10873, plain, (![X39_761, X77_763, X44_66, X40_762]: (~c5_2(X39_761, X77_763) | c6_1(X39_761) | ~c8_2(X39_761, X44_66) | ~c6_2(X39_761, X44_66) | c5_2(X39_761, X44_66) | c4_2(X39_761, a152) | ~c1_2(X39_761, a152) | ~c5_1(X39_761) | ~c3_2(X39_761, X40_762) | c7_1(X39_761) | c4_2(X39_761, X40_762) | ~c6_2(X39_761, X77_763) | c4_2(X39_761, X77_763) | c1_1(X39_761) | ~c1_2(X39_761, X40_762) | ~ndr1_1(X39_761) | c8_1(X39_761)))). % 33.45/17.89 tff(c_10995, plain, (![X141_191, V_772, X40_773]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_772) | c3_2(X141_191, V_772) | ~c4_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_773) | c7_1(X141_191) | c4_2(X141_191, X40_773) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_773) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_10993, plain, (![X141_191, V_772, X40_773]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_772) | c3_2(X141_191, V_772) | ~c4_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_773) | c7_1(X141_191) | c4_2(X141_191, X40_773) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_773) | ~ndr1_1(X141_191) | c8_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_10994, plain, (![X141_191, V_772, X40_773]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_772) | c3_2(X141_191, V_772) | ~c4_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_773) | c7_1(X141_191) | c4_2(X141_191, X40_773) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_773) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_9025, plain, (![X39_592, X77_594, V_4, X40_593]: (~c3_2(X39_592, a147) | ~c5_2(X39_592, X77_594) | c4_2(X39_592, V_4) | c3_2(X39_592, V_4) | c4_1(X39_592) | c1_2(X39_592, a152) | c2_2(X39_592, a152) | ~c5_1(X39_592) | ~c3_2(X39_592, X40_593) | c7_1(X39_592) | c4_2(X39_592, X40_593) | ~c6_2(X39_592, X77_594) | c4_2(X39_592, X77_594) | c1_1(X39_592) | ~c1_2(X39_592, X40_593) | ~ndr1_1(X39_592) | c8_1(X39_592)))). % 33.45/17.89 tff(c_11347, plain, (![X141_191, V_787, X40_788]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_787) | c3_2(X141_191, V_787) | ~c3_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_788) | c7_1(X141_191) | c4_2(X141_191, X40_788) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_788) | ~ndr1_1(X141_191) | c8_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_11348, plain, (![X141_191, V_787, X40_788]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_787) | c3_2(X141_191, V_787) | ~c3_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_788) | c7_1(X141_191) | c4_2(X141_191, X40_788) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_788) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_11349, plain, (![X141_191, V_787, X40_788]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_787) | c3_2(X141_191, V_787) | ~c3_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, X40_788) | c7_1(X141_191) | c4_2(X141_191, X40_788) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | ~c1_2(X141_191, X40_788) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_9023, plain, (![X39_592, X77_594, V_4, X40_593]: (c5_2(X39_592, a147) | ~c5_2(X39_592, X77_594) | c4_2(X39_592, V_4) | c3_2(X39_592, V_4) | c4_1(X39_592) | c1_2(X39_592, a152) | c2_2(X39_592, a152) | ~c5_1(X39_592) | ~c3_2(X39_592, X40_593) | c7_1(X39_592) | c4_2(X39_592, X40_593) | ~c6_2(X39_592, X77_594) | c4_2(X39_592, X77_594) | c1_1(X39_592) | ~c1_2(X39_592, X40_593) | ~ndr1_1(X39_592) | c8_1(X39_592)))). % 33.45/17.89 tff(c_10477, plain, (![X3_12, V_752]: (c4_2(X3_12, a152) | c4_2(X3_12, V_752) | c3_2(X3_12, V_752) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c6_1(X3_12) | c1_1(X3_12) | c5_2(X3_12, a263) | ~c1_2(X3_12, a263) | c8_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_10379, plain, (![X141_191, V_748, X40_749]: (c4_2(X141_191, a264) | c4_2(X141_191, V_748) | c3_2(X141_191, V_748) | c7_1(X141_191) | c4_2(X141_191, X40_749) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | c5_2(X141_191, X40_749) | ~c1_2(X141_191, X40_749) | c8_1(X141_191) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_10380, plain, (![X141_191, V_748, X40_749]: (c4_2(X141_191, a264) | c4_2(X141_191, V_748) | c3_2(X141_191, V_748) | c7_1(X141_191) | c4_2(X141_191, X40_749) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | c5_2(X141_191, X40_749) | ~c1_2(X141_191, X40_749) | c8_1(X141_191) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_9892, plain, (![X158_209, X77_648, X159_211, X4_650]: (~c5_2(X158_209, X77_648) | c6_1(X158_209) | c5_2(X158_209, X159_211) | c7_1(X158_209) | c4_2(X158_209, a152) | ~c1_2(X158_209, a152) | ~c6_2(X158_209, X77_648) | c4_2(X158_209, X77_648) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_650) | c7_2(X158_209, X4_650) | ~c3_2(X158_209, X4_650) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.89 tff(c_12248, plain, (![X3_841, X44_66, V_842, X4_843]: (c6_1(X3_841) | ~c8_2(X3_841, X44_66) | ~c6_2(X3_841, X44_66) | c5_2(X3_841, X44_66) | ~c5_2(X3_841, a152) | c4_2(X3_841, V_842) | c3_2(X3_841, V_842) | c7_1(X3_841) | c4_2(X3_841, a152) | ~c1_2(X3_841, a152) | ~c6_2(X3_841, a147) | c4_2(X3_841, a147) | ~c5_1(X3_841) | ~c5_2(X3_841, X4_843) | ~c3_2(X3_841, X4_843) | ~ndr1_1(X3_841)))). % 33.45/17.89 tff(c_12238, plain, (![X3_841, X4_843, V_842]: (c4_1(X3_841) | c1_2(X3_841, X4_843) | c2_2(X3_841, X4_843) | ~c5_2(X3_841, a152) | c4_2(X3_841, V_842) | c3_2(X3_841, V_842) | c7_1(X3_841) | c4_2(X3_841, a152) | ~c1_2(X3_841, a152) | ~c6_2(X3_841, a147) | c4_2(X3_841, a147) | ~c5_1(X3_841) | ~c5_2(X3_841, X4_843) | ~c3_2(X3_841, X4_843) | ~ndr1_1(X3_841)))). % 33.45/17.89 tff(c_11939, plain, (![X3_12, V_703, X4_704]: (~c5_2(X3_12, a152) | c4_2(X3_12, V_703) | c3_2(X3_12, V_703) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_704) | ~c3_2(X3_12, X4_704) | ~ndr1_1(X3_12) | c7_2(X3_12, X4_704)))). % 33.45/17.89 tff(c_10122, plain, (![X3_12, V_703, X4_704, X4_14]: (c4_2(X3_12, V_703) | c3_2(X3_12, V_703) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, X4_704) | c7_2(X3_12, X4_704) | ~c3_2(X3_12, X4_704) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X4_14) | c4_2(X3_12, X4_14) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_10216, plain, (![X141_711, V_4, V_712]: (c4_2(X141_711, a152) | ~c5_2(X141_711, a152) | c4_2(X141_711, V_4) | c3_2(X141_711, V_4) | c4_2(X141_711, V_712) | c3_2(X141_711, V_712) | c7_1(X141_711) | c4_2(X141_711, a264) | ~c1_2(X141_711, a264) | ~c6_2(X141_711, a147) | c4_2(X141_711, a147) | ~c5_1(X141_711) | ~c3_2(X141_711, a264) | ~ndr1_1(X141_711) | c4_2(X141_711, a263) | ~c6_1(X141_711)))). % 33.45/17.89 tff(c_10036, plain, (![X141_691, V_4, V_692]: (c4_2(X141_691, a152) | ~c5_2(X141_691, a152) | c4_2(X141_691, V_4) | c3_2(X141_691, V_4) | c4_2(X141_691, V_692) | c3_2(X141_691, V_692) | c7_1(X141_691) | c4_2(X141_691, a264) | ~c1_2(X141_691, a264) | ~c6_2(X141_691, a147) | c4_2(X141_691, a147) | ~c5_1(X141_691) | ~c3_2(X141_691, a264) | ~ndr1_1(X141_691) | ~c5_2(X141_691, a263) | ~c6_1(X141_691)))). % 33.45/17.89 tff(c_10142, plain, (![X141_191, V_703, X4_704]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_703) | c3_2(X141_191, V_703) | c7_1(X141_191) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | ~c5_1(X141_191) | ~c5_2(X141_191, X4_704) | c7_2(X141_191, X4_704) | ~c3_2(X141_191, X4_704) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_10143, plain, (![X141_191, V_703, X4_704]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_703) | c3_2(X141_191, V_703) | c7_1(X141_191) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | ~c5_1(X141_191) | ~c5_2(X141_191, X4_704) | c7_2(X141_191, X4_704) | ~c3_2(X141_191, X4_704) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_10144, plain, (![X141_191, V_703, X4_704]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_703) | c3_2(X141_191, V_703) | c7_1(X141_191) | c4_2(X141_191, a152) | ~c1_2(X141_191, a152) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | ~c5_1(X141_191) | ~c5_2(X141_191, X4_704) | c7_2(X141_191, X4_704) | ~c3_2(X141_191, X4_704) | ~ndr1_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.89 tff(c_8045, plain, (![X3_12, V_511, X4_14]: (c4_2(X3_12, a152) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_511) | c3_2(X3_12, V_511) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, a263) | ~c6_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_8127, plain, (![X3_12, V_518, X4_14]: (c4_2(X3_12, a152) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_518) | c3_2(X3_12, V_518) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c4_2(X3_12, a263) | ~c6_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_10870, plain, (![X39_761, X77_763, V_4, X40_762]: (c5_2(X39_761, a147) | ~c5_2(X39_761, X77_763) | c4_2(X39_761, V_4) | c3_2(X39_761, V_4) | c4_2(X39_761, a152) | ~c1_2(X39_761, a152) | ~c5_1(X39_761) | ~c3_2(X39_761, X40_762) | c7_1(X39_761) | c4_2(X39_761, X40_762) | ~c6_2(X39_761, X77_763) | c4_2(X39_761, X77_763) | c1_1(X39_761) | ~c1_2(X39_761, X40_762) | ~ndr1_1(X39_761) | c8_1(X39_761)))). % 33.45/17.89 tff(c_10872, plain, (![X39_761, X77_763, V_4, X40_762]: (~c3_2(X39_761, a147) | ~c5_2(X39_761, X77_763) | c4_2(X39_761, V_4) | c3_2(X39_761, V_4) | c4_2(X39_761, a152) | ~c1_2(X39_761, a152) | ~c5_1(X39_761) | ~c3_2(X39_761, X40_762) | c7_1(X39_761) | c4_2(X39_761, X40_762) | ~c6_2(X39_761, X77_763) | c4_2(X39_761, X77_763) | c1_1(X39_761) | ~c1_2(X39_761, X40_762) | ~ndr1_1(X39_761) | c8_1(X39_761)))). % 33.45/17.89 tff(c_7600, plain, (![X3_12, X77_306, X4_442, X4_14]: (~c5_2(X3_12, a152) | c6_1(X3_12) | c5_2(X3_12, X77_306) | ~c5_2(X3_12, X4_442) | c7_2(X3_12, X4_442) | ~c3_2(X3_12, X4_442) | c4_1(X3_12) | ~c8_1(X3_12) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_11345, plain, (![X3_12, X4_14, V_787, X40_788]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_787) | c3_2(X3_12, V_787) | ~c3_2(X3_12, X40_788) | c7_1(X3_12) | c4_2(X3_12, X40_788) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | ~c1_2(X3_12, X40_788) | c8_1(X3_12) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_10992, plain, (![X3_12, X4_14, V_772, X40_773]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_772) | c3_2(X3_12, V_772) | ~c3_2(X3_12, X40_773) | c7_1(X3_12) | c4_2(X3_12, X40_773) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | ~c1_2(X3_12, X40_773) | c8_1(X3_12) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_11342, plain, (![X3_12, V_787, X40_788]: (c4_2(X3_12, a152) | c4_2(X3_12, V_787) | c3_2(X3_12, V_787) | ~c3_2(X3_12, X40_788) | c7_1(X3_12) | c4_2(X3_12, X40_788) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | ~c1_2(X3_12, X40_788) | c8_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.89 tff(c_9457, plain, (![X39_621, W_5, V_4, X40_622]: (~c7_2(X39_621, W_5) | c4_2(X39_621, W_5) | ~c5_2(X39_621, W_5) | c4_2(X39_621, V_4) | c3_2(X39_621, V_4) | ~c3_2(X39_621, a152) | ~c5_1(X39_621) | ~c3_2(X39_621, X40_622) | c7_1(X39_621) | c4_2(X39_621, X40_622) | ~c6_2(X39_621, a147) | c4_2(X39_621, a147) | c1_1(X39_621) | ~c1_2(X39_621, X40_622) | ~ndr1_1(X39_621) | c8_1(X39_621)))). % 33.45/17.89 tff(c_9874, plain, (![X39_58, V_642, X40_643]: (c4_2(X39_58, a264) | ~c5_2(X39_58, a264) | c4_2(X39_58, V_642) | c3_2(X39_58, V_642) | c7_1(X39_58) | c4_2(X39_58, X40_643) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | c5_2(X39_58, X40_643) | ~c1_2(X39_58, X40_643) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.89 tff(c_8879, plain, (![X39_585, V_4, X40_586, X77_587]: (~c3_2(X39_585, a147) | c4_2(X39_585, a152) | ~c5_2(X39_585, a152) | c4_2(X39_585, V_4) | c3_2(X39_585, V_4) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585) | c7_2(X39_585, X77_587)))). % 33.45/17.89 tff(c_8878, plain, (![X39_585, V_4, X40_586, X77_587]: (c5_2(X39_585, a147) | c4_2(X39_585, a152) | ~c5_2(X39_585, a152) | c4_2(X39_585, V_4) | c3_2(X39_585, V_4) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585) | c7_2(X39_585, X77_587)))). % 33.45/17.89 tff(c_9770, plain, (![X39_635, W_5, V_4, X40_636]: (~c7_2(X39_635, W_5) | c4_2(X39_635, W_5) | ~c5_2(X39_635, W_5) | c4_2(X39_635, V_4) | c3_2(X39_635, V_4) | ~c4_2(X39_635, a152) | ~c5_1(X39_635) | ~c3_2(X39_635, X40_636) | c7_1(X39_635) | c4_2(X39_635, X40_636) | ~c6_2(X39_635, a147) | c4_2(X39_635, a147) | c1_1(X39_635) | ~c1_2(X39_635, X40_636) | ~ndr1_1(X39_635) | c8_1(X39_635)))). % 33.45/17.89 tff(c_10460, plain, (![X39_58, X77_318, V_752]: (~c5_2(X39_58, X77_318) | c4_2(X39_58, V_752) | c3_2(X39_58, V_752) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | c7_1(X39_58) | c4_2(X39_58, a264) | ~c1_2(X39_58, a264) | ~c6_2(X39_58, X77_318) | c4_2(X39_58, X77_318) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.89 tff(c_10863, plain, (![X39_761, X77_763, X40_762]: (c4_1(X39_761) | c1_2(X39_761, X77_763) | c2_2(X39_761, X77_763) | c4_2(X39_761, a152) | ~c1_2(X39_761, a152) | ~c5_1(X39_761) | ~c3_2(X39_761, X40_762) | c7_1(X39_761) | c4_2(X39_761, X40_762) | ~c6_2(X39_761, X77_763) | c4_2(X39_761, X77_763) | c1_1(X39_761) | ~c1_2(X39_761, X40_762) | ~ndr1_1(X39_761) | c8_1(X39_761)))). % 33.45/17.89 tff(c_10594, plain, (![X39_585, X40_586, X77_112]: (c4_2(X39_585, a152) | ~c1_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_112) | c4_2(X39_585, X77_112) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585) | c7_2(X39_585, X77_112)))). % 33.45/17.90 tff(c_10574, plain, (![X39_58, V_754]: (~c5_2(X39_58, a264) | c4_2(X39_58, V_754) | c3_2(X39_58, V_754) | c7_1(X39_58) | c4_2(X39_58, a264) | ~c1_2(X39_58, a264) | ~c6_2(X39_58, a147) | c4_2(X39_58, a147) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.90 tff(c_7729, plain, (![X39_449, W_5, V_4]: (~c7_2(X39_449, W_5) | c4_2(X39_449, W_5) | ~c5_2(X39_449, W_5) | c4_2(X39_449, V_4) | c3_2(X39_449, V_4) | c7_1(X39_449) | c4_2(X39_449, a264) | ~c1_2(X39_449, a264) | ~c6_2(X39_449, a147) | c4_2(X39_449, a147) | ~c6_1(X39_449) | c1_1(X39_449) | c5_2(X39_449, a263) | ~c1_2(X39_449, a263) | ~ndr1_1(X39_449) | c8_1(X39_449)))). % 33.45/17.90 tff(c_8263, plain, (![X3_12, X4_14, V_539, X40_540]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c7_1(X3_12) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_8265, plain, (![X3_12, X4_14, V_539, X40_540]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c7_1(X3_12) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_8264, plain, (![X3_12, X4_14, V_539, X40_540]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c7_1(X3_12) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_9772, plain, (![X39_635, X77_637, X44_66, X40_636]: (~c5_2(X39_635, X77_637) | c6_1(X39_635) | ~c8_2(X39_635, X44_66) | ~c6_2(X39_635, X44_66) | c5_2(X39_635, X44_66) | ~c4_2(X39_635, a152) | ~c5_1(X39_635) | ~c3_2(X39_635, X40_636) | c7_1(X39_635) | c4_2(X39_635, X40_636) | ~c6_2(X39_635, X77_637) | c4_2(X39_635, X77_637) | c1_1(X39_635) | ~c1_2(X39_635, X40_636) | ~ndr1_1(X39_635) | c8_1(X39_635)))). % 33.45/17.90 tff(c_9459, plain, (![X39_621, X77_623, X44_66, X40_622]: (~c5_2(X39_621, X77_623) | c6_1(X39_621) | ~c8_2(X39_621, X44_66) | ~c6_2(X39_621, X44_66) | c5_2(X39_621, X44_66) | ~c3_2(X39_621, a152) | ~c5_1(X39_621) | ~c3_2(X39_621, X40_622) | c7_1(X39_621) | c4_2(X39_621, X40_622) | ~c6_2(X39_621, X77_623) | c4_2(X39_621, X77_623) | c1_1(X39_621) | ~c1_2(X39_621, X40_622) | ~ndr1_1(X39_621) | c8_1(X39_621)))). % 33.45/17.90 tff(c_8880, plain, (![X39_585, X44_66, X40_586, X77_587]: (~c5_2(X39_585, a152) | c6_1(X39_585) | ~c8_2(X39_585, X44_66) | ~c6_2(X39_585, X44_66) | c5_2(X39_585, X44_66) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585) | c7_2(X39_585, X77_587)))). % 33.45/17.90 tff(c_8895, plain, (![X39_585, X77_587, X44_66, X40_586]: (~c5_2(X39_585, X77_587) | c6_1(X39_585) | ~c8_2(X39_585, X44_66) | ~c6_2(X39_585, X44_66) | c5_2(X39_585, X44_66) | c7_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585)))). % 33.45/17.90 tff(c_8290, plain, (![X158_209, X159_211, X77_543, X4_544]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | c7_1(X158_209) | c4_2(X158_209, a152) | ~c1_2(X158_209, a152) | ~c6_2(X158_209, X77_543) | c4_2(X158_209, X77_543) | c7_2(X158_209, X77_543) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_544) | ~c3_2(X158_209, X4_544) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.90 tff(c_10219, plain, (![X141_711, V_712]: (c4_1(X141_711) | c1_2(X141_711, a152) | c2_2(X141_711, a152) | c4_2(X141_711, V_712) | c3_2(X141_711, V_712) | c7_1(X141_711) | c4_2(X141_711, a264) | ~c1_2(X141_711, a264) | ~c6_2(X141_711, a147) | c4_2(X141_711, a147) | ~c5_1(X141_711) | ~c3_2(X141_711, a264) | ~ndr1_1(X141_711) | c4_2(X141_711, a263) | ~c6_1(X141_711)))). % 33.45/17.90 tff(c_10178, plain, (![X141_191, V_710]: (c4_2(X141_191, V_710) | c3_2(X141_191, V_710) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_8128, plain, (![X3_12, X4_14, V_518]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_518) | c3_2(X3_12, V_518) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c4_2(X3_12, a263) | ~c6_1(X3_12) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_8047, plain, (![X3_12, X4_14, V_511]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_511) | c3_2(X3_12, V_511) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, a263) | ~c6_1(X3_12) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_7363, plain, (![X3_429, W_5, V_4, X4_431]: (~c7_2(X3_429, W_5) | c4_2(X3_429, W_5) | ~c5_2(X3_429, W_5) | c4_2(X3_429, V_4) | c3_2(X3_429, V_4) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, a147) | c4_2(X3_429, a147) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | c7_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_8130, plain, (![X3_12, X4_14, V_518]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_518) | c3_2(X3_12, V_518) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c4_2(X3_12, a263) | ~c6_1(X3_12) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_8129, plain, (![X3_12, X4_14, V_518]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_518) | c3_2(X3_12, V_518) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c4_2(X3_12, a263) | ~c6_1(X3_12) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_10038, plain, (![X141_691, V_692]: (c4_1(X141_691) | c1_2(X141_691, a152) | c2_2(X141_691, a152) | c4_2(X141_691, V_692) | c3_2(X141_691, V_692) | c7_1(X141_691) | c4_2(X141_691, a264) | ~c1_2(X141_691, a264) | ~c6_2(X141_691, a147) | c4_2(X141_691, a147) | ~c5_1(X141_691) | ~c3_2(X141_691, a264) | ~ndr1_1(X141_691) | ~c5_2(X141_691, a263) | ~c6_1(X141_691)))). % 33.45/17.90 tff(c_10002, plain, (![X141_191, V_690]: (c4_2(X141_191, V_690) | c3_2(X141_191, V_690) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c7_2(X141_191, a152) | ~c5_1(X141_191) | ~c3_2(X141_191, a264) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_8046, plain, (![X3_12, X4_14, V_511]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_511) | c3_2(X3_12, V_511) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, a263) | ~c6_1(X3_12) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_8048, plain, (![X3_12, X4_14, V_511]: (c4_2(X3_12, X4_14) | c4_2(X3_12, V_511) | c3_2(X3_12, V_511) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, a263) | ~c6_1(X3_12) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_7384, plain, (![X3_429, X4_431, X77_112, X77_430]: (c4_2(X3_429, X4_431) | ~c1_2(X3_429, X4_431) | ~c6_2(X3_429, X77_112) | c4_2(X3_429, X77_112) | c7_2(X3_429, X77_112) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | c7_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_9769, plain, (![X39_635, X77_637, V_4, X40_636]: (c5_2(X39_635, a147) | ~c5_2(X39_635, X77_637) | c4_2(X39_635, V_4) | c3_2(X39_635, V_4) | ~c4_2(X39_635, a152) | ~c5_1(X39_635) | ~c3_2(X39_635, X40_636) | c7_1(X39_635) | c4_2(X39_635, X40_636) | ~c6_2(X39_635, X77_637) | c4_2(X39_635, X77_637) | c1_1(X39_635) | ~c1_2(X39_635, X40_636) | ~ndr1_1(X39_635) | c8_1(X39_635)))). % 33.45/17.90 tff(c_9771, plain, (![X39_635, X77_637, V_4, X40_636]: (~c3_2(X39_635, a147) | ~c5_2(X39_635, X77_637) | c4_2(X39_635, V_4) | c3_2(X39_635, V_4) | ~c4_2(X39_635, a152) | ~c5_1(X39_635) | ~c3_2(X39_635, X40_636) | c7_1(X39_635) | c4_2(X39_635, X40_636) | ~c6_2(X39_635, X77_637) | c4_2(X39_635, X77_637) | c1_1(X39_635) | ~c1_2(X39_635, X40_636) | ~ndr1_1(X39_635) | c8_1(X39_635)))). % 33.45/17.90 tff(c_9458, plain, (![X39_621, X77_623, V_4, X40_622]: (~c3_2(X39_621, a147) | ~c5_2(X39_621, X77_623) | c4_2(X39_621, V_4) | c3_2(X39_621, V_4) | ~c3_2(X39_621, a152) | ~c5_1(X39_621) | ~c3_2(X39_621, X40_622) | c7_1(X39_621) | c4_2(X39_621, X40_622) | ~c6_2(X39_621, X77_623) | c4_2(X39_621, X77_623) | c1_1(X39_621) | ~c1_2(X39_621, X40_622) | ~ndr1_1(X39_621) | c8_1(X39_621)))). % 33.45/17.90 tff(c_8893, plain, (![X39_585, X77_587, V_4, X40_586]: (c5_2(X39_585, a147) | ~c5_2(X39_585, X77_587) | c4_2(X39_585, V_4) | c3_2(X39_585, V_4) | c7_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585)))). % 33.45/17.90 tff(c_8894, plain, (![X39_585, X77_587, V_4, X40_586]: (~c3_2(X39_585, a147) | ~c5_2(X39_585, X77_587) | c4_2(X39_585, V_4) | c3_2(X39_585, V_4) | c7_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585)))). % 33.45/17.90 tff(c_9456, plain, (![X39_621, X77_623, V_4, X40_622]: (c5_2(X39_621, a147) | ~c5_2(X39_621, X77_623) | c4_2(X39_621, V_4) | c3_2(X39_621, V_4) | ~c3_2(X39_621, a152) | ~c5_1(X39_621) | ~c3_2(X39_621, X40_622) | c7_1(X39_621) | c4_2(X39_621, X40_622) | ~c6_2(X39_621, X77_623) | c4_2(X39_621, X77_623) | c1_1(X39_621) | ~c1_2(X39_621, X40_622) | ~ndr1_1(X39_621) | c8_1(X39_621)))). % 33.45/17.90 tff(c_8266, plain, (![X141_191, V_539, X40_540]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_539) | c3_2(X141_191, V_539) | c7_1(X141_191) | c4_2(X141_191, X40_540) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | c5_2(X141_191, X40_540) | ~c1_2(X141_191, X40_540) | ~ndr1_1(X141_191) | c8_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_8261, plain, (![X3_12, V_539, X40_540]: (c4_2(X3_12, a152) | c4_2(X3_12, V_539) | c3_2(X3_12, V_539) | c7_1(X3_12) | c4_2(X3_12, X40_540) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c1_1(X3_12) | c5_2(X3_12, X40_540) | ~c1_2(X3_12, X40_540) | c8_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_7365, plain, (![X3_429, X77_430, X44_66, X4_431]: (~c5_2(X3_429, X77_430) | c6_1(X3_429) | ~c8_2(X3_429, X44_66) | ~c6_2(X3_429, X44_66) | c5_2(X3_429, X44_66) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | c7_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_8267, plain, (![X141_191, V_539, X40_540]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_539) | c3_2(X141_191, V_539) | c7_1(X141_191) | c4_2(X141_191, X40_540) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | c5_2(X141_191, X40_540) | ~c1_2(X141_191, X40_540) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_8268, plain, (![X141_191, V_539, X40_540]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_539) | c3_2(X141_191, V_539) | c7_1(X141_191) | c4_2(X141_191, X40_540) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c1_1(X141_191) | c5_2(X141_191, X40_540) | ~c1_2(X141_191, X40_540) | ~ndr1_1(X141_191) | c8_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_9762, plain, (![X39_635, X77_637, X40_636]: (c4_1(X39_635) | c1_2(X39_635, X77_637) | c2_2(X39_635, X77_637) | ~c4_2(X39_635, a152) | ~c5_1(X39_635) | ~c3_2(X39_635, X40_636) | c7_1(X39_635) | c4_2(X39_635, X40_636) | ~c6_2(X39_635, X77_637) | c4_2(X39_635, X77_637) | c1_1(X39_635) | ~c1_2(X39_635, X40_636) | ~ndr1_1(X39_635) | c8_1(X39_635)))). % 33.45/17.90 tff(c_9524, plain, (![X39_58, X40_60, X77_428]: (~c4_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_428) | c4_2(X39_58, X77_428) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58) | c7_2(X39_58, X77_428)))). % 33.45/17.90 tff(c_9449, plain, (![X39_621, X77_623, X40_622]: (c4_1(X39_621) | c1_2(X39_621, X77_623) | c2_2(X39_621, X77_623) | ~c3_2(X39_621, a152) | ~c5_1(X39_621) | ~c3_2(X39_621, X40_622) | c7_1(X39_621) | c4_2(X39_621, X40_622) | ~c6_2(X39_621, X77_623) | c4_2(X39_621, X77_623) | c1_1(X39_621) | ~c1_2(X39_621, X40_622) | ~ndr1_1(X39_621) | c8_1(X39_621)))). % 33.45/17.90 tff(c_6604, plain, (![X3_374, X4_376, X77_112, V_375]: (c7_1(X3_374) | c4_2(X3_374, X4_376) | ~c1_2(X3_374, X4_376) | ~c6_2(X3_374, X77_112) | c4_2(X3_374, X77_112) | c7_2(X3_374, X77_112) | ~c3_2(X3_374, a147) | c4_2(X3_374, a152) | ~c5_2(X3_374, a152) | c4_2(X3_374, V_375) | c3_2(X3_374, V_375) | ~c5_1(X3_374) | ~c5_2(X3_374, X4_376) | ~c3_2(X3_374, X4_376) | ~ndr1_1(X3_374)))). % 33.45/17.90 tff(c_9211, plain, (![X39_58, X40_60, X77_436]: (~c3_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_436) | c4_2(X39_58, X77_436) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58) | c7_2(X39_58, X77_436)))). % 33.45/17.90 tff(c_9016, plain, (![X39_592, X77_594, X40_593]: (c1_2(X39_592, X77_594) | c2_2(X39_592, X77_594) | c4_1(X39_592) | c1_2(X39_592, a152) | c2_2(X39_592, a152) | ~c5_1(X39_592) | ~c3_2(X39_592, X40_593) | c7_1(X39_592) | c4_2(X39_592, X40_593) | ~c6_2(X39_592, X77_594) | c4_2(X39_592, X77_594) | c1_1(X39_592) | ~c1_2(X39_592, X40_593) | ~ndr1_1(X39_592) | c8_1(X39_592)))). % 33.45/17.90 tff(c_8946, plain, (![X39_588, X44_66, X40_589]: (~c5_2(X39_588, a152) | c6_1(X39_588) | ~c8_2(X39_588, X44_66) | ~c6_2(X39_588, X44_66) | c5_2(X39_588, X44_66) | ~c5_1(X39_588) | ~c3_2(X39_588, X40_589) | c7_1(X39_588) | c4_2(X39_588, X40_589) | ~c6_2(X39_588, a152) | c4_2(X39_588, a152) | c1_1(X39_588) | ~c1_2(X39_588, X40_589) | ~ndr1_1(X39_588) | c8_1(X39_588)))). % 33.45/17.90 tff(c_8944, plain, (![X39_588, V_4, X40_589]: (c5_2(X39_588, a147) | ~c5_2(X39_588, a152) | c4_2(X39_588, V_4) | c3_2(X39_588, V_4) | ~c5_1(X39_588) | ~c3_2(X39_588, X40_589) | c7_1(X39_588) | c4_2(X39_588, X40_589) | ~c6_2(X39_588, a152) | c4_2(X39_588, a152) | c1_1(X39_588) | ~c1_2(X39_588, X40_589) | ~ndr1_1(X39_588) | c8_1(X39_588)))). % 33.45/17.90 tff(c_8945, plain, (![X39_588, V_4, X40_589]: (~c3_2(X39_588, a147) | ~c5_2(X39_588, a152) | c4_2(X39_588, V_4) | c3_2(X39_588, V_4) | ~c5_1(X39_588) | ~c3_2(X39_588, X40_589) | c7_1(X39_588) | c4_2(X39_588, X40_589) | ~c6_2(X39_588, a152) | c4_2(X39_588, a152) | c1_1(X39_588) | ~c1_2(X39_588, X40_589) | ~ndr1_1(X39_588) | c8_1(X39_588)))). % 33.45/17.90 tff(c_6535, plain, (![X3_371, X4_373, X77_112, V_372]: (c7_1(X3_371) | c4_2(X3_371, X4_373) | ~c1_2(X3_371, X4_373) | ~c6_2(X3_371, X77_112) | c4_2(X3_371, X77_112) | c7_2(X3_371, X77_112) | c5_2(X3_371, a147) | c4_2(X3_371, a152) | ~c5_2(X3_371, a152) | c4_2(X3_371, V_372) | c3_2(X3_371, V_372) | ~c5_1(X3_371) | ~c5_2(X3_371, X4_373) | ~c3_2(X3_371, X4_373) | ~ndr1_1(X3_371)))). % 33.45/17.90 tff(c_8886, plain, (![X39_585, X77_587, X40_586]: (c4_1(X39_585) | c1_2(X39_585, X77_587) | c2_2(X39_585, X77_587) | c7_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585)))). % 33.45/17.90 tff(c_8874, plain, (![X39_585, X40_586, X77_587]: (c4_1(X39_585) | c1_2(X39_585, a152) | c2_2(X39_585, a152) | ~c5_1(X39_585) | ~c3_2(X39_585, X40_586) | c7_1(X39_585) | c4_2(X39_585, X40_586) | ~c6_2(X39_585, X77_587) | c4_2(X39_585, X77_587) | c1_1(X39_585) | ~c1_2(X39_585, X40_586) | ~ndr1_1(X39_585) | c8_1(X39_585) | c7_2(X39_585, X77_587)))). % 33.45/17.90 tff(c_8940, plain, (![X39_588, X40_589]: (c4_1(X39_588) | c1_2(X39_588, a152) | c2_2(X39_588, a152) | ~c5_1(X39_588) | ~c3_2(X39_588, X40_589) | c7_1(X39_588) | c4_2(X39_588, X40_589) | ~c6_2(X39_588, a152) | c4_2(X39_588, a152) | c1_1(X39_588) | ~c1_2(X39_588, X40_589) | ~ndr1_1(X39_588) | c8_1(X39_588)))). % 33.45/17.90 tff(c_8788, plain, (![X39_58, X40_60]: (~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, a152) | c4_2(X39_58, a152) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58) | c7_2(X39_58, a152)))). % 33.45/17.90 tff(c_8569, plain, (![X39_58, X40_60, X77_439]: (c7_2(X39_58, a152) | ~c5_1(X39_58) | ~c3_2(X39_58, X40_60) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_439) | c4_2(X39_58, X77_439) | c1_1(X39_58) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58) | c7_2(X39_58, X77_439)))). % 33.45/17.90 tff(c_7971, plain, (![X158_209, X159_211, V_507, X4_508]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | c5_2(X158_209, a147) | c4_2(X158_209, a152) | ~c5_2(X158_209, a152) | c4_2(X158_209, V_507) | c3_2(X158_209, V_507) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_508) | ~c3_2(X158_209, X4_508) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.90 tff(c_7950, plain, (![X158_209, X159_211, V_503, X4_504]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | ~c3_2(X158_209, a147) | c4_2(X158_209, a152) | ~c5_2(X158_209, a152) | c4_2(X158_209, V_503) | c3_2(X158_209, V_503) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_504) | ~c3_2(X158_209, X4_504) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.90 tff(c_7928, plain, (![X158_209, X159_211, X4_500]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | c7_1(X158_209) | c4_2(X158_209, a152) | ~c1_2(X158_209, a152) | ~c6_2(X158_209, X4_500) | c4_2(X158_209, X4_500) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_500) | ~c3_2(X158_209, X4_500) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.90 tff(c_7387, plain, (![X3_429, X4_431, V_4, X77_430]: (c5_2(X3_429, a147) | c4_2(X3_429, X4_431) | c4_2(X3_429, V_4) | c3_2(X3_429, V_4) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | c7_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_7362, plain, (![X3_429, X77_430, V_4, X4_431]: (c5_2(X3_429, a147) | ~c5_2(X3_429, X77_430) | c4_2(X3_429, V_4) | c3_2(X3_429, V_4) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | c7_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_7389, plain, (![X3_429, X4_431, V_4, X77_430]: (~c3_2(X3_429, a147) | c4_2(X3_429, X4_431) | c4_2(X3_429, V_4) | c3_2(X3_429, V_4) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | c7_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_7364, plain, (![X3_429, X77_430, V_4, X4_431]: (~c3_2(X3_429, a147) | ~c5_2(X3_429, X77_430) | c4_2(X3_429, V_4) | c3_2(X3_429, V_4) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | c7_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_8368, plain, (![X3_12, V_551]: (c4_2(X3_12, V_551) | c3_2(X3_12, V_551) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_8126, plain, (![X3_12, V_518]: (c4_2(X3_12, a152) | c4_2(X3_12, V_518) | c3_2(X3_12, V_518) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | c4_2(X3_12, a263) | ~c6_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_8044, plain, (![X3_12, V_511]: (c4_2(X3_12, a152) | c4_2(X3_12, V_511) | c3_2(X3_12, V_511) | c7_1(X3_12) | c4_2(X3_12, a264) | ~c1_2(X3_12, a264) | ~c6_2(X3_12, a147) | c4_2(X3_12, a147) | ~c5_2(X3_12, a263) | ~c6_1(X3_12) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.90 tff(c_7390, plain, (![X3_429, X44_66, X77_430, X4_431]: (c6_1(X3_429) | ~c8_2(X3_429, X44_66) | ~c6_2(X3_429, X44_66) | c5_2(X3_429, X44_66) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | c7_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.90 tff(c_5958, plain, (![X39_339, W_5, V_4, X40_340]: (~c7_2(X39_339, W_5) | c4_2(X39_339, W_5) | ~c5_2(X39_339, W_5) | c4_2(X39_339, V_4) | c3_2(X39_339, V_4) | c7_1(X39_339) | c4_2(X39_339, X40_340) | ~c6_2(X39_339, a147) | c4_2(X39_339, a147) | c1_1(X39_339) | c5_2(X39_339, X40_340) | ~c1_2(X39_339, X40_340) | ~ndr1_1(X39_339) | c8_1(X39_339)))). % 33.45/17.90 tff(c_8192, plain, (~c6_2(a281, a283))). % 33.45/17.90 tff(c_8191, plain, (~c6_2(a281, a282))). % 33.45/17.90 tff(c_5960, plain, (![X39_339, X77_341, X44_66, X40_340]: (~c5_2(X39_339, X77_341) | c6_1(X39_339) | ~c8_2(X39_339, X44_66) | ~c6_2(X39_339, X44_66) | c5_2(X39_339, X44_66) | c7_1(X39_339) | c4_2(X39_339, X40_340) | ~c6_2(X39_339, X77_341) | c4_2(X39_339, X77_341) | c1_1(X39_339) | c5_2(X39_339, X40_340) | ~c1_2(X39_339, X40_340) | ~ndr1_1(X39_339) | c8_1(X39_339)))). % 33.45/17.90 tff(c_8160, plain, (![X162_215]: (~c4_2(a288, X162_215) | ~c5_2(a288, X162_215) | ~c8_2(a288, X162_215)))). % 33.45/17.90 tff(c_7721, plain, (![X39_449, X77_450]: (c4_1(X39_449) | c1_2(X39_449, X77_450) | c2_2(X39_449, X77_450) | c7_1(X39_449) | c4_2(X39_449, a264) | ~c1_2(X39_449, a264) | ~c6_2(X39_449, X77_450) | c4_2(X39_449, X77_450) | ~c6_1(X39_449) | c1_1(X39_449) | c5_2(X39_449, a263) | ~c1_2(X39_449, a263) | ~ndr1_1(X39_449) | c8_1(X39_449)))). % 33.45/17.90 tff(c_8122, plain, (![X141_191, X77_306, V_518]: (~c5_2(X141_191, X77_306) | c4_2(X141_191, V_518) | c3_2(X141_191, V_518) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, X77_306) | c4_2(X141_191, X77_306) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_8041, plain, (![X141_191, X77_306, V_511]: (~c5_2(X141_191, X77_306) | c4_2(X141_191, V_511) | c3_2(X141_191, V_511) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, X77_306) | c4_2(X141_191, X77_306) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_7471, plain, (![X3_432, X4_433, X77_112]: (~c1_2(X3_432, X4_433) | ~c6_2(X3_432, X77_112) | c4_2(X3_432, X77_112) | c7_2(X3_432, X77_112) | c7_1(X3_432) | c4_2(X3_432, a152) | ~c1_2(X3_432, a152) | ~c6_2(X3_432, X4_433) | c4_2(X3_432, X4_433) | ~c5_1(X3_432) | ~c5_2(X3_432, X4_433) | ~c3_2(X3_432, X4_433) | ~ndr1_1(X3_432)))). % 33.45/17.90 tff(c_8131, plain, (![X141_191, V_518]: (~c5_2(X141_191, a264) | c4_2(X141_191, V_518) | c3_2(X141_191, V_518) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_5603, plain, (![X141_315, W_5, V_4]: (~c7_2(X141_315, W_5) | c4_2(X141_315, W_5) | ~c5_2(X141_315, W_5) | c4_2(X141_315, V_4) | c3_2(X141_315, V_4) | c7_1(X141_315) | c4_2(X141_315, a264) | ~c1_2(X141_315, a264) | ~c6_2(X141_315, a147) | c4_2(X141_315, a147) | ~ndr1_1(X141_315) | c4_2(X141_315, a263) | ~c6_1(X141_315)))). % 33.45/17.90 tff(c_6782, plain, (![X39_58, V_391]: (c4_2(X39_58, a264) | ~c5_2(X39_58, a264) | c4_2(X39_58, V_391) | c3_2(X39_58, V_391) | ~c7_1(X39_58) | ~c6_2(X39_58, a147) | ~c5_2(X39_58, a147) | c5_1(X39_58) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.90 tff(c_8050, plain, (![X141_191, V_511]: (~c5_2(X141_191, a264) | c4_2(X141_191, V_511) | c3_2(X141_191, V_511) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, a147) | c4_2(X141_191, a147) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.90 tff(c_5539, plain, (![X141_313, W_5, V_4]: (~c7_2(X141_313, W_5) | c4_2(X141_313, W_5) | ~c5_2(X141_313, W_5) | c4_2(X141_313, V_4) | c3_2(X141_313, V_4) | c7_1(X141_313) | c4_2(X141_313, a264) | ~c1_2(X141_313, a264) | ~c6_2(X141_313, a147) | c4_2(X141_313, a147) | ~ndr1_1(X141_313) | ~c5_2(X141_313, a263) | ~c6_1(X141_313)))). % 33.45/17.90 tff(c_6541, plain, (![X3_371, X44_66, V_372, X4_373]: (c6_1(X3_371) | ~c8_2(X3_371, X44_66) | ~c6_2(X3_371, X44_66) | c5_2(X3_371, X44_66) | c5_2(X3_371, a147) | c4_2(X3_371, a152) | ~c5_2(X3_371, a152) | c4_2(X3_371, V_372) | c3_2(X3_371, V_372) | ~c5_1(X3_371) | ~c5_2(X3_371, X4_373) | ~c3_2(X3_371, X4_373) | ~ndr1_1(X3_371)))). % 33.45/17.91 tff(c_6610, plain, (![X3_374, X44_66, V_375, X4_376]: (c6_1(X3_374) | ~c8_2(X3_374, X44_66) | ~c6_2(X3_374, X44_66) | c5_2(X3_374, X44_66) | ~c3_2(X3_374, a147) | c4_2(X3_374, a152) | ~c5_2(X3_374, a152) | c4_2(X3_374, V_375) | c3_2(X3_374, V_375) | ~c5_1(X3_374) | ~c5_2(X3_374, X4_376) | ~c3_2(X3_374, X4_376) | ~ndr1_1(X3_374)))). % 33.45/17.91 tff(c_7477, plain, (![X3_432, X44_66, X4_433]: (c6_1(X3_432) | ~c8_2(X3_432, X44_66) | ~c6_2(X3_432, X44_66) | c5_2(X3_432, X44_66) | c7_1(X3_432) | c4_2(X3_432, a152) | ~c1_2(X3_432, a152) | ~c6_2(X3_432, X4_433) | c4_2(X3_432, X4_433) | ~c5_1(X3_432) | ~c5_2(X3_432, X4_433) | ~c3_2(X3_432, X4_433) | ~ndr1_1(X3_432)))). % 33.45/17.91 tff(c_5959, plain, (![X39_339, X77_341, V_4, X40_340]: (~c3_2(X39_339, a147) | ~c5_2(X39_339, X77_341) | c4_2(X39_339, V_4) | c3_2(X39_339, V_4) | c7_1(X39_339) | c4_2(X39_339, X40_340) | ~c6_2(X39_339, X77_341) | c4_2(X39_339, X77_341) | c1_1(X39_339) | c5_2(X39_339, X40_340) | ~c1_2(X39_339, X40_340) | ~ndr1_1(X39_339) | c8_1(X39_339)))). % 33.45/17.91 tff(c_5957, plain, (![X39_339, X77_341, V_4, X40_340]: (c5_2(X39_339, a147) | ~c5_2(X39_339, X77_341) | c4_2(X39_339, V_4) | c3_2(X39_339, V_4) | c7_1(X39_339) | c4_2(X39_339, X40_340) | ~c6_2(X39_339, X77_341) | c4_2(X39_339, X77_341) | c1_1(X39_339) | c5_2(X39_339, X40_340) | ~c1_2(X39_339, X40_340) | ~ndr1_1(X39_339) | c8_1(X39_339)))). % 33.45/17.91 tff(c_5954, plain, (![X39_339, X77_341, X77_112, X40_340]: (~c1_2(X39_339, X77_341) | ~c6_2(X39_339, X77_112) | c4_2(X39_339, X77_112) | c7_2(X39_339, X77_112) | c7_1(X39_339) | c4_2(X39_339, X40_340) | ~c6_2(X39_339, X77_341) | c4_2(X39_339, X77_341) | c1_1(X39_339) | c5_2(X39_339, X40_340) | ~c1_2(X39_339, X40_340) | ~ndr1_1(X39_339) | c8_1(X39_339)))). % 33.45/17.91 tff(c_7380, plain, (![X3_429, X4_431, X77_430]: (c4_1(X3_429) | c1_2(X3_429, X4_431) | c2_2(X3_429, X4_431) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | c7_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.91 tff(c_7355, plain, (![X3_429, X77_430, X4_431]: (c4_1(X3_429) | c1_2(X3_429, X77_430) | c2_2(X3_429, X77_430) | c7_1(X3_429) | c4_2(X3_429, a152) | ~c1_2(X3_429, a152) | ~c6_2(X3_429, X77_430) | c4_2(X3_429, X77_430) | ~c5_1(X3_429) | ~c5_2(X3_429, X4_431) | c7_2(X3_429, X4_431) | ~c3_2(X3_429, X4_431) | ~ndr1_1(X3_429)))). % 33.45/17.91 tff(c_6318, plain, (![X3_361, X4_362, X77_112]: (c7_1(X3_361) | c4_2(X3_361, X4_362) | ~c1_2(X3_361, X4_362) | ~c6_2(X3_361, X77_112) | c4_2(X3_361, X77_112) | c7_2(X3_361, X77_112) | c4_1(X3_361) | c1_2(X3_361, a152) | c2_2(X3_361, a152) | ~c5_1(X3_361) | ~c5_2(X3_361, X4_362) | ~c3_2(X3_361, X4_362) | ~ndr1_1(X3_361)))). % 33.45/17.91 tff(c_7826, plain, (~c6_1(a288))). % 33.45/17.91 tff(c_7807, plain, (~c4_2(a288, a289))). % 33.45/17.91 tff(c_7805, plain, (~c5_2(a288, a289))). % 33.45/17.91 tff(c_7800, plain, (~ndr1_1(a189))). % 33.45/17.91 tff(c_6609, plain, (![X3_374, X4_376, V_4, V_375]: (c4_2(X3_374, X4_376) | c4_2(X3_374, V_4) | c3_2(X3_374, V_4) | ~c3_2(X3_374, a147) | c4_2(X3_374, a152) | ~c5_2(X3_374, a152) | c4_2(X3_374, V_375) | c3_2(X3_374, V_375) | ~c5_1(X3_374) | ~c5_2(X3_374, X4_376) | ~c3_2(X3_374, X4_376) | ~ndr1_1(X3_374)))). % 33.45/17.91 tff(c_6538, plain, (![X3_371, X4_373, V_4, V_372]: (c4_2(X3_371, X4_373) | c4_2(X3_371, V_4) | c3_2(X3_371, V_4) | c5_2(X3_371, a147) | c4_2(X3_371, a152) | ~c5_2(X3_371, a152) | c4_2(X3_371, V_372) | c3_2(X3_371, V_372) | ~c5_1(X3_371) | ~c5_2(X3_371, X4_373) | ~c3_2(X3_371, X4_373) | ~ndr1_1(X3_371)))). % 33.45/17.91 tff(c_7789, plain, (~c8_2(a288, a289))). % 33.45/17.91 tff(c_6119, plain, (![X3_351, X77_352]: (c6_1(X3_351) | c5_2(X3_351, X77_352) | c4_1(X3_351) | ~c8_1(X3_351) | c7_1(X3_351) | c4_2(X3_351, a152) | ~c1_2(X3_351, a152) | ~c6_2(X3_351, X77_352) | c4_2(X3_351, X77_352) | ~c5_1(X3_351) | ~c5_2(X3_351, a152) | ~c3_2(X3_351, a152) | ~ndr1_1(X3_351)))). % 33.45/17.91 tff(c_7474, plain, (![X3_432, V_4, X4_433]: (c5_2(X3_432, a147) | c4_2(X3_432, V_4) | c3_2(X3_432, V_4) | c7_1(X3_432) | c4_2(X3_432, a152) | ~c1_2(X3_432, a152) | ~c6_2(X3_432, X4_433) | c4_2(X3_432, X4_433) | ~c5_1(X3_432) | ~c5_2(X3_432, X4_433) | ~c3_2(X3_432, X4_433) | ~ndr1_1(X3_432)))). % 33.45/17.91 tff(c_7476, plain, (![X3_432, V_4, X4_433]: (~c3_2(X3_432, a147) | c4_2(X3_432, V_4) | c3_2(X3_432, V_4) | c7_1(X3_432) | c4_2(X3_432, a152) | ~c1_2(X3_432, a152) | ~c6_2(X3_432, X4_433) | c4_2(X3_432, X4_433) | ~c5_1(X3_432) | ~c5_2(X3_432, X4_433) | ~c3_2(X3_432, X4_433) | ~ndr1_1(X3_432)))). % 33.45/17.91 tff(c_6600, plain, (![X3_374, X4_376, V_375]: (c4_1(X3_374) | c1_2(X3_374, X4_376) | c2_2(X3_374, X4_376) | ~c3_2(X3_374, a147) | c4_2(X3_374, a152) | ~c5_2(X3_374, a152) | c4_2(X3_374, V_375) | c3_2(X3_374, V_375) | ~c5_1(X3_374) | ~c5_2(X3_374, X4_376) | ~c3_2(X3_374, X4_376) | ~ndr1_1(X3_374)))). % 33.45/17.91 tff(c_6531, plain, (![X3_371, X4_373, V_372]: (c4_1(X3_371) | c1_2(X3_371, X4_373) | c2_2(X3_371, X4_373) | c5_2(X3_371, a147) | c4_2(X3_371, a152) | ~c5_2(X3_371, a152) | c4_2(X3_371, V_372) | c3_2(X3_371, V_372) | ~c5_1(X3_371) | ~c5_2(X3_371, X4_373) | ~c3_2(X3_371, X4_373) | ~ndr1_1(X3_371)))). % 33.45/17.91 tff(c_7467, plain, (![X3_432, X4_433]: (c4_1(X3_432) | c1_2(X3_432, X4_433) | c2_2(X3_432, X4_433) | c7_1(X3_432) | c4_2(X3_432, a152) | ~c1_2(X3_432, a152) | ~c6_2(X3_432, X4_433) | c4_2(X3_432, X4_433) | ~c5_1(X3_432) | ~c5_2(X3_432, X4_433) | ~c3_2(X3_432, X4_433) | ~ndr1_1(X3_432)))). % 33.45/17.91 tff(c_6239, plain, (![X3_12, X77_306]: (c4_1(X3_12) | c1_2(X3_12, X77_306) | c2_2(X3_12, X77_306) | c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5649, plain, (![X39_58, X77_318]: (c7_1(X39_58) | c4_2(X39_58, a264) | ~c1_2(X39_58, a264) | ~c6_2(X39_58, X77_318) | c4_2(X39_58, X77_318) | c7_2(X39_58, X77_318) | ~c6_1(X39_58) | c1_1(X39_58) | c5_2(X39_58, a263) | ~c1_2(X39_58, a263) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.91 tff(c_6810, plain, (![X158_209, X159_211, X4_396]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | c1_2(X158_209, a152) | c2_2(X158_209, a152) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_396) | ~c3_2(X158_209, X4_396) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.91 tff(c_6240, plain, (![X39_58, X77_306, X40_60]: (c4_1(X39_58) | c1_2(X39_58, X77_306) | c2_2(X39_58, X77_306) | c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.91 tff(c_6065, plain, (![X158_209, X159_211, X4_347]: (~c5_2(X158_209, a152) | c6_1(X158_209) | c5_2(X158_209, X159_211) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_347) | c7_2(X158_209, X4_347) | ~c3_2(X158_209, X4_347) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.91 tff(c_5461, plain, (![X3_12, X4_14, X77_306]: (c7_1(X3_12) | c4_2(X3_12, X4_14) | ~c1_2(X3_12, X4_14) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | c7_2(X3_12, X77_306) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5462, plain, (![X3_12, X4_14, X77_306]: (c7_1(X3_12) | c4_2(X3_12, X4_14) | ~c1_2(X3_12, X4_14) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | c7_2(X3_12, X77_306) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_7256, plain, (![X3_12, X4_14]: (c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X4_14) | c4_2(X3_12, X4_14) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12) | c7_2(X3_12, X4_14)))). % 33.45/17.91 tff(c_7416, plain, (c3_1(a256))). % 33.45/17.91 tff(c_7411, plain, (~c5_1(a256))). % 33.45/17.91 tff(c_7409, plain, (c3_1(a237))). % 33.45/17.91 tff(c_7404, plain, (~c5_1(a237))). % 33.45/17.91 tff(c_5460, plain, (![X3_12, X77_306, X4_14]: (c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | c7_2(X3_12, X77_306) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5463, plain, (![X3_12, X4_14, X77_306]: (c7_1(X3_12) | c4_2(X3_12, X4_14) | ~c1_2(X3_12, X4_14) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | c7_2(X3_12, X77_306) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6321, plain, (![X3_361, X4_362, V_4]: (c5_2(X3_361, a147) | c4_2(X3_361, X4_362) | c4_2(X3_361, V_4) | c3_2(X3_361, V_4) | c4_1(X3_361) | c1_2(X3_361, a152) | c2_2(X3_361, a152) | ~c5_1(X3_361) | ~c5_2(X3_361, X4_362) | ~c3_2(X3_361, X4_362) | ~ndr1_1(X3_361)))). % 33.45/17.91 tff(c_6323, plain, (![X3_361, X4_362, V_4]: (~c3_2(X3_361, a147) | c4_2(X3_361, X4_362) | c4_2(X3_361, V_4) | c3_2(X3_361, V_4) | c4_1(X3_361) | c1_2(X3_361, a152) | c2_2(X3_361, a152) | ~c5_1(X3_361) | ~c5_2(X3_361, X4_362) | ~c3_2(X3_361, X4_362) | ~ndr1_1(X3_361)))). % 33.45/17.91 tff(c_7154, plain, (ndr1_1(a288))). % 33.45/17.91 tff(c_7051, plain, (![X39_403, V_285]: (c5_2(X39_403, a147) | c4_2(X39_403, a264) | c3_2(X39_403, V_285) | ~c6_1(X39_403) | c1_1(X39_403) | ~c1_2(X39_403, a263) | ~ndr1_1(X39_403) | c8_1(X39_403) | c4_2(X39_403, V_285)))). % 33.45/17.91 tff(c_7036, plain, (~c8_1(a288))). % 33.45/17.91 tff(c_7032, plain, (![X39_399]: (~c3_2(X39_399, a147) | c3_2(X39_399, a264) | ~c6_1(X39_399) | c1_1(X39_399) | ~c1_2(X39_399, a263) | ~ndr1_1(X39_399) | c8_1(X39_399) | c4_2(X39_399, a264)))). % 33.45/17.91 tff(c_7014, plain, (![X39_399, V_279]: (~c3_2(X39_399, a147) | c4_2(X39_399, a264) | c3_2(X39_399, V_279) | ~c6_1(X39_399) | c1_1(X39_399) | ~c1_2(X39_399, a263) | ~ndr1_1(X39_399) | c8_1(X39_399) | c4_2(X39_399, V_279)))). % 33.45/17.91 tff(c_6241, plain, (![X141_191, X77_306]: (c4_1(X141_191) | c1_2(X141_191, X77_306) | c2_2(X141_191, X77_306) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, X77_306) | c4_2(X141_191, X77_306) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.91 tff(c_6242, plain, (![X141_191, X77_306]: (c4_1(X141_191) | c1_2(X141_191, X77_306) | c2_2(X141_191, X77_306) | c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, X77_306) | c4_2(X141_191, X77_306) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.91 tff(c_6324, plain, (![X3_361, X44_66, X4_362]: (c6_1(X3_361) | ~c8_2(X3_361, X44_66) | ~c6_2(X3_361, X44_66) | c5_2(X3_361, X44_66) | c4_1(X3_361) | c1_2(X3_361, a152) | c2_2(X3_361, a152) | ~c5_1(X3_361) | ~c5_2(X3_361, X4_362) | ~c3_2(X3_361, X4_362) | ~ndr1_1(X3_361)))). % 33.45/17.91 tff(c_6795, plain, (~c3_1(a231))). % 33.45/17.91 tff(c_6787, plain, (![X102_142, X103_144]: (~c5_1(X102_142) | ~c3_1(X102_142) | c3_2(X102_142, X103_144) | ~c6_2(X102_142, X103_144) | ~ndr1_1(X102_142)))). % 33.45/17.91 tff(c_6044, plain, (![X141_191, V_344]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_344) | c3_2(X141_191, V_344) | ~c7_1(X141_191) | ~c6_2(X141_191, a147) | ~c5_2(X141_191, a147) | ~ndr1_1(X141_191) | c5_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.91 tff(c_6042, plain, (![X141_191, V_344]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_344) | c3_2(X141_191, V_344) | ~c7_1(X141_191) | ~c6_2(X141_191, a147) | ~c5_2(X141_191, a147) | ~ndr1_1(X141_191) | c5_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.91 tff(c_6734, plain, (c4_2(a231, a232))). % 33.45/17.91 tff(c_6732, plain, (~c5_2(a231, a232))). % 33.45/17.91 tff(c_6710, plain, (c6_2(a231, a232))). % 33.45/17.91 tff(c_6043, plain, (![X141_191, V_344]: (c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_344) | c3_2(X141_191, V_344) | ~c7_1(X141_191) | ~c6_2(X141_191, a147) | ~c5_2(X141_191, a147) | ~ndr1_1(X141_191) | c5_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.91 tff(c_6707, plain, (ndr1_1(a231))). % 33.45/17.91 tff(c_6706, plain, (c4_1(a231))). % 33.45/17.91 tff(c_6703, plain, (~c8_1(a231))). % 33.45/17.91 tff(c_5492, plain, (![X158_209, X159_211, X4_312]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | ~c4_2(X158_209, a152) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_312) | ~c3_2(X158_209, X4_312) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.91 tff(c_5409, plain, (![X158_209, X159_211, X4_303]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | c7_2(X158_209, a152) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_303) | ~c3_2(X158_209, X4_303) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.91 tff(c_5388, plain, (![X158_209, X159_211, X4_300]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | ~c3_2(X158_209, a152) | ~c5_1(X158_209) | ~c5_2(X158_209, X4_300) | ~c3_2(X158_209, X4_300) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.91 tff(c_5114, plain, (![X3_12, V_258, X4_14]: (~c3_2(X3_12, a147) | c4_2(X3_12, a152) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_258) | c3_2(X3_12, V_258) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5185, plain, (![X3_12, V_264, X4_14]: (c5_2(X3_12, a147) | c4_2(X3_12, a152) | ~c5_2(X3_12, a152) | c4_2(X3_12, V_264) | c3_2(X3_12, V_264) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6483, plain, (~c8_1(a191))). % 33.45/17.91 tff(c_6476, plain, (~c8_2(a191, a192))). % 33.45/17.91 tff(c_6475, plain, (~c6_1(a195))). % 33.45/17.91 tff(c_6471, plain, (~ndr1_1(a195))). % 33.45/17.91 tff(c_6314, plain, (![X3_361, X4_362]: (c1_2(X3_361, X4_362) | c2_2(X3_361, X4_362) | c4_1(X3_361) | c1_2(X3_361, a152) | c2_2(X3_361, a152) | ~c5_1(X3_361) | ~c5_2(X3_361, X4_362) | ~c3_2(X3_361, X4_362) | ~ndr1_1(X3_361)))). % 33.45/17.91 tff(c_6249, plain, (![X3_12, X4_14]: (c4_1(X3_12) | c1_2(X3_12, X4_14) | c2_2(X3_12, X4_14) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6248, plain, (![X3_12, X4_14]: (c4_1(X3_12) | c1_2(X3_12, X4_14) | c2_2(X3_12, X4_14) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6247, plain, (![X3_12, X4_14]: (c4_1(X3_12) | c1_2(X3_12, X4_14) | c2_2(X3_12, X4_14) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6246, plain, (![X3_12, X4_14]: (c4_1(X3_12) | c1_2(X3_12, a152) | c2_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6243, plain, (![X84_120, X85_122]: (c4_1(X84_120) | c1_2(X84_120, X85_122) | c2_2(X84_120, X85_122) | ~c7_1(X84_120) | ~c6_2(X84_120, X85_122) | ~c5_2(X84_120, X85_122) | ~ndr1_1(X84_120) | c5_1(X84_120)))). % 33.45/17.91 tff(c_6245, plain, (![X3_12]: (c4_1(X3_12) | c1_2(X3_12, a152) | c2_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6261, plain, (c2_2(a166, a167))). % 33.45/17.91 tff(c_6260, plain, (c2_2(a191, a192))). % 33.45/17.91 tff(c_6182, plain, (![X21_35, X22_37]: (c4_1(X21_35) | ~c7_2(X21_35, X22_37) | c1_2(X21_35, X22_37) | c2_2(X21_35, X22_37) | ~ndr1_1(X21_35)))). % 33.45/17.91 tff(c_6181, plain, (~c1_2(a191, a192))). % 33.45/17.91 tff(c_6178, plain, (~c5_2(a191, a192))). % 33.45/17.91 tff(c_6145, plain, (c7_2(a191, a192))). % 33.45/17.91 tff(c_5364, plain, (![X158_209, X159_211, X85_294]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | ~c7_1(X158_209) | ~c6_2(X158_209, X85_294) | ~c5_2(X158_209, X85_294) | c5_1(X158_209) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.91 tff(c_6143, plain, (~c3_2(a256, a152))). % 33.45/17.91 tff(c_6142, plain, (~c4_1(a196))). % 33.45/17.91 tff(c_6141, plain, (~c3_2(a237, a152))). % 33.45/17.91 tff(c_5459, plain, (![X3_12, X77_306]: (c7_1(X3_12) | c4_2(X3_12, a152) | ~c1_2(X3_12, a152) | ~c6_2(X3_12, X77_306) | c4_2(X3_12, X77_306) | c7_2(X3_12, X77_306) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_6035, plain, (![X84_120, X85_122, V_344]: (c4_2(X84_120, X85_122) | c4_2(X84_120, V_344) | c3_2(X84_120, V_344) | ~c6_2(X84_120, a147) | ~c5_2(X84_120, a147) | ~c7_1(X84_120) | ~c6_2(X84_120, X85_122) | ~c5_2(X84_120, X85_122) | ~ndr1_1(X84_120) | c5_1(X84_120)))). % 33.45/17.91 tff(c_5063, plain, (![X3_12, X44_254, X4_14]: (~c5_2(X3_12, a152) | c6_1(X3_12) | ~c8_2(X3_12, X44_254) | ~c6_2(X3_12, X44_254) | c5_2(X3_12, X44_254) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5150, plain, (![X84_120, W_260, V_261]: (~c7_2(X84_120, W_260) | c4_2(X84_120, W_260) | ~c5_2(X84_120, W_260) | c4_2(X84_120, V_261) | c3_2(X84_120, V_261) | ~c7_1(X84_120) | ~c6_2(X84_120, a147) | ~c5_2(X84_120, a147) | ~ndr1_1(X84_120) | c5_1(X84_120)))). % 33.45/17.91 tff(c_5997, plain, (ndr1_1(a191))). % 33.45/17.91 tff(c_5995, plain, (c1_1(a191))). % 33.45/17.91 tff(c_5994, plain, (c3_1(a191))). % 33.45/17.91 tff(c_5989, plain, (~c5_1(a191))). % 33.45/17.91 tff(c_5983, plain, (~c6_2(a296, a297))). % 33.45/17.91 tff(c_5985, plain, (~c5_2(a218, a219))). % 33.45/17.91 tff(c_5458, plain, (![X39_58, X40_60, X77_306]: (c7_1(X39_58) | c4_2(X39_58, X40_60) | ~c6_2(X39_58, X77_306) | c4_2(X39_58, X77_306) | c7_2(X39_58, X77_306) | c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.91 tff(c_5884, plain, (c4_2(a218, a219))). % 33.45/17.91 tff(c_5871, plain, (~c1_1(a218))). % 33.45/17.91 tff(c_5864, plain, (~ndr1_1(a173))). % 33.45/17.91 tff(c_5862, plain, (ndr1_1(a218))). % 33.45/17.91 tff(c_5223, plain, (![X158_209, X159_211]: (c6_1(X158_209) | c5_2(X158_209, X159_211) | ~c5_1(X158_209) | ~c5_2(X158_209, a152) | ~c3_2(X158_209, a152) | c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.91 tff(c_5795, plain, (~c6_1(a189))). % 33.45/17.91 tff(c_5116, plain, (![X3_12, X4_14, V_258]: (~c3_2(X3_12, a147) | c4_2(X3_12, X4_14) | c4_2(X3_12, V_258) | c3_2(X3_12, V_258) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5188, plain, (![X3_12, X4_14, V_264]: (c5_2(X3_12, a147) | c4_2(X3_12, X4_14) | c4_2(X3_12, V_264) | c3_2(X3_12, V_264) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5186, plain, (![X3_12, X4_14, V_264]: (c5_2(X3_12, a147) | c4_2(X3_12, X4_14) | c4_2(X3_12, V_264) | c3_2(X3_12, V_264) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5187, plain, (![X3_12, X4_14, V_264]: (c5_2(X3_12, a147) | c4_2(X3_12, X4_14) | c4_2(X3_12, V_264) | c3_2(X3_12, V_264) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5117, plain, (![X3_12, X4_14, V_258]: (~c3_2(X3_12, a147) | c4_2(X3_12, X4_14) | c4_2(X3_12, V_258) | c3_2(X3_12, V_258) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5678, plain, (~c3_2(a171, a172))). % 33.45/17.91 tff(c_5115, plain, (![X3_12, X4_14, V_258]: (~c3_2(X3_12, a147) | c4_2(X3_12, X4_14) | c4_2(X3_12, V_258) | c3_2(X3_12, V_258) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.91 tff(c_5466, plain, (![X141_191, X77_306]: (c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, X77_306) | c4_2(X141_191, X77_306) | c7_2(X141_191, X77_306) | ~ndr1_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5623, plain, (~c6_1(a203))). % 33.45/17.92 tff(c_5619, plain, (~ndr1_1(a203))). % 33.45/17.92 tff(c_5464, plain, (![X141_191, X77_306]: (c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, X77_306) | c4_2(X141_191, X77_306) | c7_2(X141_191, X77_306) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5563, plain, (~c6_1(a296))). % 33.45/17.92 tff(c_5562, plain, (~c6_1(a237))). % 33.45/17.92 tff(c_5561, plain, (c3_1(a218))). % 33.45/17.92 tff(c_5556, plain, (~c5_1(a218))). % 33.45/17.92 tff(c_5465, plain, (![X141_191, X77_306]: (c7_1(X141_191) | c4_2(X141_191, a264) | ~c1_2(X141_191, a264) | ~c6_2(X141_191, X77_306) | c4_2(X141_191, X77_306) | c7_2(X141_191, X77_306) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5066, plain, (![X3_12, X44_254, X4_14]: (c6_1(X3_12) | ~c8_2(X3_12, X44_254) | ~c6_2(X3_12, X44_254) | c5_2(X3_12, X44_254) | ~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_5182, plain, (![X84_120, X85_122, V_264]: (c5_2(X84_120, a147) | c4_2(X84_120, X85_122) | c4_2(X84_120, V_264) | c3_2(X84_120, V_264) | ~c7_1(X84_120) | ~c6_2(X84_120, X85_122) | ~c5_2(X84_120, X85_122) | ~ndr1_1(X84_120) | c5_1(X84_120)))). % 33.45/17.92 tff(c_5475, plain, (~c1_2(a281, a282))). % 33.45/17.92 tff(c_5474, plain, (c3_1(a281))). % 33.45/17.92 tff(c_5431, plain, (![X76_109, X78_113, X77_112]: (c7_1(X76_109) | ~c7_2(X76_109, X78_113) | c4_2(X76_109, X78_113) | ~c1_2(X76_109, X78_113) | ~c6_2(X76_109, X77_112) | c4_2(X76_109, X77_112) | c7_2(X76_109, X77_112) | ~ndr1_1(X76_109)))). % 33.45/17.92 tff(c_5425, plain, (~c5_1(a281))). % 33.45/17.92 tff(c_5424, plain, (c1_1(a208))). % 33.45/17.92 tff(c_5419, plain, (c8_1(a208))). % 33.45/17.92 tff(c_5064, plain, (![X3_12, X44_254, X4_14]: (c6_1(X3_12) | ~c8_2(X3_12, X44_254) | ~c6_2(X3_12, X44_254) | c5_2(X3_12, X44_254) | c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_5065, plain, (![X3_12, X44_254, X4_14]: (c6_1(X3_12) | ~c8_2(X3_12, X44_254) | ~c6_2(X3_12, X44_254) | c5_2(X3_12, X44_254) | ~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_5111, plain, (![X84_120, X85_122, V_258]: (~c3_2(X84_120, a147) | c4_2(X84_120, X85_122) | c4_2(X84_120, V_258) | c3_2(X84_120, V_258) | ~c7_1(X84_120) | ~c6_2(X84_120, X85_122) | ~c5_2(X84_120, X85_122) | ~ndr1_1(X84_120) | c5_1(X84_120)))). % 33.45/17.92 tff(c_5372, plain, (~c7_1(a281))). % 33.45/17.92 tff(c_5060, plain, (![X84_120, X44_254, X85_122]: (c6_1(X84_120) | ~c8_2(X84_120, X44_254) | ~c6_2(X84_120, X44_254) | c5_2(X84_120, X44_254) | ~c7_1(X84_120) | ~c6_2(X84_120, X85_122) | ~c5_2(X84_120, X85_122) | ~ndr1_1(X84_120) | c5_1(X84_120)))). % 33.45/17.92 tff(c_5350, plain, (~c6_1(a274))). % 33.45/17.92 tff(c_5346, plain, (~ndr1_1(a274))). % 33.45/17.92 tff(c_5184, plain, (![X3_12, V_264]: (c5_2(X3_12, a147) | c4_2(X3_12, a152) | c4_2(X3_12, V_264) | c3_2(X3_12, V_264) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_5113, plain, (![X3_12, V_258]: (~c3_2(X3_12, a147) | c4_2(X3_12, a152) | c4_2(X3_12, V_258) | c3_2(X3_12, V_258) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_5342, plain, (![X141_191, V_285]: (c5_2(X141_191, a147) | c4_2(X141_191, a264) | c4_2(X141_191, V_285) | c3_2(X141_191, V_285) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5120, plain, (![X141_191, V_258]: (~c3_2(X141_191, a147) | c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_258) | c3_2(X141_191, V_258) | ~ndr1_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5310, plain, (![X141_191, V_279]: (~c3_2(X141_191, a147) | c4_2(X141_191, a264) | c4_2(X141_191, V_279) | c3_2(X141_191, V_279) | ~ndr1_1(X141_191) | ~c5_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5191, plain, (![X141_191, V_264]: (c5_2(X141_191, a147) | c4_2(X141_191, a264) | ~c5_2(X141_191, a264) | c4_2(X141_191, V_264) | c3_2(X141_191, V_264) | ~ndr1_1(X141_191) | ~c7_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5276, plain, (![X141_191]: (~c3_2(X141_191, a147) | c3_2(X141_191, a264) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191) | c4_2(X141_191, a264)))). % 33.45/17.92 tff(c_5261, plain, (![X141_191, V_272]: (~c3_2(X141_191, a147) | c4_2(X141_191, a264) | c4_2(X141_191, V_272) | c3_2(X141_191, V_272) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5241, plain, (![X141_191, V_268]: (c5_2(X141_191, a147) | c4_2(X141_191, a264) | c4_2(X141_191, V_268) | c3_2(X141_191, V_268) | ~ndr1_1(X141_191) | c4_2(X141_191, a263) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_5231, plain, (~c3_2(a281, a152))). % 33.45/17.92 tff(c_5062, plain, (![X3_12, X44_254]: (c6_1(X3_12) | ~c8_2(X3_12, X44_254) | ~c6_2(X3_12, X44_254) | c5_2(X3_12, X44_254) | ~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_5156, plain, (![U_1, W_5, V_4]: (c5_2(U_1, a147) | ~c7_2(U_1, W_5) | c4_2(U_1, W_5) | ~c5_2(U_1, W_5) | c4_2(U_1, V_4) | c3_2(U_1, V_4) | ~ndr1_1(U_1)))). % 33.45/17.92 tff(c_5135, plain, (![U_1, W_5, V_4]: (~c7_2(U_1, a147) | ~c7_2(U_1, W_5) | c4_2(U_1, W_5) | ~c5_2(U_1, W_5) | c4_2(U_1, V_4) | c3_2(U_1, V_4) | ~ndr1_1(U_1)))). % 33.45/17.92 tff(c_5085, plain, (![U_1, W_5, V_4]: (~c3_2(U_1, a147) | ~c7_2(U_1, W_5) | c4_2(U_1, W_5) | ~c5_2(U_1, W_5) | c4_2(U_1, V_4) | c3_2(U_1, V_4) | ~ndr1_1(U_1)))). % 33.45/17.92 tff(c_5080, plain, (![X11_22]: (~c6_2(a160, X11_22)))). % 33.45/17.92 tff(c_5077, plain, (~c5_2(a281, a282))). % 33.45/17.92 tff(c_5076, plain, (~c5_2(a166, a167))). % 33.45/17.92 tff(c_5034, plain, (![X43_63, X45_67, X44_66]: (~c7_2(X43_63, X45_67) | ~c5_2(X43_63, X45_67) | c6_1(X43_63) | ~c8_2(X43_63, X44_66) | ~c6_2(X43_63, X44_66) | c5_2(X43_63, X44_66) | ~ndr1_1(X43_63)))). % 33.45/17.92 tff(c_5032, plain, (~c3_2(a237, a238))). % 33.45/17.92 tff(c_5001, plain, (~c7_2(a237, a238))). % 33.45/17.92 tff(c_4997, plain, (~c1_2(a237, a238))). % 33.45/17.92 tff(c_4995, plain, (c2_2(a237, a238))). % 33.45/17.92 tff(c_4972, plain, (~c6_1(a173))). % 33.45/17.92 tff(c_4971, plain, (~c7_1(a237))). % 33.45/17.92 tff(c_4969, plain, (c1_1(a237))). % 33.45/17.92 tff(c_4962, plain, (ndr1_1(a237))). % 33.45/17.92 tff(c_4960, plain, (~c3_1(a174))). % 33.45/17.92 tff(c_4957, plain, (~c6_1(a253))). % 33.45/17.92 tff(c_4953, plain, (~ndr1_1(a253))). % 33.45/17.92 tff(c_4950, plain, (c2_2(a160, a161))). % 33.45/17.92 tff(c_4940, plain, (c8_2(a160, a161))). % 33.45/17.92 tff(c_4935, plain, (~c5_2(a160, a161))). % 33.45/17.92 tff(c_4926, plain, (~c6_1(a256))). % 33.45/17.92 tff(c_4906, plain, (![X129_175]: (~c4_2(a256, X129_175) | ~c5_2(a256, X129_175) | ~c3_2(a256, X129_175)))). % 33.45/17.92 tff(c_4900, plain, (~c6_1(a160))). % 33.45/17.92 tff(c_4893, plain, (c3_1(a226))). % 33.45/17.92 tff(c_4885, plain, (![X167_221]: (c5_1(X167_221) | c4_1(X167_221) | c3_1(X167_221)))). % 33.45/17.92 tff(c_4877, plain, (ndr1_1(a160))). % 33.45/17.92 tff(c_4826, plain, (![X39_243]: (c5_2(X39_243, a264) | ~c6_1(X39_243) | c1_1(X39_243) | c5_2(X39_243, a263) | ~c1_2(X39_243, a263) | ~ndr1_1(X39_243) | c8_1(X39_243)))). % 33.45/17.92 tff(c_4873, plain, (![X39_247]: (c1_2(X39_247, a264) | ~c6_1(X39_247) | c1_1(X39_247) | ~c1_2(X39_247, a263) | ~ndr1_1(X39_247) | c8_1(X39_247)))). % 33.45/17.92 tff(c_4866, plain, (~c5_2(a256, a257))). % 33.45/17.92 tff(c_4842, plain, (![X84_120, X85_122]: (~c7_1(X84_120) | ~c6_2(X84_120, X85_122) | ~c5_2(X84_120, X85_122) | c7_2(X84_120, X85_122) | ~ndr1_1(X84_120) | c5_1(X84_120)))). % 33.45/17.92 tff(c_4809, plain, (![X39_58, X40_60]: (c1_1(X39_58) | c5_2(X39_58, X40_60) | ~c1_2(X39_58, X40_60) | c7_2(X39_58, X40_60) | ~ndr1_1(X39_58) | c8_1(X39_58)))). % 33.45/17.92 tff(c_4768, plain, (![X3_12]: (~c5_1(X3_12) | ~c5_2(X3_12, a152) | ~c3_2(X3_12, a152) | ~ndr1_1(X3_12) | c7_2(X3_12, a152)))). % 33.45/17.92 tff(c_4798, plain, (c1_1(a203))). % 33.45/17.92 tff(c_4793, plain, (c8_1(a203))). % 33.45/17.92 tff(c_4755, plain, (![X3_12, X4_14]: (c7_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_4748, plain, (c6_1(a200))). % 33.45/17.92 tff(c_4747, plain, (c4_1(a203))). % 33.45/17.92 tff(c_4746, plain, (~c8_1(a166))). % 33.45/17.92 tff(c_4738, plain, (![X158_209, X159_211]: (c4_1(X158_209) | ~c6_2(X158_209, X159_211) | ~c7_2(X158_209, X159_211) | c8_2(X158_209, X159_211) | ~ndr1_1(X158_209) | ~c8_1(X158_209)))). % 33.45/17.92 tff(c_4712, plain, (![X3_12, X4_14]: (~c3_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_4710, plain, (~c3_2(a256, a257))). % 33.45/17.92 tff(c_4708, plain, (~c3_2(a296, a297))). % 33.45/17.92 tff(c_4684, plain, (![X3_12, X4_14]: (~c4_2(X3_12, a152) | ~c5_1(X3_12) | ~c5_2(X3_12, X4_14) | c7_2(X3_12, X4_14) | ~c3_2(X3_12, X4_14) | ~ndr1_1(X3_12)))). % 33.45/17.92 tff(c_4682, plain, (~c1_1(a200))). % 33.45/17.92 tff(c_4607, plain, (~c7_1(a274))). % 33.45/17.92 tff(c_4593, plain, (~c6_1(a226))). % 33.45/17.92 tff(c_4589, plain, (~ndr1_1(a226))). % 33.45/17.92 tff(c_4575, plain, (~c6_1(a186))). % 33.45/17.92 tff(c_4571, plain, (~ndr1_1(a186))). % 33.45/17.92 tff(c_4537, plain, (~c6_1(a277))). % 33.45/17.92 tff(c_4533, plain, (~ndr1_1(a277))). % 33.45/17.92 tff(c_4519, plain, (~c2_2(a296, a297))). % 33.45/17.92 tff(c_4508, plain, (~c1_2(a171, a172))). % 33.45/17.92 tff(c_4503, plain, (![X141_191]: (c4_2(X141_191, a263) | c7_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4500, plain, (c5_2(a296, a297))). % 33.45/17.92 tff(c_4495, plain, (![X141_191]: (c4_2(X141_191, a263) | c1_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4493, plain, (c2_2(a171, a172))). % 33.45/17.92 tff(c_4489, plain, (![X141_191]: (~c7_2(X141_191, a263) | c1_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4486, plain, (![X141_191]: (~c7_2(X141_191, a263) | c5_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4483, plain, (![X141_191]: (~c5_2(X141_191, a263) | c7_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4479, plain, (![X141_191]: (c4_2(X141_191, a263) | c5_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4475, plain, (![X141_191]: (~c5_2(X141_191, a263) | c5_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4472, plain, (![X141_191]: (~c5_2(X141_191, a263) | c1_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4467, plain, (c5_2(a171, a172))). % 33.45/17.92 tff(c_4463, plain, (![X141_191]: (~c7_2(X141_191, a263) | c7_2(X141_191, a264) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4460, plain, (~c7_2(a256, a257))). % 33.45/17.92 tff(c_4458, plain, (~c1_2(a256, a257))). % 33.45/17.92 tff(c_4456, plain, (~c7_2(a296, a297))). % 33.45/17.92 tff(c_4454, plain, (~c7_1(a253))). % 33.45/17.92 tff(c_4445, plain, (~c8_1(a253))). % 33.45/17.92 tff(c_4435, plain, (~c7_1(a296))). % 33.45/17.92 tff(c_4433, plain, (ndr1_1(a296))). % 33.45/17.92 tff(c_4431, plain, (c4_1(a171))). % 33.45/17.92 tff(c_4422, plain, (![X157_208]: (c6_1(X157_208) | ~c8_1(X157_208) | c1_1(X157_208)))). % 33.45/17.92 tff(c_4410, plain, (ndr1_1(a171))). % 33.45/17.92 tff(c_4407, plain, (ndr1_1(a256))). % 33.45/17.92 tff(c_4404, plain, (c1_1(a256))). % 33.45/17.92 tff(c_4402, plain, (~c6_1(a235))). % 33.45/17.92 tff(c_4398, plain, (~ndr1_1(a235))). % 33.45/17.92 tff(c_4397, plain, (~c2_1(a171))). % 33.45/17.92 tff(c_4394, plain, (~c2_1(a166))). % 33.45/17.92 tff(c_4389, plain, (![X143_193]: (~c7_1(X143_193) | ~c2_1(X143_193)))). % 33.45/17.92 tff(c_4288, plain, (~c8_2(a166, a167))). % 33.45/17.92 tff(c_4283, plain, (~c1_2(a281, a283))). % 33.45/17.92 tff(c_4279, plain, (c5_1(a157))). % 33.45/17.92 tff(c_4278, plain, (c8_2(a281, a283))). % 33.45/17.92 tff(c_4271, plain, (c7_2(a166, a167))). % 33.45/17.92 tff(c_4265, plain, (c2_2(a281, a282))). % 33.45/17.92 tff(c_4254, plain, (c7_2(a281, a282))). % 33.45/17.92 tff(c_4250, plain, (~c3_2(a166, a167))). % 33.45/17.92 tff(c_4241, plain, (c8_2(a281, a282))). % 33.45/17.92 tff(c_4225, plain, (~c7_1(a155))). % 33.45/17.92 tff(c_4223, plain, (~c4_1(a157))). % 33.45/17.92 tff(c_4214, plain, (![X141_191]: (ndr1_1(X141_191) | ~c6_1(X141_191)))). % 33.45/17.92 tff(c_4204, plain, (ndr1_1(a281))). % 33.45/17.92 tff(c_4198, plain, (~c5_1(a226))). % 33.45/17.92 tff(c_4174, plain, (ndr1_1(a166))). % 33.45/17.92 tff(c_4167, plain, (c1_1(a166))). % 33.45/17.92 tff(c_4160, plain, (c7_1(a166))). % 33.45/17.92 tff(c_4155, plain, (~c1_1(a235))). % 33.45/17.92 tff(c_4139, plain, (~c7_1(a186))). % 33.45/17.92 tff(c_4136, plain, (~c3_1(a235))). % 33.45/17.92 tff(c_4127, plain, (c1_1(a186))). % 33.45/17.92 tff(c_4108, plain, (c7_0)). % 33.45/17.92 tff(c_4105, plain, (~c7_1(a170))). % 33.45/17.92 tff(c_4087, plain, (~c6_0)). % 33.45/17.92 tff(c_4083, plain, (c8_0)). % 33.45/17.92 tff(c_4077, plain, (c3_0)). % 33.45/17.92 tff(c_4076, plain, (~c2_0)). % 33.45/17.92 tff(c_4069, plain, (~c4_0)). % 33.45/17.92 tff(c_4067, plain, (c5_0)). % 33.45/17.92 tff(c_4066, plain, (c1_0)). % 33.45/17.92 tff(c_2734, plain, (ndr1_0)). % 33.45/17.92 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.45/17.92 %------------------------------------------------------------------------------