%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN422+1 : TPTP v9.0.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 10:03:31 PM UTC 2025 % Result : CounterSatisfiable 17.94s 5.56s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN422+1 : TPTP v9.0.0. Released v2.1.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.14/0.35 % Computer : n016.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Apr 9 07:24:53 EDT 2025 % 0.14/0.35 % CPUTime : % 17.94/5.55 % 17.94/5.56 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.94/5.56 % 17.94/5.56 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.94/5.57 %$ c9_2 > c8_2 > c7_2 > c6_2 > c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > c10_2 > ndr1_1 > c9_1 > c8_1 > c7_1 > c6_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > c10_1 > #nlpp > ndr1_0 > c9_0 > c8_0 > c7_0 > c6_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > c10_0 > a760 > a759 > a758 > a757 > a756 > a755 > a754 > a753 > a752 > a751 > a750 > a749 > a748 > a747 > a746 > a745 > a744 > a743 > a742 > a741 > a740 > a739 > a738 > a737 > a736 > a735 > a734 > a733 > a732 > a731 > a730 > a729 > a728 > a727 > a726 > a725 > a724 > a723 > a722 > a721 > a720 > a719 > a718 > a717 > a716 > a715 > a714 > a713 > a712 > a711 > a710 > a709 > a708 > a707 > a706 > a705 > a704 > a703 > a702 > a701 > a700 > a699 > a698 > a697 > a696 > a695 > a694 > a693 > a692 > a691 > a690 > a689 > a688 > a687 > a686 > a685 > a684 > a683 > a682 > a681 > a680 > a679 > a678 > a677 > a676 > a675 > a674 > a673 > a672 > a671 > a670 > a669 > a668 > a667 > a666 > a665 > a664 > a663 > a662 > a661 > a660 > a659 > a658 > a657 > a656 > a655 > a654 > a653 > a652 > a651 > a650 > a649 > a648 > a647 > a646 > a645 > a644 > a643 > a642 > a641 > a640 > a639 > a638 > a637 > a636 > a635 > a634 > a633 > a632 > a631 > a630 > a629 > a628 > a627 > a626 > a625 > a624 > a623 > a622 > a621 > a620 > a619 > a618 > a617 > a616 > a615 > a614 > a613 > a612 > a611 > a610 > a609 > a608 % 17.94/5.57 % 17.94/5.57 %Foreground sorts: % 17.94/5.57 % 17.94/5.57 % 17.94/5.57 %Background operators: % 17.94/5.57 % 17.94/5.57 % 17.94/5.57 %Foreground operators: % 17.94/5.57 tff(c7_0, type, c7_0: $o). % 17.94/5.57 tff(a750, type, a750: $i). % 17.94/5.57 tff(a760, type, a760: $i). % 17.94/5.57 tff(a749, type, a749: $i). % 17.94/5.57 tff(a679, type, a679: $i). % 17.94/5.57 tff(a713, type, a713: $i). % 17.94/5.57 tff(a697, type, a697: $i). % 17.94/5.57 tff(a658, type, a658: $i). % 17.94/5.57 tff(a662, type, a662: $i). % 17.94/5.57 tff(a708, type, a708: $i). % 17.94/5.57 tff(c4_0, type, c4_0: $o). % 17.94/5.57 tff(a712, type, a712: $i). % 17.94/5.57 tff(a687, type, a687: $i). % 17.94/5.57 tff(a748, type, a748: $i). % 17.94/5.57 tff(a669, type, a669: $i). % 17.94/5.57 tff(a681, type, a681: $i). % 17.94/5.57 tff(a692, type, a692: $i). % 17.94/5.57 tff(a672, type, a672: $i). % 17.94/5.57 tff(a717, type, a717: $i). % 17.94/5.57 tff(a739, type, a739: $i). % 17.94/5.57 tff(a733, type, a733: $i). % 17.94/5.57 tff(a706, type, a706: $i). % 17.94/5.57 tff(a648, type, a648: $i). % 17.94/5.57 tff(c3_0, type, c3_0: $o). % 17.94/5.57 tff(a725, type, a725: $i). % 17.94/5.57 tff(a734, type, a734: $i). % 17.94/5.57 tff(a640, type, a640: $i). % 17.94/5.57 tff(a751, type, a751: $i). % 17.94/5.57 tff(c1_2, type, c1_2: ($i * $i) > $o). % 17.94/5.57 tff(a727, type, a727: $i). % 17.94/5.57 tff(a758, type, a758: $i). % 17.94/5.57 tff(a627, type, a627: $i). % 17.94/5.57 tff(a731, type, a731: $i). % 17.94/5.57 tff(a624, type, a624: $i). % 17.94/5.57 tff(a693, type, a693: $i). % 17.94/5.57 tff(a649, type, a649: $i). % 17.94/5.57 tff(a753, type, a753: $i). % 17.94/5.57 tff(a613, type, a613: $i). % 17.94/5.57 tff(a628, type, a628: $i). % 17.94/5.57 tff(a736, type, a736: $i). % 17.94/5.57 tff(a661, type, a661: $i). % 17.94/5.57 tff(a655, type, a655: $i). % 17.94/5.57 tff(a704, type, a704: $i). % 17.94/5.57 tff(a691, type, a691: $i). % 17.94/5.57 tff(a721, type, a721: $i). % 17.94/5.57 tff(a759, type, a759: $i). % 17.94/5.57 tff(a741, type, a741: $i). % 17.94/5.57 tff(a698, type, a698: $i). % 17.94/5.57 tff(a724, type, a724: $i). % 17.94/5.57 tff(a746, type, a746: $i). % 17.94/5.57 tff(a629, type, a629: $i). % 17.94/5.57 tff(c8_0, type, c8_0: $o). % 17.94/5.57 tff(a620, type, a620: $i). % 17.94/5.57 tff(a680, type, a680: $i). % 17.94/5.57 tff(a747, type, a747: $i). % 17.94/5.57 tff(a703, type, a703: $i). % 17.94/5.57 tff(a619, type, a619: $i). % 17.94/5.57 tff(a709, type, a709: $i). % 17.94/5.57 tff(a665, type, a665: $i). % 17.94/5.57 tff(a621, type, a621: $i). % 17.94/5.57 tff(a695, type, a695: $i). % 17.94/5.57 tff(c5_0, type, c5_0: $o). % 17.94/5.57 tff(a714, type, a714: $i). % 17.94/5.57 tff(a696, type, a696: $i). % 17.94/5.57 tff(a685, type, a685: $i). % 17.94/5.57 tff(a677, type, a677: $i). % 17.94/5.57 tff(a711, type, a711: $i). % 17.94/5.57 tff(a616, type, a616: $i). % 17.94/5.57 tff(a722, type, a722: $i). % 17.94/5.57 tff(c6_0, type, c6_0: $o). % 17.94/5.57 tff(a638, type, a638: $i). % 17.94/5.57 tff(c8_2, type, c8_2: ($i * $i) > $o). % 17.94/5.57 tff(a719, type, a719: $i). % 17.94/5.57 tff(a690, type, a690: $i). % 17.94/5.57 tff(a707, type, a707: $i). % 17.94/5.57 tff(a626, type, a626: $i). % 17.94/5.57 tff(a617, type, a617: $i). % 17.94/5.57 tff(a636, type, a636: $i). % 17.94/5.57 tff(a730, type, a730: $i). % 17.94/5.57 tff(a678, type, a678: $i). % 17.94/5.57 tff(a611, type, a611: $i). % 17.94/5.57 tff(a686, type, a686: $i). % 17.94/5.57 tff(a745, type, a745: $i). % 17.94/5.57 tff(a650, type, a650: $i). % 17.94/5.57 tff(a614, type, a614: $i). % 17.94/5.57 tff(a642, type, a642: $i). % 17.94/5.57 tff(a612, type, a612: $i). % 17.94/5.57 tff(a670, type, a670: $i). % 17.94/5.57 tff(a645, type, a645: $i). % 17.94/5.57 tff(a737, type, a737: $i). % 17.94/5.57 tff(c1_0, type, c1_0: $o). % 17.94/5.57 tff(a754, type, a754: $i). % 17.94/5.57 tff(a755, type, a755: $i). % 17.94/5.57 tff(c8_1, type, c8_1: $i > $o). % 17.94/5.57 tff(a644, type, a644: $i). % 17.94/5.57 tff(a740, type, a740: $i). % 17.94/5.57 tff(a743, type, a743: $i). % 17.94/5.57 tff(c2_1, type, c2_1: $i > $o). % 17.94/5.57 tff(ndr1_1, type, ndr1_1: $i > $o). % 17.94/5.57 tff(a699, type, a699: $i). % 17.94/5.57 tff(c2_0, type, c2_0: $o). % 17.94/5.57 tff(c4_1, type, c4_1: $i > $o). % 17.94/5.57 tff(a738, type, a738: $i). % 17.94/5.57 tff(a715, type, a715: $i). % 17.94/5.57 tff(a710, type, a710: $i). % 17.94/5.57 tff(a664, type, a664: $i). % 17.94/5.57 tff(a654, type, a654: $i). % 17.94/5.57 tff(a673, type, a673: $i). % 17.94/5.57 tff(a609, type, a609: $i). % 17.94/5.57 tff(a728, type, a728: $i). % 17.94/5.57 tff(a671, type, a671: $i). % 17.94/5.57 tff(c9_1, type, c9_1: $i > $o). % 17.94/5.57 tff(c10_1, type, c10_1: $i > $o). % 17.94/5.57 tff(c10_0, type, c10_0: $o). % 17.94/5.57 tff(a641, type, a641: $i). % 17.94/5.57 tff(a630, type, a630: $i). % 17.94/5.57 tff(a663, type, a663: $i). % 17.94/5.57 tff(a659, type, a659: $i). % 17.94/5.57 tff(a718, type, a718: $i). % 17.94/5.57 tff(c6_2, type, c6_2: ($i * $i) > $o). % 17.94/5.57 tff(a643, type, a643: $i). % 17.94/5.57 tff(a610, type, a610: $i). % 17.94/5.57 tff(a720, type, a720: $i). % 17.94/5.57 tff(a622, type, a622: $i). % 17.94/5.57 tff(a694, type, a694: $i). % 17.94/5.57 tff(a716, type, a716: $i). % 17.94/5.57 tff(a684, type, a684: $i). % 17.94/5.57 tff(a668, type, a668: $i). % 17.94/5.57 tff(ndr1_0, type, ndr1_0: $o). % 17.94/5.57 tff(a618, type, a618: $i). % 17.94/5.57 tff(a742, type, a742: $i). % 17.94/5.57 tff(a666, type, a666: $i). % 17.94/5.57 tff(c9_2, type, c9_2: ($i * $i) > $o). % 17.94/5.57 tff(a726, type, a726: $i). % 17.94/5.57 tff(a752, type, a752: $i). % 17.94/5.57 tff(a615, type, a615: $i). % 17.94/5.57 tff(c10_2, type, c10_2: ($i * $i) > $o). % 17.94/5.57 tff(a657, type, a657: $i). % 17.94/5.57 tff(a729, type, a729: $i). % 17.94/5.57 tff(a702, type, a702: $i). % 17.94/5.57 tff(a732, type, a732: $i). % 17.94/5.57 tff(a723, type, a723: $i). % 17.94/5.57 tff(a674, type, a674: $i). % 17.94/5.57 tff(a667, type, a667: $i). % 17.94/5.57 tff(a676, type, a676: $i). % 17.94/5.57 tff(c1_1, type, c1_1: $i > $o). % 17.94/5.57 tff(a756, type, a756: $i). % 17.94/5.57 tff(a652, type, a652: $i). % 17.94/5.57 tff(a625, type, a625: $i). % 17.94/5.57 tff(c5_2, type, c5_2: ($i * $i) > $o). % 17.94/5.57 tff(c9_0, type, c9_0: $o). % 17.94/5.57 tff(a634, type, a634: $i). % 17.94/5.57 tff(a631, type, a631: $i). % 17.94/5.57 tff(a675, type, a675: $i). % 17.94/5.57 tff(a608, type, a608: $i). % 17.94/5.57 tff(c7_1, type, c7_1: $i > $o). % 17.94/5.57 tff(c6_1, type, c6_1: $i > $o). % 17.94/5.57 tff(a744, type, a744: $i). % 17.94/5.57 tff(a705, type, a705: $i). % 17.94/5.57 tff(a632, type, a632: $i). % 17.94/5.57 tff(c4_2, type, c4_2: ($i * $i) > $o). % 17.94/5.57 tff(a757, type, a757: $i). % 17.94/5.57 tff(a623, type, a623: $i). % 17.94/5.57 tff(a639, type, a639: $i). % 17.94/5.57 tff(a660, type, a660: $i). % 17.94/5.57 tff(a653, type, a653: $i). % 17.94/5.57 tff(a651, type, a651: $i). % 17.94/5.57 tff(a701, type, a701: $i). % 17.94/5.57 tff(a700, type, a700: $i). % 17.94/5.57 tff(a646, type, a646: $i). % 17.94/5.57 tff(c5_1, type, c5_1: $i > $o). % 17.94/5.57 tff(c7_2, type, c7_2: ($i * $i) > $o). % 17.94/5.57 tff(c3_2, type, c3_2: ($i * $i) > $o). % 17.94/5.57 tff(a688, type, a688: $i). % 17.94/5.57 tff(a637, type, a637: $i). % 17.94/5.57 tff(a689, type, a689: $i). % 17.94/5.57 tff(c2_2, type, c2_2: ($i * $i) > $o). % 17.94/5.57 tff(a656, type, a656: $i). % 17.94/5.57 tff(a647, type, a647: $i). % 17.94/5.57 tff(a682, type, a682: $i). % 17.94/5.57 tff(a735, type, a735: $i). % 17.94/5.57 tff(a633, type, a633: $i). % 17.94/5.57 tff(a683, type, a683: $i). % 17.94/5.57 tff(a635, type, a635: $i). % 17.94/5.57 tff(c3_1, type, c3_1: $i > $o). % 17.94/5.57 % 17.94/5.57 %Saturated clause set: % 17.94/5.57 tff(c_6646, plain, (![X139_388]: (c1_2(X139_388, a678) | c7_1(X139_388) | c1_2(X139_388, a675) | ~c2_2(X139_388, a675) | c2_2(X139_388, a677) | ~c3_2(X139_388, a726) | c3_1(X139_388) | c10_2(X139_388, a747) | c1_2(X139_388, a747) | ~c2_1(X139_388) | c3_2(X139_388, a676) | ~c1_2(X139_388, a676)))). % 17.94/5.57 tff(c_6519, plain, (![X139_379]: (c1_2(X139_379, a678) | c7_1(X139_379) | c1_2(X139_379, a675) | ~c2_2(X139_379, a675) | c2_2(X139_379, a677) | ~c4_2(X139_379, a726) | c3_1(X139_379) | c10_2(X139_379, a747) | c1_2(X139_379, a747) | ~c2_1(X139_379) | c3_2(X139_379, a676) | ~c1_2(X139_379, a676)))). % 17.94/5.57 tff(c_6651, plain, (![X139_388]: (c5_2(X139_388, a675) | c2_2(X139_388, a677) | ~c3_2(X139_388, a726) | c3_1(X139_388) | c10_2(X139_388, a747) | c1_2(X139_388, a747) | ~c2_1(X139_388) | c3_2(X139_388, a676) | ~c1_2(X139_388, a676)))). % 17.94/5.57 tff(c_6652, plain, (![X139_388]: (~c1_2(X139_388, a675) | c2_2(X139_388, a677) | ~c3_2(X139_388, a726) | c3_1(X139_388) | c10_2(X139_388, a747) | c1_2(X139_388, a747) | ~c2_1(X139_388) | c3_2(X139_388, a676) | ~c1_2(X139_388, a676)))). % 17.94/5.57 tff(c_6654, plain, (![X139_388]: (~c7_1(X139_388) | ~c8_1(X139_388) | ~c3_2(X139_388, a726) | c3_1(X139_388) | c10_2(X139_388, a747) | c1_2(X139_388, a747) | ~c2_1(X139_388) | c3_2(X139_388, a627) | ~c1_2(X139_388, a627)))). % 17.94/5.57 tff(c_6641, plain, (![X139_388]: (c4_1(X139_388) | ~c7_1(X139_388) | ~c3_2(X139_388, a726) | c3_1(X139_388) | c10_2(X139_388, a747) | c1_2(X139_388, a747) | ~c2_1(X139_388) | c3_2(X139_388, a704) | ~c1_2(X139_388, a704)))). % 17.94/5.57 tff(c_6662, plain, (~c3_2(a698, a726))). % 17.94/5.58 tff(c_6577, plain, (![X139_192, X140_194]: (~c3_2(X139_192, a726) | c3_1(X139_192) | c10_2(X139_192, a747) | c1_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.58 tff(c_6583, plain, (~c3_2(a633, a726))). % 17.94/5.58 tff(c_6570, plain, (![X92_128]: (~c3_2(X92_128, a726) | c3_1(X92_128) | c10_2(X92_128, a704) | c1_2(X92_128, a704) | c4_1(X92_128) | ~c7_1(X92_128)))). % 17.94/5.58 tff(c_6581, plain, (~c3_2(a709, a726))). % 17.94/5.58 tff(c_6553, plain, (![X124_172, X125_174]: (~c3_2(X124_172, a726) | c3_1(X124_172) | c10_2(X124_172, X125_174) | c1_2(X124_172, X125_174) | ~c9_2(X124_172, X125_174)))). % 17.94/5.58 tff(c_6525, plain, (![X139_379]: (~c1_2(X139_379, a675) | c2_2(X139_379, a677) | ~c4_2(X139_379, a726) | c3_1(X139_379) | c10_2(X139_379, a747) | c1_2(X139_379, a747) | ~c2_1(X139_379) | c3_2(X139_379, a676) | ~c1_2(X139_379, a676)))). % 17.94/5.58 tff(c_6524, plain, (![X139_379]: (c5_2(X139_379, a675) | c2_2(X139_379, a677) | ~c4_2(X139_379, a726) | c3_1(X139_379) | c10_2(X139_379, a747) | c1_2(X139_379, a747) | ~c2_1(X139_379) | c3_2(X139_379, a676) | ~c1_2(X139_379, a676)))). % 17.94/5.58 tff(c_6514, plain, (![X139_379]: (c4_1(X139_379) | ~c7_1(X139_379) | ~c4_2(X139_379, a726) | c3_1(X139_379) | c10_2(X139_379, a747) | c1_2(X139_379, a747) | ~c2_1(X139_379) | c3_2(X139_379, a704) | ~c1_2(X139_379, a704)))). % 17.94/5.58 tff(c_6527, plain, (![X139_379]: (~c7_1(X139_379) | ~c8_1(X139_379) | ~c4_2(X139_379, a726) | c3_1(X139_379) | c10_2(X139_379, a747) | c1_2(X139_379, a747) | ~c2_1(X139_379) | c3_2(X139_379, a627) | ~c1_2(X139_379, a627)))). % 17.94/5.58 tff(c_6535, plain, (~c4_2(a698, a726))). % 17.94/5.58 tff(c_6401, plain, (![X139_192, X140_194]: (~c4_2(X139_192, a726) | c3_1(X139_192) | c10_2(X139_192, a747) | c1_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.58 tff(c_6394, plain, (![X92_128]: (~c4_2(X92_128, a726) | c3_1(X92_128) | c10_2(X92_128, a704) | c1_2(X92_128, a704) | c4_1(X92_128) | ~c7_1(X92_128)))). % 17.94/5.58 tff(c_6453, plain, (~c1_2(a708, a727))). % 17.94/5.58 tff(c_6419, plain, (![X126_175]: (~c6_2(X126_175, a727) | ~c4_1(X126_175) | ~c7_1(X126_175)))). % 17.94/5.58 tff(c_6416, plain, (~c5_2(a708, a727))). % 17.94/5.58 tff(c_6409, plain, (![X126_175]: (~c7_2(X126_175, a727) | ~c4_1(X126_175) | ~c7_1(X126_175)))). % 17.94/5.58 tff(c_6406, plain, (~c4_2(a633, a726))). % 17.94/5.58 tff(c_6405, plain, (~c4_2(a709, a726))). % 17.94/5.58 tff(c_6377, plain, (![X124_172, X125_174]: (~c4_2(X124_172, a726) | c3_1(X124_172) | c10_2(X124_172, X125_174) | c1_2(X124_172, X125_174) | ~c9_2(X124_172, X125_174)))). % 17.94/5.58 tff(c_6074, plain, (![X141_354]: (c1_2(X141_354, a678) | c7_1(X141_354) | c1_2(X141_354, a675) | ~c2_2(X141_354, a675) | c2_2(X141_354, a677) | c10_2(X141_354, a748) | c10_2(X141_354, a676) | c3_2(X141_354, a676) | c8_1(X141_354)))). % 17.94/5.58 tff(c_6153, plain, (![X141_356]: (c1_2(X141_356, a678) | c7_1(X141_356) | c1_2(X141_356, a675) | ~c2_2(X141_356, a675) | c2_2(X141_356, a677) | c1_2(X141_356, a748) | c10_2(X141_356, a676) | c3_2(X141_356, a676) | c8_1(X141_356)))). % 17.94/5.58 tff(c_6234, plain, (![X141_358]: (c1_2(X141_358, a678) | c7_1(X141_358) | c1_2(X141_358, a675) | ~c2_2(X141_358, a675) | c2_2(X141_358, a677) | ~c4_2(X141_358, a748) | c10_2(X141_358, a676) | c3_2(X141_358, a676) | c8_1(X141_358)))). % 17.94/5.58 tff(c_6241, plain, (![X141_358]: (~c1_2(X141_358, a675) | c2_2(X141_358, a677) | ~c4_2(X141_358, a748) | c10_2(X141_358, a676) | c3_2(X141_358, a676) | c8_1(X141_358)))). % 17.94/5.58 tff(c_6240, plain, (![X141_358]: (c5_2(X141_358, a675) | c2_2(X141_358, a677) | ~c4_2(X141_358, a748) | c10_2(X141_358, a676) | c3_2(X141_358, a676) | c8_1(X141_358)))). % 17.94/5.58 tff(c_6159, plain, (![X141_356]: (~c1_2(X141_356, a675) | c2_2(X141_356, a677) | c1_2(X141_356, a748) | c10_2(X141_356, a676) | c3_2(X141_356, a676) | c8_1(X141_356)))). % 17.94/5.58 tff(c_6079, plain, (![X141_354]: (c5_2(X141_354, a675) | c2_2(X141_354, a677) | c10_2(X141_354, a748) | c10_2(X141_354, a676) | c3_2(X141_354, a676) | c8_1(X141_354)))). % 17.94/5.58 tff(c_6080, plain, (![X141_354]: (~c1_2(X141_354, a675) | c2_2(X141_354, a677) | c10_2(X141_354, a748) | c10_2(X141_354, a676) | c3_2(X141_354, a676) | c8_1(X141_354)))). % 17.94/5.58 tff(c_6158, plain, (![X141_356]: (c5_2(X141_356, a675) | c2_2(X141_356, a677) | c1_2(X141_356, a748) | c10_2(X141_356, a676) | c3_2(X141_356, a676) | c8_1(X141_356)))). % 17.94/5.58 tff(c_6279, plain, (![X141_363]: (c4_1(X141_363) | ~c7_1(X141_363) | c10_2(X141_363, a748) | c10_2(X141_363, a704) | c8_1(X141_363)))). % 17.94/5.58 tff(c_6273, plain, (![X141_361]: (c4_1(X141_361) | ~c7_1(X141_361) | c1_2(X141_361, a748) | c10_2(X141_361, a704) | c8_1(X141_361)))). % 17.94/5.58 tff(c_6228, plain, (![X141_358]: (c4_1(X141_358) | ~c7_1(X141_358) | ~c4_2(X141_358, a748) | c10_2(X141_358, a704) | c3_2(X141_358, a704) | c8_1(X141_358)))). % 17.94/5.58 tff(c_6253, plain, (c8_1(a708))). % 17.94/5.58 tff(c_6171, plain, (![X141_195, X142_197]: (~c4_2(X141_195, a748) | c10_2(X141_195, X142_197) | c5_2(X141_195, X142_197) | c3_2(X141_195, X142_197) | c8_1(X141_195)))). % 17.94/5.58 tff(c_6174, plain, (c8_1(a658))). % 17.94/5.58 tff(c_6172, plain, (c8_1(a698))). % 17.94/5.58 tff(c_6167, plain, (c8_1(a641))). % 17.94/5.58 tff(c_6091, plain, (![X141_195, X142_197]: (c1_2(X141_195, a748) | c10_2(X141_195, X142_197) | c5_2(X141_195, X142_197) | c3_2(X141_195, X142_197) | c8_1(X141_195)))). % 17.94/5.58 tff(c_6093, plain, (c3_2(a669, a676))). % 17.94/5.58 tff(c_6092, plain, (c8_1(a645))). % 17.94/5.58 tff(c_6088, plain, (c3_2(a652, a653))). % 17.94/5.58 tff(c_6014, plain, (![X141_195, X142_197]: (c10_2(X141_195, a748) | c10_2(X141_195, X142_197) | c5_2(X141_195, X142_197) | c3_2(X141_195, X142_197) | c8_1(X141_195)))). % 17.94/5.58 tff(c_5800, plain, (![X73_336]: (c1_2(X73_336, a678) | c7_1(X73_336) | c1_2(X73_336, a675) | ~c2_2(X73_336, a675) | ~c9_1(X73_336) | ~c7_2(X73_336, a676) | c1_2(X73_336, a676) | ~c10_1(X73_336) | c5_2(X73_336, a677)))). % 17.94/5.58 tff(c_5779, plain, (![X73_334]: (c1_2(X73_334, a678) | c7_1(X73_334) | c1_2(X73_334, a675) | ~c2_2(X73_334, a675) | ~c9_1(X73_334) | ~c7_2(X73_334, a676) | c1_2(X73_334, a676) | ~c10_1(X73_334) | c2_2(X73_334, a677)))). % 17.94/5.58 tff(c_5689, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a675) | c1_2(X73_106, a675) | ~c10_1(X73_106) | ~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.58 tff(c_5801, plain, (![X73_336]: (~c6_2(X73_336, a678) | c7_1(X73_336) | c1_2(X73_336, a675) | ~c2_2(X73_336, a675) | ~c9_1(X73_336) | ~c7_2(X73_336, a676) | c1_2(X73_336, a676) | ~c10_1(X73_336) | c5_2(X73_336, a677)))). % 17.94/5.58 tff(c_5688, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a675) | c1_2(X73_106, a675) | ~c10_1(X73_106) | ~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.58 tff(c_5687, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a675) | c1_2(X73_106, a675) | ~c10_1(X73_106) | c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.58 tff(c_5939, plain, (~c5_2(a708, a676))). % 17.94/5.58 tff(c_5780, plain, (![X73_334]: (~c6_2(X73_334, a678) | c7_1(X73_334) | c1_2(X73_334, a675) | ~c2_2(X73_334, a675) | ~c9_1(X73_334) | ~c7_2(X73_334, a676) | c1_2(X73_334, a676) | ~c10_1(X73_334) | c2_2(X73_334, a677)))). % 17.94/5.58 tff(c_5686, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a675) | c1_2(X73_106, a675) | ~c10_1(X73_106) | c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.58 tff(c_5904, plain, (![X139_192, X140_194]: (~c3_1(X139_192) | ~c4_1(X139_192) | ~c8_2(X139_192, a747) | c2_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.58 tff(c_5911, plain, (![X139_342]: (c4_1(X139_342) | ~c7_1(X139_342) | ~c1_2(X139_342, a747) | ~c2_1(X139_342) | ~c1_2(X139_342, a704)))). % 17.94/5.59 tff(c_5906, plain, (~c8_2(a633, a634))). % 17.94/5.59 tff(c_5884, plain, (![X20_34, X21_36]: (~c3_1(X20_34) | ~c4_1(X20_34) | ~c8_2(X20_34, X21_36) | ~c9_2(X20_34, X21_36) | c2_2(X20_34, X21_36)))). % 17.94/5.59 tff(c_5880, plain, (~c4_1(a669))). % 17.94/5.59 tff(c_5876, plain, (~c7_1(a669))). % 17.94/5.59 tff(c_5851, plain, (![X92_128]: (~c5_2(X92_128, a704) | c4_1(X92_128) | ~c7_1(X92_128)))). % 17.94/5.59 tff(c_5846, plain, (~c2_2(a708, a676))). % 17.94/5.59 tff(c_5842, plain, (~c1_2(a708, a676))). % 17.94/5.59 tff(c_5841, plain, (~c1_2(a708, a675))). % 17.94/5.59 tff(c_5814, plain, (~c5_2(a708, a675))). % 17.94/5.59 tff(c_5799, plain, (![X73_336]: (~c7_2(X73_336, a675) | c1_2(X73_336, a675) | ~c9_1(X73_336) | ~c7_2(X73_336, a676) | c1_2(X73_336, a676) | ~c10_1(X73_336) | c5_2(X73_336, a677)))). % 17.94/5.59 tff(c_5778, plain, (![X73_334]: (~c7_2(X73_334, a675) | c1_2(X73_334, a675) | ~c9_1(X73_334) | ~c7_2(X73_334, a676) | c1_2(X73_334, a676) | ~c10_1(X73_334) | c2_2(X73_334, a677)))). % 17.94/5.59 tff(c_5691, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a676) | c1_2(X73_106, a676) | ~c10_1(X73_106) | c8_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.59 tff(c_5698, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a676) | c1_2(X73_106, a676) | ~c10_1(X73_106) | c5_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.59 tff(c_5697, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a676) | c1_2(X73_106, a676) | ~c10_1(X73_106) | c8_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.59 tff(c_5692, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a675) | c1_2(X73_106, a675) | ~c10_1(X73_106) | ~c5_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.59 tff(c_5752, plain, (![X92_331]: (~c3_1(X92_331) | ~c8_1(X92_331) | ~c10_2(X92_331, a704) | c6_2(X92_331, a704) | c4_1(X92_331) | ~c7_1(X92_331)))). % 17.94/5.59 tff(c_5758, plain, (~c4_1(a645))). % 17.94/5.59 tff(c_5754, plain, (~c7_1(a645))). % 17.94/5.59 tff(c_5735, plain, (![X92_128]: (c9_2(X92_128, a704) | c4_1(X92_128) | ~c7_1(X92_128)))). % 17.94/5.59 tff(c_5695, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a676) | c1_2(X73_106, a676) | ~c10_1(X73_106) | ~c1_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.59 tff(c_5694, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a676) | c1_2(X73_106, a676) | ~c10_1(X73_106) | c5_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.59 tff(c_5693, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a676) | c1_2(X73_106, a676) | ~c10_1(X73_106) | ~c1_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.59 tff(c_5696, plain, (![X73_106]: (~c9_1(X73_106) | ~c7_2(X73_106, a675) | c1_2(X73_106, a675) | ~c10_1(X73_106) | ~c5_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.59 tff(c_5705, plain, (~c10_1(a697))). % 17.94/5.59 tff(c_5704, plain, (~c10_1(a639))). % 17.94/5.59 tff(c_5630, plain, (![X53_80, X54_82]: (~c9_1(X53_80) | ~c8_2(X53_80, X54_82) | ~c7_2(X53_80, X54_82) | c1_2(X53_80, X54_82) | ~c10_1(X53_80)))). % 17.94/5.59 tff(c_5622, plain, (![X92_128]: (~c3_2(X92_128, a704) | c4_1(X92_128) | ~c7_1(X92_128)))). % 17.94/5.59 tff(c_5618, plain, (~c4_1(a703))). % 17.94/5.59 tff(c_5614, plain, (~c10_1(a703))). % 17.94/5.59 tff(c_5611, plain, (~c7_1(a703))). % 17.94/5.59 tff(c_5606, plain, (~c1_2(a753, a676))). % 17.94/5.59 tff(c_5594, plain, (![X149_206]: (~c3_2(a753, X149_206) | ~c4_2(a753, X149_206)))). % 17.94/5.59 tff(c_4920, plain, (![X139_296]: (c1_2(X139_296, a678) | c1_2(X139_296, a675) | ~c2_2(X139_296, a675) | c2_2(X139_296, a677) | ~c3_2(X139_296, a619) | c7_1(X139_296) | c4_2(X139_296, a747) | ~c2_1(X139_296) | c3_2(X139_296, a676) | ~c1_2(X139_296, a676)))). % 17.94/5.59 tff(c_5558, plain, (c2_2(a708, a716))). % 17.94/5.59 tff(c_5544, plain, (![X110_153, X111_155]: (c10_2(X110_153, a715) | c2_2(X110_153, a716) | ~c3_2(X110_153, X111_155) | ~c7_2(X110_153, X111_155)))). % 17.94/5.59 tff(c_5527, plain, (![X110_153, X111_155]: (~c3_2(X110_153, a715) | c3_2(X110_153, a716) | ~c3_2(X110_153, X111_155) | ~c7_2(X110_153, X111_155)))). % 17.94/5.59 tff(c_5522, plain, (~c3_2(a708, a715))). % 17.94/5.59 tff(c_5508, plain, (![X110_153, X111_155]: (~c3_2(X110_153, a715) | c2_2(X110_153, a716) | ~c3_2(X110_153, X111_155) | ~c7_2(X110_153, X111_155)))). % 17.94/5.59 tff(c_5505, plain, (~c5_1(a651))). % 17.94/5.59 tff(c_5500, plain, (~c10_2(a652, a653))). % 17.94/5.59 tff(c_5483, plain, (![X110_153, X111_155]: (~c3_2(X110_153, a715) | c1_2(X110_153, a716) | ~c3_2(X110_153, X111_155) | ~c7_2(X110_153, X111_155)))). % 17.94/5.59 tff(c_5466, plain, (~c5_2(a652, a653))). % 17.94/5.59 tff(c_5463, plain, (c1_2(a708, a716))). % 17.94/5.59 tff(c_5462, plain, (~c4_1(a651))). % 17.94/5.59 tff(c_5458, plain, (~c7_1(a651))). % 17.94/5.59 tff(c_5442, plain, (![X110_153, X111_155]: (c10_2(X110_153, a715) | c1_2(X110_153, a716) | ~c3_2(X110_153, X111_155) | ~c7_2(X110_153, X111_155)))). % 17.94/5.59 tff(c_5439, plain, (~c9_1(a651))). % 17.94/5.59 tff(c_5434, plain, (c3_2(a708, a716))). % 17.94/5.59 tff(c_5433, plain, (~c3_2(a729, a730))). % 17.94/5.59 tff(c_5417, plain, (![X110_153, X111_155]: (c10_2(X110_153, a715) | c3_2(X110_153, a716) | ~c3_2(X110_153, X111_155) | ~c7_2(X110_153, X111_155)))). % 17.94/5.59 tff(c_5396, plain, (~c8_2(a709, a710))). % 17.94/5.59 tff(c_5389, plain, (~c2_1(a652))). % 17.94/5.59 tff(c_5374, plain, (c4_2(a709, a710))). % 17.94/5.59 tff(c_5373, plain, (~c3_2(a709, a619))). % 17.94/5.59 tff(c_5372, plain, (~c10_2(a709, a710))). % 17.94/5.59 tff(c_5354, plain, (c9_2(a709, a710))). % 17.94/5.59 tff(c_5351, plain, (~c1_2(a753, a754))). % 17.94/5.59 tff(c_5342, plain, (~c4_2(a753, a754))). % 17.94/5.59 tff(c_5339, plain, (~c3_2(a639, a640))). % 17.94/5.59 tff(c_5335, plain, (~c5_1(a609))). % 17.94/5.59 tff(c_5330, plain, (~c2_2(a639, a640))). % 17.94/5.59 tff(c_5317, plain, (c8_2(a639, a640))). % 17.94/5.59 tff(c_5313, plain, (~c8_1(a609))). % 17.94/5.59 tff(c_5310, plain, (~c10_1(a609))). % 17.94/5.59 tff(c_5307, plain, (~c8_1(a652))). % 17.94/5.59 tff(c_5304, plain, (c10_2(a753, a754))). % 17.94/5.59 tff(c_5301, plain, (~c1_2(a639, a640))). % 17.94/5.59 tff(c_5297, plain, (~c6_2(a709, a710))). % 17.94/5.59 tff(c_5294, plain, (~c8_1(a639))). % 17.94/5.59 tff(c_5286, plain, (c8_1(a709))). % 17.94/5.59 tff(c_5259, plain, (~c2_1(a639))). % 17.94/5.59 tff(c_5255, plain, (~c9_1(a709))). % 17.94/5.59 tff(c_5250, plain, (~c9_1(a753))). % 17.94/5.59 tff(c_4605, plain, (![X139_192]: (c1_2(X139_192, a678) | c7_1(X139_192) | c1_2(X139_192, a675) | ~c2_2(X139_192, a675) | c2_2(X139_192, a677) | ~c1_2(X139_192, a747) | ~c2_1(X139_192) | c3_2(X139_192, a676) | ~c1_2(X139_192, a676)))). % 17.94/5.59 tff(c_5239, plain, (~c2_1(a648))). % 17.94/5.59 tff(c_5230, plain, (![X34_55]: (~c3_2(a648, X34_55) | ~c7_2(a648, X34_55)))). % 17.94/5.59 tff(c_5146, plain, (c7_1(a697))). % 17.94/5.59 tff(c_5130, plain, (![X90_126]: (~c6_2(a697, X90_126) | c8_2(a697, X90_126) | ~c3_2(a697, X90_126)))). % 17.94/5.59 tff(c_5123, plain, (~c1_2(a708, a666))). % 17.94/5.59 tff(c_5110, plain, (~c5_2(a708, a666))). % 17.94/5.59 tff(c_5103, plain, (![X99_137]: (c7_2(a708, X99_137) | c10_2(a708, X99_137) | ~c5_2(a708, X99_137)))). % 17.94/5.59 tff(c_5099, plain, (c1_1(a663))). % 17.94/5.59 tff(c_5096, plain, (c7_1(a663))). % 17.94/5.59 tff(c_5090, plain, (~c2_1(a705))). % 17.94/5.59 tff(c_4925, plain, (![X139_296]: (~c1_2(X139_296, a675) | c2_2(X139_296, a677) | ~c3_2(X139_296, a619) | c7_1(X139_296) | c4_2(X139_296, a747) | ~c2_1(X139_296) | c3_2(X139_296, a676) | ~c1_2(X139_296, a676)))). % 17.94/5.59 tff(c_4924, plain, (![X139_296]: (c5_2(X139_296, a675) | c2_2(X139_296, a677) | ~c3_2(X139_296, a619) | c7_1(X139_296) | c4_2(X139_296, a747) | ~c2_1(X139_296) | c3_2(X139_296, a676) | ~c1_2(X139_296, a676)))). % 17.94/5.59 tff(c_4298, plain, (![X139_256, X140_257]: (~c3_1(X139_256) | ~c8_1(X139_256) | ~c10_2(X139_256, a747) | c6_2(X139_256, a747) | ~c2_1(X139_256) | c5_2(X139_256, X140_257) | c3_2(X139_256, X140_257) | ~c1_2(X139_256, X140_257)))). % 17.94/5.59 tff(c_5012, plain, (~c10_2(a633, a634))). % 17.94/5.59 tff(c_5008, plain, (c4_2(a633, a634))). % 17.94/5.59 tff(c_4995, plain, (c9_2(a633, a634))). % 17.94/5.60 tff(c_4953, plain, (![X139_192, X140_194]: (c7_2(X139_192, a619) | c7_1(X139_192) | c4_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.60 tff(c_4957, plain, (c7_1(a737))). % 17.94/5.60 tff(c_4945, plain, (![X3_11, X4_13]: (c7_2(X3_11, a619) | c7_1(X3_11) | c4_2(X3_11, X4_13) | ~c9_2(X3_11, X4_13)))). % 17.94/5.60 tff(c_4935, plain, (~c3_2(a698, a619))). % 17.94/5.60 tff(c_4877, plain, (![X139_192, X140_194]: (~c3_2(X139_192, a619) | c7_1(X139_192) | c4_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.60 tff(c_4881, plain, (~c3_2(a737, a619))). % 17.94/5.60 tff(c_4869, plain, (![X3_11, X4_13]: (~c3_2(X3_11, a619) | c7_1(X3_11) | c4_2(X3_11, X4_13) | ~c9_2(X3_11, X4_13)))). % 17.94/5.60 tff(c_4865, plain, (~c4_2(a741, a742))). % 17.94/5.60 tff(c_4856, plain, (~c1_2(a741, a742))). % 17.94/5.60 tff(c_4853, plain, (c10_2(a741, a742))). % 17.94/5.60 tff(c_4637, plain, (![X73_285]: (c1_2(X73_285, a675) | ~c2_2(X73_285, a675) | c1_2(X73_285, a678) | c7_1(X73_285) | c1_2(X73_285, a676) | ~c2_2(X73_285, a676) | c2_2(X73_285, a677)))). % 17.94/5.60 tff(c_4469, plain, (![X73_273]: (c1_2(X73_273, a675) | ~c2_2(X73_273, a675) | ~c6_2(X73_273, a678) | c7_1(X73_273) | c1_2(X73_273, a676) | ~c2_2(X73_273, a676) | c5_2(X73_273, a677)))). % 17.94/5.60 tff(c_4456, plain, (![X73_271]: (c1_2(X73_271, a675) | ~c2_2(X73_271, a675) | ~c6_2(X73_271, a678) | c7_1(X73_271) | c1_2(X73_271, a676) | ~c2_2(X73_271, a676) | c2_2(X73_271, a677)))). % 17.94/5.60 tff(c_4594, plain, (![X73_279]: (c1_2(X73_279, a675) | ~c2_2(X73_279, a675) | c1_2(X73_279, a678) | c7_1(X73_279) | c1_2(X73_279, a676) | ~c2_2(X73_279, a676) | c5_2(X73_279, a677)))). % 17.94/5.60 tff(c_4806, plain, (~c3_1(a670))). % 17.94/5.60 tff(c_4796, plain, (c10_1(a633))). % 17.94/5.60 tff(c_4764, plain, (~c2_1(a633))). % 17.94/5.60 tff(c_4744, plain, (![X96_134]: (~c7_2(a705, X96_134) | ~c6_2(a705, X96_134) | ~c2_2(a705, X96_134)))). % 17.94/5.60 tff(c_4738, plain, (c9_1(a670))). % 17.94/5.60 tff(c_4734, plain, (![X97_135]: (~c9_2(X97_135, a706) | ~c1_1(X97_135) | ~c9_1(X97_135)))). % 17.94/5.60 tff(c_4722, plain, (~c8_1(a669))). % 17.94/5.60 tff(c_4719, plain, (c4_2(a669, a676))). % 17.94/5.60 tff(c_4693, plain, (![X67_98]: (c3_2(a669, X67_98) | c5_2(a669, X67_98) | c4_2(a669, X67_98)))). % 17.94/5.60 tff(c_4687, plain, (c8_1(a670))). % 17.94/5.60 tff(c_4684, plain, (~c5_1(a741))). % 17.94/5.60 tff(c_4664, plain, (~c4_1(a648))). % 17.94/5.60 tff(c_4660, plain, (~c7_1(a648))). % 17.94/5.60 tff(c_4651, plain, (c3_1(a648))). % 17.94/5.60 tff(c_4582, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a675) | ~c2_2(X73_106, a675) | ~c5_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4583, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c8_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4584, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c5_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4581, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | ~c1_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4580, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c5_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4579, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | ~c1_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4578, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a675) | ~c2_2(X73_106, a675) | ~c5_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4577, plain, (![X73_106]: (c1_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c8_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4576, plain, (![X60_89]: (c1_2(X60_89, a678) | c1_2(X60_89, a666) | ~c2_2(X60_89, a666) | ~c3_1(X60_89) | c7_1(X60_89)))). % 17.94/5.60 tff(c_4536, plain, (![X75_108, X76_110]: (c1_2(X75_108, a678) | c7_1(X75_108) | c1_2(X75_108, X76_110) | ~c2_2(X75_108, X76_110) | ~c8_2(X75_108, X76_110)))). % 17.94/5.60 tff(c_4485, plain, (~c5_2(a669, a676))). % 17.94/5.60 tff(c_4484, plain, (~c2_2(a669, a676))). % 17.94/5.60 tff(c_4417, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | ~c1_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4416, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c5_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4413, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c8_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4420, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c5_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4419, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | c8_2(X73_106, a675) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4418, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a675) | ~c2_2(X73_106, a675) | ~c5_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4415, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a676) | ~c2_2(X73_106, a676) | ~c1_2(X73_106, a675) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_4414, plain, (![X73_106]: (~c6_2(X73_106, a678) | c7_1(X73_106) | c1_2(X73_106, a675) | ~c2_2(X73_106, a675) | ~c5_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_4431, plain, (~c3_1(a669))). % 17.94/5.60 tff(c_4412, plain, (![X60_89]: (~c6_2(X60_89, a678) | c1_2(X60_89, a666) | ~c2_2(X60_89, a666) | ~c3_1(X60_89) | c7_1(X60_89)))). % 17.94/5.60 tff(c_4422, plain, (~c2_2(a729, a730))). % 17.94/5.60 tff(c_4380, plain, (![X75_108, X76_110]: (~c6_2(X75_108, a678) | c7_1(X75_108) | c1_2(X75_108, X76_110) | ~c2_2(X75_108, X76_110) | ~c8_2(X75_108, X76_110)))). % 17.94/5.60 tff(c_4370, plain, (![X75_108, X76_110]: (~c8_2(X75_108, a678) | c7_1(X75_108) | c1_2(X75_108, X76_110) | ~c2_2(X75_108, X76_110) | ~c8_2(X75_108, X76_110)))). % 17.94/5.60 tff(c_4338, plain, (![X139_258]: (~c1_2(X139_258, a675) | c2_2(X139_258, a677) | ~c1_2(X139_258, a747) | ~c2_1(X139_258) | c3_2(X139_258, a676) | ~c1_2(X139_258, a676)))). % 17.94/5.60 tff(c_4337, plain, (![X139_258]: (c5_2(X139_258, a675) | c2_2(X139_258, a677) | ~c1_2(X139_258, a747) | ~c2_1(X139_258) | c3_2(X139_258, a676) | ~c1_2(X139_258, a676)))). % 17.94/5.60 tff(c_4340, plain, (![X139_258]: (~c7_1(X139_258) | ~c8_1(X139_258) | ~c1_2(X139_258, a747) | ~c2_1(X139_258) | c3_2(X139_258, a627) | ~c1_2(X139_258, a627)))). % 17.94/5.60 tff(c_4350, plain, (~c1_2(a641, a644))). % 17.94/5.60 tff(c_4347, plain, (~c1_2(a698, a747))). % 17.94/5.60 tff(c_4306, plain, (![X139_192, X140_194]: (~c1_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.60 tff(c_4301, plain, (~c2_1(a645))). % 17.94/5.60 tff(c_4275, plain, (![X139_192, X140_194]: (c9_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.60 tff(c_4272, plain, (~c2_1(a658))). % 17.94/5.60 tff(c_4241, plain, (![X139_192]: (~c2_1(X139_192) | c3_2(X139_192, a747) | ~c1_2(X139_192, a747) | c5_2(X139_192, a747)))). % 17.94/5.60 tff(c_4228, plain, (![X139_192, X140_194]: (c5_2(X139_192, a747) | ~c2_1(X139_192) | c5_2(X139_192, X140_194) | c3_2(X139_192, X140_194) | ~c1_2(X139_192, X140_194)))). % 17.94/5.60 tff(c_4221, plain, (~c5_1(a721))). % 17.94/5.60 tff(c_4216, plain, (c4_1(a721))). % 17.94/5.60 tff(c_4211, plain, (~c1_1(a721))). % 17.94/5.60 tff(c_4189, plain, (![X60_89]: (~c7_2(X60_89, a666) | ~c3_1(X60_89) | c7_1(X60_89)))). % 17.94/5.60 tff(c_4185, plain, (~c10_2(a737, a738))). % 17.94/5.60 tff(c_4179, plain, (![X84_119, X85_121]: (~c3_1(X84_119) | ~c8_1(X84_119) | ~c10_2(X84_119, X85_121) | c6_2(X84_119, X85_121) | ~c9_2(X84_119, X85_121)))). % 17.94/5.60 tff(c_4163, plain, (![X60_89]: (c8_2(X60_89, a666) | ~c3_1(X60_89) | c7_1(X60_89)))). % 17.94/5.60 tff(c_4152, plain, (![X66_97]: (c1_2(a669, X66_97) | c6_2(a669, X66_97)))). % 17.94/5.60 tff(c_4143, plain, (![X60_89]: (c3_2(X60_89, a666) | ~c3_1(X60_89) | c7_1(X60_89)))). % 17.94/5.60 tff(c_4085, plain, (![X33_54]: (~c9_2(a645, X33_54) | ~c5_2(a645, X33_54) | ~c2_2(a645, X33_54)))). % 17.94/5.60 tff(c_4053, plain, (c8_1(a707))). % 17.94/5.60 tff(c_4002, plain, (~c10_1(a707))). % 17.94/5.60 tff(c_3998, plain, (c9_1(a697))). % 17.94/5.60 tff(c_3978, plain, (~c4_1(a700))). % 17.94/5.60 tff(c_3977, plain, (~c4_1(a739))). % 17.94/5.60 tff(c_3976, plain, (~c4_1(a628))). % 17.94/5.60 tff(c_3965, plain, (![X78_112]: (c7_1(X78_112) | ~c4_1(X78_112)))). % 17.94/5.60 tff(c_3945, plain, (~c5_2(a658, a676))). % 17.94/5.60 tff(c_3941, plain, (![X73_106]: (~c1_2(X73_106, a675) | ~c9_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3938, plain, (![X73_106]: (c5_2(X73_106, a675) | ~c5_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3935, plain, (![X73_106]: (~c1_2(X73_106, a675) | ~c9_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3932, plain, (![X73_106]: (c8_2(X73_106, a675) | c8_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3929, plain, (![X73_106]: (c5_2(X73_106, a675) | ~c5_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3926, plain, (![X73_106]: (~c1_2(X73_106, a675) | ~c5_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3923, plain, (![X73_106]: (c8_2(X73_106, a675) | ~c5_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3920, plain, (![X73_106]: (c5_2(X73_106, a675) | ~c9_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3917, plain, (![X73_106]: (c8_2(X73_106, a675) | ~c9_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3914, plain, (![X73_106]: (c8_2(X73_106, a675) | c8_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3911, plain, (![X73_106]: (c8_2(X73_106, a675) | ~c5_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3903, plain, (![X73_106]: (c5_2(X73_106, a675) | ~c5_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3900, plain, (![X73_106]: (~c1_2(X73_106, a675) | c8_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3895, plain, (![X73_106]: (c5_2(X73_106, a675) | c8_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3892, plain, (![X73_106]: (c5_2(X73_106, a675) | c8_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3889, plain, (![X73_106]: (~c1_2(X73_106, a675) | c8_2(X73_106, a676) | ~c9_2(X73_106, a677)))). % 17.94/5.60 tff(c_3886, plain, (![X73_106]: (~c1_2(X73_106, a675) | c8_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3881, plain, (![X73_106]: (c8_2(X73_106, a675) | ~c9_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3876, plain, (![X73_106]: (c8_2(X73_106, a675) | ~c9_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3873, plain, (![X73_106]: (~c1_2(X73_106, a675) | ~c9_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3870, plain, (![X73_106]: (~c1_2(X73_106, a675) | ~c5_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3865, plain, (![X73_106]: (c8_2(X73_106, a675) | ~c5_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3860, plain, (![X73_106]: (c5_2(X73_106, a675) | ~c9_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3849, plain, (![X73_106]: (c8_2(X73_106, a675) | c8_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3846, plain, (![X73_106]: (c5_2(X73_106, a675) | c8_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3836, plain, (![X73_106]: (~c1_2(X73_106, a675) | ~c5_2(X73_106, a676) | c5_2(X73_106, a677)))). % 17.94/5.60 tff(c_3823, plain, (![X73_106]: (c5_2(X73_106, a675) | ~c9_2(X73_106, a676) | c2_2(X73_106, a677)))). % 17.94/5.60 tff(c_3804, plain, (![X45_70]: (~c4_2(a658, X45_70) | ~c3_2(a658, X45_70) | ~c5_2(a658, X45_70)))). % 17.94/5.60 tff(c_3775, plain, (~c9_1(a668))). % 17.94/5.60 tff(c_3724, plain, (![X14_26]: (~c10_2(X14_26, a627) | ~c7_1(X14_26) | ~c8_1(X14_26)))). % 17.94/5.60 tff(c_3705, plain, (![X14_26]: (~c2_2(X14_26, a627) | ~c7_1(X14_26) | ~c8_1(X14_26)))). % 17.94/5.60 tff(c_3695, plain, (![X14_26]: (~c5_2(X14_26, a627) | ~c7_1(X14_26) | ~c8_1(X14_26)))). % 17.94/5.60 tff(c_3684, plain, (~c2_1(a665))). % 17.94/5.60 tff(c_3649, plain, (c5_1(a660))). % 17.94/5.60 tff(c_3646, plain, (~c7_1(a628))). % 17.94/5.60 tff(c_3627, plain, (~c6_1(a660))). % 17.94/5.61 tff(c_3616, plain, (~c3_1(a705))). % 17.94/5.61 tff(c_3612, plain, (~c10_1(a660))). % 17.94/5.61 tff(c_3598, plain, (~c9_1(a705))). % 17.94/5.61 tff(c_3546, plain, (~c5_0)). % 17.94/5.61 tff(c_3498, plain, (c1_2(a737, a738))). % 17.94/5.61 tff(c_3495, plain, (~c3_2(a645, a646))). % 17.94/5.61 tff(c_3477, plain, (~c5_2(a645, a646))). % 17.94/5.61 tff(c_3472, plain, (~c9_2(a645, a646))). % 17.94/5.61 tff(c_3460, plain, (c9_2(a737, a738))). % 17.94/5.61 tff(c_3457, plain, (~c3_2(a734, a736))). % 17.94/5.61 tff(c_3452, plain, (~c7_2(a734, a735))). % 17.94/5.61 tff(c_3447, plain, (~c4_2(a737, a738))). % 17.94/5.61 tff(c_3437, plain, (~c9_2(a645, a647))). % 17.94/5.61 tff(c_3433, plain, (c5_2(a645, a647))). % 17.94/5.61 tff(c_3431, plain, (~c5_2(a641, a644))). % 17.94/5.61 tff(c_3429, plain, (~c9_2(a641, a644))). % 17.94/5.61 tff(c_3427, plain, (~c3_2(a645, a647))). % 17.94/5.61 tff(c_3393, plain, (c6_2(a622, a623))). % 17.94/5.61 tff(c_3354, plain, (c5_1(a695))). % 17.94/5.61 tff(c_3341, plain, (~c3_2(a692, a694))). % 17.94/5.61 tff(c_3327, plain, (~c7_2(a692, a693))). % 17.94/5.61 tff(c_3321, plain, (c8_2(a729, a730))). % 17.94/5.61 tff(c_3313, plain, (c7_2(a729, a730))). % 17.94/5.61 tff(c_3302, plain, (~c10_2(a692, a694))). % 17.94/5.61 tff(c_3298, plain, (~c9_2(a729, a730))). % 17.94/5.61 tff(c_3295, plain, (c1_2(a622, a623))). % 17.94/5.61 tff(c_3288, plain, (c2_2(a622, a623))). % 17.94/5.61 tff(c_3281, plain, (~c5_1(a692))). % 17.94/5.61 tff(c_3270, plain, (~c2_1(a739))). % 17.94/5.61 tff(c_3257, plain, (![X73_106]: (ndr1_1(X73_106)))). % 17.94/5.61 tff(c_3253, plain, (c4_1(a622))). % 17.94/5.61 tff(c_3239, plain, (~c7_1(a739))). % 17.94/5.61 tff(c_3233, plain, (~c5_1(a739))). % 17.94/5.61 tff(c_3219, plain, (~c4_1(a737))). % 17.94/5.61 tff(c_3211, plain, (~c3_1(a621))). % 17.94/5.61 tff(c_3206, plain, (~c1_1(a696))). % 17.94/5.61 tff(c_3202, plain, (~c9_1(a740))). % 17.94/5.61 tff(c_3200, plain, (c9_1(a737))). % 17.94/5.61 tff(c_3187, plain, (~c8_1(a695))). % 17.94/5.61 tff(c_3181, plain, (c3_1(a729))). % 17.94/5.61 tff(c_3176, plain, (~c10_1(a695))). % 17.94/5.61 tff(c_3167, plain, (~c7_1(a700))). % 17.94/5.61 tff(c_3164, plain, (~c9_1(a729))). % 17.94/5.61 tff(c_3158, plain, (~c3_1(a697))). % 17.94/5.61 tff(c_3156, plain, (~c8_1(a622))). % 17.94/5.61 tff(c_3153, plain, (c1_2(a698, a699))). % 17.94/5.61 tff(c_3150, plain, (~c2_1(a669))). % 17.94/5.61 tff(c_3149, plain, (~c10_1(a700))). % 17.94/5.61 tff(c_3143, plain, (~c10_1(a734))). % 17.94/5.61 tff(c_3140, plain, (~c5_2(a698, a699))). % 17.94/5.61 tff(c_3137, plain, (~c9_1(a700))). % 17.94/5.61 tff(c_3127, plain, (~c8_1(a701))). % 17.94/5.61 tff(c_3124, plain, (~c5_1(a708))). % 17.94/5.61 tff(c_3112, plain, (c1_0)). % 17.94/5.61 tff(c_3098, plain, (c2_1(a698))). % 17.94/5.61 tff(c_3094, plain, (c9_1(a698))). % 17.94/5.61 tff(c_3083, plain, (~c6_0)). % 17.94/5.61 tff(c_3069, plain, (c7_1(a658))). % 17.94/5.61 tff(c_3067, plain, (c4_0)). % 17.94/5.61 tff(c_3065, plain, (c9_0)). % 17.94/5.61 tff(c_3064, plain, (~c10_0)). % 17.94/5.61 tff(c_3063, plain, (c7_0)). % 17.94/5.61 tff(c_3050, plain, (~c2_0)). % 17.94/5.61 tff(c_3047, plain, (c8_0)). % 17.94/5.61 tff(c_3046, plain, (ndr1_0)). % 17.94/5.61 tff(c_3005, plain, (~c3_0)). % 17.94/5.61 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 17.94/5.61 %------------------------------------------------------------------------------