%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS044+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/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 : n023.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:12 PM UTC 2025
% Result : Satisfiable 3.69s 1.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.11 % Problem : KRS044+1 : TPTP v9.0.0. Released v3.1.0.
% 0.04/0.12 % 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.11/0.33 % Computer : n023.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Apr 8 02:56:24 EDT 2025
% 0.11/0.33 % CPUTime :
% 3.69/1.85
% 3.69/1.86 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.69/1.86
% 3.69/1.86 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.69/1.86 %$ rs > rinvS > rinvF1 > rinvF > rf1 > rf > ra_Px1 > xsd_string > xsd_integer > cpxcomp > cp > cowlThing > cowlNothing > cSatisfiable > #nlpp > i2003_11_14_17_16_1832 > #skF_2 > #skF_4 > #skF_1 > #skF_3
% 3.69/1.86
% 3.69/1.86 %Foreground sorts:
% 3.69/1.86
% 3.69/1.86
% 3.69/1.86 %Background operators:
% 3.69/1.86
% 3.69/1.86
% 3.69/1.86 %Foreground operators:
% 3.69/1.86 tff(rf, type, rf: ($i * $i) > $o).
% 3.69/1.86 tff('#skF_2', type, '#skF_2': $i > $i).
% 3.69/1.86 tff('#skF_4', type, '#skF_4': $i > $i).
% 3.69/1.86 tff(cowlThing, type, cowlThing: $i > $o).
% 3.69/1.86 tff(rinvS, type, rinvS: ($i * $i) > $o).
% 3.69/1.86 tff(rs, type, rs: ($i * $i) > $o).
% 3.69/1.86 tff('#skF_1', type, '#skF_1': $i > $i).
% 3.69/1.86 tff(rinvF, type, rinvF: ($i * $i) > $o).
% 3.69/1.86 tff(xsd_integer, type, xsd_integer: $i > $o).
% 3.69/1.86 tff(cpxcomp, type, cpxcomp: $i > $o).
% 3.69/1.86 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 3.69/1.86 tff(ra_Px1, type, ra_Px1: ($i * $i) > $o).
% 3.69/1.86 tff(i2003_11_14_17_16_1832, type, i2003_11_14_17_16_1832: $i).
% 3.69/1.86 tff(rf1, type, rf1: ($i * $i) > $o).
% 3.69/1.86 tff(xsd_string, type, xsd_string: $i > $o).
% 3.69/1.86 tff('#skF_3', type, '#skF_3': $i > $i).
% 3.69/1.86 tff(cp, type, cp: $i > $o).
% 3.69/1.86 tff(rinvF1, type, rinvF1: ($i * $i) > $o).
% 3.69/1.86 tff(cowlNothing, type, cowlNothing: $i > $o).
% 3.69/1.86
% 3.69/1.86 %Saturated clause set:
% 3.69/1.87 tff(c_185, plain, (![X_84, X_143, Y_85]: (X_84=X_143 | ~rinvS(X_143, Y_85) | ~rinvS(X_84, Y_85)))).
% 3.69/1.87 tff(c_168, plain, (![Y_129, X_59]: (Y_129='#skF_1'(X_59) | ~rf(X_59, Y_129) | ~cSatisfiable(X_59)))).
% 3.69/1.87 tff(c_177, plain, (![Y_137, X_59]: (Y_137='#skF_2'(X_59) | ~rf1(X_59, Y_137) | ~cSatisfiable(X_59)))).
% 3.69/1.87 tff(c_173, plain, (![Y_134, X_84, Y_85]: (Y_134=X_84 | ~rs(Y_85, Y_134) | ~rinvS(X_84, Y_85)))).
% 3.69/1.87 tff(c_52, plain, (![X_59, Y_65, Y_64]: (cSatisfiable(X_59) | ~cpxcomp(Y_65) | ~rf1(X_59, Y_65) | ~cp(Y_64) | ~rf(X_59, Y_64)))).
% 3.69/1.87 tff(c_72, plain, (![Z_79, Y_78, X_77]: (Z_79=Y_78 | ~rf1(X_77, Z_79) | ~rf1(X_77, Y_78)))).
% 3.69/1.87 tff(c_86, plain, (![Z_88, Y_87, X_86]: (Z_88=Y_87 | ~rs(X_86, Z_88) | ~rs(X_86, Y_87)))).
% 3.69/1.87 tff(c_158, plain, (![Y_85, X_84]: (rf1(Y_85, X_84) | ~rinvS(X_84, Y_85)))).
% 3.69/1.87 tff(c_70, plain, (![Z_76, Y_75, X_74]: (Z_76=Y_75 | ~rf(X_74, Z_76) | ~rf(X_74, Y_75)))).
% 3.69/1.87 tff(c_146, plain, (![Y_115, X_116]: (rf(Y_115, X_116) | ~rinvS(X_116, Y_115)))).
% 3.69/1.87 tff(c_80, plain, (![X_82, Y_83]: (rinvF1(X_82, Y_83) | ~rf1(Y_83, X_82)))).
% 3.69/1.87 tff(c_92, plain, (![X_91, Y_92]: (rf1(X_91, Y_92) | ~rs(X_91, Y_92)))).
% 3.69/1.87 tff(c_76, plain, (![X_80, Y_81]: (rinvF(X_80, Y_81) | ~rf(Y_81, X_80)))).
% 3.69/1.87 tff(c_60, plain, (![X_59]: (rf(X_59, '#skF_1'(X_59)) | ~cSatisfiable(X_59)))).
% 3.69/1.87 tff(c_74, plain, (![Y_81, X_80]: (rf(Y_81, X_80) | ~rinvF(X_80, Y_81)))).
% 3.69/1.87 tff(c_82, plain, (![Y_85, X_84]: (rs(Y_85, X_84) | ~rinvS(X_84, Y_85)))).
% 3.69/1.87 tff(c_136, plain, (![X_59]: (~cp('#skF_2'(X_59)) | ~cSatisfiable(X_59)))).
% 3.69/1.87 tff(c_126, plain, (![X_112]: (~cp(X_112) | ~cpxcomp(X_112)))).
% 3.69/1.87 tff(c_66, plain, (![X_70]: (ra_Px1(X_70, '#skF_4'(X_70)) | ~cpxcomp(X_70)))).
% 3.69/1.87 tff(c_117, plain, (![X_110]: (cpxcomp(X_110) | cp(X_110)))).
% 3.69/1.87 tff(c_64, plain, (![X_66]: (cp(X_66) | ra_Px1(X_66, '#skF_3'(X_66))))).
% 3.69/1.87 tff(c_78, plain, (![Y_83, X_82]: (rf1(Y_83, X_82) | ~rinvF1(X_82, Y_83)))).
% 3.69/1.87 tff(c_84, plain, (![X_84, Y_85]: (rinvS(X_84, Y_85) | ~rs(Y_85, X_84)))).
% 3.69/1.87 tff(c_90, plain, (![X_89, Y_90]: (rf(X_89, Y_90) | ~rs(X_89, Y_90)))).
% 3.69/1.87 tff(c_56, plain, (![X_59]: (rf1(X_59, '#skF_2'(X_59)) | ~cSatisfiable(X_59)))).
% 3.69/1.87 tff(c_54, plain, (![X_59]: (cpxcomp('#skF_2'(X_59)) | ~cSatisfiable(X_59)))).
% 3.69/1.87 tff(c_62, plain, (![X_66, Y_69]: (~ra_Px1(X_66, Y_69) | ~cp(X_66)))).
% 3.69/1.87 tff(c_68, plain, (![X_70, Y0_73]: (cpxcomp(X_70) | ~ra_Px1(X_70, Y0_73)))).
% 3.69/1.87 tff(c_58, plain, (![X_59]: (cp('#skF_1'(X_59)) | ~cSatisfiable(X_59)))).
% 3.69/1.87 tff(c_48, plain, (![X_58]: (~xsd_integer(X_58) | ~xsd_string(X_58)))).
% 3.69/1.87 tff(c_50, plain, (![X_58]: (xsd_string(X_58) | xsd_integer(X_58)))).
% 3.69/1.87 tff(c_44, plain, (![X_57]: (cowlThing(X_57)))).
% 3.69/1.87 tff(c_46, plain, (![X_57]: (~cowlNothing(X_57)))).
% 3.69/1.87 tff(c_88, plain, (cSatisfiable(i2003_11_14_17_16_1832))).
% 3.69/1.87 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.69/1.87
%------------------------------------------------------------------------------