Beagle---0.9.52.CSA-Ass.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Beagle---0.9.52
% Problem  : SYN423+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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s

% Computer : n011.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 34.43s 14.14s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12  % Problem  : SYN423+1 : TPTP v9.0.0. Released v2.1.0.
% 0.04/0.13  % Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34  % Computer : n011.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Wed Apr  9 07:24:33 EDT 2025
% 0.12/0.34  % CPUTime  : 
% 34.42/14.13  
% 34.43/14.14  % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.43/14.14  
% 34.43/14.14  % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.43/14.15  %$ 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 > a619 > a618 > a617 > a616 > a615 > a614 > a613 > a612 > a611 > a610 > a609 > a608 > a607 > a606 > a605 > a604 > a603 > a602 > a601 > a600 > a599 > a598 > a597 > a596 > a595 > a594 > a593 > a592 > a591 > a590 > a589 > a588 > a587 > a586 > a585 > a584 > a583 > a582 > a581 > a580 > a579 > a578 > a577 > a576 > a575 > a574 > a573 > a572 > a571 > a570 > a569 > a568 > a567 > a566 > a565 > a564 > a563 > a562 > a561 > a560 > a559 > a558 > a557 > a556 > a555 > a554 > a553 > a552 > a551 > a550 > a549 > a548 > a547 > a546 > a545 > a544 > a543 > a542 > a541 > a540 > a539 > a538 > a537 > a536 > a535 > a534 > a533 > a532 > a531 > a530 > a529 > a528 > a527 > a526 > a525 > a524 > a523 > a522 > a521 > a520 > a519 > a518 > a517 > a516 > a515 > a514 > a513 > a512 > a511 > a510 > a509 > a508 > a507 > a506 > a505 > a504 > a503 > a502 > a501 > a500 > a499 > a498 > a497 > a496 > a495 > a494 > a493 > a492 > a491 > a490 > a489 > a488 > a487 > a486 > a485 > a484 > a483 > a482 > a481 > a480 > a479 > a478 > a477 > a476 > a475 > a474 > a473 > a472 > a471 > a470 > a469 > a468 > a467 > a466 > a465 > a464 > a463 > a462 > a461 > a460 > a459 > a458 > a457 > a456 > a455 > a454 > a453 > a452 > a451 > a450 > a449 > a448 > a447 > a446 > a445 > a444 > a443 > a442 > a441 > a440 > a439 > a438 > a437 > a436 > a435 > a434 > a433 > a432 > a431
% 34.43/14.15  
% 34.43/14.15  %Foreground sorts:
% 34.43/14.15  
% 34.43/14.15  
% 34.43/14.15  %Background operators:
% 34.43/14.15  
% 34.43/14.15  
% 34.43/14.15  %Foreground operators:
% 34.43/14.15  tff(a565, type, a565: $i).
% 34.43/14.15  tff(c7_0, type, c7_0: $o).
% 34.43/14.15  tff(a492, type, a492: $i).
% 34.43/14.15  tff(a544, type, a544: $i).
% 34.43/14.15  tff(a577, type, a577: $i).
% 34.43/14.15  tff(a586, type, a586: $i).
% 34.43/14.15  tff(a473, type, a473: $i).
% 34.43/14.15  tff(a601, type, a601: $i).
% 34.43/14.15  tff(a433, type, a433: $i).
% 34.43/14.15  tff(a506, type, a506: $i).
% 34.43/14.15  tff(a457, type, a457: $i).
% 34.43/14.15  tff(a600, type, a600: $i).
% 34.43/14.15  tff(a580, type, a580: $i).
% 34.43/14.15  tff(a535, type, a535: $i).
% 34.43/14.15  tff(a542, type, a542: $i).
% 34.43/14.15  tff(a435, type, a435: $i).
% 34.43/14.15  tff(c4_0, type, c4_0: $o).
% 34.43/14.15  tff(a541, type, a541: $i).
% 34.43/14.15  tff(a431, type, a431: $i).
% 34.43/14.15  tff(a556, type, a556: $i).
% 34.43/14.15  tff(a446, type, a446: $i).
% 34.43/14.15  tff(a550, type, a550: $i).
% 34.43/14.15  tff(c3_0, type, c3_0: $o).
% 34.43/14.15  tff(a477, type, a477: $i).
% 34.43/14.15  tff(a460, type, a460: $i).
% 34.43/14.15  tff(a594, type, a594: $i).
% 34.43/14.15  tff(a490, type, a490: $i).
% 34.43/14.15  tff(a567, type, a567: $i).
% 34.43/14.15  tff(a484, type, a484: $i).
% 34.43/14.15  tff(c1_2, type, c1_2: ($i * $i) > $o).
% 34.43/14.15  tff(a503, type, a503: $i).
% 34.43/14.15  tff(a585, type, a585: $i).
% 34.43/14.15  tff(a432, type, a432: $i).
% 34.43/14.15  tff(a471, type, a471: $i).
% 34.43/14.15  tff(a520, type, a520: $i).
% 34.43/14.15  tff(a495, type, a495: $i).
% 34.43/14.15  tff(a502, type, a502: $i).
% 34.43/14.15  tff(a493, type, a493: $i).
% 34.43/14.15  tff(a613, type, a613: $i).
% 34.43/14.15  tff(a537, type, a537: $i).
% 34.43/14.15  tff(a511, type, a511: $i).
% 34.43/14.15  tff(a454, type, a454: $i).
% 34.43/14.15  tff(a564, type, a564: $i).
% 34.43/14.15  tff(a508, type, a508: $i).
% 34.43/14.15  tff(a510, type, a510: $i).
% 34.43/14.15  tff(a487, type, a487: $i).
% 34.43/14.15  tff(a434, type, a434: $i).
% 34.43/14.15  tff(a436, type, a436: $i).
% 34.43/14.15  tff(a488, type, a488: $i).
% 34.43/14.15  tff(a448, type, a448: $i).
% 34.43/14.15  tff(a530, type, a530: $i).
% 34.43/14.15  tff(a553, type, a553: $i).
% 34.43/14.15  tff(a569, type, a569: $i).
% 34.43/14.15  tff(a449, type, a449: $i).
% 34.43/14.15  tff(a528, type, a528: $i).
% 34.43/14.15  tff(a462, type, a462: $i).
% 34.43/14.15  tff(a458, type, a458: $i).
% 34.43/14.15  tff(c8_0, type, c8_0: $o).
% 34.43/14.15  tff(a536, type, a536: $i).
% 34.43/14.15  tff(a459, type, a459: $i).
% 34.43/14.15  tff(a467, type, a467: $i).
% 34.43/14.15  tff(a461, type, a461: $i).
% 34.43/14.15  tff(a596, type, a596: $i).
% 34.43/14.15  tff(a619, type, a619: $i).
% 34.43/14.15  tff(a498, type, a498: $i).
% 34.43/14.15  tff(a505, type, a505: $i).
% 34.43/14.15  tff(a456, type, a456: $i).
% 34.43/14.15  tff(a532, type, a532: $i).
% 34.43/14.15  tff(a504, type, a504: $i).
% 34.43/14.15  tff(a439, type, a439: $i).
% 34.43/14.15  tff(a437, type, a437: $i).
% 34.43/14.15  tff(a468, type, a468: $i).
% 34.43/14.15  tff(c5_0, type, c5_0: $o).
% 34.43/14.15  tff(a438, type, a438: $i).
% 34.43/14.15  tff(a539, type, a539: $i).
% 34.43/14.15  tff(a551, type, a551: $i).
% 34.43/14.15  tff(a572, type, a572: $i).
% 34.43/14.15  tff(a616, type, a616: $i).
% 34.43/14.15  tff(a518, type, a518: $i).
% 34.43/14.15  tff(a546, type, a546: $i).
% 34.43/14.15  tff(a599, type, a599: $i).
% 34.43/14.15  tff(c6_0, type, c6_0: $o).
% 34.43/14.15  tff(c8_2, type, c8_2: ($i * $i) > $o).
% 34.43/14.15  tff(a602, type, a602: $i).
% 34.43/14.15  tff(a453, type, a453: $i).
% 34.43/14.15  tff(a606, type, a606: $i).
% 34.43/14.15  tff(a442, type, a442: $i).
% 34.43/14.15  tff(a570, type, a570: $i).
% 34.43/14.15  tff(a499, type, a499: $i).
% 34.43/14.15  tff(a617, type, a617: $i).
% 34.43/14.15  tff(a605, type, a605: $i).
% 34.43/14.15  tff(a533, type, a533: $i).
% 34.43/14.15  tff(a500, type, a500: $i).
% 34.43/14.15  tff(a472, type, a472: $i).
% 34.43/14.15  tff(a611, type, a611: $i).
% 34.43/14.15  tff(a443, type, a443: $i).
% 34.43/14.15  tff(a470, type, a470: $i).
% 34.43/14.15  tff(a598, type, a598: $i).
% 34.43/14.15  tff(a614, type, a614: $i).
% 34.43/14.15  tff(a516, type, a516: $i).
% 34.43/14.15  tff(a612, type, a612: $i).
% 34.43/14.15  tff(a524, type, a524: $i).
% 34.43/14.15  tff(a563, type, a563: $i).
% 34.43/14.15  tff(a451, type, a451: $i).
% 34.43/14.15  tff(a571, type, a571: $i).
% 34.43/14.15  tff(a543, type, a543: $i).
% 34.43/14.15  tff(a509, type, a509: $i).
% 34.43/14.15  tff(a589, type, a589: $i).
% 34.43/14.15  tff(a558, type, a558: $i).
% 34.43/14.15  tff(c1_0, type, c1_0: $o).
% 34.43/14.15  tff(c8_1, type, c8_1: $i > $o).
% 34.43/14.15  tff(a465, type, a465: $i).
% 34.43/14.15  tff(a469, type, a469: $i).
% 34.43/14.15  tff(c2_1, type, c2_1: $i > $o).
% 34.43/14.15  tff(a549, type, a549: $i).
% 34.43/14.15  tff(a555, type, a555: $i).
% 34.43/14.15  tff(ndr1_1, type, ndr1_1: $i > $o).
% 34.43/14.15  tff(c2_0, type, c2_0: $o).
% 34.43/14.15  tff(c4_1, type, c4_1: $i > $o).
% 34.43/14.15  tff(a529, type, a529: $i).
% 34.43/14.15  tff(a475, type, a475: $i).
% 34.43/14.15  tff(a557, type, a557: $i).
% 34.43/14.15  tff(a575, type, a575: $i).
% 34.43/14.15  tff(a597, type, a597: $i).
% 34.43/14.15  tff(a591, type, a591: $i).
% 34.43/14.15  tff(a494, type, a494: $i).
% 34.43/14.15  tff(a545, type, a545: $i).
% 34.43/14.15  tff(a491, type, a491: $i).
% 34.43/14.15  tff(a562, type, a562: $i).
% 34.43/14.15  tff(a463, type, a463: $i).
% 34.43/14.15  tff(a474, type, a474: $i).
% 34.43/14.15  tff(a581, type, a581: $i).
% 34.43/14.15  tff(a568, type, a568: $i).
% 34.43/14.15  tff(a593, type, a593: $i).
% 34.43/14.15  tff(a609, type, a609: $i).
% 34.43/14.15  tff(a479, type, a479: $i).
% 34.43/14.15  tff(a489, type, a489: $i).
% 34.43/14.15  tff(c9_1, type, c9_1: $i > $o).
% 34.43/14.15  tff(a584, type, a584: $i).
% 34.43/14.15  tff(c10_1, type, c10_1: $i > $o).
% 34.43/14.15  tff(c10_0, type, c10_0: $o).
% 34.43/14.15  tff(a482, type, a482: $i).
% 34.43/14.15  tff(a603, type, a603: $i).
% 34.43/14.15  tff(a452, type, a452: $i).
% 34.43/14.15  tff(a447, type, a447: $i).
% 34.43/14.15  tff(c6_2, type, c6_2: ($i * $i) > $o).
% 34.43/14.15  tff(a507, type, a507: $i).
% 34.43/14.15  tff(a587, type, a587: $i).
% 34.43/14.15  tff(a578, type, a578: $i).
% 34.43/14.15  tff(a610, type, a610: $i).
% 34.43/14.15  tff(a559, type, a559: $i).
% 34.43/14.15  tff(a478, type, a478: $i).
% 34.43/14.15  tff(a464, type, a464: $i).
% 34.43/14.15  tff(a552, type, a552: $i).
% 34.43/14.15  tff(a548, type, a548: $i).
% 34.43/14.15  tff(a534, type, a534: $i).
% 34.43/14.15  tff(a588, type, a588: $i).
% 34.43/14.15  tff(a525, type, a525: $i).
% 34.43/14.15  tff(a523, type, a523: $i).
% 34.43/14.15  tff(a595, type, a595: $i).
% 34.43/14.15  tff(a531, type, a531: $i).
% 34.43/14.15  tff(a522, type, a522: $i).
% 34.43/14.15  tff(a573, type, a573: $i).
% 34.43/14.15  tff(ndr1_0, type, ndr1_0: $o).
% 34.43/14.15  tff(a480, type, a480: $i).
% 34.43/14.15  tff(a618, type, a618: $i).
% 34.43/14.15  tff(a485, type, a485: $i).
% 34.43/14.15  tff(a476, type, a476: $i).
% 34.43/14.15  tff(a483, type, a483: $i).
% 34.43/14.15  tff(a455, type, a455: $i).
% 34.43/14.15  tff(a444, type, a444: $i).
% 34.43/14.15  tff(a538, type, a538: $i).
% 34.43/14.15  tff(a501, type, a501: $i).
% 34.43/14.15  tff(a486, type, a486: $i).
% 34.43/14.15  tff(c9_2, type, c9_2: ($i * $i) > $o).
% 34.43/14.15  tff(a547, type, a547: $i).
% 34.43/14.15  tff(a450, type, a450: $i).
% 34.43/14.15  tff(a615, type, a615: $i).
% 34.43/14.15  tff(c10_2, type, c10_2: ($i * $i) > $o).
% 34.43/14.15  tff(a527, type, a527: $i).
% 34.43/14.15  tff(a526, type, a526: $i).
% 34.43/14.15  tff(a441, type, a441: $i).
% 34.43/14.15  tff(a576, type, a576: $i).
% 34.43/14.15  tff(a561, type, a561: $i).
% 34.43/14.15  tff(a481, type, a481: $i).
% 34.43/14.15  tff(c1_1, type, c1_1: $i > $o).
% 34.43/14.15  tff(a497, type, a497: $i).
% 34.43/14.15  tff(a607, type, a607: $i).
% 34.43/14.15  tff(a521, type, a521: $i).
% 34.43/14.15  tff(c5_2, type, c5_2: ($i * $i) > $o).
% 34.43/14.15  tff(a496, type, a496: $i).
% 34.43/14.15  tff(a540, type, a540: $i).
% 34.43/14.15  tff(c9_0, type, c9_0: $o).
% 34.43/14.15  tff(a519, type, a519: $i).
% 34.43/14.15  tff(a608, type, a608: $i).
% 34.43/14.15  tff(c7_1, type, c7_1: $i > $o).
% 34.43/14.15  tff(c6_1, type, c6_1: $i > $o).
% 34.43/14.15  tff(a445, type, a445: $i).
% 34.43/14.15  tff(a590, type, a590: $i).
% 34.43/14.15  tff(a440, type, a440: $i).
% 34.43/14.15  tff(c4_2, type, c4_2: ($i * $i) > $o).
% 34.43/14.15  tff(a517, type, a517: $i).
% 34.43/14.15  tff(a560, type, a560: $i).
% 34.43/14.15  tff(a582, type, a582: $i).
% 34.43/14.15  tff(a566, type, a566: $i).
% 34.43/14.15  tff(a554, type, a554: $i).
% 34.43/14.15  tff(a515, type, a515: $i).
% 34.43/14.15  tff(c5_1, type, c5_1: $i > $o).
% 34.43/14.15  tff(c7_2, type, c7_2: ($i * $i) > $o).
% 34.43/14.15  tff(a583, type, a583: $i).
% 34.43/14.15  tff(c3_2, type, c3_2: ($i * $i) > $o).
% 34.43/14.15  tff(a514, type, a514: $i).
% 34.43/14.15  tff(a466, type, a466: $i).
% 34.43/14.15  tff(c2_2, type, c2_2: ($i * $i) > $o).
% 34.43/14.15  tff(a604, type, a604: $i).
% 34.43/14.15  tff(a513, type, a513: $i).
% 34.43/14.15  tff(a512, type, a512: $i).
% 34.43/14.15  tff(a574, type, a574: $i).
% 34.43/14.15  tff(a592, type, a592: $i).
% 34.43/14.15  tff(c3_1, type, c3_1: $i > $o).
% 34.43/14.15  tff(a579, type, a579: $i).
% 34.43/14.15  
% 34.43/14.15  %Saturated clause set:
% 34.43/14.15  tff(c_20537, plain, (![X73_99, X33_1060]: (c8_1(X73_99) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | ~c1_2(X73_99, X33_1060) | ~c3_1(X73_99) | ~c10_2(X73_99, X33_1060) | c2_2(X73_99, a545) | c10_2(X73_99, a545) | ~c2_2(X73_99, X33_1060) | c4_2(X73_99, X33_1060) | c6_1(X73_99) | c2_2(X73_99, a511) | c10_2(X73_99, a511) | c10_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.15  tff(c_20700, plain, (![X73_99]: (~c1_2(X73_99, a545) | ~c3_1(X73_99) | c8_1(X73_99) | ~c10_2(X73_99, a545) | ~c2_2(X73_99, a545) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | c6_1(X73_99) | c2_2(X73_99, a511) | c10_2(X73_99, a511) | c10_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99) | c4_2(X73_99, a545)))).
% 34.43/14.15  tff(c_20016, plain, (![X73_99, X33_1027]: (~c1_2(X73_99, X33_1027) | ~c3_1(X73_99) | c8_1(X73_99) | ~c10_2(X73_99, X33_1027) | ~c2_2(X73_99, X33_1027) | c4_2(X73_99, a545) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | c4_2(X73_99, X33_1027) | c6_1(X73_99) | c2_2(X73_99, a511) | c10_2(X73_99, a511) | c10_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.15  tff(c_19945, plain, (![X73_99, X33_1025]: (~c1_2(X73_99, X33_1025) | ~c3_1(X73_99) | c8_1(X73_99) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | ~c10_2(X73_99, X33_1025) | c2_2(X73_99, a545) | c10_2(X73_99, a545) | c10_1(X73_99) | c1_2(X73_99, a511) | ~c2_2(X73_99, X33_1025) | c4_2(X73_99, X33_1025) | c6_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.16  tff(c_20550, plain, (![X73_99]: (~c1_2(X73_99, a511) | ~c3_1(X73_99) | c8_1(X73_99) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | ~c10_2(X73_99, a511) | c2_2(X73_99, a545) | c10_2(X73_99, a545) | c10_1(X73_99) | ~c2_2(X73_99, a511) | c6_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99) | c4_2(X73_99, a511)))).
% 34.43/14.16  tff(c_19874, plain, (![X73_99, X33_1023]: (~c1_2(X73_99, X33_1023) | ~c3_1(X73_99) | c8_1(X73_99) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | ~c10_2(X73_99, X33_1023) | c2_2(X73_99, a545) | c10_2(X73_99, a545) | c10_1(X73_99) | c4_2(X73_99, a511) | ~c2_2(X73_99, X33_1023) | c4_2(X73_99, X33_1023) | c6_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.16  tff(c_20369, plain, (![U_1050, X33_1052]: (~c1_1(U_1050) | c8_1(U_1050) | ~c2_2(U_1050, a576) | ~c10_2(U_1050, a576) | ~c1_2(U_1050, X33_1052) | ~c3_1(U_1050) | ~c10_2(U_1050, X33_1052) | c2_2(U_1050, a545) | c10_2(U_1050, a545) | ~c2_2(U_1050, X33_1052) | ~c4_2(U_1050, a576) | c4_2(U_1050, X33_1052) | c6_1(U_1050) | c2_2(U_1050, a511) | c10_2(U_1050, a511) | ~ndr1_1(U_1050) | c10_1(U_1050) | ~c10_2(U_1050, a431) | ~c2_1(U_1050)))).
% 34.43/14.16  tff(c_19008, plain, (![X150_946, X33_947, X143_188]: (~c1_2(X150_946, X33_947) | ~c10_2(X150_946, X143_188) | ~c3_1(X150_946) | ~c1_1(X150_946) | c8_1(X150_946) | ~c2_2(X150_946, a576) | ~c10_2(X150_946, a576) | ~c10_2(X150_946, X33_947) | c2_2(X150_946, a545) | c10_2(X150_946, a545) | ~c2_2(X150_946, X33_947) | ~c2_1(X150_946) | ~c4_2(X150_946, a576) | c4_2(X150_946, X33_947) | c6_1(X150_946) | c2_2(X150_946, a511) | c10_2(X150_946, a511) | ~ndr1_1(X150_946) | c10_1(X150_946)))).
% 34.43/14.16  tff(c_20326, plain, (![U_1, X33_1047, X34_1049]: (~c1_2(U_1, X33_1047) | ~c3_1(U_1) | ~c10_2(U_1, X33_1047) | ~c2_2(U_1, X33_1047) | ~c2_2(U_1, X34_1049) | ~c10_2(U_1, X34_1049) | c2_2(U_1, a545) | c10_2(U_1, a545) | ~c4_2(U_1, X34_1049) | c6_2(U_1, X34_1049) | c4_2(U_1, X33_1047) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_18956, plain, (![X150_939, X33_940, X143_188, X34_941]: (~c1_2(X150_939, X33_940) | ~c10_2(X150_939, X143_188) | ~c3_1(X150_939) | ~c10_2(X150_939, X33_940) | ~c2_2(X150_939, X33_940) | ~c2_1(X150_939) | ~c2_2(X150_939, X34_941) | ~c10_2(X150_939, X34_941) | c2_2(X150_939, a545) | c10_2(X150_939, a545) | ~c4_2(X150_939, X34_941) | c6_2(X150_939, X34_941) | c4_2(X150_939, X33_940) | c6_1(X150_939) | c2_2(X150_939, a511) | c10_2(X150_939, a511) | ~ndr1_1(X150_939) | c10_1(X150_939)))).
% 34.43/14.16  tff(c_20244, plain, (![X73_99]: (~c1_2(X73_99, a545) | ~c3_1(X73_99) | c8_1(X73_99) | ~c10_2(X73_99, a545) | c4_2(X73_99, a511) | ~c2_2(X73_99, a545) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | c6_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99) | c4_2(X73_99, a545)))).
% 34.43/14.16  tff(c_17606, plain, (![X73_99, X33_861]: (~c1_2(X73_99, X33_861) | ~c3_1(X73_99) | c8_1(X73_99) | ~c10_2(X73_99, X33_861) | c4_2(X73_99, a511) | ~c2_2(X73_99, X33_861) | c4_2(X73_99, a545) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | c4_2(X73_99, X33_861) | c6_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.16  tff(c_20188, plain, (![X73_99]: (~c1_2(X73_99, a545) | ~c3_1(X73_99) | c8_1(X73_99) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | ~c10_2(X73_99, a545) | c1_2(X73_99, a511) | ~c2_2(X73_99, a545) | c6_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99) | c4_2(X73_99, a545)))).
% 34.43/14.16  tff(c_17527, plain, (![X73_99, X33_857]: (~c1_2(X73_99, X33_857) | ~c3_1(X73_99) | c8_1(X73_99) | ~c2_2(X73_99, a576) | ~c10_2(X73_99, a576) | c4_2(X73_99, a545) | ~c10_2(X73_99, X33_857) | c1_2(X73_99, a511) | ~c2_2(X73_99, X33_857) | c4_2(X73_99, X33_857) | c6_1(X73_99) | ~c10_2(X73_99, a431) | ~c2_1(X73_99) | ~c2_2(X73_99, a520) | ~c3_2(X73_99, a576) | c1_2(X73_99, a576) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.16  tff(c_12867, plain, (![U_546, X34_548, X33_547]: (~c2_2(U_546, X34_548) | ~c10_2(U_546, X34_548) | c2_2(U_546, a545) | c10_2(U_546, a545) | c10_1(U_546) | ~c1_2(U_546, X33_547) | ~c3_1(U_546) | c6_2(U_546, a505) | ~c10_2(U_546, X33_547) | c2_2(U_546, X33_547) | c1_1(U_546) | ~c4_2(U_546, X34_548) | c6_2(U_546, X34_548) | c4_2(U_546, X33_547) | ~ndr1_1(U_546) | c6_1(U_546) | ~c10_2(U_546, a431) | ~c2_1(U_546)))).
% 34.43/14.16  tff(c_17305, plain, (![U_1, X33_838, X34_840]: (~c1_2(U_1, X33_838) | ~c3_1(U_1) | ~c2_2(U_1, X34_840) | ~c10_2(U_1, X34_840) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | ~c3_2(U_1, a505) | ~c10_2(U_1, X33_838) | c2_2(U_1, X33_838) | c1_1(U_1) | ~c4_2(U_1, X34_840) | c6_2(U_1, X34_840) | c4_2(U_1, X33_838) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_19708, plain, (![U_1007, X33_1008]: (~c1_1(U_1007) | c8_1(U_1007) | ~c1_2(U_1007, X33_1008) | ~c3_1(U_1007) | ~c10_2(U_1007, X33_1008) | ~c2_2(U_1007, X33_1008) | c6_2(U_1007, a545) | ~c2_2(U_1007, a576) | ~c10_2(U_1007, a576) | ~c4_2(U_1007, a576) | c4_2(U_1007, X33_1008) | c6_1(U_1007) | c2_2(U_1007, a511) | c10_2(U_1007, a511) | ~ndr1_1(U_1007) | c10_1(U_1007) | ~c10_2(U_1007, a431) | ~c2_1(U_1007)))).
% 34.43/14.16  tff(c_19777, plain, (![U_1, X33_1017]: (~c1_2(U_1, X33_1017) | ~c3_1(U_1) | ~c1_1(U_1) | c8_1(U_1) | ~c10_2(U_1, X33_1017) | ~c2_2(U_1, X33_1017) | c4_2(U_1, a545) | ~c2_2(U_1, a576) | ~c10_2(U_1, a576) | ~c4_2(U_1, a576) | c4_2(U_1, X33_1017) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_19755, plain, (![U_1, X33_1014]: (~c1_2(U_1, X33_1014) | ~c3_1(U_1) | ~c1_1(U_1) | c8_1(U_1) | ~c2_2(U_1, a576) | ~c10_2(U_1, a576) | ~c10_2(U_1, X33_1014) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | c1_2(U_1, a511) | ~c2_2(U_1, X33_1014) | ~c4_2(U_1, a576) | c4_2(U_1, X33_1014) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_19733, plain, (![U_1, X33_1011]: (~c1_2(U_1, X33_1011) | ~c3_1(U_1) | ~c1_1(U_1) | c8_1(U_1) | ~c2_2(U_1, a576) | ~c10_2(U_1, a576) | ~c10_2(U_1, X33_1011) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | c4_2(U_1, a511) | ~c2_2(U_1, X33_1011) | ~c4_2(U_1, a576) | c4_2(U_1, X33_1011) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_17474, plain, (![X150_854, X33_855, X143_188]: (~c1_2(X150_854, X33_855) | ~c10_2(X150_854, X143_188) | ~c3_1(X150_854) | ~c1_1(X150_854) | c8_1(X150_854) | ~c2_2(X150_854, a576) | ~c10_2(X150_854, a576) | c6_2(X150_854, a545) | ~c10_2(X150_854, X33_855) | ~c2_2(X150_854, X33_855) | ~c2_1(X150_854) | ~c4_2(X150_854, a576) | c4_2(X150_854, X33_855) | c6_1(X150_854) | c2_2(X150_854, a511) | c10_2(X150_854, a511) | ~ndr1_1(X150_854) | c10_1(X150_854)))).
% 34.43/14.16  tff(c_17391, plain, (![X150_850, X33_851, X143_188]: (~c1_2(X150_850, X33_851) | ~c10_2(X150_850, X143_188) | ~c3_1(X150_850) | ~c1_1(X150_850) | c8_1(X150_850) | ~c10_2(X150_850, X33_851) | ~c2_2(X150_850, X33_851) | ~c2_1(X150_850) | c4_2(X150_850, a545) | ~c2_2(X150_850, a576) | ~c10_2(X150_850, a576) | ~c4_2(X150_850, a576) | c4_2(X150_850, X33_851) | c6_1(X150_850) | c2_2(X150_850, a511) | c10_2(X150_850, a511) | ~ndr1_1(X150_850) | c10_1(X150_850)))).
% 34.43/14.16  tff(c_17255, plain, (![X32_832, X33_833, X143_188]: (~c1_2(X32_832, X33_833) | ~c10_2(X32_832, X143_188) | ~c3_1(X32_832) | ~c1_1(X32_832) | c8_1(X32_832) | ~c2_2(X32_832, a576) | ~c10_2(X32_832, a576) | ~c10_2(X32_832, X33_833) | c2_2(X32_832, a545) | c10_2(X32_832, a545) | c10_1(X32_832) | c1_2(X32_832, a511) | ~c2_2(X32_832, X33_833) | ~c2_1(X32_832) | ~c4_2(X32_832, a576) | c4_2(X32_832, X33_833) | ~ndr1_1(X32_832) | c6_1(X32_832)))).
% 34.43/14.16  tff(c_17217, plain, (![X32_830, X33_831, X143_188]: (~c1_2(X32_830, X33_831) | ~c10_2(X32_830, X143_188) | ~c3_1(X32_830) | ~c1_1(X32_830) | c8_1(X32_830) | ~c2_2(X32_830, a576) | ~c10_2(X32_830, a576) | ~c10_2(X32_830, X33_831) | c2_2(X32_830, a545) | c10_2(X32_830, a545) | c10_1(X32_830) | c4_2(X32_830, a511) | ~c2_2(X32_830, X33_831) | ~c2_1(X32_830) | ~c4_2(X32_830, a576) | c4_2(X32_830, X33_831) | ~ndr1_1(X32_830) | c6_1(X32_830)))).
% 34.43/14.16  tff(c_19171, plain, (![U_1, X33_973, X34_975]: (~c1_2(U_1, X33_973) | ~c3_1(U_1) | ~c10_2(U_1, X33_973) | ~c2_2(U_1, X33_973) | c6_2(U_1, a545) | ~c2_2(U_1, X34_975) | ~c10_2(U_1, X34_975) | ~c4_2(U_1, X34_975) | c6_2(U_1, X34_975) | c4_2(U_1, X33_973) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_19193, plain, (![U_1, X33_977, X34_979]: (~c1_2(U_1, X33_977) | ~c3_1(U_1) | ~c10_2(U_1, X33_977) | c1_2(U_1, a511) | ~c2_2(U_1, X33_977) | ~c2_2(U_1, X34_979) | ~c10_2(U_1, X34_979) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | ~c4_2(U_1, X34_979) | c6_2(U_1, X34_979) | c4_2(U_1, X33_977) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_19149, plain, (![U_1, X33_969, X34_971]: (~c1_2(U_1, X33_969) | ~c3_1(U_1) | ~c10_2(U_1, X33_969) | ~c2_2(U_1, X33_969) | c4_2(U_1, a545) | ~c2_2(U_1, X34_971) | ~c10_2(U_1, X34_971) | ~c4_2(U_1, X34_971) | c6_2(U_1, X34_971) | c4_2(U_1, X33_969) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_19105, plain, (![U_1, X33_961, X34_963]: (~c1_2(U_1, X33_961) | ~c3_1(U_1) | ~c10_2(U_1, X33_961) | c4_2(U_1, a511) | ~c2_2(U_1, X33_961) | ~c2_2(U_1, X34_963) | ~c10_2(U_1, X34_963) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | ~c4_2(U_1, X34_963) | c6_2(U_1, X34_963) | c4_2(U_1, X33_961) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_18961, plain, (![X150_939, X33_940, X34_941]: (c3_2(X150_939, X33_940) | c1_1(X150_939) | ~c10_2(X150_939, X33_940) | ~c2_2(X150_939, X33_940) | ~c2_1(X150_939) | ~c2_2(X150_939, X34_941) | ~c10_2(X150_939, X34_941) | c2_2(X150_939, a545) | c10_2(X150_939, a545) | ~c4_2(X150_939, X34_941) | c6_2(X150_939, X34_941) | c4_2(X150_939, X33_940) | c6_1(X150_939) | c2_2(X150_939, a511) | c10_2(X150_939, a511) | ~ndr1_1(X150_939) | c10_1(X150_939)))).
% 34.43/14.16  tff(c_19039, plain, (![U_1, X33_949, X34_951]: (~c1_2(U_1, X33_949) | ~c3_1(U_1) | ~c10_2(U_1, X33_949) | c2_2(U_1, a545) | c10_2(U_1, a545) | ~c2_2(U_1, X33_949) | ~c4_2(U_1, X34_951) | c8_2(U_1, X34_951) | c6_2(U_1, X34_951) | c4_2(U_1, X33_949) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.16  tff(c_16621, plain, (![X32_795, X33_796, X143_188, X34_797]: (~c1_2(X32_795, X33_796) | ~c10_2(X32_795, X143_188) | ~c3_1(X32_795) | ~c10_2(X32_795, X33_796) | c1_2(X32_795, a511) | ~c2_2(X32_795, X33_796) | ~c2_1(X32_795) | ~c2_2(X32_795, X34_797) | ~c10_2(X32_795, X34_797) | c2_2(X32_795, a545) | c10_2(X32_795, a545) | c10_1(X32_795) | ~c4_2(X32_795, X34_797) | c6_2(X32_795, X34_797) | c4_2(X32_795, X33_796) | ~ndr1_1(X32_795) | c6_1(X32_795)))).
% 34.43/14.16  tff(c_16695, plain, (![X150_798, X33_799, X143_188, X34_800]: (~c1_2(X150_798, X33_799) | ~c10_2(X150_798, X143_188) | ~c3_1(X150_798) | ~c10_2(X150_798, X33_799) | ~c2_2(X150_798, X33_799) | ~c2_1(X150_798) | c6_2(X150_798, a545) | ~c2_2(X150_798, X34_800) | ~c10_2(X150_798, X34_800) | ~c4_2(X150_798, X34_800) | c6_2(X150_798, X34_800) | c4_2(X150_798, X33_799) | c6_1(X150_798) | c2_2(X150_798, a511) | c10_2(X150_798, a511) | ~ndr1_1(X150_798) | c10_1(X150_798)))).
% 34.43/14.17  tff(c_16396, plain, (![X150_765, X33_766, X143_188, X34_767]: (~c1_2(X150_765, X33_766) | ~c10_2(X150_765, X143_188) | ~c3_1(X150_765) | ~c10_2(X150_765, X33_766) | ~c2_2(X150_765, X33_766) | ~c2_1(X150_765) | c4_2(X150_765, a545) | ~c2_2(X150_765, X34_767) | ~c10_2(X150_765, X34_767) | ~c4_2(X150_765, X34_767) | c6_2(X150_765, X34_767) | c4_2(X150_765, X33_766) | c6_1(X150_765) | c2_2(X150_765, a511) | c10_2(X150_765, a511) | ~ndr1_1(X150_765) | c10_1(X150_765)))).
% 34.43/14.17  tff(c_16529, plain, (![X32_784, X33_785, X143_188, X34_786]: (~c1_2(X32_784, X33_785) | ~c10_2(X32_784, X143_188) | ~c3_1(X32_784) | ~c10_2(X32_784, X33_785) | c4_2(X32_784, a511) | ~c2_2(X32_784, X33_785) | ~c2_1(X32_784) | ~c2_2(X32_784, X34_786) | ~c10_2(X32_784, X34_786) | c2_2(X32_784, a545) | c10_2(X32_784, a545) | c10_1(X32_784) | ~c4_2(X32_784, X34_786) | c6_2(X32_784, X34_786) | c4_2(X32_784, X33_785) | ~ndr1_1(X32_784) | c6_1(X32_784)))).
% 34.43/14.17  tff(c_15718, plain, (![X150_709, X33_710, X143_188, X34_711]: (~c1_2(X150_709, X33_710) | ~c10_2(X150_709, X143_188) | ~c3_1(X150_709) | ~c10_2(X150_709, X33_710) | c2_2(X150_709, a545) | c10_2(X150_709, a545) | ~c2_2(X150_709, X33_710) | ~c2_1(X150_709) | ~c4_2(X150_709, X34_711) | c8_2(X150_709, X34_711) | c6_2(X150_709, X34_711) | c4_2(X150_709, X33_710) | c6_1(X150_709) | c2_2(X150_709, a511) | c10_2(X150_709, a511) | ~ndr1_1(X150_709) | c10_1(X150_709)))).
% 34.43/14.17  tff(c_18792, plain, (![X150_931, X33_933]: (~c1_1(X150_931) | c8_1(X150_931) | ~c2_2(X150_931, a576) | ~c10_2(X150_931, a576) | ~c10_2(X150_931, X33_933) | c2_2(X150_931, a545) | c10_2(X150_931, a545) | ~c2_2(X150_931, X33_933) | ~c2_1(X150_931) | ~c4_2(X150_931, a576) | c5_2(X150_931, X33_933) | c4_2(X150_931, X33_933) | c6_1(X150_931) | c2_2(X150_931, a511) | c10_2(X150_931, a511) | ~ndr1_1(X150_931) | c10_1(X150_931)))).
% 34.43/14.17  tff(c_18857, plain, (![X150_934, X33_935, X34_936]: (~c10_2(X150_934, X33_935) | ~c2_2(X150_934, X33_935) | ~c2_1(X150_934) | ~c2_2(X150_934, X34_936) | ~c10_2(X150_934, X34_936) | c2_2(X150_934, a545) | c10_2(X150_934, a545) | ~c4_2(X150_934, X34_936) | c6_2(X150_934, X34_936) | c5_2(X150_934, X33_935) | c4_2(X150_934, X33_935) | c6_1(X150_934) | c2_2(X150_934, a511) | c10_2(X150_934, a511) | ~ndr1_1(X150_934) | c10_1(X150_934)))).
% 34.43/14.17  tff(c_17748, plain, (![U_1, X33_876]: (~c1_2(U_1, X33_876) | ~c3_1(U_1) | ~c2_2(U_1, a505) | ~c10_2(U_1, a505) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | ~c10_2(U_1, X33_876) | c2_2(U_1, X33_876) | c1_1(U_1) | ~c4_2(U_1, a505) | c4_2(U_1, X33_876) | ~ndr1_1(U_1) | c6_1(U_1) | c6_2(U_1, a505) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_14792, plain, (![X150_197, X33_663, X34_664]: (~c2_2(X150_197, X33_663) | c8_2(X150_197, X33_663) | ~c2_1(X150_197) | ~c2_2(X150_197, X34_664) | ~c10_2(X150_197, X34_664) | c2_2(X150_197, a545) | c10_2(X150_197, a545) | ~c4_2(X150_197, X34_664) | c6_2(X150_197, X34_664) | c5_2(X150_197, X33_663) | c4_2(X150_197, X33_663) | c6_1(X150_197) | c2_2(X150_197, a511) | c10_2(X150_197, a511) | ~ndr1_1(X150_197) | c10_1(X150_197)))).
% 34.43/14.17  tff(c_15706, plain, (![X150_709, X34_711, X33_710]: (~c2_2(X150_709, X34_711) | ~c10_2(X150_709, X34_711) | ~c10_2(X150_709, X33_710) | c2_2(X150_709, a545) | c10_2(X150_709, a545) | ~c2_2(X150_709, X33_710) | ~c2_1(X150_709) | ~c4_2(X150_709, X34_711) | c6_2(X150_709, X34_711) | c5_2(X150_709, X33_710) | c4_2(X150_709, X33_710) | c6_1(X150_709) | c2_2(X150_709, a511) | c10_2(X150_709, a511) | ~ndr1_1(X150_709) | c10_1(X150_709)))).
% 34.43/14.17  tff(c_18721, plain, (![U_1, X33_927]: (~c1_2(U_1, X33_927) | ~c3_1(U_1) | ~c2_2(U_1, a545) | ~c10_2(U_1, a545) | ~c10_2(U_1, X33_927) | ~c2_2(U_1, X33_927) | ~c4_2(U_1, a545) | c4_2(U_1, X33_927) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16210, plain, (![X150_750, X33_751, X143_188]: (~c1_2(X150_750, X33_751) | ~c10_2(X150_750, X143_188) | ~c3_1(X150_750) | ~c2_2(X150_750, a545) | ~c10_2(X150_750, a545) | ~c10_2(X150_750, X33_751) | ~c2_2(X150_750, X33_751) | ~c2_1(X150_750) | ~c4_2(X150_750, a545) | c4_2(X150_750, X33_751) | c6_1(X150_750) | c2_2(X150_750, a511) | c10_2(X150_750, a511) | ~ndr1_1(X150_750) | c10_1(X150_750) | c6_2(X150_750, a545)))).
% 34.43/14.17  tff(c_17676, plain, (![U_1, X33_869, X34_871]: (~c1_2(U_1, X33_869) | ~c3_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, X33_869) | ~c2_2(U_1, X33_869) | ~c4_2(U_1, X34_871) | c8_2(U_1, X34_871) | c6_2(U_1, X34_871) | c4_2(U_1, X33_869) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_17654, plain, (![U_1, X33_865, X34_867]: (~c1_2(U_1, X33_865) | ~c3_1(U_1) | c4_2(U_1, a545) | ~c10_2(U_1, X33_865) | ~c2_2(U_1, X33_865) | ~c4_2(U_1, X34_867) | c8_2(U_1, X34_867) | c6_2(U_1, X34_867) | c4_2(U_1, X33_865) | c6_1(U_1) | c2_2(U_1, a511) | c10_2(U_1, a511) | ~ndr1_1(U_1) | c10_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16401, plain, (![X150_765, X33_766, X34_767]: (c3_2(X150_765, X33_766) | c1_1(X150_765) | ~c10_2(X150_765, X33_766) | ~c2_2(X150_765, X33_766) | ~c2_1(X150_765) | c4_2(X150_765, a545) | ~c2_2(X150_765, X34_767) | ~c10_2(X150_765, X34_767) | ~c4_2(X150_765, X34_767) | c6_2(X150_765, X34_767) | c4_2(X150_765, X33_766) | c6_1(X150_765) | c2_2(X150_765, a511) | c10_2(X150_765, a511) | ~ndr1_1(X150_765) | c10_1(X150_765)))).
% 34.43/14.17  tff(c_16626, plain, (![X32_795, X33_796, X34_797]: (c3_2(X32_795, X33_796) | c1_1(X32_795) | ~c10_2(X32_795, X33_796) | c1_2(X32_795, a511) | ~c2_2(X32_795, X33_796) | ~c2_1(X32_795) | ~c2_2(X32_795, X34_797) | ~c10_2(X32_795, X34_797) | c2_2(X32_795, a545) | c10_2(X32_795, a545) | c10_1(X32_795) | ~c4_2(X32_795, X34_797) | c6_2(X32_795, X34_797) | c4_2(X32_795, X33_796) | ~ndr1_1(X32_795) | c6_1(X32_795)))).
% 34.43/14.17  tff(c_16700, plain, (![X150_798, X33_799, X34_800]: (c3_2(X150_798, X33_799) | c1_1(X150_798) | ~c10_2(X150_798, X33_799) | ~c2_2(X150_798, X33_799) | ~c2_1(X150_798) | c6_2(X150_798, a545) | ~c2_2(X150_798, X34_800) | ~c10_2(X150_798, X34_800) | ~c4_2(X150_798, X34_800) | c6_2(X150_798, X34_800) | c4_2(X150_798, X33_799) | c6_1(X150_798) | c2_2(X150_798, a511) | c10_2(X150_798, a511) | ~ndr1_1(X150_798) | c10_1(X150_798)))).
% 34.43/14.17  tff(c_16534, plain, (![X32_784, X33_785, X34_786]: (c3_2(X32_784, X33_785) | c1_1(X32_784) | ~c10_2(X32_784, X33_785) | c4_2(X32_784, a511) | ~c2_2(X32_784, X33_785) | ~c2_1(X32_784) | ~c2_2(X32_784, X34_786) | ~c10_2(X32_784, X34_786) | c2_2(X32_784, a545) | c10_2(X32_784, a545) | c10_1(X32_784) | ~c4_2(X32_784, X34_786) | c6_2(X32_784, X34_786) | c4_2(X32_784, X33_785) | ~ndr1_1(X32_784) | c6_1(X32_784)))).
% 34.43/14.17  tff(c_15934, plain, (![U_1, X33_726, X34_728]: (~c1_2(U_1, X33_726) | ~c3_1(U_1) | c4_2(U_1, a545) | ~c2_2(U_1, X34_728) | ~c10_2(U_1, X34_728) | c6_2(U_1, a505) | ~c10_2(U_1, X33_726) | c2_2(U_1, X33_726) | c1_1(U_1) | ~c4_2(U_1, X34_728) | c6_2(U_1, X34_728) | c4_2(U_1, X33_726) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_15974, plain, (![U_1, X33_734, X34_736]: (~c1_2(U_1, X33_734) | ~c3_1(U_1) | c6_2(U_1, a545) | ~c2_2(U_1, X34_736) | ~c10_2(U_1, X34_736) | ~c3_2(U_1, a505) | ~c10_2(U_1, X33_734) | c2_2(U_1, X33_734) | c1_1(U_1) | ~c4_2(U_1, X34_736) | c6_2(U_1, X34_736) | c4_2(U_1, X33_734) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16476, plain, (![U_1, X33_781, X34_783]: (~c1_2(U_1, X33_781) | ~c3_1(U_1) | ~c10_2(U_1, X33_781) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | c1_2(U_1, a511) | ~c2_2(U_1, X33_781) | ~c4_2(U_1, X34_783) | c8_2(U_1, X34_783) | c6_2(U_1, X34_783) | c4_2(U_1, X33_781) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_12819, plain, (![U_543, X34_545, X33_544]: (c4_2(U_543, a545) | ~c2_2(U_543, X34_545) | ~c10_2(U_543, X34_545) | ~c1_2(U_543, X33_544) | ~c3_1(U_543) | ~c3_2(U_543, a505) | ~c10_2(U_543, X33_544) | c2_2(U_543, X33_544) | c1_1(U_543) | ~c4_2(U_543, X34_545) | c6_2(U_543, X34_545) | c4_2(U_543, X33_544) | ~ndr1_1(U_543) | c6_1(U_543) | ~c10_2(U_543, a431) | ~c2_1(U_543)))).
% 34.43/14.17  tff(c_15954, plain, (![U_1, X33_730, X34_732]: (~c1_2(U_1, X33_730) | ~c3_1(U_1) | c6_2(U_1, a545) | ~c2_2(U_1, X34_732) | ~c10_2(U_1, X34_732) | c6_2(U_1, a505) | ~c10_2(U_1, X33_730) | c2_2(U_1, X33_730) | c1_1(U_1) | ~c4_2(U_1, X34_732) | c6_2(U_1, X34_732) | c4_2(U_1, X33_730) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16270, plain, (![U_1, X33_755, X34_757]: (~c1_2(U_1, X33_755) | ~c3_1(U_1) | ~c10_2(U_1, X33_755) | c2_2(U_1, a545) | c10_2(U_1, a545) | c10_1(U_1) | c4_2(U_1, a511) | ~c2_2(U_1, X33_755) | ~c4_2(U_1, X34_757) | c8_2(U_1, X34_757) | c6_2(U_1, X34_757) | c4_2(U_1, X33_755) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_15723, plain, (![X150_709, X33_710, X34_711]: (c3_2(X150_709, X33_710) | c1_1(X150_709) | ~c10_2(X150_709, X33_710) | c2_2(X150_709, a545) | c10_2(X150_709, a545) | ~c2_2(X150_709, X33_710) | ~c2_1(X150_709) | ~c4_2(X150_709, X34_711) | c8_2(X150_709, X34_711) | c6_2(X150_709, X34_711) | c4_2(X150_709, X33_710) | c6_1(X150_709) | c2_2(X150_709, a511) | c10_2(X150_709, a511) | ~ndr1_1(X150_709) | c10_1(X150_709)))).
% 34.43/14.17  tff(c_14591, plain, (![X32_658, X33_659, X143_188]: (~c1_2(X32_658, X33_659) | ~c10_2(X32_658, X143_188) | ~c3_1(X32_658) | ~c2_2(X32_658, a505) | ~c10_2(X32_658, a505) | c2_2(X32_658, a545) | c10_2(X32_658, a545) | c10_1(X32_658) | ~c10_2(X32_658, X33_659) | c2_2(X32_658, X33_659) | c1_1(X32_658) | ~c4_2(X32_658, a505) | c4_2(X32_658, X33_659) | ~ndr1_1(X32_658) | c6_1(X32_658) | c6_2(X32_658, a505)))).
% 34.43/14.17  tff(c_13435, plain, (![X150_584, X33_585, X143_188, X34_586]: (~c1_2(X150_584, X33_585) | ~c10_2(X150_584, X143_188) | ~c3_1(X150_584) | c6_2(X150_584, a545) | ~c10_2(X150_584, X33_585) | ~c2_2(X150_584, X33_585) | ~c2_1(X150_584) | ~c4_2(X150_584, X34_586) | c8_2(X150_584, X34_586) | c6_2(X150_584, X34_586) | c4_2(X150_584, X33_585) | c6_1(X150_584) | c2_2(X150_584, a511) | c10_2(X150_584, a511) | ~ndr1_1(X150_584) | c10_1(X150_584)))).
% 34.43/14.17  tff(c_13373, plain, (![X150_581, X33_582, X143_188, X34_583]: (~c1_2(X150_581, X33_582) | ~c10_2(X150_581, X143_188) | ~c3_1(X150_581) | c4_2(X150_581, a545) | ~c10_2(X150_581, X33_582) | ~c2_2(X150_581, X33_582) | ~c2_1(X150_581) | ~c4_2(X150_581, X34_583) | c8_2(X150_581, X34_583) | c6_2(X150_581, X34_583) | c4_2(X150_581, X33_582) | c6_1(X150_581) | c2_2(X150_581, a511) | c10_2(X150_581, a511) | ~ndr1_1(X150_581) | c10_1(X150_581)))).
% 34.43/14.17  tff(c_17363, plain, (![U_1, X33_848]: (~c1_2(U_1, X33_848) | ~c3_1(U_1) | ~c1_1(U_1) | c8_1(U_1) | ~c2_2(U_1, a576) | ~c10_2(U_1, a576) | c6_2(U_1, a545) | ~c10_2(U_1, X33_848) | c1_2(U_1, a511) | ~c2_2(U_1, X33_848) | ~c4_2(U_1, a576) | c4_2(U_1, X33_848) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_17325, plain, (![U_1, X33_842]: (~c1_2(U_1, X33_842) | ~c3_1(U_1) | ~c1_1(U_1) | c8_1(U_1) | ~c10_2(U_1, X33_842) | c4_2(U_1, a511) | ~c2_2(U_1, X33_842) | c4_2(U_1, a545) | ~c2_2(U_1, a576) | ~c10_2(U_1, a576) | ~c4_2(U_1, a576) | c4_2(U_1, X33_842) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_17344, plain, (![U_1, X33_845]: (~c1_2(U_1, X33_845) | ~c3_1(U_1) | ~c1_1(U_1) | c8_1(U_1) | ~c10_2(U_1, X33_845) | c4_2(U_1, a511) | ~c2_2(U_1, X33_845) | c6_2(U_1, a545) | ~c2_2(U_1, a576) | ~c10_2(U_1, a576) | ~c4_2(U_1, a576) | c4_2(U_1, X33_845) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_17284, plain, (![U_1, X33_835]: (~c1_2(U_1, X33_835) | ~c3_1(U_1) | ~c1_1(U_1) | c8_1(U_1) | ~c2_2(U_1, a576) | ~c10_2(U_1, a576) | c4_2(U_1, a545) | ~c10_2(U_1, X33_835) | c1_2(U_1, a511) | ~c2_2(U_1, X33_835) | ~c4_2(U_1, a576) | c4_2(U_1, X33_835) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16172, plain, (![X150_747, X33_749]: (~c1_1(X150_747) | c8_1(X150_747) | ~c2_2(X150_747, a576) | ~c10_2(X150_747, a576) | c6_2(X150_747, a545) | ~c10_2(X150_747, X33_749) | ~c2_2(X150_747, X33_749) | ~c2_1(X150_747) | ~c4_2(X150_747, a576) | c5_2(X150_747, X33_749) | c4_2(X150_747, X33_749) | c6_1(X150_747) | c2_2(X150_747, a511) | c10_2(X150_747, a511) | ~ndr1_1(X150_747) | c10_1(X150_747)))).
% 34.43/14.17  tff(c_16329, plain, (![X150_762, X33_764]: (~c1_1(X150_762) | c8_1(X150_762) | ~c2_2(X150_762, a576) | ~c10_2(X150_762, a576) | c4_2(X150_762, a545) | ~c10_2(X150_762, X33_764) | ~c2_2(X150_762, X33_764) | ~c2_1(X150_762) | ~c4_2(X150_762, a576) | c5_2(X150_762, X33_764) | c4_2(X150_762, X33_764) | c6_1(X150_762) | c2_2(X150_762, a511) | c10_2(X150_762, a511) | ~ndr1_1(X150_762) | c10_1(X150_762)))).
% 34.43/14.17  tff(c_12982, plain, (![X32_553, X33_554, X143_188]: (~c1_2(X32_553, X33_554) | ~c10_2(X32_553, X143_188) | ~c3_1(X32_553) | ~c1_1(X32_553) | c8_1(X32_553) | ~c2_2(X32_553, a576) | ~c10_2(X32_553, a576) | c6_2(X32_553, a545) | ~c10_2(X32_553, X33_554) | c1_2(X32_553, a511) | ~c2_2(X32_553, X33_554) | ~c2_1(X32_553) | ~c4_2(X32_553, a576) | c4_2(X32_553, X33_554) | ~ndr1_1(X32_553) | c6_1(X32_553)))).
% 34.43/14.17  tff(c_13018, plain, (![X32_555, X33_556, X143_188]: (~c1_2(X32_555, X33_556) | ~c10_2(X32_555, X143_188) | ~c3_1(X32_555) | ~c1_1(X32_555) | c8_1(X32_555) | ~c10_2(X32_555, X33_556) | c4_2(X32_555, a511) | ~c2_2(X32_555, X33_556) | ~c2_1(X32_555) | c6_2(X32_555, a545) | ~c2_2(X32_555, a576) | ~c10_2(X32_555, a576) | ~c4_2(X32_555, a576) | c4_2(X32_555, X33_556) | ~ndr1_1(X32_555) | c6_1(X32_555)))).
% 34.43/14.17  tff(c_13048, plain, (![X32_557, X33_558, X143_188]: (~c1_2(X32_557, X33_558) | ~c10_2(X32_557, X143_188) | ~c3_1(X32_557) | ~c1_1(X32_557) | c8_1(X32_557) | ~c10_2(X32_557, X33_558) | c4_2(X32_557, a511) | ~c2_2(X32_557, X33_558) | ~c2_1(X32_557) | c4_2(X32_557, a545) | ~c2_2(X32_557, a576) | ~c10_2(X32_557, a576) | ~c4_2(X32_557, a576) | c4_2(X32_557, X33_558) | ~ndr1_1(X32_557) | c6_1(X32_557)))).
% 34.43/14.17  tff(c_14875, plain, (![X32_665, X33_667, X143_188, X34_666]: (~c1_2(X32_665, X33_667) | ~c10_2(X32_665, X143_188) | ~c3_1(X32_665) | ~c2_2(X32_665, X34_666) | ~c10_2(X32_665, X34_666) | c2_2(X32_665, a545) | c10_2(X32_665, a545) | c10_1(X32_665) | ~c3_2(X32_665, a505) | ~c10_2(X32_665, X33_667) | c2_2(X32_665, X33_667) | c1_1(X32_665) | ~c4_2(X32_665, X34_666) | c6_2(X32_665, X34_666) | c4_2(X32_665, X33_667) | ~ndr1_1(X32_665) | c6_1(X32_665)))).
% 34.43/14.17  tff(c_12938, plain, (![X32_551, X33_552, X143_188]: (~c1_2(X32_551, X33_552) | ~c10_2(X32_551, X143_188) | ~c3_1(X32_551) | ~c1_1(X32_551) | c8_1(X32_551) | ~c2_2(X32_551, a576) | ~c10_2(X32_551, a576) | c4_2(X32_551, a545) | ~c10_2(X32_551, X33_552) | c1_2(X32_551, a511) | ~c2_2(X32_551, X33_552) | ~c2_1(X32_551) | ~c4_2(X32_551, a576) | c4_2(X32_551, X33_552) | ~ndr1_1(X32_551) | c6_1(X32_551)))).
% 34.43/14.17  tff(c_15508, plain, (![X32_700, X33_702]: (~c1_1(X32_700) | c8_1(X32_700) | ~c2_2(X32_700, a576) | ~c10_2(X32_700, a576) | ~c10_2(X32_700, X33_702) | c2_2(X32_700, a545) | c10_2(X32_700, a545) | c10_1(X32_700) | c1_2(X32_700, a511) | ~c2_2(X32_700, X33_702) | ~c2_1(X32_700) | ~c4_2(X32_700, a576) | c5_2(X32_700, X33_702) | c4_2(X32_700, X33_702) | ~ndr1_1(X32_700) | c6_1(X32_700)))).
% 34.43/14.17  tff(c_15813, plain, (![X32_715, X33_717]: (~c1_1(X32_715) | c8_1(X32_715) | ~c2_2(X32_715, a576) | ~c10_2(X32_715, a576) | ~c10_2(X32_715, X33_717) | c2_2(X32_715, a545) | c10_2(X32_715, a545) | c10_1(X32_715) | c4_2(X32_715, a511) | ~c2_2(X32_715, X33_717) | ~c2_1(X32_715) | ~c4_2(X32_715, a576) | c5_2(X32_715, X33_717) | c4_2(X32_715, X33_717) | ~ndr1_1(X32_715) | c6_1(X32_715)))).
% 34.43/14.17  tff(c_15713, plain, (![X150_709, X33_710]: (~c9_1(X150_709) | ~c1_1(X150_709) | ~c10_2(X150_709, X33_710) | c2_2(X150_709, a545) | c10_2(X150_709, a545) | ~c2_2(X150_709, X33_710) | ~c2_1(X150_709) | ~c4_2(X150_709, a518) | c6_2(X150_709, a518) | c5_2(X150_709, X33_710) | c4_2(X150_709, X33_710) | c6_1(X150_709) | c2_2(X150_709, a511) | c10_2(X150_709, a511) | ~ndr1_1(X150_709) | c10_1(X150_709)))).
% 34.43/14.17  tff(c_14561, plain, (![X32_655, X33_657, X143_188, X34_656]: (~c1_2(X32_655, X33_657) | ~c10_2(X32_655, X143_188) | ~c3_1(X32_655) | ~c2_2(X32_655, X34_656) | ~c10_2(X32_655, X34_656) | c2_2(X32_655, a545) | c10_2(X32_655, a545) | c10_1(X32_655) | c6_2(X32_655, a505) | ~c10_2(X32_655, X33_657) | c2_2(X32_655, X33_657) | c1_1(X32_655) | ~c4_2(X32_655, X34_656) | c6_2(X32_655, X34_656) | c4_2(X32_655, X33_657) | ~ndr1_1(X32_655) | c6_1(X32_655)))).
% 34.43/14.17  tff(c_16108, plain, (![U_1, X33_744, X34_746]: (~c1_2(U_1, X33_744) | ~c3_1(U_1) | ~c10_2(U_1, X33_744) | c4_2(U_1, a511) | ~c2_2(U_1, X33_744) | c4_2(U_1, a545) | ~c2_2(U_1, X34_746) | ~c10_2(U_1, X34_746) | ~c4_2(U_1, X34_746) | c6_2(U_1, X34_746) | c4_2(U_1, X33_744) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16436, plain, (![U_1, X33_773, X34_775]: (~c1_2(U_1, X33_773) | ~c3_1(U_1) | ~c10_2(U_1, X33_773) | c4_2(U_1, a511) | ~c2_2(U_1, X33_773) | c6_2(U_1, a545) | ~c2_2(U_1, X34_775) | ~c10_2(U_1, X34_775) | ~c4_2(U_1, X34_775) | c6_2(U_1, X34_775) | c4_2(U_1, X33_773) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16455, plain, (![U_1, X33_777, X34_779]: (~c1_2(U_1, X33_777) | ~c3_1(U_1) | ~c10_2(U_1, X33_777) | c1_2(U_1, a511) | ~c2_2(U_1, X33_777) | c4_2(U_1, a545) | ~c2_2(U_1, X34_779) | ~c10_2(U_1, X34_779) | ~c4_2(U_1, X34_779) | c6_2(U_1, X34_779) | c4_2(U_1, X33_777) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_16569, plain, (![U_1, X33_792, X34_794]: (~c1_2(U_1, X33_792) | ~c3_1(U_1) | ~c10_2(U_1, X33_792) | c1_2(U_1, a511) | ~c2_2(U_1, X33_792) | c6_2(U_1, a545) | ~c2_2(U_1, X34_794) | ~c10_2(U_1, X34_794) | ~c4_2(U_1, X34_794) | c6_2(U_1, X34_794) | c4_2(U_1, X33_792) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.17  tff(c_12452, plain, (![X150_516, X34_518, X33_517]: (~c2_2(X150_516, X34_518) | ~c10_2(X150_516, X34_518) | c2_2(X150_516, a545) | c10_2(X150_516, a545) | ~c2_2(X150_516, X33_517) | c8_2(X150_516, X33_517) | ~c2_1(X150_516) | ~c4_2(X150_516, X34_518) | c6_2(X150_516, X34_518) | c5_2(X150_516, X33_517) | c4_2(X150_516, X33_517) | c6_1(X150_516) | c2_2(X150_516, a511) | c10_2(X150_516, a511) | ~ndr1_1(X150_516) | c10_1(X150_516)))).
% 34.43/14.17  tff(c_15580, plain, (![X150_703, X33_704, X34_705]: (~c10_2(X150_703, X33_704) | ~c2_2(X150_703, X33_704) | ~c2_1(X150_703) | c6_2(X150_703, a545) | ~c2_2(X150_703, X34_705) | ~c10_2(X150_703, X34_705) | ~c4_2(X150_703, X34_705) | c6_2(X150_703, X34_705) | c5_2(X150_703, X33_704) | c4_2(X150_703, X33_704) | c6_1(X150_703) | c2_2(X150_703, a511) | c10_2(X150_703, a511) | ~ndr1_1(X150_703) | c10_1(X150_703)))).
% 34.43/14.17  tff(c_14146, plain, (![X32_630, X33_631, X34_632]: (~c10_2(X32_630, X33_631) | c1_2(X32_630, a511) | ~c2_2(X32_630, X33_631) | ~c2_1(X32_630) | ~c2_2(X32_630, X34_632) | ~c10_2(X32_630, X34_632) | c2_2(X32_630, a545) | c10_2(X32_630, a545) | c10_1(X32_630) | ~c4_2(X32_630, X34_632) | c6_2(X32_630, X34_632) | c5_2(X32_630, X33_631) | c4_2(X32_630, X33_631) | ~ndr1_1(X32_630) | c6_1(X32_630)))).
% 34.43/14.17  tff(c_12695, plain, (![X32_405, X33_406, X143_526, X34_407]: (~c1_2(X32_405, X33_406) | ~c10_2(X32_405, X143_526) | ~c3_1(X32_405) | ~c10_2(X32_405, X33_406) | c1_2(X32_405, a511) | ~c2_2(X32_405, X33_406) | ~c2_1(X32_405) | c6_2(X32_405, a545) | ~c2_2(X32_405, X34_407) | ~c10_2(X32_405, X34_407) | ~c4_2(X32_405, X34_407) | c6_2(X32_405, X34_407) | c4_2(X32_405, X33_406) | ~ndr1_1(X32_405) | c6_1(X32_405)))).
% 34.43/14.17  tff(c_14472, plain, (![X32_652, X33_653, X34_654]: (~c10_2(X32_652, X33_653) | c4_2(X32_652, a511) | ~c2_2(X32_652, X33_653) | ~c2_1(X32_652) | ~c2_2(X32_652, X34_654) | ~c10_2(X32_652, X34_654) | c2_2(X32_652, a545) | c10_2(X32_652, a545) | c10_1(X32_652) | ~c4_2(X32_652, X34_654) | c6_2(X32_652, X34_654) | c5_2(X32_652, X33_653) | c4_2(X32_652, X33_653) | ~ndr1_1(X32_652) | c6_1(X32_652)))).
% 34.43/14.17  tff(c_13192, plain, (![X32_563, X33_564, X143_188, X34_565]: (~c1_2(X32_563, X33_564) | ~c10_2(X32_563, X143_188) | ~c3_1(X32_563) | ~c10_2(X32_563, X33_564) | c2_2(X32_563, a545) | c10_2(X32_563, a545) | c10_1(X32_563) | c1_2(X32_563, a511) | ~c2_2(X32_563, X33_564) | ~c2_1(X32_563) | ~c4_2(X32_563, X34_565) | c8_2(X32_563, X34_565) | c6_2(X32_563, X34_565) | c4_2(X32_563, X33_564) | ~ndr1_1(X32_563) | c6_1(X32_563)))).
% 34.43/14.17  tff(c_12693, plain, (![X32_399, X33_400, X143_526, X34_401]: (~c1_2(X32_399, X33_400) | ~c10_2(X32_399, X143_526) | ~c3_1(X32_399) | ~c10_2(X32_399, X33_400) | c1_2(X32_399, a511) | ~c2_2(X32_399, X33_400) | ~c2_1(X32_399) | c4_2(X32_399, a545) | ~c2_2(X32_399, X34_401) | ~c10_2(X32_399, X34_401) | ~c4_2(X32_399, X34_401) | c6_2(X32_399, X34_401) | c4_2(X32_399, X33_400) | ~ndr1_1(X32_399) | c6_1(X32_399)))).
% 34.43/14.17  tff(c_12696, plain, (![X32_402, X33_403, X143_526, X34_404]: (~c1_2(X32_402, X33_403) | ~c10_2(X32_402, X143_526) | ~c3_1(X32_402) | ~c10_2(X32_402, X33_403) | c4_2(X32_402, a511) | ~c2_2(X32_402, X33_403) | ~c2_1(X32_402) | c6_2(X32_402, a545) | ~c2_2(X32_402, X34_404) | ~c10_2(X32_402, X34_404) | ~c4_2(X32_402, X34_404) | c6_2(X32_402, X34_404) | c4_2(X32_402, X33_403) | ~ndr1_1(X32_402) | c6_1(X32_402)))).
% 34.43/14.17  tff(c_15459, plain, (![X150_697, X33_698, X34_699]: (~c10_2(X150_697, X33_698) | ~c2_2(X150_697, X33_698) | ~c2_1(X150_697) | c4_2(X150_697, a545) | ~c2_2(X150_697, X34_699) | ~c10_2(X150_697, X34_699) | ~c4_2(X150_697, X34_699) | c6_2(X150_697, X34_699) | c5_2(X150_697, X33_698) | c4_2(X150_697, X33_698) | c6_1(X150_697) | c2_2(X150_697, a511) | c10_2(X150_697, a511) | ~ndr1_1(X150_697) | c10_1(X150_697)))).
% 34.43/14.17  tff(c_13366, plain, (![X150_581, X34_583, X33_582]: (~c2_2(X150_581, X34_583) | ~c10_2(X150_581, X34_583) | c4_2(X150_581, a545) | ~c10_2(X150_581, X33_582) | ~c2_2(X150_581, X33_582) | ~c2_1(X150_581) | ~c4_2(X150_581, X34_583) | c6_2(X150_581, X34_583) | c5_2(X150_581, X33_582) | c4_2(X150_581, X33_582) | c6_1(X150_581) | c2_2(X150_581, a511) | c10_2(X150_581, a511) | ~ndr1_1(X150_581) | c10_1(X150_581)))).
% 34.43/14.18  tff(c_13254, plain, (![X32_566, X33_567, X143_188, X34_568]: (~c1_2(X32_566, X33_567) | ~c10_2(X32_566, X143_188) | ~c3_1(X32_566) | ~c10_2(X32_566, X33_567) | c2_2(X32_566, a545) | c10_2(X32_566, a545) | c10_1(X32_566) | c4_2(X32_566, a511) | ~c2_2(X32_566, X33_567) | ~c2_1(X32_566) | ~c4_2(X32_566, X34_568) | c8_2(X32_566, X34_568) | c6_2(X32_566, X34_568) | c4_2(X32_566, X33_567) | ~ndr1_1(X32_566) | c6_1(X32_566)))).
% 34.43/14.18  tff(c_16215, plain, (![X150_750, X33_751]: (c3_2(X150_750, X33_751) | c1_1(X150_750) | ~c2_2(X150_750, a545) | ~c10_2(X150_750, a545) | ~c10_2(X150_750, X33_751) | ~c2_2(X150_750, X33_751) | ~c2_1(X150_750) | ~c4_2(X150_750, a545) | c4_2(X150_750, X33_751) | c6_1(X150_750) | c2_2(X150_750, a511) | c10_2(X150_750, a511) | ~ndr1_1(X150_750) | c10_1(X150_750) | c6_2(X150_750, a545)))).
% 34.43/14.18  tff(c_16124, plain, (![X150_584, X33_585]: (~c2_2(X150_584, a545) | ~c10_2(X150_584, a545) | ~c10_2(X150_584, X33_585) | ~c2_2(X150_584, X33_585) | ~c2_1(X150_584) | ~c4_2(X150_584, a545) | c5_2(X150_584, X33_585) | c4_2(X150_584, X33_585) | c6_1(X150_584) | c2_2(X150_584, a511) | c10_2(X150_584, a511) | ~ndr1_1(X150_584) | c10_1(X150_584) | c6_2(X150_584, a545)))).
% 34.43/14.18  tff(c_13429, plain, (![X150_584, X34_586, X33_585]: (~c2_2(X150_584, X34_586) | ~c10_2(X150_584, X34_586) | c6_2(X150_584, a545) | ~c10_2(X150_584, X33_585) | ~c2_2(X150_584, X33_585) | ~c2_1(X150_584) | ~c4_2(X150_584, X34_586) | c6_2(X150_584, X34_586) | c5_2(X150_584, X33_585) | c4_2(X150_584, X33_585) | c6_1(X150_584) | c2_2(X150_584, a511) | c10_2(X150_584, a511) | ~ndr1_1(X150_584) | c10_1(X150_584)))).
% 34.43/14.18  tff(c_12694, plain, (![X32_396, X33_397, X143_526, X34_398]: (~c1_2(X32_396, X33_397) | ~c10_2(X32_396, X143_526) | ~c3_1(X32_396) | ~c10_2(X32_396, X33_397) | c4_2(X32_396, a511) | ~c2_2(X32_396, X33_397) | ~c2_1(X32_396) | c4_2(X32_396, a545) | ~c2_2(X32_396, X34_398) | ~c10_2(X32_396, X34_398) | ~c4_2(X32_396, X34_398) | c6_2(X32_396, X34_398) | c4_2(X32_396, X33_397) | ~ndr1_1(X32_396) | c6_1(X32_396)))).
% 34.43/14.18  tff(c_12258, plain, (![X32_469, X34_471, X33_470]: (~c2_2(X32_469, X34_471) | ~c10_2(X32_469, X34_471) | c2_2(X32_469, a545) | c10_2(X32_469, a545) | c10_1(X32_469) | c3_2(X32_469, X33_470) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, X34_471) | c6_2(X32_469, X34_471) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469)))).
% 34.43/14.18  tff(c_12260, plain, (![X32_426, X34_428, X33_427]: (~c2_2(X32_426, X34_428) | ~c10_2(X32_426, X34_428) | c2_2(X32_426, a545) | c10_2(X32_426, a545) | c10_1(X32_426) | c3_2(X32_426, X33_427) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, X34_428) | c6_2(X32_426, X34_428) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426)))).
% 34.43/14.18  tff(c_12702, plain, (![X32_426, X33_427, X143_526, X34_428]: (~c1_2(X32_426, X33_427) | ~c10_2(X32_426, X143_526) | ~c3_1(X32_426) | c6_2(X32_426, a545) | ~c2_2(X32_426, X34_428) | ~c10_2(X32_426, X34_428) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, X34_428) | c6_2(X32_426, X34_428) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426)))).
% 34.43/14.18  tff(c_12691, plain, (![X32_469, X33_470, X143_526, X34_471]: (~c1_2(X32_469, X33_470) | ~c10_2(X32_469, X143_526) | ~c3_1(X32_469) | c6_2(X32_469, a545) | ~c2_2(X32_469, X34_471) | ~c10_2(X32_469, X34_471) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, X34_471) | c6_2(X32_469, X34_471) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469)))).
% 34.43/14.18  tff(c_12689, plain, (![X32_469, X33_470, X143_526, X34_471]: (~c1_2(X32_469, X33_470) | ~c10_2(X32_469, X143_526) | ~c3_1(X32_469) | c4_2(X32_469, a545) | ~c2_2(X32_469, X34_471) | ~c10_2(X32_469, X34_471) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, X34_471) | c6_2(X32_469, X34_471) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469)))).
% 34.43/14.18  tff(c_12458, plain, (![X150_516, X34_518, X33_517]: (c6_2(X150_516, a545) | ~c2_2(X150_516, X34_518) | ~c10_2(X150_516, X34_518) | ~c2_2(X150_516, X33_517) | c8_2(X150_516, X33_517) | ~c2_1(X150_516) | ~c4_2(X150_516, X34_518) | c6_2(X150_516, X34_518) | c5_2(X150_516, X33_517) | c4_2(X150_516, X33_517) | c6_1(X150_516) | c2_2(X150_516, a511) | c10_2(X150_516, a511) | ~ndr1_1(X150_516) | c10_1(X150_516)))).
% 34.43/14.18  tff(c_12700, plain, (![X32_426, X33_427, X143_526, X34_428]: (~c1_2(X32_426, X33_427) | ~c10_2(X32_426, X143_526) | ~c3_1(X32_426) | c4_2(X32_426, a545) | ~c2_2(X32_426, X34_428) | ~c10_2(X32_426, X34_428) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, X34_428) | c6_2(X32_426, X34_428) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426)))).
% 34.43/14.18  tff(c_13242, plain, (![X32_566, X34_568, X33_567]: (~c2_2(X32_566, X34_568) | ~c10_2(X32_566, X34_568) | ~c10_2(X32_566, X33_567) | c2_2(X32_566, a545) | c10_2(X32_566, a545) | c10_1(X32_566) | c4_2(X32_566, a511) | ~c2_2(X32_566, X33_567) | ~c2_1(X32_566) | ~c4_2(X32_566, X34_568) | c6_2(X32_566, X34_568) | c5_2(X32_566, X33_567) | c4_2(X32_566, X33_567) | ~ndr1_1(X32_566) | c6_1(X32_566)))).
% 34.43/14.18  tff(c_12440, plain, (![X150_516, X33_517, X34_518]: (~c10_2(X150_516, X33_517) | c2_2(X150_516, a545) | c10_2(X150_516, a545) | ~c2_2(X150_516, X33_517) | ~c2_1(X150_516) | ~c4_2(X150_516, X34_518) | c8_2(X150_516, X34_518) | c6_2(X150_516, X34_518) | c5_2(X150_516, X33_517) | c4_2(X150_516, X33_517) | c6_1(X150_516) | c2_2(X150_516, a511) | c10_2(X150_516, a511) | ~ndr1_1(X150_516) | c10_1(X150_516)))).
% 34.43/14.18  tff(c_12457, plain, (![X150_516, X34_518, X33_517]: (c4_2(X150_516, a545) | ~c2_2(X150_516, X34_518) | ~c10_2(X150_516, X34_518) | ~c2_2(X150_516, X33_517) | c8_2(X150_516, X33_517) | ~c2_1(X150_516) | ~c4_2(X150_516, X34_518) | c6_2(X150_516, X34_518) | c5_2(X150_516, X33_517) | c4_2(X150_516, X33_517) | c6_1(X150_516) | c2_2(X150_516, a511) | c10_2(X150_516, a511) | ~ndr1_1(X150_516) | c10_1(X150_516)))).
% 34.43/14.18  tff(c_12131, plain, (![X150_508, X33_327, X34_326]: (~c2_2(X150_508, X33_327) | c8_2(X150_508, X33_327) | ~c2_1(X150_508) | c6_2(X150_508, a545) | ~c2_2(X150_508, X34_326) | ~c10_2(X150_508, X34_326) | ~c4_2(X150_508, X34_326) | c6_2(X150_508, X34_326) | c5_2(X150_508, X33_327) | c4_2(X150_508, X33_327) | c6_1(X150_508) | c2_2(X150_508, a511) | c10_2(X150_508, a511) | ~ndr1_1(X150_508) | c10_1(X150_508)))).
% 34.43/14.18  tff(c_13180, plain, (![X32_563, X34_565, X33_564]: (~c2_2(X32_563, X34_565) | ~c10_2(X32_563, X34_565) | ~c10_2(X32_563, X33_564) | c2_2(X32_563, a545) | c10_2(X32_563, a545) | c10_1(X32_563) | c1_2(X32_563, a511) | ~c2_2(X32_563, X33_564) | ~c2_1(X32_563) | ~c4_2(X32_563, X34_565) | c6_2(X32_563, X34_565) | c5_2(X32_563, X33_564) | c4_2(X32_563, X33_564) | ~ndr1_1(X32_563) | c6_1(X32_563)))).
% 34.43/14.18  tff(c_12132, plain, (![X150_508, X33_330, X34_329]: (~c2_2(X150_508, X33_330) | c8_2(X150_508, X33_330) | ~c2_1(X150_508) | c4_2(X150_508, a545) | ~c2_2(X150_508, X34_329) | ~c10_2(X150_508, X34_329) | ~c4_2(X150_508, X34_329) | c6_2(X150_508, X34_329) | c5_2(X150_508, X33_330) | c4_2(X150_508, X33_330) | c6_1(X150_508) | c2_2(X150_508, a511) | c10_2(X150_508, a511) | ~ndr1_1(X150_508) | c10_1(X150_508)))).
% 34.43/14.18  tff(c_13993, plain, (![U_1, X33_622]: (~c1_2(U_1, X33_622) | ~c3_1(U_1) | ~c2_2(U_1, a545) | ~c10_2(U_1, a545) | c6_2(U_1, a505) | ~c10_2(U_1, X33_622) | c2_2(U_1, X33_622) | c1_1(U_1) | ~c4_2(U_1, a545) | c4_2(U_1, X33_622) | ~ndr1_1(U_1) | c6_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_13776, plain, (![U_1, X33_607]: (~c1_2(U_1, X33_607) | ~c3_1(U_1) | c4_2(U_1, a545) | ~c2_2(U_1, a505) | ~c10_2(U_1, a505) | ~c10_2(U_1, X33_607) | c2_2(U_1, X33_607) | c1_1(U_1) | ~c4_2(U_1, a505) | c4_2(U_1, X33_607) | ~ndr1_1(U_1) | c6_1(U_1) | c6_2(U_1, a505) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_13796, plain, (![U_1, X33_610]: (~c1_2(U_1, X33_610) | ~c3_1(U_1) | ~c2_2(U_1, a545) | ~c10_2(U_1, a545) | ~c3_2(U_1, a505) | ~c10_2(U_1, X33_610) | c2_2(U_1, X33_610) | c1_1(U_1) | ~c4_2(U_1, a545) | c4_2(U_1, X33_610) | ~ndr1_1(U_1) | c6_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_13378, plain, (![X150_581, X33_582, X34_583]: (c3_2(X150_581, X33_582) | c1_1(X150_581) | c4_2(X150_581, a545) | ~c10_2(X150_581, X33_582) | ~c2_2(X150_581, X33_582) | ~c2_1(X150_581) | ~c4_2(X150_581, X34_583) | c8_2(X150_581, X34_583) | c6_2(X150_581, X34_583) | c4_2(X150_581, X33_582) | c6_1(X150_581) | c2_2(X150_581, a511) | c10_2(X150_581, a511) | ~ndr1_1(X150_581) | c10_1(X150_581)))).
% 34.43/14.18  tff(c_13440, plain, (![X150_584, X33_585, X34_586]: (c3_2(X150_584, X33_585) | c1_1(X150_584) | c6_2(X150_584, a545) | ~c10_2(X150_584, X33_585) | ~c2_2(X150_584, X33_585) | ~c2_1(X150_584) | ~c4_2(X150_584, X34_586) | c8_2(X150_584, X34_586) | c6_2(X150_584, X34_586) | c4_2(X150_584, X33_585) | c6_1(X150_584) | c2_2(X150_584, a511) | c10_2(X150_584, a511) | ~ndr1_1(X150_584) | c10_1(X150_584)))).
% 34.43/14.18  tff(c_13197, plain, (![X32_563, X33_564, X34_565]: (c3_2(X32_563, X33_564) | c1_1(X32_563) | ~c10_2(X32_563, X33_564) | c2_2(X32_563, a545) | c10_2(X32_563, a545) | c10_1(X32_563) | c1_2(X32_563, a511) | ~c2_2(X32_563, X33_564) | ~c2_1(X32_563) | ~c4_2(X32_563, X34_565) | c8_2(X32_563, X34_565) | c6_2(X32_563, X34_565) | c4_2(X32_563, X33_564) | ~ndr1_1(X32_563) | c6_1(X32_563)))).
% 34.43/14.18  tff(c_13259, plain, (![X32_566, X33_567, X34_568]: (c3_2(X32_566, X33_567) | c1_1(X32_566) | ~c10_2(X32_566, X33_567) | c2_2(X32_566, a545) | c10_2(X32_566, a545) | c10_1(X32_566) | c4_2(X32_566, a511) | ~c2_2(X32_566, X33_567) | ~c2_1(X32_566) | ~c4_2(X32_566, X34_568) | c8_2(X32_566, X34_568) | c6_2(X32_566, X34_568) | c4_2(X32_566, X33_567) | ~ndr1_1(X32_566) | c6_1(X32_566)))).
% 34.43/14.18  tff(c_13430, plain, (![X150_584, X33_585]: (~c9_1(X150_584) | ~c1_1(X150_584) | c6_2(X150_584, a545) | ~c10_2(X150_584, X33_585) | ~c2_2(X150_584, X33_585) | ~c2_1(X150_584) | ~c4_2(X150_584, a518) | c6_2(X150_584, a518) | c5_2(X150_584, X33_585) | c4_2(X150_584, X33_585) | c6_1(X150_584) | c2_2(X150_584, a511) | c10_2(X150_584, a511) | ~ndr1_1(X150_584) | c10_1(X150_584)))).
% 34.43/14.18  tff(c_13368, plain, (![X150_581, X33_582]: (~c9_1(X150_581) | ~c1_1(X150_581) | c4_2(X150_581, a545) | ~c10_2(X150_581, X33_582) | ~c2_2(X150_581, X33_582) | ~c2_1(X150_581) | ~c4_2(X150_581, a518) | c6_2(X150_581, a518) | c5_2(X150_581, X33_582) | c4_2(X150_581, X33_582) | c6_1(X150_581) | c2_2(X150_581, a511) | c10_2(X150_581, a511) | ~ndr1_1(X150_581) | c10_1(X150_581)))).
% 34.43/14.18  tff(c_12279, plain, (![X32_334, X33_335]: (~c10_2(X32_334, X33_335) | c2_2(X32_334, a545) | c10_2(X32_334, a545) | c10_1(X32_334) | ~c9_1(X32_334) | ~c1_1(X32_334) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, a518) | c6_2(X32_334, a518) | c5_2(X32_334, X33_335) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.18  tff(c_13187, plain, (![X32_563, X33_564]: (~c9_1(X32_563) | ~c1_1(X32_563) | ~c10_2(X32_563, X33_564) | c2_2(X32_563, a545) | c10_2(X32_563, a545) | c10_1(X32_563) | c1_2(X32_563, a511) | ~c2_2(X32_563, X33_564) | ~c2_1(X32_563) | ~c4_2(X32_563, a518) | c6_2(X32_563, a518) | c5_2(X32_563, X33_564) | c4_2(X32_563, X33_564) | ~ndr1_1(X32_563) | c6_1(X32_563)))).
% 34.43/14.18  tff(c_12261, plain, (![X32_47, X34_51, X33_50]: (~c2_2(X32_47, X34_51) | ~c10_2(X32_47, X34_51) | c2_2(X32_47, a545) | c10_2(X32_47, a545) | c10_1(X32_47) | ~c3_2(X32_47, a505) | ~c10_2(X32_47, X33_50) | c2_2(X32_47, X33_50) | c1_1(X32_47) | ~c4_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.18  tff(c_12364, plain, (![X32_513, X33_515, X34_514]: (~c8_2(X32_513, a511) | ~c2_2(X32_513, X33_515) | c8_2(X32_513, X33_515) | ~c2_1(X32_513) | ~c2_2(X32_513, X34_514) | ~c10_2(X32_513, X34_514) | c2_2(X32_513, a545) | c10_2(X32_513, a545) | c10_1(X32_513) | ~c4_2(X32_513, X34_514) | c6_2(X32_513, X34_514) | c5_2(X32_513, X33_515) | c4_2(X32_513, X33_515) | ~ndr1_1(X32_513) | c6_1(X32_513)))).
% 34.43/14.18  tff(c_14596, plain, (![X32_658, X33_659]: (c3_2(X32_658, X33_659) | ~c2_2(X32_658, a505) | ~c10_2(X32_658, a505) | c2_2(X32_658, a545) | c10_2(X32_658, a545) | c10_1(X32_658) | ~c10_2(X32_658, X33_659) | c2_2(X32_658, X33_659) | c1_1(X32_658) | ~c4_2(X32_658, a505) | c4_2(X32_658, X33_659) | ~ndr1_1(X32_658) | c6_1(X32_658) | c6_2(X32_658, a505)))).
% 34.43/14.18  tff(c_14503, plain, (![X32_47, X33_50]: (~c2_2(X32_47, a505) | ~c10_2(X32_47, a505) | c2_2(X32_47, a545) | c10_2(X32_47, a545) | c10_1(X32_47) | ~c10_2(X32_47, X33_50) | c2_2(X32_47, X33_50) | c1_1(X32_47) | ~c4_2(X32_47, a505) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47) | c6_2(X32_47, a505)))).
% 34.43/14.18  tff(c_12259, plain, (![X32_47, X34_51, X33_50]: (~c2_2(X32_47, X34_51) | ~c10_2(X32_47, X34_51) | c2_2(X32_47, a545) | c10_2(X32_47, a545) | c10_1(X32_47) | c6_2(X32_47, a505) | ~c10_2(X32_47, X33_50) | c2_2(X32_47, X33_50) | c1_1(X32_47) | ~c4_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.18  tff(c_12363, plain, (![X32_513, X33_515, X34_514]: (c4_2(X32_513, a511) | ~c2_2(X32_513, X33_515) | c8_2(X32_513, X33_515) | ~c2_1(X32_513) | ~c2_2(X32_513, X34_514) | ~c10_2(X32_513, X34_514) | c2_2(X32_513, a545) | c10_2(X32_513, a545) | c10_1(X32_513) | ~c4_2(X32_513, X34_514) | c6_2(X32_513, X34_514) | c5_2(X32_513, X33_515) | c4_2(X32_513, X33_515) | ~ndr1_1(X32_513) | c6_1(X32_513)))).
% 34.43/14.18  tff(c_14308, plain, (![U_1, X33_643]: (~c1_2(U_1, X33_643) | ~c3_1(U_1) | ~c2_2(U_1, a545) | ~c10_2(U_1, a545) | ~c10_2(U_1, X33_643) | c4_2(U_1, a511) | ~c2_2(U_1, X33_643) | ~c4_2(U_1, a545) | c4_2(U_1, X33_643) | ~ndr1_1(U_1) | c6_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_12283, plain, (![X32_302, X34_303, X33_304]: (~c2_2(X32_302, X34_303) | ~c10_2(X32_302, X34_303) | c2_2(X32_302, a545) | c10_2(X32_302, a545) | c10_1(X32_302) | c4_2(X32_302, a511) | ~c2_2(X32_302, X33_304) | c8_2(X32_302, X33_304) | ~c2_1(X32_302) | ~c4_2(X32_302, X34_303) | c6_2(X32_302, X34_303) | c5_2(X32_302, X33_304) | c4_2(X32_302, X33_304) | ~ndr1_1(X32_302) | c6_1(X32_302)))).
% 34.43/14.18  tff(c_14289, plain, (![U_1, X33_640]: (~c1_2(U_1, X33_640) | ~c3_1(U_1) | ~c2_2(U_1, a545) | ~c10_2(U_1, a545) | ~c10_2(U_1, X33_640) | c1_2(U_1, a511) | ~c2_2(U_1, X33_640) | ~c4_2(U_1, a545) | c4_2(U_1, X33_640) | ~ndr1_1(U_1) | c6_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_12697, plain, (![X32_347, X33_348, X143_526]: (~c1_2(X32_347, X33_348) | ~c10_2(X32_347, X143_526) | ~c3_1(X32_347) | ~c2_2(X32_347, a545) | ~c10_2(X32_347, a545) | ~c10_2(X32_347, X33_348) | c4_2(X32_347, a511) | ~c2_2(X32_347, X33_348) | ~c2_1(X32_347) | ~c4_2(X32_347, a545) | c4_2(X32_347, X33_348) | ~ndr1_1(X32_347) | c6_1(X32_347) | c6_2(X32_347, a545)))).
% 34.43/14.18  tff(c_12686, plain, (![X32_353, X33_354, X143_526]: (~c1_2(X32_353, X33_354) | ~c10_2(X32_353, X143_526) | ~c3_1(X32_353) | ~c2_2(X32_353, a545) | ~c10_2(X32_353, a545) | ~c10_2(X32_353, X33_354) | c1_2(X32_353, a511) | ~c2_2(X32_353, X33_354) | ~c2_1(X32_353) | ~c4_2(X32_353, a545) | c4_2(X32_353, X33_354) | ~ndr1_1(X32_353) | c6_1(X32_353) | c6_2(X32_353, a545)))).
% 34.43/14.18  tff(c_13313, plain, (![U_1, X33_578, X34_580]: (~c1_2(U_1, X33_578) | ~c3_1(U_1) | c4_2(U_1, a545) | ~c10_2(U_1, X33_578) | c4_2(U_1, a511) | ~c2_2(U_1, X33_578) | ~c4_2(U_1, X34_580) | c8_2(U_1, X34_580) | c6_2(U_1, X34_580) | c4_2(U_1, X33_578) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_13275, plain, (![U_1, X33_570, X34_572]: (~c1_2(U_1, X33_570) | ~c3_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, X33_570) | c4_2(U_1, a511) | ~c2_2(U_1, X33_570) | ~c4_2(U_1, X34_572) | c8_2(U_1, X34_572) | c6_2(U_1, X34_572) | c4_2(U_1, X33_570) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_12362, plain, (![X32_513, X33_515, X34_514]: (c1_2(X32_513, a511) | ~c2_2(X32_513, X33_515) | c8_2(X32_513, X33_515) | ~c2_1(X32_513) | ~c2_2(X32_513, X34_514) | ~c10_2(X32_513, X34_514) | c2_2(X32_513, a545) | c10_2(X32_513, a545) | c10_1(X32_513) | ~c4_2(X32_513, X34_514) | c6_2(X32_513, X34_514) | c5_2(X32_513, X33_515) | c4_2(X32_513, X33_515) | ~ndr1_1(X32_513) | c6_1(X32_513)))).
% 34.43/14.18  tff(c_13294, plain, (![U_1, X33_574, X34_576]: (~c1_2(U_1, X33_574) | ~c3_1(U_1) | c4_2(U_1, a545) | ~c10_2(U_1, X33_574) | c1_2(U_1, a511) | ~c2_2(U_1, X33_574) | ~c4_2(U_1, X34_576) | c8_2(U_1, X34_576) | c6_2(U_1, X34_576) | c4_2(U_1, X33_574) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_13456, plain, (![U_1, X33_588, X34_590]: (~c1_2(U_1, X33_588) | ~c3_1(U_1) | c6_2(U_1, a545) | ~c10_2(U_1, X33_588) | c1_2(U_1, a511) | ~c2_2(U_1, X33_588) | ~c4_2(U_1, X34_590) | c8_2(U_1, X34_590) | c6_2(U_1, X34_590) | c4_2(U_1, X33_588) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_12690, plain, (![X32_469, X33_470, X143_526]: (~c1_2(X32_469, X33_470) | ~c10_2(X32_469, X143_526) | ~c3_1(X32_469) | ~c2_2(X32_469, a545) | ~c10_2(X32_469, a545) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, a545) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469) | c6_2(X32_469, a545)))).
% 34.43/14.18  tff(c_12281, plain, (![X32_302, X34_303, X33_304]: (~c2_2(X32_302, X34_303) | ~c10_2(X32_302, X34_303) | c2_2(X32_302, a545) | c10_2(X32_302, a545) | c10_1(X32_302) | c1_2(X32_302, a511) | ~c2_2(X32_302, X33_304) | c8_2(X32_302, X33_304) | ~c2_1(X32_302) | ~c4_2(X32_302, X34_303) | c6_2(X32_302, X34_303) | c5_2(X32_302, X33_304) | c4_2(X32_302, X33_304) | ~ndr1_1(X32_302) | c6_1(X32_302)))).
% 34.43/14.18  tff(c_11090, plain, (![X32_455, X33_456, X34_457]: (c3_2(X32_455, X33_456) | c1_1(X32_455) | ~c10_2(X32_455, X33_456) | c4_2(X32_455, a511) | ~c2_2(X32_455, X33_456) | ~c2_1(X32_455) | c6_2(X32_455, a545) | ~c2_2(X32_455, X34_457) | ~c10_2(X32_455, X34_457) | ~c4_2(X32_455, X34_457) | c6_2(X32_455, X34_457) | c4_2(X32_455, X33_456) | ~ndr1_1(X32_455) | c6_1(X32_455)))).
% 34.43/14.18  tff(c_11258, plain, (![X32_464, X33_465, X34_466]: (c3_2(X32_464, X33_465) | c1_1(X32_464) | ~c10_2(X32_464, X33_465) | c1_2(X32_464, a511) | ~c2_2(X32_464, X33_465) | ~c2_1(X32_464) | c4_2(X32_464, a545) | ~c2_2(X32_464, X34_466) | ~c10_2(X32_464, X34_466) | ~c4_2(X32_464, X34_466) | c6_2(X32_464, X34_466) | c4_2(X32_464, X33_465) | ~ndr1_1(X32_464) | c6_1(X32_464)))).
% 34.43/14.18  tff(c_12701, plain, (![X32_426, X33_427, X143_526]: (~c1_2(X32_426, X33_427) | ~c10_2(X32_426, X143_526) | ~c3_1(X32_426) | ~c2_2(X32_426, a545) | ~c10_2(X32_426, a545) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, a545) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426) | c6_2(X32_426, a545)))).
% 34.43/14.18  tff(c_12688, plain, (![X32_469, X33_470, X143_526]: (~c1_2(X32_469, X33_470) | ~c10_2(X32_469, X143_526) | ~c3_1(X32_469) | c4_2(X32_469, a545) | ~c2_2(X32_469, a505) | ~c10_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, a505) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469) | c6_2(X32_469, a505)))).
% 34.43/14.18  tff(c_11159, plain, (![X32_458, X33_459, X34_460]: (c3_2(X32_458, X33_459) | c1_1(X32_458) | ~c10_2(X32_458, X33_459) | c1_2(X32_458, a511) | ~c2_2(X32_458, X33_459) | ~c2_1(X32_458) | c6_2(X32_458, a545) | ~c2_2(X32_458, X34_460) | ~c10_2(X32_458, X34_460) | ~c4_2(X32_458, X34_460) | c6_2(X32_458, X34_460) | c4_2(X32_458, X33_459) | ~ndr1_1(X32_458) | c6_1(X32_458)))).
% 34.43/14.18  tff(c_11209, plain, (![X32_461, X33_462, X34_463]: (c3_2(X32_461, X33_462) | c1_1(X32_461) | ~c10_2(X32_461, X33_462) | c4_2(X32_461, a511) | ~c2_2(X32_461, X33_462) | ~c2_1(X32_461) | c4_2(X32_461, a545) | ~c2_2(X32_461, X34_463) | ~c10_2(X32_461, X34_463) | ~c4_2(X32_461, X34_463) | c6_2(X32_461, X34_463) | c4_2(X32_461, X33_462) | ~ndr1_1(X32_461) | c6_1(X32_461)))).
% 34.43/14.18  tff(c_12710, plain, (![X32_337, X33_338, X143_526, X34_339]: (~c1_2(X32_337, X33_338) | ~c10_2(X32_337, X143_526) | ~c3_1(X32_337) | c6_2(X32_337, a545) | ~c10_2(X32_337, X33_338) | c1_2(X32_337, a511) | ~c2_2(X32_337, X33_338) | ~c2_1(X32_337) | ~c4_2(X32_337, X34_339) | c8_2(X32_337, X34_339) | c6_2(X32_337, X34_339) | c4_2(X32_337, X33_338) | ~ndr1_1(X32_337) | c6_1(X32_337)))).
% 34.43/14.18  tff(c_12446, plain, (![X150_516, X33_517, X34_518]: (c6_2(X150_516, a545) | ~c10_2(X150_516, X33_517) | ~c2_2(X150_516, X33_517) | ~c2_1(X150_516) | ~c4_2(X150_516, X34_518) | c8_2(X150_516, X34_518) | c6_2(X150_516, X34_518) | c5_2(X150_516, X33_517) | c4_2(X150_516, X33_517) | c6_1(X150_516) | c2_2(X150_516, a511) | c10_2(X150_516, a511) | ~ndr1_1(X150_516) | c10_1(X150_516)))).
% 34.43/14.18  tff(c_12445, plain, (![X150_516, X33_517, X34_518]: (c4_2(X150_516, a545) | ~c10_2(X150_516, X33_517) | ~c2_2(X150_516, X33_517) | ~c2_1(X150_516) | ~c4_2(X150_516, X34_518) | c8_2(X150_516, X34_518) | c6_2(X150_516, X34_518) | c5_2(X150_516, X33_517) | c4_2(X150_516, X33_517) | c6_1(X150_516) | c2_2(X150_516, a511) | c10_2(X150_516, a511) | ~ndr1_1(X150_516) | c10_1(X150_516)))).
% 34.43/14.18  tff(c_12713, plain, (![X32_334, X33_335, X143_526, X34_336]: (~c1_2(X32_334, X33_335) | ~c10_2(X32_334, X143_526) | ~c3_1(X32_334) | c4_2(X32_334, a545) | ~c10_2(X32_334, X33_335) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, X34_336) | c8_2(X32_334, X34_336) | c6_2(X32_334, X34_336) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.18  tff(c_12711, plain, (![X32_337, X33_338, X143_526, X34_339]: (~c1_2(X32_337, X33_338) | ~c10_2(X32_337, X143_526) | ~c3_1(X32_337) | c4_2(X32_337, a545) | ~c10_2(X32_337, X33_338) | c1_2(X32_337, a511) | ~c2_2(X32_337, X33_338) | ~c2_1(X32_337) | ~c4_2(X32_337, X34_339) | c8_2(X32_337, X34_339) | c6_2(X32_337, X34_339) | c4_2(X32_337, X33_338) | ~ndr1_1(X32_337) | c6_1(X32_337)))).
% 34.43/14.18  tff(c_12712, plain, (![X32_334, X33_335, X143_526, X34_336]: (~c1_2(X32_334, X33_335) | ~c10_2(X32_334, X143_526) | ~c3_1(X32_334) | c6_2(X32_334, a545) | ~c10_2(X32_334, X33_335) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, X34_336) | c8_2(X32_334, X34_336) | c6_2(X32_334, X34_336) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.18  tff(c_12282, plain, (![X32_302, X33_304, X34_303]: (~c10_2(X32_302, X33_304) | c2_2(X32_302, a545) | c10_2(X32_302, a545) | c10_1(X32_302) | c4_2(X32_302, a511) | ~c2_2(X32_302, X33_304) | ~c2_1(X32_302) | ~c4_2(X32_302, X34_303) | c8_2(X32_302, X34_303) | c6_2(X32_302, X34_303) | c5_2(X32_302, X33_304) | c4_2(X32_302, X33_304) | ~ndr1_1(X32_302) | c6_1(X32_302)))).
% 34.43/14.18  tff(c_12280, plain, (![X32_302, X33_304, X34_303]: (~c10_2(X32_302, X33_304) | c2_2(X32_302, a545) | c10_2(X32_302, a545) | c10_1(X32_302) | c1_2(X32_302, a511) | ~c2_2(X32_302, X33_304) | ~c2_1(X32_302) | ~c4_2(X32_302, X34_303) | c8_2(X32_302, X34_303) | c6_2(X32_302, X34_303) | c5_2(X32_302, X33_304) | c4_2(X32_302, X33_304) | ~ndr1_1(X32_302) | c6_1(X32_302)))).
% 34.43/14.18  tff(c_10945, plain, (![X32_448, X33_450]: (~c1_1(X32_448) | c8_1(X32_448) | ~c2_2(X32_448, a576) | ~c10_2(X32_448, a576) | c6_2(X32_448, a545) | ~c10_2(X32_448, X33_450) | c4_2(X32_448, a511) | ~c2_2(X32_448, X33_450) | ~c2_1(X32_448) | ~c4_2(X32_448, a576) | c5_2(X32_448, X33_450) | c4_2(X32_448, X33_450) | ~ndr1_1(X32_448) | c6_1(X32_448)))).
% 34.43/14.18  tff(c_10407, plain, (![X32_421, X33_423]: (~c1_1(X32_421) | c8_1(X32_421) | ~c2_2(X32_421, a576) | ~c10_2(X32_421, a576) | c4_2(X32_421, a545) | ~c10_2(X32_421, X33_423) | c4_2(X32_421, a511) | ~c2_2(X32_421, X33_423) | ~c2_1(X32_421) | ~c4_2(X32_421, a576) | c5_2(X32_421, X33_423) | c4_2(X32_421, X33_423) | ~ndr1_1(X32_421) | c6_1(X32_421)))).
% 34.43/14.18  tff(c_11872, plain, (![X32_494, X33_496]: (~c1_1(X32_494) | c8_1(X32_494) | ~c2_2(X32_494, a576) | ~c10_2(X32_494, a576) | c6_2(X32_494, a545) | ~c10_2(X32_494, X33_496) | c1_2(X32_494, a511) | ~c2_2(X32_494, X33_496) | ~c2_1(X32_494) | ~c4_2(X32_494, a576) | c5_2(X32_494, X33_496) | c4_2(X32_494, X33_496) | ~ndr1_1(X32_494) | c6_1(X32_494)))).
% 34.43/14.18  tff(c_10872, plain, (![X32_445, X33_447]: (~c1_1(X32_445) | c8_1(X32_445) | ~c2_2(X32_445, a576) | ~c10_2(X32_445, a576) | c4_2(X32_445, a545) | ~c10_2(X32_445, X33_447) | c1_2(X32_445, a511) | ~c2_2(X32_445, X33_447) | ~c2_1(X32_445) | ~c4_2(X32_445, a576) | c5_2(X32_445, X33_447) | c4_2(X32_445, X33_447) | ~ndr1_1(X32_445) | c6_1(X32_445)))).
% 34.43/14.18  tff(c_12748, plain, (![U_1, X33_536, X34_538]: (~c1_2(U_1, X33_536) | ~c3_1(U_1) | c6_2(U_1, a505) | ~c10_2(U_1, X33_536) | c2_2(U_1, X33_536) | c1_1(U_1) | ~c4_2(U_1, X34_538) | c8_2(U_1, X34_538) | c6_2(U_1, X34_538) | c4_2(U_1, X33_536) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_12768, plain, (![U_1, X33_540, X34_542]: (~c1_2(U_1, X33_540) | ~c3_1(U_1) | ~c3_2(U_1, a505) | ~c10_2(U_1, X33_540) | c2_2(U_1, X33_540) | c1_1(U_1) | ~c4_2(U_1, X34_542) | c8_2(U_1, X34_542) | c6_2(U_1, X34_542) | c4_2(U_1, X33_540) | ~ndr1_1(U_1) | c6_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.18  tff(c_12703, plain, (![X32_47, X33_50, X143_526, X34_51]: (~c1_2(X32_47, X33_50) | ~c10_2(X32_47, X143_526) | ~c3_1(X32_47) | ~c3_2(X32_47, a505) | ~c10_2(X32_47, X33_50) | c2_2(X32_47, X33_50) | c1_1(X32_47) | ~c4_2(X32_47, X34_51) | c8_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.18  tff(c_12692, plain, (![X32_47, X33_50, X143_526, X34_51]: (~c1_2(X32_47, X33_50) | ~c10_2(X32_47, X143_526) | ~c3_1(X32_47) | c6_2(X32_47, a505) | ~c10_2(X32_47, X33_50) | c2_2(X32_47, X33_50) | c1_1(X32_47) | ~c4_2(X32_47, X34_51) | c8_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.19  tff(c_12718, plain, (![U_1, X143_526]: (~c10_2(U_1, a432) | ~c1_2(U_1, a432) | ~c10_2(U_1, X143_526) | ~ndr1_1(U_1) | ~c3_1(U_1) | c1_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.19  tff(c_12717, plain, (![U_1, X143_526]: (~c10_2(U_1, a432) | ~c1_2(U_1, a432) | ~c10_2(U_1, X143_526) | ~ndr1_1(U_1) | ~c3_1(U_1) | ~c10_2(U_1, a431) | ~c2_1(U_1)))).
% 34.43/14.19  tff(c_12719, plain, (![V_2, X143_526]: (~c10_2(V_2, a433) | ~c1_2(V_2, a433) | ~c10_2(V_2, X143_526) | ~ndr1_1(V_2) | ~c3_1(V_2) | ~c7_1(V_2) | ~c6_1(V_2)))).
% 34.43/14.19  tff(c_12705, plain, (![X137_178, X143_526]: (~c10_2(X137_178, a576) | ~c1_2(X137_178, a576) | ~c10_2(X137_178, X143_526) | ~ndr1_1(X137_178) | ~c3_1(X137_178) | ~c1_1(X137_178) | c8_1(X137_178)))).
% 34.43/14.19  tff(c_12727, plain, (~c3_1(a485))).
% 34.43/14.19  tff(c_12726, plain, (~c3_1(a542))).
% 34.43/14.19  tff(c_12612, plain, (![X142_185, X144_189, X143_188]: (~c5_2(X142_185, X144_189) | ~c10_2(X142_185, X144_189) | ~c1_2(X142_185, X144_189) | ~c10_2(X142_185, X143_188) | ~ndr1_1(X142_185) | ~c3_1(X142_185)))).
% 34.43/14.19  tff(c_12616, plain, (~c6_1(a600))).
% 34.43/14.19  tff(c_12614, plain, (c5_1(a600))).
% 34.43/14.19  tff(c_12613, plain, (~c4_1(a600))).
% 34.43/14.19  tff(c_12611, plain, (~c1_1(a600))).
% 34.43/14.19  tff(c_12610, plain, (~c3_1(a600))).
% 34.43/14.19  tff(c_12609, plain, (~c2_1(a600))).
% 34.43/14.19  tff(c_12576, plain, (~ndr1_1(a600))).
% 34.43/14.19  tff(c_11500, plain, (![X32_475, X33_477, X34_476]: (c3_2(X32_475, X33_477) | c6_2(X32_475, a545) | ~c2_2(X32_475, X34_476) | ~c10_2(X32_475, X34_476) | c6_2(X32_475, a505) | ~c10_2(X32_475, X33_477) | c2_2(X32_475, X33_477) | c1_1(X32_475) | ~c4_2(X32_475, X34_476) | c6_2(X32_475, X34_476) | c4_2(X32_475, X33_477) | ~ndr1_1(X32_475) | c6_1(X32_475)))).
% 34.43/14.19  tff(c_12459, plain, (![X150_516, X33_517]: (~c9_1(X150_516) | ~c1_1(X150_516) | ~c2_2(X150_516, X33_517) | c8_2(X150_516, X33_517) | ~c2_1(X150_516) | ~c4_2(X150_516, a518) | c6_2(X150_516, a518) | c5_2(X150_516, X33_517) | c4_2(X150_516, X33_517) | c6_1(X150_516) | c2_2(X150_516, a511) | c10_2(X150_516, a511) | ~ndr1_1(X150_516) | c10_1(X150_516)))).
% 34.43/14.19  tff(c_12133, plain, (![X150_508, X33_304, X34_303]: (~c2_2(X150_508, X33_304) | c8_2(X150_508, X33_304) | ~c2_1(X150_508) | ~c4_2(X150_508, X34_303) | c8_2(X150_508, X34_303) | c6_2(X150_508, X34_303) | c5_2(X150_508, X33_304) | c4_2(X150_508, X33_304) | c6_1(X150_508) | c2_2(X150_508, a511) | c10_2(X150_508, a511) | ~ndr1_1(X150_508) | c10_1(X150_508)))).
% 34.43/14.19  tff(c_12289, plain, (![X32_47, X34_51, X33_50]: (~c2_2(X32_47, X34_51) | ~c10_2(X32_47, X34_51) | c2_2(X32_47, a545) | c10_2(X32_47, a545) | c10_1(X32_47) | ~c4_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c9_2(X32_47, X33_50) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.19  tff(c_12306, plain, (c10_1(a489))).
% 34.43/14.19  tff(c_12134, plain, (![X150_508, X100_132]: (~c8_2(X150_508, X100_132) | ~c2_2(X150_508, X100_132) | ~c10_2(X150_508, X100_132) | c2_2(X150_508, a545) | c10_2(X150_508, a545) | ~ndr1_1(X150_508) | c10_1(X150_508)))).
% 34.43/14.19  tff(c_12137, plain, (![X150_508]: (~c9_1(X150_508) | ~c1_1(X150_508) | c2_2(X150_508, a518) | c10_2(X150_508, a518) | ~ndr1_1(X150_508) | c10_1(X150_508)))).
% 34.43/14.19  tff(c_12141, plain, (c10_2(a485, a487))).
% 34.43/14.19  tff(c_12104, plain, (![X150_197, X151_199]: (c8_2(X150_197, X151_199) | c2_2(X150_197, X151_199) | c10_2(X150_197, X151_199) | ~ndr1_1(X150_197) | c10_1(X150_197)))).
% 34.43/14.19  tff(c_10593, plain, (![X32_429, X34_431, X33_430]: (c6_2(X32_429, a545) | ~c2_2(X32_429, X34_431) | ~c10_2(X32_429, X34_431) | c3_2(X32_429, X33_430) | ~c3_2(X32_429, a505) | ~c10_2(X32_429, X33_430) | c2_2(X32_429, X33_430) | c1_1(X32_429) | ~c4_2(X32_429, X34_431) | c6_2(X32_429, X34_431) | c4_2(X32_429, X33_430) | ~ndr1_1(X32_429) | c6_1(X32_429)))).
% 34.43/14.19  tff(c_10592, plain, (![X32_429, X34_431, X33_430]: (c4_2(X32_429, a545) | ~c2_2(X32_429, X34_431) | ~c10_2(X32_429, X34_431) | c3_2(X32_429, X33_430) | ~c3_2(X32_429, a505) | ~c10_2(X32_429, X33_430) | c2_2(X32_429, X33_430) | c1_1(X32_429) | ~c4_2(X32_429, X34_431) | c6_2(X32_429, X34_431) | c4_2(X32_429, X33_430) | ~ndr1_1(X32_429) | c6_1(X32_429)))).
% 34.43/14.19  tff(c_11639, plain, (![X32_482, X33_483, X34_484]: (c3_2(X32_482, X33_483) | c6_2(X32_482, a505) | ~c10_2(X32_482, X33_483) | c2_2(X32_482, X33_483) | c1_1(X32_482) | c4_2(X32_482, a545) | ~c2_2(X32_482, X34_484) | ~c10_2(X32_482, X34_484) | ~c4_2(X32_482, X34_484) | c6_2(X32_482, X34_484) | c4_2(X32_482, X33_483) | ~ndr1_1(X32_482) | c6_1(X32_482)))).
% 34.43/14.19  tff(c_11827, plain, (![X32_353, X33_354]: (~c2_2(X32_353, a545) | ~c10_2(X32_353, a545) | ~c10_2(X32_353, X33_354) | c1_2(X32_353, a511) | ~c2_2(X32_353, X33_354) | ~c2_1(X32_353) | ~c4_2(X32_353, a545) | c5_2(X32_353, X33_354) | c4_2(X32_353, X33_354) | ~ndr1_1(X32_353) | c6_1(X32_353) | c6_2(X32_353, a545)))).
% 34.43/14.19  tff(c_9145, plain, (![X32_353, X34_355, X33_354]: (~c2_2(X32_353, X34_355) | ~c10_2(X32_353, X34_355) | c6_2(X32_353, a545) | ~c10_2(X32_353, X33_354) | c1_2(X32_353, a511) | ~c2_2(X32_353, X33_354) | ~c2_1(X32_353) | ~c4_2(X32_353, X34_355) | c6_2(X32_353, X34_355) | c5_2(X32_353, X33_354) | c4_2(X32_353, X33_354) | ~ndr1_1(X32_353) | c6_1(X32_353)))).
% 34.43/14.19  tff(c_11719, plain, (![X32_469, X33_470]: (c4_2(X32_469, a545) | ~c2_2(X32_469, a505) | ~c10_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, a505) | c5_2(X32_469, X33_470) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469) | c6_2(X32_469, a505)))).
% 34.43/14.19  tff(c_11367, plain, (![X32_469, X34_471, X33_470]: (c4_2(X32_469, a545) | ~c2_2(X32_469, X34_471) | ~c10_2(X32_469, X34_471) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, X34_471) | c6_2(X32_469, X34_471) | c5_2(X32_469, X33_470) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469)))).
% 34.43/14.19  tff(c_11666, plain, (![X32_485, X33_486]: (c3_2(X32_485, X33_486) | ~c10_2(X32_485, X33_486) | c2_2(X32_485, X33_486) | c1_1(X32_485) | c4_2(X32_485, a545) | ~c2_2(X32_485, a505) | ~c10_2(X32_485, a505) | ~c4_2(X32_485, a505) | c4_2(X32_485, X33_486) | ~ndr1_1(X32_485) | c6_1(X32_485) | c6_2(X32_485, a505)))).
% 34.43/14.19  tff(c_11527, plain, (![X32_478, X33_479]: (c3_2(X32_478, X33_479) | ~c2_2(X32_478, a545) | ~c10_2(X32_478, a545) | c6_2(X32_478, a505) | ~c10_2(X32_478, X33_479) | c2_2(X32_478, X33_479) | c1_1(X32_478) | ~c4_2(X32_478, a545) | c4_2(X32_478, X33_479) | ~ndr1_1(X32_478) | c6_1(X32_478) | c6_2(X32_478, a545)))).
% 34.43/14.19  tff(c_11440, plain, (![X32_469, X33_470]: (~c2_2(X32_469, a545) | ~c10_2(X32_469, a545) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, a545) | c5_2(X32_469, X33_470) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469) | c6_2(X32_469, a545)))).
% 34.43/14.19  tff(c_11368, plain, (![X32_469, X34_471, X33_470]: (c6_2(X32_469, a545) | ~c2_2(X32_469, X34_471) | ~c10_2(X32_469, X34_471) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, X34_471) | c6_2(X32_469, X34_471) | c5_2(X32_469, X33_470) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469)))).
% 34.43/14.19  tff(c_11377, plain, (![X32_469, X33_470, X34_471]: (c3_2(X32_469, X33_470) | c6_2(X32_469, a505) | ~c10_2(X32_469, X33_470) | c2_2(X32_469, X33_470) | c1_1(X32_469) | ~c4_2(X32_469, X34_471) | c8_2(X32_469, X34_471) | c6_2(X32_469, X34_471) | c4_2(X32_469, X33_470) | ~ndr1_1(X32_469) | c6_1(X32_469)))).
% 34.43/14.19  tff(c_11290, plain, (![X32_47, X33_50, X34_51]: (c6_2(X32_47, a505) | ~c10_2(X32_47, X33_50) | c2_2(X32_47, X33_50) | c1_1(X32_47) | ~c4_2(X32_47, X34_51) | c8_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.19  tff(c_11323, plain, (~c10_1(a468))).
% 34.43/14.19  tff(c_11318, plain, (c1_1(a468))).
% 34.43/14.19  tff(c_11317, plain, (~c1_2(a501, a505))).
% 34.43/14.19  tff(c_11311, plain, (c6_2(a501, a505))).
% 34.43/14.19  tff(c_11259, plain, (![X52_70, X53_72]: (c6_2(X52_70, a505) | ~c9_2(X52_70, X53_72) | ~c10_2(X52_70, X53_72) | c2_2(X52_70, X53_72) | ~ndr1_1(X52_70) | c1_1(X52_70)))).
% 34.43/14.19  tff(c_9968, plain, (![X32_399, X33_400, X34_401]: (~c10_2(X32_399, X33_400) | c1_2(X32_399, a511) | ~c2_2(X32_399, X33_400) | ~c2_1(X32_399) | c4_2(X32_399, a545) | ~c2_2(X32_399, X34_401) | ~c10_2(X32_399, X34_401) | ~c4_2(X32_399, X34_401) | c6_2(X32_399, X34_401) | c5_2(X32_399, X33_400) | c4_2(X32_399, X33_400) | ~ndr1_1(X32_399) | c6_1(X32_399)))).
% 34.43/14.19  tff(c_9916, plain, (![X32_396, X33_397, X34_398]: (~c10_2(X32_396, X33_397) | c4_2(X32_396, a511) | ~c2_2(X32_396, X33_397) | ~c2_1(X32_396) | c4_2(X32_396, a545) | ~c2_2(X32_396, X34_398) | ~c10_2(X32_396, X34_398) | ~c4_2(X32_396, X34_398) | c6_2(X32_396, X34_398) | c5_2(X32_396, X33_397) | c4_2(X32_396, X33_397) | ~ndr1_1(X32_396) | c6_1(X32_396)))).
% 34.43/14.19  tff(c_10075, plain, (![X32_405, X33_406, X34_407]: (~c10_2(X32_405, X33_406) | c1_2(X32_405, a511) | ~c2_2(X32_405, X33_406) | ~c2_1(X32_405) | c6_2(X32_405, a545) | ~c2_2(X32_405, X34_407) | ~c10_2(X32_405, X34_407) | ~c4_2(X32_405, X34_407) | c6_2(X32_405, X34_407) | c5_2(X32_405, X33_406) | c4_2(X32_405, X33_406) | ~ndr1_1(X32_405) | c6_1(X32_405)))).
% 34.43/14.19  tff(c_10022, plain, (![X32_402, X33_403, X34_404]: (~c10_2(X32_402, X33_403) | c4_2(X32_402, a511) | ~c2_2(X32_402, X33_403) | ~c2_1(X32_402) | c6_2(X32_402, a545) | ~c2_2(X32_402, X34_404) | ~c10_2(X32_402, X34_404) | ~c4_2(X32_402, X34_404) | c6_2(X32_402, X34_404) | c5_2(X32_402, X33_403) | c4_2(X32_402, X33_403) | ~ndr1_1(X32_402) | c6_1(X32_402)))).
% 34.43/14.19  tff(c_10983, plain, (![X32_451, X33_452]: (c3_2(X32_451, X33_452) | c1_1(X32_451) | ~c2_2(X32_451, a545) | ~c10_2(X32_451, a545) | ~c10_2(X32_451, X33_452) | c4_2(X32_451, a511) | ~c2_2(X32_451, X33_452) | ~c2_1(X32_451) | ~c4_2(X32_451, a545) | c4_2(X32_451, X33_452) | ~ndr1_1(X32_451) | c6_1(X32_451) | c6_2(X32_451, a545)))).
% 34.43/14.19  tff(c_10900, plain, (![X32_347, X33_348]: (~c2_2(X32_347, a545) | ~c10_2(X32_347, a545) | ~c10_2(X32_347, X33_348) | c4_2(X32_347, a511) | ~c2_2(X32_347, X33_348) | ~c2_1(X32_347) | ~c4_2(X32_347, a545) | c5_2(X32_347, X33_348) | c4_2(X32_347, X33_348) | ~ndr1_1(X32_347) | c6_1(X32_347) | c6_2(X32_347, a545)))).
% 34.43/14.19  tff(c_9053, plain, (![X32_347, X34_349, X33_348]: (~c2_2(X32_347, X34_349) | ~c10_2(X32_347, X34_349) | c6_2(X32_347, a545) | ~c10_2(X32_347, X33_348) | c4_2(X32_347, a511) | ~c2_2(X32_347, X33_348) | ~c2_1(X32_347) | ~c4_2(X32_347, X34_349) | c6_2(X32_347, X34_349) | c5_2(X32_347, X33_348) | c4_2(X32_347, X33_348) | ~ndr1_1(X32_347) | c6_1(X32_347)))).
% 34.43/14.19  tff(c_9098, plain, (![X32_350, X34_352, X33_351]: (~c2_2(X32_350, X34_352) | ~c10_2(X32_350, X34_352) | c4_2(X32_350, a545) | ~c10_2(X32_350, X33_351) | c1_2(X32_350, a511) | ~c2_2(X32_350, X33_351) | ~c2_1(X32_350) | ~c4_2(X32_350, X34_352) | c6_2(X32_350, X34_352) | c5_2(X32_350, X33_351) | c4_2(X32_350, X33_351) | ~ndr1_1(X32_350) | c6_1(X32_350)))).
% 34.43/14.19  tff(c_10537, plain, (![X32_426, X34_428, X33_427]: (c4_2(X32_426, a545) | ~c2_2(X32_426, X34_428) | ~c10_2(X32_426, X34_428) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, X34_428) | c6_2(X32_426, X34_428) | c5_2(X32_426, X33_427) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426)))).
% 34.43/14.19  tff(c_10697, plain, (![X32_435, X33_436]: (c3_2(X32_435, X33_436) | ~c2_2(X32_435, a545) | ~c10_2(X32_435, a545) | ~c3_2(X32_435, a505) | ~c10_2(X32_435, X33_436) | c2_2(X32_435, X33_436) | c1_1(X32_435) | ~c4_2(X32_435, a545) | c4_2(X32_435, X33_436) | ~ndr1_1(X32_435) | c6_1(X32_435) | c6_2(X32_435, a545)))).
% 34.43/14.19  tff(c_10610, plain, (![X32_426, X33_427]: (~c2_2(X32_426, a545) | ~c10_2(X32_426, a545) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, a545) | c5_2(X32_426, X33_427) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426) | c6_2(X32_426, a545)))).
% 34.43/14.19  tff(c_10538, plain, (![X32_426, X34_428, X33_427]: (c6_2(X32_426, a545) | ~c2_2(X32_426, X34_428) | ~c10_2(X32_426, X34_428) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, X34_428) | c6_2(X32_426, X34_428) | c5_2(X32_426, X33_427) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426)))).
% 34.43/14.19  tff(c_10547, plain, (![X32_426, X33_427, X34_428]: (c3_2(X32_426, X33_427) | ~c3_2(X32_426, a505) | ~c10_2(X32_426, X33_427) | c2_2(X32_426, X33_427) | c1_1(X32_426) | ~c4_2(X32_426, X34_428) | c8_2(X32_426, X34_428) | c6_2(X32_426, X34_428) | c4_2(X32_426, X33_427) | ~ndr1_1(X32_426) | c6_1(X32_426)))).
% 34.43/14.19  tff(c_10468, plain, (![X32_47, X33_50, X34_51]: (~c3_2(X32_47, a505) | ~c10_2(X32_47, X33_50) | c2_2(X32_47, X33_50) | c1_1(X32_47) | ~c4_2(X32_47, X34_51) | c8_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.19  tff(c_10493, plain, (~c3_2(a468, a505))).
% 34.43/14.19  tff(c_10492, plain, (~c3_2(a501, a505))).
% 34.43/14.19  tff(c_10490, plain, (~c10_2(a468, a469))).
% 34.43/14.19  tff(c_10489, plain, (~c10_2(a501, a502))).
% 34.43/14.19  tff(c_10424, plain, (![X52_70, X53_72]: (~c3_2(X52_70, a505) | ~c9_2(X52_70, X53_72) | ~c10_2(X52_70, X53_72) | c2_2(X52_70, X53_72) | ~ndr1_1(X52_70) | c1_1(X52_70)))).
% 34.43/14.19  tff(c_10437, plain, (~c3_2(a485, a486))).
% 34.43/14.19  tff(c_10423, plain, (~c4_2(a485, a486))).
% 34.43/14.19  tff(c_9006, plain, (![X32_344, X34_346, X33_345]: (~c2_2(X32_344, X34_346) | ~c10_2(X32_344, X34_346) | c4_2(X32_344, a545) | ~c10_2(X32_344, X33_345) | c4_2(X32_344, a511) | ~c2_2(X32_344, X33_345) | ~c2_1(X32_344) | ~c4_2(X32_344, X34_346) | c6_2(X32_344, X34_346) | c5_2(X32_344, X33_345) | c4_2(X32_344, X33_345) | ~ndr1_1(X32_344) | c6_1(X32_344)))).
% 34.43/14.19  tff(c_10338, plain, (![X32_417, X33_418]: (c3_2(X32_417, X33_418) | c1_1(X32_417) | ~c10_2(X32_417, X33_418) | ~c2_2(X32_417, a545) | ~c10_2(X32_417, a545) | c1_2(X32_417, a511) | ~c2_2(X32_417, X33_418) | ~c2_1(X32_417) | ~c4_2(X32_417, a545) | c4_2(X32_417, X33_418) | ~ndr1_1(X32_417) | c6_1(X32_417) | c6_2(X32_417, a545)))).
% 34.43/14.19  tff(c_8674, plain, (![X32_325, X33_327, X34_326]: (~c8_2(X32_325, a511) | ~c2_2(X32_325, X33_327) | c8_2(X32_325, X33_327) | ~c2_1(X32_325) | c6_2(X32_325, a545) | ~c2_2(X32_325, X34_326) | ~c10_2(X32_325, X34_326) | ~c4_2(X32_325, X34_326) | c6_2(X32_325, X34_326) | c5_2(X32_325, X33_327) | c4_2(X32_325, X33_327) | ~ndr1_1(X32_325) | c6_1(X32_325)))).
% 34.43/14.19  tff(c_8814, plain, (![X32_334, X34_336, X33_335]: (c6_2(X32_334, a545) | ~c2_2(X32_334, X34_336) | ~c10_2(X32_334, X34_336) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | c8_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, X34_336) | c6_2(X32_334, X34_336) | c5_2(X32_334, X33_335) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.19  tff(c_8672, plain, (![X32_325, X33_327, X34_326]: (c1_2(X32_325, a511) | ~c2_2(X32_325, X33_327) | c8_2(X32_325, X33_327) | ~c2_1(X32_325) | c6_2(X32_325, a545) | ~c2_2(X32_325, X34_326) | ~c10_2(X32_325, X34_326) | ~c4_2(X32_325, X34_326) | c6_2(X32_325, X34_326) | c5_2(X32_325, X33_327) | c4_2(X32_325, X33_327) | ~ndr1_1(X32_325) | c6_1(X32_325)))).
% 34.43/14.19  tff(c_8673, plain, (![X32_325, X33_327, X34_326]: (c4_2(X32_325, a511) | ~c2_2(X32_325, X33_327) | c8_2(X32_325, X33_327) | ~c2_1(X32_325) | c6_2(X32_325, a545) | ~c2_2(X32_325, X34_326) | ~c10_2(X32_325, X34_326) | ~c4_2(X32_325, X34_326) | c6_2(X32_325, X34_326) | c5_2(X32_325, X33_327) | c4_2(X32_325, X33_327) | ~ndr1_1(X32_325) | c6_1(X32_325)))).
% 34.43/14.19  tff(c_8724, plain, (![X32_328, X33_330, X34_329]: (c1_2(X32_328, a511) | ~c2_2(X32_328, X33_330) | c8_2(X32_328, X33_330) | ~c2_1(X32_328) | c4_2(X32_328, a545) | ~c2_2(X32_328, X34_329) | ~c10_2(X32_328, X34_329) | ~c4_2(X32_328, X34_329) | c6_2(X32_328, X34_329) | c5_2(X32_328, X33_330) | c4_2(X32_328, X33_330) | ~ndr1_1(X32_328) | c6_1(X32_328)))).
% 34.43/14.19  tff(c_8725, plain, (![X32_328, X33_330, X34_329]: (c4_2(X32_328, a511) | ~c2_2(X32_328, X33_330) | c8_2(X32_328, X33_330) | ~c2_1(X32_328) | c4_2(X32_328, a545) | ~c2_2(X32_328, X34_329) | ~c10_2(X32_328, X34_329) | ~c4_2(X32_328, X34_329) | c6_2(X32_328, X34_329) | c5_2(X32_328, X33_330) | c4_2(X32_328, X33_330) | ~ndr1_1(X32_328) | c6_1(X32_328)))).
% 34.43/14.19  tff(c_8891, plain, (![X32_337, X34_339, X33_338]: (c4_2(X32_337, a545) | ~c2_2(X32_337, X34_339) | ~c10_2(X32_337, X34_339) | c1_2(X32_337, a511) | ~c2_2(X32_337, X33_338) | c8_2(X32_337, X33_338) | ~c2_1(X32_337) | ~c4_2(X32_337, X34_339) | c6_2(X32_337, X34_339) | c5_2(X32_337, X33_338) | c4_2(X32_337, X33_338) | ~ndr1_1(X32_337) | c6_1(X32_337)))).
% 34.43/14.19  tff(c_8726, plain, (![X32_328, X33_330, X34_329]: (~c8_2(X32_328, a511) | ~c2_2(X32_328, X33_330) | c8_2(X32_328, X33_330) | ~c2_1(X32_328) | c4_2(X32_328, a545) | ~c2_2(X32_328, X34_329) | ~c10_2(X32_328, X34_329) | ~c4_2(X32_328, X34_329) | c6_2(X32_328, X34_329) | c5_2(X32_328, X33_330) | c4_2(X32_328, X33_330) | ~ndr1_1(X32_328) | c6_1(X32_328)))).
% 34.43/14.19  tff(c_8813, plain, (![X32_334, X34_336, X33_335]: (c4_2(X32_334, a545) | ~c2_2(X32_334, X34_336) | ~c10_2(X32_334, X34_336) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | c8_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, X34_336) | c6_2(X32_334, X34_336) | c5_2(X32_334, X33_335) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.19  tff(c_8892, plain, (![X32_337, X34_339, X33_338]: (c6_2(X32_337, a545) | ~c2_2(X32_337, X34_339) | ~c10_2(X32_337, X34_339) | c1_2(X32_337, a511) | ~c2_2(X32_337, X33_338) | c8_2(X32_337, X33_338) | ~c2_1(X32_337) | ~c4_2(X32_337, X34_339) | c6_2(X32_337, X34_339) | c5_2(X32_337, X33_338) | c4_2(X32_337, X33_338) | ~ndr1_1(X32_337) | c6_1(X32_337)))).
% 34.43/14.19  tff(c_9648, plain, (~c1_1(a513))).
% 34.43/14.19  tff(c_9637, plain, (![X137_178]: (c5_2(X137_178, a576) | ~c1_1(X137_178) | c8_1(X137_178)))).
% 34.43/14.19  tff(c_9016, plain, (![X32_344, X33_345, X34_346]: (c3_2(X32_344, X33_345) | c1_1(X32_344) | c4_2(X32_344, a545) | ~c10_2(X32_344, X33_345) | c4_2(X32_344, a511) | ~c2_2(X32_344, X33_345) | ~c2_1(X32_344) | ~c4_2(X32_344, X34_346) | c8_2(X32_344, X34_346) | c6_2(X32_344, X34_346) | c4_2(X32_344, X33_345) | ~ndr1_1(X32_344) | c6_1(X32_344)))).
% 34.43/14.19  tff(c_9154, plain, (![X32_353, X33_354, X34_355]: (c3_2(X32_353, X33_354) | c1_1(X32_353) | c6_2(X32_353, a545) | ~c10_2(X32_353, X33_354) | c1_2(X32_353, a511) | ~c2_2(X32_353, X33_354) | ~c2_1(X32_353) | ~c4_2(X32_353, X34_355) | c8_2(X32_353, X34_355) | c6_2(X32_353, X34_355) | c4_2(X32_353, X33_354) | ~ndr1_1(X32_353) | c6_1(X32_353)))).
% 34.43/14.19  tff(c_9062, plain, (![X32_347, X33_348, X34_349]: (c3_2(X32_347, X33_348) | c1_1(X32_347) | c6_2(X32_347, a545) | ~c10_2(X32_347, X33_348) | c4_2(X32_347, a511) | ~c2_2(X32_347, X33_348) | ~c2_1(X32_347) | ~c4_2(X32_347, X34_349) | c8_2(X32_347, X34_349) | c6_2(X32_347, X34_349) | c4_2(X32_347, X33_348) | ~ndr1_1(X32_347) | c6_1(X32_347)))).
% 34.43/14.19  tff(c_9108, plain, (![X32_350, X33_351, X34_352]: (c3_2(X32_350, X33_351) | c1_1(X32_350) | c4_2(X32_350, a545) | ~c10_2(X32_350, X33_351) | c1_2(X32_350, a511) | ~c2_2(X32_350, X33_351) | ~c2_1(X32_350) | ~c4_2(X32_350, X34_352) | c8_2(X32_350, X34_352) | c6_2(X32_350, X34_352) | c4_2(X32_350, X33_351) | ~ndr1_1(X32_350) | c6_1(X32_350)))).
% 34.43/14.19  tff(c_9430, plain, (![X137_178]: (~c7_2(X137_178, a576) | ~c1_1(X137_178) | c8_1(X137_178)))).
% 34.43/14.19  tff(c_9390, plain, (![X137_178]: (~c6_2(X137_178, a576) | ~c1_1(X137_178) | c8_1(X137_178)))).
% 34.43/14.19  tff(c_9355, plain, (c10_1(a600))).
% 34.43/14.19  tff(c_8922, plain, (![X32_340, X33_341]: (c6_2(X32_340, a545) | ~c10_2(X32_340, X33_341) | ~c9_1(X32_340) | ~c1_1(X32_340) | c4_2(X32_340, a511) | ~c2_2(X32_340, X33_341) | ~c2_1(X32_340) | ~c4_2(X32_340, a518) | c6_2(X32_340, a518) | c5_2(X32_340, X33_341) | c4_2(X32_340, X33_341) | ~ndr1_1(X32_340) | c6_1(X32_340)))).
% 34.43/14.19  tff(c_9321, plain, (~c1_1(a595))).
% 34.43/14.19  tff(c_9288, plain, (![X137_178]: (ndr1_1(X137_178) | ~c1_1(X137_178) | c8_1(X137_178)))).
% 34.43/14.19  tff(c_8951, plain, (![X32_342, X33_343]: (c6_2(X32_342, a545) | ~c10_2(X32_342, X33_343) | ~c9_1(X32_342) | ~c1_1(X32_342) | c1_2(X32_342, a511) | ~c2_2(X32_342, X33_343) | ~c2_1(X32_342) | ~c4_2(X32_342, a518) | c6_2(X32_342, a518) | c5_2(X32_342, X33_343) | c4_2(X32_342, X33_343) | ~ndr1_1(X32_342) | c6_1(X32_342)))).
% 34.43/14.19  tff(c_8921, plain, (![X32_340, X33_341]: (c4_2(X32_340, a545) | ~c10_2(X32_340, X33_341) | ~c9_1(X32_340) | ~c1_1(X32_340) | c4_2(X32_340, a511) | ~c2_2(X32_340, X33_341) | ~c2_1(X32_340) | ~c4_2(X32_340, a518) | c6_2(X32_340, a518) | c5_2(X32_340, X33_341) | c4_2(X32_340, X33_341) | ~ndr1_1(X32_340) | c6_1(X32_340)))).
% 34.43/14.19  tff(c_8950, plain, (![X32_342, X33_343]: (c4_2(X32_342, a545) | ~c10_2(X32_342, X33_343) | ~c9_1(X32_342) | ~c1_1(X32_342) | c1_2(X32_342, a511) | ~c2_2(X32_342, X33_343) | ~c2_1(X32_342) | ~c4_2(X32_342, a518) | c6_2(X32_342, a518) | c5_2(X32_342, X33_343) | c4_2(X32_342, X33_343) | ~ndr1_1(X32_342) | c6_1(X32_342)))).
% 34.43/14.19  tff(c_8883, plain, (![X32_337, X33_338, X34_339]: (c6_2(X32_337, a545) | ~c10_2(X32_337, X33_338) | c1_2(X32_337, a511) | ~c2_2(X32_337, X33_338) | ~c2_1(X32_337) | ~c4_2(X32_337, X34_339) | c8_2(X32_337, X34_339) | c6_2(X32_337, X34_339) | c5_2(X32_337, X33_338) | c4_2(X32_337, X33_338) | ~ndr1_1(X32_337) | c6_1(X32_337)))).
% 34.43/14.19  tff(c_8882, plain, (![X32_337, X33_338, X34_339]: (c4_2(X32_337, a545) | ~c10_2(X32_337, X33_338) | c1_2(X32_337, a511) | ~c2_2(X32_337, X33_338) | ~c2_1(X32_337) | ~c4_2(X32_337, X34_339) | c8_2(X32_337, X34_339) | c6_2(X32_337, X34_339) | c5_2(X32_337, X33_338) | c4_2(X32_337, X33_338) | ~ndr1_1(X32_337) | c6_1(X32_337)))).
% 34.43/14.19  tff(c_8806, plain, (![X32_334, X33_335, X34_336]: (c6_2(X32_334, a545) | ~c10_2(X32_334, X33_335) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, X34_336) | c8_2(X32_334, X34_336) | c6_2(X32_334, X34_336) | c5_2(X32_334, X33_335) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.19  tff(c_8805, plain, (![X32_334, X33_335, X34_336]: (c4_2(X32_334, a545) | ~c10_2(X32_334, X33_335) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, X34_336) | c8_2(X32_334, X34_336) | c6_2(X32_334, X34_336) | c5_2(X32_334, X33_335) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.19  tff(c_8968, plain, (c7_2(a584, a585))).
% 34.43/14.20  tff(c_8967, plain, (~c2_2(a584, a585))).
% 34.43/14.20  tff(c_8966, plain, (~c1_1(a584))).
% 34.43/14.20  tff(c_8958, plain, (~c4_2(a584, a585))).
% 34.43/14.20  tff(c_8957, plain, (~c1_2(a489, a511))).
% 34.43/14.20  tff(c_8893, plain, (![X32_337, X33_338]: (~c9_1(X32_337) | ~c1_1(X32_337) | c1_2(X32_337, a511) | ~c2_2(X32_337, X33_338) | c8_2(X32_337, X33_338) | ~c2_1(X32_337) | ~c4_2(X32_337, a518) | c6_2(X32_337, a518) | c5_2(X32_337, X33_338) | c4_2(X32_337, X33_338) | ~ndr1_1(X32_337) | c6_1(X32_337)))).
% 34.43/14.20  tff(c_8815, plain, (![X32_334, X33_335]: (~c9_1(X32_334) | ~c1_1(X32_334) | c4_2(X32_334, a511) | ~c2_2(X32_334, X33_335) | c8_2(X32_334, X33_335) | ~c2_1(X32_334) | ~c4_2(X32_334, a518) | c6_2(X32_334, a518) | c5_2(X32_334, X33_335) | c4_2(X32_334, X33_335) | ~ndr1_1(X32_334) | c6_1(X32_334)))).
% 34.43/14.20  tff(c_8897, plain, (~c8_1(a584))).
% 34.43/14.20  tff(c_8220, plain, (![X32_302, X33_304, X34_303]: (c1_2(X32_302, a511) | ~c2_2(X32_302, X33_304) | c8_2(X32_302, X33_304) | ~c2_1(X32_302) | ~c4_2(X32_302, X34_303) | c8_2(X32_302, X34_303) | c6_2(X32_302, X34_303) | c5_2(X32_302, X33_304) | c4_2(X32_302, X33_304) | ~ndr1_1(X32_302) | c6_1(X32_302)))).
% 34.43/14.20  tff(c_8819, plain, (~c4_2(a485, a487))).
% 34.43/14.20  tff(c_8221, plain, (![X32_302, X33_304, X34_303]: (c4_2(X32_302, a511) | ~c2_2(X32_302, X33_304) | c8_2(X32_302, X33_304) | ~c2_1(X32_302) | ~c4_2(X32_302, X34_303) | c8_2(X32_302, X34_303) | c6_2(X32_302, X34_303) | c5_2(X32_302, X33_304) | c4_2(X32_302, X33_304) | ~ndr1_1(X32_302) | c6_1(X32_302)))).
% 34.43/14.20  tff(c_8222, plain, (![X32_302, X33_304, X34_303]: (~c8_2(X32_302, a511) | ~c2_2(X32_302, X33_304) | c8_2(X32_302, X33_304) | ~c2_1(X32_302) | ~c4_2(X32_302, X34_303) | c8_2(X32_302, X34_303) | c6_2(X32_302, X34_303) | c5_2(X32_302, X33_304) | c4_2(X32_302, X33_304) | ~ndr1_1(X32_302) | c6_1(X32_302)))).
% 34.43/14.20  tff(c_8731, plain, (c6_1(a501))).
% 34.43/14.20  tff(c_8732, plain, (ndr1_1(a584))).
% 34.43/14.20  tff(c_8373, plain, (![X32_47, X34_51, X33_50]: (c4_2(X32_47, a545) | ~c2_2(X32_47, X34_51) | ~c10_2(X32_47, X34_51) | ~c4_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c9_2(X32_47, X33_50) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.20  tff(c_8679, plain, (c6_1(a542))).
% 34.43/14.20  tff(c_8328, plain, (![X32_47, X34_51, X33_50]: (c6_2(X32_47, a545) | ~c2_2(X32_47, X34_51) | ~c10_2(X32_47, X34_51) | ~c4_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c9_2(X32_47, X33_50) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.20  tff(c_8597, plain, (![X73_320]: (c1_2(X73_320, a475) | ~c2_1(X73_320) | ~c2_2(X73_320, a520) | ~c3_2(X73_320, a476) | c1_2(X73_320, a476) | ~ndr1_1(X73_320) | ~c1_1(X73_320)))).
% 34.43/14.20  tff(c_8598, plain, (![X73_320]: (~c7_1(X73_320) | ~c6_1(X73_320) | ~c2_2(X73_320, a520) | ~c3_2(X73_320, a433) | c1_2(X73_320, a433) | ~ndr1_1(X73_320) | ~c1_1(X73_320)))).
% 34.43/14.20  tff(c_8599, plain, (![X73_320]: (c2_1(X73_320) | c10_1(X73_320) | ~c2_2(X73_320, a520) | ~c3_2(X73_320, a478) | c1_2(X73_320, a478) | ~ndr1_1(X73_320) | ~c1_1(X73_320)))).
% 34.43/14.20  tff(c_8613, plain, (~c1_1(a470))).
% 34.43/14.20  tff(c_8612, plain, (~c3_2(a479, a481))).
% 34.43/14.20  tff(c_8611, plain, (~c1_1(a524))).
% 34.43/14.20  tff(c_8610, plain, (~c1_1(a491))).
% 34.43/14.20  tff(c_8568, plain, (![X73_99, X74_101]: (~c2_2(X73_99, a520) | ~c3_2(X73_99, X74_101) | c4_2(X73_99, X74_101) | c1_2(X73_99, X74_101) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.20  tff(c_8564, plain, (~c1_1(a501))).
% 34.43/14.20  tff(c_8563, plain, (~c1_1(a542))).
% 34.43/14.20  tff(c_8492, plain, (![X73_99, X74_101]: (c8_2(X73_99, a520) | ~c3_2(X73_99, X74_101) | c4_2(X73_99, X74_101) | c1_2(X73_99, X74_101) | ~ndr1_1(X73_99) | ~c1_1(X73_99)))).
% 34.43/14.20  tff(c_8488, plain, (~c2_2(a513, a545))).
% 34.43/14.20  tff(c_8487, plain, (~c2_1(a513))).
% 34.43/14.20  tff(c_8484, plain, (~c6_1(a513))).
% 34.43/14.20  tff(c_8467, plain, (![X65_311]: (~c10_2(a513, X65_311) | ~c5_2(a513, X65_311) | ~c2_2(a513, X65_311)))).
% 34.43/14.20  tff(c_8464, plain, (~c2_2(a513, a518))).
% 34.43/14.20  tff(c_8439, plain, (![X65_89]: (~c5_2(a513, X65_89) | ~c2_2(a513, X65_89) | c8_2(a513, X65_89)))).
% 34.43/14.20  tff(c_8438, plain, (~c1_2(a489, a545))).
% 34.43/14.20  tff(c_8437, plain, (ndr1_1(a513))).
% 34.43/14.20  tff(c_8401, plain, (c4_2(a489, a545))).
% 34.43/14.20  tff(c_8392, plain, (![X99_130, X100_132]: (~c8_2(X99_130, a545) | ~c8_2(X99_130, X100_132) | ~c2_2(X99_130, X100_132) | ~c10_2(X99_130, X100_132) | ~ndr1_1(X99_130)))).
% 34.43/14.20  tff(c_8389, plain, (c6_2(a489, a545))).
% 34.43/14.20  tff(c_8352, plain, (![X99_130, X100_132]: (c4_2(X99_130, a545) | ~c8_2(X99_130, X100_132) | ~c2_2(X99_130, X100_132) | ~c10_2(X99_130, X100_132) | ~ndr1_1(X99_130)))).
% 34.43/14.20  tff(c_8353, plain, (~c10_2(a521, a522))).
% 34.43/14.20  tff(c_8349, plain, (~c10_2(a470, a471))).
% 34.43/14.20  tff(c_8348, plain, (~c10_2(a479, a481))).
% 34.43/14.20  tff(c_8347, plain, (c10_1(a609))).
% 34.43/14.20  tff(c_8346, plain, (~c1_1(a609))).
% 34.43/14.20  tff(c_8345, plain, (~c6_1(a595))).
% 34.43/14.20  tff(c_8344, plain, (c10_1(a595))).
% 34.43/14.20  tff(c_8308, plain, (~c6_1(a609))).
% 34.43/14.20  tff(c_8305, plain, (![X99_130, X100_132]: (c6_2(X99_130, a545) | ~c8_2(X99_130, X100_132) | ~c2_2(X99_130, X100_132) | ~c10_2(X99_130, X100_132) | ~ndr1_1(X99_130)))).
% 34.43/14.20  tff(c_8307, plain, (c5_1(a609))).
% 34.43/14.20  tff(c_8306, plain, (~c4_1(a609))).
% 34.43/14.20  tff(c_8302, plain, (~c2_1(a609))).
% 34.43/14.20  tff(c_8273, plain, (c5_1(a595))).
% 34.43/14.20  tff(c_8274, plain, (~ndr1_1(a609))).
% 34.43/14.20  tff(c_8266, plain, (~c4_1(a595))).
% 34.43/14.20  tff(c_8272, plain, (~c2_1(a595))).
% 34.43/14.20  tff(c_8242, plain, (~ndr1_1(a595))).
% 34.43/14.20  tff(c_8241, plain, (c10_1(a514))).
% 34.43/14.20  tff(c_8240, plain, (~c8_1(a514))).
% 34.43/14.20  tff(c_8237, plain, (c6_1(a579))).
% 34.43/14.20  tff(c_8236, plain, (c6_1(a508))).
% 34.43/14.20  tff(c_8233, plain, (~c6_1(a546))).
% 34.43/14.20  tff(c_8232, plain, (c2_1(a546))).
% 34.43/14.20  tff(c_8188, plain, (~c2_2(a546, a504))).
% 34.43/14.20  tff(c_8189, plain, (![X32_47, X34_51, X33_50]: (~c4_2(X32_47, X34_51) | c8_2(X32_47, X34_51) | c6_2(X32_47, X34_51) | c9_2(X32_47, X33_50) | c5_2(X32_47, X33_50) | c4_2(X32_47, X33_50) | ~ndr1_1(X32_47) | c6_1(X32_47)))).
% 34.43/14.20  tff(c_8172, plain, (![X102_134]: (~c3_2(a546, X102_134) | ~c2_2(a546, X102_134)))).
% 34.43/14.20  tff(c_8171, plain, (ndr1_1(a546))).
% 34.43/14.20  tff(c_8095, plain, (~c2_1(a470))).
% 34.43/14.20  tff(c_8094, plain, (~c2_1(a491))).
% 34.43/14.20  tff(c_8079, plain, (![X84_112]: (~c8_1(X84_112) | ~c2_1(X84_112) | c10_1(X84_112)))).
% 34.43/14.20  tff(c_8065, plain, (~c10_1(a591))).
% 34.43/14.20  tff(c_8066, plain, (~c10_1(a479))).
% 34.43/14.20  tff(c_8068, plain, (~c10_1(a610))).
% 34.43/14.20  tff(c_8069, plain, (~c10_1(a485))).
% 34.43/14.20  tff(c_8067, plain, (~c10_1(a571))).
% 34.43/14.20  tff(c_8048, plain, (![X43_60]: (~c10_1(X43_60) | ~c1_1(X43_60)))).
% 34.43/14.20  tff(c_8041, plain, (c1_1(a591))).
% 34.43/14.20  tff(c_8036, plain, (![X96_126]: (~c9_1(X96_126) | c1_1(X96_126)))).
% 34.43/14.20  tff(c_8033, plain, (~c1_2(a579, a580))).
% 34.43/14.20  tff(c_8018, plain, (~c9_2(a579, a580))).
% 34.43/14.20  tff(c_8008, plain, (c8_2(a521, a522))).
% 34.43/14.20  tff(c_8005, plain, (~c3_2(a579, a580))).
% 34.43/14.20  tff(c_8001, plain, (~c2_1(a521))).
% 34.43/14.20  tff(c_7970, plain, (c9_2(a521, a522))).
% 34.43/14.20  tff(c_7966, plain, (c3_2(a521, a522))).
% 34.43/14.20  tff(c_7959, plain, (~c3_1(a609))).
% 34.43/14.20  tff(c_7954, plain, (~c7_2(a591, a592))).
% 34.43/14.20  tff(c_7950, plain, (~c1_2(a591, a592))).
% 34.43/14.20  tff(c_7947, plain, (c7_1(a579))).
% 34.43/14.20  tff(c_7944, plain, (c4_2(a591, a592))).
% 34.43/14.20  tff(c_7943, plain, (ndr1_1(a521))).
% 34.43/14.20  tff(c_7941, plain, (~c1_1(a579))).
% 34.43/14.20  tff(c_7935, plain, (ndr1_1(a579))).
% 34.43/14.20  tff(c_7929, plain, (c10_1(a513))).
% 34.43/14.20  tff(c_7924, plain, (~c9_1(a595))).
% 34.43/14.20  tff(c_7923, plain, (~c1_1(a489))).
% 34.43/14.20  tff(c_7918, plain, (~c1_2(a489, a518))).
% 34.43/14.20  tff(c_7911, plain, (![X41_58]: (~c1_2(a489, X41_58) | c8_2(a489, X41_58) | c3_2(a489, X41_58)))).
% 34.43/14.20  tff(c_7910, plain, (ndr1_1(a489))).
% 34.43/14.20  tff(c_7839, plain, (![X63_86, X64_88]: (~c3_2(X63_86, a512) | ~c9_2(X63_86, X64_88) | ~c7_2(X63_86, X64_88) | ~c4_2(X63_86, X64_88) | ~ndr1_1(X63_86) | ~c2_1(X63_86)))).
% 34.43/14.20  tff(c_7838, plain, (~c3_1(a591))).
% 34.43/14.20  tff(c_7834, plain, (c9_1(a591))).
% 34.43/14.20  tff(c_7830, plain, (~c3_1(a595))).
% 34.43/14.20  tff(c_7798, plain, (![X63_86, X64_88]: (~c4_2(X63_86, a512) | ~c9_2(X63_86, X64_88) | ~c7_2(X63_86, X64_88) | ~c4_2(X63_86, X64_88) | ~ndr1_1(X63_86) | ~c2_1(X63_86)))).
% 34.43/14.20  tff(c_7795, plain, (c3_1(a513))).
% 34.43/14.20  tff(c_7794, plain, (ndr1_1(a591))).
% 34.43/14.20  tff(c_7790, plain, (c6_1(a591))).
% 34.43/14.20  tff(c_7788, plain, (c6_1(a510))).
% 34.43/14.20  tff(c_7787, plain, (~c8_1(a510))).
% 34.43/14.20  tff(c_7784, plain, (~c1_1(a540))).
% 34.74/14.20  tff(c_7783, plain, (~c6_1(a540))).
% 34.74/14.20  tff(c_7780, plain, (~c4_1(a540))).
% 34.74/14.20  tff(c_7774, plain, (c10_1(a540))).
% 34.74/14.20  tff(c_7770, plain, (c5_1(a540))).
% 34.74/14.20  tff(c_7778, plain, (~c3_1(a540))).
% 34.74/14.20  tff(c_7745, plain, (~ndr1_1(a540))).
% 34.74/14.20  tff(c_7742, plain, (c3_1(a546))).
% 34.74/14.20  tff(c_7739, plain, (c7_1(a510))).
% 34.74/14.20  tff(c_4758, plain, (![X61_83, X62_85]: (c1_2(X61_83, a511) | ~c9_2(X61_83, X62_85) | ~c2_2(X61_83, X62_85) | c8_2(X61_83, X62_85) | ~ndr1_1(X61_83) | ~c2_1(X61_83)))).
% 34.74/14.20  tff(c_7703, plain, (~c1_1(a474))).
% 34.74/14.20  tff(c_7671, plain, (~c6_1(a474))).
% 34.74/14.20  tff(c_4760, plain, (![X61_83, X62_85]: (c4_2(X61_83, a511) | ~c9_2(X61_83, X62_85) | ~c2_2(X61_83, X62_85) | c8_2(X61_83, X62_85) | ~ndr1_1(X61_83) | ~c2_1(X61_83)))).
% 34.74/14.20  tff(c_7670, plain, (~c4_1(a474))).
% 34.74/14.20  tff(c_7669, plain, (~c3_1(a474))).
% 34.74/14.20  tff(c_7662, plain, (c5_1(a474))).
% 34.74/14.20  tff(c_7668, plain, (~c2_1(a474))).
% 34.74/14.20  tff(c_7637, plain, (~ndr1_1(a474))).
% 34.74/14.20  tff(c_7613, plain, (~c2_1(a468))).
% 34.74/14.20  tff(c_7612, plain, (~c2_1(a479))).
% 34.74/14.20  tff(c_4762, plain, (![X61_83, X62_85]: (~c8_2(X61_83, a511) | ~c9_2(X61_83, X62_85) | ~c2_2(X61_83, X62_85) | c8_2(X61_83, X62_85) | ~ndr1_1(X61_83) | ~c2_1(X61_83)))).
% 34.74/14.20  tff(c_7578, plain, (![X57_78]: (~c5_2(X57_78, a507) | ~c4_1(X57_78) | c9_1(X57_78)))).
% 34.74/14.20  tff(c_7569, plain, (c5_2(a542, a432))).
% 34.74/14.21  tff(c_7566, plain, (c10_2(a542, a432))).
% 34.74/14.21  tff(c_7563, plain, (c4_2(a542, a432))).
% 34.74/14.21  tff(c_7560, plain, (c2_1(a542))).
% 34.74/14.21  tff(c_7536, plain, (![X93_123]: (~c6_2(a542, X93_123) | c3_2(a542, X93_123)))).
% 34.74/14.21  tff(c_7535, plain, (ndr1_1(a542))).
% 34.74/14.21  tff(c_7498, plain, (![V_280]: (c3_2(V_280, a433) | ~ndr1_1(V_280) | c1_1(V_280) | ~c7_1(V_280) | ~c6_1(V_280)))).
% 34.74/14.21  tff(c_7492, plain, (c1_1(a479))).
% 34.74/14.21  tff(c_7465, plain, (![W_3, X_5]: (~c5_2(W_3, X_5) | c4_2(W_3, X_5) | c3_2(W_3, X_5) | ~ndr1_1(W_3) | c1_1(W_3)))).
% 34.74/14.21  tff(c_7461, plain, (![X57_78]: (~c2_2(X57_78, a507) | ~c4_1(X57_78) | c9_1(X57_78)))).
% 34.74/14.21  tff(c_7456, plain, (![X57_78]: (c1_2(X57_78, a507) | ~c4_1(X57_78) | c9_1(X57_78)))).
% 34.74/14.21  tff(c_7449, plain, (~c4_1(a503))).
% 34.74/14.21  tff(c_7448, plain, (~c4_1(a615))).
% 34.74/14.21  tff(c_7447, plain, (~c4_1(a619))).
% 34.74/14.21  tff(c_7433, plain, (![X57_78]: (ndr1_1(X57_78) | ~c4_1(X57_78) | c9_1(X57_78)))).
% 34.74/14.21  tff(c_7429, plain, (~c6_1(a619))).
% 34.74/14.21  tff(c_7428, plain, (c10_1(a619))).
% 34.74/14.21  tff(c_7427, plain, (~c1_1(a619))).
% 34.74/14.21  tff(c_7426, plain, (~c2_1(a619))).
% 34.74/14.21  tff(c_7401, plain, (~ndr1_1(a619))).
% 34.74/14.21  tff(c_7378, plain, (~c8_1(a540))).
% 34.74/14.21  tff(c_7368, plain, (~c4_2(a470, a475))).
% 34.74/14.21  tff(c_7367, plain, (~c2_1(a501))).
% 34.74/14.21  tff(c_7366, plain, (~c2_1(a540))).
% 34.74/14.21  tff(c_7359, plain, (![X162_213]: (~c2_2(X162_213, a596) | c8_1(X162_213) | c5_1(X162_213)))).
% 34.74/14.21  tff(c_7340, plain, (![X162_213]: (~c5_2(X162_213, a596) | c8_1(X162_213) | c5_1(X162_213)))).
% 34.74/14.21  tff(c_7336, plain, (~c10_2(a581, a582))).
% 34.74/14.21  tff(c_7335, plain, (ndr1_1(a541))).
% 34.74/14.21  tff(c_7302, plain, (~c3_2(a588, a589))).
% 34.74/14.21  tff(c_7290, plain, (~c1_2(a588, a589))).
% 34.74/14.21  tff(c_7276, plain, (![X28_42]: (~c4_2(a468, X28_42) | c9_2(a468, X28_42) | c1_2(a468, X28_42)))).
% 34.74/14.21  tff(c_7265, plain, (c6_2(a588, a589))).
% 34.74/14.21  tff(c_7262, plain, (c4_2(a581, a582))).
% 34.74/14.21  tff(c_7261, plain, (c6_1(a571))).
% 34.74/14.21  tff(c_7248, plain, (~c1_2(a501, a478))).
% 34.74/14.21  tff(c_7246, plain, (c5_1(a503))).
% 34.74/14.21  tff(c_7245, plain, (c5_1(a615))).
% 34.74/14.21  tff(c_7238, plain, (![U_1]: (c6_2(U_1, a431) | c4_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7228, plain, (![X162_213]: (ndr1_1(X162_213) | c8_1(X162_213) | c5_1(X162_213)))).
% 34.74/14.21  tff(c_7226, plain, (c1_1(a571))).
% 34.74/14.21  tff(c_7218, plain, (ndr1_1(a588))).
% 34.74/14.21  tff(c_7215, plain, (![U_1]: (~c10_2(U_1, a431) | c5_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7213, plain, (![U_1]: (c1_2(U_1, a431) | c10_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7211, plain, (c1_1(a610))).
% 34.74/14.21  tff(c_7208, plain, (~c3_1(a588))).
% 34.74/14.21  tff(c_7207, plain, (c7_1(a571))).
% 34.74/14.21  tff(c_7202, plain, (~c1_1(a588))).
% 34.74/14.21  tff(c_7198, plain, (ndr1_1(a581))).
% 34.74/14.21  tff(c_7194, plain, (![U_1]: (~c10_2(U_1, a431) | c4_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7193, plain, (c10_1(a615))).
% 34.74/14.21  tff(c_7192, plain, (~c3_1(a615))).
% 34.74/14.21  tff(c_7189, plain, (~c6_1(a615))).
% 34.74/14.21  tff(c_7191, plain, (~c2_1(a615))).
% 34.74/14.21  tff(c_7169, plain, (~ndr1_1(a615))).
% 34.74/14.21  tff(c_7168, plain, (~c2_1(a581))).
% 34.74/14.21  tff(c_7159, plain, (![U_1]: (c6_2(U_1, a431) | c5_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7152, plain, (![U_1]: (c6_2(U_1, a431) | c10_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7150, plain, (![U_1]: (c1_2(U_1, a431) | c4_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7146, plain, (![U_1]: (~c10_2(U_1, a431) | c10_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7122, plain, (![X29_43]: (~c4_2(a470, X29_43) | c7_2(a470, X29_43) | c3_2(a470, X29_43)))).
% 34.74/14.21  tff(c_7114, plain, (![U_1]: (c1_2(U_1, a431) | c5_2(U_1, a432) | ~c2_1(U_1)))).
% 34.74/14.21  tff(c_7100, plain, (~c9_2(a508, a509))).
% 34.74/14.21  tff(c_7097, plain, (c3_1(a489))).
% 34.74/14.21  tff(c_7090, plain, (![X37_54]: (c1_2(X37_54, a475) | ~c4_2(X37_54, a476) | ~c2_1(X37_54)))).
% 34.74/14.21  tff(c_7088, plain, (~c5_2(a508, a509))).
% 34.74/14.21  tff(c_7084, plain, (~c9_1(a539))).
% 34.74/14.21  tff(c_7080, plain, (![X71_97]: (c4_2(X71_97, a518) | ~c9_1(X71_97) | ~c1_1(X71_97)))).
% 34.74/14.21  tff(c_7075, plain, (![X37_54]: (~c7_2(X37_54, a475) | c2_2(X37_54, a476) | ~c2_1(X37_54)))).
% 34.74/14.21  tff(c_7073, plain, (![X71_97]: (c1_2(X71_97, a518) | ~c9_1(X71_97) | ~c1_1(X71_97)))).
% 34.74/14.21  tff(c_7066, plain, (![X37_54]: (~c7_2(X37_54, a475) | ~c10_2(X37_54, a476) | ~c2_1(X37_54)))).
% 34.74/14.21  tff(c_7064, plain, (![X71_97]: (~c8_2(X71_97, a518) | ~c9_1(X71_97) | ~c1_1(X71_97)))).
% 34.74/14.21  tff(c_7051, plain, (~c8_1(a489))).
% 34.74/14.21  tff(c_7054, plain, (![X47_65]: (~c6_2(a501, X47_65) | ~c1_2(a501, X47_65) | c3_2(a501, X47_65)))).
% 34.74/14.21  tff(c_7048, plain, (![X37_54]: (c1_2(X37_54, a475) | c2_2(X37_54, a476) | ~c2_1(X37_54)))).
% 34.74/14.21  tff(c_7045, plain, (~c2_2(a508, a509))).
% 34.74/14.21  tff(c_7042, plain, (![V_2]: (c5_2(V_2, a433) | ~c7_1(V_2) | ~c6_1(V_2)))).
% 34.74/14.21  tff(c_7037, plain, (![X37_54]: (c1_2(X37_54, a475) | ~c10_2(X37_54, a476) | ~c2_1(X37_54)))).
% 34.74/14.21  tff(c_7036, plain, (c3_1(a539))).
% 34.74/14.21  tff(c_7031, plain, (![X37_54]: (~c7_2(X37_54, a475) | ~c4_2(X37_54, a476) | ~c2_1(X37_54)))).
% 34.74/14.21  tff(c_7029, plain, (![X48_66]: (~c7_2(a501, X48_66) | c9_2(a501, X48_66) | c6_2(a501, X48_66)))).
% 34.74/14.21  tff(c_7023, plain, (![V_2]: (~c4_2(V_2, a433) | ~c7_1(V_2) | ~c6_1(V_2)))).
% 34.74/14.21  tff(c_7016, plain, (![X38_55]: (~c4_2(X38_55, a478) | c2_1(X38_55) | c10_1(X38_55)))).
% 34.74/14.21  tff(c_7010, plain, (![V_2]: (~c6_2(V_2, a433) | ~c7_1(V_2) | ~c6_1(V_2)))).
% 34.74/14.21  tff(c_6999, plain, (~c10_1(a542))).
% 34.74/14.21  tff(c_6994, plain, (![X38_55]: (~c7_2(X38_55, a478) | c2_1(X38_55) | c10_1(X38_55)))).
% 34.74/14.21  tff(c_6991, plain, (c10_1(a503))).
% 34.74/14.21  tff(c_6990, plain, (~c1_1(a503))).
% 34.74/14.21  tff(c_6989, plain, (~c3_1(a503))).
% 34.74/14.21  tff(c_6988, plain, (~c2_1(a503))).
% 34.74/14.21  tff(c_6968, plain, (~ndr1_1(a503))).
% 34.74/14.21  tff(c_6954, plain, (![X38_55]: (c6_2(X38_55, a478) | c2_1(X38_55) | c10_1(X38_55)))).
% 34.74/14.21  tff(c_6947, plain, (~c6_1(a603))).
% 34.74/14.21  tff(c_6944, plain, (c3_2(a524, a525))).
% 34.74/14.21  tff(c_6940, plain, (![X71_97]: (ndr1_1(X71_97) | ~c9_1(X71_97) | ~c1_1(X71_97)))).
% 34.74/14.21  tff(c_6937, plain, (~c4_2(a524, a525))).
% 34.74/14.21  tff(c_6933, plain, (~c3_2(a485, a487))).
% 34.74/14.21  tff(c_6926, plain, (~c6_2(a485, a486))).
% 34.74/14.21  tff(c_6924, plain, (~c8_2(a485, a487))).
% 34.74/14.21  tff(c_6922, plain, (c7_2(a485, a486))).
% 34.74/14.21  tff(c_6920, plain, (~c2_2(a485, a487))).
% 34.74/14.21  tff(c_6917, plain, (c7_2(a524, a525))).
% 34.74/14.21  tff(c_6913, plain, (ndr1_1(a508))).
% 34.74/14.21  tff(c_6912, plain, (~c10_1(a603))).
% 34.74/14.21  tff(c_6910, plain, (~c8_1(a603))).
% 34.74/14.21  tff(c_6908, plain, (![X38_55]: (ndr1_1(X38_55) | c2_1(X38_55) | c10_1(X38_55)))).
% 34.74/14.21  tff(c_6900, plain, (![V_2]: (ndr1_1(V_2) | ~c7_1(V_2) | ~c6_1(V_2)))).
% 34.74/14.21  tff(c_6897, plain, (c5_2(a485, a486))).
% 34.74/14.21  tff(c_6887, plain, (ndr1_1(a485))).
% 34.74/14.21  tff(c_4698, plain, (![X51_69]: (c2_2(X51_69, a504) | ~c3_1(X51_69) | c2_1(X51_69)))).
% 34.74/14.21  tff(c_6881, plain, (~c2_1(a498))).
% 34.74/14.21  tff(c_6879, plain, (~c6_1(a498))).
% 34.74/14.21  tff(c_6874, plain, (c10_1(a474))).
% 34.74/14.21  tff(c_6872, plain, (c3_1(a524))).
% 34.74/14.21  tff(c_6864, plain, (ndr1_1(a524))).
% 34.74/14.21  tff(c_4432, plain, (![X51_69]: (c3_2(X51_69, a504) | ~c3_1(X51_69) | c2_1(X51_69)))).
% 34.74/14.21  tff(c_6859, plain, (~c8_1(a474))).
% 34.74/14.21  tff(c_6851, plain, (c1_1(a485))).
% 34.74/14.21  tff(c_6811, plain, (~c3_1(a619))).
% 34.74/14.21  tff(c_4430, plain, (![X51_69]: (ndr1_1(X51_69) | ~c3_1(X51_69) | c2_1(X51_69)))).
% 34.74/14.21  tff(c_6802, plain, (c3_2(a491, a492))).
% 34.74/14.21  tff(c_6800, plain, (c8_1(a619))).
% 34.74/14.21  tff(c_6795, plain, (~c4_2(a491, a492))).
% 34.74/14.21  tff(c_6782, plain, (~c1_2(a491, a492))).
% 34.74/14.21  tff(c_6774, plain, (c2_1(a544))).
% 34.74/14.21  tff(c_6770, plain, (c9_2(a468, a469))).
% 34.74/14.21  tff(c_6767, plain, (~c5_1(a541))).
% 34.74/14.21  tff(c_6764, plain, (~c1_1(a544))).
% 34.74/14.21  tff(c_6760, plain, (~c8_1(a541))).
% 34.74/14.21  tff(c_6756, plain, (c4_1(a500))).
% 34.74/14.21  tff(c_6751, plain, (c6_1(a544))).
% 34.74/14.21  tff(c_6744, plain, (~c1_1(a547))).
% 34.74/14.21  tff(c_6741, plain, (c10_1(a500))).
% 34.74/14.21  tff(c_6739, plain, (~c8_1(a547))).
% 34.74/14.21  tff(c_6736, plain, (c6_2(a468, a469))).
% 34.74/14.21  tff(c_6728, plain, (~c1_2(a572, a573))).
% 34.74/14.21  tff(c_6726, plain, (![X37_54]: (ndr1_1(X37_54) | ~c2_1(X37_54)))).
% 34.74/14.21  tff(c_6725, plain, (c8_2(a572, a573))).
% 34.74/14.21  tff(c_6724, plain, (c7_1(a436))).
% 34.74/14.21  tff(c_6718, plain, (~c3_1(a436))).
% 34.74/14.21  tff(c_6715, plain, (~c7_2(a468, a469))).
% 34.74/14.21  tff(c_6705, plain, (c8_1(a491))).
% 34.74/14.21  tff(c_6701, plain, (~c2_1(a499))).
% 34.74/14.21  tff(c_6697, plain, (~c9_1(a490))).
% 34.74/14.21  tff(c_6694, plain, (~c9_1(a436))).
% 34.74/14.21  tff(c_6692, plain, (~c7_2(a611, a612))).
% 34.74/14.21  tff(c_6691, plain, (~c10_2(a572, a573))).
% 34.74/14.21  tff(c_6690, plain, (~c5_2(a611, a612))).
% 34.74/14.21  tff(c_6689, plain, (~c4_1(a491))).
% 34.74/14.21  tff(c_6687, plain, (c1_2(a611, a612))).
% 34.74/14.21  tff(c_6686, plain, (ndr1_1(a491))).
% 34.74/14.21  tff(c_6679, plain, (c2_1(a516))).
% 34.74/14.21  tff(c_6674, plain, (c5_2(a479, a481))).
% 34.74/14.21  tff(c_6670, plain, (c9_2(a479, a480))).
% 34.74/14.21  tff(c_6666, plain, (c7_1(a516))).
% 34.74/14.21  tff(c_6665, plain, (~c6_1(a468))).
% 34.74/14.21  tff(c_6663, plain, (~c4_2(a479, a481))).
% 34.74/14.22  tff(c_6659, plain, (c3_2(a501, a502))).
% 34.74/14.22  tff(c_6656, plain, (~c4_1(a516))).
% 34.74/14.22  tff(c_6653, plain, (ndr1_1(a572))).
% 34.74/14.22  tff(c_6648, plain, (c8_2(a470, a471))).
% 34.74/14.22  tff(c_6578, plain, (![X66_90]: (~c9_1(X66_90) | ~c3_1(X66_90)))).
% 34.74/14.22  tff(c_6640, plain, (~c1_1(a572))).
% 34.74/14.22  tff(c_6639, plain, (~c2_2(a501, a502))).
% 34.74/14.22  tff(c_6635, plain, (c10_2(a479, a480))).
% 34.74/14.22  tff(c_6634, plain, (ndr1_1(a611))).
% 34.74/14.22  tff(c_6631, plain, (~c1_1(a615))).
% 34.74/14.22  tff(c_6628, plain, (c2_0)).
% 34.74/14.22  tff(c_6626, plain, (c6_1(a611))).
% 34.74/14.22  tff(c_6625, plain, (c7_1(a615))).
% 34.74/14.22  tff(c_6620, plain, (ndr1_1(a468))).
% 34.74/14.22  tff(c_6619, plain, (c9_2(a501, a502))).
% 34.74/14.22  tff(c_6614, plain, (c7_2(a470, a471))).
% 34.74/14.22  tff(c_6613, plain, (c8_2(a479, a481))).
% 34.74/14.22  tff(c_6609, plain, (ndr1_1(a479))).
% 34.74/14.22  tff(c_6607, plain, (c8_1(a470))).
% 34.74/14.22  tff(c_6605, plain, (c3_0)).
% 34.74/14.22  tff(c_6603, plain, (~c6_1(a503))).
% 34.74/14.22  tff(c_6601, plain, (~c5_0)).
% 34.74/14.22  tff(c_6599, plain, (ndr1_1(a501))).
% 34.74/14.22  tff(c_6598, plain, (ndr1_1(a470))).
% 34.74/14.22  tff(c_6596, plain, (~c1_0)).
% 34.74/14.22  tff(c_6593, plain, (~c4_0)).
% 34.74/14.22  tff(c_6595, plain, (~c7_0)).
% 34.74/14.22  tff(c_6592, plain, (c10_0)).
% 34.74/14.22  tff(c_6591, plain, (~c9_0)).
% 34.74/14.22  tff(c_52, plain, (~c8_0)).
% 34.74/14.22  tff(c_54, plain, (c6_0)).
% 34.74/14.22  tff(c_3166, plain, (ndr1_0)).
% 34.74/14.22  % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.74/14.22  
%------------------------------------------------------------------------------