%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN421-1 : TPTP v9.0.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 10:03:31 PM UTC 2025 % Result : Satisfiable 15.68s 5.09s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN421-1 : TPTP v9.0.0. Released v2.1.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.35 % Computer : n014.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Apr 9 07:23:34 EDT 2025 % 0.13/0.35 % CPUTime : % 15.68/5.09 % 15.68/5.09 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.68/5.09 % 15.68/5.09 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.68/5.10 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ssSkP9 > ssSkP8 > ssSkP7 > ssSkP6 > ssSkP5 > ssSkP4 > ssSkP3 > ssSkP2 > ssSkP10 > ssSkP1 > ssSkP0 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ssSkC9 > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC32 > ssSkC31 > ssSkC30 > ssSkC3 > ssSkC29 > ssSkC28 > ssSkC27 > ssSkC26 > ssSkC25 > ssSkC24 > ssSkC23 > ssSkC22 > ssSkC21 > ssSkC20 > ssSkC2 > ssSkC19 > ssSkC18 > ssSkC17 > ssSkC16 > ssSkC15 > ssSkC14 > ssSkC13 > ssSkC12 > ssSkC11 > ssSkC10 > ssSkC1 > ssSkC0 > ndr1_0 > c9_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > c10_0 > 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 % 15.68/5.10 % 15.68/5.10 %Foreground sorts: % 15.68/5.10 % 15.68/5.10 % 15.68/5.10 %Background operators: % 15.68/5.10 % 15.68/5.10 % 15.68/5.10 %Foreground operators: % 15.68/5.10 tff(a565, type, a565: $i). % 15.68/5.10 tff(c7_0, type, c7_0: $o). % 15.68/5.10 tff(a492, type, a492: $i). % 15.68/5.10 tff(a544, type, a544: $i). % 15.68/5.10 tff(a577, type, a577: $i). % 15.68/5.10 tff(a586, type, a586: $i). % 15.68/5.10 tff(ssSkC8, type, ssSkC8: $o). % 15.68/5.10 tff(a473, type, a473: $i). % 15.68/5.10 tff(a601, type, a601: $i). % 15.68/5.10 tff(ssSkC7, type, ssSkC7: $o). % 15.68/5.10 tff(a506, type, a506: $i). % 15.68/5.10 tff(a457, type, a457: $i). % 15.68/5.10 tff(a600, type, a600: $i). % 15.68/5.10 tff(a580, type, a580: $i). % 15.68/5.10 tff(a535, type, a535: $i). % 15.68/5.10 tff(ssSkC21, type, ssSkC21: $o). % 15.68/5.10 tff(a542, type, a542: $i). % 15.68/5.10 tff(c4_0, type, c4_0: $o). % 15.68/5.10 tff(a541, type, a541: $i). % 15.68/5.10 tff(ssSkC10, type, ssSkC10: $o). % 15.68/5.10 tff(a556, type, a556: $i). % 15.68/5.10 tff(ssSkP0, type, ssSkP0: $i > $o). % 15.68/5.10 tff(a550, type, a550: $i). % 15.68/5.10 tff(ssSkC6, type, ssSkC6: $o). % 15.68/5.10 tff(c3_0, type, c3_0: $o). % 15.68/5.10 tff(a477, type, a477: $i). % 15.68/5.10 tff(a460, type, a460: $i). % 15.68/5.10 tff(a594, type, a594: $i). % 15.68/5.10 tff(a490, type, a490: $i). % 15.68/5.10 tff(ssSkP7, type, ssSkP7: $i > $o). % 15.68/5.10 tff(a567, type, a567: $i). % 15.68/5.10 tff(a484, type, a484: $i). % 15.68/5.10 tff(c1_2, type, c1_2: ($i * $i) > $o). % 15.68/5.10 tff(ssSkC23, type, ssSkC23: $o). % 15.68/5.10 tff(ssSkC3, type, ssSkC3: $o). % 15.68/5.10 tff(a503, type, a503: $i). % 15.68/5.10 tff(a585, type, a585: $i). % 15.68/5.10 tff(a471, type, a471: $i). % 15.68/5.10 tff(a520, type, a520: $i). % 15.68/5.10 tff(a495, type, a495: $i). % 15.68/5.10 tff(a502, type, a502: $i). % 15.68/5.10 tff(a493, type, a493: $i). % 15.68/5.10 tff(ssSkP2, type, ssSkP2: $i > $o). % 15.68/5.10 tff(a537, type, a537: $i). % 15.68/5.10 tff(ssSkC19, type, ssSkC19: $o). % 15.68/5.10 tff(ssSkC28, type, ssSkC28: $o). % 15.68/5.10 tff(a511, type, a511: $i). % 15.68/5.10 tff(a454, type, a454: $i). % 15.68/5.10 tff(a564, type, a564: $i). % 15.68/5.10 tff(a508, type, a508: $i). % 15.68/5.10 tff(a510, type, a510: $i). % 15.68/5.10 tff(ssSkC26, type, ssSkC26: $o). % 15.68/5.10 tff(a487, type, a487: $i). % 15.68/5.10 tff(a488, type, a488: $i). % 15.68/5.10 tff(a530, type, a530: $i). % 15.68/5.10 tff(a553, type, a553: $i). % 15.68/5.10 tff(a569, type, a569: $i). % 15.68/5.10 tff(a449, type, a449: $i). % 15.68/5.10 tff(a528, type, a528: $i). % 15.68/5.10 tff(a462, type, a462: $i). % 15.68/5.10 tff(a458, type, a458: $i). % 15.68/5.10 tff(c8_0, type, c8_0: $o). % 15.68/5.10 tff(a536, type, a536: $i). % 15.68/5.10 tff(a459, type, a459: $i). % 15.68/5.10 tff(a467, type, a467: $i). % 15.68/5.10 tff(a461, type, a461: $i). % 15.68/5.10 tff(a596, type, a596: $i). % 15.68/5.10 tff(a498, type, a498: $i). % 15.68/5.10 tff(ssSkC4, type, ssSkC4: $o). % 15.68/5.10 tff(a505, type, a505: $i). % 15.68/5.10 tff(a456, type, a456: $i). % 15.68/5.10 tff(a532, type, a532: $i). % 15.68/5.10 tff(a504, type, a504: $i). % 15.68/5.10 tff(a468, type, a468: $i). % 15.68/5.10 tff(c5_0, type, c5_0: $o). % 15.68/5.10 tff(ssSkC9, type, ssSkC9: $o). % 15.68/5.10 tff(ssSkP6, type, ssSkP6: $i > $o). % 15.68/5.10 tff(a539, type, a539: $i). % 15.68/5.10 tff(a551, type, a551: $i). % 15.68/5.10 tff(a572, type, a572: $i). % 15.68/5.10 tff(ssSkP8, type, ssSkP8: $i > $o). % 15.68/5.10 tff(a518, type, a518: $i). % 15.68/5.10 tff(a546, type, a546: $i). % 15.68/5.10 tff(a599, type, a599: $i). % 15.68/5.10 tff(c6_0, type, c6_0: $o). % 15.68/5.10 tff(c8_2, type, c8_2: ($i * $i) > $o). % 15.68/5.10 tff(ssSkC30, type, ssSkC30: $o). % 15.68/5.10 tff(a602, type, a602: $i). % 15.68/5.10 tff(a453, type, a453: $i). % 15.68/5.10 tff(ssSkC11, type, ssSkC11: $o). % 15.68/5.10 tff(a606, type, a606: $i). % 15.68/5.10 tff(ssSkC18, type, ssSkC18: $o). % 15.68/5.10 tff(a570, type, a570: $i). % 15.68/5.10 tff(a499, type, a499: $i). % 15.68/5.10 tff(a605, type, a605: $i). % 15.68/5.10 tff(a533, type, a533: $i). % 15.68/5.10 tff(ssSkC16, type, ssSkC16: $o). % 15.68/5.10 tff(a500, type, a500: $i). % 15.68/5.10 tff(a472, type, a472: $i). % 15.68/5.10 tff(a470, type, a470: $i). % 15.68/5.10 tff(a598, type, a598: $i). % 15.68/5.10 tff(ssSkP3, type, ssSkP3: $i > $o). % 15.68/5.10 tff(a516, type, a516: $i). % 15.68/5.10 tff(a524, type, a524: $i). % 15.68/5.10 tff(ssSkC32, type, ssSkC32: $o). % 15.68/5.10 tff(a563, type, a563: $i). % 15.68/5.10 tff(ssSkC24, type, ssSkC24: $o). % 15.68/5.10 tff(a451, type, a451: $i). % 15.68/5.10 tff(a571, type, a571: $i). % 15.68/5.10 tff(a543, type, a543: $i). % 15.68/5.10 tff(a509, type, a509: $i). % 15.68/5.10 tff(ssSkC17, type, ssSkC17: $o). % 15.68/5.10 tff(ssSkP9, type, ssSkP9: $i > $o). % 15.68/5.10 tff(a589, type, a589: $i). % 15.68/5.10 tff(a558, type, a558: $i). % 15.68/5.10 tff(c1_0, type, c1_0: $o). % 15.68/5.10 tff(c8_1, type, c8_1: $i > $o). % 15.68/5.10 tff(ssSkC29, type, ssSkC29: $o). % 15.68/5.10 tff(ssSkP4, type, ssSkP4: $i > $o). % 15.68/5.10 tff(a465, type, a465: $i). % 15.68/5.10 tff(a469, type, a469: $i). % 15.68/5.10 tff(c2_1, type, c2_1: $i > $o). % 15.68/5.10 tff(a549, type, a549: $i). % 15.68/5.10 tff(a555, type, a555: $i). % 15.68/5.10 tff(ssSkC27, type, ssSkC27: $o). % 15.68/5.10 tff(ndr1_1, type, ndr1_1: $i > $o). % 15.68/5.10 tff(ssSkC15, type, ssSkC15: $o). % 15.68/5.10 tff(c2_0, type, c2_0: $o). % 15.68/5.10 tff(c4_1, type, c4_1: $i > $o). % 15.68/5.10 tff(a529, type, a529: $i). % 15.68/5.10 tff(a475, type, a475: $i). % 15.68/5.10 tff(a557, type, a557: $i). % 15.68/5.10 tff(a575, type, a575: $i). % 15.68/5.10 tff(a597, type, a597: $i). % 15.68/5.10 tff(a591, type, a591: $i). % 15.68/5.10 tff(a494, type, a494: $i). % 15.68/5.10 tff(a545, type, a545: $i). % 15.68/5.10 tff(a491, type, a491: $i). % 15.68/5.10 tff(a562, type, a562: $i). % 15.68/5.10 tff(a463, type, a463: $i). % 15.68/5.10 tff(a474, type, a474: $i). % 15.68/5.10 tff(a581, type, a581: $i). % 15.68/5.10 tff(a568, type, a568: $i). % 15.68/5.10 tff(a593, type, a593: $i). % 15.68/5.10 tff(a479, type, a479: $i). % 15.68/5.10 tff(a489, type, a489: $i). % 15.68/5.10 tff(c9_1, type, c9_1: $i > $o). % 15.68/5.10 tff(a584, type, a584: $i). % 15.68/5.10 tff(c10_1, type, c10_1: $i > $o). % 15.68/5.10 tff(c10_0, type, c10_0: $o). % 15.68/5.10 tff(a482, type, a482: $i). % 15.68/5.10 tff(a603, type, a603: $i). % 15.68/5.10 tff(ssSkC12, type, ssSkC12: $o). % 15.68/5.10 tff(a452, type, a452: $i). % 15.68/5.10 tff(c6_2, type, c6_2: ($i * $i) > $o). % 15.68/5.10 tff(a507, type, a507: $i). % 15.68/5.10 tff(a587, type, a587: $i). % 15.68/5.10 tff(a578, type, a578: $i). % 15.68/5.10 tff(a559, type, a559: $i). % 15.68/5.10 tff(a478, type, a478: $i). % 15.68/5.10 tff(a464, type, a464: $i). % 15.68/5.10 tff(ssSkC20, type, ssSkC20: $o). % 15.68/5.10 tff(a552, type, a552: $i). % 15.68/5.10 tff(a548, type, a548: $i). % 15.68/5.10 tff(a534, type, a534: $i). % 15.68/5.10 tff(a588, type, a588: $i). % 15.68/5.10 tff(a525, type, a525: $i). % 15.68/5.10 tff(a523, type, a523: $i). % 15.68/5.10 tff(a595, type, a595: $i). % 15.68/5.10 tff(a531, type, a531: $i). % 15.68/5.10 tff(a522, type, a522: $i). % 15.68/5.10 tff(a573, type, a573: $i). % 15.68/5.10 tff(ndr1_0, type, ndr1_0: $o). % 15.68/5.10 tff(a480, type, a480: $i). % 15.68/5.10 tff(a485, type, a485: $i). % 15.68/5.10 tff(a476, type, a476: $i). % 15.68/5.10 tff(a483, type, a483: $i). % 15.68/5.10 tff(a455, type, a455: $i). % 15.68/5.10 tff(a538, type, a538: $i). % 15.68/5.10 tff(a501, type, a501: $i). % 15.68/5.10 tff(ssSkC14, type, ssSkC14: $o). % 15.68/5.10 tff(a486, type, a486: $i). % 15.68/5.10 tff(c9_2, type, c9_2: ($i * $i) > $o). % 15.68/5.10 tff(a547, type, a547: $i). % 15.68/5.10 tff(a450, type, a450: $i). % 15.68/5.10 tff(c10_2, type, c10_2: ($i * $i) > $o). % 15.68/5.10 tff(a527, type, a527: $i). % 15.68/5.10 tff(a526, type, a526: $i). % 15.68/5.10 tff(a576, type, a576: $i). % 15.68/5.10 tff(a561, type, a561: $i). % 15.68/5.10 tff(a481, type, a481: $i). % 15.68/5.10 tff(c1_1, type, c1_1: $i > $o). % 15.68/5.10 tff(a497, type, a497: $i). % 15.68/5.10 tff(a607, type, a607: $i). % 15.68/5.10 tff(a521, type, a521: $i). % 15.68/5.10 tff(ssSkC13, type, ssSkC13: $o). % 15.68/5.10 tff(ssSkC25, type, ssSkC25: $o). % 15.68/5.10 tff(ssSkC2, type, ssSkC2: $o). % 15.68/5.10 tff(c5_2, type, c5_2: ($i * $i) > $o). % 15.68/5.10 tff(ssSkC31, type, ssSkC31: $o). % 15.68/5.10 tff(a496, type, a496: $i). % 15.68/5.10 tff(a540, type, a540: $i). % 15.68/5.10 tff(c9_0, type, c9_0: $o). % 15.68/5.10 tff(a519, type, a519: $i). % 15.68/5.10 tff(c7_1, type, c7_1: $i > $o). % 15.68/5.10 tff(c6_1, type, c6_1: $i > $o). % 15.68/5.10 tff(ssSkC22, type, ssSkC22: $o). % 15.68/5.10 tff(a590, type, a590: $i). % 15.68/5.10 tff(c4_2, type, c4_2: ($i * $i) > $o). % 15.68/5.10 tff(a517, type, a517: $i). % 15.68/5.10 tff(a560, type, a560: $i). % 15.68/5.10 tff(a582, type, a582: $i). % 15.68/5.10 tff(ssSkC1, type, ssSkC1: $o). % 15.68/5.10 tff(a566, type, a566: $i). % 15.68/5.10 tff(ssSkP5, type, ssSkP5: $i > $o). % 15.68/5.10 tff(a554, type, a554: $i). % 15.68/5.10 tff(ssSkC0, type, ssSkC0: $o). % 15.68/5.10 tff(a515, type, a515: $i). % 15.68/5.10 tff(ssSkC5, type, ssSkC5: $o). % 15.68/5.10 tff(ssSkP1, type, ssSkP1: $i > $o). % 15.68/5.10 tff(c5_1, type, c5_1: $i > $o). % 15.68/5.10 tff(c7_2, type, c7_2: ($i * $i) > $o). % 15.68/5.10 tff(a583, type, a583: $i). % 15.68/5.10 tff(c3_2, type, c3_2: ($i * $i) > $o). % 15.68/5.10 tff(a514, type, a514: $i). % 15.68/5.10 tff(a466, type, a466: $i). % 15.68/5.10 tff(c2_2, type, c2_2: ($i * $i) > $o). % 15.68/5.10 tff(a604, type, a604: $i). % 15.68/5.10 tff(a513, type, a513: $i). % 15.68/5.10 tff(a512, type, a512: $i). % 15.68/5.10 tff(a574, type, a574: $i). % 15.68/5.10 tff(a592, type, a592: $i). % 15.68/5.10 tff(ssSkP10, type, ssSkP10: $i > $o). % 15.68/5.10 tff(c3_1, type, c3_1: $i > $o). % 15.68/5.10 tff(a579, type, a579: $i). % 15.68/5.10 % 15.68/5.10 %Saturated clause set: % 15.68/5.11 tff(c_4732, plain, (![U_620]: (c3_2(U_620, a553) | c1_2(U_620, a498) | ~c1_2(U_620, a553) | ~c6_2(U_620, a553) | ~ssSkP3(U_620) | ~c1_2(U_620, a474) | c3_2(U_620, a506) | ~c7_2(U_620, a506) | ~c8_1(U_620) | ~c5_2(U_620, a506) | c1_1(U_620) | c2_2(U_620, a589) | ~c5_2(U_620, a589) | c7_1(U_620) | ~c6_1(U_620) | ~ndr1_1(U_620) | c9_1(U_620) | c10_1(U_620)))). % 15.68/5.11 tff(c_4731, plain, (![U_620]: (c3_2(U_620, a553) | c10_2(U_620, a498) | ~c1_2(U_620, a553) | ~c6_2(U_620, a553) | ~ssSkP3(U_620) | ~c1_2(U_620, a474) | c3_2(U_620, a506) | ~c7_2(U_620, a506) | ~c8_1(U_620) | ~c5_2(U_620, a506) | c1_1(U_620) | c2_2(U_620, a589) | ~c5_2(U_620, a589) | c7_1(U_620) | ~c6_1(U_620) | ~ndr1_1(U_620) | c9_1(U_620) | c10_1(U_620)))). % 15.68/5.11 tff(c_4715, plain, (![U_619]: (c3_2(U_619, a553) | c10_2(U_619, a498) | ~c1_2(U_619, a553) | ~c6_2(U_619, a553) | ~ssSkP3(U_619) | c10_1(U_619) | ~c1_2(U_619, a529) | c7_1(U_619) | c3_2(U_619, a506) | ~c6_1(U_619) | ~c7_2(U_619, a506) | ~c8_1(U_619) | ~c5_2(U_619, a506) | c1_1(U_619) | c2_2(U_619, a589) | ~ndr1_1(U_619) | ~c5_2(U_619, a589) | ssSkP6(U_619)))). % 15.68/5.11 tff(c_4700, plain, (![U_618]: (c3_2(U_618, a553) | c1_2(U_618, a498) | ~c1_2(U_618, a553) | ~c6_2(U_618, a553) | ~ssSkP3(U_618) | c10_1(U_618) | ~c1_2(U_618, a507) | c7_1(U_618) | c3_2(U_618, a506) | ~c6_1(U_618) | ~c7_2(U_618, a506) | ~c8_1(U_618) | ~c5_2(U_618, a506) | c1_1(U_618) | c2_2(U_618, a589) | ~ndr1_1(U_618) | ~c5_2(U_618, a589) | ssSkP4(U_618)))). % 15.68/5.11 tff(c_4699, plain, (![U_618]: (c3_2(U_618, a553) | c10_2(U_618, a498) | ~c1_2(U_618, a553) | ~c6_2(U_618, a553) | ~ssSkP3(U_618) | c10_1(U_618) | ~c1_2(U_618, a507) | c7_1(U_618) | c3_2(U_618, a506) | ~c6_1(U_618) | ~c7_2(U_618, a506) | ~c8_1(U_618) | ~c5_2(U_618, a506) | c1_1(U_618) | c2_2(U_618, a589) | ~ndr1_1(U_618) | ~c5_2(U_618, a589) | ssSkP4(U_618)))). % 15.68/5.11 tff(c_5854, plain, (![U_623]: (c3_2(U_623, a553) | c3_2(U_623, a506) | ~c7_2(U_623, a506) | ~c8_1(U_623) | ~c5_2(U_623, a506) | c7_1(U_623) | c3_2(U_623, a567) | ~c6_1(U_623) | c10_2(U_623, a498) | ~c1_2(U_623, a567) | ~ssSkP3(U_623) | c1_1(U_623) | c2_2(U_623, a567) | ~ndr1_1(U_623) | ~c5_2(U_623, a567) | ssSkP10(U_623)))). % 15.68/5.11 tff(c_4716, plain, (![U_619]: (c3_2(U_619, a553) | c1_2(U_619, a498) | ~c1_2(U_619, a553) | ~c6_2(U_619, a553) | ~ssSkP3(U_619) | c10_1(U_619) | ~c1_2(U_619, a529) | c7_1(U_619) | c3_2(U_619, a506) | ~c6_1(U_619) | ~c7_2(U_619, a506) | ~c8_1(U_619) | ~c5_2(U_619, a506) | c1_1(U_619) | c2_2(U_619, a589) | ~ndr1_1(U_619) | ~c5_2(U_619, a589) | ssSkP6(U_619)))). % 15.68/5.11 tff(c_4730, plain, (![U_620, V_568]: (c3_2(U_620, a553) | c2_2(U_620, V_568) | c7_2(U_620, V_568) | ~c5_2(U_620, V_568) | ~c1_2(U_620, a474) | c3_2(U_620, a506) | ~c7_2(U_620, a506) | ~c8_1(U_620) | ~c5_2(U_620, a506) | c1_1(U_620) | c2_2(U_620, a589) | ~c5_2(U_620, a589) | c7_1(U_620) | ~c6_1(U_620) | ~ndr1_1(U_620) | c9_1(U_620) | c10_1(U_620)))). % 15.68/5.11 tff(c_4714, plain, (![U_619, V_568]: (c3_2(U_619, a553) | c2_2(U_619, V_568) | c7_2(U_619, V_568) | ~c5_2(U_619, V_568) | c10_1(U_619) | ~c1_2(U_619, a529) | c7_1(U_619) | c3_2(U_619, a506) | ~c6_1(U_619) | ~c7_2(U_619, a506) | ~c8_1(U_619) | ~c5_2(U_619, a506) | c1_1(U_619) | c2_2(U_619, a589) | ~ndr1_1(U_619) | ~c5_2(U_619, a589) | ssSkP6(U_619)))). % 15.68/5.11 tff(c_5652, plain, (![U_596]: (c3_2(U_596, a553) | c3_2(U_596, a506) | ~c7_2(U_596, a506) | c7_1(U_596) | c3_2(U_596, a567) | ~c6_1(U_596) | c1_2(U_596, a498) | ~c1_2(U_596, a567) | ~ssSkP3(U_596) | ~c8_1(U_596) | ~c5_2(U_596, a506) | c1_1(U_596) | c2_2(U_596, a567) | ~ndr1_1(U_596) | ~c5_2(U_596, a567) | ssSkP10(U_596)))). % 15.68/5.11 tff(c_4698, plain, (![U_618, V_568]: (c3_2(U_618, a553) | c2_2(U_618, V_568) | c7_2(U_618, V_568) | ~c5_2(U_618, V_568) | c10_1(U_618) | ~c1_2(U_618, a507) | c7_1(U_618) | c3_2(U_618, a506) | ~c6_1(U_618) | ~c7_2(U_618, a506) | ~c8_1(U_618) | ~c5_2(U_618, a506) | c1_1(U_618) | c2_2(U_618, a589) | ~ndr1_1(U_618) | ~c5_2(U_618, a589) | ssSkP4(U_618)))). % 15.68/5.11 tff(c_4733, plain, (![U_620]: (~c10_2(U_620, a568) | ~c1_2(U_620, a553) | ~c5_2(U_620, a553) | ~ssSkP10(U_620) | ~c1_2(U_620, a474) | c3_2(U_620, a506) | ~c7_2(U_620, a506) | ~c8_1(U_620) | ~c5_2(U_620, a506) | c1_1(U_620) | c2_2(U_620, a589) | ~c5_2(U_620, a589) | c7_1(U_620) | ~c6_1(U_620) | ~ndr1_1(U_620) | c9_1(U_620) | c10_1(U_620)))). % 15.68/5.11 tff(c_4717, plain, (![U_619]: (~c10_2(U_619, a568) | ~c1_2(U_619, a553) | ~c5_2(U_619, a553) | ~ssSkP10(U_619) | c10_1(U_619) | ~c1_2(U_619, a529) | c7_1(U_619) | c3_2(U_619, a506) | ~c6_1(U_619) | ~c7_2(U_619, a506) | ~c8_1(U_619) | ~c5_2(U_619, a506) | c1_1(U_619) | c2_2(U_619, a589) | ~ndr1_1(U_619) | ~c5_2(U_619, a589) | ssSkP6(U_619)))). % 15.68/5.11 tff(c_4264, plain, (![U_587, V_588]: (c3_2(U_587, V_588) | c10_2(U_587, a498) | ~c1_2(U_587, V_588) | ~c6_2(U_587, V_588) | ~ssSkP3(U_587) | c7_1(U_587) | c3_2(U_587, a506) | ~c6_1(U_587) | ~c7_2(U_587, a506) | c7_2(U_587, a553) | ~c8_1(U_587) | ~c5_2(U_587, a506) | c1_1(U_587) | c2_2(U_587, V_588) | ~ndr1_1(U_587) | ~c5_2(U_587, V_588)))). % 15.68/5.11 tff(c_4265, plain, (![U_587, V_588]: (c3_2(U_587, V_588) | c1_2(U_587, a498) | ~c1_2(U_587, V_588) | ~c6_2(U_587, V_588) | ~ssSkP3(U_587) | c7_1(U_587) | c3_2(U_587, a506) | ~c6_1(U_587) | ~c7_2(U_587, a506) | c7_2(U_587, a553) | ~c8_1(U_587) | ~c5_2(U_587, a506) | c1_1(U_587) | c2_2(U_587, V_588) | ~ndr1_1(U_587) | ~c5_2(U_587, V_588)))). % 15.83/5.11 tff(c_4262, plain, (![U_587, V_588]: (c3_2(U_587, a553) | c1_2(U_587, a498) | ~c1_2(U_587, a553) | ~c6_2(U_587, a553) | ~ssSkP3(U_587) | c7_1(U_587) | c3_2(U_587, a506) | ~c6_1(U_587) | ~c7_2(U_587, a506) | ~c8_1(U_587) | ~c5_2(U_587, a506) | c1_1(U_587) | c2_2(U_587, V_588) | c7_2(U_587, V_588) | ~ndr1_1(U_587) | ~c5_2(U_587, V_588)))). % 15.83/5.11 tff(c_3968, plain, (![U_567, V_568]: (c3_2(U_567, V_568) | c1_2(U_567, a498) | ~c1_2(U_567, V_568) | ~c6_2(U_567, V_568) | ~ssSkP3(U_567) | c7_1(U_567) | c3_2(U_567, a553) | ~c6_1(U_567) | ~c7_2(U_567, a553) | c8_2(U_567, a506) | ~c8_1(U_567) | ~c5_2(U_567, a506) | c1_1(U_567) | c2_2(U_567, V_568) | ~ndr1_1(U_567) | ~c5_2(U_567, V_568)))). % 15.83/5.11 tff(c_4261, plain, (![U_587, V_588]: (c3_2(U_587, a553) | c10_2(U_587, a498) | ~c1_2(U_587, a553) | ~c6_2(U_587, a553) | ~ssSkP3(U_587) | c7_1(U_587) | c3_2(U_587, a506) | ~c6_1(U_587) | ~c7_2(U_587, a506) | ~c8_1(U_587) | ~c5_2(U_587, a506) | c1_1(U_587) | c2_2(U_587, V_588) | c7_2(U_587, V_588) | ~ndr1_1(U_587) | ~c5_2(U_587, V_588)))). % 15.83/5.11 tff(c_4701, plain, (![U_618]: (~c10_2(U_618, a568) | ~c1_2(U_618, a553) | ~c5_2(U_618, a553) | ~ssSkP10(U_618) | c10_1(U_618) | ~c1_2(U_618, a507) | c7_1(U_618) | c3_2(U_618, a506) | ~c6_1(U_618) | ~c7_2(U_618, a506) | ~c8_1(U_618) | ~c5_2(U_618, a506) | c1_1(U_618) | c2_2(U_618, a589) | ~ndr1_1(U_618) | ~c5_2(U_618, a589) | ssSkP4(U_618)))). % 15.83/5.11 tff(c_4817, plain, (![U_627]: (c3_2(U_627, a506) | ~c7_2(U_627, a506) | c10_2(U_627, a553) | ~c8_1(U_627) | ~c5_2(U_627, a506) | c7_1(U_627) | c3_2(U_627, a567) | ~c6_1(U_627) | c1_2(U_627, a498) | ~c1_2(U_627, a567) | ~ssSkP3(U_627) | c1_1(U_627) | c2_2(U_627, a567) | ~ndr1_1(U_627) | ~c5_2(U_627, a567) | ssSkP10(U_627)))). % 15.83/5.11 tff(c_3967, plain, (![U_567, V_568]: (c3_2(U_567, V_568) | c10_2(U_567, a498) | ~c1_2(U_567, V_568) | ~c6_2(U_567, V_568) | ~ssSkP3(U_567) | c7_1(U_567) | c3_2(U_567, a553) | ~c6_1(U_567) | ~c7_2(U_567, a553) | c8_2(U_567, a506) | ~c8_1(U_567) | ~c5_2(U_567, a506) | c1_1(U_567) | c2_2(U_567, V_568) | ~ndr1_1(U_567) | ~c5_2(U_567, V_568)))). % 15.83/5.11 tff(c_4779, plain, (![U_624]: (c3_2(U_624, a506) | ~c7_2(U_624, a506) | c10_2(U_624, a553) | ~c8_1(U_624) | ~c5_2(U_624, a506) | c7_1(U_624) | c3_2(U_624, a567) | ~c6_1(U_624) | c10_2(U_624, a498) | ~c1_2(U_624, a567) | ~ssSkP3(U_624) | c1_1(U_624) | c2_2(U_624, a567) | ~ndr1_1(U_624) | ~c5_2(U_624, a567) | ssSkP10(U_624)))). % 15.83/5.11 tff(c_4767, plain, (![U_623]: (c3_2(U_623, a506) | ~c7_2(U_623, a506) | c7_2(U_623, a553) | ~c8_1(U_623) | ~c5_2(U_623, a506) | c7_1(U_623) | c3_2(U_623, a567) | ~c6_1(U_623) | c10_2(U_623, a498) | ~c1_2(U_623, a567) | ~ssSkP3(U_623) | c1_1(U_623) | c2_2(U_623, a567) | ~ndr1_1(U_623) | ~c5_2(U_623, a567) | ssSkP10(U_623)))). % 15.83/5.11 tff(c_4282, plain, (![U_589]: (c3_2(U_589, a553) | ~c7_2(U_589, a553) | c8_2(U_589, a506) | ~c8_1(U_589) | ~c5_2(U_589, a506) | c7_1(U_589) | c3_2(U_589, a567) | ~c6_1(U_589) | c10_2(U_589, a498) | ~c1_2(U_589, a567) | ~ssSkP3(U_589) | c1_1(U_589) | c2_2(U_589, a567) | ~ndr1_1(U_589) | ~c5_2(U_589, a567) | ssSkP10(U_589)))). % 15.83/5.12 tff(c_4433, plain, (![U_538, V_599, V_539]: (c3_2(U_538, a553) | c2_2(U_538, V_599) | c7_2(U_538, V_599) | ~c5_2(U_538, V_599) | c7_1(U_538) | c3_2(U_538, a506) | ~c6_1(U_538) | ~c7_2(U_538, a506) | ~c8_1(U_538) | ~c5_2(U_538, a506) | c1_1(U_538) | c2_2(U_538, V_539) | c7_2(U_538, V_539) | ~ndr1_1(U_538) | ~c5_2(U_538, V_539)))). % 15.83/5.12 tff(c_4294, plain, (![U_590]: (c3_2(U_590, a553) | c1_2(U_590, a498) | ~c1_2(U_590, a553) | ~c6_2(U_590, a553) | ~ssSkP3(U_590) | c7_1(U_590) | c3_2(U_590, a506) | ~c6_1(U_590) | ~c7_2(U_590, a506) | ~c8_1(U_590) | ~c5_2(U_590, a506) | c1_1(U_590) | c2_2(U_590, a553) | ~ndr1_1(U_590) | ~c5_2(U_590, a553)))). % 15.83/5.12 tff(c_4374, plain, (![U_596]: (c3_2(U_596, a506) | ~c7_2(U_596, a506) | c7_1(U_596) | c3_2(U_596, a567) | ~c6_1(U_596) | c1_2(U_596, a498) | ~c1_2(U_596, a567) | ~ssSkP3(U_596) | c7_2(U_596, a553) | ~c8_1(U_596) | ~c5_2(U_596, a506) | c1_1(U_596) | c2_2(U_596, a567) | ~ndr1_1(U_596) | ~c5_2(U_596, a567) | ssSkP10(U_596)))). % 15.83/5.12 tff(c_4293, plain, (![U_590]: (c3_2(U_590, a553) | c10_2(U_590, a498) | ~c1_2(U_590, a553) | ~c6_2(U_590, a553) | ~ssSkP3(U_590) | c7_1(U_590) | c3_2(U_590, a506) | ~c6_1(U_590) | ~c7_2(U_590, a506) | ~c8_1(U_590) | ~c5_2(U_590, a506) | c1_1(U_590) | c2_2(U_590, a553) | ~ndr1_1(U_590) | ~c5_2(U_590, a553)))). % 15.83/5.12 tff(c_4263, plain, (![U_587, V_588]: (~c10_2(U_587, a568) | ~c1_2(U_587, a553) | ~c5_2(U_587, a553) | ~ssSkP10(U_587) | c7_1(U_587) | c3_2(U_587, a506) | ~c6_1(U_587) | ~c7_2(U_587, a506) | ~c8_1(U_587) | ~c5_2(U_587, a506) | c1_1(U_587) | c2_2(U_587, V_588) | c7_2(U_587, V_588) | ~ndr1_1(U_587) | ~c5_2(U_587, V_588)))). % 15.83/5.12 tff(c_3541, plain, (![U_538, V_539]: (c7_1(U_538) | c3_2(U_538, V_539) | ~c6_1(U_538) | c10_2(U_538, a498) | ~c1_2(U_538, V_539) | ~c6_2(U_538, V_539) | ~ssSkP3(U_538) | c7_2(U_538, a553) | c8_2(U_538, a506) | ~c8_1(U_538) | ~c5_2(U_538, a506) | c1_1(U_538) | c2_2(U_538, V_539) | ~ndr1_1(U_538) | ~c5_2(U_538, V_539)))). % 15.83/5.12 tff(c_3507, plain, (![U_535, V_536]: (c7_1(U_535) | c3_2(U_535, V_536) | ~c6_1(U_535) | c1_2(U_535, a498) | ~c1_2(U_535, V_536) | ~c6_2(U_535, V_536) | ~ssSkP3(U_535) | c10_2(U_535, a553) | c8_2(U_535, a506) | ~c8_1(U_535) | ~c5_2(U_535, a506) | c1_1(U_535) | c2_2(U_535, V_536) | ~ndr1_1(U_535) | ~c5_2(U_535, V_536)))). % 15.83/5.12 tff(c_5045, plain, (![U_558]: (c3_2(U_558, a553) | c7_1(U_558) | c3_2(U_558, a506) | ~c6_1(U_558) | ~c7_2(U_558, a506) | ~c8_1(U_558) | ~c5_2(U_558, a506) | ~c10_2(U_558, a568) | ~c1_2(U_558, a542) | ~ssSkP10(U_558) | c1_1(U_558) | c2_2(U_558, a542) | ~ndr1_1(U_558) | ssSkP8(U_558)))). % 15.83/5.12 tff(c_4555, plain, (![U_607]: (~c1_2(U_607, a553) | ~c5_2(U_607, a553) | c7_1(U_607) | c3_2(U_607, a506) | ~c6_1(U_607) | ~c7_2(U_607, a506) | ~c8_1(U_607) | ~c5_2(U_607, a506) | ~c10_2(U_607, a568) | ~c1_2(U_607, a542) | ~ssSkP10(U_607) | c1_1(U_607) | c2_2(U_607, a542) | ~ndr1_1(U_607) | ssSkP8(U_607)))). % 15.83/5.12 tff(c_4919, plain, (![U_553]: (c3_2(U_553, a553) | c7_1(U_553) | c3_2(U_553, a506) | ~c6_1(U_553) | ~c7_2(U_553, a506) | ~c10_2(U_553, a568) | ~c1_2(U_553, a531) | ~ssSkP10(U_553) | ~c8_1(U_553) | ~c5_2(U_553, a506) | c1_1(U_553) | c2_2(U_553, a531) | ~ndr1_1(U_553) | ssSkP7(U_553)))). % 15.83/5.12 tff(c_4527, plain, (![U_605]: (c3_2(U_605, a553) | ~c7_2(U_605, a553) | c7_1(U_605) | c3_2(U_605, a567) | ~c6_1(U_605) | c1_2(U_605, a498) | ~c1_2(U_605, a567) | ~ssSkP3(U_605) | c8_2(U_605, a506) | ~c8_1(U_605) | ~c5_2(U_605, a506) | c1_1(U_605) | c2_2(U_605, a567) | ~ndr1_1(U_605) | ~c5_2(U_605, a567) | ssSkP10(U_605)))). % 15.83/5.12 tff(c_4083, plain, (![U_577]: (~c1_2(U_577, a553) | ~c5_2(U_577, a553) | c7_1(U_577) | c3_2(U_577, a506) | ~c6_1(U_577) | ~c7_2(U_577, a506) | ~c10_2(U_577, a568) | ~c1_2(U_577, a531) | ~ssSkP10(U_577) | ~c8_1(U_577) | ~c5_2(U_577, a506) | c1_1(U_577) | c2_2(U_577, a531) | ~ndr1_1(U_577) | ssSkP7(U_577)))). % 15.83/5.12 tff(c_4029, plain, (![U_573]: (c10_2(U_573, a553) | c8_2(U_573, a506) | ~c8_1(U_573) | ~c5_2(U_573, a506) | c7_1(U_573) | c3_2(U_573, a567) | ~c6_1(U_573) | c1_2(U_573, a498) | ~c1_2(U_573, a567) | ~ssSkP3(U_573) | c1_1(U_573) | c2_2(U_573, a567) | ~ndr1_1(U_573) | ~c5_2(U_573, a567) | ssSkP10(U_573)))). % 15.83/5.12 tff(c_3506, plain, (![U_535, V_536]: (c7_1(U_535) | c3_2(U_535, V_536) | ~c6_1(U_535) | c10_2(U_535, a498) | ~c1_2(U_535, V_536) | ~c6_2(U_535, V_536) | ~ssSkP3(U_535) | c10_2(U_535, a553) | c8_2(U_535, a506) | ~c8_1(U_535) | ~c5_2(U_535, a506) | c1_1(U_535) | c2_2(U_535, V_536) | ~ndr1_1(U_535) | ~c5_2(U_535, V_536)))). % 15.83/5.12 tff(c_4123, plain, (![U_580]: (c10_2(U_580, a553) | c8_2(U_580, a506) | ~c8_1(U_580) | ~c5_2(U_580, a506) | c7_1(U_580) | c3_2(U_580, a567) | ~c6_1(U_580) | c10_2(U_580, a498) | ~c1_2(U_580, a567) | ~ssSkP3(U_580) | c1_1(U_580) | c2_2(U_580, a567) | ~ndr1_1(U_580) | ~c5_2(U_580, a567) | ssSkP10(U_580)))). % 15.83/5.12 tff(c_4122, plain, (![U_580]: (c7_2(U_580, a553) | c8_2(U_580, a506) | ~c8_1(U_580) | ~c5_2(U_580, a506) | c7_1(U_580) | c3_2(U_580, a567) | ~c6_1(U_580) | c10_2(U_580, a498) | ~c1_2(U_580, a567) | ~ssSkP3(U_580) | c1_1(U_580) | c2_2(U_580, a567) | ~ndr1_1(U_580) | ~c5_2(U_580, a567) | ssSkP10(U_580)))). % 15.83/5.12 tff(c_4432, plain, (![U_538, V_599]: (c3_2(U_538, a553) | c2_2(U_538, V_599) | c7_2(U_538, V_599) | ~c5_2(U_538, V_599) | c7_1(U_538) | c3_2(U_538, a506) | ~c6_1(U_538) | ~c7_2(U_538, a506) | ~c8_1(U_538) | ~c5_2(U_538, a506) | c1_1(U_538) | c2_2(U_538, a553) | ~ndr1_1(U_538) | ~c5_2(U_538, a553)))). % 15.83/5.12 tff(c_4674, plain, (![U_63]: (~c1_2(U_63, a474) | c3_2(U_63, a506) | ~c7_2(U_63, a506) | c7_2(U_63, a553) | ~c8_1(U_63) | ~c5_2(U_63, a506) | c1_1(U_63) | c2_2(U_63, a589) | ~c5_2(U_63, a589) | c7_1(U_63) | ~c6_1(U_63) | ~ndr1_1(U_63) | c9_1(U_63) | c10_1(U_63)))). % 15.83/5.12 tff(c_4679, plain, (![U_16]: (c10_1(U_16) | ~c1_2(U_16, a529) | c7_1(U_16) | c3_2(U_16, a506) | ~c6_1(U_16) | ~c7_2(U_16, a506) | c7_2(U_16, a553) | ~c8_1(U_16) | ~c5_2(U_16, a506) | c1_1(U_16) | c2_2(U_16, a589) | ~ndr1_1(U_16) | ~c5_2(U_16, a589) | ssSkP6(U_16)))). % 15.83/5.12 tff(c_4678, plain, (![U_21]: (c10_1(U_21) | ~c1_2(U_21, a507) | c7_1(U_21) | c3_2(U_21, a506) | ~c6_1(U_21) | ~c7_2(U_21, a506) | c7_2(U_21, a553) | ~c8_1(U_21) | ~c5_2(U_21, a506) | c1_1(U_21) | c2_2(U_21, a589) | ~ndr1_1(U_21) | ~c5_2(U_21, a589) | ssSkP4(U_21)))). % 15.83/5.12 tff(c_4267, plain, (![U_587, V_184]: (c10_1(U_587) | ~c3_2(U_587, V_184) | ~c1_2(U_587, V_184) | c7_1(U_587) | c3_2(U_587, a506) | ~c6_1(U_587) | ~c7_2(U_587, a506) | c7_2(U_587, a553) | ~c8_1(U_587) | ~c5_2(U_587, a506) | c1_1(U_587) | c2_2(U_587, a589) | ~ndr1_1(U_587) | ~c5_2(U_587, a589)))). % 15.83/5.12 tff(c_4266, plain, (![U_587, V_588]: (~c10_2(U_587, a568) | ~c1_2(U_587, V_588) | ~ssSkP10(U_587) | c7_1(U_587) | c3_2(U_587, a506) | ~c6_1(U_587) | ~c7_2(U_587, a506) | c7_2(U_587, a553) | ~c8_1(U_587) | ~c5_2(U_587, a506) | c1_1(U_587) | c2_2(U_587, V_588) | ~ndr1_1(U_587) | ~c5_2(U_587, V_588)))). % 15.83/5.12 tff(c_3574, plain, (![U_540, V_541]: (c7_1(U_540) | c3_2(U_540, V_541) | ~c6_1(U_540) | c10_2(U_540, a498) | ~c1_2(U_540, V_541) | ~c6_2(U_540, V_541) | ~ssSkP3(U_540) | c8_2(U_540, a553) | c8_2(U_540, a506) | ~c8_1(U_540) | ~c5_2(U_540, a506) | c1_1(U_540) | c2_2(U_540, V_541) | ~ndr1_1(U_540) | ~c5_2(U_540, V_541)))). % 15.83/5.12 tff(c_3969, plain, (![U_567, V_568]: (~c10_2(U_567, a568) | ~c1_2(U_567, V_568) | ~ssSkP10(U_567) | c7_1(U_567) | c3_2(U_567, a553) | ~c6_1(U_567) | ~c7_2(U_567, a553) | c8_2(U_567, a506) | ~c8_1(U_567) | ~c5_2(U_567, a506) | c1_1(U_567) | c2_2(U_567, V_568) | ~ndr1_1(U_567) | ~c5_2(U_567, V_568)))). % 15.83/5.12 tff(c_3845, plain, (![U_561]: (c7_1(U_561) | c3_2(U_561, a553) | ~c6_1(U_561) | ~c7_2(U_561, a553) | c8_2(U_561, a506) | ~c8_1(U_561) | ~c5_2(U_561, a506) | ~c10_2(U_561, a568) | ~c1_2(U_561, a542) | ~ssSkP10(U_561) | c1_1(U_561) | c2_2(U_561, a542) | ~ndr1_1(U_561) | ssSkP8(U_561)))). % 15.83/5.12 tff(c_3792, plain, (![U_556]: (c7_1(U_556) | c3_2(U_556, a506) | ~c6_1(U_556) | ~c7_2(U_556, a506) | c10_2(U_556, a553) | ~c8_1(U_556) | ~c5_2(U_556, a506) | ~c10_2(U_556, a568) | ~c1_2(U_556, a542) | ~ssSkP10(U_556) | c1_1(U_556) | c2_2(U_556, a542) | ~ndr1_1(U_556) | ssSkP8(U_556)))). % 15.83/5.12 tff(c_3816, plain, (![U_558]: (c7_1(U_558) | c3_2(U_558, a506) | ~c6_1(U_558) | ~c7_2(U_558, a506) | c7_2(U_558, a553) | ~c8_1(U_558) | ~c5_2(U_558, a506) | ~c10_2(U_558, a568) | ~c1_2(U_558, a542) | ~ssSkP10(U_558) | c1_1(U_558) | c2_2(U_558, a542) | ~ndr1_1(U_558) | ssSkP8(U_558)))). % 15.83/5.12 tff(c_3857, plain, (![U_562]: (c7_1(U_562) | c3_2(U_562, a553) | ~c6_1(U_562) | ~c7_2(U_562, a553) | c8_2(U_562, a506) | ~c8_1(U_562) | ~c5_2(U_562, a506) | ~c10_2(U_562, a568) | ~c1_2(U_562, a531) | ~ssSkP10(U_562) | c1_1(U_562) | c2_2(U_562, a531) | ~ndr1_1(U_562) | ssSkP7(U_562)))). % 15.83/5.12 tff(c_4463, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c1_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c8_2(U_12, a553) | c8_2(U_12, a506) | ~c8_1(U_12) | ~c5_2(U_12, a506) | c1_1(U_12) | c2_2(U_12, a567) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.12 tff(c_3896, plain, (![U_215]: (~c10_2(U_215, a568) | ~c1_2(U_215, a553) | ~c5_2(U_215, a553) | ~ssSkP10(U_215) | c7_1(U_215) | c3_2(U_215, a452) | ~c6_1(U_215) | ~c8_1(U_215) | ssSkP1(U_215) | c1_1(U_215) | c2_2(U_215, a452) | ~c3_2(U_215, a506) | ~ndr1_1(U_215) | ~c5_2(U_215, a452)))). % 15.83/5.12 tff(c_3897, plain, (![U_187]: (~c10_2(U_187, a568) | ~c1_2(U_187, a553) | ~c5_2(U_187, a553) | ~ssSkP10(U_187) | c7_1(U_187) | c3_2(U_187, a452) | ~c6_1(U_187) | ~c8_1(U_187) | ssSkP1(U_187) | c1_1(U_187) | c10_2(U_187, a506) | c2_2(U_187, a452) | ~ndr1_1(U_187) | ~c5_2(U_187, a452)))). % 15.83/5.12 tff(c_3804, plain, (![U_557]: (c7_1(U_557) | c3_2(U_557, a506) | ~c6_1(U_557) | ~c7_2(U_557, a506) | c10_2(U_557, a553) | ~c8_1(U_557) | ~c5_2(U_557, a506) | ~c10_2(U_557, a568) | ~c1_2(U_557, a531) | ~ssSkP10(U_557) | c1_1(U_557) | c2_2(U_557, a531) | ~ndr1_1(U_557) | ssSkP7(U_557)))). % 15.83/5.12 tff(c_3575, plain, (![U_540, V_541]: (c7_1(U_540) | c3_2(U_540, V_541) | ~c6_1(U_540) | c1_2(U_540, a498) | ~c1_2(U_540, V_541) | ~c6_2(U_540, V_541) | ~ssSkP3(U_540) | c8_2(U_540, a553) | c8_2(U_540, a506) | ~c8_1(U_540) | ~c5_2(U_540, a506) | c1_1(U_540) | c2_2(U_540, V_541) | ~ndr1_1(U_540) | ~c5_2(U_540, V_541)))). % 15.83/5.12 tff(c_3966, plain, (![U_567, V_568]: (c3_2(U_567, a506) | ~c7_2(U_567, a506) | c7_1(U_567) | c3_2(U_567, a553) | ~c6_1(U_567) | ~c7_2(U_567, a553) | ~c8_1(U_567) | ~c5_2(U_567, a506) | c1_1(U_567) | c2_2(U_567, V_568) | c7_2(U_567, V_568) | ~ndr1_1(U_567) | ~c5_2(U_567, V_568)))). % 15.83/5.12 tff(c_4295, plain, (![U_590]: (~c10_2(U_590, a568) | ~c1_2(U_590, a553) | ~ssSkP10(U_590) | c7_1(U_590) | c3_2(U_590, a506) | ~c6_1(U_590) | ~c7_2(U_590, a506) | ~c8_1(U_590) | ~c5_2(U_590, a506) | c1_1(U_590) | c2_2(U_590, a553) | ~ndr1_1(U_590) | ~c5_2(U_590, a553)))). % 15.83/5.13 tff(c_4357, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c1_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c7_2(U_12, a553) | c8_2(U_12, a506) | ~c8_1(U_12) | ~c5_2(U_12, a506) | c1_1(U_12) | c2_2(U_12, a567) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.13 tff(c_3542, plain, (![U_538, V_539]: (c7_1(U_538) | c3_2(U_538, V_539) | ~c6_1(U_538) | c1_2(U_538, a498) | ~c1_2(U_538, V_539) | ~c6_2(U_538, V_539) | ~ssSkP3(U_538) | c7_2(U_538, a553) | c8_2(U_538, a506) | ~c8_1(U_538) | ~c5_2(U_538, a506) | c1_1(U_538) | c2_2(U_538, V_539) | ~ndr1_1(U_538) | ~c5_2(U_538, V_539)))). % 15.83/5.13 tff(c_4322, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c1_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c1_1(U_12) | c2_2(U_12, a567) | ~c3_2(U_12, a506) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.13 tff(c_3403, plain, (![U_215, V_216]: (c7_1(U_215) | c3_2(U_215, V_216) | ~c6_1(U_215) | c1_2(U_215, a498) | ~c1_2(U_215, V_216) | ~c6_2(U_215, V_216) | ~ssSkP3(U_215) | c1_1(U_215) | c2_2(U_215, V_216) | ~c3_2(U_215, a506) | ~ndr1_1(U_215) | ~c5_2(U_215, V_216)))). % 15.83/5.13 tff(c_4218, plain, (![U_538]: (c7_1(U_538) | c3_2(U_538, a506) | ~c6_1(U_538) | ~c7_2(U_538, a506) | ~c8_1(U_538) | ~c5_2(U_538, a506) | c1_1(U_538) | c2_2(U_538, a553) | ~ndr1_1(U_538) | ~c5_2(U_538, a553) | c7_2(U_538, a553)))). % 15.83/5.13 tff(c_4121, plain, (![U_580]: (c8_2(U_580, a553) | c8_2(U_580, a506) | ~c8_1(U_580) | ~c5_2(U_580, a506) | c7_1(U_580) | c3_2(U_580, a567) | ~c6_1(U_580) | c10_2(U_580, a498) | ~c1_2(U_580, a567) | ~ssSkP3(U_580) | c1_1(U_580) | c2_2(U_580, a567) | ~ndr1_1(U_580) | ~c5_2(U_580, a567) | ssSkP10(U_580)))). % 15.83/5.13 tff(c_3540, plain, (![U_538, V_539]: (c7_1(U_538) | c3_2(U_538, a506) | ~c6_1(U_538) | ~c7_2(U_538, a506) | c7_2(U_538, a553) | ~c8_1(U_538) | ~c5_2(U_538, a506) | c1_1(U_538) | c2_2(U_538, V_539) | c7_2(U_538, V_539) | ~ndr1_1(U_538) | ~c5_2(U_538, V_539)))). % 15.83/5.13 tff(c_4182, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c10_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c1_1(U_12) | c10_2(U_12, a506) | c2_2(U_12, a567) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.13 tff(c_4150, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c10_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c1_1(U_12) | c2_2(U_12, a567) | ~c3_2(U_12, a506) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.13 tff(c_3461, plain, (![U_187, V_188]: (c7_1(U_187) | c3_2(U_187, V_188) | ~c6_1(U_187) | c10_2(U_187, a498) | ~c1_2(U_187, V_188) | ~c6_2(U_187, V_188) | ~ssSkP3(U_187) | c1_1(U_187) | c10_2(U_187, a506) | c2_2(U_187, V_188) | ~ndr1_1(U_187) | ~c5_2(U_187, V_188)))). % 15.83/5.13 tff(c_3460, plain, (![U_215, V_216]: (c7_1(U_215) | c3_2(U_215, V_216) | ~c6_1(U_215) | c10_2(U_215, a498) | ~c1_2(U_215, V_216) | ~c6_2(U_215, V_216) | ~ssSkP3(U_215) | c1_1(U_215) | c2_2(U_215, V_216) | ~c3_2(U_215, a506) | ~ndr1_1(U_215) | ~c5_2(U_215, V_216)))). % 15.83/5.13 tff(c_4105, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c10_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c1_1(U_12) | c9_2(U_12, a506) | c2_2(U_12, a567) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.13 tff(c_3462, plain, (![U_189, V_190]: (c7_1(U_189) | c3_2(U_189, V_190) | ~c6_1(U_189) | c10_2(U_189, a498) | ~c1_2(U_189, V_190) | ~c6_2(U_189, V_190) | ~ssSkP3(U_189) | c1_1(U_189) | c9_2(U_189, a506) | c2_2(U_189, V_190) | ~ndr1_1(U_189) | ~c5_2(U_189, V_190)))). % 15.83/5.13 tff(c_4084, plain, (~c10_2(a515, a567))). % 15.83/5.13 tff(c_3764, plain, (![U_553]: (c7_1(U_553) | c3_2(U_553, a506) | ~c6_1(U_553) | ~c7_2(U_553, a506) | ~c10_2(U_553, a568) | ~c1_2(U_553, a531) | ~ssSkP10(U_553) | c7_2(U_553, a553) | ~c8_1(U_553) | ~c5_2(U_553, a506) | c1_1(U_553) | c2_2(U_553, a531) | ~ndr1_1(U_553) | ssSkP7(U_553)))). % 15.83/5.13 tff(c_4056, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c1_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c1_1(U_12) | c10_2(U_12, a506) | c2_2(U_12, a567) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.13 tff(c_3404, plain, (![U_187, V_188]: (c7_1(U_187) | c3_2(U_187, V_188) | ~c6_1(U_187) | c1_2(U_187, a498) | ~c1_2(U_187, V_188) | ~c6_2(U_187, V_188) | ~ssSkP3(U_187) | c1_1(U_187) | c10_2(U_187, a506) | c2_2(U_187, V_188) | ~ndr1_1(U_187) | ~c5_2(U_187, V_188)))). % 15.83/5.13 tff(c_3990, plain, (![U_12]: (c7_1(U_12) | c3_2(U_12, a567) | ~c6_1(U_12) | c1_2(U_12, a498) | ~c1_2(U_12, a567) | ~ssSkP3(U_12) | c1_1(U_12) | c9_2(U_12, a506) | c2_2(U_12, a567) | ~ndr1_1(U_12) | ~c5_2(U_12, a567) | ssSkP10(U_12)))). % 15.83/5.13 tff(c_3505, plain, (![U_535, V_536]: (c7_1(U_535) | c3_2(U_535, a506) | ~c6_1(U_535) | ~c7_2(U_535, a506) | c10_2(U_535, a553) | ~c8_1(U_535) | ~c5_2(U_535, a506) | c1_1(U_535) | c2_2(U_535, V_536) | c7_2(U_535, V_536) | ~ndr1_1(U_535) | ~c5_2(U_535, V_536)))). % 15.83/5.13 tff(c_3405, plain, (![U_189, V_190]: (c7_1(U_189) | c3_2(U_189, V_190) | ~c6_1(U_189) | c1_2(U_189, a498) | ~c1_2(U_189, V_190) | ~c6_2(U_189, V_190) | ~ssSkP3(U_189) | c1_1(U_189) | c9_2(U_189, a506) | c2_2(U_189, V_190) | ~ndr1_1(U_189) | ~c5_2(U_189, V_190)))). % 15.83/5.13 tff(c_3573, plain, (![U_540, V_541]: (c7_1(U_540) | c3_2(U_540, a553) | ~c6_1(U_540) | ~c7_2(U_540, a553) | c8_2(U_540, a506) | ~c8_1(U_540) | ~c5_2(U_540, a506) | c1_1(U_540) | c2_2(U_540, V_541) | c7_2(U_540, V_541) | ~ndr1_1(U_540) | ~c5_2(U_540, V_541)))). % 15.83/5.13 tff(c_3321, plain, (![U_526]: (~c10_2(U_526, a568) | ~c1_2(U_526, a553) | ~c5_2(U_526, a553) | ~ssSkP10(U_526) | c7_1(U_526) | c3_2(U_526, a497) | ~c6_1(U_526) | ~c7_2(U_526, a497) | ~c8_1(U_526) | ~ndr1_1(U_526) | ~c5_2(U_526, a497) | ssSkP3(U_526)))). % 15.83/5.13 tff(c_3314, plain, (![U_525]: (~c10_2(U_525, a568) | ~c1_2(U_525, a553) | ~c5_2(U_525, a553) | ~ssSkP10(U_525) | c7_1(U_525) | c3_2(U_525, a452) | ~c6_1(U_525) | ~c7_2(U_525, a452) | ~c8_1(U_525) | ~ndr1_1(U_525) | ~c5_2(U_525, a452) | ssSkP1(U_525)))). % 15.83/5.13 tff(c_3576, plain, (![U_540, V_541]: (~c10_2(U_540, a568) | ~c1_2(U_540, V_541) | ~ssSkP10(U_540) | c8_2(U_540, a553) | c8_2(U_540, a506) | ~c8_1(U_540) | ~c5_2(U_540, a506) | c1_1(U_540) | c2_2(U_540, V_541) | ~ndr1_1(U_540) | ~c5_2(U_540, V_541)))). % 15.83/5.13 tff(c_3129, plain, (![U_510]: (c8_2(U_510, a553) | c8_2(U_510, a506) | ~c8_1(U_510) | ~c5_2(U_510, a506) | ~c10_2(U_510, a568) | ~c1_2(U_510, a531) | ~ssSkP10(U_510) | c1_1(U_510) | c2_2(U_510, a531) | ~ndr1_1(U_510) | ssSkP7(U_510)))). % 15.83/5.13 tff(c_3114, plain, (![U_509]: (c8_2(U_509, a553) | c8_2(U_509, a506) | ~c8_1(U_509) | ~c5_2(U_509, a506) | ~c10_2(U_509, a568) | ~c1_2(U_509, a542) | ~ssSkP10(U_509) | c1_1(U_509) | c2_2(U_509, a542) | ~ndr1_1(U_509) | ssSkP8(U_509)))). % 15.83/5.13 tff(c_3508, plain, (![U_535, V_536]: (~c10_2(U_535, a568) | ~c1_2(U_535, V_536) | ~ssSkP10(U_535) | c10_2(U_535, a553) | c8_2(U_535, a506) | ~c8_1(U_535) | ~c5_2(U_535, a506) | c1_1(U_535) | c2_2(U_535, V_536) | ~ndr1_1(U_535) | ~c5_2(U_535, V_536)))). % 15.83/5.13 tff(c_3115, plain, (![U_509]: (c7_2(U_509, a553) | c8_2(U_509, a506) | ~c8_1(U_509) | ~c5_2(U_509, a506) | ~c10_2(U_509, a568) | ~c1_2(U_509, a542) | ~ssSkP10(U_509) | c1_1(U_509) | c2_2(U_509, a542) | ~ndr1_1(U_509) | ssSkP8(U_509)))). % 15.83/5.13 tff(c_3131, plain, (![U_510]: (c10_2(U_510, a553) | c8_2(U_510, a506) | ~c8_1(U_510) | ~c5_2(U_510, a506) | ~c10_2(U_510, a568) | ~c1_2(U_510, a531) | ~ssSkP10(U_510) | c1_1(U_510) | c2_2(U_510, a531) | ~ndr1_1(U_510) | ssSkP7(U_510)))). % 15.83/5.13 tff(c_3116, plain, (![U_509]: (c10_2(U_509, a553) | c8_2(U_509, a506) | ~c8_1(U_509) | ~c5_2(U_509, a506) | ~c10_2(U_509, a568) | ~c1_2(U_509, a542) | ~ssSkP10(U_509) | c1_1(U_509) | c2_2(U_509, a542) | ~ndr1_1(U_509) | ssSkP8(U_509)))). % 15.83/5.13 tff(c_3713, plain, (![U_215]: (c3_2(U_215, a553) | c7_1(U_215) | c3_2(U_215, a452) | ~c6_1(U_215) | ~c8_1(U_215) | ssSkP1(U_215) | c1_1(U_215) | c2_2(U_215, a452) | ~c3_2(U_215, a506) | ~ndr1_1(U_215) | ~c5_2(U_215, a452)))). % 15.83/5.13 tff(c_3714, plain, (![U_187]: (c3_2(U_187, a553) | c7_1(U_187) | c3_2(U_187, a452) | ~c6_1(U_187) | ~c8_1(U_187) | ssSkP1(U_187) | c1_1(U_187) | c10_2(U_187, a506) | c2_2(U_187, a452) | ~ndr1_1(U_187) | ~c5_2(U_187, a452)))). % 15.83/5.13 tff(c_3740, plain, (![U_15]: (~c10_2(U_15, a568) | ~c1_2(U_15, a531) | ~ssSkP10(U_15) | c7_2(U_15, a553) | c8_2(U_15, a506) | ~c8_1(U_15) | ~c5_2(U_15, a506) | c1_1(U_15) | c2_2(U_15, a531) | ~ndr1_1(U_15) | ssSkP7(U_15)))). % 15.83/5.13 tff(c_3358, plain, (![U_215]: (c7_1(U_215) | c3_2(U_215, a452) | ~c6_1(U_215) | c10_2(U_215, a553) | ~c8_1(U_215) | ssSkP1(U_215) | c1_1(U_215) | c2_2(U_215, a452) | ~c3_2(U_215, a506) | ~ndr1_1(U_215) | ~c5_2(U_215, a452)))). % 15.83/5.13 tff(c_3744, plain, (~c10_2(a515, a452))). % 15.83/5.13 tff(c_3543, plain, (![U_538, V_539]: (~c10_2(U_538, a568) | ~c1_2(U_538, V_539) | ~ssSkP10(U_538) | c7_2(U_538, a553) | c8_2(U_538, a506) | ~c8_1(U_538) | ~c5_2(U_538, a506) | c1_1(U_538) | c2_2(U_538, V_539) | ~ndr1_1(U_538) | ~c5_2(U_538, V_539)))). % 15.83/5.13 tff(c_3359, plain, (![U_187]: (c7_1(U_187) | c3_2(U_187, a452) | ~c6_1(U_187) | c10_2(U_187, a553) | ~c8_1(U_187) | ssSkP1(U_187) | c1_1(U_187) | c10_2(U_187, a506) | c2_2(U_187, a452) | ~ndr1_1(U_187) | ~c5_2(U_187, a452)))). % 15.83/5.13 tff(c_3685, plain, (![U_481]: (c3_2(U_481, a553) | c7_1(U_481) | c3_2(U_481, a452) | ~c6_1(U_481) | ~c7_2(U_481, a452) | ~c8_1(U_481) | ~ndr1_1(U_481) | ~c5_2(U_481, a452) | ssSkP1(U_481)))). % 15.83/5.13 tff(c_3622, plain, (![U_482]: (c3_2(U_482, a553) | c7_1(U_482) | c3_2(U_482, a497) | ~c6_1(U_482) | ~c7_2(U_482, a497) | ~c8_1(U_482) | ~ndr1_1(U_482) | ~c5_2(U_482, a497) | ssSkP3(U_482)))). % 15.83/5.13 tff(c_3463, plain, (![U_26]: (c7_1(U_26) | c3_2(U_26, a512) | ~c6_1(U_26) | c10_2(U_26, a498) | ~c1_2(U_26, a512) | ~c6_2(U_26, a512) | ~ssSkP3(U_26) | c10_2(U_26, a451) | ~ndr1_1(U_26) | ~ssSkP5(U_26) | ssSkP0(U_26)))). % 15.83/5.13 tff(c_3593, plain, (~c5_2(a560, a506))). % 15.83/5.13 tff(c_3145, plain, (![U_63]: (~c1_2(U_63, a474) | c1_1(U_63) | c10_2(U_63, a506) | c2_2(U_63, a589) | ~c5_2(U_63, a589) | c7_1(U_63) | ~c6_1(U_63) | ~ndr1_1(U_63) | c9_1(U_63) | c10_1(U_63)))). % 15.83/5.13 tff(c_3211, plain, (![U_63]: (~c1_2(U_63, a474) | c1_1(U_63) | c2_2(U_63, a589) | ~c3_2(U_63, a506) | ~c5_2(U_63, a589) | c7_1(U_63) | ~c6_1(U_63) | ~ndr1_1(U_63) | c9_1(U_63) | c10_1(U_63)))). % 15.83/5.13 tff(c_2634, plain, (![U_189, V_190]: (c8_2(U_189, a553) | c8_2(U_189, a506) | ~c8_1(U_189) | ~c5_2(U_189, a506) | c1_1(U_189) | c2_2(U_189, V_190) | c7_2(U_189, V_190) | ~ndr1_1(U_189) | ~c5_2(U_189, V_190)))). % 15.83/5.13 tff(c_2493, plain, (![U_189, V_190]: (c7_2(U_189, a553) | c8_2(U_189, a506) | ~c8_1(U_189) | ~c5_2(U_189, a506) | c1_1(U_189) | c2_2(U_189, V_190) | c7_2(U_189, V_190) | ~ndr1_1(U_189) | ~c5_2(U_189, V_190)))). % 15.83/5.13 tff(c_3406, plain, (![U_26]: (c7_1(U_26) | c3_2(U_26, a512) | ~c6_1(U_26) | c1_2(U_26, a498) | ~c1_2(U_26, a512) | ~c6_2(U_26, a512) | ~ssSkP3(U_26) | c10_2(U_26, a451) | ~ndr1_1(U_26) | ~ssSkP5(U_26) | ssSkP0(U_26)))). % 15.83/5.13 tff(c_2313, plain, (![U_189, V_190]: (c10_2(U_189, a553) | c8_2(U_189, a506) | ~c8_1(U_189) | ~c5_2(U_189, a506) | c1_1(U_189) | c2_2(U_189, V_190) | c7_2(U_189, V_190) | ~ndr1_1(U_189) | ~c5_2(U_189, V_190)))). % 15.83/5.13 tff(c_3471, plain, (![U_27]: (c7_1(U_27) | c3_2(U_27, a451) | ~c6_1(U_27) | c10_2(U_27, a498) | ~ndr1_1(U_27) | ~c1_2(U_27, a451) | ~c6_2(U_27, a451) | ~ssSkP3(U_27) | ssSkP0(U_27)))). % 15.83/5.13 tff(c_2753, plain, (![U_495, V_496]: (c7_1(U_495) | c3_2(U_495, V_496) | ~c6_1(U_495) | ~c7_2(U_495, V_496) | c10_2(U_495, a498) | ~ndr1_1(U_495) | ~c1_2(U_495, V_496) | ~c6_2(U_495, V_496) | ~ssSkP3(U_495)))). % 15.83/5.13 tff(c_3414, plain, (![U_27]: (c7_1(U_27) | c3_2(U_27, a451) | ~c6_1(U_27) | c1_2(U_27, a498) | ~ndr1_1(U_27) | ~c1_2(U_27, a451) | ~c6_2(U_27, a451) | ~ssSkP3(U_27) | ssSkP0(U_27)))). % 15.83/5.13 tff(c_2833, plain, (![U_498, V_499]: (c7_1(U_498) | c3_2(U_498, V_499) | ~c6_1(U_498) | ~c7_2(U_498, V_499) | c1_2(U_498, a498) | ~ndr1_1(U_498) | ~c1_2(U_498, V_499) | ~c6_2(U_498, V_499) | ~ssSkP3(U_498)))). % 15.83/5.13 tff(c_2355, plain, (![U_25]: (c7_1(U_25) | c3_2(U_25, a452) | ~c6_1(U_25) | ~c7_2(U_25, a452) | c10_2(U_25, a553) | ~c8_1(U_25) | ~ndr1_1(U_25) | ~c5_2(U_25, a452) | ssSkP1(U_25)))). % 15.83/5.13 tff(c_2354, plain, (![U_23]: (c7_1(U_23) | c3_2(U_23, a497) | ~c6_1(U_23) | ~c7_2(U_23, a497) | c10_2(U_23, a553) | ~c8_1(U_23) | ~ndr1_1(U_23) | ~c5_2(U_23, a497) | ssSkP3(U_23)))). % 15.83/5.13 tff(c_2546, plain, (![U_482]: (c7_1(U_482) | c3_2(U_482, a497) | ~c6_1(U_482) | ~c7_2(U_482, a497) | c7_2(U_482, a553) | ~c8_1(U_482) | ~ndr1_1(U_482) | ~c5_2(U_482, a497) | ssSkP3(U_482)))). % 15.83/5.13 tff(c_2541, plain, (![U_481]: (c7_1(U_481) | c3_2(U_481, a452) | ~c6_1(U_481) | ~c7_2(U_481, a452) | c7_2(U_481, a553) | ~c8_1(U_481) | ~ndr1_1(U_481) | ~c5_2(U_481, a452) | ssSkP1(U_481)))). % 15.83/5.13 tff(c_3308, plain, (~c6_0)). % 15.83/5.13 tff(c_3305, plain, (~c5_1(a566))). % 15.83/5.13 tff(c_3303, plain, (c1_1(a566))). % 15.83/5.13 tff(c_3300, plain, (c10_1(a566))). % 15.83/5.13 tff(c_3297, plain, (c2_1(a566))). % 15.83/5.13 tff(c_3272, plain, (~ndr1_1(a566))). % 15.83/5.13 tff(c_2653, plain, (![U_490]: (c7_1(U_490) | c3_2(U_490, a553) | ~c6_1(U_490) | ~c7_2(U_490, a553) | c8_2(U_490, a497) | ~c8_1(U_490) | ~ndr1_1(U_490) | ~c5_2(U_490, a497) | ssSkP3(U_490)))). % 15.83/5.13 tff(c_2658, plain, (![U_491]: (c7_1(U_491) | c3_2(U_491, a553) | ~c6_1(U_491) | ~c7_2(U_491, a553) | c8_2(U_491, a452) | ~c8_1(U_491) | ~ndr1_1(U_491) | ~c5_2(U_491, a452) | ssSkP1(U_491)))). % 15.83/5.13 tff(c_3244, plain, (~c10_2(a515, a589))). % 15.83/5.13 tff(c_3216, plain, (![U_16]: (c10_1(U_16) | ~c1_2(U_16, a529) | c1_1(U_16) | c2_2(U_16, a589) | ~c3_2(U_16, a506) | ~ndr1_1(U_16) | ~c5_2(U_16, a589) | ssSkP6(U_16)))). % 15.83/5.13 tff(c_3215, plain, (![U_21]: (c10_1(U_21) | ~c1_2(U_21, a507) | c1_1(U_21) | c2_2(U_21, a589) | ~c3_2(U_21, a506) | ~ndr1_1(U_21) | ~c5_2(U_21, a589) | ssSkP4(U_21)))). % 15.83/5.13 tff(c_3225, plain, (~c3_1(a566))). % 15.83/5.13 tff(c_2605, plain, (![U_486, V_184]: (c10_1(U_486) | ~c3_2(U_486, V_184) | ~c1_2(U_486, V_184) | c1_1(U_486) | c2_2(U_486, a589) | ~c3_2(U_486, a506) | ~ndr1_1(U_486) | ~c5_2(U_486, a589)))). % 15.83/5.13 tff(c_3192, plain, (![U_15]: (~c10_2(U_15, a568) | ~c1_2(U_15, a531) | ~ssSkP10(U_15) | c1_1(U_15) | c10_2(U_15, a506) | c2_2(U_15, a531) | ~ndr1_1(U_15) | ssSkP7(U_15)))). % 15.83/5.13 tff(c_3191, plain, (![U_14]: (~c10_2(U_14, a568) | ~c1_2(U_14, a542) | ~ssSkP10(U_14) | c1_1(U_14) | c10_2(U_14, a506) | c2_2(U_14, a542) | ~ndr1_1(U_14) | ssSkP8(U_14)))). % 15.83/5.14 tff(c_2449, plain, (![U_187, V_188]: (~c10_2(U_187, a568) | ~c1_2(U_187, V_188) | ~ssSkP10(U_187) | c1_1(U_187) | c10_2(U_187, a506) | c2_2(U_187, V_188) | ~ndr1_1(U_187) | ~c5_2(U_187, V_188)))). % 15.83/5.14 tff(c_3150, plain, (![U_16]: (c10_1(U_16) | ~c1_2(U_16, a529) | c1_1(U_16) | c10_2(U_16, a506) | c2_2(U_16, a589) | ~ndr1_1(U_16) | ~c5_2(U_16, a589) | ssSkP6(U_16)))). % 15.83/5.14 tff(c_3149, plain, (![U_21]: (c10_1(U_21) | ~c1_2(U_21, a507) | c1_1(U_21) | c10_2(U_21, a506) | c2_2(U_21, a589) | ~ndr1_1(U_21) | ~c5_2(U_21, a589) | ssSkP4(U_21)))). % 15.83/5.14 tff(c_2283, plain, (![U_463, V_184]: (c10_1(U_463) | ~c3_2(U_463, V_184) | ~c1_2(U_463, V_184) | c1_1(U_463) | c10_2(U_463, a506) | c2_2(U_463, a589) | ~ndr1_1(U_463) | ~c5_2(U_463, a589)))). % 15.83/5.14 tff(c_3086, plain, (![U_15]: (~c10_2(U_15, a568) | ~c1_2(U_15, a531) | ~ssSkP10(U_15) | c1_1(U_15) | c9_2(U_15, a506) | c2_2(U_15, a531) | ~ndr1_1(U_15) | ssSkP7(U_15)))). % 15.83/5.14 tff(c_3085, plain, (![U_14]: (~c10_2(U_14, a568) | ~c1_2(U_14, a542) | ~ssSkP10(U_14) | c1_1(U_14) | c9_2(U_14, a506) | c2_2(U_14, a542) | ~ndr1_1(U_14) | ssSkP8(U_14)))). % 15.83/5.14 tff(c_3098, plain, (~ssSkP10(a515))). % 15.83/5.14 tff(c_3092, plain, (~ssSkP10(a575))). % 15.83/5.14 tff(c_2450, plain, (![U_189, V_190]: (~c10_2(U_189, a568) | ~c1_2(U_189, V_190) | ~ssSkP10(U_189) | c1_1(U_189) | c9_2(U_189, a506) | c2_2(U_189, V_190) | ~ndr1_1(U_189) | ~c5_2(U_189, V_190)))). % 15.83/5.14 tff(c_3060, plain, (![U_15]: (~c10_2(U_15, a568) | ~c1_2(U_15, a531) | ~ssSkP10(U_15) | c1_1(U_15) | c2_2(U_15, a531) | ~c3_2(U_15, a506) | ~ndr1_1(U_15) | ssSkP7(U_15)))). % 15.83/5.14 tff(c_3071, plain, (ssSkC2)). % 15.83/5.14 tff(c_3059, plain, (![U_14]: (~c10_2(U_14, a568) | ~c1_2(U_14, a542) | ~ssSkP10(U_14) | c1_1(U_14) | c2_2(U_14, a542) | ~c3_2(U_14, a506) | ~ndr1_1(U_14) | ssSkP8(U_14)))). % 15.83/5.14 tff(c_3067, plain, (~c3_2(a515, a506))). % 15.83/5.14 tff(c_3066, plain, (~c3_2(a575, a506))). % 15.83/5.14 tff(c_2597, plain, (![U_486, V_487]: (~c10_2(U_486, a568) | ~c1_2(U_486, V_487) | ~ssSkP10(U_486) | c1_1(U_486) | c2_2(U_486, V_487) | ~c3_2(U_486, a506) | ~ndr1_1(U_486) | ~c5_2(U_486, V_487)))). % 15.83/5.14 tff(c_3032, plain, (~c10_2(a515, a512))). % 15.83/5.14 tff(c_2451, plain, (![U_26]: (~c10_2(U_26, a568) | ~c1_2(U_26, a512) | ~c5_2(U_26, a512) | ~ssSkP10(U_26) | c10_2(U_26, a451) | ~ndr1_1(U_26) | ~ssSkP5(U_26) | ssSkP0(U_26)))). % 15.83/5.14 tff(c_3020, plain, (~c5_2(a502, a503))). % 15.83/5.14 tff(c_3002, plain, (~c7_2(a502, a503))). % 15.83/5.14 tff(c_2995, plain, (c8_2(a502, a503))). % 15.83/5.14 tff(c_2989, plain, (~c3_2(a605, a606))). % 15.83/5.14 tff(c_2986, plain, (c2_2(a605, a606))). % 15.83/5.14 tff(c_2981, plain, (~c1_2(a502, a503))). % 15.83/5.14 tff(c_2968, plain, (~c5_2(a560, a536))). % 15.83/5.14 tff(c_2971, plain, (~c1_2(a605, a606))). % 15.83/5.14 tff(c_2962, plain, (~ssSkP3(a560))). % 15.83/5.14 tff(c_2957, plain, (~c5_2(a560, a452))). % 15.83/5.14 tff(c_2956, plain, (~c5_2(a560, a497))). % 15.83/5.14 tff(c_2953, plain, (c10_1(a560))). % 15.83/5.14 tff(c_2869, plain, (![U_269]: (c3_2(a560, U_269) | c10_2(a560, U_269) | ~c8_2(a560, U_269)))). % 15.83/5.14 tff(c_2864, plain, (c3_1(a601))). % 15.83/5.14 tff(c_2854, plain, (![U_282]: (c10_1(U_282) | c3_1(U_282) | ~c6_1(U_282)))). % 15.83/5.14 tff(c_2849, plain, (ndr1_1(a605))). % 15.83/5.14 tff(c_2812, plain, (![U_233, V_234]: (c1_2(U_233, a498) | c8_2(U_233, V_234) | ~ndr1_1(U_233) | ~c1_2(U_233, V_234) | ~c6_2(U_233, V_234) | ~ssSkP3(U_233)))). % 15.83/5.14 tff(c_2807, plain, (~c1_1(a502))). % 15.83/5.14 tff(c_2801, plain, (~c9_1(a502))). % 15.83/5.14 tff(c_2797, plain, (~c10_2(a517, a511))). % 15.83/5.14 tff(c_2726, plain, (![U_19]: (c7_1(U_19) | ~c2_1(U_19) | ~ndr1_1(U_19) | ~c4_2(U_19, a511) | ~c3_2(U_19, a511) | ssSkP5(U_19)))). % 15.83/5.14 tff(c_2779, plain, (~ssSkP3(a575))). % 15.83/5.14 tff(c_2783, plain, (~c5_1(a502))). % 15.83/5.14 tff(c_2769, plain, (~ssSkP3(a571))). % 15.83/5.14 tff(c_2773, plain, (ndr1_1(a502))). % 15.83/5.14 tff(c_2768, plain, (~c3_2(a582, a583))). % 15.83/5.14 tff(c_2767, plain, (~c4_2(a467, a468))). % 15.83/5.14 tff(c_2732, plain, (![U_231, V_232]: (c10_2(U_231, a498) | c8_2(U_231, V_232) | ~ndr1_1(U_231) | ~c1_2(U_231, V_232) | ~c6_2(U_231, V_232) | ~ssSkP3(U_231)))). % 15.83/5.14 tff(c_2698, plain, (![U_271, V_272]: (c7_1(U_271) | ~c2_1(U_271) | ~ndr1_1(U_271) | ~c4_2(U_271, V_272) | ~c6_2(U_271, V_272) | ~c3_2(U_271, V_272)))). % 15.83/5.14 tff(c_2689, plain, (~c5_1(a605))). % 15.83/5.14 tff(c_2684, plain, (~ssSkC31)). % 15.83/5.14 tff(c_2679, plain, (~ssSkC29)). % 15.83/5.14 tff(c_2676, plain, (~c4_1(a605))). % 15.83/5.14 tff(c_2635, plain, (![U_60]: (c8_2(U_60, a553) | c8_2(U_60, a536) | ~c8_1(U_60) | ~ndr1_1(U_60) | ~c5_2(U_60, a536) | c6_1(U_60) | c2_1(U_60)))). % 15.83/5.14 tff(c_2637, plain, (![U_25]: (c8_2(U_25, a553) | c8_2(U_25, a452) | ~c8_1(U_25) | ~ndr1_1(U_25) | ~c5_2(U_25, a452) | ssSkP1(U_25)))). % 15.83/5.14 tff(c_2636, plain, (![U_23]: (c8_2(U_23, a553) | c8_2(U_23, a497) | ~c8_1(U_23) | ~ndr1_1(U_23) | ~c5_2(U_23, a497) | ssSkP3(U_23)))). % 15.83/5.14 tff(c_2611, plain, (![U_227, V_228]: (c8_2(U_227, a553) | c8_2(U_227, V_228) | ~c8_1(U_227) | ~ndr1_1(U_227) | ~c5_2(U_227, V_228) | ~c9_2(U_227, V_228)))). % 15.83/5.14 tff(c_2580, plain, (![U_215, V_216]: (c1_1(U_215) | c2_2(U_215, V_216) | c7_2(U_215, V_216) | ~c3_2(U_215, a506) | ~ndr1_1(U_215) | ~c5_2(U_215, V_216)))). % 15.83/5.14 tff(c_2494, plain, (![U_60]: (c7_2(U_60, a553) | c8_2(U_60, a536) | ~c8_1(U_60) | ~ndr1_1(U_60) | ~c5_2(U_60, a536) | c6_1(U_60) | c2_1(U_60)))). % 15.83/5.14 tff(c_2562, plain, (~c10_2(a515, a474))). % 15.83/5.14 tff(c_2455, plain, (![U_63]: (~c10_2(U_63, a568) | ~ndr1_1(U_63) | ~c1_2(U_63, a474) | ~c5_2(U_63, a474) | ~ssSkP10(U_63) | c9_1(U_63) | c10_1(U_63)))). % 15.83/5.14 tff(c_2314, plain, (![U_60]: (c10_2(U_60, a553) | c8_2(U_60, a536) | ~c8_1(U_60) | ~ndr1_1(U_60) | ~c5_2(U_60, a536) | c6_1(U_60) | c2_1(U_60)))). % 15.83/5.14 tff(c_2495, plain, (![U_23]: (c7_2(U_23, a553) | c8_2(U_23, a497) | ~c8_1(U_23) | ~ndr1_1(U_23) | ~c5_2(U_23, a497) | ssSkP3(U_23)))). % 15.83/5.14 tff(c_2496, plain, (![U_25]: (c7_2(U_25, a553) | c8_2(U_25, a452) | ~c8_1(U_25) | ~ndr1_1(U_25) | ~c5_2(U_25, a452) | ssSkP1(U_25)))). % 15.83/5.14 tff(c_2534, plain, (~c10_2(a515, a451))). % 15.83/5.14 tff(c_2458, plain, (![U_27]: (~c10_2(U_27, a568) | ~ndr1_1(U_27) | ~c1_2(U_27, a451) | ~c5_2(U_27, a451) | ~ssSkP10(U_27) | ssSkP0(U_27)))). % 15.83/5.14 tff(c_2525, plain, (ssSkC24)). % 15.83/5.14 tff(c_2522, plain, (~c10_2(a515, a529))). % 15.83/5.14 tff(c_2457, plain, (![U_18]: (~c10_2(U_18, a568) | ~ndr1_1(U_18) | ~c1_2(U_18, a529) | ~c5_2(U_18, a529) | ~ssSkP10(U_18) | ssSkP6(U_18)))). % 15.83/5.14 tff(c_2508, plain, (~ssSkP10(a597))). % 15.83/5.14 tff(c_2470, plain, (![U_223, V_224]: (c7_2(U_223, a553) | c8_2(U_223, V_224) | ~c8_1(U_223) | ~ndr1_1(U_223) | ~c5_2(U_223, V_224) | ~c9_2(U_223, V_224)))). % 15.83/5.14 tff(c_2462, plain, (~ssSkP10(a478))). % 15.83/5.14 tff(c_2420, plain, (![U_274, V_275]: (~c10_2(U_274, a568) | ~ndr1_1(U_274) | ~c7_2(U_274, V_275) | ~c1_2(U_274, V_275) | ~c5_2(U_274, V_275) | ~ssSkP10(U_274)))). % 15.83/5.14 tff(c_2415, plain, (![U_472]: (~c10_2(U_472, a589) | ~c1_2(U_472, a474) | c7_1(U_472) | ~c6_1(U_472) | ~ndr1_1(U_472) | c9_1(U_472) | c10_1(U_472)))). % 15.83/5.14 tff(c_2414, plain, (![U_472]: (~c2_2(U_472, a589) | ~c1_2(U_472, a474) | c7_1(U_472) | ~c6_1(U_472) | ~ndr1_1(U_472) | c9_1(U_472) | c10_1(U_472)))). % 15.83/5.14 tff(c_2406, plain, (![U_63]: (c7_1(U_63) | c3_2(U_63, a474) | ~c6_1(U_63) | ~ndr1_1(U_63) | c9_1(U_63) | c10_1(U_63)))). % 15.83/5.14 tff(c_2384, plain, (~c5_2(a517, a518))). % 15.83/5.14 tff(c_2380, plain, (~c5_2(a523, a524))). % 15.83/5.14 tff(c_2383, plain, (ssSkC21)). % 15.83/5.14 tff(c_2371, plain, (~c7_2(a523, a524))). % 15.83/5.14 tff(c_2363, plain, (~c7_2(a517, a518))). % 15.83/5.14 tff(c_2337, plain, (![U_239, V_240]: (c7_1(U_239) | c3_2(U_239, V_240) | ~c6_1(U_239) | ~ndr1_1(U_239) | ~c8_2(U_239, V_240) | ~c7_2(U_239, V_240)))). % 15.83/5.14 tff(c_2315, plain, (![U_23]: (c10_2(U_23, a553) | c8_2(U_23, a497) | ~c8_1(U_23) | ~ndr1_1(U_23) | ~c5_2(U_23, a497) | ssSkP3(U_23)))). % 15.83/5.14 tff(c_2316, plain, (![U_25]: (c10_2(U_25, a553) | c8_2(U_25, a452) | ~c8_1(U_25) | ~ndr1_1(U_25) | ~c5_2(U_25, a452) | ssSkP1(U_25)))). % 15.83/5.14 tff(c_2332, plain, (ssSkC9)). % 15.83/5.14 tff(c_2329, plain, (~c5_2(a571, a572))). % 15.83/5.14 tff(c_2328, plain, (~c8_1(a575))). % 15.83/5.14 tff(c_2287, plain, (~c5_2(a602, a603))). % 15.83/5.14 tff(c_2290, plain, (![U_225, V_226]: (c10_2(U_225, a553) | c8_2(U_225, V_226) | ~c8_1(U_225) | ~ndr1_1(U_225) | ~c5_2(U_225, V_226) | ~c9_2(U_225, V_226)))). % 15.83/5.14 tff(c_2275, plain, (![U_187, V_188]: (c1_1(U_187) | c10_2(U_187, a506) | c2_2(U_187, V_188) | c7_2(U_187, V_188) | ~ndr1_1(U_187) | ~c5_2(U_187, V_188)))). % 15.83/5.14 tff(c_2272, plain, (ssSkC11)). % 15.83/5.14 tff(c_2266, plain, (![U_189, V_190]: (c1_1(U_189) | c9_2(U_189, a506) | c2_2(U_189, V_190) | c7_2(U_189, V_190) | ~ndr1_1(U_189) | ~c5_2(U_189, V_190)))). % 15.83/5.14 tff(c_2245, plain, (![U_16]: (c10_1(U_16) | ~c2_2(U_16, a589) | ~ndr1_1(U_16) | ~c1_2(U_16, a529) | ssSkP6(U_16)))). % 15.83/5.14 tff(c_2262, plain, (~c10_2(a515, a511))). % 15.83/5.14 tff(c_2255, plain, (![U_255]: (c5_2(a515, U_255) | ~c1_2(a515, U_255) | ~c10_2(a515, U_255)))). % 15.83/5.14 tff(c_2244, plain, (![U_21]: (c10_1(U_21) | ~c2_2(U_21, a589) | ~ndr1_1(U_21) | ~c1_2(U_21, a507) | ssSkP4(U_21)))). % 15.83/5.14 tff(c_2224, plain, (![U_179, V_180]: (c10_1(U_179) | ~c2_2(U_179, a589) | ~ndr1_1(U_179) | ~c3_2(U_179, V_180) | ~c1_2(U_179, V_180)))). % 15.83/5.14 tff(c_2213, plain, (![U_26]: (c1_2(U_26, a512) | c10_2(U_26, a451) | ~ndr1_1(U_26) | ~ssSkP5(U_26) | ssSkP0(U_26)))). % 15.83/5.14 tff(c_2199, plain, (![U_165, V_166]: (c1_2(U_165, a512) | c10_2(U_165, V_166) | ~ndr1_1(U_165) | ~c4_2(U_165, V_166) | ~ssSkP5(U_165)))). % 15.83/5.14 tff(c_2194, plain, (~c1_2(a597, a589))). % 15.83/5.14 tff(c_2186, plain, (![U_183, V_184]: (c10_1(U_183) | ~c7_2(U_183, a589) | ~ndr1_1(U_183) | ~c3_2(U_183, V_184) | ~c1_2(U_183, V_184)))). % 15.83/5.14 tff(c_2170, plain, (![U_21]: (c10_1(U_21) | ~c10_2(U_21, a589) | ~ndr1_1(U_21) | ~c1_2(U_21, a507) | ssSkP4(U_21)))). % 15.83/5.14 tff(c_2171, plain, (![U_16]: (c10_1(U_16) | ~c10_2(U_16, a589) | ~ndr1_1(U_16) | ~c1_2(U_16, a529) | ssSkP6(U_16)))). % 15.83/5.14 tff(c_2179, plain, (~c1_2(a467, a468))). % 15.83/5.14 tff(c_2178, plain, (~c1_2(a471, a472))). % 15.83/5.14 tff(c_2150, plain, (![U_181, V_182]: (c10_1(U_181) | ~c10_2(U_181, a589) | ~ndr1_1(U_181) | ~c3_2(U_181, V_182) | ~c1_2(U_181, V_182)))). % 15.83/5.14 tff(c_2143, plain, (![U_26]: (c7_2(U_26, a512) | c10_2(U_26, a451) | ~ndr1_1(U_26) | ~ssSkP5(U_26) | ssSkP0(U_26)))). % 15.83/5.15 tff(c_2132, plain, (![U_163, V_164]: (c7_2(U_163, a512) | c10_2(U_163, V_164) | ~ndr1_1(U_163) | ~c4_2(U_163, V_164) | ~ssSkP5(U_163)))). % 15.83/5.15 tff(c_2119, plain, (![U_26]: (c2_2(U_26, a512) | c10_2(U_26, a451) | ~ndr1_1(U_26) | ~ssSkP5(U_26) | ssSkP0(U_26)))). % 15.83/5.15 tff(c_2123, plain, (~ssSkP5(a523))). % 15.83/5.15 tff(c_2105, plain, (![U_167, V_168]: (c2_2(U_167, a512) | c10_2(U_167, V_168) | ~ndr1_1(U_167) | ~c4_2(U_167, V_168) | ~ssSkP5(U_167)))). % 15.83/5.15 tff(c_2093, plain, (c7_1(a601))). % 15.83/5.15 tff(c_2091, plain, (c6_1(a601))). % 15.83/5.15 tff(c_2080, plain, (~c2_1(a601))). % 15.83/5.15 tff(c_2089, plain, (c8_1(a601))). % 15.83/5.15 tff(c_2085, plain, (c9_1(a601))). % 15.83/5.15 tff(c_2059, plain, (~ndr1_1(a601))). % 15.83/5.15 tff(c_2058, plain, (c7_1(a469))). % 15.83/5.15 tff(c_2056, plain, (![U_151]: (c7_2(a597, U_151) | ~c3_2(a597, U_151) | ~c1_2(a597, U_151)))). % 15.83/5.15 tff(c_2053, plain, (~c2_1(a469))). % 15.83/5.15 tff(c_2025, plain, (~ndr1_1(a469))). % 15.83/5.15 tff(c_2024, plain, (ssSkC32)). % 15.83/5.15 tff(c_2021, plain, (c2_2(a560, a561))). % 15.83/5.15 tff(c_2018, plain, (~c9_2(a504, a505))). % 15.83/5.15 tff(c_2011, plain, (c3_2(a467, a468))). % 15.83/5.15 tff(c_2015, plain, (~c10_2(a467, a468))). % 15.83/5.15 tff(c_1982, plain, (~c5_2(a582, a583))). % 15.83/5.15 tff(c_1978, plain, (~c2_2(a504, a505))). % 15.83/5.15 tff(c_1975, plain, (~c3_2(a504, a505))). % 15.83/5.15 tff(c_1972, plain, (c1_2(a560, a561))). % 15.83/5.15 tff(c_1969, plain, (c6_2(a582, a583))). % 15.83/5.15 tff(c_1965, plain, (~c10_2(a582, a583))). % 15.83/5.15 tff(c_1961, plain, (c6_2(a467, a468))). % 15.83/5.15 tff(c_1929, plain, (~c10_2(a517, a528))). % 15.83/5.15 tff(c_1920, plain, (![U_138]: (~c2_1(U_138) | ~c5_1(U_138) | ~c4_2(U_138, a528)))). % 15.83/5.15 tff(c_1914, plain, (ndr1_1(a560))). % 15.83/5.15 tff(c_1905, plain, (ndr1_1(a582))). % 15.83/5.15 tff(c_1894, plain, (c4_1(a467))). % 15.83/5.15 tff(c_1858, plain, (ndr1_1(a504))). % 15.83/5.15 tff(c_1855, plain, (ndr1_1(a467))). % 15.83/5.15 tff(c_1825, plain, (![U_82]: (c2_1(U_82) | c7_1(U_82) | ~c10_2(U_82, a545)))). % 15.83/5.15 tff(c_1822, plain, (c2_1(a467))). % 15.83/5.15 tff(c_1788, plain, (c10_1(a504))). % 15.83/5.15 tff(c_1784, plain, (![U_139]: (~c2_1(U_139) | ~c5_1(U_139) | ~c2_2(U_139, a528)))). % 15.83/5.15 tff(c_1777, plain, (![U_140]: (~c2_1(U_140) | ~c5_1(U_140) | ~c3_2(U_140, a528)))). % 15.83/5.15 tff(c_1772, plain, (~c10_2(a517, a545))). % 15.83/5.15 tff(c_1765, plain, (![U_81]: (c2_1(U_81) | c7_1(U_81) | ~c4_2(U_81, a545)))). % 15.83/5.15 tff(c_1762, plain, (~c1_1(a582))). % 15.83/5.15 tff(c_1757, plain, (![U_96]: (c1_1(U_96) | ~c2_1(U_96) | ~c1_2(U_96, a546)))). % 15.83/5.15 tff(c_1753, plain, (![U_63]: (c9_1(U_63) | c10_1(U_63) | c7_2(U_63, a474)))). % 15.83/5.15 tff(c_1750, plain, (~c6_2(a515, a516))). % 15.83/5.15 tff(c_1746, plain, (![U_64]: (c10_1(U_64) | c8_1(U_64) | ~c8_2(U_64, a557)))). % 15.83/5.15 tff(c_1741, plain, (~c5_1(a449))). % 15.83/5.15 tff(c_1738, plain, (~c5_1(a493))). % 15.83/5.15 tff(c_1728, plain, (![U_107]: (ndr1_1(U_107) | ~c2_1(U_107) | ~c5_1(U_107)))). % 15.83/5.15 tff(c_1722, plain, (~c10_2(a517, a536))). % 15.83/5.15 tff(c_1712, plain, (~c10_2(a517, a546))). % 15.83/5.15 tff(c_1715, plain, (![U_74]: (c6_1(U_74) | c2_1(U_74) | ~c4_2(U_74, a536)))). % 15.83/5.15 tff(c_1705, plain, (![U_95]: (c1_1(U_95) | ~c2_1(U_95) | ~c4_2(U_95, a546)))). % 15.83/5.15 tff(c_1701, plain, (![U_75]: (c6_1(U_75) | c2_1(U_75) | ~c3_2(U_75, a536)))). % 15.83/5.15 tff(c_1692, plain, (~c10_2(a517, a507))). % 15.83/5.15 tff(c_1695, plain, (![U_62]: (c9_1(U_62) | c10_1(U_62) | c8_2(U_62, a474)))). % 15.83/5.15 tff(c_1691, plain, (~c10_2(a517, a497))). % 15.83/5.15 tff(c_1677, plain, (![U_86]: (c4_2(a517, U_86) | ~c10_2(a517, U_86)))). % 15.83/5.15 tff(c_1670, plain, (![U_73]: (c1_1(U_73) | c7_2(U_73, a546) | ~c2_1(U_73)))). % 15.83/5.15 tff(c_1666, plain, (![U_50]: (c10_1(U_50) | c8_1(U_50) | c1_2(U_50, a557)))). % 15.83/5.15 tff(c_1662, plain, (![U_78]: (c9_1(U_78) | c10_1(U_78) | ~c6_2(U_78, a474)))). % 15.83/5.15 tff(c_1656, plain, (![U_65]: (c10_1(U_65) | c8_1(U_65) | ~c6_2(U_65, a557)))). % 15.83/5.15 tff(c_1653, plain, (~ssSkC1)). % 15.83/5.15 tff(c_1646, plain, (c8_1(a493))). % 15.83/5.15 tff(c_1645, plain, (c1_1(a493))). % 15.83/5.15 tff(c_1641, plain, (c2_1(a493))). % 15.83/5.15 tff(c_1619, plain, (~ndr1_1(a493))). % 15.83/5.15 tff(c_1618, plain, (~ssSkC0)). % 15.83/5.15 tff(c_1615, plain, (~c1_1(a488))). % 15.83/5.15 tff(c_1599, plain, (![U_67]: (c5_1(U_67) | c9_1(U_67) | ~c1_1(U_67)))). % 15.83/5.15 tff(c_1591, plain, (c1_1(a449))). % 15.83/5.15 tff(c_1587, plain, (c10_1(a449))). % 15.83/5.15 tff(c_1586, plain, (c2_1(a449))). % 15.83/5.15 tff(c_1564, plain, (~ndr1_1(a449))). % 15.83/5.15 tff(c_1561, plain, (~c10_2(a515, a516))). % 15.83/5.15 tff(c_1547, plain, (![U_60]: (c6_1(U_60) | c2_1(U_60) | c9_2(U_60, a536)))). % 15.83/5.15 tff(c_1541, plain, (![U_51]: (c2_1(U_51) | c7_1(U_51) | ndr1_1(U_51)))). % 15.83/5.15 tff(c_1537, plain, (![U_48]: (c6_1(U_48) | c2_1(U_48) | ndr1_1(U_48)))). % 15.83/5.15 tff(c_1534, plain, (ssSkC23)). % 15.83/5.15 tff(c_1527, plain, (![U_49]: (c9_1(U_49) | c10_1(U_49) | ndr1_1(U_49)))). % 15.83/5.15 tff(c_1521, plain, (ssSkC22)). % 15.83/5.15 tff(c_1515, plain, (ndr1_1(a515))). % 15.83/5.15 tff(c_1512, plain, (ssSkC15)). % 15.83/5.15 tff(c_1508, plain, (![U_59]: (c1_1(U_59) | ndr1_1(U_59) | ~c2_1(U_59)))). % 15.83/5.15 tff(c_1504, plain, (![U_44]: (c10_1(U_44) | c8_1(U_44) | ndr1_1(U_44)))). % 15.83/5.15 tff(c_1501, plain, (c8_1(a515))). % 15.83/5.15 tff(c_1498, plain, (ssSkC28)). % 15.83/5.15 tff(c_1495, plain, (ssSkC16)). % 15.83/5.15 tff(c_1492, plain, (~c1_1(a597))). % 15.83/5.15 tff(c_1487, plain, (![U_47]: (c7_1(U_47) | ~c1_1(U_47)))). % 15.83/5.15 tff(c_1482, plain, (~ssSkC27)). % 15.83/5.15 tff(c_1472, plain, (ssSkC19)). % 15.83/5.15 tff(c_264, plain, (![U_18]: (ssSkP6(U_18) | c7_2(U_18, a529)))). % 15.83/5.15 tff(c_306, plain, (![U_26]: (ssSkP0(U_26) | c4_2(U_26, a451)))). % 15.83/5.15 tff(c_248, plain, (![U_12]: (ssSkP10(U_12) | c6_2(U_12, a567)))). % 15.83/5.15 tff(c_280, plain, (![U_21]: (ssSkP4(U_21) | c3_2(U_21, a507)))). % 15.83/5.15 tff(c_284, plain, (![U_23]: (ssSkP3(U_23) | c9_2(U_23, a497)))). % 15.83/5.15 tff(c_260, plain, (![U_16]: (ssSkP6(U_16) | c3_2(U_16, a529)))). % 15.83/5.15 tff(c_262, plain, (![U_17]: (ssSkP6(U_17) | c2_2(U_17, a529)))). % 15.83/5.15 tff(c_304, plain, (![U_25]: (ssSkP1(U_25) | c9_2(U_25, a452)))). % 15.83/5.15 tff(c_252, plain, (![U_14]: (ssSkP8(U_14) | c5_2(U_14, a542)))). % 15.83/5.15 tff(c_278, plain, (![U_20]: (ssSkP4(U_20) | c6_2(U_20, a507)))). % 15.83/5.15 tff(c_302, plain, (![U_24]: (ssSkP1(U_24) | c1_2(U_24, a452)))). % 15.83/5.15 tff(c_308, plain, (![U_27]: (ssSkP0(U_27) | c7_2(U_27, a451)))). % 15.83/5.15 tff(c_468, plain, (![U_30]: (ssSkP9(U_30) | ~c9_2(U_30, a564)))). % 15.83/5.15 tff(c_464, plain, (![U_28]: (ssSkP10(U_28) | ~c2_2(U_28, a567)))). % 15.83/5.15 tff(c_486, plain, (![U_37]: (ssSkP3(U_37) | ~c4_2(U_37, a497)))). % 15.83/5.15 tff(c_484, plain, (![U_36]: (ssSkP4(U_36) | ~c4_2(U_36, a507)))). % 15.83/5.15 tff(c_492, plain, (![U_40]: (ssSkP2(U_40) | ~c9_2(U_40, a486)))). % 15.83/5.15 tff(c_502, plain, (![U_41]: (ssSkP1(U_41) | ~c2_2(U_41, a452)))). % 15.83/5.15 tff(c_488, plain, (![U_38]: (ssSkP2(U_38) | ~c1_2(U_38, a486)))). % 15.83/5.15 tff(c_250, plain, (![U_13]: (ssSkP8(U_13) | c1_2(U_13, a542)))). % 15.83/5.15 tff(c_258, plain, (![U_15]: (ssSkP7(U_15) | c5_2(U_15, a531)))). % 15.83/5.15 tff(c_482, plain, (![U_35]: (ssSkP5(U_35) | ~c5_2(U_35, a511)))). % 15.83/5.15 tff(c_476, plain, (![U_34]: (ssSkP7(U_34) | ~c6_2(U_34, a531)))). % 15.83/5.15 tff(c_472, plain, (![U_32]: (ssSkP8(U_32) | ~c6_2(U_32, a542)))). % 15.83/5.15 tff(c_470, plain, (![U_31]: (ssSkP9(U_31) | ~c2_2(U_31, a564)))). % 15.83/5.15 tff(c_466, plain, (![U_29]: (ssSkP10(U_29) | ~c3_2(U_29, a567)))). % 15.83/5.15 tff(c_490, plain, (![U_39]: (ssSkP2(U_39) | ~c2_2(U_39, a486)))). % 15.83/5.15 tff(c_282, plain, (![U_22]: (ssSkP3(U_22) | c2_2(U_22, a497)))). % 15.83/5.15 tff(c_276, plain, (![U_19]: (ssSkP5(U_19) | c6_2(U_19, a511)))). % 15.83/5.15 tff(c_474, plain, (![U_33]: (ssSkP7(U_33) | ~c10_2(U_33, a531)))). % 15.83/5.15 tff(c_108, plain, (![U_4]: (ssSkP7(U_4) | ndr1_1(U_4)))). % 15.83/5.15 tff(c_1357, plain, (c7_2(a478, a480))). % 15.83/5.15 tff(c_1355, plain, (c3_2(a471, a472))). % 15.83/5.16 tff(c_1354, plain, (c8_2(a517, a518))). % 15.83/5.16 tff(c_1348, plain, (~c8_2(a571, a572))). % 15.83/5.16 tff(c_1340, plain, (c2_2(a478, a480))). % 15.83/5.16 tff(c_1337, plain, (c3_2(a478, a479))). % 15.83/5.16 tff(c_110, plain, (![U_5]: (ssSkP6(U_5) | ndr1_1(U_5)))). % 15.83/5.16 tff(c_120, plain, (![U_6]: (ssSkP5(U_6) | ndr1_1(U_6)))). % 15.83/5.16 tff(c_1332, plain, (c6_2(a471, a472))). % 15.83/5.16 tff(c_100, plain, (![U_1]: (ssSkP10(U_1) | ndr1_1(U_1)))). % 15.83/5.16 tff(c_1326, plain, (c8_2(a523, a524))). % 15.83/5.16 tff(c_1325, plain, (c9_2(a575, a576))). % 15.83/5.16 tff(c_1323, plain, (~c1_2(a517, a518))). % 15.83/5.16 tff(c_1322, plain, (~c4_2(a478, a480))). % 15.83/5.16 tff(c_1318, plain, (c9_2(a517, a518))). % 15.83/5.16 tff(c_1317, plain, (~c8_2(a602, a603))). % 15.83/5.16 tff(c_1316, plain, (c5_1(a454))). % 15.83/5.16 tff(c_1315, plain, (~c1_2(a478, a479))). % 15.83/5.16 tff(c_1313, plain, (~ssSkC5)). % 15.83/5.16 tff(c_1307, plain, (~ssSkC6)). % 15.83/5.16 tff(c_1298, plain, (~c7_2(a602, a603))). % 15.83/5.16 tff(c_1297, plain, (~c4_1(a454))). % 15.83/5.16 tff(c_1295, plain, (~c9_1(a454))). % 15.83/5.16 tff(c_148, plain, (![U_10]: (ssSkP1(U_10) | ndr1_1(U_10)))). % 15.83/5.16 tff(c_1292, plain, (~ssSkC17)). % 15.83/5.16 tff(c_1291, plain, (~ssSkC13)). % 15.83/5.16 tff(c_1289, plain, (~ssSkC20)). % 15.83/5.16 tff(c_1285, plain, (c5_2(a575, a576))). % 15.83/5.16 tff(c_130, plain, (![U_9]: (ssSkP2(U_9) | ndr1_1(U_9)))). % 15.83/5.16 tff(c_1275, plain, (~c1_2(a597, a598))). % 15.83/5.16 tff(c_1274, plain, (~ssSkC14)). % 15.83/5.16 tff(c_1272, plain, (~c9_2(a597, a598))). % 15.83/5.16 tff(c_122, plain, (![U_7]: (ssSkP4(U_7) | ndr1_1(U_7)))). % 15.83/5.16 tff(c_1264, plain, (~ssSkC7)). % 15.83/5.16 tff(c_1262, plain, (~ssSkC30)). % 15.83/5.16 tff(c_1260, plain, (c4_2(a523, a524))). % 15.83/5.16 tff(c_150, plain, (![U_11]: (ssSkP0(U_11) | ndr1_1(U_11)))). % 15.83/5.16 tff(c_124, plain, (![U_8]: (ssSkP3(U_8) | ndr1_1(U_8)))). % 15.83/5.16 tff(c_1253, plain, (~c4_2(a471, a472))). % 15.83/5.16 tff(c_1252, plain, (~c4_2(a597, a598))). % 15.83/5.16 tff(c_1251, plain, (~c2_2(a523, a524))). % 15.83/5.16 tff(c_1250, plain, (~c8_2(a575, a576))). % 15.83/5.16 tff(c_1249, plain, (~c8_2(a478, a479))). % 15.83/5.16 tff(c_1248, plain, (~ssSkC26)). % 15.83/5.16 tff(c_1246, plain, (~ssSkC25)). % 15.83/5.16 tff(c_1241, plain, (~c6_2(a602, a603))). % 15.83/5.16 tff(c_102, plain, (![U_2]: (ssSkP9(U_2) | ndr1_1(U_2)))). % 15.83/5.16 tff(c_104, plain, (![U_3]: (ssSkP8(U_3) | ndr1_1(U_3)))). % 15.83/5.16 tff(c_1235, plain, (c9_2(a571, a572))). % 15.83/5.16 tff(c_1234, plain, (~ssSkC10)). % 15.83/5.16 tff(c_1233, plain, (~c1_0)). % 15.83/5.16 tff(c_1228, plain, (~ssSkC12)). % 15.83/5.16 tff(c_1223, plain, (c8_1(a449))). % 15.83/5.16 tff(c_1222, plain, (~c3_1(a523))). % 15.83/5.16 tff(c_1219, plain, (c7_1(a478))). % 15.83/5.16 tff(c_1213, plain, (~c3_1(a571))). % 15.83/5.16 tff(c_1204, plain, (c9_1(a471))). % 15.83/5.16 tff(c_1202, plain, (c6_1(a469))). % 15.83/5.16 tff(c_1198, plain, (~c8_0)). % 15.83/5.16 tff(c_1195, plain, (c3_1(a449))). % 15.83/5.16 tff(c_1194, plain, (c9_1(a517))). % 15.83/5.16 tff(c_1192, plain, (~c8_1(a455))). % 15.83/5.16 tff(c_1191, plain, (~c5_1(a585))). % 15.83/5.16 tff(c_1190, plain, (c9_1(a455))). % 15.83/5.16 tff(c_1189, plain, (~c7_1(a597))). % 15.83/5.16 tff(c_1186, plain, (~c8_1(a537))). % 15.83/5.16 tff(c_1185, plain, (c10_1(a469))). % 15.83/5.16 tff(c_1182, plain, (c9_1(a493))). % 15.83/5.16 tff(c_1181, plain, (c4_1(a523))). % 15.83/5.16 tff(c_1180, plain, (~c3_1(a471))). % 15.83/5.16 tff(c_1177, plain, (c7_1(a575))). % 15.83/5.16 tff(c_1176, plain, (c9_1(a592))). % 15.83/5.16 tff(c_1174, plain, (~c9_1(a537))). % 15.83/5.16 tff(c_1173, plain, (ndr1_1(a478))). % 15.83/5.16 tff(c_1172, plain, (~c9_1(a488))). % 15.83/5.16 tff(c_1171, plain, (ndr1_1(a523))). % 15.83/5.16 tff(c_1170, plain, (ndr1_1(a471))). % 15.83/5.16 tff(c_1169, plain, (c2_1(a488))). % 15.83/5.16 tff(c_1168, plain, (c5_1(a601))). % 15.83/5.16 tff(c_1167, plain, (~c8_1(a592))). % 15.83/5.16 tff(c_1166, plain, (c5_1(a537))). % 15.83/5.16 tff(c_1165, plain, (~c10_1(a601))). % 15.83/5.16 tff(c_1164, plain, (ndr1_1(a597))). % 15.83/5.16 tff(c_1163, plain, (ndr1_1(a575))). % 15.83/5.16 tff(c_1162, plain, (c1_1(a455))). % 15.83/5.16 tff(c_1161, plain, (ndr1_1(a517))). % 15.83/5.16 tff(c_1160, plain, (c9_1(a585))). % 15.83/5.16 tff(c_1156, plain, (c5_1(a575))). % 15.83/5.16 tff(c_1148, plain, (~c2_0)). % 15.83/5.16 tff(c_1145, plain, (c7_1(a602))). % 15.83/5.16 tff(c_1144, plain, (ndr1_1(a602))). % 15.83/5.16 tff(c_1139, plain, (c10_0)). % 15.83/5.16 tff(c_1135, plain, (c5_1(a571))). % 15.83/5.16 tff(c_1134, plain, (ndr1_1(a571))). % 15.83/5.16 tff(c_1107, plain, (c9_0)). % 15.83/5.16 tff(c_1099, plain, (c5_0)). % 15.83/5.16 tff(c_1098, plain, (~c4_0)). % 15.83/5.16 tff(c_1097, plain, (ndr1_0)). % 15.83/5.16 tff(c_1096, plain, (~c3_0)). % 15.83/5.16 tff(c_1095, plain, (~c7_0)). % 15.83/5.16 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.83/5.16 %------------------------------------------------------------------------------