%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS042+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 : n028.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.88s 1.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS042+1 : TPTP v9.0.0. Released v3.1.0.
% 0.13/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.33 % Computer : n028.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % 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:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 3.88/1.86
% 3.88/1.86 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.88/1.86
% 3.88/1.86 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.88/1.87 %$ rrxa > rrx4a > rrx4 > rrx3a > rrx3 > rrx2a > rrx2 > rrx1a > rrx1 > rrx > ra_Px1 > xsd_string > xsd_integer > cowlThing > cowlNothing > cc2 > cc1 > ca_Cx1xcomp > ca_Cx1 > ca_Ax2 > cSatisfiable > #nlpp > i2003_11_14_17_16_10980 > #skF_5 > #skF_2 > #skF_4 > #skF_1 > #skF_3
% 3.88/1.87
% 3.88/1.87 %Foreground sorts:
% 3.88/1.87
% 3.88/1.87
% 3.88/1.87 %Background operators:
% 3.88/1.87
% 3.88/1.87
% 3.88/1.87 %Foreground operators:
% 3.88/1.87 tff('#skF_5', type, '#skF_5': $i > $i).
% 3.88/1.87 tff('#skF_2', type, '#skF_2': $i > $i).
% 3.88/1.87 tff('#skF_4', type, '#skF_4': $i > $i).
% 3.88/1.87 tff(rrxa, type, rrxa: ($i * $i) > $o).
% 3.88/1.87 tff(cowlThing, type, cowlThing: $i > $o).
% 3.88/1.87 tff('#skF_1', type, '#skF_1': $i > $i).
% 3.88/1.87 tff(rrx2, type, rrx2: ($i * $i) > $o).
% 3.88/1.87 tff(ca_Ax2, type, ca_Ax2: $i > $o).
% 3.88/1.87 tff(rrx1a, type, rrx1a: ($i * $i) > $o).
% 3.88/1.87 tff(rrx, type, rrx: ($i * $i) > $o).
% 3.88/1.87 tff(cc1, type, cc1: $i > $o).
% 3.88/1.87 tff(ca_Cx1xcomp, type, ca_Cx1xcomp: $i > $o).
% 3.88/1.87 tff(rrx2a, type, rrx2a: ($i * $i) > $o).
% 3.88/1.87 tff(xsd_integer, type, xsd_integer: $i > $o).
% 3.88/1.87 tff(rrx4, type, rrx4: ($i * $i) > $o).
% 3.88/1.87 tff(rrx3a, type, rrx3a: ($i * $i) > $o).
% 3.88/1.87 tff(rrx4a, type, rrx4a: ($i * $i) > $o).
% 3.88/1.87 tff(rrx1, type, rrx1: ($i * $i) > $o).
% 3.88/1.87 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 3.88/1.87 tff(ra_Px1, type, ra_Px1: ($i * $i) > $o).
% 3.88/1.87 tff(rrx3, type, rrx3: ($i * $i) > $o).
% 3.88/1.87 tff(ca_Cx1, type, ca_Cx1: $i > $o).
% 3.88/1.87 tff(xsd_string, type, xsd_string: $i > $o).
% 3.88/1.87 tff('#skF_3', type, '#skF_3': $i > $i).
% 3.88/1.87 tff(cc2, type, cc2: $i > $o).
% 3.88/1.87 tff(i2003_11_14_17_16_10980, type, i2003_11_14_17_16_10980: $i).
% 3.88/1.87 tff(cowlNothing, type, cowlNothing: $i > $o).
% 3.88/1.87
% 3.88/1.87 %Saturated clause set:
% 3.88/1.87 tff(c_249, plain, (![X_101]: ('#skF_4'(X_101)='#skF_1'(X_101) | ~cSatisfiable(X_101) | ~ca_Cx1xcomp(X_101)))).
% 3.88/1.87 tff(c_224, plain, (![Y_188, X_101]: (Y_188='#skF_4'(X_101) | ~rrx3a(X_101, Y_188) | ~ca_Cx1xcomp(X_101)))).
% 3.88/1.87 tff(c_169, plain, (![X_89]: (ca_Ax2('#skF_2'(X_89)) | ~cc1('#skF_2'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.87 tff(c_225, plain, (![Y_188, X_89]: (Y_188='#skF_1'(X_89) | ~rrx3a(X_89, Y_188) | ~cSatisfiable(X_89)))).
% 3.88/1.87 tff(c_230, plain, (![Y_194, X_89]: (Y_194='#skF_2'(X_89) | ~rrx4a(X_89, Y_194) | ~cSatisfiable(X_89)))).
% 3.88/1.87 tff(c_74, plain, (![X_89, Y_95, Y_94]: (cSatisfiable(X_89) | ~cc2(Y_95) | ~rrx4a(X_89, Y_95) | ~ca_Cx1(X_89) | ~cc1(Y_94) | ~rrx3a(X_89, Y_94)))).
% 3.88/1.87 tff(c_112, plain, (![Z_120, Y_119, X_118]: (Z_120=Y_119 | ~rrx4(X_118, Z_120) | ~rrx4(X_118, Y_119)))).
% 3.88/1.87 tff(c_114, plain, (![Z_123, Y_122, X_121]: (Z_123=Y_122 | ~rrx4a(X_121, Z_123) | ~rrx4a(X_121, Y_122)))).
% 3.88/1.87 tff(c_106, plain, (![Z_111, Y_110, X_109]: (Z_111=Y_110 | ~rrx(X_109, Z_111) | ~rrx(X_109, Y_110)))).
% 3.88/1.87 tff(c_110, plain, (![Z_117, Y_116, X_115]: (Z_117=Y_116 | ~rrx3a(X_115, Z_117) | ~rrx3a(X_115, Y_116)))).
% 3.88/1.87 tff(c_108, plain, (![Z_114, Y_113, X_112]: (Z_114=Y_113 | ~rrx3(X_112, Z_114) | ~rrx3(X_112, Y_113)))).
% 3.88/1.87 tff(c_213, plain, (![X_89]: (ca_Cx1xcomp(X_89) | ~ca_Ax2('#skF_1'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.87 tff(c_175, plain, (![X_89]: (rrx2a(X_89, '#skF_2'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.87 tff(c_203, plain, (![X_175]: (rrx1a(X_175, '#skF_4'(X_175)) | ~ca_Cx1xcomp(X_175)))).
% 3.88/1.87 tff(c_184, plain, (![X_89]: (rrx1a(X_89, '#skF_1'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.87 tff(c_96, plain, (![X_101, Y_104]: (ca_Cx1xcomp(X_101) | ~ca_Ax2(Y_104) | ~rrx3a(X_101, Y_104)))).
% 3.88/1.87 tff(c_122, plain, (![X_128, Y_129]: (rrx(X_128, Y_129) | ~rrx3(X_128, Y_129)))).
% 3.88/1.87 tff(c_100, plain, (![X_101]: (rrx3a(X_101, '#skF_4'(X_101)) | ~ca_Cx1xcomp(X_101)))).
% 3.88/1.87 tff(c_192, plain, (![X_173]: (ca_Cx1(X_173) | ca_Cx1xcomp(X_173)))).
% 3.88/1.87 tff(c_104, plain, (![X_105]: (ca_Cx1xcomp(X_105) | ra_Px1(X_105, '#skF_5'(X_105))))).
% 3.88/1.87 tff(c_118, plain, (![X_124, Y_125]: (rrx1a(X_124, Y_125) | ~rrx3a(X_124, Y_125)))).
% 3.88/1.87 tff(c_132, plain, (![X_138, Y_139]: (rrx2(X_138, Y_139) | ~rrx4(X_138, Y_139)))).
% 3.88/1.87 tff(c_84, plain, (![X_89]: (rrx3a(X_89, '#skF_1'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.87 tff(c_126, plain, (![X_132, Y_133]: (rrxa(X_132, Y_133) | ~rrx3a(X_132, Y_133)))).
% 3.88/1.87 tff(c_128, plain, (![X_134, Y_135]: (rrx1(X_134, Y_135) | ~rrx3(X_134, Y_135)))).
% 3.88/1.87 tff(c_130, plain, (![X_136, Y_137]: (rrx2a(X_136, Y_137) | ~rrx4a(X_136, Y_137)))).
% 3.88/1.88 tff(c_86, plain, (![X_96]: (ca_Ax2(X_96) | ~cc1(X_96) | ~cc2(X_96)))).
% 3.88/1.88 tff(c_160, plain, (![X_159]: (~ca_Cx1xcomp(X_159) | ~ca_Cx1(X_159)))).
% 3.88/1.88 tff(c_92, plain, (![X_97]: (ra_Px1(X_97, '#skF_3'(X_97)) | ~ca_Cx1(X_97)))).
% 3.88/1.88 tff(c_124, plain, (![X_130, Y_131]: (rrxa(X_130, Y_131) | ~rrx4a(X_130, Y_131)))).
% 3.88/1.88 tff(c_120, plain, (![X_126, Y_127]: (rrx(X_126, Y_127) | ~rrx4(X_126, Y_127)))).
% 3.88/1.88 tff(c_78, plain, (![X_89]: (rrx4a(X_89, '#skF_2'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.88 tff(c_94, plain, (![X_97, Y0_100]: (ca_Cx1(X_97) | ~ra_Px1(X_97, Y0_100)))).
% 3.88/1.88 tff(c_102, plain, (![X_105, Y_108]: (~ra_Px1(X_105, Y_108) | ~ca_Cx1xcomp(X_105)))).
% 3.88/1.88 tff(c_98, plain, (![X_101]: (ca_Ax2('#skF_4'(X_101)) | ~ca_Cx1xcomp(X_101)))).
% 3.88/1.88 tff(c_82, plain, (![X_89]: (cc1('#skF_1'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.88 tff(c_76, plain, (![X_89]: (cc2('#skF_2'(X_89)) | ~cSatisfiable(X_89)))).
% 3.88/1.88 tff(c_80, plain, (![X_89]: (ca_Cx1(X_89) | ~cSatisfiable(X_89)))).
% 3.88/1.88 tff(c_72, plain, (![X_88]: (xsd_string(X_88) | xsd_integer(X_88)))).
% 3.88/1.88 tff(c_88, plain, (![X_96]: (cc1(X_96) | ~ca_Ax2(X_96)))).
% 3.88/1.88 tff(c_70, plain, (![X_88]: (~xsd_integer(X_88) | ~xsd_string(X_88)))).
% 3.88/1.88 tff(c_90, plain, (![X_96]: (cc2(X_96) | ~ca_Ax2(X_96)))).
% 3.88/1.88 tff(c_66, plain, (![X_87]: (cowlThing(X_87)))).
% 3.88/1.88 tff(c_68, plain, (![X_87]: (~cowlNothing(X_87)))).
% 3.88/1.88 tff(c_116, plain, (cSatisfiable(i2003_11_14_17_16_10980))).
% 3.88/1.88 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.88/1.88
%------------------------------------------------------------------------------