%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN547-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 : n020.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:53 PM UTC 2025 % Result : Satisfiable 20.72s 7.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN547-1 : TPTP v9.0.0. Released v2.1.0. % 0.07/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.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 07:59:34 EDT 2025 % 0.13/0.34 % CPUTime : % 20.72/7.53 % 20.72/7.53 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.72/7.54 % 20.72/7.54 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.72/7.55 %$ c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP8 > ssSkP7 > ssSkP6 > ssSkP5 > ssSkP4 > ssSkP3 > ssSkP2 > ssSkP1 > ssSkP0 > ndr1_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC9 > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC26 > ssSkC25 > ssSkC24 > ssSkC23 > ssSkC22 > ssSkC21 > ssSkC20 > ssSkC2 > ssSkC19 > ssSkC18 > ssSkC17 > ssSkC16 > ssSkC15 > ssSkC14 > ssSkC13 > ssSkC12 > ssSkC11 > ssSkC10 > ssSkC1 > ssSkC0 > ndr1_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > 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 > a477 > a476 > a475 > a474 > a473 > a472 > a471 > a470 > a469 > a468 > a467 > a466 > a465 > a464 > a463 > a462 > a461 > a460 > a459 > a458 > a457 > a456 % 20.72/7.55 % 20.72/7.55 %Foreground sorts: % 20.72/7.55 % 20.72/7.55 % 20.72/7.55 %Background operators: % 20.72/7.55 % 20.72/7.55 % 20.72/7.55 %Foreground operators: % 20.72/7.55 tff(a565, type, a565: $i). % 20.72/7.55 tff(c7_0, type, c7_0: $o). % 20.72/7.55 tff(a492, type, a492: $i). % 20.72/7.55 tff(a544, type, a544: $i). % 20.72/7.55 tff(a577, type, a577: $i). % 20.72/7.55 tff(a586, type, a586: $i). % 20.72/7.55 tff(ssSkC8, type, ssSkC8: $o). % 20.72/7.55 tff(a473, type, a473: $i). % 20.72/7.55 tff(a601, type, a601: $i). % 20.72/7.55 tff(ssSkC7, type, ssSkC7: $o). % 20.72/7.55 tff(a506, type, a506: $i). % 20.72/7.55 tff(a457, type, a457: $i). % 20.72/7.55 tff(a600, type, a600: $i). % 20.72/7.55 tff(a580, type, a580: $i). % 20.72/7.55 tff(a535, type, a535: $i). % 20.72/7.55 tff(ssSkC21, type, ssSkC21: $o). % 20.72/7.55 tff(a542, type, a542: $i). % 20.72/7.55 tff(c4_0, type, c4_0: $o). % 20.72/7.55 tff(a541, type, a541: $i). % 20.72/7.55 tff(ssSkC10, type, ssSkC10: $o). % 20.72/7.55 tff(a556, type, a556: $i). % 20.72/7.55 tff(ssSkP0, type, ssSkP0: $i > $o). % 20.72/7.55 tff(a550, type, a550: $i). % 20.72/7.55 tff(ssSkC6, type, ssSkC6: $o). % 20.72/7.55 tff(c3_0, type, c3_0: $o). % 20.72/7.55 tff(a477, type, a477: $i). % 20.72/7.55 tff(a460, type, a460: $i). % 20.72/7.55 tff(a594, type, a594: $i). % 20.72/7.55 tff(a490, type, a490: $i). % 20.72/7.55 tff(ssSkP7, type, ssSkP7: $i > $o). % 20.72/7.55 tff(a567, type, a567: $i). % 20.72/7.55 tff(a484, type, a484: $i). % 20.72/7.55 tff(c1_2, type, c1_2: ($i * $i) > $o). % 20.72/7.55 tff(ssSkC23, type, ssSkC23: $o). % 20.72/7.55 tff(ssSkC3, type, ssSkC3: $o). % 20.72/7.55 tff(a503, type, a503: $i). % 20.72/7.55 tff(a585, type, a585: $i). % 20.72/7.55 tff(a471, type, a471: $i). % 20.72/7.55 tff(a520, type, a520: $i). % 20.72/7.55 tff(a495, type, a495: $i). % 20.72/7.55 tff(a502, type, a502: $i). % 20.72/7.55 tff(a493, type, a493: $i). % 20.72/7.55 tff(ssSkP2, type, ssSkP2: $i > $o). % 20.72/7.55 tff(a537, type, a537: $i). % 20.72/7.55 tff(ssSkC19, type, ssSkC19: $o). % 20.72/7.55 tff(a511, type, a511: $i). % 20.72/7.55 tff(a564, type, a564: $i). % 20.72/7.55 tff(a508, type, a508: $i). % 20.72/7.55 tff(a510, type, a510: $i). % 20.72/7.55 tff(ssSkC26, type, ssSkC26: $o). % 20.72/7.55 tff(a487, type, a487: $i). % 20.72/7.55 tff(a488, type, a488: $i). % 20.72/7.55 tff(a530, type, a530: $i). % 20.72/7.55 tff(a553, type, a553: $i). % 20.72/7.55 tff(a569, type, a569: $i). % 20.72/7.55 tff(a528, type, a528: $i). % 20.72/7.55 tff(a462, type, a462: $i). % 20.72/7.55 tff(a458, type, a458: $i). % 20.72/7.55 tff(c8_0, type, c8_0: $o). % 20.72/7.55 tff(a536, type, a536: $i). % 20.72/7.55 tff(a459, type, a459: $i). % 20.72/7.55 tff(a467, type, a467: $i). % 20.72/7.55 tff(a461, type, a461: $i). % 20.72/7.55 tff(a596, type, a596: $i). % 20.72/7.55 tff(a498, type, a498: $i). % 20.72/7.55 tff(ssSkC4, type, ssSkC4: $o). % 20.72/7.55 tff(a505, type, a505: $i). % 20.72/7.55 tff(a456, type, a456: $i). % 20.72/7.55 tff(a532, type, a532: $i). % 20.72/7.55 tff(a504, type, a504: $i). % 20.72/7.55 tff(a468, type, a468: $i). % 20.72/7.55 tff(c5_0, type, c5_0: $o). % 20.72/7.55 tff(ssSkC9, type, ssSkC9: $o). % 20.72/7.55 tff(ssSkP6, type, ssSkP6: $i > $o). % 20.72/7.55 tff(a539, type, a539: $i). % 20.72/7.55 tff(a551, type, a551: $i). % 20.72/7.55 tff(a572, type, a572: $i). % 20.72/7.55 tff(ssSkP8, type, ssSkP8: $i > $o). % 20.72/7.55 tff(a518, type, a518: $i). % 20.72/7.55 tff(a546, type, a546: $i). % 20.72/7.55 tff(a599, type, a599: $i). % 20.72/7.55 tff(c6_0, type, c6_0: $o). % 20.72/7.55 tff(c8_2, type, c8_2: ($i * $i) > $o). % 20.72/7.55 tff(a602, type, a602: $i). % 20.72/7.55 tff(ssSkC11, type, ssSkC11: $o). % 20.72/7.55 tff(ssSkC18, type, ssSkC18: $o). % 20.72/7.55 tff(a570, type, a570: $i). % 20.72/7.55 tff(a499, type, a499: $i). % 20.72/7.55 tff(a533, type, a533: $i). % 20.72/7.55 tff(ssSkC16, type, ssSkC16: $o). % 20.72/7.55 tff(a500, type, a500: $i). % 20.72/7.55 tff(a472, type, a472: $i). % 20.72/7.55 tff(a470, type, a470: $i). % 20.72/7.55 tff(a598, type, a598: $i). % 20.72/7.55 tff(ssSkP3, type, ssSkP3: $i > $o). % 20.72/7.55 tff(a516, type, a516: $i). % 20.72/7.55 tff(a524, type, a524: $i). % 20.72/7.55 tff(a563, type, a563: $i). % 20.72/7.55 tff(ssSkC24, type, ssSkC24: $o). % 20.72/7.55 tff(a571, type, a571: $i). % 20.72/7.55 tff(a543, type, a543: $i). % 20.72/7.55 tff(a509, type, a509: $i). % 20.72/7.55 tff(ssSkC17, type, ssSkC17: $o). % 20.72/7.55 tff(a589, type, a589: $i). % 20.72/7.55 tff(a558, type, a558: $i). % 20.72/7.55 tff(c1_0, type, c1_0: $o). % 20.72/7.55 tff(c8_1, type, c8_1: $i > $o). % 20.72/7.55 tff(ssSkP4, type, ssSkP4: $i > $o). % 20.72/7.55 tff(a465, type, a465: $i). % 20.72/7.55 tff(a469, type, a469: $i). % 20.72/7.55 tff(c2_1, type, c2_1: $i > $o). % 20.72/7.55 tff(a549, type, a549: $i). % 20.72/7.55 tff(a555, type, a555: $i). % 20.72/7.55 tff(ndr1_1, type, ndr1_1: $i > $o). % 20.72/7.55 tff(ssSkC15, type, ssSkC15: $o). % 20.72/7.55 tff(c2_0, type, c2_0: $o). % 20.72/7.55 tff(c4_1, type, c4_1: $i > $o). % 20.72/7.55 tff(a529, type, a529: $i). % 20.72/7.55 tff(a475, type, a475: $i). % 20.72/7.55 tff(a557, type, a557: $i). % 20.72/7.55 tff(a575, type, a575: $i). % 20.72/7.55 tff(a597, type, a597: $i). % 20.72/7.55 tff(a591, type, a591: $i). % 20.72/7.55 tff(a494, type, a494: $i). % 20.72/7.55 tff(a545, type, a545: $i). % 20.72/7.55 tff(a491, type, a491: $i). % 20.72/7.55 tff(a562, type, a562: $i). % 20.72/7.55 tff(a463, type, a463: $i). % 20.72/7.55 tff(a474, type, a474: $i). % 20.72/7.55 tff(a581, type, a581: $i). % 20.72/7.55 tff(a568, type, a568: $i). % 20.72/7.55 tff(a593, type, a593: $i). % 20.72/7.55 tff(a479, type, a479: $i). % 20.72/7.55 tff(a489, type, a489: $i). % 20.72/7.55 tff(a584, type, a584: $i). % 20.72/7.55 tff(a482, type, a482: $i). % 20.72/7.55 tff(ssSkC12, type, ssSkC12: $o). % 20.72/7.55 tff(c6_2, type, c6_2: ($i * $i) > $o). % 20.72/7.55 tff(a507, type, a507: $i). % 20.72/7.55 tff(a587, type, a587: $i). % 20.72/7.55 tff(a578, type, a578: $i). % 20.72/7.55 tff(a559, type, a559: $i). % 20.72/7.55 tff(a464, type, a464: $i). % 20.72/7.55 tff(ssSkC20, type, ssSkC20: $o). % 20.72/7.55 tff(a552, type, a552: $i). % 20.72/7.55 tff(a548, type, a548: $i). % 20.72/7.55 tff(a534, type, a534: $i). % 20.72/7.55 tff(a588, type, a588: $i). % 20.72/7.55 tff(a525, type, a525: $i). % 20.72/7.55 tff(a523, type, a523: $i). % 20.72/7.55 tff(a595, type, a595: $i). % 20.72/7.55 tff(a531, type, a531: $i). % 20.72/7.55 tff(a522, type, a522: $i). % 20.72/7.55 tff(a573, type, a573: $i). % 20.72/7.55 tff(ndr1_0, type, ndr1_0: $o). % 20.72/7.55 tff(a480, type, a480: $i). % 20.72/7.55 tff(a485, type, a485: $i). % 20.72/7.55 tff(a476, type, a476: $i). % 20.72/7.55 tff(a483, type, a483: $i). % 20.72/7.55 tff(a538, type, a538: $i). % 20.72/7.55 tff(a501, type, a501: $i). % 20.72/7.55 tff(ssSkC14, type, ssSkC14: $o). % 20.72/7.55 tff(a486, type, a486: $i). % 20.72/7.55 tff(a547, type, a547: $i). % 20.72/7.55 tff(a527, type, a527: $i). % 20.72/7.55 tff(a526, type, a526: $i). % 20.72/7.55 tff(a576, type, a576: $i). % 20.72/7.55 tff(a561, type, a561: $i). % 20.72/7.55 tff(a481, type, a481: $i). % 20.72/7.55 tff(c1_1, type, c1_1: $i > $o). % 20.72/7.55 tff(a497, type, a497: $i). % 20.72/7.55 tff(a521, type, a521: $i). % 20.72/7.55 tff(ssSkC13, type, ssSkC13: $o). % 20.72/7.55 tff(ssSkC25, type, ssSkC25: $o). % 20.72/7.55 tff(ssSkC2, type, ssSkC2: $o). % 20.72/7.55 tff(c5_2, type, c5_2: ($i * $i) > $o). % 20.72/7.55 tff(a496, type, a496: $i). % 20.72/7.55 tff(a540, type, a540: $i). % 20.72/7.55 tff(a519, type, a519: $i). % 20.72/7.55 tff(c7_1, type, c7_1: $i > $o). % 20.72/7.55 tff(c6_1, type, c6_1: $i > $o). % 20.72/7.55 tff(ssSkC22, type, ssSkC22: $o). % 20.72/7.55 tff(a590, type, a590: $i). % 20.72/7.55 tff(c4_2, type, c4_2: ($i * $i) > $o). % 20.72/7.55 tff(a517, type, a517: $i). % 20.72/7.55 tff(a560, type, a560: $i). % 20.72/7.55 tff(a582, type, a582: $i). % 20.72/7.55 tff(ssSkC1, type, ssSkC1: $o). % 20.72/7.55 tff(a566, type, a566: $i). % 20.72/7.55 tff(ssSkP5, type, ssSkP5: $i > $o). % 20.72/7.55 tff(a554, type, a554: $i). % 20.72/7.55 tff(ssSkC0, type, ssSkC0: $o). % 20.72/7.55 tff(a515, type, a515: $i). % 20.72/7.55 tff(ssSkC5, type, ssSkC5: $o). % 20.72/7.55 tff(ssSkP1, type, ssSkP1: $i > $o). % 20.72/7.55 tff(c5_1, type, c5_1: $i > $o). % 20.72/7.55 tff(c7_2, type, c7_2: ($i * $i) > $o). % 20.72/7.55 tff(a583, type, a583: $i). % 20.72/7.55 tff(c3_2, type, c3_2: ($i * $i) > $o). % 20.72/7.55 tff(a514, type, a514: $i). % 20.72/7.55 tff(a466, type, a466: $i). % 20.72/7.55 tff(c2_2, type, c2_2: ($i * $i) > $o). % 20.72/7.55 tff(a513, type, a513: $i). % 20.72/7.55 tff(a512, type, a512: $i). % 20.72/7.55 tff(a574, type, a574: $i). % 20.72/7.55 tff(a592, type, a592: $i). % 20.72/7.55 tff(c3_1, type, c3_1: $i > $o). % 20.72/7.55 tff(a579, type, a579: $i). % 20.72/7.55 % 20.72/7.55 %Saturated clause set: % 20.72/7.55 tff(c_12990, plain, (![U_1042, W_1041, W_1039, V_1038]: (c2_2(U_1042, a548) | c3_2(U_1042, a526) | ~c1_1(U_1042) | ssSkP6(U_1042) | c1_2(U_1042, W_1041) | c3_2(U_1042, W_1041) | ~c2_2(U_1042, W_1041) | c7_1(U_1042) | c4_1(U_1042) | ~c2_2(U_1042, a479) | c1_2(U_1042, W_1039) | ~c8_1(U_1042) | c3_2(U_1042, W_1039) | c3_2(U_1042, V_1038) | c2_2(U_1042, a526) | ~c2_2(U_1042, W_1039) | ~c1_2(U_1042, V_1038) | ~ndr1_1(U_1042) | c5_2(U_1042, V_1038)))). % 20.72/7.55 tff(c_12991, plain, (![U_1042, W_1041, W_1039, V_1038]: (c3_2(U_1042, a526) | ~c1_1(U_1042) | ~c4_2(U_1042, a548) | ssSkP6(U_1042) | c1_2(U_1042, W_1041) | c3_2(U_1042, W_1041) | ~c2_2(U_1042, W_1041) | c7_1(U_1042) | c4_1(U_1042) | ~c2_2(U_1042, a479) | c1_2(U_1042, W_1039) | ~c8_1(U_1042) | c3_2(U_1042, W_1039) | c3_2(U_1042, V_1038) | c2_2(U_1042, a526) | ~c2_2(U_1042, W_1039) | ~c1_2(U_1042, V_1038) | ~ndr1_1(U_1042) | c5_2(U_1042, V_1038)))). % 20.72/7.55 tff(c_13000, plain, (![U_1042, W_1041, W_1039, V_1038]: (~c3_1(U_1042) | c1_2(U_1042, W_1041) | c3_2(U_1042, W_1041) | ~c2_2(U_1042, W_1041) | c7_1(U_1042) | c4_1(U_1042) | ~c2_2(U_1042, a479) | c1_2(U_1042, W_1039) | ~c8_1(U_1042) | c3_2(U_1042, W_1039) | c3_2(U_1042, V_1038) | c2_2(U_1042, a459) | ~c2_2(U_1042, W_1039) | ~c1_2(U_1042, V_1038) | ~ndr1_1(U_1042) | c5_2(U_1042, V_1038)))). % 20.72/7.55 tff(c_11472, plain, (![V_753, U_590, W_591, W_752, X_754]: (c1_2(U_590, W_752) | c3_2(U_590, W_752) | ~c2_2(U_590, W_752) | c7_1(U_590) | c4_1(U_590) | ~c2_2(U_590, a479) | c1_2(U_590, W_591) | ~c8_1(U_590) | c3_2(U_590, W_591) | c3_2(U_590, V_753) | c2_2(U_590, X_754) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_753) | ~ndr1_1(U_590) | c5_2(U_590, V_753) | c6_2(U_590, X_754)))). % 20.72/7.55 tff(c_12648, plain, (![U_1025, W_1026, V_1027]: (c2_2(U_1025, a548) | c3_2(U_1025, a526) | ~c1_1(U_1025) | ssSkP6(U_1025) | c7_1(U_1025) | c4_1(U_1025) | ~c2_2(U_1025, a479) | c1_2(U_1025, W_1026) | ~c8_1(U_1025) | c3_2(U_1025, V_1027) | c2_2(U_1025, a526) | ~c2_2(U_1025, W_1026) | ~c1_2(U_1025, V_1027) | ~ndr1_1(U_1025) | c5_2(U_1025, V_1027) | c3_2(U_1025, W_1026)))). % 20.72/7.55 tff(c_12649, plain, (![U_1025, W_1026, V_1027]: (c3_2(U_1025, a526) | ~c1_1(U_1025) | ~c4_2(U_1025, a548) | ssSkP6(U_1025) | c7_1(U_1025) | c4_1(U_1025) | ~c2_2(U_1025, a479) | c1_2(U_1025, W_1026) | ~c8_1(U_1025) | c3_2(U_1025, V_1027) | c2_2(U_1025, a526) | ~c2_2(U_1025, W_1026) | ~c1_2(U_1025, V_1027) | ~ndr1_1(U_1025) | c5_2(U_1025, V_1027) | c3_2(U_1025, W_1026)))). % 20.72/7.55 tff(c_12658, plain, (![U_1025, W_1026, V_1027]: (~c3_1(U_1025) | c7_1(U_1025) | c4_1(U_1025) | ~c2_2(U_1025, a479) | c1_2(U_1025, W_1026) | ~c8_1(U_1025) | c3_2(U_1025, V_1027) | c2_2(U_1025, a459) | ~c2_2(U_1025, W_1026) | ~c1_2(U_1025, V_1027) | ~ndr1_1(U_1025) | c5_2(U_1025, V_1027) | c3_2(U_1025, W_1026)))). % 20.72/7.56 tff(c_11963, plain, (![U_590, W_752, V_753, X_754]: (c7_1(U_590) | c4_1(U_590) | ~c2_2(U_590, a479) | c1_2(U_590, W_752) | ~c8_1(U_590) | c3_2(U_590, V_753) | c2_2(U_590, X_754) | ~c2_2(U_590, W_752) | ~c1_2(U_590, V_753) | ~ndr1_1(U_590) | c5_2(U_590, V_753) | c3_2(U_590, W_752) | c6_2(U_590, X_754)))). % 20.72/7.56 tff(c_10868, plain, (![U_1000, W_1002, W_999, V_998]: (c1_2(U_1000, W_1002) | c3_2(U_1000, W_1002) | ~c2_2(U_1000, W_1002) | c7_1(U_1000) | c4_1(U_1000) | ~c2_2(U_1000, a479) | ssSkP7(U_1000) | c1_2(U_1000, W_999) | ~c8_1(U_1000) | c3_2(U_1000, W_999) | c3_2(U_1000, V_998) | c2_2(U_1000, a554) | ~c2_2(U_1000, W_999) | ~c1_2(U_1000, V_998) | ~ndr1_1(U_1000) | c5_2(U_1000, V_998)))). % 20.72/7.56 tff(c_10574, plain, (![U_991, W_993, V_994]: (c7_1(U_991) | c4_1(U_991) | ~c2_2(U_991, a479) | ssSkP7(U_991) | c1_2(U_991, W_993) | ~c8_1(U_991) | c3_2(U_991, V_994) | c2_2(U_991, a554) | ~c2_2(U_991, W_993) | ~c1_2(U_991, V_994) | ~ndr1_1(U_991) | c3_2(U_991, W_993) | c5_2(U_991, V_994)))). % 20.72/7.56 tff(c_9476, plain, (![U_966, W_968, W_964, V_965]: (c1_2(U_966, W_968) | c3_2(U_966, W_968) | ~c2_2(U_966, W_968) | c7_1(U_966) | c4_1(U_966) | ~c2_2(U_966, a479) | ssSkP2(U_966) | c1_2(U_966, W_964) | ~c8_1(U_966) | c3_2(U_966, W_964) | c3_2(U_966, V_965) | c2_2(U_966, a492) | ~c2_2(U_966, W_964) | ~c1_2(U_966, V_965) | ~ndr1_1(U_966) | c5_2(U_966, V_965)))). % 20.72/7.56 tff(c_10003, plain, (![U_975, W_977, V_978]: (c7_1(U_975) | c4_1(U_975) | ~c2_2(U_975, a479) | ssSkP2(U_975) | c1_2(U_975, W_977) | ~c8_1(U_975) | c3_2(U_975, V_978) | c2_2(U_975, a492) | ~c2_2(U_975, W_977) | ~c1_2(U_975, V_978) | ~ndr1_1(U_975) | c5_2(U_975, V_978) | c3_2(U_975, W_977)))). % 20.72/7.56 tff(c_5367, plain, (![U_248, X_810, V_811]: (c3_2(U_248, a481) | ~c6_2(U_248, a481) | ~c1_1(U_248) | c8_1(U_248) | c4_2(U_248, X_810) | ~c3_2(U_248, X_810) | c3_2(U_248, a456) | c3_2(U_248, V_811) | c5_2(U_248, V_811) | c2_2(U_248, X_810) | ~c2_2(U_248, a456) | ~c1_2(U_248, V_811) | ssSkP0(U_248) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.72/7.56 tff(c_5351, plain, (![U_248, X_807, V_808]: (c3_2(U_248, a481) | ~c1_1(U_248) | ~c6_2(U_248, a481) | c8_1(U_248) | c4_2(U_248, X_807) | ~c3_2(U_248, X_807) | ssSkP3(U_248) | c3_2(U_248, a502) | c3_2(U_248, V_808) | c5_2(U_248, V_808) | c2_2(U_248, X_807) | ~c2_2(U_248, a502) | ~c1_2(U_248, V_808) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.72/7.56 tff(c_7809, plain, (![U_896, V_148, W_897]: (c5_2(U_896, V_148) | c2_2(U_896, V_148) | ~c4_1(U_896) | c3_2(U_896, a526) | ssSkP6(U_896) | c2_2(U_896, a548) | ~c1_1(U_896) | c3_2(U_896, a479) | ~c2_2(U_896, a479) | c1_2(U_896, W_897) | ~c8_1(U_896) | c3_2(U_896, W_897) | c3_2(U_896, a572) | c2_2(U_896, a526) | ~c2_2(U_896, W_897) | ~c1_2(U_896, a572) | ~ndr1_1(U_896)))). % 20.72/7.56 tff(c_8595, plain, (![U_923, V_148, W_924]: (c5_2(U_923, V_148) | c2_2(U_923, V_148) | ~c4_1(U_923) | c3_2(U_923, a526) | ssSkP6(U_923) | ~c1_1(U_923) | ~c4_2(U_923, a548) | c3_2(U_923, a479) | ~c2_2(U_923, a479) | c1_2(U_923, W_924) | ~c8_1(U_923) | c3_2(U_923, W_924) | c3_2(U_923, a572) | c2_2(U_923, a526) | ~c2_2(U_923, W_924) | ~c1_2(U_923, a572) | ~ndr1_1(U_923)))). % 20.72/7.56 tff(c_8777, plain, (![U_16, X_941, V_942]: (~c1_1(U_16) | c8_1(U_16) | c2_2(U_16, a481) | c4_2(U_16, X_941) | ~c3_2(U_16, X_941) | c3_2(U_16, a456) | c3_2(U_16, V_942) | c5_2(U_16, V_942) | c2_2(U_16, X_941) | ~c2_2(U_16, a456) | ~c1_2(U_16, V_942) | c7_1(U_16) | c4_1(U_16) | ~ndr1_1(U_16) | ~c6_2(U_16, a548) | ~c2_2(U_16, a548) | ssSkP0(U_16)))). % 20.72/7.56 tff(c_5082, plain, (![U_248, W_774, X_775, V_776]: (~c1_1(U_248) | ~c6_2(U_248, W_774) | c8_1(U_248) | c2_2(U_248, a481) | c4_2(U_248, X_775) | ~c3_2(U_248, X_775) | c3_2(U_248, W_774) | c3_2(U_248, V_776) | c5_2(U_248, V_776) | c2_2(U_248, X_775) | ~c2_2(U_248, W_774) | ~c1_2(U_248, V_776) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.72/7.56 tff(c_8695, plain, (![U_16, X_934, V_935]: (~c1_1(U_16) | c8_1(U_16) | c4_2(U_16, X_934) | ~c3_1(U_16) | ~c3_2(U_16, X_934) | c3_2(U_16, a456) | c3_2(U_16, V_935) | c5_2(U_16, V_935) | c2_2(U_16, X_934) | ~c2_2(U_16, a456) | ~c1_2(U_16, V_935) | c7_1(U_16) | c4_1(U_16) | ~ndr1_1(U_16) | ~c6_2(U_16, a548) | ~c2_2(U_16, a548) | ssSkP0(U_16)))). % 20.72/7.56 tff(c_4257, plain, (![U_248, W_709, X_710, V_711]: (~c1_1(U_248) | ~c6_2(U_248, W_709) | c8_1(U_248) | c4_2(U_248, X_710) | ~c3_1(U_248) | ~c3_2(U_248, X_710) | c3_2(U_248, W_709) | c3_2(U_248, V_711) | c5_2(U_248, V_711) | c2_2(U_248, X_710) | ~c2_2(U_248, W_709) | ~c1_2(U_248, V_711) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.72/7.56 tff(c_8570, plain, (![U_920, V_148, W_921]: (c5_2(U_920, V_148) | c2_2(U_920, V_148) | ~c4_1(U_920) | ~c3_1(U_920) | ~c1_1(U_920) | ~c4_2(U_920, a548) | c3_2(U_920, a479) | ~c2_2(U_920, a479) | c1_2(U_920, W_921) | ~c8_1(U_920) | c3_2(U_920, W_921) | c3_2(U_920, a572) | c2_2(U_920, a459) | ~c2_2(U_920, W_921) | ~c1_2(U_920, a572) | ~ndr1_1(U_920)))). % 20.72/7.56 tff(c_8546, plain, (![U_917, V_148, W_918]: (c5_2(U_917, V_148) | c2_2(U_917, V_148) | ~c4_1(U_917) | ssSkP2(U_917) | ~c1_1(U_917) | ~c4_2(U_917, a548) | c3_2(U_917, a479) | ~c2_2(U_917, a479) | c1_2(U_917, W_918) | ~c8_1(U_917) | c3_2(U_917, W_918) | c3_2(U_917, a572) | c2_2(U_917, a492) | ~c2_2(U_917, W_918) | ~c1_2(U_917, a572) | ~ndr1_1(U_917)))). % 20.72/7.56 tff(c_8512, plain, (![U_913, W_914, V_915]: (c3_2(U_913, a526) | ssSkP6(U_913) | ~c1_1(U_913) | ~c4_2(U_913, a548) | c3_2(U_913, a479) | ~c2_2(U_913, a479) | c1_2(U_913, W_914) | ~c8_1(U_913) | c3_2(U_913, W_914) | c3_2(U_913, V_915) | c2_2(U_913, a526) | ~c2_2(U_913, W_914) | ~c1_2(U_913, V_915) | ~ndr1_1(U_913) | c5_2(U_913, V_915)))). % 20.72/7.56 tff(c_8520, plain, (![U_913, W_914, V_915]: (~c3_1(U_913) | ~c1_1(U_913) | ~c4_2(U_913, a548) | c3_2(U_913, a479) | ~c2_2(U_913, a479) | c1_2(U_913, W_914) | ~c8_1(U_913) | c3_2(U_913, W_914) | c3_2(U_913, V_915) | c2_2(U_913, a459) | ~c2_2(U_913, W_914) | ~c1_2(U_913, V_915) | ~ndr1_1(U_913) | c5_2(U_913, V_915)))). % 20.72/7.56 tff(c_8522, plain, (![U_913, W_914, V_915]: (ssSkP2(U_913) | ~c1_1(U_913) | ~c4_2(U_913, a548) | c3_2(U_913, a479) | ~c2_2(U_913, a479) | c1_2(U_913, W_914) | ~c8_1(U_913) | c3_2(U_913, W_914) | c3_2(U_913, V_915) | c2_2(U_913, a492) | ~c2_2(U_913, W_914) | ~c1_2(U_913, V_915) | ~ndr1_1(U_913) | c5_2(U_913, V_915)))). % 20.72/7.56 tff(c_7896, plain, (![U_628, W_629, V_630, X_593]: (~c1_1(U_628) | ~c4_2(U_628, a548) | c3_2(U_628, a479) | ~c2_2(U_628, a479) | c1_2(U_628, W_629) | ~c8_1(U_628) | c3_2(U_628, W_629) | c3_2(U_628, V_630) | c2_2(U_628, X_593) | ~c2_2(U_628, W_629) | ~c1_2(U_628, V_630) | ~ndr1_1(U_628) | c5_2(U_628, V_630) | c6_2(U_628, X_593)))). % 20.72/7.56 tff(c_7784, plain, (![U_893, V_148, W_894]: (c5_2(U_893, V_148) | c2_2(U_893, V_148) | ~c4_1(U_893) | ~c3_1(U_893) | c2_2(U_893, a548) | ~c1_1(U_893) | c3_2(U_893, a479) | ~c2_2(U_893, a479) | c1_2(U_893, W_894) | ~c8_1(U_893) | c3_2(U_893, W_894) | c3_2(U_893, a572) | c2_2(U_893, a459) | ~c2_2(U_893, W_894) | ~c1_2(U_893, a572) | ~ndr1_1(U_893)))). % 20.72/7.56 tff(c_7736, plain, (![U_887, V_148, W_888]: (c5_2(U_887, V_148) | c2_2(U_887, V_148) | ~c4_1(U_887) | ssSkP7(U_887) | c2_2(U_887, a548) | ~c1_1(U_887) | c3_2(U_887, a479) | ~c2_2(U_887, a479) | c1_2(U_887, W_888) | ~c8_1(U_887) | c3_2(U_887, W_888) | c3_2(U_887, a572) | c2_2(U_887, a554) | ~c2_2(U_887, W_888) | ~c1_2(U_887, a572) | ~ndr1_1(U_887)))). % 20.72/7.56 tff(c_7760, plain, (![U_890, V_148, W_891]: (c5_2(U_890, V_148) | c2_2(U_890, V_148) | ~c4_1(U_890) | ssSkP2(U_890) | c2_2(U_890, a548) | ~c1_1(U_890) | c3_2(U_890, a479) | ~c2_2(U_890, a479) | c1_2(U_890, W_891) | ~c8_1(U_890) | c3_2(U_890, W_891) | c3_2(U_890, a572) | c2_2(U_890, a492) | ~c2_2(U_890, W_891) | ~c1_2(U_890, a572) | ~ndr1_1(U_890)))). % 20.72/7.56 tff(c_7701, plain, (![U_883, W_884, V_885]: (c3_2(U_883, a526) | ssSkP6(U_883) | c2_2(U_883, a548) | ~c1_1(U_883) | c3_2(U_883, a479) | ~c2_2(U_883, a479) | c1_2(U_883, W_884) | ~c8_1(U_883) | c3_2(U_883, W_884) | c3_2(U_883, V_885) | c2_2(U_883, a526) | ~c2_2(U_883, W_884) | ~c1_2(U_883, V_885) | ~ndr1_1(U_883) | c5_2(U_883, V_885)))). % 20.72/7.56 tff(c_7710, plain, (![U_883, W_884, V_885]: (~c3_1(U_883) | c2_2(U_883, a548) | ~c1_1(U_883) | c3_2(U_883, a479) | ~c2_2(U_883, a479) | c1_2(U_883, W_884) | ~c8_1(U_883) | c3_2(U_883, W_884) | c3_2(U_883, V_885) | c2_2(U_883, a459) | ~c2_2(U_883, W_884) | ~c1_2(U_883, V_885) | ~ndr1_1(U_883) | c5_2(U_883, V_885)))). % 20.72/7.56 tff(c_7712, plain, (![U_883, W_884, V_885]: (ssSkP2(U_883) | c2_2(U_883, a548) | ~c1_1(U_883) | c3_2(U_883, a479) | ~c2_2(U_883, a479) | c1_2(U_883, W_884) | ~c8_1(U_883) | c3_2(U_883, W_884) | c3_2(U_883, V_885) | c2_2(U_883, a492) | ~c2_2(U_883, W_884) | ~c1_2(U_883, V_885) | ~ndr1_1(U_883) | c5_2(U_883, V_885)))). % 20.72/7.56 tff(c_7711, plain, (![U_883, W_884, V_885]: (ssSkP7(U_883) | c2_2(U_883, a548) | ~c1_1(U_883) | c3_2(U_883, a479) | ~c2_2(U_883, a479) | c1_2(U_883, W_884) | ~c8_1(U_883) | c3_2(U_883, W_884) | c3_2(U_883, V_885) | c2_2(U_883, a554) | ~c2_2(U_883, W_884) | ~c1_2(U_883, V_885) | ~ndr1_1(U_883) | c5_2(U_883, V_885)))). % 20.72/7.56 tff(c_7086, plain, (![U_628, W_629, V_630, X_593]: (c2_2(U_628, a548) | ~c1_1(U_628) | c3_2(U_628, a479) | ~c2_2(U_628, a479) | c1_2(U_628, W_629) | ~c8_1(U_628) | c3_2(U_628, W_629) | c3_2(U_628, V_630) | c2_2(U_628, X_593) | ~c2_2(U_628, W_629) | ~c1_2(U_628, V_630) | ~ndr1_1(U_628) | c5_2(U_628, V_630) | c6_2(U_628, X_593)))). % 20.72/7.56 tff(c_5219, plain, (![U_788, V_148]: (c5_2(U_788, V_148) | c2_2(U_788, V_148) | ~c4_1(U_788) | c3_2(U_788, a515) | ~c1_1(U_788) | ~c4_2(U_788, a548) | c8_1(U_788) | ~c2_1(U_788) | ~c4_2(U_788, a515) | ssSkP5(U_788) | ssSkP3(U_788) | c3_2(U_788, a502) | c3_2(U_788, a572) | c2_2(U_788, a515) | ~c2_2(U_788, a502) | ~c1_2(U_788, a572) | ~ndr1_1(U_788)))). % 20.72/7.56 tff(c_5224, plain, (![U_790, V_148]: (c5_2(U_790, V_148) | c2_2(U_790, V_148) | ~c4_1(U_790) | c2_2(U_790, a548) | c3_2(U_790, a515) | ~c1_1(U_790) | c8_1(U_790) | ~c2_1(U_790) | ~c4_2(U_790, a515) | ssSkP5(U_790) | ssSkP3(U_790) | c3_2(U_790, a502) | c3_2(U_790, a572) | c2_2(U_790, a515) | ~c2_2(U_790, a502) | ~c1_2(U_790, a572) | ~ndr1_1(U_790)))). % 20.72/7.56 tff(c_6596, plain, (![U_862, V_148, W_863]: (c5_2(U_862, V_148) | c2_2(U_862, V_148) | ~c4_1(U_862) | ssSkP7(U_862) | ~c1_1(U_862) | ~c4_2(U_862, a548) | c3_2(U_862, a479) | ~c2_2(U_862, a479) | c1_2(U_862, W_863) | ~c8_1(U_862) | c3_2(U_862, W_863) | c3_2(U_862, a572) | c2_2(U_862, a554) | ~c2_2(U_862, W_863) | ~c1_2(U_862, a572) | ~ndr1_1(U_862)))). % 20.72/7.56 tff(c_6571, plain, (![U_858, W_859, V_860]: (ssSkP7(U_858) | ~c1_1(U_858) | ~c4_2(U_858, a548) | c3_2(U_858, a479) | ~c2_2(U_858, a479) | c1_2(U_858, W_859) | ~c8_1(U_858) | c3_2(U_858, W_859) | c3_2(U_858, V_860) | c2_2(U_858, a554) | ~c2_2(U_858, W_859) | ~c1_2(U_858, V_860) | ~ndr1_1(U_858) | c5_2(U_858, V_860)))). % 20.72/7.56 tff(c_4001, plain, (![U_248, X_682, V_683]: (~c1_1(U_248) | ~c6_2(U_248, a481) | c8_1(U_248) | c4_2(U_248, X_682) | ~c3_2(U_248, X_682) | c3_2(U_248, a481) | c3_2(U_248, V_683) | c5_2(U_248, V_683) | c2_2(U_248, X_682) | ~c2_2(U_248, a481) | ~c1_2(U_248, V_683) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.72/7.56 tff(c_4245, plain, (![U_706, V_148]: (c5_2(U_706, V_148) | c2_2(U_706, V_148) | ~c4_1(U_706) | ~c3_1(U_706) | ~c1_1(U_706) | ~c4_2(U_706, a548) | c3_2(U_706, a479) | c3_2(U_706, a572) | c2_2(U_706, a459) | ~c2_2(U_706, a479) | ~c1_2(U_706, a572) | c1_2(U_706, a526) | c3_2(U_706, a526) | ~c8_1(U_706) | ~ndr1_1(U_706) | ssSkP6(U_706)))). % 20.72/7.57 tff(c_4664, plain, (![U_734, V_148]: (c5_2(U_734, V_148) | c2_2(U_734, V_148) | ~c4_1(U_734) | ~c3_1(U_734) | c2_2(U_734, a548) | ~c1_1(U_734) | c3_2(U_734, a479) | c3_2(U_734, a572) | c2_2(U_734, a459) | ~c2_2(U_734, a479) | ~c1_2(U_734, a572) | c1_2(U_734, a526) | c3_2(U_734, a526) | ~c8_1(U_734) | ~ndr1_1(U_734) | ssSkP6(U_734)))). % 20.72/7.57 tff(c_4654, plain, (![U_730, V_148]: (c5_2(U_730, V_148) | c2_2(U_730, V_148) | ~c4_1(U_730) | ssSkP7(U_730) | c2_2(U_730, a548) | ~c1_1(U_730) | c3_2(U_730, a479) | c3_2(U_730, a572) | c2_2(U_730, a554) | ~c2_2(U_730, a479) | ~c1_2(U_730, a572) | c1_2(U_730, a526) | c3_2(U_730, a526) | ~c8_1(U_730) | ~ndr1_1(U_730) | ssSkP6(U_730)))). % 20.72/7.57 tff(c_4659, plain, (![U_732, V_148]: (c5_2(U_732, V_148) | c2_2(U_732, V_148) | ~c4_1(U_732) | ssSkP2(U_732) | c2_2(U_732, a548) | ~c1_1(U_732) | c3_2(U_732, a479) | c3_2(U_732, a572) | c2_2(U_732, a492) | ~c2_2(U_732, a479) | ~c1_2(U_732, a572) | c1_2(U_732, a526) | c3_2(U_732, a526) | ~c8_1(U_732) | ~ndr1_1(U_732) | ssSkP6(U_732)))). % 20.72/7.57 tff(c_4240, plain, (![U_704, V_148]: (c5_2(U_704, V_148) | c2_2(U_704, V_148) | ~c4_1(U_704) | ssSkP2(U_704) | ~c1_1(U_704) | ~c4_2(U_704, a548) | c3_2(U_704, a479) | c3_2(U_704, a572) | c2_2(U_704, a492) | ~c2_2(U_704, a479) | ~c1_2(U_704, a572) | c1_2(U_704, a526) | c3_2(U_704, a526) | ~c8_1(U_704) | ~ndr1_1(U_704) | ssSkP6(U_704)))). % 20.72/7.57 tff(c_4235, plain, (![U_702, V_148]: (c5_2(U_702, V_148) | c2_2(U_702, V_148) | ~c4_1(U_702) | ssSkP7(U_702) | ~c1_1(U_702) | ~c4_2(U_702, a548) | c3_2(U_702, a479) | c3_2(U_702, a572) | c2_2(U_702, a554) | ~c2_2(U_702, a479) | ~c1_2(U_702, a572) | c1_2(U_702, a526) | c3_2(U_702, a526) | ~c8_1(U_702) | ~ndr1_1(U_702) | ssSkP6(U_702)))). % 20.72/7.57 tff(c_5481, plain, (![U_816, W_818, X_817, V_819]: (~c6_2(U_816, W_818) | c3_2(U_816, a481) | ~c1_1(U_816) | ~c7_2(U_816, a548) | ~c6_2(U_816, a481) | c8_1(U_816) | c4_2(U_816, X_817) | ~c3_2(U_816, X_817) | c3_2(U_816, W_818) | c3_2(U_816, V_819) | c5_2(U_816, V_819) | c2_2(U_816, X_817) | ~c2_2(U_816, W_818) | ~c1_2(U_816, V_819) | ~ndr1_1(U_816)))). % 20.72/7.57 tff(c_5330, plain, (![U_802, W_804, X_803, V_805]: (~c6_2(U_802, W_804) | c2_2(U_802, a548) | c3_2(U_802, a481) | ~c1_1(U_802) | ~c6_2(U_802, a481) | c8_1(U_802) | c4_2(U_802, X_803) | ~c3_2(U_802, X_803) | c3_2(U_802, W_804) | c3_2(U_802, V_805) | c5_2(U_802, V_805) | c2_2(U_802, X_803) | ~c2_2(U_802, W_804) | ~c1_2(U_802, V_805) | ~ndr1_1(U_802)))). % 20.72/7.57 tff(c_5424, plain, (![U_812, W_814, X_813, V_815]: (~c6_2(U_812, W_814) | c3_2(U_812, a481) | ~c1_1(U_812) | ~c4_2(U_812, a548) | ~c6_2(U_812, a481) | c8_1(U_812) | c4_2(U_812, X_813) | ~c3_2(U_812, X_813) | c3_2(U_812, W_814) | c3_2(U_812, V_815) | c5_2(U_812, V_815) | c2_2(U_812, X_813) | ~c2_2(U_812, W_814) | ~c1_2(U_812, V_815) | ~ndr1_1(U_812)))). % 20.72/7.57 tff(c_3932, plain, (![U_674, X_675, W_676, V_677]: (c3_2(U_674, a481) | ~c1_1(U_674) | ~c7_2(U_674, a548) | ~c6_2(U_674, a481) | c8_1(U_674) | c4_2(U_674, X_675) | ~c3_2(U_674, X_675) | c8_2(U_674, W_676) | c3_2(U_674, W_676) | c3_2(U_674, V_677) | c5_2(U_674, V_677) | c2_2(U_674, X_675) | ~c2_2(U_674, W_676) | ~c1_2(U_674, V_677) | ~ndr1_1(U_674)))). % 20.72/7.57 tff(c_3936, plain, (![U_674, X_675, W_676, V_677]: (c3_2(U_674, a481) | ~c1_1(U_674) | ~c4_2(U_674, a548) | ~c6_2(U_674, a481) | c8_1(U_674) | c4_2(U_674, X_675) | ~c3_2(U_674, X_675) | c8_2(U_674, W_676) | c3_2(U_674, W_676) | c3_2(U_674, V_677) | c5_2(U_674, V_677) | c2_2(U_674, X_675) | ~c2_2(U_674, W_676) | ~c1_2(U_674, V_677) | ~ndr1_1(U_674)))). % 20.72/7.57 tff(c_5164, plain, (![U_781, X_782, V_783]: (c3_2(U_781, a481) | ~c6_2(U_781, a481) | ~c1_1(U_781) | ~c7_2(U_781, a548) | c8_1(U_781) | c4_2(U_781, X_782) | ~c3_2(U_781, X_782) | c3_2(U_781, a456) | c3_2(U_781, V_783) | c5_2(U_781, V_783) | c2_2(U_781, X_782) | ~c2_2(U_781, a456) | ~c1_2(U_781, V_783) | ~ndr1_1(U_781) | ssSkP0(U_781)))). % 20.72/7.57 tff(c_3816, plain, (![U_665, X_666, V_667]: (c3_2(U_665, a481) | ~c1_1(U_665) | ~c7_2(U_665, a548) | ~c6_2(U_665, a481) | c8_1(U_665) | c4_2(U_665, X_666) | ~c3_2(U_665, X_666) | ssSkP3(U_665) | c3_2(U_665, a502) | c3_2(U_665, V_667) | c5_2(U_665, V_667) | c2_2(U_665, X_666) | ~c2_2(U_665, a502) | ~c1_2(U_665, V_667) | ~ndr1_1(U_665)))). % 20.72/7.57 tff(c_3935, plain, (![U_674, X_675, W_676, V_677]: (c2_2(U_674, a548) | c3_2(U_674, a481) | ~c1_1(U_674) | ~c6_2(U_674, a481) | c8_1(U_674) | c4_2(U_674, X_675) | ~c3_2(U_674, X_675) | c8_2(U_674, W_676) | c3_2(U_674, W_676) | c3_2(U_674, V_677) | c5_2(U_674, V_677) | c2_2(U_674, X_675) | ~c2_2(U_674, W_676) | ~c1_2(U_674, V_677) | ~ndr1_1(U_674)))). % 20.72/7.57 tff(c_3819, plain, (![U_665, X_666, V_667]: (c2_2(U_665, a548) | c3_2(U_665, a481) | ~c1_1(U_665) | ~c6_2(U_665, a481) | c8_1(U_665) | c4_2(U_665, X_666) | ~c3_2(U_665, X_666) | ssSkP3(U_665) | c3_2(U_665, a502) | c3_2(U_665, V_667) | c5_2(U_665, V_667) | c2_2(U_665, X_666) | ~c2_2(U_665, a502) | ~c1_2(U_665, V_667) | ~ndr1_1(U_665)))). % 20.72/7.57 tff(c_3820, plain, (![U_665, X_666, V_667]: (c3_2(U_665, a481) | ~c1_1(U_665) | ~c4_2(U_665, a548) | ~c6_2(U_665, a481) | c8_1(U_665) | c4_2(U_665, X_666) | ~c3_2(U_665, X_666) | ssSkP3(U_665) | c3_2(U_665, a502) | c3_2(U_665, V_667) | c5_2(U_665, V_667) | c2_2(U_665, X_666) | ~c2_2(U_665, a502) | ~c1_2(U_665, V_667) | ~ndr1_1(U_665)))). % 20.72/7.57 tff(c_4649, plain, (![U_728, V_148]: (c5_2(U_728, V_148) | c2_2(U_728, V_148) | ~c4_1(U_728) | c2_2(U_728, a548) | ~c1_1(U_728) | c3_2(U_728, a479) | c3_2(U_728, a572) | c2_2(U_728, a526) | ~c2_2(U_728, a479) | ~c1_2(U_728, a572) | c1_2(U_728, a526) | c3_2(U_728, a526) | ~c8_1(U_728) | ~ndr1_1(U_728) | ssSkP6(U_728)))). % 20.72/7.57 tff(c_4230, plain, (![U_700, V_148]: (c5_2(U_700, V_148) | c2_2(U_700, V_148) | ~c4_1(U_700) | ~c1_1(U_700) | ~c4_2(U_700, a548) | c3_2(U_700, a479) | c3_2(U_700, a572) | c2_2(U_700, a526) | ~c2_2(U_700, a479) | ~c1_2(U_700, a572) | c1_2(U_700, a526) | c3_2(U_700, a526) | ~c8_1(U_700) | ~ndr1_1(U_700) | ssSkP6(U_700)))). % 20.72/7.57 tff(c_3026, plain, (![U_594, V_595]: (c2_2(U_594, a548) | c3_2(U_594, a515) | ~c1_1(U_594) | c8_1(U_594) | ~c2_1(U_594) | ~c4_2(U_594, a515) | ssSkP5(U_594) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, a515) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.72/7.57 tff(c_3027, plain, (![U_594, V_595]: (c3_2(U_594, a515) | ~c1_1(U_594) | ~c4_2(U_594, a548) | c8_1(U_594) | ~c2_1(U_594) | ~c4_2(U_594, a515) | ssSkP5(U_594) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, a515) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.72/7.57 tff(c_3776, plain, (![U_661, W_663, X_662, V_664]: (~c1_1(U_661) | ~c4_2(U_661, a548) | ~c6_2(U_661, W_663) | c8_1(U_661) | c2_2(U_661, a481) | c4_2(U_661, X_662) | ~c3_2(U_661, X_662) | c3_2(U_661, W_663) | c3_2(U_661, V_664) | c5_2(U_661, V_664) | c2_2(U_661, X_662) | ~c2_2(U_661, W_663) | ~c1_2(U_661, V_664) | ~ndr1_1(U_661)))). % 20.72/7.57 tff(c_5132, plain, (![U_16, X_779, V_780]: (~c1_1(U_16) | ~c7_2(U_16, a548) | c8_1(U_16) | c8_2(U_16, a481) | c4_2(U_16, X_779) | ~c3_2(U_16, X_779) | c3_2(U_16, a456) | c3_2(U_16, V_780) | c5_2(U_16, V_780) | c2_2(U_16, X_779) | ~c2_2(U_16, a456) | ~c1_2(U_16, V_780) | ~ndr1_1(U_16) | ssSkP0(U_16)))). % 20.72/7.57 tff(c_3941, plain, (![U_674, W_676, X_675, V_677]: (~c1_1(U_674) | ~c7_2(U_674, a548) | ~c6_2(U_674, W_676) | c8_1(U_674) | c8_2(U_674, a481) | c4_2(U_674, X_675) | ~c3_2(U_674, X_675) | c3_2(U_674, W_676) | c3_2(U_674, V_677) | c5_2(U_674, V_677) | c2_2(U_674, X_675) | ~c2_2(U_674, W_676) | ~c1_2(U_674, V_677) | ~ndr1_1(U_674)))). % 20.72/7.57 tff(c_3772, plain, (![U_661, W_663, X_662, V_664]: (~c1_1(U_661) | ~c7_2(U_661, a548) | ~c6_2(U_661, W_663) | c8_1(U_661) | c2_2(U_661, a481) | c4_2(U_661, X_662) | ~c3_2(U_661, X_662) | c3_2(U_661, W_663) | c3_2(U_661, V_664) | c5_2(U_661, V_664) | c2_2(U_661, X_662) | ~c2_2(U_661, W_663) | ~c1_2(U_661, V_664) | ~ndr1_1(U_661)))). % 20.72/7.57 tff(c_3775, plain, (![U_661, W_663, X_662, V_664]: (c2_2(U_661, a548) | ~c1_1(U_661) | ~c6_2(U_661, W_663) | c8_1(U_661) | c2_2(U_661, a481) | c4_2(U_661, X_662) | ~c3_2(U_661, X_662) | c3_2(U_661, W_663) | c3_2(U_661, V_664) | c5_2(U_661, V_664) | c2_2(U_661, X_662) | ~c2_2(U_661, W_663) | ~c1_2(U_661, V_664) | ~ndr1_1(U_661)))). % 20.72/7.57 tff(c_3945, plain, (![U_674, W_676, X_675, V_677]: (~c1_1(U_674) | ~c4_2(U_674, a548) | ~c6_2(U_674, W_676) | c8_1(U_674) | c8_2(U_674, a481) | c4_2(U_674, X_675) | ~c3_2(U_674, X_675) | c3_2(U_674, W_676) | c3_2(U_674, V_677) | c5_2(U_674, V_677) | c2_2(U_674, X_675) | ~c2_2(U_674, W_676) | ~c1_2(U_674, V_677) | ~ndr1_1(U_674)))). % 20.72/7.57 tff(c_3944, plain, (![U_674, W_676, X_675, V_677]: (c2_2(U_674, a548) | ~c1_1(U_674) | ~c6_2(U_674, W_676) | c8_1(U_674) | c8_2(U_674, a481) | c4_2(U_674, X_675) | ~c3_2(U_674, X_675) | c3_2(U_674, W_676) | c3_2(U_674, V_677) | c5_2(U_674, V_677) | c2_2(U_674, X_675) | ~c2_2(U_674, W_676) | ~c1_2(U_674, V_677) | ~ndr1_1(U_674)))). % 20.87/7.57 tff(c_3839, plain, (![U_668, V_148, X_669]: (c5_2(U_668, V_148) | c2_2(U_668, V_148) | ~c4_1(U_668) | c8_1(U_668) | c2_2(U_668, a481) | c4_2(U_668, X_669) | ~c3_2(U_668, X_669) | ssSkP3(U_668) | c3_2(U_668, a502) | c3_2(U_668, a572) | c2_2(U_668, X_669) | ~c2_2(U_668, a502) | ~c1_2(U_668, a572) | ~ndr1_1(U_668)))). % 20.87/7.57 tff(c_3378, plain, (![U_628, W_629, V_630]: (c2_2(U_628, a548) | c3_2(U_628, a526) | ~c1_1(U_628) | ssSkP6(U_628) | c6_2(U_628, a479) | c1_2(U_628, W_629) | ~c8_1(U_628) | c3_2(U_628, W_629) | c3_2(U_628, V_630) | c5_2(U_628, V_630) | c2_2(U_628, a526) | ~c2_2(U_628, W_629) | ~c1_2(U_628, V_630) | ~ndr1_1(U_628)))). % 20.87/7.57 tff(c_3195, plain, (![U_248, W_625, V_626, X_627]: (c1_2(U_248, W_625) | ~c8_1(U_248) | c3_2(U_248, W_625) | c3_2(U_248, V_626) | c5_2(U_248, V_626) | c2_2(U_248, X_627) | c6_2(U_248, X_627) | ~c2_2(U_248, W_625) | ~c1_2(U_248, V_626) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a479) | ~c2_2(U_248, a479)))). % 20.87/7.57 tff(c_4793, plain, (![U_16, V_746, X_747]: (~c1_1(U_16) | c3_2(U_16, a456) | c3_2(U_16, V_746) | c5_2(U_16, V_746) | c2_2(U_16, X_747) | c6_2(U_16, X_747) | ~c2_2(U_16, a456) | ~c1_2(U_16, V_746) | c7_1(U_16) | c4_1(U_16) | ~ndr1_1(U_16) | ~c6_2(U_16, a548) | ~c2_2(U_16, a548) | ssSkP0(U_16)))). % 20.87/7.57 tff(c_3168, plain, (![U_248, W_617, V_618, X_619]: (~c1_1(U_248) | ~c6_2(U_248, W_617) | c3_2(U_248, W_617) | c3_2(U_248, V_618) | c5_2(U_248, V_618) | c2_2(U_248, X_619) | c6_2(U_248, X_619) | ~c2_2(U_248, W_617) | ~c1_2(U_248, V_618) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.87/7.57 tff(c_3545, plain, (![U_639, W_641, X_640, V_642]: (c2_2(U_639, a548) | ~c1_1(U_639) | ~c6_2(U_639, W_641) | c8_1(U_639) | c4_2(U_639, X_640) | ~c3_1(U_639) | ~c3_2(U_639, X_640) | c3_2(U_639, W_641) | c3_2(U_639, V_642) | c5_2(U_639, V_642) | c2_2(U_639, X_640) | ~c2_2(U_639, W_641) | ~c1_2(U_639, V_642) | ~ndr1_1(U_639)))). % 20.87/7.57 tff(c_3546, plain, (![U_639, W_641, X_640, V_642]: (~c1_1(U_639) | ~c4_2(U_639, a548) | ~c6_2(U_639, W_641) | c8_1(U_639) | c4_2(U_639, X_640) | ~c3_1(U_639) | ~c3_2(U_639, X_640) | c3_2(U_639, W_641) | c3_2(U_639, V_642) | c5_2(U_639, V_642) | c2_2(U_639, X_640) | ~c2_2(U_639, W_641) | ~c1_2(U_639, V_642) | ~ndr1_1(U_639)))). % 20.87/7.57 tff(c_4642, plain, (![U_725, V_726]: (~c3_1(U_725) | c2_2(U_725, a548) | ~c1_1(U_725) | c3_2(U_725, a479) | c3_2(U_725, V_726) | c5_2(U_725, V_726) | c2_2(U_725, a459) | ~c2_2(U_725, a479) | ~c1_2(U_725, V_726) | c1_2(U_725, a526) | c3_2(U_725, a526) | ~c8_1(U_725) | ~ndr1_1(U_725) | ssSkP6(U_725)))). % 20.87/7.57 tff(c_4644, plain, (![U_725, V_726]: (ssSkP2(U_725) | c2_2(U_725, a548) | ~c1_1(U_725) | c3_2(U_725, a479) | c3_2(U_725, V_726) | c5_2(U_725, V_726) | c2_2(U_725, a492) | ~c2_2(U_725, a479) | ~c1_2(U_725, V_726) | c1_2(U_725, a526) | c3_2(U_725, a526) | ~c8_1(U_725) | ~ndr1_1(U_725) | ssSkP6(U_725)))). % 20.87/7.57 tff(c_4643, plain, (![U_725, V_726]: (ssSkP7(U_725) | c2_2(U_725, a548) | ~c1_1(U_725) | c3_2(U_725, a479) | c3_2(U_725, V_726) | c5_2(U_725, V_726) | c2_2(U_725, a554) | ~c2_2(U_725, a479) | ~c1_2(U_725, V_726) | c1_2(U_725, a526) | c3_2(U_725, a526) | ~c8_1(U_725) | ~ndr1_1(U_725) | ssSkP6(U_725)))). % 20.87/7.57 tff(c_4633, plain, (![U_725, V_726]: (c2_2(U_725, a548) | ~c1_1(U_725) | c3_2(U_725, a479) | c3_2(U_725, V_726) | c5_2(U_725, V_726) | c2_2(U_725, a526) | ~c2_2(U_725, a479) | ~c1_2(U_725, V_726) | c1_2(U_725, a526) | c3_2(U_725, a526) | ~c8_1(U_725) | ~ndr1_1(U_725) | ssSkP6(U_725)))). % 20.87/7.57 tff(c_3157, plain, (![U_12, V_614, X_615]: (c2_2(U_12, a548) | ~c1_1(U_12) | c3_2(U_12, a479) | c3_2(U_12, V_614) | c5_2(U_12, V_614) | c2_2(U_12, X_615) | c6_2(U_12, X_615) | ~c2_2(U_12, a479) | ~c1_2(U_12, V_614) | c1_2(U_12, a526) | c3_2(U_12, a526) | ~c8_1(U_12) | ~ndr1_1(U_12) | ssSkP6(U_12)))). % 20.87/7.57 tff(c_4426, plain, (![U_712, W_713, V_714]: (~c3_1(U_712) | c1_2(U_712, W_713) | ~c8_1(U_712) | c3_2(U_712, W_713) | c3_2(U_712, V_714) | c5_2(U_712, V_714) | c2_2(U_712, a459) | ~c2_2(U_712, W_713) | ~c1_2(U_712, V_714) | c2_1(U_712) | c1_1(U_712) | c3_2(U_712, a479) | c1_2(U_712, a479) | ~ndr1_1(U_712)))). % 20.87/7.57 tff(c_4428, plain, (![U_712, W_713, V_714]: (ssSkP2(U_712) | c1_2(U_712, W_713) | ~c8_1(U_712) | c3_2(U_712, W_713) | c3_2(U_712, V_714) | c5_2(U_712, V_714) | c2_2(U_712, a492) | ~c2_2(U_712, W_713) | ~c1_2(U_712, V_714) | c2_1(U_712) | c1_1(U_712) | c3_2(U_712, a479) | c1_2(U_712, a479) | ~ndr1_1(U_712)))). % 20.87/7.57 tff(c_4427, plain, (![U_712, W_713, V_714]: (ssSkP7(U_712) | c1_2(U_712, W_713) | ~c8_1(U_712) | c3_2(U_712, W_713) | c3_2(U_712, V_714) | c5_2(U_712, V_714) | c2_2(U_712, a554) | ~c2_2(U_712, W_713) | ~c1_2(U_712, V_714) | c2_1(U_712) | c1_1(U_712) | c3_2(U_712, a479) | c1_2(U_712, a479) | ~ndr1_1(U_712)))). % 20.87/7.57 tff(c_3456, plain, (![U_632, W_591, V_592, X_593]: (c1_2(U_632, W_591) | ~c8_1(U_632) | c3_2(U_632, W_591) | c3_2(U_632, V_592) | c5_2(U_632, V_592) | c2_2(U_632, X_593) | c6_2(U_632, X_593) | ~c2_2(U_632, W_591) | ~c1_2(U_632, V_592) | c2_1(U_632) | c1_1(U_632) | c3_2(U_632, a479) | c1_2(U_632, a479) | ~ndr1_1(U_632)))). % 20.87/7.57 tff(c_3542, plain, (![U_639, W_641, X_640, V_642]: (~c1_1(U_639) | ~c7_2(U_639, a548) | ~c6_2(U_639, W_641) | c8_1(U_639) | c4_2(U_639, X_640) | ~c3_1(U_639) | ~c3_2(U_639, X_640) | c3_2(U_639, W_641) | c3_2(U_639, V_642) | c5_2(U_639, V_642) | c2_2(U_639, X_640) | ~c2_2(U_639, W_641) | ~c1_2(U_639, V_642) | ~ndr1_1(U_639)))). % 20.87/7.57 tff(c_4223, plain, (![U_697, V_698]: (~c3_1(U_697) | ~c1_1(U_697) | ~c4_2(U_697, a548) | c3_2(U_697, a479) | c3_2(U_697, V_698) | c5_2(U_697, V_698) | c2_2(U_697, a459) | ~c2_2(U_697, a479) | ~c1_2(U_697, V_698) | c1_2(U_697, a526) | c3_2(U_697, a526) | ~c8_1(U_697) | ~ndr1_1(U_697) | ssSkP6(U_697)))). % 20.87/7.57 tff(c_4225, plain, (![U_697, V_698]: (ssSkP2(U_697) | ~c1_1(U_697) | ~c4_2(U_697, a548) | c3_2(U_697, a479) | c3_2(U_697, V_698) | c5_2(U_697, V_698) | c2_2(U_697, a492) | ~c2_2(U_697, a479) | ~c1_2(U_697, V_698) | c1_2(U_697, a526) | c3_2(U_697, a526) | ~c8_1(U_697) | ~ndr1_1(U_697) | ssSkP6(U_697)))). % 20.87/7.57 tff(c_4224, plain, (![U_697, V_698]: (ssSkP7(U_697) | ~c1_1(U_697) | ~c4_2(U_697, a548) | c3_2(U_697, a479) | c3_2(U_697, V_698) | c5_2(U_697, V_698) | c2_2(U_697, a554) | ~c2_2(U_697, a479) | ~c1_2(U_697, V_698) | c1_2(U_697, a526) | c3_2(U_697, a526) | ~c8_1(U_697) | ~ndr1_1(U_697) | ssSkP6(U_697)))). % 20.87/7.57 tff(c_4215, plain, (![U_697, V_698]: (~c1_1(U_697) | ~c4_2(U_697, a548) | c3_2(U_697, a479) | c3_2(U_697, V_698) | c5_2(U_697, V_698) | c2_2(U_697, a526) | ~c2_2(U_697, a479) | ~c1_2(U_697, V_698) | c1_2(U_697, a526) | c3_2(U_697, a526) | ~c8_1(U_697) | ~ndr1_1(U_697) | ssSkP6(U_697)))). % 20.87/7.57 tff(c_3186, plain, (![U_12, V_622, X_623]: (~c1_1(U_12) | ~c4_2(U_12, a548) | c3_2(U_12, a479) | c3_2(U_12, V_622) | c5_2(U_12, V_622) | c2_2(U_12, X_623) | c6_2(U_12, X_623) | ~c2_2(U_12, a479) | ~c1_2(U_12, V_622) | c1_2(U_12, a526) | c3_2(U_12, a526) | ~c8_1(U_12) | ~ndr1_1(U_12) | ssSkP6(U_12)))). % 20.87/7.57 tff(c_3718, plain, (![U_657, V_148]: (c5_2(U_657, V_148) | c2_2(U_657, V_148) | ~c4_1(U_657) | c3_2(U_657, a526) | ~c1_1(U_657) | ~c4_2(U_657, a548) | ssSkP6(U_657) | ssSkP3(U_657) | c3_2(U_657, a502) | c3_2(U_657, a572) | c2_2(U_657, a526) | ~c2_2(U_657, a502) | ~c1_2(U_657, a572) | ~ndr1_1(U_657)))). % 20.87/7.57 tff(c_3723, plain, (![U_659, V_148]: (c5_2(U_659, V_148) | c2_2(U_659, V_148) | ~c4_1(U_659) | c2_2(U_659, a548) | c3_2(U_659, a526) | ~c1_1(U_659) | ssSkP6(U_659) | ssSkP3(U_659) | c3_2(U_659, a502) | c3_2(U_659, a572) | c2_2(U_659, a526) | ~c2_2(U_659, a502) | ~c1_2(U_659, a572) | ~ndr1_1(U_659)))). % 20.87/7.57 tff(c_3989, plain, (![U_678, X_679, V_680]: (~c1_1(U_678) | ~c4_2(U_678, a548) | ~c6_2(U_678, a481) | c8_1(U_678) | c4_2(U_678, X_679) | ~c3_2(U_678, X_679) | c3_2(U_678, a481) | c3_2(U_678, V_680) | c5_2(U_678, V_680) | c2_2(U_678, X_679) | ~c2_2(U_678, a481) | ~c1_2(U_678, V_680) | ~ndr1_1(U_678)))). % 20.87/7.57 tff(c_3379, plain, (![U_628, W_629, V_630]: (c3_2(U_628, a526) | ~c1_1(U_628) | ~c4_2(U_628, a548) | ssSkP6(U_628) | c6_2(U_628, a479) | c1_2(U_628, W_629) | ~c8_1(U_628) | c3_2(U_628, W_629) | c3_2(U_628, V_630) | c5_2(U_628, V_630) | c2_2(U_628, a526) | ~c2_2(U_628, W_629) | ~c1_2(U_628, V_630) | ~ndr1_1(U_628)))). % 20.87/7.57 tff(c_3988, plain, (![U_678, X_679, V_680]: (c2_2(U_678, a548) | ~c1_1(U_678) | ~c6_2(U_678, a481) | c8_1(U_678) | c4_2(U_678, X_679) | ~c3_2(U_678, X_679) | c3_2(U_678, a481) | c3_2(U_678, V_680) | c5_2(U_678, V_680) | c2_2(U_678, X_679) | ~c2_2(U_678, a481) | ~c1_2(U_678, V_680) | ~ndr1_1(U_678)))). % 20.87/7.57 tff(c_3985, plain, (![U_678, X_679, V_680]: (~c1_1(U_678) | ~c7_2(U_678, a548) | ~c6_2(U_678, a481) | c8_1(U_678) | c4_2(U_678, X_679) | ~c3_2(U_678, X_679) | c3_2(U_678, a481) | c3_2(U_678, V_680) | c5_2(U_678, V_680) | c2_2(U_678, X_679) | ~c2_2(U_678, a481) | ~c1_2(U_678, V_680) | ~ndr1_1(U_678)))). % 20.87/7.58 tff(c_3871, plain, (![U_590, X_593, V_592]: (c8_1(U_590) | c4_2(U_590, X_593) | ~c3_2(U_590, X_593) | c3_2(U_590, a481) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | ~c2_2(U_590, a481) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590) | c8_2(U_590, a481)))). % 20.87/7.58 tff(c_2916, plain, (![U_590, X_593, W_591, V_592]: (c8_1(U_590) | c8_2(U_590, a481) | c4_2(U_590, X_593) | ~c3_2(U_590, X_593) | c8_2(U_590, W_591) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_3713, plain, (![U_654, V_148, X_655]: (c5_2(U_654, V_148) | c2_2(U_654, V_148) | ~c4_1(U_654) | ssSkP3(U_654) | c8_1(U_654) | c4_2(U_654, X_655) | ~c3_1(U_654) | ~c3_2(U_654, X_655) | c3_2(U_654, a502) | c3_2(U_654, a572) | c2_2(U_654, X_655) | ~c2_2(U_654, a502) | ~c1_2(U_654, a572) | ~ndr1_1(U_654)))). % 20.87/7.58 tff(c_3032, plain, (![U_594, X_596, V_595]: (c8_1(U_594) | c2_2(U_594, a481) | c4_2(U_594, X_596) | ~c3_2(U_594, X_596) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, X_596) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.87/7.58 tff(c_3031, plain, (![U_594, X_596, V_595]: (c8_1(U_594) | c8_2(U_594, a481) | c4_2(U_594, X_596) | ~c3_2(U_594, X_596) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, X_596) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.87/7.58 tff(c_2917, plain, (![U_590, X_593, W_591, V_592]: (c8_1(U_590) | c2_2(U_590, a481) | c4_2(U_590, X_593) | ~c3_2(U_590, X_593) | c8_2(U_590, W_591) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_3033, plain, (![U_594, V_595]: (c2_2(U_594, a548) | c3_2(U_594, a526) | ~c1_1(U_594) | ssSkP6(U_594) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, a526) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.87/7.58 tff(c_3034, plain, (![U_594, V_595]: (c3_2(U_594, a526) | ~c1_1(U_594) | ~c4_2(U_594, a548) | ssSkP6(U_594) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, a526) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.87/7.58 tff(c_3547, plain, (![U_639, X_640, V_642]: (ssSkP3(U_639) | c8_1(U_639) | c4_2(U_639, X_640) | ~c3_1(U_639) | ~c3_2(U_639, X_640) | c3_2(U_639, a502) | c3_2(U_639, V_642) | c5_2(U_639, V_642) | c2_2(U_639, X_640) | ~c2_2(U_639, a502) | ~c1_2(U_639, V_642) | ~ndr1_1(U_639)))). % 20.87/7.58 tff(c_3129, plain, (![U_606, V_148]: (c5_2(U_606, V_148) | c2_2(U_606, V_148) | ~c4_1(U_606) | ~c8_1(U_606) | ~c3_1(U_606) | ssSkP3(U_606) | c3_2(U_606, a502) | c3_2(U_606, a572) | c2_2(U_606, a459) | ~c2_2(U_606, a502) | ~c1_2(U_606, a572) | ~ndr1_1(U_606)))). % 20.87/7.58 tff(c_3387, plain, (![U_628, W_629, V_630]: (ssSkP7(U_628) | c6_2(U_628, a479) | c1_2(U_628, W_629) | ~c8_1(U_628) | c3_2(U_628, W_629) | c3_2(U_628, V_630) | c5_2(U_628, V_630) | c2_2(U_628, a554) | ~c2_2(U_628, W_629) | ~c1_2(U_628, V_630) | ~ndr1_1(U_628)))). % 20.87/7.58 tff(c_3388, plain, (![U_628, W_629, V_630]: (ssSkP2(U_628) | c6_2(U_628, a479) | c1_2(U_628, W_629) | ~c8_1(U_628) | c3_2(U_628, W_629) | c3_2(U_628, V_630) | c5_2(U_628, V_630) | c2_2(U_628, a492) | ~c2_2(U_628, W_629) | ~c1_2(U_628, V_630) | ~ndr1_1(U_628)))). % 20.87/7.58 tff(c_3212, plain, (![U_590, W_591, V_592]: (c1_2(U_590, W_591) | ~c8_1(U_590) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, a479) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590) | c6_2(U_590, a479)))). % 20.87/7.58 tff(c_3087, plain, (![U_382, X_385, W_384, V_383]: (c8_1(U_382) | c4_2(U_382, X_385) | ~c3_1(U_382) | ~c3_2(U_382, X_385) | c8_2(U_382, W_384) | c3_2(U_382, W_384) | c3_2(U_382, V_383) | c5_2(U_382, V_383) | c2_2(U_382, X_385) | ~c2_2(U_382, W_384) | ~c1_2(U_382, V_383) | ~ndr1_1(U_382)))). % 20.87/7.58 tff(c_3493, plain, (c2_2(a534, a535))). % 20.87/7.58 tff(c_3491, plain, (![U_637]: (c1_2(U_637, a526) | ~c8_1(U_637) | ssSkP6(U_637) | c2_1(U_637) | c1_1(U_637) | c3_2(U_637, a479) | c1_2(U_637, a479) | ~ndr1_1(U_637)))). % 20.87/7.58 tff(c_3470, plain, (![U_632]: (c1_2(U_632, a456) | c3_2(U_632, a456) | ~c8_1(U_632) | ssSkP0(U_632) | c2_1(U_632) | c1_1(U_632) | c3_2(U_632, a479) | c1_2(U_632, a479) | ~ndr1_1(U_632)))). % 20.87/7.58 tff(c_3473, plain, (![U_632]: (ssSkP3(U_632) | c2_1(U_632) | c1_1(U_632) | c3_2(U_632, a502) | c1_2(U_632, a502) | ~ndr1_1(U_632)))). % 20.87/7.58 tff(c_3472, plain, (![U_632]: (ssSkP2(U_632) | c2_1(U_632) | c1_1(U_632) | c3_2(U_632, a492) | c1_2(U_632, a492) | ~ndr1_1(U_632)))). % 20.87/7.58 tff(c_3479, plain, (c1_2(a534, a479))). % 20.87/7.58 tff(c_3478, plain, (c1_2(a498, a500))). % 20.87/7.58 tff(c_3399, plain, (![U_469, Z_470]: (c2_1(U_469) | c1_1(U_469) | c3_2(U_469, Z_470) | c7_2(U_469, Z_470) | c1_2(U_469, Z_470) | ~ndr1_1(U_469)))). % 20.87/7.58 tff(c_3396, plain, (~c1_1(a577))). % 20.87/7.58 tff(c_3389, plain, (~c8_1(a577))). % 20.87/7.58 tff(c_2904, plain, (![U_590, W_591, V_592, X_593]: (c6_2(U_590, a479) | c1_2(U_590, W_591) | ~c8_1(U_590) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | c6_2(U_590, X_593) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_2903, plain, (![U_590, W_591, V_592, X_593]: (c1_2(U_590, W_591) | ~c8_1(U_590) | ~c7_2(U_590, a479) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | c6_2(U_590, X_593) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_2906, plain, (![U_590, W_591, V_592, X_593]: (~c1_1(U_590) | ~c4_2(U_590, a548) | ~c6_2(U_590, W_591) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | c6_2(U_590, X_593) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_2902, plain, (![U_590, W_591, V_592, X_593]: (~c1_1(U_590) | ~c7_2(U_590, a548) | ~c6_2(U_590, W_591) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | c6_2(U_590, X_593) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_2905, plain, (![U_590, W_591, V_592, X_593]: (c2_2(U_590, a548) | ~c1_1(U_590) | ~c6_2(U_590, W_591) | c3_2(U_590, W_591) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | c6_2(U_590, X_593) | ~c2_2(U_590, W_591) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_3124, plain, (![U_604, V_148]: (c5_2(U_604, V_148) | c2_2(U_604, V_148) | ~c4_1(U_604) | ssSkP7(U_604) | ssSkP3(U_604) | c3_2(U_604, a502) | c3_2(U_604, a572) | c2_2(U_604, a554) | ~c2_2(U_604, a502) | ~c1_2(U_604, a572) | ~ndr1_1(U_604)))). % 20.87/7.58 tff(c_3137, plain, (~ssSkC23)). % 20.87/7.58 tff(c_3119, plain, (![U_602, V_148]: (c5_2(U_602, V_148) | c2_2(U_602, V_148) | ~c4_1(U_602) | ssSkP2(U_602) | ssSkP3(U_602) | c3_2(U_602, a502) | c3_2(U_602, a572) | c2_2(U_602, a492) | ~c2_2(U_602, a502) | ~c1_2(U_602, a572) | ~ndr1_1(U_602)))). % 20.87/7.58 tff(c_3042, plain, (![U_594, V_595]: (~c8_1(U_594) | ~c3_1(U_594) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, a459) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.87/7.58 tff(c_3043, plain, (![U_594, V_595]: (ssSkP7(U_594) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, a554) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.87/7.58 tff(c_3044, plain, (![U_594, V_595]: (ssSkP2(U_594) | ssSkP3(U_594) | c3_2(U_594, a502) | c3_2(U_594, V_595) | c5_2(U_594, V_595) | c2_2(U_594, a492) | ~c2_2(U_594, a502) | ~c1_2(U_594, V_595) | ~ndr1_1(U_594)))). % 20.87/7.58 tff(c_3112, plain, (~c2_2(a498, a502))). % 20.87/7.58 tff(c_3111, plain, (~c2_2(a542, a502))). % 20.87/7.58 tff(c_3108, plain, (~c2_2(a534, a502))). % 20.87/7.58 tff(c_3106, plain, (![U_16]: (c8_1(U_16) | ~c3_1(U_16) | c2_2(U_16, a548) | ~c1_1(U_16) | ~ndr1_1(U_16) | ssSkP0(U_16)))). % 20.87/7.58 tff(c_3095, plain, (![U_599]: (c8_1(U_599) | ~c3_1(U_599) | ~ndr1_1(U_599) | ~c3_2(U_599, a456) | ssSkP0(U_599)))). % 20.87/7.58 tff(c_3069, plain, (![U_427, V_430]: (c8_1(U_427) | c4_2(U_427, V_430) | ~c3_1(U_427) | ~ndr1_1(U_427) | ~c3_2(U_427, V_430) | ~c6_2(U_427, V_430)))). % 20.87/7.58 tff(c_3066, plain, (~c2_2(a577, a502))). % 20.87/7.58 tff(c_3065, plain, (~c2_1(a573))). % 20.87/7.58 tff(c_3057, plain, (~c8_1(a573))). % 20.87/7.58 tff(c_3048, plain, (~ndr1_1(a573))). % 20.87/7.58 tff(c_2907, plain, (![U_590, V_592, X_593]: (ssSkP3(U_590) | c3_2(U_590, a502) | c3_2(U_590, V_592) | c5_2(U_590, V_592) | c2_2(U_590, X_593) | c6_2(U_590, X_593) | ~c2_2(U_590, a502) | ~c1_2(U_590, V_592) | ~ndr1_1(U_590)))). % 20.87/7.58 tff(c_2918, plain, (~c2_2(a577, a579))). % 20.87/7.58 tff(c_2822, plain, (![U_382, W_384, V_383, X_385]: (c8_2(U_382, W_384) | c3_2(U_382, W_384) | c3_2(U_382, V_383) | c5_2(U_382, V_383) | c2_2(U_382, X_385) | c6_2(U_382, X_385) | ~c2_2(U_382, W_384) | ~c1_2(U_382, V_383) | ~ndr1_1(U_382)))). % 20.87/7.58 tff(c_2817, plain, (c1_2(a577, a578))). % 20.87/7.58 tff(c_2814, plain, (~c6_2(a577, a578))). % 20.87/7.58 tff(c_2783, plain, (c8_2(a577, a578))). % 20.87/7.58 tff(c_2530, plain, (![U_248]: (c3_2(U_248, a481) | ~c1_1(U_248) | ~c6_2(U_248, a481) | c8_1(U_248) | c4_2(U_248, a456) | ~c3_2(U_248, a456) | ssSkP0(U_248) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.87/7.58 tff(c_2752, plain, (![U_248, V_249]: (c3_2(U_248, V_249) | ~c1_1(U_248) | c8_1(U_248) | ~c2_1(U_248) | ~c4_2(U_248, V_249) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, V_249) | ~c2_2(U_248, V_249)))). % 20.87/7.58 tff(c_2778, plain, (~c4_2(a577, a579))). % 20.87/7.58 tff(c_2771, plain, (~c8_2(a577, a579))). % 20.87/7.58 tff(c_2763, plain, (![U_13]: (c3_2(U_13, a515) | ~c1_1(U_13) | ~c6_2(U_13, a515) | c8_1(U_13) | ~c2_1(U_13) | ~c4_2(U_13, a515) | c7_1(U_13) | c4_1(U_13) | ~ndr1_1(U_13) | ~c6_2(U_13, a548) | ~c2_2(U_13, a548) | ssSkP5(U_13)))). % 20.87/7.58 tff(c_2512, plain, (![U_248, V_575]: (c3_2(U_248, V_575) | ~c1_1(U_248) | ~c6_2(U_248, V_575) | c8_1(U_248) | ~c2_1(U_248) | ~c7_2(U_248, V_575) | ~c4_2(U_248, V_575) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, a548) | ~c2_2(U_248, a548)))). % 20.87/7.58 tff(c_2722, plain, (~c6_2(a577, a579))). % 20.87/7.58 tff(c_2719, plain, (c1_1(a531))). % 20.87/7.58 tff(c_2718, plain, (c1_1(a570))). % 20.87/7.58 tff(c_2717, plain, (ndr1_1(a577))). % 20.87/7.58 tff(c_2713, plain, (c1_1(a537))). % 20.87/7.58 tff(c_2708, plain, (c1_1(a458))). % 20.87/7.58 tff(c_2688, plain, (![U_410]: (c2_1(U_410) | c1_1(U_410) | ~c4_1(U_410)))). % 20.87/7.58 tff(c_2684, plain, (~c7_1(a577))). % 20.87/7.58 tff(c_2487, plain, (![U_248, V_249]: (c2_2(U_248, a548) | c3_2(U_248, V_249) | ~c1_1(U_248) | c8_1(U_248) | ~c2_1(U_248) | ~c4_2(U_248, V_249) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, V_249) | ~c2_2(U_248, V_249)))). % 20.87/7.58 tff(c_2449, plain, (![U_248, V_249]: (c3_2(U_248, V_249) | ~c1_1(U_248) | ~c4_2(U_248, a548) | c8_1(U_248) | ~c2_1(U_248) | ~c4_2(U_248, V_249) | c7_1(U_248) | c4_1(U_248) | ~ndr1_1(U_248) | ~c6_2(U_248, V_249) | ~c2_2(U_248, V_249)))). % 20.87/7.58 tff(c_2652, plain, (c4_2(a534, a535))). % 20.87/7.58 tff(c_2649, plain, (~c2_1(a559))). % 20.87/7.58 tff(c_2647, plain, (~c3_2(a559, a560))). % 20.87/7.58 tff(c_2625, plain, (~c2_2(a534, a479))). % 20.87/7.58 tff(c_2628, plain, (c7_2(a559, a560))). % 20.87/7.58 tff(c_2621, plain, (c3_2(a534, a535))). % 20.87/7.58 tff(c_2624, plain, (c4_2(a559, a560))). % 20.87/7.58 tff(c_2614, plain, (~c7_2(a534, a479))). % 20.87/7.58 tff(c_2583, plain, (c8_2(a534, a535))). % 20.87/7.58 tff(c_2580, plain, (~c6_2(a534, a535))). % 20.87/7.58 tff(c_2577, plain, (~c2_1(a534))). % 20.87/7.58 tff(c_2574, plain, (ndr1_1(a559))). % 20.87/7.58 tff(c_2571, plain, (~c6_1(a559))). % 20.87/7.58 tff(c_2568, plain, (c8_1(a534))). % 20.87/7.58 tff(c_2565, plain, (c7_1(a559))). % 20.87/7.58 tff(c_2562, plain, (c1_1(a573))). % 20.87/7.58 tff(c_2558, plain, (c3_1(a573))). % 20.87/7.58 tff(c_2554, plain, (ndr1_1(a534))). % 20.87/7.58 tff(c_2551, plain, (c4_1(a531))). % 20.87/7.59 tff(c_2548, plain, (~c6_1(a531))). % 20.87/7.59 tff(c_2545, plain, (~c5_1(a531))). % 20.87/7.59 tff(c_2134, plain, (![U_551]: (c3_2(U_551, a481) | ~c1_1(U_551) | ~c7_2(U_551, a548) | ~c6_2(U_551, a481) | c8_1(U_551) | c4_2(U_551, a456) | ~ndr1_1(U_551) | ~c3_2(U_551, a456) | ssSkP0(U_551)))). % 20.87/7.59 tff(c_2137, plain, (![U_551]: (c2_2(U_551, a548) | c3_2(U_551, a481) | ~c1_1(U_551) | ~c6_2(U_551, a481) | c8_1(U_551) | c4_2(U_551, a456) | ~ndr1_1(U_551) | ~c3_2(U_551, a456) | ssSkP0(U_551)))). % 20.87/7.59 tff(c_2138, plain, (![U_551]: (c3_2(U_551, a481) | ~c1_1(U_551) | ~c4_2(U_551, a548) | ~c6_2(U_551, a481) | c8_1(U_551) | c4_2(U_551, a456) | ~ndr1_1(U_551) | ~c3_2(U_551, a456) | ssSkP0(U_551)))). % 20.87/7.59 tff(c_2324, plain, (![U_558, V_559]: (c3_2(U_558, V_559) | ~c1_1(U_558) | ~c7_2(U_558, a548) | ~c6_2(U_558, V_559) | c8_1(U_558) | ~c2_1(U_558) | ~ndr1_1(U_558) | ~c7_2(U_558, V_559) | ~c4_2(U_558, V_559)))). % 20.87/7.59 tff(c_2498, plain, (![U_13]: (c2_2(U_13, a548) | c3_2(U_13, a515) | ~c1_1(U_13) | ~c6_2(U_13, a515) | c8_1(U_13) | ~c2_1(U_13) | ~ndr1_1(U_13) | ~c4_2(U_13, a515) | ssSkP5(U_13)))). % 20.87/7.59 tff(c_2327, plain, (![U_558, V_559]: (c2_2(U_558, a548) | c3_2(U_558, V_559) | ~c1_1(U_558) | ~c6_2(U_558, V_559) | c8_1(U_558) | ~c2_1(U_558) | ~ndr1_1(U_558) | ~c7_2(U_558, V_559) | ~c4_2(U_558, V_559)))). % 20.87/7.59 tff(c_2460, plain, (![U_13]: (c3_2(U_13, a515) | ~c1_1(U_13) | ~c4_2(U_13, a548) | ~c6_2(U_13, a515) | c8_1(U_13) | ~c2_1(U_13) | ~ndr1_1(U_13) | ~c4_2(U_13, a515) | ssSkP5(U_13)))). % 20.87/7.59 tff(c_2328, plain, (![U_558, V_559]: (c3_2(U_558, V_559) | ~c1_1(U_558) | ~c4_2(U_558, a548) | ~c6_2(U_558, V_559) | c8_1(U_558) | ~c2_1(U_558) | ~ndr1_1(U_558) | ~c7_2(U_558, V_559) | ~c4_2(U_558, V_559)))). % 20.87/7.59 tff(c_2426, plain, (~c1_1(a542))). % 20.87/7.59 tff(c_2423, plain, (~c1_1(a498))). % 20.87/7.59 tff(c_2420, plain, (~c1_1(a501))). % 20.87/7.59 tff(c_2419, plain, (~c1_1(a552))). % 20.87/7.59 tff(c_2384, plain, (![U_297]: (c8_1(U_297) | c3_1(U_297) | ~c1_1(U_297)))). % 20.87/7.59 tff(c_2284, plain, (![U_555]: (c3_2(U_555, a526) | ~c1_1(U_555) | ~c6_2(U_555, a526) | ssSkP6(U_555) | c7_1(U_555) | c4_1(U_555) | ~ndr1_1(U_555) | ~c6_2(U_555, a548) | ~c2_2(U_555, a548)))). % 20.87/7.59 tff(c_2368, plain, (![U_564]: (c7_1(U_564) | c4_1(U_564) | ~c2_2(U_564, a479) | c1_2(U_564, a526) | ~c8_1(U_564) | ~ndr1_1(U_564) | ssSkP6(U_564)))). % 20.87/7.59 tff(c_2348, plain, (![U_17]: (c7_1(U_17) | c4_1(U_17) | ~c2_2(U_17, a479) | c1_2(U_17, a456) | c3_2(U_17, a456) | ~c8_1(U_17) | ~ndr1_1(U_17) | ssSkP0(U_17)))). % 20.87/7.59 tff(c_2285, plain, (![U_555]: (c3_2(U_555, a456) | ~c1_1(U_555) | ~c6_2(U_555, a456) | ssSkP0(U_555) | c7_1(U_555) | c4_1(U_555) | ~ndr1_1(U_555) | ~c6_2(U_555, a548) | ~c2_2(U_555, a548)))). % 20.87/7.59 tff(c_2337, plain, (~c4_2(a546, a547))). % 20.87/7.59 tff(c_2297, plain, (![U_319, V_320]: (c8_1(U_319) | c8_2(U_319, V_320) | ~c2_1(U_319) | ~ndr1_1(U_319) | ~c7_2(U_319, V_320) | ~c4_2(U_319, V_320)))). % 20.87/7.59 tff(c_2290, plain, (![U_555]: (ssSkP3(U_555) | c7_1(U_555) | c4_1(U_555) | ~ndr1_1(U_555) | ~c6_2(U_555, a502) | ~c2_2(U_555, a502)))). % 20.87/7.59 tff(c_2252, plain, (![U_248, V_249]: (c7_1(U_248) | c4_1(U_248) | c7_2(U_248, V_249) | ~ndr1_1(U_248) | ~c6_2(U_248, V_249) | ~c2_2(U_248, V_249)))). % 20.87/7.59 tff(c_2246, plain, (~c3_1(a512))). % 20.87/7.59 tff(c_2245, plain, (~c3_1(a552))). % 20.87/7.59 tff(c_2241, plain, (~c3_1(a517))). % 20.87/7.59 tff(c_2239, plain, (c5_1(a565))). % 20.87/7.59 tff(c_2221, plain, (![U_292]: (c5_1(U_292) | ~c3_1(U_292) | ~c6_1(U_292)))). % 20.87/7.59 tff(c_2203, plain, (~c8_1(a501))). % 20.87/7.59 tff(c_2182, plain, (~ssSkC13)). % 20.87/7.59 tff(c_2177, plain, (~c6_1(a501))). % 20.87/7.59 tff(c_2173, plain, (c5_1(a501))). % 20.87/7.59 tff(c_2111, plain, (![U_12]: (c3_2(U_12, a526) | ~c1_1(U_12) | ~c7_2(U_12, a548) | ~ndr1_1(U_12) | ~c6_2(U_12, a526) | ssSkP6(U_12)))). % 20.87/7.59 tff(c_2147, plain, (~c4_2(a542, a548))). % 20.87/7.59 tff(c_2151, plain, (~ssSkC24)). % 20.87/7.59 tff(c_2110, plain, (![U_17]: (c3_2(U_17, a456) | ~c1_1(U_17) | ~c7_2(U_17, a548) | ~ndr1_1(U_17) | ~c6_2(U_17, a456) | ssSkP0(U_17)))). % 20.87/7.59 tff(c_2094, plain, (![U_16]: (c8_1(U_16) | c8_2(U_16, a481) | c4_2(U_16, a456) | ~ndr1_1(U_16) | ~c3_2(U_16, a456) | ssSkP0(U_16)))). % 20.87/7.59 tff(c_2096, plain, (![U_231, V_232]: (c3_2(U_231, V_232) | ~c1_1(U_231) | ~c7_2(U_231, a548) | ~ndr1_1(U_231) | ~c8_2(U_231, V_232) | ~c6_2(U_231, V_232)))). % 20.87/7.59 tff(c_2084, plain, (![U_180, V_181]: (c8_1(U_180) | c8_2(U_180, a481) | c4_2(U_180, V_181) | ~ndr1_1(U_180) | ~c3_2(U_180, V_181) | ~c6_2(U_180, V_181)))). % 20.87/7.59 tff(c_2053, plain, (![U_12]: (c1_2(U_12, a526) | c3_2(U_12, a526) | ~c8_1(U_12) | ~c7_2(U_12, a479) | ~ndr1_1(U_12) | ssSkP6(U_12)))). % 20.87/7.59 tff(c_2052, plain, (![U_17]: (c1_2(U_17, a456) | c3_2(U_17, a456) | ~c8_1(U_17) | ~c7_2(U_17, a479) | ~ndr1_1(U_17) | ssSkP0(U_17)))). % 20.87/7.59 tff(c_2064, plain, (![U_16]: (c8_1(U_16) | c2_2(U_16, a481) | c2_2(U_16, a548) | ~c1_1(U_16) | ~ndr1_1(U_16) | ssSkP0(U_16)))). % 20.87/7.59 tff(c_2035, plain, (![U_540]: (c8_1(U_540) | c2_2(U_540, a481) | ~ndr1_1(U_540) | ~c3_2(U_540, a456) | ssSkP0(U_540)))). % 20.87/7.59 tff(c_2038, plain, (![U_219, V_220]: (c1_2(U_219, V_220) | c3_2(U_219, V_220) | ~c8_1(U_219) | ~c7_2(U_219, a479) | ~ndr1_1(U_219) | ~c8_2(U_219, V_220)))). % 20.87/7.59 tff(c_2017, plain, (![U_178, V_179]: (c8_1(U_178) | c2_2(U_178, a481) | c4_2(U_178, V_179) | ~ndr1_1(U_178) | ~c3_2(U_178, V_179) | ~c6_2(U_178, V_179)))). % 20.87/7.59 tff(c_1989, plain, (![U_17]: (c6_2(U_17, a479) | c1_2(U_17, a456) | c3_2(U_17, a456) | ~c8_1(U_17) | ~ndr1_1(U_17) | ssSkP0(U_17)))). % 20.87/7.59 tff(c_1990, plain, (![U_12]: (c6_2(U_12, a479) | c1_2(U_12, a526) | c3_2(U_12, a526) | ~c8_1(U_12) | ~ndr1_1(U_12) | ssSkP6(U_12)))). % 20.87/7.59 tff(c_2001, plain, (~c8_1(a542))). % 20.87/7.59 tff(c_1997, plain, (~c8_1(a498))). % 20.87/7.59 tff(c_2000, plain, (ssSkC1)). % 20.87/7.59 tff(c_1975, plain, (![U_182, V_183]: (c6_2(U_182, a479) | c1_2(U_182, V_183) | c3_2(U_182, V_183) | ~c8_1(U_182) | ~ndr1_1(U_182) | ~c8_2(U_182, V_183)))). % 20.87/7.59 tff(c_1964, plain, (ssSkC7)). % 20.87/7.59 tff(c_1936, plain, (![U_12]: (c2_2(U_12, a548) | c3_2(U_12, a526) | ~c1_1(U_12) | ~ndr1_1(U_12) | ~c6_2(U_12, a526) | ssSkP6(U_12)))). % 20.87/7.59 tff(c_1957, plain, (![U_16]: (c3_2(U_16, a456) | ~c1_1(U_16) | ~c4_2(U_16, a548) | ~ndr1_1(U_16) | ssSkP0(U_16)))). % 20.87/7.59 tff(c_1951, plain, (![U_16]: (c2_2(U_16, a548) | c3_2(U_16, a456) | ~c1_1(U_16) | ~ndr1_1(U_16) | ssSkP0(U_16)))). % 20.87/7.59 tff(c_1946, plain, (ssSkC12)). % 20.87/7.59 tff(c_1911, plain, (![U_12]: (c3_2(U_12, a526) | ~c1_1(U_12) | ~c4_2(U_12, a548) | ~ndr1_1(U_12) | ~c6_2(U_12, a526) | ssSkP6(U_12)))). % 20.87/7.59 tff(c_1919, plain, (~c6_2(a542, a543))). % 20.87/7.59 tff(c_1921, plain, (![U_188, V_189]: (c2_2(U_188, a548) | c3_2(U_188, V_189) | ~c1_1(U_188) | ~ndr1_1(U_188) | ~c8_2(U_188, V_189) | ~c6_2(U_188, V_189)))). % 20.87/7.59 tff(c_1918, plain, (~c6_2(a498, a500))). % 20.87/7.59 tff(c_1896, plain, (![U_229, V_230]: (c3_2(U_229, V_230) | ~c1_1(U_229) | ~c4_2(U_229, a548) | ~ndr1_1(U_229) | ~c8_2(U_229, V_230) | ~c6_2(U_229, V_230)))). % 20.87/7.59 tff(c_1892, plain, (~c4_1(a542))). % 20.87/7.59 tff(c_1891, plain, (~c4_2(a498, a499))). % 20.87/7.59 tff(c_1857, plain, (![U_259, V_260]: (~c4_1(U_259) | ~ndr1_1(U_259) | ~c7_2(U_259, V_260) | ~c3_2(U_259, V_260) | ~c4_2(U_259, V_260)))). % 20.87/7.59 tff(c_1849, plain, (![U_139, V_140]: (c2_2(U_139, a572) | c5_2(U_139, V_140) | c2_2(U_139, V_140) | ~c4_1(U_139) | ~ndr1_1(U_139)))). % 20.87/7.59 tff(c_1845, plain, (![U_145, V_146]: (c5_2(U_145, V_146) | c2_2(U_145, V_146) | ~c4_1(U_145) | ~c6_2(U_145, a572) | ~ndr1_1(U_145)))). % 20.87/7.59 tff(c_1842, plain, (c4_1(a458))). % 20.87/7.59 tff(c_1829, plain, (![U_147, V_148]: (c5_2(U_147, V_148) | c2_2(U_147, V_148) | ~c4_1(U_147) | ~c5_2(U_147, a572) | ~ndr1_1(U_147)))). % 20.87/7.59 tff(c_1826, plain, (~c2_1(a458))). % 20.87/7.59 tff(c_1820, plain, (~c6_1(a458))). % 20.87/7.59 tff(c_1809, plain, (~ssSkC9)). % 20.87/7.59 tff(c_1791, plain, (~c3_1(a514))). % 20.87/7.59 tff(c_1789, plain, (~c3_1(a491))). % 20.87/7.59 tff(c_1779, plain, (~ndr1_1(a514))). % 20.87/7.59 tff(c_1778, plain, (~c2_1(a491))). % 20.87/7.59 tff(c_1768, plain, (~ndr1_1(a491))). % 20.87/7.59 tff(c_1766, plain, (~c3_1(a536))). % 20.87/7.59 tff(c_1765, plain, (~c2_1(a532))). % 20.87/7.59 tff(c_1755, plain, (~ndr1_1(a536))). % 20.87/7.59 tff(c_1753, plain, (~c2_1(a552))). % 20.87/7.59 tff(c_1751, plain, (~c8_1(a532))). % 20.87/7.59 tff(c_1734, plain, (~ndr1_1(a532))). % 20.87/7.59 tff(c_1733, plain, (~ndr1_1(a552))). % 20.87/7.59 tff(c_1728, plain, (~c3_1(a537))). % 20.87/7.59 tff(c_1731, plain, (ssSkC17)). % 20.87/7.59 tff(c_1727, plain, (~c3_1(a564))). % 20.87/7.59 tff(c_1726, plain, (~c2_1(a537))). % 20.87/7.59 tff(c_1716, plain, (~ndr1_1(a537))). % 20.87/7.59 tff(c_1706, plain, (~ndr1_1(a564))). % 20.87/7.59 tff(c_1704, plain, (~c2_1(a587))). % 20.87/7.59 tff(c_1702, plain, (~c8_1(a587))). % 20.87/7.59 tff(c_1693, plain, (~ndr1_1(a587))). % 20.87/7.59 tff(c_1600, plain, (![U_52]: (c5_1(U_52) | c4_2(U_52, a487) | ~c2_1(U_52)))). % 20.87/7.59 tff(c_1594, plain, (![U_51]: (c5_1(U_51) | c1_2(U_51, a487) | ~c2_1(U_51)))). % 20.87/7.59 tff(c_1590, plain, (![U_105]: (~c8_1(U_105) | ~c3_1(U_105) | ~c3_2(U_105, a459)))). % 20.87/7.59 tff(c_1587, plain, (~ssSkC3)). % 20.87/7.59 tff(c_1576, plain, (~c4_2(a542, a502))). % 20.87/7.59 tff(c_1571, plain, (~c2_1(a470))). % 20.87/7.59 tff(c_1574, plain, (![U_74]: (c7_2(U_74, a459) | ~c8_1(U_74) | ~c3_1(U_74)))). % 20.87/7.59 tff(c_1570, plain, (~c3_1(a470))). % 20.87/7.59 tff(c_1567, plain, (~c2_1(a596))). % 20.87/7.59 tff(c_1566, plain, (~c3_1(a596))). % 20.87/7.59 tff(c_1557, plain, (~ndr1_1(a470))). % 20.87/7.59 tff(c_1556, plain, (ssSkP2(a542))). % 20.87/7.59 tff(c_1543, plain, (~c4_2(a542, a492))). % 20.87/7.59 tff(c_1544, plain, (~ndr1_1(a596))). % 20.87/7.60 tff(c_1531, plain, (![U_70]: (c7_2(a542, U_70) | ~c4_2(a542, U_70)))). % 20.87/7.60 tff(c_1528, plain, (~ssSkC18)). % 20.87/7.60 tff(c_1514, plain, (~c2_1(a568))). % 20.87/7.60 tff(c_1513, plain, (~c3_1(a568))). % 20.87/7.60 tff(c_1504, plain, (~ndr1_1(a568))). % 20.87/7.60 tff(c_1498, plain, (~c2_1(a600))). % 20.87/7.60 tff(c_1495, plain, (~c2_1(a592))). % 20.87/7.60 tff(c_1493, plain, (~c8_1(a600))). % 20.87/7.60 tff(c_1482, plain, (~c3_1(a592))). % 20.87/7.60 tff(c_1484, plain, (~ndr1_1(a600))). % 20.87/7.60 tff(c_1473, plain, (~ndr1_1(a592))). % 20.87/7.60 tff(c_1471, plain, (![U_104]: (~c8_1(U_104) | ~c3_1(U_104) | ~c6_2(U_104, a459)))). % 20.87/7.60 tff(c_1456, plain, (![U_53]: (ndr1_1(U_53) | ~c8_1(U_53) | ~c3_1(U_53)))). % 20.87/7.60 tff(c_1451, plain, (ssSkC22)). % 20.87/7.60 tff(c_1446, plain, (~ssSkC16)). % 20.87/7.60 tff(c_1442, plain, (![U_42]: (c5_1(U_42) | ndr1_1(U_42) | ~c2_1(U_42)))). % 20.87/7.60 tff(c_1439, plain, (ssSkC8)). % 20.87/7.60 tff(c_1424, plain, (~ssSkC0)). % 20.87/7.60 tff(c_268, plain, (![U_17]: (ssSkP0(U_17) | c8_2(U_17, a456)))). % 20.87/7.60 tff(c_232, plain, (![U_10]: (ssSkP8(U_10) | c5_2(U_10, a588)))). % 20.87/7.60 tff(c_250, plain, (![U_12]: (ssSkP6(U_12) | c8_2(U_12, a526)))). % 20.87/7.60 tff(c_266, plain, (![U_16]: (ssSkP0(U_16) | c6_2(U_16, a456)))). % 20.87/7.60 tff(c_248, plain, (![U_11]: (ssSkP6(U_11) | c7_2(U_11, a526)))). % 20.87/7.60 tff(c_258, plain, (![U_14]: (ssSkP4(U_14) | c1_2(U_14, a503)))). % 20.87/7.60 tff(c_396, plain, (![U_31]: (ssSkP1(U_31) | ~c2_2(U_31, a485)))). % 20.87/7.60 tff(c_390, plain, (![U_28]: (ssSkP3(U_28) | ~c8_2(U_28, a502)))). % 20.87/7.60 tff(c_394, plain, (![U_30]: (ssSkP2(U_30) | ~c7_2(U_30, a492)))). % 20.87/7.60 tff(c_372, plain, (![U_21]: (ssSkP6(U_21) | ~c3_2(U_21, a526)))). % 20.87/7.60 tff(c_360, plain, (![U_18]: (ssSkP8(U_18) | ~c1_2(U_18, a588)))). % 20.87/7.60 tff(c_364, plain, (![U_20]: (ssSkP7(U_20) | ~c3_2(U_20, a554)))). % 20.87/7.60 tff(c_384, plain, (![U_25]: (ssSkP4(U_25) | ~c4_2(U_25, a503)))). % 20.87/7.60 tff(c_386, plain, (![U_26]: (ssSkP3(U_26) | ~c1_2(U_26, a502)))). % 20.87/7.60 tff(c_374, plain, (![U_22]: (ssSkP5(U_22) | ~c2_2(U_22, a515)))). % 20.87/7.60 tff(c_400, plain, (![U_33]: (ssSkP1(U_33) | ~c1_2(U_33, a485)))). % 20.87/7.60 tff(c_388, plain, (![U_27]: (ssSkP3(U_27) | ~c7_2(U_27, a502)))). % 20.87/7.60 tff(c_376, plain, (![U_23]: (ssSkP5(U_23) | ~c3_2(U_23, a515)))). % 20.87/7.60 tff(c_398, plain, (![U_32]: (ssSkP1(U_32) | ~c3_2(U_32, a485)))). % 20.87/7.60 tff(c_362, plain, (![U_19]: (ssSkP7(U_19) | ~c6_2(U_19, a554)))). % 20.87/7.60 tff(c_402, plain, (![U_34]: (ssSkP0(U_34) | ~c4_2(U_34, a456)))). % 20.87/7.60 tff(c_1372, plain, (c7_2(a498, a499))). % 20.87/7.60 tff(c_392, plain, (![U_29]: (ssSkP2(U_29) | ~c6_2(U_29, a492)))). % 20.87/7.60 tff(c_382, plain, (![U_24]: (ssSkP4(U_24) | ~c3_2(U_24, a503)))). % 20.87/7.60 tff(c_1360, plain, (c3_2(a498, a499))). % 20.87/7.60 tff(c_1359, plain, (c8_2(a498, a500))). % 20.87/7.60 tff(c_1358, plain, (c4_2(a498, a500))). % 20.87/7.60 tff(c_1353, plain, (~c4_2(a520, a521))). % 20.87/7.60 tff(c_1350, plain, (c2_2(a520, a521))). % 20.87/7.60 tff(c_1349, plain, (~c1_2(a520, a521))). % 20.87/7.60 tff(c_252, plain, (![U_13]: (ssSkP5(U_13) | c7_2(U_13, a515)))). % 20.87/7.60 tff(c_1340, plain, (~c7_2(a498, a500))). % 20.87/7.60 tff(c_260, plain, (![U_15]: (ssSkP2(U_15) | c4_2(U_15, a492)))). % 20.87/7.60 tff(c_1337, plain, (~c8_2(a498, a499))). % 20.87/7.60 tff(c_1333, plain, (c3_2(a570, a571))). % 20.87/7.60 tff(c_1332, plain, (c8_2(a542, a543))). % 20.87/7.60 tff(c_1330, plain, (c7_1(a498))). % 20.87/7.60 tff(c_1324, plain, (~ssSkC14)). % 20.87/7.60 tff(c_92, plain, (![U_1]: (ssSkP8(U_1) | ndr1_1(U_1)))). % 20.87/7.60 tff(c_1320, plain, (~ssSkC4)). % 20.87/7.60 tff(c_1317, plain, (c7_2(a546, a547))). % 20.87/7.60 tff(c_1316, plain, (~c4_2(a542, a543))). % 20.87/7.60 tff(c_1312, plain, (ndr1_1(a520))). % 20.87/7.60 tff(c_150, plain, (![U_9]: (ssSkP0(U_9) | ndr1_1(U_9)))). % 20.87/7.60 tff(c_1309, plain, (~c5_1(a520))). % 20.87/7.60 tff(c_1308, plain, (~c2_1(a520))). % 20.87/7.60 tff(c_1304, plain, (ndr1_1(a498))). % 20.87/7.60 tff(c_1303, plain, (c2_2(a570, a571))). % 20.87/7.60 tff(c_1300, plain, (~ssSkC6)). % 20.87/7.60 tff(c_1299, plain, (c3_2(a512, a513))). % 20.87/7.60 tff(c_1298, plain, (c1_2(a570, a571))). % 20.87/7.60 tff(c_146, plain, (![U_8]: (ssSkP1(U_8) | ndr1_1(U_8)))). % 20.87/7.60 tff(c_1293, plain, (~ssSkC19)). % 20.87/7.60 tff(c_140, plain, (![U_5]: (ssSkP4(U_5) | ndr1_1(U_5)))). % 20.87/7.60 tff(c_1289, plain, (~c2_2(a546, a547))). % 20.87/7.60 tff(c_1288, plain, (~ssSkC5)). % 20.87/7.60 tff(c_144, plain, (![U_7]: (ssSkP2(U_7) | ndr1_1(U_7)))). % 20.87/7.60 tff(c_142, plain, (![U_6]: (ssSkP3(U_6) | ndr1_1(U_6)))). % 20.87/7.60 tff(c_132, plain, (![U_4]: (ssSkP5(U_4) | ndr1_1(U_4)))). % 20.87/7.60 tff(c_106, plain, (![U_2]: (ssSkP7(U_2) | ndr1_1(U_2)))). % 20.87/7.60 tff(c_1281, plain, (~c2_2(a512, a513))). % 20.87/7.60 tff(c_1280, plain, (~c8_2(a546, a547))). % 20.87/7.60 tff(c_1278, plain, (~c1_2(a512, a513))). % 20.87/7.60 tff(c_124, plain, (![U_3]: (ssSkP6(U_3) | ndr1_1(U_3)))). % 20.87/7.60 tff(c_1271, plain, (c2_1(a565))). % 20.87/7.60 tff(c_1270, plain, (~c5_1(a537))). % 20.87/7.60 tff(c_1269, plain, (c5_1(a514))). % 20.87/7.60 tff(c_1266, plain, (c7_1(a470))). % 20.87/7.60 tff(c_1265, plain, (c6_1(a517))). % 20.87/7.60 tff(c_1264, plain, (~c7_1(a536))). % 20.87/7.60 tff(c_1263, plain, (ndr1_1(a546))). % 20.87/7.60 tff(c_1262, plain, (~c4_1(a568))). % 20.87/7.60 tff(c_1261, plain, (c2_1(a542))). % 20.87/7.60 tff(c_1258, plain, (ndr1_1(a542))). % 20.87/7.60 tff(c_1257, plain, (c2_1(a517))). % 20.87/7.60 tff(c_1256, plain, (c7_1(a596))). % 20.87/7.60 tff(c_1255, plain, (c4_1(a517))). % 20.87/7.60 tff(c_1254, plain, (ndr1_1(a570))). % 20.87/7.60 tff(c_1253, plain, (c1_1(a532))). % 20.87/7.60 tff(c_1252, plain, (ndr1_1(a512))). % 20.87/7.60 tff(c_1251, plain, (c3_1(a532))). % 20.87/7.60 tff(c_1249, plain, (~c6_1(a596))). % 20.87/7.60 tff(c_1247, plain, (~c5_1(a491))). % 20.87/7.60 tff(c_1246, plain, (c3_1(a565))). % 20.87/7.60 tff(c_1245, plain, (c5_1(a536))). % 20.87/7.60 tff(c_1244, plain, (~c4_0)). % 20.87/7.60 tff(c_1243, plain, (c4_1(a537))). % 20.87/7.60 tff(c_1240, plain, (c6_1(a552))). % 20.87/7.60 tff(c_1239, plain, (c3_1(a587))). % 20.87/7.60 tff(c_1238, plain, (~c6_1(a592))). % 20.87/7.60 tff(c_1237, plain, (c6_1(a565))). % 20.87/7.60 tff(c_1236, plain, (c7_1(a564))). % 20.87/7.60 tff(c_1235, plain, (c5_1(a564))). % 20.87/7.60 tff(c_1232, plain, (c3_1(a600))). % 20.87/7.60 tff(c_1229, plain, (c6_1(a512))). % 20.87/7.60 tff(c_1227, plain, (~c2_1(a561))). % 20.87/7.60 tff(c_1224, plain, (~c8_1(a552))). % 20.87/7.60 tff(c_1222, plain, (c4_1(a570))). % 20.87/7.60 tff(c_1221, plain, (~c4_1(a546))). % 20.87/7.60 tff(c_1220, plain, (~c1_1(a514))). % 20.87/7.60 tff(c_1213, plain, (~c4_1(a491))). % 20.87/7.60 tff(c_1212, plain, (c5_1(a570))). % 20.87/7.60 tff(c_1208, plain, (~c5_1(a561))). % 20.87/7.60 tff(c_1204, plain, (~c4_1(a468))). % 20.87/7.60 tff(c_1203, plain, (~c3_1(a468))). % 20.87/7.60 tff(c_1177, plain, (ndr1_0)). % 20.87/7.60 tff(c_1175, plain, (~c2_0)). % 20.87/7.60 tff(c_1174, plain, (~c7_0)). % 20.87/7.60 tff(c_1173, plain, (~ssSkC26)). % 20.87/7.60 tff(c_1172, plain, (c6_0)). % 20.87/7.60 tff(c_1171, plain, (~c1_0)). % 20.87/7.60 tff(c_1170, plain, (c8_0)). % 20.87/7.60 tff(c_1169, plain, (~c5_0)). % 20.87/7.60 tff(c_2, plain, (c3_0)). % 20.87/7.60 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.87/7.61 %------------------------------------------------------------------------------