%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS050+1 : TPTP v9.0.0. Released v3.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 : n026.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 07:07:13 PM UTC 2025
% Result : Satisfiable 3.65s 1.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS050+1 : TPTP v9.0.0. Released v3.1.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 02:56:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 3.65/1.85
% 3.65/1.85 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.65/1.85
% 3.65/1.85 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.65/1.86 %$ rr1 > rr > rinvR > ra_Px1 > xsd_string > xsd_integer > cpxcomp > cp > cowlThing > cowlNothing > ca_Vx5 > ca_Vx4 > ca_Vx3 > ca_Vx2 > cSatisfiable > #nlpp > i2003_11_14_17_16_39209 > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_1 > #skF_8 > #skF_3 > #skF_6
% 3.65/1.86
% 3.65/1.86 %Foreground sorts:
% 3.65/1.86
% 3.65/1.86
% 3.65/1.86 %Background operators:
% 3.65/1.86
% 3.65/1.86
% 3.65/1.86 %Foreground operators:
% 3.65/1.86 tff('#skF_7', type, '#skF_7': $i > $i).
% 3.65/1.86 tff('#skF_5', type, '#skF_5': $i > $i).
% 3.65/1.86 tff(rinvR, type, rinvR: ($i * $i) > $o).
% 3.65/1.86 tff(rr, type, rr: ($i * $i) > $o).
% 3.65/1.86 tff('#skF_2', type, '#skF_2': $i > $i).
% 3.65/1.86 tff('#skF_4', type, '#skF_4': $i > $i).
% 3.65/1.86 tff(cowlThing, type, cowlThing: $i > $o).
% 3.65/1.86 tff('#skF_1', type, '#skF_1': $i > $i).
% 3.65/1.86 tff('#skF_8', type, '#skF_8': $i > $i).
% 3.65/1.86 tff(i2003_11_14_17_16_39209, type, i2003_11_14_17_16_39209: $i).
% 3.65/1.86 tff(ca_Vx2, type, ca_Vx2: $i > $o).
% 3.65/1.86 tff(xsd_integer, type, xsd_integer: $i > $o).
% 3.65/1.86 tff(ca_Vx4, type, ca_Vx4: $i > $o).
% 3.65/1.86 tff(cpxcomp, type, cpxcomp: $i > $o).
% 3.65/1.86 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 3.65/1.86 tff(rr1, type, rr1: ($i * $i) > $o).
% 3.65/1.86 tff(ra_Px1, type, ra_Px1: ($i * $i) > $o).
% 3.65/1.86 tff(ca_Vx3, type, ca_Vx3: $i > $o).
% 3.65/1.86 tff(xsd_string, type, xsd_string: $i > $o).
% 3.65/1.86 tff('#skF_3', type, '#skF_3': $i > $i).
% 3.65/1.86 tff(ca_Vx5, type, ca_Vx5: $i > $o).
% 3.65/1.86 tff(cp, type, cp: $i > $o).
% 3.65/1.86 tff('#skF_6', type, '#skF_6': $i > $i).
% 3.65/1.86 tff(cowlNothing, type, cowlNothing: $i > $o).
% 3.65/1.86
% 3.65/1.86 %Saturated clause set:
% 3.65/1.86 tff(c_238, plain, (![X_26, X_93]: (cSatisfiable('#skF_7'(X_26)) | ~ca_Vx5(X_26) | ~ca_Vx4(X_93) | ~rinvR(X_93, '#skF_7'(X_26)) | ca_Vx4(X_26)))).
% 3.65/1.86 tff(c_223, plain, (![Y_35, X_89, X_34]: (cSatisfiable(Y_35) | ~ca_Vx5(X_89) | ~ca_Vx4(X_34) | ~rinvR(X_89, Y_35) | ~rinvR(X_34, Y_35)))).
% 3.65/1.86 tff(c_190, plain, (![Y_35, X_34, Y_80]: (cSatisfiable(Y_35) | ~ca_Vx5(X_34) | ~ca_Vx4(Y_80) | ~rr(Y_35, Y_80) | ~rinvR(X_34, Y_35)))).
% 3.65/1.86 tff(c_214, plain, (![X_26]: (ca_Vx4(X_26) | ~cSatisfiable('#skF_7'(X_26))))).
% 3.65/1.86 tff(c_209, plain, (![X_3]: (ca_Vx2(X_3) | ~cSatisfiable(X_3)))).
% 3.65/1.86 tff(c_203, plain, (![X_30]: (ca_Vx5(X_30) | ~cSatisfiable('#skF_8'(X_30))))).
% 3.65/1.86 tff(c_198, plain, (![X_3]: (ca_Vx3(X_3) | ~cSatisfiable(X_3)))).
% 3.65/1.86 tff(c_10, plain, (![X_3, Y_9, Y_8]: (cSatisfiable(X_3) | ~ca_Vx5(Y_9) | ~rr(X_3, Y_9) | ~ca_Vx4(Y_8) | ~rr(X_3, Y_8)))).
% 3.65/1.87 tff(c_157, plain, (![X_30]: (ca_Vx2('#skF_8'(X_30)) | ~ca_Vx4(X_30) | ca_Vx5(X_30)))).
% 3.65/1.87 tff(c_175, plain, (![X_26]: (ca_Vx3('#skF_7'(X_26)) | ~ca_Vx5(X_26) | ca_Vx4(X_26)))).
% 3.65/1.87 tff(c_140, plain, (![X_18]: (cpxcomp('#skF_5'(X_18)) | ~ca_Vx3(X_18) | ca_Vx2(X_18)))).
% 3.65/1.87 tff(c_46, plain, (![Y_33, X_30]: (ca_Vx3(Y_33) | ~rinvR(X_30, Y_33) | ~ca_Vx5(X_30)))).
% 3.65/1.87 tff(c_40, plain, (![Y_29, X_26]: (ca_Vx2(Y_29) | ~rinvR(X_26, Y_29) | ~ca_Vx4(X_26)))).
% 3.65/1.87 tff(c_34, plain, (![Y_25, X_22]: (cpxcomp(Y_25) | ~rr1(X_22, Y_25) | ~ca_Vx3(X_22)))).
% 3.65/1.87 tff(c_28, plain, (![Y_21, X_18]: (cp(Y_21) | ~rr1(X_18, Y_21) | ~ca_Vx2(X_18)))).
% 3.65/1.87 tff(c_95, plain, (![X_57]: (rinvR('#skF_1'(X_57), X_57) | ~cSatisfiable(X_57)))).
% 3.65/1.87 tff(c_81, plain, (![X_3]: (rinvR('#skF_2'(X_3), X_3) | ~cSatisfiable(X_3)))).
% 3.65/1.87 tff(c_52, plain, (![Y_35, X_34]: (rr(Y_35, X_34) | ~rinvR(X_34, Y_35)))).
% 3.65/1.87 tff(c_110, plain, (![X_61]: (~cp(X_61) | ~cpxcomp(X_61)))).
% 3.65/1.87 tff(c_24, plain, (![X_14]: (ra_Px1(X_14, '#skF_4'(X_14)) | ~cpxcomp(X_14)))).
% 3.65/1.87 tff(c_50, plain, (![X_30]: (rinvR(X_30, '#skF_8'(X_30)) | ca_Vx5(X_30)))).
% 3.65/1.87 tff(c_100, plain, (![X_22]: (ca_Vx3(X_22) | cp('#skF_6'(X_22))))).
% 3.65/1.87 tff(c_90, plain, (![X_56]: (cpxcomp(X_56) | cp(X_56)))).
% 3.65/1.87 tff(c_18, plain, (![X_3]: (rr(X_3, '#skF_1'(X_3)) | ~cSatisfiable(X_3)))).
% 3.65/1.87 tff(c_22, plain, (![X_10]: (cp(X_10) | ra_Px1(X_10, '#skF_3'(X_10))))).
% 3.65/1.87 tff(c_54, plain, (![X_34, Y_35]: (rinvR(X_34, Y_35) | ~rr(Y_35, X_34)))).
% 3.65/1.87 tff(c_32, plain, (![X_18]: (rr1(X_18, '#skF_5'(X_18)) | ca_Vx2(X_18)))).
% 3.65/1.87 tff(c_14, plain, (![X_3]: (rr(X_3, '#skF_2'(X_3)) | ~cSatisfiable(X_3)))).
% 3.65/1.87 tff(c_38, plain, (![X_22]: (rr1(X_22, '#skF_6'(X_22)) | ca_Vx3(X_22)))).
% 3.65/1.87 tff(c_44, plain, (![X_26]: (rinvR(X_26, '#skF_7'(X_26)) | ca_Vx4(X_26)))).
% 3.65/1.87 tff(c_20, plain, (![X_10, Y_13]: (~ra_Px1(X_10, Y_13) | ~cp(X_10)))).
% 3.65/1.87 tff(c_26, plain, (![X_14, Y0_17]: (cpxcomp(X_14) | ~ra_Px1(X_14, Y0_17)))).
% 3.65/1.87 tff(c_42, plain, (![X_26]: (~ca_Vx2('#skF_7'(X_26)) | ca_Vx4(X_26)))).
% 3.65/1.87 tff(c_36, plain, (![X_22]: (~cpxcomp('#skF_6'(X_22)) | ca_Vx3(X_22)))).
% 3.65/1.87 tff(c_16, plain, (![X_3]: (ca_Vx4('#skF_1'(X_3)) | ~cSatisfiable(X_3)))).
% 3.65/1.87 tff(c_12, plain, (![X_3]: (ca_Vx5('#skF_2'(X_3)) | ~cSatisfiable(X_3)))).
% 3.65/1.87 tff(c_30, plain, (![X_18]: (~cp('#skF_5'(X_18)) | ca_Vx2(X_18)))).
% 3.65/1.87 tff(c_48, plain, (![X_30]: (~ca_Vx3('#skF_8'(X_30)) | ca_Vx5(X_30)))).
% 3.65/1.87 tff(c_6, plain, (![X_2]: (~xsd_integer(X_2) | ~xsd_string(X_2)))).
% 3.65/1.87 tff(c_8, plain, (![X_2]: (xsd_string(X_2) | xsd_integer(X_2)))).
% 3.65/1.87 tff(c_2, plain, (![X_1]: (cowlThing(X_1)))).
% 3.65/1.87 tff(c_4, plain, (![X_1]: (~cowlNothing(X_1)))).
% 3.65/1.87 tff(c_56, plain, (cSatisfiable(i2003_11_14_17_16_39209))).
% 3.65/1.87 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.65/1.87
%------------------------------------------------------------------------------