%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO582+1 : TPTP v9.0.0. Released v5.5.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 : n031.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:37:53 PM UTC 2025
% Result : CounterSatisfiable 5.27s 2.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO582+1 : TPTP v9.0.0. Released v5.5.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n031.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 09:22:22 EDT 2025
% 0.12/0.34 % CPUTime :
% 5.27/2.24
% 5.27/2.25 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.27/2.25
% 5.27/2.25 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.27/2.25 %$ k04_buttercup10517 > k04_buttercup10516 > k04_buttercup10419 > k04_buttercup10225 > b48_buttercup10521 > b48_buttercup10520 > b48_buttercup10519 > b48_buttercup10518 > b48_buttercup10515 > b48_buttercup10422 > b48_buttercup10421 > b48_buttercup10417 > b48_buttercup10229 > b48_buttercup10228 > b48_buttercup10227 > b48_buttercup10222 > #nlpp > #skF_33 > #skF_20 > #skF_18 > #skF_17 > #skF_11 > #skF_31 > #skF_15 > #skF_25 > #skF_19 > #skF_7 > #skF_10 > #skF_16 > #skF_26 > #skF_14 > #skF_5 > #skF_6 > #skF_13 > #skF_2 > #skF_3 > #skF_1 > #skF_21 > #skF_9 > #skF_32 > #skF_8 > #skF_30 > #skF_4 > #skF_22 > #skF_29 > #skF_28 > #skF_35 > #skF_24 > #skF_27 > #skF_23 > #skF_12 > #skF_34
% 5.27/2.25
% 5.27/2.25 %Foreground sorts:
% 5.27/2.25
% 5.27/2.25
% 5.27/2.25 %Background operators:
% 5.27/2.25
% 5.27/2.25
% 5.27/2.25 %Foreground operators:
% 5.27/2.25 tff(b48_buttercup10521, type, b48_buttercup10521: $i > $o).
% 5.27/2.25 tff('#skF_33', type, '#skF_33': $i).
% 5.27/2.25 tff(b48_buttercup10229, type, b48_buttercup10229: $i > $o).
% 5.27/2.25 tff(b48_buttercup10519, type, b48_buttercup10519: $i > $o).
% 5.27/2.25 tff(b48_buttercup10227, type, b48_buttercup10227: $i > $o).
% 5.27/2.25 tff('#skF_20', type, '#skF_20': $i).
% 5.27/2.25 tff('#skF_18', type, '#skF_18': $i).
% 5.27/2.25 tff(b48_buttercup10417, type, b48_buttercup10417: $i > $o).
% 5.27/2.25 tff('#skF_17', type, '#skF_17': $i).
% 5.27/2.25 tff('#skF_11', type, '#skF_11': $i).
% 5.27/2.25 tff('#skF_31', type, '#skF_31': $i).
% 5.27/2.25 tff('#skF_15', type, '#skF_15': $i).
% 5.27/2.25 tff('#skF_25', type, '#skF_25': $i).
% 5.27/2.25 tff(k04_buttercup10419, type, k04_buttercup10419: $i > $o).
% 5.27/2.25 tff(k04_buttercup10517, type, k04_buttercup10517: $i > $o).
% 5.27/2.25 tff(k04_buttercup10225, type, k04_buttercup10225: $i > $o).
% 5.27/2.25 tff(k04_buttercup10516, type, k04_buttercup10516: $i > $o).
% 5.27/2.25 tff(b48_buttercup10520, type, b48_buttercup10520: $i > $o).
% 5.27/2.25 tff('#skF_19', type, '#skF_19': $i).
% 5.27/2.25 tff('#skF_7', type, '#skF_7': $i).
% 5.27/2.25 tff('#skF_10', type, '#skF_10': $i).
% 5.27/2.25 tff('#skF_16', type, '#skF_16': $i).
% 5.27/2.25 tff(b48_buttercup10422, type, b48_buttercup10422: $i > $o).
% 5.27/2.25 tff('#skF_26', type, '#skF_26': $i).
% 5.27/2.25 tff('#skF_14', type, '#skF_14': $i).
% 5.27/2.25 tff('#skF_5', type, '#skF_5': $i).
% 5.27/2.25 tff('#skF_6', type, '#skF_6': $i).
% 5.27/2.25 tff('#skF_13', type, '#skF_13': $i).
% 5.27/2.25 tff('#skF_2', type, '#skF_2': $i).
% 5.27/2.25 tff('#skF_3', type, '#skF_3': $i).
% 5.27/2.25 tff('#skF_1', type, '#skF_1': $i).
% 5.27/2.25 tff('#skF_21', type, '#skF_21': $i).
% 5.27/2.25 tff('#skF_9', type, '#skF_9': $i).
% 5.27/2.25 tff('#skF_32', type, '#skF_32': $i).
% 5.27/2.25 tff(b48_buttercup10228, type, b48_buttercup10228: $i > $o).
% 5.27/2.25 tff('#skF_8', type, '#skF_8': $i).
% 5.27/2.25 tff('#skF_30', type, '#skF_30': $i).
% 5.27/2.25 tff('#skF_4', type, '#skF_4': $i).
% 5.27/2.25 tff(b48_buttercup10222, type, b48_buttercup10222: $i > $o).
% 5.27/2.25 tff('#skF_22', type, '#skF_22': $i).
% 5.27/2.25 tff('#skF_29', type, '#skF_29': $i).
% 5.27/2.25 tff('#skF_28', type, '#skF_28': $i).
% 5.27/2.25 tff('#skF_35', type, '#skF_35': $i).
% 5.27/2.25 tff('#skF_24', type, '#skF_24': $i).
% 5.27/2.25 tff('#skF_27', type, '#skF_27': $i).
% 5.27/2.25 tff('#skF_23', type, '#skF_23': $i).
% 5.27/2.25 tff(b48_buttercup10518, type, b48_buttercup10518: $i > $o).
% 5.27/2.25 tff('#skF_12', type, '#skF_12': $i).
% 5.27/2.25 tff(b48_buttercup10421, type, b48_buttercup10421: $i > $o).
% 5.27/2.25 tff(b48_buttercup10515, type, b48_buttercup10515: $i > $o).
% 5.27/2.25 tff('#skF_34', type, '#skF_34': $i).
% 5.27/2.25
% 5.27/2.25 %Saturated clause set:
% 5.27/2.26 tff(c_1077, plain, (~b48_buttercup10227('#skF_14'))).
% 5.27/2.26 tff(c_1065, plain, (![X12_94]: (b48_buttercup10417(X12_94) | ~b48_buttercup10227(X12_94)))).
% 5.27/2.26 tff(c_1072, plain, (~b48_buttercup10229('#skF_14'))).
% 5.27/2.26 tff(c_1052, plain, (![X21_93]: (b48_buttercup10417(X21_93) | ~b48_buttercup10229(X21_93)))).
% 5.27/2.26 tff(c_1054, plain, (~b48_buttercup10229('#skF_9'))).
% 5.27/2.26 tff(c_1066, plain, (~b48_buttercup10227('#skF_7'))).
% 5.27/2.26 tff(c_1067, plain, (~b48_buttercup10227('#skF_9'))).
% 5.27/2.26 tff(c_1053, plain, (~b48_buttercup10229('#skF_7'))).
% 5.27/2.26 tff(c_943, plain, (![X12_87]: (b48_buttercup10515(X12_87) | ~b48_buttercup10227(X12_87)))).
% 5.27/2.26 tff(c_986, plain, (![X21_90]: (b48_buttercup10515(X21_90) | ~b48_buttercup10229(X21_90)))).
% 5.27/2.26 tff(c_1033, plain, (b48_buttercup10417('#skF_16'))).
% 5.27/2.26 tff(c_1032, plain, (b48_buttercup10417('#skF_2'))).
% 5.27/2.26 tff(c_1031, plain, (b48_buttercup10417('#skF_8'))).
% 5.27/2.26 tff(c_1034, plain, (b48_buttercup10417('#skF_34'))).
% 5.27/2.26 tff(c_1035, plain, (b48_buttercup10417('#skF_32'))).
% 5.27/2.26 tff(c_1039, plain, (b48_buttercup10417('#skF_20'))).
% 5.27/2.26 tff(c_1040, plain, (b48_buttercup10417('#skF_31'))).
% 5.27/2.26 tff(c_1041, plain, (b48_buttercup10417('#skF_27'))).
% 5.27/2.26 tff(c_1038, plain, (b48_buttercup10417('#skF_30'))).
% 5.27/2.26 tff(c_1037, plain, (b48_buttercup10417('#skF_35'))).
% 5.27/2.26 tff(c_1036, plain, (b48_buttercup10417('#skF_29'))).
% 5.27/2.26 tff(c_679, plain, (![X23_63]: (b48_buttercup10417(X23_63) | ~b48_buttercup10515(X23_63)))).
% 5.27/2.26 tff(c_996, plain, (~b48_buttercup10421('#skF_7'))).
% 5.27/2.26 tff(c_953, plain, (![X28_88]: (k04_buttercup10516(X28_88) | ~b48_buttercup10421(X28_88)))).
% 5.27/2.26 tff(c_836, plain, (![X21_15]: (b48_buttercup10519(X21_15) | ~b48_buttercup10229(X21_15)))).
% 5.27/2.26 tff(c_977, plain, (b48_buttercup10222('#skF_2'))).
% 5.27/2.26 tff(c_978, plain, (b48_buttercup10222('#skF_35'))).
% 5.27/2.26 tff(c_976, plain, (b48_buttercup10222('#skF_8'))).
% 5.27/2.26 tff(c_975, plain, (b48_buttercup10222('#skF_16'))).
% 5.27/2.26 tff(c_74, plain, (![X25_17]: (b48_buttercup10222(X25_17) | ~k04_buttercup10225(X25_17)))).
% 5.27/2.26 tff(c_86, plain, (![X28_18]: (k04_buttercup10517(X28_18) | ~b48_buttercup10421(X28_18)))).
% 5.27/2.26 tff(c_933, plain, (~b48_buttercup10228('#skF_11'))).
% 5.27/2.26 tff(c_935, plain, (~b48_buttercup10228('#skF_15'))).
% 5.27/2.26 tff(c_934, plain, (~b48_buttercup10228('#skF_6'))).
% 5.27/2.26 tff(c_858, plain, (![X12_79]: (b48_buttercup10519(X12_79) | ~b48_buttercup10227(X12_79)))).
% 5.27/2.26 tff(c_38, plain, (![X14_13]: (k04_buttercup10419(X14_13) | ~b48_buttercup10228(X14_13)))).
% 5.27/2.26 tff(c_921, plain, (b48_buttercup10222('#skF_28'))).
% 5.27/2.26 tff(c_922, plain, (k04_buttercup10419('#skF_12'))).
% 5.27/2.26 tff(c_18, plain, (![X8_9]: (b48_buttercup10222(X8_9) | ~b48_buttercup10228(X8_9)))).
% 5.27/2.26 tff(c_910, plain, (b48_buttercup10515('#skF_8'))).
% 5.27/2.26 tff(c_911, plain, (b48_buttercup10515('#skF_2'))).
% 5.27/2.26 tff(c_912, plain, (b48_buttercup10515('#skF_16'))).
% 5.27/2.26 tff(c_913, plain, (b48_buttercup10515('#skF_34'))).
% 5.27/2.26 tff(c_914, plain, (b48_buttercup10515('#skF_32'))).
% 5.27/2.26 tff(c_915, plain, (b48_buttercup10515('#skF_29'))).
% 5.27/2.26 tff(c_916, plain, (b48_buttercup10515('#skF_35'))).
% 5.27/2.26 tff(c_887, plain, (b48_buttercup10515('#skF_30'))).
% 5.27/2.26 tff(c_6, plain, (![X2_3]: (b48_buttercup10515(X2_3) | ~b48_buttercup10519(X2_3)))).
% 5.27/2.26 tff(c_4, plain, (![X1_2]: (b48_buttercup10515(X1_2) | ~b48_buttercup10518(X1_2)))).
% 5.27/2.26 tff(c_882, plain, (b48_buttercup10515('#skF_20'))).
% 5.27/2.26 tff(c_10, plain, (![X4_5]: (b48_buttercup10515(X4_5) | ~b48_buttercup10521(X4_5)))).
% 5.27/2.26 tff(c_877, plain, (b48_buttercup10222('#skF_24'))).
% 5.27/2.26 tff(c_20, plain, (![X9_10]: (b48_buttercup10222(X9_10) | ~b48_buttercup10229(X9_10)))).
% 5.27/2.26 tff(c_861, plain, (~b48_buttercup10227('#skF_33'))).
% 5.27/2.26 tff(c_860, plain, (~b48_buttercup10227('#skF_32'))).
% 5.27/2.26 tff(c_859, plain, (~b48_buttercup10227('#skF_34'))).
% 5.27/2.26 tff(c_872, plain, (b48_buttercup10417('#skF_22'))).
% 5.27/2.26 tff(c_12, plain, (![X5_6]: (b48_buttercup10417(X5_6) | ~b48_buttercup10421(X5_6)))).
% 5.27/2.26 tff(c_862, plain, (~b48_buttercup10227('#skF_10'))).
% 5.27/2.26 tff(c_32, plain, (![X12_12]: (k04_buttercup10225(X12_12) | ~b48_buttercup10227(X12_12)))).
% 5.27/2.26 tff(c_838, plain, (b48_buttercup10519('#skF_8'))).
% 5.27/2.26 tff(c_839, plain, (b48_buttercup10519('#skF_2'))).
% 5.27/2.26 tff(c_837, plain, (b48_buttercup10519('#skF_16'))).
% 5.27/2.27 tff(c_799, plain, (![X52_21]: (b48_buttercup10519(X52_21) | ~k04_buttercup10225(X52_21)))).
% 5.27/2.27 tff(c_819, plain, (b48_buttercup10515('#skF_31'))).
% 5.27/2.27 tff(c_8, plain, (![X3_4]: (b48_buttercup10515(X3_4) | ~b48_buttercup10520(X3_4)))).
% 5.27/2.27 tff(c_814, plain, (b48_buttercup10222('#skF_23'))).
% 5.27/2.27 tff(c_16, plain, (![X7_8]: (b48_buttercup10222(X7_8) | ~b48_buttercup10227(X7_8)))).
% 5.27/2.27 tff(c_809, plain, (b48_buttercup10421('#skF_17'))).
% 5.27/2.27 tff(c_84, plain, (![X28_18]: (b48_buttercup10421(X28_18) | ~k04_buttercup10517(X28_18)))).
% 5.27/2.27 tff(c_804, plain, (~b48_buttercup10422('#skF_11'))).
% 5.27/2.27 tff(c_800, plain, (~k04_buttercup10419('#skF_11'))).
% 5.27/2.27 tff(c_760, plain, (b48_buttercup10417('#skF_17'))).
% 5.27/2.27 tff(c_756, plain, (b48_buttercup10417('#skF_21'))).
% 5.27/2.27 tff(c_751, plain, (k04_buttercup10516('#skF_17'))).
% 5.27/2.27 tff(c_14, plain, (![X6_7]: (b48_buttercup10417(X6_7) | ~b48_buttercup10422(X6_7)))).
% 5.27/2.27 tff(c_2, plain, (![X0_1]: (k04_buttercup10516(X0_1) | ~k04_buttercup10517(X0_1)))).
% 5.27/2.27 tff(c_704, plain, (~b48_buttercup10229('#skF_32'))).
% 5.27/2.27 tff(c_705, plain, (~b48_buttercup10229('#skF_33'))).
% 5.27/2.27 tff(c_703, plain, (~b48_buttercup10229('#skF_34'))).
% 5.27/2.27 tff(c_706, plain, (~b48_buttercup10229('#skF_10'))).
% 5.27/2.27 tff(c_62, plain, (![X21_15]: (k04_buttercup10225(X21_15) | ~b48_buttercup10229(X21_15)))).
% 5.27/2.27 tff(c_689, plain, (~b48_buttercup10422('#skF_15'))).
% 5.27/2.27 tff(c_688, plain, (~b48_buttercup10422('#skF_6'))).
% 5.27/2.27 tff(c_26, plain, (![X10_11]: (k04_buttercup10419(X10_11) | ~b48_buttercup10422(X10_11)))).
% 5.27/2.27 tff(c_680, plain, (~b48_buttercup10515('#skF_7'))).
% 5.27/2.27 tff(c_68, plain, (![X23_16]: (k04_buttercup10516(X23_16) | ~b48_buttercup10515(X23_16)))).
% 5.27/2.27 tff(c_669, plain, (b48_buttercup10417('#skF_18'))).
% 5.27/2.27 tff(c_670, plain, (b48_buttercup10417('#skF_9'))).
% 5.27/2.27 tff(c_671, plain, (b48_buttercup10519('#skF_34'))).
% 5.27/2.27 tff(c_56, plain, (![X19_14]: (b48_buttercup10417(X19_14) | ~k04_buttercup10516(X19_14)))).
% 5.27/2.27 tff(c_661, plain, (~b48_buttercup10421('#skF_12'))).
% 5.27/2.27 tff(c_660, plain, (~k04_buttercup10225('#skF_34'))).
% 5.27/2.27 tff(c_656, plain, (b48_buttercup10519('#skF_32'))).
% 5.27/2.27 tff(c_658, plain, (~k04_buttercup10225('#skF_32'))).
% 5.27/2.27 tff(c_657, plain, (~k04_buttercup10225('#skF_33'))).
% 5.27/2.27 tff(c_149, plain, (~b48_buttercup10519('#skF_33'))).
% 5.27/2.27 tff(c_100, plain, (k04_buttercup10225('#skF_16'))).
% 5.27/2.27 tff(c_120, plain, (b48_buttercup10222('#skF_26'))).
% 5.27/2.27 tff(c_104, plain, (k04_buttercup10516('#skF_18'))).
% 5.27/2.27 tff(c_102, plain, (k04_buttercup10517('#skF_17'))).
% 5.27/2.27 tff(c_124, plain, (b48_buttercup10228('#skF_28'))).
% 5.27/2.27 tff(c_126, plain, (b48_buttercup10519('#skF_29'))).
% 5.27/2.27 tff(c_58, plain, (~b48_buttercup10229('#skF_8'))).
% 5.27/2.27 tff(c_98, plain, (k04_buttercup10419('#skF_13'))).
% 5.27/2.27 tff(c_46, plain, (k04_buttercup10419('#skF_5'))).
% 5.27/2.27 tff(c_52, plain, (~k04_buttercup10516('#skF_7'))).
% 5.27/2.27 tff(c_94, plain, (k04_buttercup10419('#skF_14'))).
% 5.27/2.27 tff(c_54, plain, (b48_buttercup10417('#skF_7'))).
% 5.27/2.27 tff(c_50, plain, (k04_buttercup10419('#skF_4'))).
% 5.27/2.27 tff(c_48, plain, (b48_buttercup10222('#skF_4'))).
% 5.27/2.27 tff(c_106, plain, (k04_buttercup10419('#skF_19'))).
% 5.27/2.27 tff(c_60, plain, (k04_buttercup10225('#skF_8'))).
% 5.27/2.27 tff(c_96, plain, (b48_buttercup10417('#skF_13'))).
% 5.27/2.27 tff(c_42, plain, (~k04_buttercup10419('#skF_6'))).
% 5.27/2.27 tff(c_30, plain, (k04_buttercup10225('#skF_2'))).
% 5.27/2.27 tff(c_88, plain, (b48_buttercup10417('#skF_15'))).
% 5.27/2.27 tff(c_44, plain, (~b48_buttercup10222('#skF_5'))).
% 5.27/2.27 tff(c_122, plain, (b48_buttercup10515('#skF_27'))).
% 5.27/2.27 tff(c_36, plain, (k04_buttercup10419('#skF_3'))).
% 5.27/2.27 tff(c_40, plain, (b48_buttercup10222('#skF_6'))).
% 5.27/2.27 tff(c_128, plain, (b48_buttercup10518('#skF_30'))).
% 5.27/2.27 tff(c_112, plain, (b48_buttercup10421('#skF_22'))).
% 5.27/2.27 tff(c_92, plain, (~b48_buttercup10417('#skF_14'))).
% 5.27/2.27 tff(c_34, plain, (~b48_buttercup10228('#skF_3'))).
% 5.27/2.27 tff(c_24, plain, (k04_buttercup10419('#skF_1'))).
% 5.27/2.27 tff(c_64, plain, (~b48_buttercup10515('#skF_9'))).
% 5.27/2.27 tff(c_108, plain, (b48_buttercup10521('#skF_20'))).
% 5.27/2.27 tff(c_72, plain, (b48_buttercup10222('#skF_10'))).
% 5.27/2.27 tff(c_28, plain, (~b48_buttercup10227('#skF_2'))).
% 5.27/2.27 tff(c_130, plain, (b48_buttercup10520('#skF_31'))).
% 5.27/2.27 tff(c_66, plain, (k04_buttercup10516('#skF_9'))).
% 5.27/2.27 tff(c_110, plain, (b48_buttercup10422('#skF_21'))).
% 5.27/2.27 tff(c_70, plain, (~k04_buttercup10225('#skF_10'))).
% 5.27/2.27 tff(c_90, plain, (~k04_buttercup10419('#skF_15'))).
% 5.27/2.27 tff(c_114, plain, (b48_buttercup10227('#skF_23'))).
% 5.27/2.27 tff(c_22, plain, (~b48_buttercup10422('#skF_1'))).
% 5.27/2.27 tff(c_116, plain, (b48_buttercup10229('#skF_24'))).
% 5.27/2.27 tff(c_118, plain, (b48_buttercup10417('#skF_25'))).
% 5.27/2.27 tff(c_132, plain, (b48_buttercup10519('#skF_35'))).
% 5.27/2.27 tff(c_134, plain, (k04_buttercup10225('#skF_35'))).
% 5.27/2.27 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.27/2.27
%------------------------------------------------------------------------------