%------------------------------------------------------------------------------ % 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 : n024.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 : CounterSatisfiable 19.49s 6.86s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SYN547+1 : TPTP v9.0.0. Released v2.1.0. % 0.13/0.14 % 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.35 % Computer : n024.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:59:36 EDT 2025 % 0.20/0.36 % CPUTime : % 19.49/6.86 % 19.49/6.86 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.49/6.86 % 19.49/6.86 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.71/6.88 %$ c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ndr1_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ndr1_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > 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 % 19.71/6.88 % 19.71/6.88 %Foreground sorts: % 19.71/6.88 % 19.71/6.88 % 19.71/6.88 %Background operators: % 19.71/6.88 % 19.71/6.88 % 19.71/6.88 %Foreground operators: % 19.71/6.88 tff(a565, type, a565: $i). % 19.71/6.88 tff(c7_0, type, c7_0: $o). % 19.71/6.88 tff(a492, type, a492: $i). % 19.71/6.88 tff(a544, type, a544: $i). % 19.71/6.88 tff(a577, type, a577: $i). % 19.71/6.88 tff(a586, type, a586: $i). % 19.71/6.88 tff(a473, type, a473: $i). % 19.71/6.88 tff(a601, type, a601: $i). % 19.71/6.88 tff(a506, type, a506: $i). % 19.71/6.88 tff(a457, type, a457: $i). % 19.71/6.88 tff(a600, type, a600: $i). % 19.71/6.88 tff(a580, type, a580: $i). % 19.71/6.88 tff(a535, type, a535: $i). % 19.71/6.88 tff(a542, type, a542: $i). % 19.71/6.88 tff(c4_0, type, c4_0: $o). % 19.71/6.88 tff(a541, type, a541: $i). % 19.71/6.88 tff(a556, type, a556: $i). % 19.71/6.88 tff(a550, type, a550: $i). % 19.71/6.88 tff(c3_0, type, c3_0: $o). % 19.71/6.88 tff(a477, type, a477: $i). % 19.71/6.88 tff(a460, type, a460: $i). % 19.71/6.88 tff(a594, type, a594: $i). % 19.71/6.88 tff(a490, type, a490: $i). % 19.71/6.88 tff(a567, type, a567: $i). % 19.71/6.88 tff(a484, type, a484: $i). % 19.71/6.88 tff(c1_2, type, c1_2: ($i * $i) > $o). % 19.71/6.88 tff(a503, type, a503: $i). % 19.71/6.88 tff(a585, type, a585: $i). % 19.71/6.88 tff(a471, type, a471: $i). % 19.71/6.88 tff(a520, type, a520: $i). % 19.71/6.88 tff(a495, type, a495: $i). % 19.71/6.88 tff(a502, type, a502: $i). % 19.71/6.88 tff(a493, type, a493: $i). % 19.71/6.88 tff(a537, type, a537: $i). % 19.71/6.88 tff(a511, type, a511: $i). % 19.71/6.88 tff(a564, type, a564: $i). % 19.71/6.88 tff(a508, type, a508: $i). % 19.71/6.88 tff(a510, type, a510: $i). % 19.71/6.88 tff(a487, type, a487: $i). % 19.71/6.88 tff(a488, type, a488: $i). % 19.71/6.88 tff(a530, type, a530: $i). % 19.71/6.88 tff(a553, type, a553: $i). % 19.71/6.88 tff(a569, type, a569: $i). % 19.71/6.88 tff(a528, type, a528: $i). % 19.71/6.88 tff(a462, type, a462: $i). % 19.71/6.88 tff(a458, type, a458: $i). % 19.71/6.88 tff(c8_0, type, c8_0: $o). % 19.71/6.88 tff(a536, type, a536: $i). % 19.71/6.88 tff(a459, type, a459: $i). % 19.71/6.88 tff(a467, type, a467: $i). % 19.71/6.88 tff(a461, type, a461: $i). % 19.71/6.88 tff(a596, type, a596: $i). % 19.71/6.88 tff(a498, type, a498: $i). % 19.71/6.88 tff(a505, type, a505: $i). % 19.71/6.88 tff(a456, type, a456: $i). % 19.71/6.88 tff(a532, type, a532: $i). % 19.71/6.88 tff(a504, type, a504: $i). % 19.71/6.88 tff(a468, type, a468: $i). % 19.71/6.88 tff(c5_0, type, c5_0: $o). % 19.71/6.88 tff(a539, type, a539: $i). % 19.71/6.88 tff(a551, type, a551: $i). % 19.71/6.88 tff(a572, type, a572: $i). % 19.71/6.88 tff(a518, type, a518: $i). % 19.71/6.88 tff(a546, type, a546: $i). % 19.71/6.88 tff(a599, type, a599: $i). % 19.71/6.88 tff(c6_0, type, c6_0: $o). % 19.71/6.88 tff(c8_2, type, c8_2: ($i * $i) > $o). % 19.71/6.88 tff(a602, type, a602: $i). % 19.71/6.88 tff(a570, type, a570: $i). % 19.71/6.88 tff(a499, type, a499: $i). % 19.71/6.88 tff(a533, type, a533: $i). % 19.71/6.88 tff(a500, type, a500: $i). % 19.71/6.88 tff(a472, type, a472: $i). % 19.71/6.88 tff(a470, type, a470: $i). % 19.71/6.88 tff(a598, type, a598: $i). % 19.71/6.88 tff(a516, type, a516: $i). % 19.71/6.88 tff(a524, type, a524: $i). % 19.71/6.88 tff(a563, type, a563: $i). % 19.71/6.88 tff(a571, type, a571: $i). % 19.71/6.88 tff(a543, type, a543: $i). % 19.71/6.88 tff(a509, type, a509: $i). % 19.71/6.88 tff(a589, type, a589: $i). % 19.71/6.88 tff(a558, type, a558: $i). % 19.71/6.88 tff(c1_0, type, c1_0: $o). % 19.71/6.88 tff(c8_1, type, c8_1: $i > $o). % 19.71/6.88 tff(a465, type, a465: $i). % 19.71/6.88 tff(a469, type, a469: $i). % 19.71/6.88 tff(c2_1, type, c2_1: $i > $o). % 19.71/6.88 tff(a549, type, a549: $i). % 19.71/6.88 tff(a555, type, a555: $i). % 19.71/6.88 tff(ndr1_1, type, ndr1_1: $i > $o). % 19.71/6.88 tff(c2_0, type, c2_0: $o). % 19.71/6.88 tff(c4_1, type, c4_1: $i > $o). % 19.71/6.88 tff(a529, type, a529: $i). % 19.71/6.88 tff(a475, type, a475: $i). % 19.71/6.88 tff(a557, type, a557: $i). % 19.71/6.88 tff(a575, type, a575: $i). % 19.71/6.88 tff(a597, type, a597: $i). % 19.71/6.88 tff(a591, type, a591: $i). % 19.71/6.88 tff(a494, type, a494: $i). % 19.71/6.88 tff(a545, type, a545: $i). % 19.71/6.88 tff(a491, type, a491: $i). % 19.71/6.88 tff(a562, type, a562: $i). % 19.71/6.88 tff(a463, type, a463: $i). % 19.71/6.88 tff(a474, type, a474: $i). % 19.71/6.88 tff(a581, type, a581: $i). % 19.71/6.88 tff(a568, type, a568: $i). % 19.71/6.88 tff(a593, type, a593: $i). % 19.71/6.88 tff(a479, type, a479: $i). % 19.71/6.88 tff(a489, type, a489: $i). % 19.71/6.88 tff(a584, type, a584: $i). % 19.71/6.88 tff(a482, type, a482: $i). % 19.71/6.88 tff(a603, type, a603: $i). % 19.71/6.88 tff(c6_2, type, c6_2: ($i * $i) > $o). % 19.71/6.88 tff(a507, type, a507: $i). % 19.71/6.88 tff(a587, type, a587: $i). % 19.71/6.88 tff(a578, type, a578: $i). % 19.71/6.88 tff(a559, type, a559: $i). % 19.71/6.88 tff(a478, type, a478: $i). % 19.71/6.88 tff(a464, type, a464: $i). % 19.71/6.88 tff(a552, type, a552: $i). % 19.71/6.88 tff(a548, type, a548: $i). % 19.71/6.88 tff(a534, type, a534: $i). % 19.71/6.88 tff(a588, type, a588: $i). % 19.71/6.88 tff(a525, type, a525: $i). % 19.71/6.88 tff(a523, type, a523: $i). % 19.71/6.88 tff(a595, type, a595: $i). % 19.71/6.88 tff(a531, type, a531: $i). % 19.71/6.88 tff(a522, type, a522: $i). % 19.71/6.88 tff(a573, type, a573: $i). % 19.71/6.88 tff(ndr1_0, type, ndr1_0: $o). % 19.71/6.88 tff(a480, type, a480: $i). % 19.71/6.88 tff(a485, type, a485: $i). % 19.71/6.88 tff(a476, type, a476: $i). % 19.71/6.88 tff(a483, type, a483: $i). % 19.71/6.88 tff(a538, type, a538: $i). % 19.71/6.88 tff(a501, type, a501: $i). % 19.71/6.88 tff(a486, type, a486: $i). % 19.71/6.88 tff(a547, type, a547: $i). % 19.71/6.88 tff(a527, type, a527: $i). % 19.71/6.88 tff(a526, type, a526: $i). % 19.71/6.88 tff(a576, type, a576: $i). % 19.71/6.88 tff(a561, type, a561: $i). % 19.71/6.88 tff(a481, type, a481: $i). % 19.71/6.88 tff(c1_1, type, c1_1: $i > $o). % 19.71/6.88 tff(a497, type, a497: $i). % 19.71/6.88 tff(a521, type, a521: $i). % 19.71/6.88 tff(c5_2, type, c5_2: ($i * $i) > $o). % 19.71/6.88 tff(a496, type, a496: $i). % 19.71/6.88 tff(a540, type, a540: $i). % 19.71/6.88 tff(a519, type, a519: $i). % 19.71/6.88 tff(c7_1, type, c7_1: $i > $o). % 19.71/6.88 tff(c6_1, type, c6_1: $i > $o). % 19.71/6.88 tff(a590, type, a590: $i). % 19.71/6.88 tff(c4_2, type, c4_2: ($i * $i) > $o). % 19.71/6.88 tff(a517, type, a517: $i). % 19.71/6.88 tff(a560, type, a560: $i). % 19.71/6.88 tff(a582, type, a582: $i). % 19.71/6.88 tff(a566, type, a566: $i). % 19.71/6.88 tff(a554, type, a554: $i). % 19.71/6.88 tff(a515, type, a515: $i). % 19.71/6.88 tff(c5_1, type, c5_1: $i > $o). % 19.71/6.88 tff(c7_2, type, c7_2: ($i * $i) > $o). % 19.71/6.88 tff(a583, type, a583: $i). % 19.71/6.88 tff(c3_2, type, c3_2: ($i * $i) > $o). % 19.71/6.88 tff(a514, type, a514: $i). % 19.71/6.88 tff(a466, type, a466: $i). % 19.71/6.88 tff(c2_2, type, c2_2: ($i * $i) > $o). % 19.71/6.88 tff(a513, type, a513: $i). % 19.71/6.88 tff(a512, type, a512: $i). % 19.71/6.88 tff(a574, type, a574: $i). % 19.71/6.88 tff(a592, type, a592: $i). % 19.71/6.88 tff(c3_1, type, c3_1: $i > $o). % 19.71/6.88 tff(a579, type, a579: $i). % 19.71/6.88 % 19.71/6.88 %Saturated clause set: % 19.71/6.88 tff(c_7563, plain, (~c4_1(a566))). % 19.71/6.88 tff(c_7556, plain, (~c5_2(a566, a465))). % 19.71/6.88 tff(c_7457, plain, (![X130_179, X131_181]: (~c5_2(X130_179, a465) | c8_1(X130_179) | c5_2(X130_179, X131_181) | c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.88 tff(c_7526, plain, (~c2_2(a577, a578))). % 19.71/6.88 tff(c_7525, plain, (~c1_2(a566, a465))). % 19.71/6.88 tff(c_7486, plain, (![X130_179, X131_181]: (~c1_2(X130_179, a465) | c8_1(X130_179) | c5_2(X130_179, X131_181) | c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.88 tff(c_7501, plain, (~c8_1(a587))). % 19.71/6.88 tff(c_7495, plain, (~ndr1_1(a587))). % 19.71/6.88 tff(c_7494, plain, (~c6_2(a498, a499))). % 19.71/6.88 tff(c_7437, plain, (![X4_13, X5_15]: (~c1_2(X4_13, a465) | c8_1(X4_13) | ~c7_2(X4_13, X5_15) | c5_2(X4_13, X5_15) | ~c6_2(X4_13, X5_15) | ~ndr1_1(X4_13)))). % 19.71/6.88 tff(c_7466, plain, (~c6_2(a546, a547))). % 19.71/6.88 tff(c_7465, plain, (~c6_2(a559, a560))). % 19.71/6.89 tff(c_7436, plain, (![X4_13, X5_15]: (~c5_2(X4_13, a465) | c8_1(X4_13) | ~c7_2(X4_13, X5_15) | c5_2(X4_13, X5_15) | ~c6_2(X4_13, X5_15) | ~ndr1_1(X4_13)))). % 19.71/6.89 tff(c_7425, plain, (![X130_179, X131_181]: (c8_1(X130_179) | c5_2(X130_179, X131_181) | ~c6_2(X130_179, a465) | ~c2_2(X130_179, a465) | c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.89 tff(c_7404, plain, (![X130_179, X5_355]: (c8_1(X130_179) | ~c7_2(X130_179, X5_355) | c5_2(X130_179, X5_355) | ~c6_2(X130_179, X5_355) | c7_1(X130_179) | ~c6_2(X130_179, a465) | ~c2_2(X130_179, a465) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.89 tff(c_7399, plain, (![X4_13, X5_15]: (~c7_2(X4_13, a465) | c8_1(X4_13) | ~c7_2(X4_13, X5_15) | c5_2(X4_13, X5_15) | ~c6_2(X4_13, X5_15) | ~ndr1_1(X4_13)))). % 19.71/6.89 tff(c_7393, plain, (c3_1(a587))). % 19.71/6.89 tff(c_7386, plain, (~c6_2(a577, a579))). % 19.71/6.89 tff(c_7332, plain, (c8_2(a577, a578))). % 19.71/6.89 tff(c_7325, plain, (~c1_1(a577))). % 19.71/6.89 tff(c_7323, plain, (~c4_2(a577, a579))). % 19.71/6.89 tff(c_7320, plain, (c2_2(a577, a579))). % 19.71/6.89 tff(c_7290, plain, (~c2_2(a577, a557))). % 19.71/6.89 tff(c_7291, plain, (~c8_2(a577, a579))). % 19.71/6.89 tff(c_7286, plain, (c1_2(a577, a578))). % 19.71/6.89 tff(c_7241, plain, (~c3_2(a577, a578))). % 19.71/6.89 tff(c_7144, plain, (c6_2(a577, a578))). % 19.71/6.89 tff(c_6622, plain, (![X100_138, X101_140]: (~c1_1(X100_138) | c3_2(X100_138, a479) | c2_2(X100_138, a479) | ~c6_2(X100_138, a548) | ~c2_2(X100_138, a548) | c4_1(X100_138) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.89 tff(c_6611, plain, (![X100_138, X101_140]: (~c1_1(X100_138) | c3_2(X100_138, a479) | c2_2(X100_138, a479) | ~c6_2(X100_138, a548) | ~c2_2(X100_138, a548) | c4_1(X100_138) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.89 tff(c_7141, plain, (~c8_1(a573))). % 19.71/6.89 tff(c_7135, plain, (~ndr1_1(a573))). % 19.71/6.89 tff(c_7133, plain, (ndr1_1(a577))). % 19.71/6.89 tff(c_7132, plain, (~c7_1(a577))). % 19.71/6.89 tff(c_7131, plain, (~c7_1(a566))). % 19.71/6.89 tff(c_7114, plain, (![X22_37, X23_39]: (~c6_2(X22_37, X23_39) | c4_2(X22_37, X23_39) | c1_2(X22_37, X23_39) | ~ndr1_1(X22_37) | ~c7_1(X22_37) | c6_1(X22_37)))). % 19.71/6.89 tff(c_7084, plain, (![X100_344]: (~c3_1(X100_344) | ~c2_2(X100_344, a479) | c4_1(X100_344) | ~c8_1(X100_344) | c1_2(X100_344, a459) | c1_2(X100_344, a557) | c7_1(X100_344) | c2_2(X100_344, a459) | ~ndr1_1(X100_344)))). % 19.71/6.89 tff(c_7045, plain, (![X100_138, X101_267]: (~c2_2(X100_138, a479) | c4_1(X100_138) | ~c8_1(X100_138) | c1_2(X100_138, X101_267) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_267) | ~ndr1_1(X100_138) | c3_2(X100_138, X101_267)))). % 19.71/6.89 tff(c_7029, plain, (![X100_338]: (~c3_1(X100_338) | ~c2_2(X100_338, a479) | c4_1(X100_338) | ~c8_1(X100_338) | c1_2(X100_338, a459) | ~c2_2(X100_338, a557) | c7_1(X100_338) | c2_2(X100_338, a459) | ~ndr1_1(X100_338)))). % 19.71/6.89 tff(c_6990, plain, (![X100_138, X101_265]: (~c2_2(X100_138, a479) | c4_1(X100_138) | ~c8_1(X100_138) | c1_2(X100_138, X101_265) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_265) | ~ndr1_1(X100_138) | c3_2(X100_138, X101_265)))). % 19.71/6.89 tff(c_6967, plain, (![X130_179, X131_181]: (~c1_1(X130_179) | c3_2(X130_179, X131_181) | ~c2_1(X130_179) | c8_1(X130_179) | ~c4_2(X130_179, X131_181) | ~c6_2(X130_179, a548) | ~c2_2(X130_179, a548) | c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.89 tff(c_6575, plain, (![X130_179, X11_285]: (~c1_1(X130_179) | c3_2(X130_179, X11_285) | ~c6_2(X130_179, X11_285) | ~c2_1(X130_179) | c8_1(X130_179) | ~c7_2(X130_179, X11_285) | ~c4_2(X130_179, X11_285) | c7_1(X130_179) | ~c6_2(X130_179, a548) | ~c2_2(X130_179, a548) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.89 tff(c_6702, plain, (![X100_138, X101_140]: (~c4_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, a479) | c2_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.89 tff(c_6933, plain, (![X100_138]: (c2_2(X100_138, a548) | ~c1_1(X100_138) | ~c8_1(X100_138) | c1_2(X100_138, a479) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, a479) | ~ndr1_1(X100_138) | c3_2(X100_138, a479)))). % 19.71/6.89 tff(c_6540, plain, (![X100_138, X101_140]: (c2_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, a479) | c2_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.89 tff(c_6908, plain, (![X100_138]: (c2_2(X100_138, a548) | ~c1_1(X100_138) | ~c8_1(X100_138) | c1_2(X100_138, a479) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, a479) | ~ndr1_1(X100_138) | c3_2(X100_138, a479)))). % 19.71/6.90 tff(c_6566, plain, (![X100_138, X101_140]: (c2_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, a479) | c2_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6688, plain, (![X100_138, X101_140]: (~c4_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, a479) | c2_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6887, plain, (![X_5]: (c1_2(X_5, a572) | ~c1_2(X_5, a459) | c2_2(X_5, a459) | ~c5_1(X_5) | ~c4_1(X_5) | ~ndr1_1(X_5) | ~c8_1(X_5) | ~c3_1(X_5) | c2_2(X_5, a572)))). % 19.71/6.90 tff(c_6870, plain, (![X_5, X112_316]: (c1_2(X_5, X112_316) | ~c1_2(X_5, a459) | c2_2(X_5, a459) | ~c5_1(X_5) | c2_2(X_5, a572) | ~c4_1(X_5) | c2_2(X_5, X112_316) | ~ndr1_1(X_5) | ~c8_1(X_5) | ~c3_1(X_5)))). % 19.71/6.90 tff(c_6843, plain, (![X111_152, X112_154, X46_314]: (c1_2(X111_152, X112_154) | ~c1_2(X111_152, X46_314) | c2_2(X111_152, X46_314) | ~c7_2(X111_152, X46_314) | ~c5_1(X111_152) | c2_2(X111_152, a572) | ~c4_1(X111_152) | c2_2(X111_152, X112_154) | ~ndr1_1(X111_152)))). % 19.71/6.90 tff(c_6850, plain, (~c5_1(a482))). % 19.71/6.90 tff(c_6849, plain, (~c3_1(a491))). % 19.71/6.90 tff(c_6844, plain, (~ndr1_1(a491))). % 19.71/6.90 tff(c_6834, plain, (![X45_67, X47_71, X46_70]: (c2_2(X45_67, X47_71) | ~c5_2(X45_67, X47_71) | c1_2(X45_67, X47_71) | ~c1_2(X45_67, X46_70) | c2_2(X45_67, X46_70) | ~c7_2(X45_67, X46_70) | ~ndr1_1(X45_67) | ~c5_1(X45_67)))). % 19.71/6.90 tff(c_6816, plain, (![X32_51, X33_53]: (c2_2(X32_51, a481) | c8_1(X32_51) | ~c3_2(X32_51, X33_53) | ~c6_2(X32_51, X33_53) | c4_2(X32_51, X33_53) | ~ndr1_1(X32_51)))). % 19.71/6.90 tff(c_6795, plain, (~c3_2(a566, a567))). % 19.71/6.90 tff(c_6781, plain, (![X32_51, X33_53]: (c8_2(X32_51, a481) | c8_1(X32_51) | ~c3_2(X32_51, X33_53) | ~c6_2(X32_51, X33_53) | c4_2(X32_51, X33_53) | ~ndr1_1(X32_51)))). % 19.71/6.90 tff(c_6738, plain, (![X130_179, X131_181]: (~c4_2(X130_179, a548) | ~c1_1(X130_179) | c3_2(X130_179, X131_181) | ~c2_1(X130_179) | c8_1(X130_179) | ~c4_2(X130_179, X131_181) | c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.90 tff(c_6595, plain, (![X130_179, X131_181]: (c2_2(X130_179, a548) | ~c1_1(X130_179) | c3_2(X130_179, X131_181) | ~c2_1(X130_179) | c8_1(X130_179) | ~c4_2(X130_179, X131_181) | c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.90 tff(c_6667, plain, (![X10_22, X11_24]: (~c4_2(X10_22, a548) | ~c1_1(X10_22) | c3_2(X10_22, X11_24) | ~c6_2(X10_22, X11_24) | ~c2_1(X10_22) | c8_1(X10_22) | ~c7_2(X10_22, X11_24) | ~c4_2(X10_22, X11_24) | ~ndr1_1(X10_22)))). % 19.71/6.90 tff(c_6673, plain, (![X100_138, X101_140]: (~c4_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | ~c6_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6672, plain, (![X100_138, X101_140]: (~c4_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6671, plain, (![X100_138, X101_140]: (~c4_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6641, plain, (![X92_128, X93_130]: (~c4_2(X92_128, a548) | ~c1_1(X92_128) | c3_2(X92_128, X93_130) | ~c8_2(X92_128, X93_130) | ~c6_2(X92_128, X93_130) | ~ndr1_1(X92_128)))). % 19.71/6.90 tff(c_6518, plain, (![X130_179, X101_273]: (~c1_1(X130_179) | c3_2(X130_179, X101_273) | ~c6_2(X130_179, X101_273) | ~c6_2(X130_179, a557) | c2_2(X130_179, X101_273) | c7_1(X130_179) | ~c6_2(X130_179, a548) | ~c2_2(X130_179, a548) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.90 tff(c_6523, plain, (![X130_179, X101_275]: (~c1_1(X130_179) | c3_2(X130_179, X101_275) | ~c6_2(X130_179, X101_275) | ~c2_2(X130_179, a557) | c2_2(X130_179, X101_275) | c7_1(X130_179) | ~c6_2(X130_179, a548) | ~c2_2(X130_179, a548) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.90 tff(c_6528, plain, (![X130_179, X101_277]: (~c1_1(X130_179) | c3_2(X130_179, X101_277) | ~c6_2(X130_179, X101_277) | c1_2(X130_179, a557) | c2_2(X130_179, X101_277) | c7_1(X130_179) | ~c6_2(X130_179, a548) | ~c2_2(X130_179, a548) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.90 tff(c_6504, plain, (![X10_22, X11_24]: (c2_2(X10_22, a548) | ~c1_1(X10_22) | c3_2(X10_22, X11_24) | ~c6_2(X10_22, X11_24) | ~c2_1(X10_22) | c8_1(X10_22) | ~c7_2(X10_22, X11_24) | ~c4_2(X10_22, X11_24) | ~ndr1_1(X10_22)))). % 19.71/6.90 tff(c_6465, plain, (![X10_22, X11_24]: (~c7_2(X10_22, a548) | ~c1_1(X10_22) | c3_2(X10_22, X11_24) | ~c6_2(X10_22, X11_24) | ~c2_1(X10_22) | c8_1(X10_22) | ~c7_2(X10_22, X11_24) | ~c4_2(X10_22, X11_24) | ~ndr1_1(X10_22)))). % 19.71/6.90 tff(c_6509, plain, (![X100_138, X101_140]: (c2_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6510, plain, (![X100_138, X101_140]: (c2_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | ~c6_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6508, plain, (![X100_138, X101_140]: (c2_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6469, plain, (![X100_138, X101_140]: (~c7_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6470, plain, (![X100_138, X101_140]: (~c7_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6471, plain, (![X100_138, X101_140]: (~c7_2(X100_138, a548) | ~c1_1(X100_138) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, X101_140) | ~c6_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.90 tff(c_6478, plain, (![X92_128, X93_130]: (c2_2(X92_128, a548) | ~c1_1(X92_128) | c3_2(X92_128, X93_130) | ~c8_2(X92_128, X93_130) | ~c6_2(X92_128, X93_130) | ~ndr1_1(X92_128)))). % 19.71/6.90 tff(c_6475, plain, (~c6_2(a498, a500))). % 19.71/6.90 tff(c_6439, plain, (![X92_128, X93_130]: (~c7_2(X92_128, a548) | ~c1_1(X92_128) | c3_2(X92_128, X93_130) | ~c8_2(X92_128, X93_130) | ~c6_2(X92_128, X93_130) | ~ndr1_1(X92_128)))). % 19.71/6.90 tff(c_6291, plain, (![X130_179, X101_259]: (~c8_1(X130_179) | c1_2(X130_179, X101_259) | c3_2(X130_179, X101_259) | ~c6_2(X130_179, a557) | c2_2(X130_179, X101_259) | c7_1(X130_179) | ~c6_2(X130_179, a479) | ~c2_2(X130_179, a479) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.90 tff(c_6421, plain, (~c3_1(a514))). % 19.71/6.90 tff(c_6416, plain, (~ndr1_1(a514))). % 19.71/6.90 tff(c_6415, plain, (~c2_1(a559))). % 19.71/6.90 tff(c_6413, plain, (~c2_2(a534, a479))). % 19.71/6.90 tff(c_6412, plain, (c4_2(a534, a535))). % 19.71/6.90 tff(c_6409, plain, (~c4_1(a559))). % 19.71/6.90 tff(c_6396, plain, (c7_2(a559, a560))). % 19.71/6.90 tff(c_6393, plain, (c3_2(a534, a535))). % 19.71/6.90 tff(c_6386, plain, (~c7_2(a534, a479))). % 19.71/6.90 tff(c_6385, plain, (~c6_2(a534, a535))). % 19.71/6.90 tff(c_6364, plain, (c8_2(a534, a535))). % 19.71/6.90 tff(c_6361, plain, (c4_2(a559, a560))). % 19.71/6.90 tff(c_6180, plain, (![X130_179, X131_181]: (c3_2(X130_179, X131_181) | c1_2(X130_179, X131_181) | ~c2_1(X130_179) | c8_1(X130_179) | ~c4_2(X130_179, X131_181) | c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.90 tff(c_6338, plain, (c8_1(a534))). % 19.71/6.90 tff(c_6335, plain, (c3_1(a573))). % 19.71/6.90 tff(c_6333, plain, (~c2_1(a534))). % 19.71/6.90 tff(c_6330, plain, (ndr1_1(a534))). % 19.71/6.90 tff(c_6327, plain, (~c6_1(a559))). % 19.71/6.90 tff(c_6323, plain, (c1_1(a573))). % 19.71/6.90 tff(c_6320, plain, (c7_1(a559))). % 19.71/6.90 tff(c_6317, plain, (~c3_1(a592))). % 19.71/6.90 tff(c_6312, plain, (~ndr1_1(a592))). % 19.71/6.90 tff(c_6310, plain, (ndr1_1(a559))). % 19.71/6.90 tff(c_6305, plain, (~c5_1(a531))). % 19.71/6.90 tff(c_6304, plain, (~c6_1(a531))). % 19.71/6.90 tff(c_6293, plain, (c4_1(a531))). % 19.71/6.91 tff(c_6272, plain, (![X100_138, X101_140]: (~c7_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6271, plain, (![X100_138, X101_140]: (~c7_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6270, plain, (![X100_138, X101_140]: (~c7_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6246, plain, (![X29_47, X30_49]: (~c7_2(X29_47, a479) | ~c8_1(X29_47) | ~c8_2(X29_47, X30_49) | c1_2(X29_47, X30_49) | c3_2(X29_47, X30_49) | ~ndr1_1(X29_47)))). % 19.71/6.91 tff(c_6232, plain, (![X100_138, X101_140]: (c6_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | ~c6_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6231, plain, (![X100_138, X101_140]: (c6_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6230, plain, (![X100_138, X101_140]: (c6_2(X100_138, a479) | ~c8_1(X100_138) | c1_2(X100_138, X101_140) | c3_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6206, plain, (![X29_47, X30_49]: (c6_2(X29_47, a479) | ~c8_1(X29_47) | ~c8_2(X29_47, X30_49) | c1_2(X29_47, X30_49) | c3_2(X29_47, X30_49) | ~ndr1_1(X29_47)))). % 19.71/6.91 tff(c_6160, plain, (![X100_138, X101_140]: (c4_1(X100_138) | c8_1(X100_138) | c3_2(X100_138, X101_140) | c1_2(X100_138, X101_140) | ~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6161, plain, (![X100_138, X101_140]: (c4_1(X100_138) | c8_1(X100_138) | c3_2(X100_138, X101_140) | c1_2(X100_138, X101_140) | ~c6_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6159, plain, (![X100_138, X101_140]: (c4_1(X100_138) | c8_1(X100_138) | c3_2(X100_138, X101_140) | c1_2(X100_138, X101_140) | c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6155, plain, (![X10_22, X11_24]: (c4_1(X10_22) | c3_2(X10_22, X11_24) | c1_2(X10_22, X11_24) | ~c2_1(X10_22) | c8_1(X10_22) | ~c7_2(X10_22, X11_24) | ~c4_2(X10_22, X11_24) | ~ndr1_1(X10_22)))). % 19.71/6.91 tff(c_6166, plain, (c1_2(a498, a500))). % 19.71/6.91 tff(c_6135, plain, (![X149_204, X150_206]: (c4_1(X149_204) | c8_1(X149_204) | c3_2(X149_204, X150_206) | c1_2(X149_204, X150_206) | ~c8_2(X149_204, X150_206) | ~ndr1_1(X149_204)))). % 19.71/6.91 tff(c_6133, plain, (~c4_2(a566, a567))). % 19.71/6.91 tff(c_6132, plain, (~c4_2(a546, a547))). % 19.71/6.91 tff(c_6131, plain, (~c4_2(a498, a499))). % 19.71/6.91 tff(c_6111, plain, (![X10_22, X11_24]: (~c2_1(X10_22) | c8_1(X10_22) | ~c7_2(X10_22, X11_24) | ~c4_2(X10_22, X11_24) | c8_2(X10_22, X11_24) | ~ndr1_1(X10_22)))). % 19.71/6.91 tff(c_6110, plain, (~c4_1(a491))). % 19.71/6.91 tff(c_6097, plain, (![X130_179, X131_181]: (c7_1(X130_179) | ~c6_2(X130_179, X131_181) | ~c2_2(X130_179, X131_181) | c7_2(X130_179, X131_181) | ~ndr1_1(X130_179) | c4_1(X130_179)))). % 19.71/6.91 tff(c_6096, plain, (~c5_1(a491))). % 19.71/6.91 tff(c_6092, plain, (~c6_2(a482, a484))). % 19.71/6.91 tff(c_6088, plain, (c2_2(a566, a567))). % 19.71/6.91 tff(c_6090, plain, (c8_2(a482, a483))). % 19.71/6.91 tff(c_6087, plain, (c7_1(a546))). % 19.71/6.91 tff(c_6066, plain, (![X100_138, X101_140]: (c1_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | c8_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6062, plain, (c2_2(a482, a483))). % 19.71/6.91 tff(c_6060, plain, (~c2_2(a566, a557))). % 19.71/6.91 tff(c_6059, plain, (~c2_2(a546, a557))). % 19.71/6.91 tff(c_6036, plain, (![X100_138, X101_140]: (~c2_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | c8_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6033, plain, (~c6_2(a566, a557))). % 19.71/6.91 tff(c_6032, plain, (~c6_2(a546, a557))). % 19.71/6.91 tff(c_6011, plain, (![X100_138, X101_140]: (~c6_2(X100_138, a557) | c7_1(X100_138) | c2_2(X100_138, X101_140) | c8_2(X100_138, X101_140) | ~ndr1_1(X100_138)))). % 19.71/6.91 tff(c_6009, plain, (c3_2(a482, a483))). % 19.71/6.91 tff(c_6005, plain, (~c4_2(a482, a484))). % 19.71/6.91 tff(c_6003, plain, (c5_2(a482, a484))). % 19.71/6.91 tff(c_5978, plain, (c7_2(a546, a547))). % 19.71/6.91 tff(c_5977, plain, (~c3_1(a533))). % 19.71/6.91 tff(c_5967, plain, (~c6_1(a592))). % 19.71/6.91 tff(c_5963, plain, (ndr1_1(a482))). % 19.71/6.91 tff(c_5961, plain, (~c2_2(a546, a547))). % 19.71/6.91 tff(c_5960, plain, (~c8_2(a546, a547))). % 19.71/6.91 tff(c_5945, plain, (~c6_1(a501))). % 19.71/6.91 tff(c_5928, plain, (~ndr1_1(a488))). % 19.71/6.91 tff(c_5926, plain, (~c1_1(a514))). % 19.71/6.91 tff(c_5924, plain, (c5_1(a501))). % 19.71/6.91 tff(c_5915, plain, (~ndr1_1(a552))). % 19.71/6.91 tff(c_5913, plain, (~c4_1(a546))). % 19.71/6.91 tff(c_5912, plain, (~c8_1(a501))). % 19.71/6.91 tff(c_5907, plain, (ndr1_1(a546))). % 19.71/6.91 tff(c_5906, plain, (c5_1(a514))). % 19.71/6.91 tff(c_5897, plain, (~c4_1(a498))). % 19.71/6.91 tff(c_5884, plain, (![X54_79, X55_81]: (~c7_2(X54_79, X55_81) | ~c3_2(X54_79, X55_81) | ~c4_2(X54_79, X55_81) | ~ndr1_1(X54_79) | ~c4_1(X54_79)))). % 19.71/6.91 tff(c_5867, plain, (![X111_152, X112_154]: (~c6_2(X111_152, a572) | ~c4_1(X111_152) | c5_2(X111_152, X112_154) | c2_2(X111_152, X112_154) | ~ndr1_1(X111_152)))). % 19.71/6.91 tff(c_5860, plain, (![X111_152, X112_154]: (~c5_2(X111_152, a572) | ~c4_1(X111_152) | c5_2(X111_152, X112_154) | c2_2(X111_152, X112_154) | ~ndr1_1(X111_152)))). % 19.71/6.91 tff(c_5859, plain, (~c6_1(a458))). % 19.71/6.91 tff(c_5850, plain, (~c2_1(a458))). % 19.71/6.91 tff(c_5846, plain, (![X111_152, X112_154]: (c2_2(X111_152, a572) | ~c4_1(X111_152) | c5_2(X111_152, X112_154) | c2_2(X111_152, X112_154) | ~ndr1_1(X111_152)))). % 19.71/6.91 tff(c_5845, plain, (c4_1(a458))). % 19.71/6.91 tff(c_5842, plain, (c6_1(a565))). % 19.71/6.91 tff(c_5830, plain, (c3_1(a565))). % 19.71/6.91 tff(c_5826, plain, (~c3_1(a538))). % 19.71/6.91 tff(c_5821, plain, (~ndr1_1(a538))). % 19.71/6.91 tff(c_5820, plain, (c2_1(a565))). % 19.71/6.91 tff(c_5762, plain, (![X_5]: (~c6_2(X_5, a459) | ~c8_1(X_5) | ~c3_1(X_5)))). % 19.71/6.91 tff(c_5756, plain, (![X_5]: (~c3_2(X_5, a459) | ~c8_1(X_5) | ~c3_1(X_5)))). % 19.71/6.91 tff(c_5731, plain, (![X_5]: (c7_2(X_5, a459) | ~c8_1(X_5) | ~c3_1(X_5)))). % 19.71/6.91 tff(c_5727, plain, (~c3_1(a488))). % 19.71/6.91 tff(c_5725, plain, (c6_1(a552))). % 19.71/6.91 tff(c_5718, plain, (~c8_1(a552))). % 19.71/6.91 tff(c_5711, plain, (![X_5]: (ndr1_1(X_5) | ~c8_1(X_5) | ~c3_1(X_5)))). % 19.71/6.91 tff(c_5697, plain, (c4_1(a488))). % 19.71/6.91 tff(c_5690, plain, (![X88_124]: (~c2_1(X88_124) | ~c8_1(X88_124)))). % 19.71/6.91 tff(c_5681, plain, (c6_2(a566, a567))). % 19.71/6.91 tff(c_5680, plain, (~c1_2(a566, a567))). % 19.71/6.91 tff(c_5679, plain, (~c8_2(a566, a567))). % 19.71/6.91 tff(c_5659, plain, (ndr1_1(a566))). % 19.71/6.91 tff(c_5653, plain, (c1_1(a566))). % 19.71/6.91 tff(c_5650, plain, (c1_1(a538))). % 19.71/6.91 tff(c_5646, plain, (~c7_1(a536))). % 19.71/6.91 tff(c_5643, plain, (~c5_1(a537))). % 19.71/6.91 tff(c_5621, plain, (~c8_2(a498, a499))). % 19.71/6.92 tff(c_5606, plain, (c7_2(a498, a499))). % 19.71/6.92 tff(c_5596, plain, (c4_2(a498, a500))). % 19.71/6.92 tff(c_5595, plain, (c2_2(a520, a521))). % 19.71/6.92 tff(c_5591, plain, (c8_2(a498, a500))). % 19.71/6.92 tff(c_5582, plain, (~c7_2(a498, a500))). % 19.71/6.92 tff(c_5578, plain, (c3_2(a498, a499))). % 19.71/6.92 tff(c_5577, plain, (~c4_2(a520, a521))). % 19.71/6.92 tff(c_5576, plain, (~c1_2(a520, a521))). % 19.71/6.92 tff(c_5574, plain, (c3_2(a570, a571))). % 19.71/6.92 tff(c_5572, plain, (c1_2(a570, a571))). % 19.71/6.92 tff(c_5571, plain, (ndr1_1(a520))). % 19.71/6.92 tff(c_5565, plain, (c2_2(a570, a571))). % 19.71/6.92 tff(c_5557, plain, (c7_1(a601))). % 19.71/6.92 tff(c_5556, plain, (~c1_1(a601))). % 19.71/6.92 tff(c_5553, plain, (ndr1_1(a498))). % 19.71/6.92 tff(c_5550, plain, (c5_1(a601))). % 19.71/6.92 tff(c_5548, plain, (~c2_1(a520))). % 19.71/6.92 tff(c_5543, plain, (c7_1(a498))). % 19.71/6.92 tff(c_5542, plain, (~c5_1(a520))). % 19.71/6.92 tff(c_5535, plain, (ndr1_1(a570))). % 19.71/6.92 tff(c_5533, plain, (c5_1(a570))). % 19.71/6.92 tff(c_5532, plain, (c4_1(a570))). % 19.71/6.92 tff(c_5531, plain, (c8_0)). % 19.71/6.92 tff(c_5527, plain, (~c4_0)). % 19.71/6.92 tff(c_5524, plain, (~c2_0)). % 19.71/6.92 tff(c_5522, plain, (~c2_1(a584))). % 19.71/6.92 tff(c_5520, plain, (~c7_0)). % 19.71/6.92 tff(c_5519, plain, (c6_0)). % 19.71/6.92 tff(c_5518, plain, (~c5_0)). % 19.71/6.92 tff(c_5517, plain, (~c1_0)). % 19.71/6.92 tff(c_42, plain, (c3_0)). % 19.71/6.92 tff(c_1102, plain, (ndr1_0)). % 19.71/6.92 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.71/6.92 %------------------------------------------------------------------------------