Beagle---0.9.52.CSA-Ass.s

%------------------------------------------------------------------------------
% File     : Beagle---0.9.52
% Problem  : SYN426+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 : n016.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:32 PM UTC 2025

% Result   : CounterSatisfiable 33.31s 13.87s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12  % Problem  : SYN426+1 : TPTP v9.0.0. Released v2.1.0.
% 0.12/0.13  % Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/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.35  % Computer : n016.cluster.edu
% 0.14/0.35  % Model    : x86_64 x86_64
% 0.14/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35  % Memory   : 8042.1875MB
% 0.14/0.35  % 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:25:08 EDT 2025
% 0.14/0.35  % CPUTime  : 
% 33.31/13.86  
% 33.31/13.87  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.31/13.87  
% 33.31/13.87  % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.31/13.88  %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ndr1_0 > c9_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > c10_0 > a430 > a429 > a428 > a427 > a426 > a425 > a424 > a423 > a422 > a421 > a420 > a419 > a418 > a417 > a416 > a415 > a414 > a413 > a412 > a411 > a410 > a409 > a408 > a407 > a406 > a405 > a404 > a403 > a402 > a401 > a400 > a399 > a398 > a397 > a396 > a395 > a394 > a393 > a392 > a391 > a390 > a389 > a388 > a387 > a386 > a385 > a384 > a383 > a382 > a381 > a380 > a379 > a378 > a377 > a376 > a375 > a374 > a373 > a372 > a371 > a370 > a369 > a368 > a367 > a366 > a365 > a364 > a363 > a362 > a361 > a360 > a359 > a358 > a357 > a356 > a355 > a354 > a353 > a352 > a351 > a350 > a349 > a348 > a347 > a346 > a345 > a344 > a343 > a342 > a341 > a340 > a339 > a338 > a337 > a336 > a335 > a334 > a333 > a332 > a331 > a330 > a329 > a328 > a327 > a326 > a325 > a324 > a323 > a322 > a321 > a320 > a319 > a318 > a317 > a316 > a315 > a314 > a313 > a312 > a311 > a310 > a309 > a308 > a307 > a306 > a305 > a304 > a303 > a302 > a301 > a300 > a299 > a298 > 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
% 33.31/13.88  
% 33.31/13.88  %Foreground sorts:
% 33.31/13.88  
% 33.31/13.88  
% 33.31/13.88  %Background operators:
% 33.31/13.88  
% 33.31/13.88  
% 33.31/13.88  %Foreground operators:
% 33.31/13.88  tff(a430, type, a430: $i).
% 33.31/13.88  tff(a230, type, a230: $i).
% 33.31/13.88  tff(a229, type, a229: $i).
% 33.31/13.88  tff(a254, type, a254: $i).
% 33.31/13.88  tff(c7_0, type, c7_0: $o).
% 33.31/13.88  tff(a242, type, a242: $i).
% 33.31/13.88  tff(a323, type, a323: $i).
% 33.31/13.88  tff(a421, type, a421: $i).
% 33.31/13.88  tff(a316, type, a316: $i).
% 33.31/13.88  tff(a389, type, a389: $i).
% 33.31/13.88  tff(a347, type, a347: $i).
% 33.31/13.88  tff(a281, type, a281: $i).
% 33.31/13.88  tff(a257, type, a257: $i).
% 33.31/13.88  tff(a322, type, a322: $i).
% 33.31/13.88  tff(a313, type, a313: $i).
% 33.31/13.88  tff(a292, type, a292: $i).
% 33.31/13.88  tff(a336, type, a336: $i).
% 33.31/13.88  tff(a422, type, a422: $i).
% 33.31/13.88  tff(c4_0, type, c4_0: $o).
% 33.31/13.88  tff(a335, type, a335: $i).
% 33.31/13.88  tff(a280, type, a280: $i).
% 33.31/13.88  tff(a326, type, a326: $i).
% 33.31/13.88  tff(a297, type, a297: $i).
% 33.31/13.88  tff(a290, type, a290: $i).
% 33.31/13.88  tff(a359, type, a359: $i).
% 33.31/13.88  tff(a249, type, a249: $i).
% 33.31/13.88  tff(c3_0, type, c3_0: $o).
% 33.31/13.88  tff(a386, type, a386: $i).
% 33.31/13.88  tff(a399, type, a399: $i).
% 33.31/13.88  tff(a423, type, a423: $i).
% 33.31/13.88  tff(a338, type, a338: $i).
% 33.31/13.88  tff(a398, type, a398: $i).
% 33.31/13.88  tff(c1_2, type, c1_2: ($i * $i) > $o).
% 33.31/13.88  tff(a334, type, a334: $i).
% 33.31/13.88  tff(a384, type, a384: $i).
% 33.31/13.88  tff(a373, type, a373: $i).
% 33.31/13.88  tff(a387, type, a387: $i).
% 33.31/13.88  tff(a272, type, a272: $i).
% 33.31/13.88  tff(a309, type, a309: $i).
% 33.31/13.88  tff(a302, type, a302: $i).
% 33.31/13.88  tff(a337, type, a337: $i).
% 33.31/13.88  tff(a306, type, a306: $i).
% 33.31/13.88  tff(a368, type, a368: $i).
% 33.31/13.88  tff(a233, type, a233: $i).
% 33.31/13.88  tff(a367, type, a367: $i).
% 33.31/13.88  tff(a417, type, a417: $i).
% 33.31/13.88  tff(a320, type, a320: $i).
% 33.31/13.88  tff(a301, type, a301: $i).
% 33.31/13.88  tff(a401, type, a401: $i).
% 33.31/13.88  tff(a354, type, a354: $i).
% 33.31/13.88  tff(a264, type, a264: $i).
% 33.31/13.88  tff(a284, type, a284: $i).
% 33.31/13.88  tff(a295, type, a295: $i).
% 33.31/13.88  tff(a310, type, a310: $i).
% 33.31/13.88  tff(a407, type, a407: $i).
% 33.31/13.88  tff(a285, type, a285: $i).
% 33.31/13.88  tff(a348, type, a348: $i).
% 33.31/13.88  tff(a266, type, a266: $i).
% 33.31/13.88  tff(a232, type, a232: $i).
% 33.31/13.88  tff(a341, type, a341: $i).
% 33.31/13.88  tff(a380, type, a380: $i).
% 33.31/13.88  tff(a361, type, a361: $i).
% 33.31/13.88  tff(a342, type, a342: $i).
% 33.31/13.88  tff(c8_0, type, c8_0: $o).
% 33.31/13.88  tff(a311, type, a311: $i).
% 33.31/13.88  tff(a391, type, a391: $i).
% 33.31/13.88  tff(a355, type, a355: $i).
% 33.31/13.88  tff(a269, type, a269: $i).
% 33.31/13.88  tff(a286, type, a286: $i).
% 33.31/13.88  tff(a237, type, a237: $i).
% 33.31/13.88  tff(a330, type, a330: $i).
% 33.31/13.88  tff(a248, type, a248: $i).
% 33.31/13.88  tff(a418, type, a418: $i).
% 33.31/13.88  tff(a291, type, a291: $i).
% 33.31/13.88  tff(a314, type, a314: $i).
% 33.31/13.88  tff(a413, type, a413: $i).
% 33.31/13.88  tff(a405, type, a405: $i).
% 33.31/13.88  tff(a283, type, a283: $i).
% 33.31/13.88  tff(a238, type, a238: $i).
% 33.31/13.88  tff(a397, type, a397: $i).
% 33.31/13.88  tff(a402, type, a402: $i).
% 33.31/13.88  tff(a228, type, a228: $i).
% 33.31/13.88  tff(a370, type, a370: $i).
% 33.31/13.88  tff(a293, type, a293: $i).
% 33.31/13.88  tff(a294, type, a294: $i).
% 33.31/13.88  tff(a321, type, a321: $i).
% 33.31/13.88  tff(a318, type, a318: $i).
% 33.31/13.88  tff(c5_0, type, c5_0: $o).
% 33.31/13.88  tff(a414, type, a414: $i).
% 33.31/13.88  tff(a366, type, a366: $i).
% 33.31/13.88  tff(a396, type, a396: $i).
% 33.31/13.88  tff(a268, type, a268: $i).
% 33.31/13.88  tff(a261, type, a261: $i).
% 33.31/13.88  tff(a308, type, a308: $i).
% 33.31/13.88  tff(a329, type, a329: $i).
% 33.31/13.88  tff(a245, type, a245: $i).
% 33.31/13.88  tff(c6_0, type, c6_0: $o).
% 33.31/13.88  tff(a235, type, a235: $i).
% 33.31/13.88  tff(c8_2, type, c8_2: ($i * $i) > $o).
% 33.31/13.88  tff(a270, type, a270: $i).
% 33.31/13.88  tff(a278, type, a278: $i).
% 33.31/13.88  tff(a222, type, a222: $i).
% 33.31/13.88  tff(a220, type, a220: $i).
% 33.31/13.88  tff(a410, type, a410: $i).
% 33.31/13.88  tff(a388, type, a388: $i).
% 33.31/13.88  tff(a298, type, a298: $i).
% 33.31/13.88  tff(a353, type, a353: $i).
% 33.31/13.88  tff(a227, type, a227: $i).
% 33.31/13.88  tff(a265, type, a265: $i).
% 33.31/13.88  tff(a374, type, a374: $i).
% 33.31/13.88  tff(a251, type, a251: $i).
% 33.31/13.88  tff(a358, type, a358: $i).
% 33.31/13.88  tff(a236, type, a236: $i).
% 33.31/13.88  tff(a304, type, a304: $i).
% 33.31/13.88  tff(a343, type, a343: $i).
% 33.31/13.88  tff(a275, type, a275: $i).
% 33.31/13.88  tff(a246, type, a246: $i).
% 33.31/13.88  tff(a218, type, a218: $i).
% 33.31/13.88  tff(a357, type, a357: $i).
% 33.31/13.88  tff(a282, type, a282: $i).
% 33.31/13.88  tff(a273, type, a273: $i).
% 33.31/13.88  tff(c1_0, type, c1_0: $o).
% 33.31/13.88  tff(a240, type, a240: $i).
% 33.31/13.88  tff(a331, type, a331: $i).
% 33.31/13.88  tff(c8_1, type, c8_1: $i > $o).
% 33.31/13.88  tff(a427, type, a427: $i).
% 33.31/13.88  tff(a371, type, a371: $i).
% 33.31/13.88  tff(a234, type, a234: $i).
% 33.31/13.88  tff(a250, type, a250: $i).
% 33.31/13.88  tff(a267, type, a267: $i).
% 33.31/13.88  tff(a393, type, a393: $i).
% 33.31/13.88  tff(c2_1, type, c2_1: $i > $o).
% 33.31/13.88  tff(a219, type, a219: $i).
% 33.31/13.88  tff(a392, type, a392: $i).
% 33.31/13.88  tff(a258, type, a258: $i).
% 33.31/13.88  tff(ndr1_1, type, ndr1_1: $i > $o).
% 33.31/13.88  tff(c2_0, type, c2_0: $o).
% 33.31/13.88  tff(c4_1, type, c4_1: $i > $o).
% 33.31/13.88  tff(a277, type, a277: $i).
% 33.31/13.88  tff(a333, type, a333: $i).
% 33.31/13.88  tff(a382, type, a382: $i).
% 33.31/13.88  tff(a274, type, a274: $i).
% 33.31/13.88  tff(a420, type, a420: $i).
% 33.31/13.88  tff(a383, type, a383: $i).
% 33.31/13.88  tff(a345, type, a345: $i).
% 33.31/13.88  tff(a408, type, a408: $i).
% 33.31/13.88  tff(a363, type, a363: $i).
% 33.31/13.88  tff(a416, type, a416: $i).
% 33.31/13.88  tff(a223, type, a223: $i).
% 33.31/13.88  tff(a271, type, a271: $i).
% 33.31/13.88  tff(a252, type, a252: $i).
% 33.31/13.88  tff(a352, type, a352: $i).
% 33.31/13.88  tff(a327, type, a327: $i).
% 33.31/13.88  tff(a390, type, a390: $i).
% 33.31/13.88  tff(c9_1, type, c9_1: $i > $o).
% 33.31/13.88  tff(c10_1, type, c10_1: $i > $o).
% 33.31/13.88  tff(a243, type, a243: $i).
% 33.31/13.88  tff(c10_0, type, c10_0: $o).
% 33.31/13.88  tff(a425, type, a425: $i).
% 33.31/13.88  tff(c6_2, type, c6_2: ($i * $i) > $o).
% 33.31/13.88  tff(a400, type, a400: $i).
% 33.31/13.88  tff(a260, type, a260: $i).
% 33.31/13.88  tff(a263, type, a263: $i).
% 33.31/13.88  tff(a364, type, a364: $i).
% 33.31/13.88  tff(a381, type, a381: $i).
% 33.31/13.88  tff(a429, type, a429: $i).
% 33.31/13.88  tff(a289, type, a289: $i).
% 33.31/13.88  tff(a411, type, a411: $i).
% 33.31/13.88  tff(a226, type, a226: $i).
% 33.31/13.88  tff(ndr1_0, type, ndr1_0: $o).
% 33.31/13.88  tff(a288, type, a288: $i).
% 33.31/13.88  tff(a300, type, a300: $i).
% 33.31/13.88  tff(a287, type, a287: $i).
% 33.31/13.88  tff(a375, type, a375: $i).
% 33.31/13.88  tff(a344, type, a344: $i).
% 33.31/13.88  tff(a351, type, a351: $i).
% 33.31/13.88  tff(a241, type, a241: $i).
% 33.31/13.88  tff(a231, type, a231: $i).
% 33.31/13.88  tff(c9_2, type, c9_2: ($i * $i) > $o).
% 33.31/13.88  tff(a224, type, a224: $i).
% 33.31/13.88  tff(a395, type, a395: $i).
% 33.31/13.88  tff(c10_2, type, c10_2: ($i * $i) > $o).
% 33.31/13.88  tff(a255, type, a255: $i).
% 33.31/13.88  tff(a424, type, a424: $i).
% 33.31/13.88  tff(a317, type, a317: $i).
% 33.31/13.88  tff(a349, type, a349: $i).
% 33.31/13.88  tff(a253, type, a253: $i).
% 33.31/13.88  tff(a426, type, a426: $i).
% 33.31/13.88  tff(a324, type, a324: $i).
% 33.31/13.88  tff(a403, type, a403: $i).
% 33.31/13.88  tff(a419, type, a419: $i).
% 33.31/13.88  tff(c1_1, type, c1_1: $i > $o).
% 33.31/13.88  tff(a369, type, a369: $i).
% 33.31/13.88  tff(a378, type, a378: $i).
% 33.31/13.88  tff(a415, type, a415: $i).
% 33.31/13.88  tff(a409, type, a409: $i).
% 33.31/13.88  tff(a385, type, a385: $i).
% 33.31/13.88  tff(c5_2, type, c5_2: ($i * $i) > $o).
% 33.31/13.88  tff(a340, type, a340: $i).
% 33.31/13.88  tff(a225, type, a225: $i).
% 33.31/13.88  tff(a299, type, a299: $i).
% 33.31/13.88  tff(c9_0, type, c9_0: $o).
% 33.31/13.88  tff(a394, type, a394: $i).
% 33.31/13.88  tff(c7_1, type, c7_1: $i > $o).
% 33.31/13.88  tff(a362, type, a362: $i).
% 33.31/13.88  tff(c6_1, type, c6_1: $i > $o).
% 33.31/13.88  tff(a315, type, a315: $i).
% 33.31/13.88  tff(c4_2, type, c4_2: ($i * $i) > $o).
% 33.31/13.88  tff(a259, type, a259: $i).
% 33.31/13.88  tff(a276, type, a276: $i).
% 33.31/13.88  tff(a406, type, a406: $i).
% 33.31/13.88  tff(a262, type, a262: $i).
% 33.31/13.88  tff(a239, type, a239: $i).
% 33.31/13.88  tff(a319, type, a319: $i).
% 33.31/13.88  tff(a376, type, a376: $i).
% 33.31/13.88  tff(a328, type, a328: $i).
% 33.31/13.88  tff(a332, type, a332: $i).
% 33.31/13.88  tff(a428, type, a428: $i).
% 33.31/13.88  tff(a247, type, a247: $i).
% 33.31/13.88  tff(a279, type, a279: $i).
% 33.31/13.88  tff(a296, type, a296: $i).
% 33.31/13.88  tff(c5_1, type, c5_1: $i > $o).
% 33.31/13.88  tff(a221, type, a221: $i).
% 33.31/13.88  tff(a346, type, a346: $i).
% 33.31/13.88  tff(c7_2, type, c7_2: ($i * $i) > $o).
% 33.31/13.88  tff(c3_2, type, c3_2: ($i * $i) > $o).
% 33.31/13.88  tff(a350, type, a350: $i).
% 33.31/13.88  tff(a404, type, a404: $i).
% 33.31/13.88  tff(a412, type, a412: $i).
% 33.31/13.88  tff(c2_2, type, c2_2: ($i * $i) > $o).
% 33.31/13.88  tff(a365, type, a365: $i).
% 33.31/13.88  tff(a325, type, a325: $i).
% 33.31/13.88  tff(a360, type, a360: $i).
% 33.31/13.88  tff(a372, type, a372: $i).
% 33.31/13.88  tff(a305, type, a305: $i).
% 33.31/13.88  tff(a312, type, a312: $i).
% 33.31/13.88  tff(a244, type, a244: $i).
% 33.31/13.88  tff(a307, type, a307: $i).
% 33.31/13.88  tff(a303, type, a303: $i).
% 33.31/13.88  tff(a339, type, a339: $i).
% 33.31/13.88  tff(a379, type, a379: $i).
% 33.31/13.88  tff(a377, type, a377: $i).
% 33.31/13.88  tff(a356, type, a356: $i).
% 33.31/13.88  tff(c3_1, type, c3_1: $i > $o).
% 33.31/13.88  tff(a256, type, a256: $i).
% 33.31/13.88  
% 33.31/13.88  %Saturated clause set:
% 33.31/13.88  tff(c_18727, plain, (![X161_216, X47_688]: (c2_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, X47_688) | ~c10_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c3_2(X161_216, X47_688) | c2_2(X161_216, X47_688) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216)))).
% 33.31/13.88  tff(c_19181, plain, (![X161_216]: (c2_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c2_2(X161_216, a270) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216) | c3_2(X161_216, a270)))).
% 33.31/13.88  tff(c_18693, plain, (![X161_216, X47_684]: (c2_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, X47_684) | c3_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c3_2(X161_216, X47_684) | c2_2(X161_216, X47_684) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216)))).
% 33.31/13.88  tff(c_18744, plain, (![X161_216, X47_690]: (c10_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, X47_690) | ~c10_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c3_2(X161_216, X47_690) | c2_2(X161_216, X47_690) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216)))).
% 33.31/13.88  tff(c_18890, plain, (![X161_216]: (c10_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c2_2(X161_216, a270) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216) | c3_2(X161_216, a270)))).
% 33.31/13.89  tff(c_18761, plain, (![X161_216, X47_692]: (c2_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, X47_692) | c1_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c3_2(X161_216, X47_692) | c2_2(X161_216, X47_692) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216)))).
% 33.31/13.89  tff(c_18710, plain, (![X161_216, X47_686]: (c10_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, X47_686) | c3_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c3_2(X161_216, X47_686) | c2_2(X161_216, X47_686) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216)))).
% 33.31/13.89  tff(c_18778, plain, (![X161_216, X47_694]: (c10_2(X161_216, a338) | c8_1(X161_216) | c10_2(X161_216, X47_694) | c1_2(X161_216, a270) | ~c7_1(X161_216) | ~c3_1(X161_216) | ~c2_1(X161_216) | c3_2(X161_216, X47_694) | c2_2(X161_216, X47_694) | c4_1(X161_216) | ~c2_2(X161_216, a392) | c10_2(X161_216, a392) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216)))).
% 33.31/13.89  tff(c_18510, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | c1_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | ~c6_2(X46_70, a392) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17675, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | c1_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | ~c6_2(X46_70, a392) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_18592, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c10_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | ~c6_2(X46_70, a392) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_18346, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c10_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | ~c6_2(X46_70, a392) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_18674, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | c3_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | ~c6_2(X46_70, a392) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_18428, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | c3_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | ~c6_2(X46_70, a392) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_13861, plain, (![X49_74, X186_513]: (c10_2(X49_74, a338) | c8_1(X49_74) | c10_2(X49_74, X186_513) | c3_2(X49_74, a270) | c10_1(X49_74) | ~c6_2(X49_74, X186_513) | c2_2(X49_74, X186_513) | ~c7_1(X49_74) | ~c6_2(X49_74, a392) | c10_2(X49_74, a392) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.31/13.89  tff(c_13719, plain, (![X49_74, X186_513]: (c10_2(X49_74, a338) | c8_1(X49_74) | c10_2(X49_74, X186_513) | ~c10_2(X49_74, a270) | c10_1(X49_74) | ~c6_2(X49_74, X186_513) | c2_2(X49_74, X186_513) | ~c7_1(X49_74) | ~c6_2(X49_74, a392) | c10_2(X49_74, a392) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.31/13.89  tff(c_13658, plain, (![X49_74, X186_513]: (c10_2(X49_74, a338) | c8_1(X49_74) | c10_2(X49_74, X186_513) | c1_2(X49_74, a270) | c10_1(X49_74) | ~c6_2(X49_74, X186_513) | c2_2(X49_74, X186_513) | ~c7_1(X49_74) | ~c6_2(X49_74, a392) | c10_2(X49_74, a392) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.31/13.89  tff(c_13520, plain, (![X49_74, X186_513]: (c2_2(X49_74, a338) | c8_1(X49_74) | c10_2(X49_74, X186_513) | c3_2(X49_74, a270) | c10_1(X49_74) | ~c6_2(X49_74, X186_513) | c2_2(X49_74, X186_513) | ~c7_1(X49_74) | ~c6_2(X49_74, a392) | c10_2(X49_74, a392) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.31/13.89  tff(c_13780, plain, (![X49_74, X186_513]: (c2_2(X49_74, a338) | c8_1(X49_74) | c10_2(X49_74, X186_513) | ~c10_2(X49_74, a270) | c10_1(X49_74) | ~c6_2(X49_74, X186_513) | c2_2(X49_74, X186_513) | ~c7_1(X49_74) | ~c6_2(X49_74, a392) | c10_2(X49_74, a392) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.31/13.89  tff(c_15524, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c1_2(X46_70, a270) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_15440, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | ~c10_2(X46_70, a270) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_18039, plain, (![X46_70]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c1_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | c2_2(X46_70, a392) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a392)))).
% 33.31/13.89  tff(c_15776, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c1_2(X46_70, a270) | c10_1(X46_70) | c3_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17988, plain, (![X46_70]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c1_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | c2_2(X46_70, a392) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a392)))).
% 33.31/13.89  tff(c_15608, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c1_2(X46_70, a270) | c10_1(X46_70) | c3_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17937, plain, (![X46_70]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | c2_2(X46_70, a392) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a392)))).
% 33.31/13.89  tff(c_15103, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a270) | c10_1(X46_70) | c3_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_15860, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c1_2(X46_70, a270) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_15356, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | ~c10_2(X46_70, a270) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17693, plain, (![X46_70]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | ~c10_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | c2_2(X46_70, a392) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a392)))).
% 33.31/13.89  tff(c_16028, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | ~c10_2(X46_70, a270) | c10_1(X46_70) | c3_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_13597, plain, (![X49_74, X186_513]: (c2_2(X49_74, a338) | c8_1(X49_74) | c10_2(X49_74, X186_513) | c1_2(X49_74, a270) | c10_1(X49_74) | ~c6_2(X49_74, X186_513) | c2_2(X49_74, X186_513) | ~c7_1(X49_74) | ~c6_2(X49_74, a392) | c10_2(X49_74, a392) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.31/13.89  tff(c_17512, plain, (![X46_70]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a270) | ~c3_1(X46_70) | ~c2_1(X46_70) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c2_2(X46_70, a270) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a270)))).
% 33.31/13.89  tff(c_15272, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a270) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17461, plain, (![X46_70]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | c2_2(X46_70, a392) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a392)))).
% 33.31/13.89  tff(c_15188, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a270) | c10_1(X46_70) | c3_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17361, plain, (![X46_70]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a270) | ~c3_1(X46_70) | ~c2_1(X46_70) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c2_2(X46_70, a270) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a270)))).
% 33.31/13.89  tff(c_15692, plain, (![X46_70, X47_72]: (c2_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a270) | c10_1(X46_70) | c2_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17328, plain, (![X46_70]: (c9_1(X46_70) | c10_2(X46_70, a311) | ~c3_1(X46_70) | ~c2_1(X46_70) | ~c2_2(X46_70, a312) | c10_2(X46_70, a312) | ~c6_1(X46_70) | c10_1(X46_70) | c3_2(X46_70, a311) | c2_2(X46_70, a311) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.89  tff(c_17346, plain, (![X129_177]: (c10_2(X129_177, a338) | c8_1(X129_177) | ~c3_1(X129_177) | ~c2_1(X129_177) | c10_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c6_1(X129_177) | c10_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.31/13.89  tff(c_17333, plain, (![X129_177]: (c2_2(X129_177, a338) | c8_1(X129_177) | ~c3_1(X129_177) | ~c2_1(X129_177) | c10_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c6_1(X129_177) | c10_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.31/13.90  tff(c_17283, plain, (![X161_628]: (c9_1(X161_628) | ~c6_2(X161_628, a311) | c10_2(X161_628, a311) | ~c3_1(X161_628) | ~c2_1(X161_628) | ~c2_2(X161_628, a312) | c10_2(X161_628, a312) | ~ndr1_1(X161_628) | ~c6_1(X161_628) | c10_1(X161_628)))).
% 33.31/13.90  tff(c_17288, plain, (![X161_628]: (c9_1(X161_628) | c7_1(X161_628) | ~c3_1(X161_628) | ~c2_1(X161_628) | ~c2_2(X161_628, a345) | c10_2(X161_628, a345) | ~ndr1_1(X161_628) | ~c6_1(X161_628) | c10_1(X161_628)))).
% 33.31/13.90  tff(c_17261, plain, (![X161_628]: (c1_2(X161_628, a277) | ~c3_1(X161_628) | ~c2_1(X161_628) | ~c2_2(X161_628, a278) | c10_2(X161_628, a278) | ~ndr1_1(X161_628) | ~c6_1(X161_628) | c10_1(X161_628)))).
% 33.31/13.90  tff(c_17262, plain, (![X161_628]: (~c10_2(X161_628, a277) | ~c3_1(X161_628) | ~c2_1(X161_628) | ~c2_2(X161_628, a278) | c10_2(X161_628, a278) | ~ndr1_1(X161_628) | ~c6_1(X161_628) | c10_1(X161_628)))).
% 33.31/13.90  tff(c_17282, plain, (![X161_628]: (~c5_1(X161_628) | ~c3_1(X161_628) | ~c2_1(X161_628) | ~c2_2(X161_628, a313) | c10_2(X161_628, a313) | ~ndr1_1(X161_628) | ~c6_1(X161_628) | c10_1(X161_628)))).
% 33.31/13.90  tff(c_17290, plain, (![X161_628]: (~c2_2(X161_628, a311) | c9_1(X161_628) | ~c2_2(X161_628, a312) | c10_2(X161_628, a312) | ~ndr1_1(X161_628) | ~c6_1(X161_628) | c10_1(X161_628)))).
% 33.31/13.90  tff(c_17302, plain, (~c6_1(a387))).
% 33.31/13.90  tff(c_17301, plain, (~c6_1(a340))).
% 33.31/13.90  tff(c_17289, plain, (![X161_628]: (c4_2(X161_628, a311) | c9_1(X161_628) | ~c2_2(X161_628, a312) | c10_2(X161_628, a312) | ~ndr1_1(X161_628) | ~c6_1(X161_628) | c10_1(X161_628)))).
% 33.31/13.90  tff(c_17299, plain, (~c6_1(a383))).
% 33.31/13.90  tff(c_17298, plain, (~c6_1(a350))).
% 33.31/13.90  tff(c_17297, plain, (~c6_1(a314))).
% 33.31/13.90  tff(c_17296, plain, (~c6_1(a229))).
% 33.31/13.90  tff(c_17069, plain, (![X161_216, X162_218]: (~c2_2(X161_216, X162_218) | c6_2(X161_216, X162_218) | c10_2(X161_216, X162_218) | ~ndr1_1(X161_216) | ~c6_1(X161_216) | c10_1(X161_216)))).
% 33.31/13.90  tff(c_17083, plain, (~c1_1(a346))).
% 33.31/13.90  tff(c_17071, plain, (c8_1(a346))).
% 33.31/13.90  tff(c_17068, plain, (~c3_1(a346))).
% 33.31/13.90  tff(c_17052, plain, (~c6_1(a346))).
% 33.31/13.90  tff(c_17056, plain, (c9_1(a346))).
% 33.31/13.90  tff(c_17053, plain, (c7_1(a346))).
% 33.31/13.90  tff(c_17049, plain, (~c2_1(a346))).
% 33.31/13.90  tff(c_17026, plain, (~ndr1_1(a346))).
% 33.31/13.90  tff(c_16372, plain, (![X46_70]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, a392) | ~c3_1(X46_70) | ~c2_1(X46_70) | ~c10_2(X46_70, a270) | c10_1(X46_70) | ~c7_1(X46_70) | c2_2(X46_70, a392) | ~ndr1_1(X46_70) | c4_1(X46_70) | c3_2(X46_70, a392)))).
% 33.31/13.90  tff(c_16989, plain, (![X185_250, X118_622]: (~c8_1(X185_250) | ~c3_2(X185_250, X118_622) | c6_2(X185_250, X118_622) | c2_1(X185_250) | c10_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, a228) | c2_2(X185_250, a228) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_16990, plain, (![X185_250, X118_622]: (~c8_1(X185_250) | ~c3_2(X185_250, X118_622) | c6_2(X185_250, X118_622) | c2_1(X185_250) | c10_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, a228) | c2_2(X185_250, a228) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_16494, plain, (![X117_615, X118_616]: (~c7_2(X117_615, a228) | ~c8_1(X117_615) | ~c3_2(X117_615, X118_616) | c6_2(X117_615, X118_616) | ~ndr1_1(X117_615) | c2_1(X117_615) | c10_1(X117_615)))).
% 33.31/13.90  tff(c_16495, plain, (![X117_615, X118_616]: (c4_2(X117_615, a228) | ~c8_1(X117_615) | ~c3_2(X117_615, X118_616) | c6_2(X117_615, X118_616) | ~ndr1_1(X117_615) | c2_1(X117_615) | c10_1(X117_615)))).
% 33.31/13.90  tff(c_16768, plain, (~c3_2(a387, a388))).
% 33.31/13.90  tff(c_16764, plain, (~c3_2(a350, a352))).
% 33.31/13.90  tff(c_16762, plain, (~c3_2(a350, a351))).
% 33.31/13.90  tff(c_16758, plain, (~c3_2(a383, a384))).
% 33.31/13.90  tff(c_16756, plain, (~c3_2(a314, a315))).
% 33.31/13.90  tff(c_16752, plain, (~c3_2(a229, a230))).
% 33.31/13.90  tff(c_16496, plain, (![X117_615, X118_616]: (c3_2(X117_615, a228) | ~c8_1(X117_615) | ~c3_2(X117_615, X118_616) | c6_2(X117_615, X118_616) | ~ndr1_1(X117_615) | c2_1(X117_615) | c10_1(X117_615)))).
% 33.31/13.90  tff(c_16544, plain, (c10_1(a223))).
% 33.31/13.90  tff(c_16536, plain, (~c3_2(a406, a407))).
% 33.31/13.90  tff(c_16534, plain, (~c3_2(a223, a224))).
% 33.31/13.90  tff(c_16530, plain, (~c3_2(a340, a341))).
% 33.31/13.90  tff(c_16396, plain, (![X117_159, X118_161]: (~c3_2(X117_159, X118_161) | c8_2(X117_159, X118_161) | c6_2(X117_159, X118_161) | ~ndr1_1(X117_159) | c2_1(X117_159) | c10_1(X117_159)))).
% 33.31/13.90  tff(c_15944, plain, (![X46_70, X47_72]: (c10_2(X46_70, a338) | c8_1(X46_70) | c10_2(X46_70, X47_72) | ~c3_1(X46_70) | ~c2_1(X46_70) | ~c10_2(X46_70, a270) | c10_1(X46_70) | c3_2(X46_70, a392) | ~c7_1(X46_70) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.90  tff(c_16342, plain, (![X175_237]: (~c8_2(X175_237, a386) | c7_1(X175_237) | c3_1(X175_237)))).
% 33.31/13.90  tff(c_16291, plain, (![X175_237]: (c6_2(X175_237, a386) | c7_1(X175_237) | c3_1(X175_237)))).
% 33.31/13.90  tff(c_16289, plain, (~c2_2(a281, a386))).
% 33.31/13.90  tff(c_16288, plain, (~c10_1(a346))).
% 33.31/13.90  tff(c_16264, plain, (![X175_237]: (~c7_2(X175_237, a386) | c7_1(X175_237) | c3_1(X175_237)))).
% 33.31/13.90  tff(c_16266, plain, (~c10_1(a403))).
% 33.31/13.90  tff(c_16265, plain, (~c10_1(a314))).
% 33.31/13.90  tff(c_16262, plain, (~c10_1(a259))).
% 33.31/13.90  tff(c_16261, plain, (~c10_1(a229))).
% 33.31/13.90  tff(c_16210, plain, (![X180_244]: (~c3_1(X180_244) | ~c10_1(X180_244) | c4_1(X180_244)))).
% 33.31/13.90  tff(c_13437, plain, (![X185_250]: (c6_2(X185_250, a278) | ~c8_1(X185_250) | ~c3_2(X185_250, a273) | ~c10_2(X185_250, a273) | c5_2(X185_250, a277) | c3_1(X185_250) | ~c2_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, a228) | c2_2(X185_250, a228) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13436, plain, (![X185_250]: (c6_2(X185_250, a278) | ~c8_1(X185_250) | ~c3_2(X185_250, a273) | ~c10_2(X185_250, a273) | c5_2(X185_250, a277) | c3_1(X185_250) | ~c2_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, a228) | c2_2(X185_250, a228) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_16091, plain, (c1_2(a387, a388))).
% 33.31/13.90  tff(c_16090, plain, (~c4_1(a346))).
% 33.31/13.90  tff(c_16085, plain, (c5_1(a346))).
% 33.31/13.90  tff(c_16082, plain, (c4_1(a387))).
% 33.31/13.90  tff(c_16074, plain, (~c6_2(a387, a388))).
% 33.31/13.90  tff(c_16037, plain, (c7_2(a387, a388))).
% 33.31/13.90  tff(c_16034, plain, (ndr1_1(a387))).
% 33.31/13.90  tff(c_13781, plain, (![X185_250, X186_252]: (c2_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | ~c10_2(X185_250, a270) | c10_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13720, plain, (![X185_250, X186_252]: (c10_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | ~c10_2(X185_250, a270) | c10_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13660, plain, (![X185_250, X186_252]: (c10_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c1_2(X185_250, a270) | c10_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13659, plain, (![X185_250, X186_252]: (c10_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c1_2(X185_250, a270) | c10_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13522, plain, (![X185_250, X186_252]: (c2_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c3_2(X185_250, a270) | c10_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13598, plain, (![X185_250, X186_252]: (c2_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c1_2(X185_250, a270) | c10_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13599, plain, (![X185_250, X186_252]: (c2_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c1_2(X185_250, a270) | c10_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13721, plain, (![X185_250, X186_252]: (c10_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | ~c10_2(X185_250, a270) | c10_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13782, plain, (![X185_250, X186_252]: (c2_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | ~c10_2(X185_250, a270) | c10_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13863, plain, (![X185_250, X186_252]: (c10_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c3_2(X185_250, a270) | c10_1(X185_250) | c2_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_13521, plain, (![X185_250, X186_252]: (c2_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c3_2(X185_250, a270) | c10_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_15109, plain, (~c2_1(a425))).
% 33.31/13.90  tff(c_13862, plain, (![X185_250, X186_252]: (c10_2(X185_250, a338) | c8_1(X185_250) | c10_2(X185_250, X186_252) | ~c3_1(X185_250) | ~c2_1(X185_250) | c3_2(X185_250, a270) | c10_1(X185_250) | c3_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.31/13.90  tff(c_15023, plain, (~c5_1(a422))).
% 33.31/13.90  tff(c_15021, plain, (~c4_1(a422))).
% 33.31/13.90  tff(c_15019, plain, (~c3_1(a422))).
% 33.31/13.90  tff(c_15010, plain, (c8_1(a422))).
% 33.31/13.90  tff(c_14998, plain, (c9_1(a422))).
% 33.31/13.90  tff(c_14995, plain, (c7_1(a422))).
% 33.31/13.90  tff(c_14993, plain, (~c2_1(a422))).
% 33.31/13.90  tff(c_14970, plain, (~ndr1_1(a422))).
% 33.31/13.90  tff(c_14004, plain, (![X46_70]: (c2_2(X46_70, a338) | c10_2(X46_70, a312) | c8_1(X46_70) | c9_1(X46_70) | c10_2(X46_70, a311) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a311) | c2_2(X46_70, a311) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.90  tff(c_13918, plain, (![X46_70]: (c10_2(X46_70, a338) | c10_2(X46_70, a312) | c8_1(X46_70) | c9_1(X46_70) | c10_2(X46_70, a311) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a311) | c2_2(X46_70, a311) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.31/13.91  tff(c_11918, plain, (![X56_84]: (c10_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | c1_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.31/13.91  tff(c_11902, plain, (![X56_84]: (~c7_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | c1_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.31/13.91  tff(c_11903, plain, (![X56_84]: (~c7_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | ~c10_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.31/13.91  tff(c_11379, plain, (![X56_394]: (c2_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c1_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11162, plain, (![X56_389]: (~c7_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c5_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11885, plain, (![X56_84]: (c2_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | c1_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.31/13.91  tff(c_11382, plain, (![X56_394]: (c2_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c5_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11285, plain, (![X56_392]: (c10_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c1_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.31/13.91  tff(c_11283, plain, (![X56_392]: (~c7_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c2_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.31/13.91  tff(c_11375, plain, (![X56_394]: (~c7_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c2_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11380, plain, (![X56_394]: (c10_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c5_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11156, plain, (![X56_389]: (~c7_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c2_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11284, plain, (![X56_392]: (c2_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c2_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.31/13.91  tff(c_11378, plain, (![X56_394]: (~c7_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c1_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11381, plain, (![X56_394]: (~c7_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c5_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11157, plain, (![X56_389]: (c2_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c2_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11161, plain, (![X56_389]: (c10_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c5_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11287, plain, (![X56_392]: (c2_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c1_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.31/13.91  tff(c_11886, plain, (![X56_84]: (c2_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | ~c10_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.31/13.91  tff(c_11887, plain, (![X56_84]: (c2_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | c3_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.31/13.91  tff(c_11377, plain, (![X56_394]: (c10_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c1_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11376, plain, (![X56_394]: (c2_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c2_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.31/13.91  tff(c_11159, plain, (![X56_389]: (~c7_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c1_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11163, plain, (![X56_389]: (c2_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c5_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11155, plain, (![X56_389]: (c10_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c2_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11920, plain, (![X56_84]: (c10_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | c3_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.31/13.91  tff(c_11158, plain, (![X56_389]: (c10_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c1_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.31/13.91  tff(c_11288, plain, (![X56_392]: (c10_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c5_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_11374, plain, (![X56_394]: (c10_2(X56_394, a338) | c10_2(X56_394, a348) | c8_1(X56_394) | ~c2_2(X56_394, a349) | c7_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, a348) | ~c6_2(X56_394, a348) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.56/13.91  tff(c_11904, plain, (![X56_84]: (~c7_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | c3_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.56/13.91  tff(c_11286, plain, (![X56_392]: (~c7_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c1_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_11290, plain, (![X56_392]: (c2_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c5_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_11919, plain, (![X56_84]: (c10_2(X56_84, a338) | c10_2(X56_84, a277) | c8_1(X56_84) | c7_2(X56_84, a278) | ~c2_1(X56_84) | ~c10_2(X56_84, a270) | ~c7_2(X56_84, a277) | ~c6_2(X56_84, a277) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.56/13.91  tff(c_11289, plain, (![X56_392]: (~c7_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c5_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_11160, plain, (![X56_389]: (c2_2(X56_389, a338) | c10_2(X56_389, a348) | c8_1(X56_389) | ~c1_2(X56_389, a349) | c7_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, a348) | ~c6_2(X56_389, a348) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.56/13.91  tff(c_11282, plain, (![X56_392]: (c10_2(X56_392, a338) | c10_2(X56_392, a348) | c8_1(X56_392) | ~c2_2(X56_392, a349) | c7_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, a348) | ~c6_2(X56_392, a348) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_11628, plain, (![X46_70]: (c9_1(X46_70) | c10_2(X46_70, a311) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a312) | c2_2(X46_70, a312) | c3_2(X46_70, a311) | c2_2(X46_70, a311) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.56/13.91  tff(c_13996, plain, (![X49_316]: (c2_2(X49_316, a338) | c10_2(X49_316, a312) | c8_1(X49_316) | c9_1(X49_316) | ~c6_2(X49_316, a311) | c10_2(X49_316, a311) | ~ndr1_1(X49_316) | ~c3_1(X49_316) | ~c2_1(X49_316)))).
% 33.56/13.91  tff(c_13944, plain, (![X49_316]: (~c7_2(X49_316, a338) | c10_2(X49_316, a312) | c8_1(X49_316) | c9_1(X49_316) | ~c6_2(X49_316, a311) | c10_2(X49_316, a311) | ~ndr1_1(X49_316) | ~c3_1(X49_316) | ~c2_1(X49_316)))).
% 33.56/13.91  tff(c_13910, plain, (![X49_316]: (c10_2(X49_316, a338) | c10_2(X49_316, a312) | c8_1(X49_316) | c9_1(X49_316) | ~c6_2(X49_316, a311) | c10_2(X49_316, a311) | ~ndr1_1(X49_316) | ~c3_1(X49_316) | ~c2_1(X49_316)))).
% 33.56/13.91  tff(c_11152, plain, (![X56_389, X57_390]: (c10_2(X56_389, a338) | c8_1(X56_389) | c10_2(X56_389, X57_390) | ~c3_1(X56_389) | ~c2_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, X57_390) | ~c6_2(X56_389, X57_390) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.56/13.91  tff(c_11154, plain, (![X56_389, X57_390]: (~c7_2(X56_389, a338) | c8_1(X56_389) | c10_2(X56_389, X57_390) | ~c3_1(X56_389) | ~c2_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, X57_390) | ~c6_2(X56_389, X57_390) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.56/13.91  tff(c_11280, plain, (![X56_392, X57_393]: (c2_2(X56_392, a338) | c8_1(X56_392) | c10_2(X56_392, X57_393) | ~c3_1(X56_392) | ~c2_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, X57_393) | ~c6_2(X56_392, X57_393) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_11279, plain, (![X56_392, X57_393]: (c10_2(X56_392, a338) | c8_1(X56_392) | c10_2(X56_392, X57_393) | ~c3_1(X56_392) | ~c2_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, X57_393) | ~c6_2(X56_392, X57_393) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_11371, plain, (![X56_394, X57_395]: (c10_2(X56_394, a338) | c8_1(X56_394) | c10_2(X56_394, X57_395) | ~c3_1(X56_394) | ~c2_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, X57_395) | ~c6_2(X56_394, X57_395) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.56/13.91  tff(c_11372, plain, (![X56_394, X57_395]: (c2_2(X56_394, a338) | c8_1(X56_394) | c10_2(X56_394, X57_395) | ~c3_1(X56_394) | ~c2_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, X57_395) | ~c6_2(X56_394, X57_395) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.56/13.91  tff(c_13553, plain, (~c6_2(a350, a352))).
% 33.56/13.91  tff(c_13552, plain, (c2_2(a314, a315))).
% 33.56/13.91  tff(c_13544, plain, (~c6_2(a314, a315))).
% 33.56/13.91  tff(c_11153, plain, (![X56_389, X57_390]: (c2_2(X56_389, a338) | c8_1(X56_389) | c10_2(X56_389, X57_390) | ~c3_1(X56_389) | ~c2_1(X56_389) | c3_2(X56_389, a270) | ~c7_2(X56_389, X57_390) | ~c6_2(X56_389, X57_390) | ~ndr1_1(X56_389) | c10_1(X56_389)))).
% 33.56/13.91  tff(c_11373, plain, (![X56_394, X57_395]: (~c7_2(X56_394, a338) | c8_1(X56_394) | c10_2(X56_394, X57_395) | ~c3_1(X56_394) | ~c2_1(X56_394) | c1_2(X56_394, a270) | ~c7_2(X56_394, X57_395) | ~c6_2(X56_394, X57_395) | ~ndr1_1(X56_394) | c10_1(X56_394)))).
% 33.56/13.91  tff(c_11281, plain, (![X56_392, X57_393]: (~c7_2(X56_392, a338) | c8_1(X56_392) | c10_2(X56_392, X57_393) | ~c3_1(X56_392) | ~c2_1(X56_392) | ~c10_2(X56_392, a270) | ~c7_2(X56_392, X57_393) | ~c6_2(X56_392, X57_393) | ~ndr1_1(X56_392) | c10_1(X56_392)))).
% 33.56/13.91  tff(c_13159, plain, (![X46_70]: (c4_2(X46_70, a228) | ~c8_1(X46_70) | c9_1(X46_70) | c10_2(X46_70, a311) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a311) | c2_2(X46_70, a311) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.56/13.91  tff(c_12785, plain, (![X62_412]: (~c7_2(X62_412, a228) | c6_2(X62_412, a278) | ~c8_1(X62_412) | ~c3_2(X62_412, a273) | ~c10_2(X62_412, a273) | c5_2(X62_412, a277) | ~ndr1_1(X62_412) | c3_1(X62_412) | ~c2_1(X62_412)))).
% 33.56/13.91  tff(c_12663, plain, (![X62_412]: (c4_2(X62_412, a228) | c6_2(X62_412, a278) | ~c8_1(X62_412) | ~c3_2(X62_412, a273) | ~c10_2(X62_412, a273) | c5_2(X62_412, a277) | ~ndr1_1(X62_412) | c3_1(X62_412) | ~c2_1(X62_412)))).
% 33.56/13.91  tff(c_12978, plain, (![X185_488]: (c6_2(X185_488, a278) | ~c8_1(X185_488) | ~c10_2(X185_488, a277) | ~c2_1(X185_488) | c2_2(X185_488, a392) | ~c6_2(X185_488, a228) | c2_2(X185_488, a228) | ~ndr1_1(X185_488) | ~c7_1(X185_488)))).
% 33.56/13.91  tff(c_13322, plain, (![X49_74, X186_513]: (~c6_2(X49_74, X186_513) | c7_2(X49_74, X186_513) | c2_2(X49_74, X186_513) | ~c7_1(X49_74) | ~c6_2(X49_74, a392) | c10_2(X49_74, a392) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.91  tff(c_13317, plain, (![X185_250, X186_252]: (~c9_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c7_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.56/13.91  tff(c_13106, plain, (![X185_492]: (c6_2(X185_492, a278) | ~c8_1(X185_492) | c1_2(X185_492, a277) | ~c2_1(X185_492) | c3_2(X185_492, a392) | ~c6_2(X185_492, a228) | c2_2(X185_492, a228) | ~ndr1_1(X185_492) | ~c7_1(X185_492)))).
% 33.56/13.91  tff(c_13105, plain, (![X185_492]: (c6_2(X185_492, a278) | ~c8_1(X185_492) | ~c10_2(X185_492, a277) | ~c2_1(X185_492) | c3_2(X185_492, a392) | ~c6_2(X185_492, a228) | c2_2(X185_492, a228) | ~ndr1_1(X185_492) | ~c7_1(X185_492)))).
% 33.56/13.91  tff(c_12979, plain, (![X185_488]: (c6_2(X185_488, a278) | ~c8_1(X185_488) | c1_2(X185_488, a277) | ~c2_1(X185_488) | c2_2(X185_488, a392) | ~c6_2(X185_488, a228) | c2_2(X185_488, a228) | ~ndr1_1(X185_488) | ~c7_1(X185_488)))).
% 33.56/13.91  tff(c_13231, plain, (![X185_505]: (~c8_1(X185_505) | c4_2(X185_505, a311) | c9_1(X185_505) | c3_2(X185_505, a392) | ~c6_2(X185_505, a228) | c2_2(X185_505, a228) | ~ndr1_1(X185_505) | ~c7_1(X185_505)))).
% 33.56/13.91  tff(c_13213, plain, (![X185_503]: (~c8_1(X185_503) | ~c2_2(X185_503, a311) | c9_1(X185_503) | c3_2(X185_503, a392) | ~c6_2(X185_503, a228) | c2_2(X185_503, a228) | ~ndr1_1(X185_503) | ~c7_1(X185_503)))).
% 33.56/13.91  tff(c_13194, plain, (![X185_501]: (~c8_1(X185_501) | ~c2_2(X185_501, a311) | c9_1(X185_501) | c2_2(X185_501, a392) | ~c6_2(X185_501, a228) | c2_2(X185_501, a228) | ~ndr1_1(X185_501) | ~c7_1(X185_501)))).
% 33.56/13.91  tff(c_13174, plain, (![X185_499]: (~c8_1(X185_499) | c4_2(X185_499, a311) | c9_1(X185_499) | c2_2(X185_499, a392) | ~c6_2(X185_499, a228) | c2_2(X185_499, a228) | ~ndr1_1(X185_499) | ~c7_1(X185_499)))).
% 33.56/13.91  tff(c_12981, plain, (![X185_488]: (c6_2(X185_488, a358) | ~c8_1(X185_488) | c9_1(X185_488) | c3_1(X185_488) | c2_2(X185_488, a392) | ~c6_2(X185_488, a228) | c2_2(X185_488, a228) | ~ndr1_1(X185_488) | ~c7_1(X185_488)))).
% 33.56/13.91  tff(c_13108, plain, (![X185_492]: (c6_2(X185_492, a358) | ~c8_1(X185_492) | c9_1(X185_492) | c3_1(X185_492) | c3_2(X185_492, a392) | ~c6_2(X185_492, a228) | c2_2(X185_492, a228) | ~ndr1_1(X185_492) | ~c7_1(X185_492)))).
% 33.56/13.91  tff(c_13151, plain, (![X49_495]: (c4_2(X49_495, a228) | ~c8_1(X49_495) | c9_1(X49_495) | ~c6_2(X49_495, a311) | c10_2(X49_495, a311) | ~ndr1_1(X49_495) | ~c3_1(X49_495) | ~c2_1(X49_495)))).
% 33.56/13.91  tff(c_12796, plain, (![X49_316]: (~c7_2(X49_316, a228) | c6_2(X49_316, a312) | ~c8_1(X49_316) | c9_1(X49_316) | ~c6_2(X49_316, a311) | c10_2(X49_316, a311) | ~ndr1_1(X49_316) | ~c3_1(X49_316) | ~c2_1(X49_316)))).
% 33.56/13.91  tff(c_13050, plain, (![X185_250, X186_252]: (c3_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c7_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.56/13.91  tff(c_12997, plain, (~c7_1(a318))).
% 33.56/13.91  tff(c_12996, plain, (~c7_1(a406))).
% 33.56/13.91  tff(c_12923, plain, (![X185_250, X186_252]: (c2_2(X185_250, a392) | ~c6_2(X185_250, X186_252) | c7_2(X185_250, X186_252) | c2_2(X185_250, X186_252) | ~ndr1_1(X185_250) | ~c7_1(X185_250)))).
% 33.56/13.91  tff(c_12702, plain, (![X62_470]: (c10_2(X62_470, a278) | ~c3_1(X62_470) | c4_2(X62_470, a228) | ~ndr1_1(X62_470) | ~c8_1(X62_470) | c1_2(X62_470, a277) | ~c2_1(X62_470)))).
% 33.56/13.91  tff(c_12712, plain, (![X62_471]: (c10_2(X62_471, a278) | ~c3_1(X62_471) | c4_2(X62_471, a228) | ~ndr1_1(X62_471) | ~c8_1(X62_471) | ~c10_2(X62_471, a277) | ~c2_1(X62_471)))).
% 33.56/13.91  tff(c_12798, plain, (![X91_127]: (~c7_2(X91_127, a228) | c6_2(X91_127, a312) | ~ndr1_1(X91_127) | ~c8_1(X91_127) | c4_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.91  tff(c_12797, plain, (![X91_127]: (~c7_2(X91_127, a228) | c6_2(X91_127, a312) | ~ndr1_1(X91_127) | ~c8_1(X91_127) | ~c2_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.91  tff(c_12851, plain, (![X91_480]: (c4_2(X91_480, a228) | ~ndr1_1(X91_480) | ~c8_1(X91_480) | ~c2_2(X91_480, a311) | c9_1(X91_480)))).
% 33.56/13.91  tff(c_12789, plain, (![X62_91]: (~c7_2(X62_91, a228) | c6_2(X62_91, a278) | ~ndr1_1(X62_91) | ~c8_1(X62_91) | ~c10_2(X62_91, a277) | ~c2_1(X62_91)))).
% 33.56/13.91  tff(c_12784, plain, (![X62_91]: (~c7_2(X62_91, a228) | c6_2(X62_91, a278) | ~ndr1_1(X62_91) | ~c8_1(X62_91) | c1_2(X62_91, a277) | ~c2_1(X62_91)))).
% 33.56/13.91  tff(c_12799, plain, (![X129_177]: (~c7_2(X129_177, a228) | c6_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c8_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.91  tff(c_12783, plain, (![X145_196]: (~c7_2(X145_196, a228) | c6_2(X145_196, a358) | ~ndr1_1(X145_196) | ~c8_1(X145_196) | c9_1(X145_196) | c3_1(X145_196)))).
% 33.56/13.91  tff(c_12729, plain, (![X3_11, X4_13]: (~c7_2(X3_11, a228) | ~c8_2(X3_11, X4_13) | c6_2(X3_11, X4_13) | ~ndr1_1(X3_11) | ~c8_1(X3_11)))).
% 33.56/13.91  tff(c_12724, plain, (![X91_472]: (c4_2(X91_472, a228) | ~ndr1_1(X91_472) | ~c8_1(X91_472) | c4_2(X91_472, a311) | c9_1(X91_472)))).
% 33.56/13.91  tff(c_12667, plain, (![X62_91]: (c4_2(X62_91, a228) | c6_2(X62_91, a278) | ~ndr1_1(X62_91) | ~c8_1(X62_91) | ~c10_2(X62_91, a277) | ~c2_1(X62_91)))).
% 33.56/13.91  tff(c_12662, plain, (![X62_91]: (c4_2(X62_91, a228) | c6_2(X62_91, a278) | ~ndr1_1(X62_91) | ~c8_1(X62_91) | c1_2(X62_91, a277) | ~c2_1(X62_91)))).
% 33.56/13.91  tff(c_12677, plain, (![X129_177]: (c4_2(X129_177, a228) | c6_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c8_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.91  tff(c_12661, plain, (![X145_196]: (c4_2(X145_196, a228) | c6_2(X145_196, a358) | ~ndr1_1(X145_196) | ~c8_1(X145_196) | c9_1(X145_196) | c3_1(X145_196)))).
% 33.56/13.91  tff(c_12608, plain, (![X3_11, X4_13]: (c4_2(X3_11, a228) | ~c8_2(X3_11, X4_13) | c6_2(X3_11, X4_13) | ~ndr1_1(X3_11) | ~c8_1(X3_11)))).
% 33.56/13.92  tff(c_12546, plain, (![X46_70]: (c3_2(X46_70, a228) | ~c8_1(X46_70) | c9_1(X46_70) | c10_2(X46_70, a311) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a311) | c2_2(X46_70, a311) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.56/13.92  tff(c_12431, plain, (![X62_412]: (c3_2(X62_412, a228) | c6_2(X62_412, a278) | ~c8_1(X62_412) | ~c3_2(X62_412, a273) | ~c10_2(X62_412, a273) | c5_2(X62_412, a277) | ~ndr1_1(X62_412) | c3_1(X62_412) | ~c2_1(X62_412)))).
% 33.56/13.92  tff(c_12538, plain, (![X49_462]: (c3_2(X49_462, a228) | ~c8_1(X49_462) | c9_1(X49_462) | ~c6_2(X49_462, a311) | c10_2(X49_462, a311) | ~ndr1_1(X49_462) | ~c3_1(X49_462) | ~c2_1(X49_462)))).
% 33.56/13.92  tff(c_12494, plain, (![X62_455]: (c10_2(X62_455, a278) | ~c3_1(X62_455) | c3_2(X62_455, a228) | ~ndr1_1(X62_455) | ~c8_1(X62_455) | ~c10_2(X62_455, a277) | ~c2_1(X62_455)))).
% 33.56/13.92  tff(c_12484, plain, (![X62_454]: (c10_2(X62_454, a278) | ~c3_1(X62_454) | c3_2(X62_454, a228) | ~ndr1_1(X62_454) | ~c8_1(X62_454) | c1_2(X62_454, a277) | ~c2_1(X62_454)))).
% 33.56/13.92  tff(c_12521, plain, (![X91_458]: (c3_2(X91_458, a228) | ~ndr1_1(X91_458) | ~c8_1(X91_458) | c4_2(X91_458, a311) | c9_1(X91_458)))).
% 33.56/13.92  tff(c_12508, plain, (![X91_456]: (c3_2(X91_456, a228) | ~ndr1_1(X91_456) | ~c8_1(X91_456) | ~c2_2(X91_456, a311) | c9_1(X91_456)))).
% 33.56/13.92  tff(c_12435, plain, (![X62_91]: (c3_2(X62_91, a228) | c6_2(X62_91, a278) | ~ndr1_1(X62_91) | ~c8_1(X62_91) | ~c10_2(X62_91, a277) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_12430, plain, (![X62_91]: (c3_2(X62_91, a228) | c6_2(X62_91, a278) | ~ndr1_1(X62_91) | ~c8_1(X62_91) | c1_2(X62_91, a277) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_12445, plain, (![X129_177]: (c3_2(X129_177, a228) | c6_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c8_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.92  tff(c_12429, plain, (![X145_196]: (c3_2(X145_196, a228) | c6_2(X145_196, a358) | ~ndr1_1(X145_196) | ~c8_1(X145_196) | c9_1(X145_196) | c3_1(X145_196)))).
% 33.56/13.92  tff(c_12465, plain, (c1_1(a403))).
% 33.56/13.92  tff(c_12459, plain, (~c8_1(a403))).
% 33.56/13.92  tff(c_12452, plain, (~c8_1(a281))).
% 33.56/13.92  tff(c_12376, plain, (![X3_11, X4_13]: (c3_2(X3_11, a228) | ~c8_2(X3_11, X4_13) | c6_2(X3_11, X4_13) | ~ndr1_1(X3_11) | ~c8_1(X3_11)))).
% 33.56/13.92  tff(c_12338, plain, (c2_2(a389, a390))).
% 33.56/13.92  tff(c_12318, plain, (c4_2(a389, a390))).
% 33.56/13.92  tff(c_12287, plain, (c3_1(a222))).
% 33.56/13.92  tff(c_12282, plain, (~c1_2(a222, a358))).
% 33.56/13.92  tff(c_12274, plain, (![X145_196]: (~c3_2(X145_196, a358) | c9_1(X145_196) | c3_1(X145_196)))).
% 33.56/13.92  tff(c_12265, plain, (c3_1(a223))).
% 33.56/13.92  tff(c_12260, plain, (~c1_2(a223, a358))).
% 33.56/13.92  tff(c_12241, plain, (![X145_196]: (c8_2(X145_196, a358) | c9_1(X145_196) | c3_1(X145_196)))).
% 33.56/13.92  tff(c_12231, plain, (![X145_196]: (c1_2(X145_196, a358) | c9_1(X145_196) | c3_1(X145_196)))).
% 33.56/13.92  tff(c_11680, plain, (![X49_407]: (c10_2(X49_407, a338) | ~c8_2(X49_407, a277) | c10_2(X49_407, a277) | c8_1(X49_407) | ~c6_2(X49_407, a278) | c10_2(X49_407, a278) | ~ndr1_1(X49_407) | ~c3_1(X49_407) | ~c2_1(X49_407)))).
% 33.56/13.92  tff(c_11678, plain, (![X49_407]: (c2_2(X49_407, a338) | ~c8_2(X49_407, a277) | c10_2(X49_407, a277) | c8_1(X49_407) | ~c6_2(X49_407, a278) | c10_2(X49_407, a278) | ~ndr1_1(X49_407) | ~c3_1(X49_407) | ~c2_1(X49_407)))).
% 33.56/13.92  tff(c_11798, plain, (![X62_416]: (~c6_2(X62_416, a278) | c10_2(X62_416, a278) | ~c3_1(X62_416) | ~c7_2(X62_416, a338) | ~c8_2(X62_416, a277) | c10_2(X62_416, a277) | ~ndr1_1(X62_416) | c8_1(X62_416) | ~c2_1(X62_416)))).
% 33.56/13.92  tff(c_12149, plain, (![X169_229]: (c6_2(X169_229, a377) | ~c4_1(X169_229) | c2_1(X169_229)))).
% 33.56/13.92  tff(c_12124, plain, (![X169_229]: (c4_2(X169_229, a377) | ~c4_1(X169_229) | c2_1(X169_229)))).
% 33.56/13.92  tff(c_12091, plain, (![X91_127]: (~c3_2(X91_127, a377) | ~c10_2(X91_127, a377) | c5_2(X91_127, a312) | ~ndr1_1(X91_127) | c3_1(X91_127) | ~c4_1(X91_127) | c2_1(X91_127) | c4_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.92  tff(c_12092, plain, (![X91_127]: (~c3_2(X91_127, a377) | ~c10_2(X91_127, a377) | c5_2(X91_127, a312) | ~ndr1_1(X91_127) | c3_1(X91_127) | ~c4_1(X91_127) | c2_1(X91_127) | ~c2_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.92  tff(c_12090, plain, (![X91_127]: (~c3_2(X91_127, a377) | ~c10_2(X91_127, a377) | c5_2(X91_127, a312) | ~ndr1_1(X91_127) | c3_1(X91_127) | ~c4_1(X91_127) | c2_1(X91_127) | ~c9_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.92  tff(c_12084, plain, (![X130_178]: (~c3_2(X130_178, a377) | ~c10_2(X130_178, a377) | c5_2(X130_178, a348) | ~ndr1_1(X130_178) | c3_1(X130_178) | ~c4_1(X130_178) | c2_1(X130_178) | ~c5_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.92  tff(c_12083, plain, (![X130_178]: (~c3_2(X130_178, a377) | ~c10_2(X130_178, a377) | c5_2(X130_178, a348) | ~ndr1_1(X130_178) | c3_1(X130_178) | ~c4_1(X130_178) | c2_1(X130_178) | ~c1_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.92  tff(c_12082, plain, (![X130_178]: (~c3_2(X130_178, a377) | ~c10_2(X130_178, a377) | c5_2(X130_178, a348) | ~ndr1_1(X130_178) | c3_1(X130_178) | ~c4_1(X130_178) | c2_1(X130_178) | ~c2_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.92  tff(c_12099, plain, (~c10_2(a340, a377))).
% 33.56/13.92  tff(c_12098, plain, (~c10_2(a223, a377))).
% 33.56/13.92  tff(c_12041, plain, (![X169_433, X44_68]: (~c3_2(X169_433, a377) | ~c10_2(X169_433, a377) | ~c9_2(X169_433, X44_68) | c5_2(X169_433, X44_68) | ~ndr1_1(X169_433) | c3_1(X169_433) | ~c4_1(X169_433) | c2_1(X169_433)))).
% 33.56/13.92  tff(c_12037, plain, (![X169_229]: (c5_2(X169_229, a377) | ~c4_1(X169_229) | c2_1(X169_229)))).
% 33.56/13.92  tff(c_12036, plain, (ndr1_1(a389))).
% 33.56/13.92  tff(c_12025, plain, (![X46_70]: (c1_2(X46_70, a277) | c10_2(X46_70, a278) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a278) | c2_2(X46_70, a278) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.56/13.92  tff(c_12019, plain, (![X49_74]: (c1_2(X49_74, a277) | ~c6_2(X49_74, a278) | c10_2(X49_74, a278) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.92  tff(c_12013, plain, (![X62_91]: (c1_2(X62_91, a277) | ~c9_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_12008, plain, (~c3_1(a389))).
% 33.56/13.92  tff(c_11999, plain, (![X135_184]: (~c5_1(X135_184) | ~c4_1(X135_184) | c3_1(X135_184)))).
% 33.56/13.92  tff(c_11944, plain, (![X62_91]: (c1_2(X62_91, a277) | c8_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_11868, plain, (![X62_420]: (~c3_2(X62_420, a273) | ~c10_2(X62_420, a273) | c5_2(X62_420, a277) | ~ndr1_1(X62_420) | c3_1(X62_420) | c7_2(X62_420, a278) | ~c2_1(X62_420)))).
% 33.56/13.92  tff(c_11871, plain, (![X62_420]: (c10_2(X62_420, a338) | ~c8_2(X62_420, a277) | c10_2(X62_420, a277) | ~ndr1_1(X62_420) | c8_1(X62_420) | c7_2(X62_420, a278) | ~c2_1(X62_420)))).
% 33.56/13.92  tff(c_11870, plain, (![X62_420]: (~c7_2(X62_420, a338) | ~c8_2(X62_420, a277) | c10_2(X62_420, a277) | ~ndr1_1(X62_420) | c8_1(X62_420) | c7_2(X62_420, a278) | ~c2_1(X62_420)))).
% 33.56/13.92  tff(c_11869, plain, (![X62_420]: (c2_2(X62_420, a338) | ~c8_2(X62_420, a277) | c10_2(X62_420, a277) | ~ndr1_1(X62_420) | c8_1(X62_420) | c7_2(X62_420, a278) | ~c2_1(X62_420)))).
% 33.56/13.92  tff(c_11854, plain, (![X62_91]: (c9_2(X62_91, a277) | c7_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_11781, plain, (![X46_70]: (~c10_2(X46_70, a277) | c10_2(X46_70, a278) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a278) | c2_2(X46_70, a278) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.56/13.92  tff(c_11744, plain, (![X62_412]: (~c3_2(X62_412, a273) | ~c10_2(X62_412, a273) | c5_2(X62_412, a277) | ~ndr1_1(X62_412) | c3_1(X62_412) | c8_2(X62_412, a278) | ~c2_1(X62_412)))).
% 33.56/13.92  tff(c_11747, plain, (![X62_412]: (c10_2(X62_412, a338) | ~c8_2(X62_412, a277) | c10_2(X62_412, a277) | ~ndr1_1(X62_412) | c8_1(X62_412) | c8_2(X62_412, a278) | ~c2_1(X62_412)))).
% 33.56/13.92  tff(c_11746, plain, (![X62_412]: (~c7_2(X62_412, a338) | ~c8_2(X62_412, a277) | c10_2(X62_412, a277) | ~ndr1_1(X62_412) | c8_1(X62_412) | c8_2(X62_412, a278) | ~c2_1(X62_412)))).
% 33.56/13.92  tff(c_11775, plain, (![X49_74]: (~c10_2(X49_74, a277) | ~c6_2(X49_74, a278) | c10_2(X49_74, a278) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.92  tff(c_11769, plain, (![X62_91]: (~c10_2(X62_91, a277) | ~c9_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_11745, plain, (![X62_412]: (c2_2(X62_412, a338) | ~c8_2(X62_412, a277) | c10_2(X62_412, a277) | ~ndr1_1(X62_412) | c8_1(X62_412) | c8_2(X62_412, a278) | ~c2_1(X62_412)))).
% 33.56/13.92  tff(c_11730, plain, (![X62_91]: (c9_2(X62_91, a277) | c8_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_11684, plain, (![X62_91]: (~c10_2(X62_91, a277) | c8_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_11663, plain, (![X49_74]: (c9_2(X49_74, a277) | ~c6_2(X49_74, a278) | c10_2(X49_74, a278) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.92  tff(c_11657, plain, (![X62_91]: (c9_2(X62_91, a277) | ~c9_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_11644, plain, (![X62_91]: (c1_2(X62_91, a277) | c7_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_11642, plain, (~c2_1(a318))).
% 33.56/13.92  tff(c_11630, plain, (![X62_91]: (~c10_2(X62_91, a277) | c7_2(X62_91, a278) | ~c2_1(X62_91)))).
% 33.56/13.92  tff(c_10335, plain, (![X46_70]: (c9_1(X46_70) | ~c6_2(X46_70, a311) | c10_2(X46_70, a311) | ~c3_1(X46_70) | ~c2_1(X46_70) | c3_2(X46_70, a312) | c2_2(X46_70, a312) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.56/13.92  tff(c_11586, plain, (![X169_229]: (ndr1_1(X169_229) | ~c4_1(X169_229) | c2_1(X169_229)))).
% 33.56/13.92  tff(c_11580, plain, (c4_1(a397))).
% 33.56/13.92  tff(c_11573, plain, (~c6_2(a397, a398))).
% 33.56/13.92  tff(c_11568, plain, (c4_2(a397, a398))).
% 33.56/13.92  tff(c_11567, plain, (~c3_1(a227))).
% 33.56/13.92  tff(c_11565, plain, (~c3_1(a406))).
% 33.56/13.92  tff(c_11529, plain, (![X140_191]: (~c9_1(X140_191) | ~c5_1(X140_191) | ~c3_1(X140_191)))).
% 33.56/13.92  tff(c_11525, plain, (c10_2(a397, a398))).
% 33.56/13.92  tff(c_11468, plain, (![X132_399]: (~c7_1(X132_399) | ~c3_1(X132_399) | c4_1(X132_399) | c1_1(X132_399)))).
% 33.56/13.92  tff(c_11479, plain, (c1_1(a318))).
% 33.56/13.92  tff(c_11478, plain, (c1_1(a429))).
% 33.56/13.92  tff(c_11477, plain, (~c10_2(a397, a399))).
% 33.56/13.92  tff(c_11476, plain, (c1_1(a425))).
% 33.56/13.92  tff(c_11475, plain, (c1_1(a397))).
% 33.56/13.92  tff(c_11444, plain, (![X132_180]: (c8_1(X132_180) | c4_1(X132_180) | c1_1(X132_180)))).
% 33.56/13.92  tff(c_11441, plain, (~c2_1(a397))).
% 33.56/13.92  tff(c_11419, plain, (c8_2(a397, a399))).
% 33.56/13.92  tff(c_11418, plain, (~c1_2(a397, a399))).
% 33.56/13.92  tff(c_10955, plain, (![X129_177]: (~c7_2(X129_177, a338) | c8_1(X129_177) | ~c6_2(X129_177, a347) | c10_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c3_1(X129_177) | ~c2_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.92  tff(c_10985, plain, (![X129_177]: (c2_2(X129_177, a338) | c8_1(X129_177) | ~c6_2(X129_177, a347) | c10_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c3_1(X129_177) | ~c2_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.92  tff(c_11015, plain, (![X129_177]: (c10_2(X129_177, a338) | c8_1(X129_177) | ~c6_2(X129_177, a347) | c10_2(X129_177, a347) | ~ndr1_1(X129_177) | ~c3_1(X129_177) | ~c2_1(X129_177) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.92  tff(c_11308, plain, (![X56_84, X57_86]: (c1_2(X56_84, a270) | ~c7_2(X56_84, X57_86) | ~c6_2(X56_84, X57_86) | c8_2(X56_84, X57_86) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.56/13.92  tff(c_11302, plain, (~c2_2(a406, a407))).
% 33.56/13.92  tff(c_11216, plain, (![X56_84, X57_86]: (~c10_2(X56_84, a270) | ~c7_2(X56_84, X57_86) | ~c6_2(X56_84, X57_86) | c8_2(X56_84, X57_86) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.56/13.92  tff(c_11208, plain, (~c8_2(a406, a407))).
% 33.56/13.92  tff(c_11199, plain, (~c6_2(a223, a345))).
% 33.56/13.92  tff(c_11190, plain, (![X57_390]: (~c1_2(a223, X57_390) | ~c7_2(a223, X57_390) | ~c6_2(a223, X57_390)))).
% 33.56/13.92  tff(c_11189, plain, (c4_1(a223))).
% 33.56/13.92  tff(c_11181, plain, (~c6_2(a223, a224))).
% 33.56/13.92  tff(c_11182, plain, (ndr1_1(a397))).
% 33.56/13.92  tff(c_11180, plain, (c4_1(a340))).
% 33.56/13.92  tff(c_11173, plain, (~c6_2(a340, a341))).
% 33.56/13.92  tff(c_11095, plain, (![X56_84, X57_86]: (c3_2(X56_84, a270) | ~c7_2(X56_84, X57_86) | ~c6_2(X56_84, X57_86) | c8_2(X56_84, X57_86) | ~ndr1_1(X56_84) | c10_1(X56_84)))).
% 33.56/13.92  tff(c_11092, plain, (~c7_2(a406, a407))).
% 33.56/13.92  tff(c_11089, plain, (~c8_1(a397))).
% 33.56/13.92  tff(c_11073, plain, (~c3_1(a269))).
% 33.56/13.92  tff(c_11070, plain, (~c3_1(a401))).
% 33.56/13.92  tff(c_11076, plain, (~c3_1(a357))).
% 33.56/13.92  tff(c_11082, plain, (~c3_1(a309))).
% 33.56/13.92  tff(c_11088, plain, (~c3_1(a376))).
% 33.56/13.92  tff(c_11085, plain, (~c3_1(a418))).
% 33.56/13.92  tff(c_11045, plain, (![X202_270]: (~c8_1(X202_270) | ~c7_1(X202_270) | ~c3_1(X202_270)))).
% 33.56/13.92  tff(c_10782, plain, (![X91_127]: (~c3_2(X91_127, a273) | ~c10_2(X91_127, a273) | c5_2(X91_127, a312) | ~ndr1_1(X91_127) | ~c2_1(X91_127) | c3_1(X91_127) | ~c9_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.92  tff(c_10783, plain, (![X91_127]: (~c3_2(X91_127, a273) | ~c10_2(X91_127, a273) | c5_2(X91_127, a312) | ~ndr1_1(X91_127) | ~c2_1(X91_127) | c3_1(X91_127) | c4_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.92  tff(c_10784, plain, (![X91_127]: (~c3_2(X91_127, a273) | ~c10_2(X91_127, a273) | c5_2(X91_127, a312) | ~ndr1_1(X91_127) | ~c2_1(X91_127) | c3_1(X91_127) | ~c2_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.92  tff(c_10875, plain, (![X130_365]: (~c3_2(X130_365, a273) | ~c10_2(X130_365, a273) | c5_2(X130_365, a348) | ~ndr1_1(X130_365) | ~c2_1(X130_365) | c3_1(X130_365) | ~c1_2(X130_365, a349) | c7_1(X130_365)))).
% 33.56/13.92  tff(c_10806, plain, (![X130_359]: (~c3_2(X130_359, a273) | ~c10_2(X130_359, a273) | c5_2(X130_359, a348) | ~ndr1_1(X130_359) | ~c2_1(X130_359) | c3_1(X130_359) | ~c5_2(X130_359, a349) | c7_1(X130_359)))).
% 33.56/13.92  tff(c_10902, plain, (![X130_369]: (~c3_2(X130_369, a273) | ~c10_2(X130_369, a273) | c5_2(X130_369, a348) | ~ndr1_1(X130_369) | ~c2_1(X130_369) | c3_1(X130_369) | ~c2_2(X130_369, a349) | c7_1(X130_369)))).
% 33.56/13.92  tff(c_10357, plain, (![X49_74, X50_76]: (c10_2(X49_74, a338) | ~c8_2(X49_74, X50_76) | c8_1(X49_74) | ~c6_2(X49_74, X50_76) | c10_2(X49_74, X50_76) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.92  tff(c_10452, plain, (![X49_74, X50_76]: (c2_2(X49_74, a338) | ~c8_2(X49_74, X50_76) | c8_1(X49_74) | ~c6_2(X49_74, X50_76) | c10_2(X49_74, X50_76) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.92  tff(c_10962, plain, (~c2_1(a281))).
% 33.56/13.92  tff(c_10392, plain, (![X49_74, X50_76]: (~c7_2(X49_74, a338) | ~c8_2(X49_74, X50_76) | c8_1(X49_74) | ~c6_2(X49_74, X50_76) | c10_2(X49_74, X50_76) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.92  tff(c_10931, plain, (![X130_178]: (~c4_2(X130_178, a348) | ~c5_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.92  tff(c_10919, plain, (![X130_178]: (~c3_2(X130_178, a348) | ~c1_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.92  tff(c_10915, plain, (![X130_178]: (~c4_2(X130_178, a348) | ~c1_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10912, plain, (~c1_2(a383, a384))).
% 33.56/13.93  tff(c_10905, plain, (![X130_369]: (c10_2(X130_369, a338) | ~c8_2(X130_369, a348) | c10_2(X130_369, a348) | ~ndr1_1(X130_369) | c8_1(X130_369) | ~c2_2(X130_369, a349) | c7_1(X130_369)))).
% 33.56/13.93  tff(c_10904, plain, (![X130_369]: (~c7_2(X130_369, a338) | ~c8_2(X130_369, a348) | c10_2(X130_369, a348) | ~ndr1_1(X130_369) | c8_1(X130_369) | ~c2_2(X130_369, a349) | c7_1(X130_369)))).
% 33.56/13.93  tff(c_10903, plain, (![X130_369]: (c2_2(X130_369, a338) | ~c8_2(X130_369, a348) | c10_2(X130_369, a348) | ~ndr1_1(X130_369) | c8_1(X130_369) | ~c2_2(X130_369, a349) | c7_1(X130_369)))).
% 33.56/13.93  tff(c_10888, plain, (![X130_178]: (c9_2(X130_178, a348) | ~c2_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10878, plain, (![X130_365]: (c10_2(X130_365, a338) | ~c8_2(X130_365, a348) | c10_2(X130_365, a348) | ~ndr1_1(X130_365) | c8_1(X130_365) | ~c1_2(X130_365, a349) | c7_1(X130_365)))).
% 33.56/13.93  tff(c_10877, plain, (![X130_365]: (~c7_2(X130_365, a338) | ~c8_2(X130_365, a348) | c10_2(X130_365, a348) | ~ndr1_1(X130_365) | c8_1(X130_365) | ~c1_2(X130_365, a349) | c7_1(X130_365)))).
% 33.56/13.93  tff(c_10876, plain, (![X130_365]: (c2_2(X130_365, a338) | ~c8_2(X130_365, a348) | c10_2(X130_365, a348) | ~ndr1_1(X130_365) | c8_1(X130_365) | ~c1_2(X130_365, a349) | c7_1(X130_365)))).
% 33.56/13.93  tff(c_10861, plain, (![X130_178]: (c9_2(X130_178, a348) | ~c1_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10856, plain, (c9_1(a406))).
% 33.56/13.93  tff(c_10853, plain, (~c5_2(a383, a385))).
% 33.56/13.93  tff(c_10851, plain, (c4_1(a383))).
% 33.56/13.93  tff(c_10844, plain, (~c6_2(a383, a384))).
% 33.56/13.93  tff(c_10839, plain, (![X130_178]: (~c4_2(X130_178, a348) | ~c2_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10836, plain, (~c1_2(a222, a348))).
% 33.56/13.93  tff(c_10827, plain, (![X130_178]: (~c3_2(X130_178, a348) | ~c2_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10823, plain, (~c10_2(a383, a385))).
% 33.56/13.93  tff(c_10819, plain, (~c3_2(a383, a385))).
% 33.56/13.93  tff(c_10809, plain, (![X130_359]: (c10_2(X130_359, a338) | ~c8_2(X130_359, a348) | c10_2(X130_359, a348) | ~ndr1_1(X130_359) | c8_1(X130_359) | ~c5_2(X130_359, a349) | c7_1(X130_359)))).
% 33.56/13.93  tff(c_10808, plain, (![X130_359]: (~c7_2(X130_359, a338) | ~c8_2(X130_359, a348) | c10_2(X130_359, a348) | ~ndr1_1(X130_359) | c8_1(X130_359) | ~c5_2(X130_359, a349) | c7_1(X130_359)))).
% 33.56/13.93  tff(c_10813, plain, (c4_1(a406))).
% 33.56/13.93  tff(c_10807, plain, (![X130_359]: (c2_2(X130_359, a338) | ~c8_2(X130_359, a348) | c10_2(X130_359, a348) | ~ndr1_1(X130_359) | c8_1(X130_359) | ~c5_2(X130_359, a349) | c7_1(X130_359)))).
% 33.56/13.93  tff(c_10792, plain, (![X130_178]: (c9_2(X130_178, a348) | ~c5_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10789, plain, (~c2_1(a340))).
% 33.56/13.93  tff(c_10788, plain, (~c2_1(a223))).
% 33.56/13.93  tff(c_10734, plain, (![X59_88, X44_355]: (~c3_2(X59_88, a273) | ~c10_2(X59_88, a273) | ~c9_2(X59_88, X44_355) | c5_2(X59_88, X44_355) | ~ndr1_1(X59_88) | ~c2_1(X59_88) | c3_1(X59_88)))).
% 33.56/13.93  tff(c_10758, plain, (~c10_2(a425, a426))).
% 33.56/13.93  tff(c_10756, plain, (![X130_178]: (~c3_2(X130_178, a348) | ~c5_2(X130_178, a349) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10753, plain, (~c10_2(a350, a351))).
% 33.56/13.93  tff(c_10752, plain, (~c10_2(a429, a430))).
% 33.56/13.93  tff(c_10751, plain, (~c3_2(a403, a404))).
% 33.56/13.93  tff(c_10750, plain, (~c3_2(a418, a419))).
% 33.56/13.93  tff(c_10749, plain, (ndr1_1(a406))).
% 33.56/13.93  tff(c_10717, plain, (![X43_65, X45_69, X44_68]: (~c5_2(X43_65, X45_69) | ~c3_2(X43_65, X45_69) | ~c10_2(X43_65, X45_69) | ~c9_2(X43_65, X44_68) | c5_2(X43_65, X44_68) | ~ndr1_1(X43_65) | c3_1(X43_65)))).
% 33.56/13.93  tff(c_10709, plain, (![X92_128]: (c3_2(X92_128, a313) | ~c6_1(X92_128) | ~c5_1(X92_128)))).
% 33.56/13.93  tff(c_10704, plain, (ndr1_1(a383))).
% 33.56/13.93  tff(c_10702, plain, (~c1_1(a422))).
% 33.56/13.93  tff(c_10694, plain, (~c10_1(a422))).
% 33.56/13.93  tff(c_10687, plain, (![X49_74]: (~c6_1(X49_74) | ~c5_1(X49_74) | ~c6_2(X49_74, a313) | c10_2(X49_74, a313) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.93  tff(c_10681, plain, (![X92_128]: (~c9_2(X92_128, a313) | ~c6_1(X92_128) | ~c5_1(X92_128)))).
% 33.56/13.93  tff(c_10397, plain, (![X91_127]: (~c7_2(X91_127, a338) | ~c8_2(X91_127, a312) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | ~c9_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10457, plain, (![X91_127]: (c2_2(X91_127, a338) | ~c8_2(X91_127, a312) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | ~c9_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10663, plain, (![X91_127]: (c10_2(X91_127, a338) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | c4_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10649, plain, (~c2_2(a281, a311))).
% 33.56/13.93  tff(c_10613, plain, (![X91_127]: (c2_2(X91_127, a338) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | ~c2_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10616, plain, (![X62_91]: (ndr1_1(X62_91) | ~c2_1(X62_91)))).
% 33.56/13.93  tff(c_10362, plain, (![X91_127]: (c10_2(X91_127, a338) | ~c8_2(X91_127, a312) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | ~c9_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10586, plain, (![X91_127]: (~c7_2(X91_127, a338) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | ~c2_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10574, plain, (~c2_2(a281, a338))).
% 33.56/13.93  tff(c_10565, plain, (![X91_127]: (~c7_2(X91_127, a338) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | c4_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10522, plain, (![X91_127]: (c10_2(X91_127, a338) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | ~c2_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10551, plain, (~c2_1(a376))).
% 33.56/13.93  tff(c_10550, plain, (~c4_1(a376))).
% 33.56/13.93  tff(c_10549, plain, (c9_1(a376))).
% 33.56/13.93  tff(c_10544, plain, (c7_1(a376))).
% 33.56/13.93  tff(c_10524, plain, (~ndr1_1(a376))).
% 33.56/13.93  tff(c_10509, plain, (![X91_127]: (c2_2(X91_127, a338) | c10_2(X91_127, a312) | ~ndr1_1(X91_127) | c8_1(X91_127) | c4_2(X91_127, a311) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_10495, plain, (~c1_2(a223, a312))).
% 33.56/13.93  tff(c_10494, plain, (~c2_2(a223, a311))).
% 33.56/13.93  tff(c_10493, plain, (~c1_2(a223, a347))).
% 33.56/13.93  tff(c_10467, plain, (![X1_9]: (~c8_2(a223, X1_9) | ~c7_2(a223, X1_9) | ~c1_2(a223, X1_9)))).
% 33.56/13.93  tff(c_10432, plain, (![X111_150, X112_152]: (c2_2(X111_150, a338) | ~c9_2(X111_150, X112_152) | ~c8_2(X111_150, X112_152) | c10_2(X111_150, X112_152) | ~ndr1_1(X111_150) | c8_1(X111_150)))).
% 33.56/13.93  tff(c_10427, plain, (~c6_1(a269))).
% 33.56/13.93  tff(c_10407, plain, (![X92_128]: (ndr1_1(X92_128) | ~c6_1(X92_128) | ~c5_1(X92_128)))).
% 33.56/13.93  tff(c_10372, plain, (![X111_150, X112_152]: (~c7_2(X111_150, a338) | ~c9_2(X111_150, X112_152) | ~c8_2(X111_150, X112_152) | c10_2(X111_150, X112_152) | ~ndr1_1(X111_150) | c8_1(X111_150)))).
% 33.56/13.93  tff(c_10370, plain, (~c8_2(a340, a341))).
% 33.56/13.93  tff(c_10369, plain, (~c8_2(a223, a224))).
% 33.56/13.93  tff(c_10337, plain, (![X111_150, X112_152]: (c10_2(X111_150, a338) | ~c9_2(X111_150, X112_152) | ~c8_2(X111_150, X112_152) | c10_2(X111_150, X112_152) | ~ndr1_1(X111_150) | c8_1(X111_150)))).
% 33.56/13.93  tff(c_10104, plain, (![X49_316]: (~c6_2(X49_316, a312) | c9_1(X49_316) | ~c6_2(X49_316, a311) | c10_2(X49_316, a311) | ~ndr1_1(X49_316) | ~c3_1(X49_316) | ~c2_1(X49_316)))).
% 33.56/13.93  tff(c_10103, plain, (![X49_316]: (c8_2(X49_316, a312) | c9_1(X49_316) | ~c6_2(X49_316, a311) | c10_2(X49_316, a311) | ~ndr1_1(X49_316) | ~c3_1(X49_316) | ~c2_1(X49_316)))).
% 33.56/13.93  tff(c_10296, plain, (c7_2(a229, a230))).
% 33.56/13.93  tff(c_10272, plain, (c2_2(a229, a230))).
% 33.56/13.93  tff(c_10263, plain, (~c6_2(a229, a230))).
% 33.56/13.93  tff(c_10260, plain, (c1_2(a229, a230))).
% 33.56/13.93  tff(c_10238, plain, (![X46_320]: (c4_2(X46_320, a311) | c9_1(X46_320) | c3_2(X46_320, a312) | c2_2(X46_320, a312) | ~ndr1_1(X46_320) | c4_1(X46_320)))).
% 33.56/13.93  tff(c_10239, plain, (![X46_320]: (~c2_2(X46_320, a311) | c9_1(X46_320) | c3_2(X46_320, a312) | c2_2(X46_320, a312) | ~ndr1_1(X46_320) | c4_1(X46_320)))).
% 33.56/13.93  tff(c_10244, plain, (c4_1(a350))).
% 33.56/13.93  tff(c_10220, plain, (![X46_70, X47_72]: (c6_2(X46_70, X47_72) | c3_2(X46_70, X47_72) | c2_2(X46_70, X47_72) | ~ndr1_1(X46_70) | c4_1(X46_70)))).
% 33.56/13.93  tff(c_10102, plain, (![X49_316]: (c9_1(X49_316) | c7_1(X49_316) | ~c6_2(X49_316, a345) | c10_2(X49_316, a345) | ~ndr1_1(X49_316) | ~c3_1(X49_316) | ~c2_1(X49_316)))).
% 33.56/13.93  tff(c_10215, plain, (c7_1(a309))).
% 33.56/13.93  tff(c_10214, plain, (c7_1(a342))).
% 33.56/13.93  tff(c_10213, plain, (c7_1(a357))).
% 33.56/13.93  tff(c_10210, plain, (c7_1(a401))).
% 33.56/13.93  tff(c_10193, plain, (![X130_178]: (ndr1_1(X130_178) | c7_1(X130_178)))).
% 33.56/13.93  tff(c_10182, plain, (~c5_1(a401))).
% 33.56/13.93  tff(c_10180, plain, (c1_1(a401))).
% 33.56/13.93  tff(c_10174, plain, (c8_1(a401))).
% 33.56/13.93  tff(c_10172, plain, (~c2_1(a401))).
% 33.56/13.93  tff(c_10171, plain, (~c4_1(a401))).
% 33.56/13.93  tff(c_10169, plain, (c9_1(a401))).
% 33.56/13.93  tff(c_10149, plain, (~ndr1_1(a401))).
% 33.56/13.93  tff(c_10122, plain, (~c4_1(a229))).
% 33.56/13.93  tff(c_10114, plain, (ndr1_1(a229))).
% 33.56/13.93  tff(c_8929, plain, (![X49_74, X50_76]: (~c6_2(X49_74, X50_76) | c9_2(X49_74, X50_76) | c10_2(X49_74, X50_76) | ~ndr1_1(X49_74) | ~c3_1(X49_74) | ~c2_1(X49_74)))).
% 33.56/13.93  tff(c_10024, plain, (c7_1(a269))).
% 33.56/13.93  tff(c_10022, plain, (~c2_1(a269))).
% 33.56/13.93  tff(c_10021, plain, (~c1_1(a269))).
% 33.56/13.93  tff(c_10015, plain, (c8_1(a269))).
% 33.56/13.93  tff(c_10011, plain, (~c4_1(a269))).
% 33.56/13.93  tff(c_10010, plain, (c9_1(a269))).
% 33.56/13.93  tff(c_9990, plain, (~ndr1_1(a269))).
% 33.56/13.93  tff(c_9980, plain, (![X60_89]: (c2_2(X60_89, a274) | ~c4_1(X60_89) | c3_1(X60_89)))).
% 33.56/13.93  tff(c_9955, plain, (![X60_89]: (c3_2(X60_89, a274) | ~c4_1(X60_89) | c3_1(X60_89)))).
% 33.56/13.93  tff(c_9895, plain, (![X123_168]: (~c9_2(X123_168, a345) | c9_1(X123_168) | c7_1(X123_168)))).
% 33.56/13.93  tff(c_9876, plain, (![X123_168]: (c3_2(X123_168, a345) | c9_1(X123_168) | c7_1(X123_168)))).
% 33.56/13.93  tff(c_9849, plain, (~c10_2(a318, a345))).
% 33.56/13.93  tff(c_9842, plain, (![X123_168]: (c7_2(X123_168, a345) | c9_1(X123_168) | c7_1(X123_168)))).
% 33.56/13.93  tff(c_9795, plain, (![X60_89]: (~c4_2(X60_89, a274) | ~c4_1(X60_89) | c3_1(X60_89)))).
% 33.56/13.93  tff(c_9773, plain, (c1_2(a408, a409))).
% 33.56/13.93  tff(c_9767, plain, (~c5_2(a408, a409))).
% 33.56/13.93  tff(c_9764, plain, (c4_2(a408, a409))).
% 33.56/13.93  tff(c_9719, plain, (~c5_1(a357))).
% 33.56/13.93  tff(c_9715, plain, (c1_1(a357))).
% 33.56/13.93  tff(c_9712, plain, (~c2_1(a357))).
% 33.56/13.93  tff(c_9711, plain, (~c4_1(a357))).
% 33.56/13.93  tff(c_9703, plain, (c8_1(a357))).
% 33.56/13.93  tff(c_9683, plain, (~ndr1_1(a357))).
% 33.56/13.93  tff(c_9650, plain, (![X95_131]: (~c7_2(a318, X95_131) | ~c4_2(a318, X95_131) | ~c10_2(a318, X95_131)))).
% 33.56/13.93  tff(c_9598, plain, (c10_2(a418, a419))).
% 33.56/13.93  tff(c_9592, plain, (~c4_2(a418, a419))).
% 33.56/13.93  tff(c_9589, plain, (~c2_1(a408))).
% 33.56/13.93  tff(c_9586, plain, (ndr1_1(a318))).
% 33.56/13.93  tff(c_9545, plain, (ndr1_1(a408))).
% 33.56/13.93  tff(c_9514, plain, (~c5_1(a342))).
% 33.56/13.93  tff(c_9511, plain, (c1_1(a342))).
% 33.56/13.93  tff(c_9506, plain, (c8_1(a342))).
% 33.56/13.93  tff(c_9499, plain, (~c4_1(a342))).
% 33.56/13.93  tff(c_9504, plain, (c9_1(a342))).
% 33.56/13.93  tff(c_9481, plain, (~ndr1_1(a342))).
% 33.56/13.93  tff(c_9473, plain, (c5_2(a418, a419))).
% 33.56/13.93  tff(c_9467, plain, (~c4_1(a309))).
% 33.56/13.93  tff(c_9461, plain, (![X60_89]: (ndr1_1(X60_89) | ~c4_1(X60_89) | c3_1(X60_89)))).
% 33.56/13.93  tff(c_9457, plain, (c1_1(a281))).
% 33.56/13.93  tff(c_9452, plain, (~c2_2(a281, a347))).
% 33.56/13.93  tff(c_9440, plain, (![X91_127]: (c4_2(X91_127, a311) | ~c6_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9436, plain, (~c5_1(a309))).
% 33.56/13.93  tff(c_9434, plain, (c1_1(a309))).
% 33.56/13.93  tff(c_9432, plain, (~c2_1(a309))).
% 33.56/13.93  tff(c_9427, plain, (c8_1(a309))).
% 33.56/13.93  tff(c_9425, plain, (c9_1(a309))).
% 33.56/13.93  tff(c_9409, plain, (~ndr1_1(a309))).
% 33.56/13.93  tff(c_9405, plain, (c9_2(a223, a224))).
% 33.56/13.93  tff(c_9401, plain, (~c5_2(a314, a315))).
% 33.56/13.93  tff(c_9397, plain, (![Y_7]: (~c2_2(a222, Y_7) | ~c1_2(a222, Y_7) | c3_2(a222, Y_7)))).
% 33.56/13.93  tff(c_9398, plain, (ndr1_1(a222))).
% 33.56/13.93  tff(c_9372, plain, (![X91_127]: (~c9_2(X91_127, a311) | c8_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9368, plain, (~c1_2(a223, a224))).
% 33.56/13.93  tff(c_9365, plain, (![X91_127]: (~c9_2(X91_127, a311) | c9_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9357, plain, (![X91_127]: (~c2_2(X91_127, a311) | ~c6_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9354, plain, (c7_1(a418))).
% 33.56/13.93  tff(c_9345, plain, (![X91_127]: (c4_2(X91_127, a311) | c9_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9341, plain, (![X91_127]: (~c9_2(X91_127, a311) | ~c6_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9337, plain, (![X91_127]: (~c2_2(X91_127, a311) | c8_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9334, plain, (~c10_2(a223, a224))).
% 33.56/13.93  tff(c_9321, plain, (![X65_95]: (~c3_2(a281, X65_95) | ~c2_2(a281, X65_95) | c7_2(a281, X65_95)))).
% 33.56/13.93  tff(c_9314, plain, (![X91_127]: (c4_2(X91_127, a311) | c8_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9309, plain, (~c1_1(a418))).
% 33.56/13.93  tff(c_9304, plain, (c8_1(a418))).
% 33.56/13.93  tff(c_9303, plain, (~c1_1(a376))).
% 33.56/13.93  tff(c_9298, plain, (c8_1(a376))).
% 33.56/13.93  tff(c_9296, plain, (![X91_127]: (~c2_2(X91_127, a311) | c9_2(X91_127, a312) | c9_1(X91_127)))).
% 33.56/13.93  tff(c_9292, plain, (ndr1_1(a418))).
% 33.56/13.93  tff(c_9289, plain, (~c6_1(a376))).
% 33.56/13.93  tff(c_9286, plain, (c4_2(a314, a315))).
% 33.56/13.93  tff(c_9283, plain, (c7_2(a314, a315))).
% 33.56/13.93  tff(c_9280, plain, (![X129_177]: (~c7_2(X129_177, a347) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.93  tff(c_9277, plain, (![X129_177]: (c8_2(X129_177, a347) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.93  tff(c_9270, plain, (![X129_177]: (c2_2(X129_177, a347) | c7_1(X129_177) | c1_1(X129_177)))).
% 33.56/13.93  tff(c_9268, plain, (~c7_1(a223))).
% 33.56/13.93  tff(c_9255, plain, (ndr1_1(a223))).
% 33.56/13.93  tff(c_9249, plain, (~c4_1(a314))).
% 33.56/13.93  tff(c_9245, plain, (ndr1_1(a314))).
% 33.56/13.93  tff(c_9232, plain, (![X59_88]: (c2_2(X59_88, a273) | ~c2_1(X59_88) | c3_1(X59_88)))).
% 33.56/13.93  tff(c_9228, plain, (![X59_88]: (c5_2(X59_88, a273) | ~c2_1(X59_88) | c3_1(X59_88)))).
% 33.56/13.93  tff(c_9227, plain, (c7_2(a350, a352))).
% 33.56/13.93  tff(c_9224, plain, (~c5_2(a350, a352))).
% 33.56/13.93  tff(c_9221, plain, (~c6_2(a350, a351))).
% 33.56/13.93  tff(c_9217, plain, (![X141_192]: (c1_2(X141_192, a354) | ~c9_1(X141_192) | c8_1(X141_192)))).
% 33.56/13.93  tff(c_9214, plain, (![X141_192]: (~c2_2(X141_192, a354) | ~c9_1(X141_192) | c8_1(X141_192)))).
% 33.56/13.93  tff(c_9211, plain, (![X204_272]: (~c8_1(X204_272) | ~c5_1(X204_272) | ~c1_1(X204_272)))).
% 33.56/13.93  tff(c_9206, plain, (c5_2(a350, a351))).
% 33.56/13.93  tff(c_9202, plain, (![X141_192]: (c10_2(X141_192, a354) | ~c9_1(X141_192) | c8_1(X141_192)))).
% 33.56/13.93  tff(c_9199, plain, (~c4_2(a350, a352))).
% 33.56/13.93  tff(c_9195, plain, (![X59_88]: (c6_2(X59_88, a273) | ~c2_1(X59_88) | c3_1(X59_88)))).
% 33.56/13.93  tff(c_9191, plain, (c5_2(a425, a426))).
% 33.56/13.93  tff(c_9190, plain, (c9_1(a227))).
% 33.56/13.93  tff(c_9186, plain, (c6_2(a425, a426))).
% 33.56/13.93  tff(c_9179, plain, (![X141_192]: (ndr1_1(X141_192) | ~c9_1(X141_192) | c8_1(X141_192)))).
% 33.56/13.93  tff(c_9176, plain, (~c1_1(a227))).
% 33.56/13.93  tff(c_9174, plain, (c5_2(a403, a404))).
% 33.56/13.94  tff(c_9169, plain, (~c5_1(a423))).
% 33.56/13.94  tff(c_9168, plain, (ndr1_1(a350))).
% 33.56/13.94  tff(c_9163, plain, (c10_2(a403, a404))).
% 33.56/13.94  tff(c_9162, plain, (~c10_1(a227))).
% 33.56/13.94  tff(c_9157, plain, (c8_2(a403, a404))).
% 33.56/13.94  tff(c_9146, plain, (c1_2(a340, a341))).
% 33.56/13.94  tff(c_9143, plain, (~c8_1(a425))).
% 33.56/13.94  tff(c_9141, plain, (ndr1_1(a425))).
% 33.56/13.94  tff(c_9138, plain, (c2_1(a403))).
% 33.56/13.94  tff(c_9137, plain, (~c6_1(a423))).
% 33.56/13.94  tff(c_9135, plain, (~c4_1(a403))).
% 33.56/13.94  tff(c_9134, plain, (ndr1_1(a403))).
% 33.56/13.94  tff(c_9133, plain, (c7_1(a425))).
% 33.56/13.94  tff(c_9128, plain, (c9_2(a340, a341))).
% 33.56/13.94  tff(c_9114, plain, (~c6_1(a339))).
% 33.56/13.94  tff(c_9107, plain, (c7_2(a340, a341))).
% 33.56/13.94  tff(c_9100, plain, (![X91_127]: (ndr1_1(X91_127) | c9_1(X91_127)))).
% 33.56/13.94  tff(c_9085, plain, (~c8_1(a318))).
% 33.56/13.94  tff(c_9073, plain, (c1_2(a429, a430))).
% 33.56/13.94  tff(c_9067, plain, (~c10_1(a318))).
% 33.56/13.94  tff(c_9061, plain, (c2_2(a429, a430))).
% 33.56/13.94  tff(c_9054, plain, (ndr1_1(a340))).
% 33.56/13.94  tff(c_9050, plain, (~c8_1(a340))).
% 33.56/13.94  tff(c_9047, plain, (c9_1(a357))).
% 33.56/13.94  tff(c_9044, plain, (c5_2(a429, a430))).
% 33.56/13.94  tff(c_9030, plain, (~c8_1(a429))).
% 33.56/13.94  tff(c_9028, plain, (c2_1(a429))).
% 33.56/13.94  tff(c_9027, plain, (~c6_1(a309))).
% 33.56/13.94  tff(c_9022, plain, (c8_2(a281, a282))).
% 33.56/13.94  tff(c_9021, plain, (~c7_1(a222))).
% 33.56/13.94  tff(c_9018, plain, (~c4_2(a281, a282))).
% 33.56/13.94  tff(c_9011, plain, (ndr1_1(a429))).
% 33.56/13.94  tff(c_9005, plain, (c5_1(a269))).
% 33.56/13.94  tff(c_8993, plain, (~c10_0)).
% 33.56/13.94  tff(c_8988, plain, (~c2_1(a342))).
% 33.56/13.94  tff(c_8984, plain, (~c3_1(a342))).
% 33.56/13.94  tff(c_8982, plain, (~c1_1(a222))).
% 33.56/13.94  tff(c_8974, plain, (c3_0)).
% 33.56/13.94  tff(c_8963, plain, (~c4_1(a259))).
% 33.56/13.94  tff(c_8962, plain, (c8_0)).
% 33.56/13.94  tff(c_8958, plain, (~c5_1(a259))).
% 33.56/13.94  tff(c_8955, plain, (c4_0)).
% 33.56/13.94  tff(c_8952, plain, (c7_0)).
% 33.56/13.94  tff(c_8951, plain, (~c5_1(a281))).
% 33.56/13.94  tff(c_8950, plain, (c2_0)).
% 33.56/13.94  tff(c_8949, plain, (ndr1_1(a281))).
% 33.56/13.94  tff(c_8948, plain, (~c9_0)).
% 33.56/13.94  tff(c_8947, plain, (~c6_0)).
% 33.56/13.94  tff(c_8946, plain, (~c1_0)).
% 33.56/13.94  tff(c_54, plain, (~c5_0)).
% 33.56/13.94  tff(c_330, plain, (ndr1_0)).
% 33.56/13.94  % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.56/13.94  
%------------------------------------------------------------------------------