%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS045+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 : n009.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.48s 1.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS045+1 : TPTP v9.0.0. Released v3.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.13/0.34 % Computer : n009.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:55:57 EDT 2025
% 0.13/0.35 % CPUTime :
% 3.48/1.69
% 3.48/1.69 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.48/1.70
% 3.48/1.70 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.48/1.70 %$ rr > rf2 > rf1 > ra_Px1 > xsd_string > xsd_integer > cp2xcomp > cp2 > cp1 > cowlThing > cowlNothing > cSatisfiable > #nlpp > i2003_11_14_17_16_21280 > #skF_2 > #skF_4 > #skF_1 > #skF_3
% 3.48/1.70
% 3.48/1.70 %Foreground sorts:
% 3.48/1.70
% 3.48/1.70
% 3.48/1.70 %Background operators:
% 3.48/1.70
% 3.48/1.70
% 3.48/1.70 %Foreground operators:
% 3.48/1.70 tff(i2003_11_14_17_16_21280, type, i2003_11_14_17_16_21280: $i).
% 3.48/1.70 tff(rr, type, rr: ($i * $i) > $o).
% 3.48/1.70 tff('#skF_2', type, '#skF_2': $i > $i).
% 3.48/1.70 tff('#skF_4', type, '#skF_4': $i > $i).
% 3.48/1.70 tff(cowlThing, type, cowlThing: $i > $o).
% 3.48/1.70 tff('#skF_1', type, '#skF_1': $i > $i).
% 3.48/1.70 tff(xsd_integer, type, xsd_integer: $i > $o).
% 3.48/1.70 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 3.48/1.70 tff(ra_Px1, type, ra_Px1: ($i * $i) > $o).
% 3.48/1.70 tff(rf1, type, rf1: ($i * $i) > $o).
% 3.48/1.70 tff(xsd_string, type, xsd_string: $i > $o).
% 3.48/1.70 tff('#skF_3', type, '#skF_3': $i > $i).
% 3.48/1.70 tff(cp2xcomp, type, cp2xcomp: $i > $o).
% 3.48/1.70 tff(rf2, type, rf2: ($i * $i) > $o).
% 3.48/1.70 tff(cp2, type, cp2: $i > $o).
% 3.48/1.70 tff(cowlNothing, type, cowlNothing: $i > $o).
% 3.48/1.70 tff(cp1, type, cp1: $i > $o).
% 3.48/1.70
% 3.48/1.70 %Saturated clause set:
% 3.48/1.70 tff(c_42, plain, (![X_43, Y_49, Y_48]: (cSatisfiable(X_43) | ~cp1(Y_49) | ~rf1(X_43, Y_49) | ~cp2(Y_48) | ~rf2(X_43, Y_48)))).
% 3.48/1.70 tff(c_133, plain, (![Y0_100, X_43]: (Y0_100='#skF_2'(X_43) | ~rf1(X_43, Y0_100) | ~cSatisfiable(X_43)))).
% 3.48/1.70 tff(c_129, plain, (![Y0_97, X_43]: (Y0_97='#skF_1'(X_43) | ~rf2(X_43, Y0_97) | ~cSatisfiable(X_43)))).
% 3.48/1.70 tff(c_72, plain, (![Y1_63, Y0_62, X_59]: (Y1_63=Y0_62 | ~rf1(X_59, Y1_63) | ~rf1(X_59, Y0_62)))).
% 3.48/1.71 tff(c_74, plain, (![Y1_68, Y0_67, X_64]: (Y1_68=Y0_67 | ~rf2(X_64, Y1_68) | ~rf2(X_64, Y0_67)))).
% 3.48/1.71 tff(c_68, plain, (![X_69, Y_70]: (rf1(X_69, Y_70) | ~rr(X_69, Y_70)))).
% 3.48/1.71 tff(c_123, plain, (![X_43]: (~cp1('#skF_1'(X_43)) | ~cSatisfiable(X_43)))).
% 3.48/1.71 tff(c_118, plain, (![X_50]: (~cp2(X_50) | ~cp1(X_50)))).
% 3.48/1.71 tff(c_108, plain, (![X_90]: (~cp2(X_90) | ~cp2xcomp(X_90)))).
% 3.48/1.71 tff(c_58, plain, (![X_55]: (ra_Px1(X_55, '#skF_4'(X_55)) | ~cp2xcomp(X_55)))).
% 3.48/1.71 tff(c_50, plain, (![X_43]: (rf2(X_43, '#skF_1'(X_43)) | ~cSatisfiable(X_43)))).
% 3.48/1.71 tff(c_70, plain, (![X_71, Y_72]: (rf2(X_71, Y_72) | ~rr(X_71, Y_72)))).
% 3.48/1.71 tff(c_97, plain, (![X_85]: (cp2xcomp(X_85) | cp2(X_85)))).
% 3.48/1.71 tff(c_56, plain, (![X_51]: (cp2(X_51) | ra_Px1(X_51, '#skF_3'(X_51))))).
% 3.48/1.71 tff(c_46, plain, (![X_43]: (rf1(X_43, '#skF_2'(X_43)) | ~cSatisfiable(X_43)))).
% 3.48/1.71 tff(c_54, plain, (![X_51, Y_54]: (~ra_Px1(X_51, Y_54) | ~cp2(X_51)))).
% 3.48/1.71 tff(c_60, plain, (![X_55, Y0_58]: (cp2xcomp(X_55) | ~ra_Px1(X_55, Y0_58)))).
% 3.48/1.71 tff(c_48, plain, (![X_43]: (cp2('#skF_1'(X_43)) | ~cSatisfiable(X_43)))).
% 3.48/1.71 tff(c_44, plain, (![X_43]: (cp1('#skF_2'(X_43)) | ~cSatisfiable(X_43)))).
% 3.48/1.71 tff(c_40, plain, (![X_42]: (xsd_string(X_42) | xsd_integer(X_42)))).
% 3.48/1.71 tff(c_38, plain, (![X_42]: (~xsd_integer(X_42) | ~xsd_string(X_42)))).
% 3.48/1.71 tff(c_52, plain, (![X_50]: (cp2xcomp(X_50) | ~cp1(X_50)))).
% 3.48/1.71 tff(c_34, plain, (![X_41]: (cowlThing(X_41)))).
% 3.48/1.71 tff(c_36, plain, (![X_41]: (~cowlNothing(X_41)))).
% 3.48/1.71 tff(c_66, plain, (cSatisfiable(i2003_11_14_17_16_21280))).
% 3.48/1.71 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.48/1.71
%------------------------------------------------------------------------------