%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS043+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 : n010.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 5.16s 2.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS043+1 : TPTP v9.0.0. Released v3.1.0.
% 0.03/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 : n010.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:17 EDT 2025
% 0.13/0.34 % CPUTime :
% 5.16/2.13
% 5.16/2.14 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.16/2.14
% 5.16/2.14 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.30/2.14 %$ rr > rinvR > ra_Px7 > ra_Px6 > ra_Px5 > ra_Px4 > ra_Px3 > ra_Px2 > ra_Px1 > xsd_string > xsd_integer > cp5xcomp > cp5 > cp4xcomp > cp4 > cp3xcomp > cp3 > cp2xcomp > cp2 > cp1 > cowlThing > cowlNothing > ca_Cx3xcomp > ca_Cx3 > ca_Cx2xcomp > ca_Cx2 > ca_Cx1xcomp > ca_Cx1 > ca_Ax14 > cSatisfiable > #nlpp > i2003_11_14_17_16_14536 > #skF_9 > #skF_7 > #skF_5 > #skF_16 > #skF_2 > #skF_4 > #skF_18 > #skF_1 > #skF_8 > #skF_15 > #skF_10 > #skF_13 > #skF_17 > #skF_3 > #skF_11 > #skF_14 > #skF_12 > #skF_6
% 5.30/2.14
% 5.30/2.14 %Foreground sorts:
% 5.30/2.14
% 5.30/2.14
% 5.30/2.14 %Background operators:
% 5.30/2.14
% 5.30/2.14
% 5.30/2.14 %Foreground operators:
% 5.30/2.14 tff(cp4xcomp, type, cp4xcomp: $i > $o).
% 5.30/2.14 tff('#skF_9', type, '#skF_9': $i > $i).
% 5.30/2.14 tff('#skF_7', type, '#skF_7': $i > $i).
% 5.30/2.14 tff('#skF_5', type, '#skF_5': $i > $i).
% 5.30/2.14 tff(ca_Cx2xcomp, type, ca_Cx2xcomp: $i > $o).
% 5.30/2.14 tff(ra_Px5, type, ra_Px5: ($i * $i) > $o).
% 5.30/2.14 tff(rinvR, type, rinvR: ($i * $i) > $o).
% 5.30/2.14 tff(cp5, type, cp5: $i > $o).
% 5.30/2.14 tff(rr, type, rr: ($i * $i) > $o).
% 5.30/2.14 tff('#skF_16', type, '#skF_16': $i > $i).
% 5.30/2.14 tff('#skF_2', type, '#skF_2': $i > $i).
% 5.30/2.14 tff('#skF_4', type, '#skF_4': $i > $i).
% 5.30/2.14 tff('#skF_18', type, '#skF_18': $i > $i).
% 5.30/2.14 tff(ra_Px2, type, ra_Px2: ($i * $i) > $o).
% 5.30/2.14 tff(cowlThing, type, cowlThing: $i > $o).
% 5.30/2.14 tff('#skF_1', type, '#skF_1': $i > $i).
% 5.30/2.14 tff(ca_Cx3, type, ca_Cx3: $i > $o).
% 5.30/2.14 tff(ra_Px6, type, ra_Px6: ($i * $i) > $o).
% 5.30/2.14 tff('#skF_8', type, '#skF_8': $i > $i).
% 5.30/2.14 tff(cp4, type, cp4: $i > $o).
% 5.30/2.14 tff(ca_Cx1xcomp, type, ca_Cx1xcomp: $i > $o).
% 5.30/2.14 tff(cp3xcomp, type, cp3xcomp: $i > $o).
% 5.30/2.14 tff('#skF_15', type, '#skF_15': $i > $i).
% 5.30/2.14 tff(xsd_integer, type, xsd_integer: $i > $o).
% 5.30/2.14 tff(ca_Cx3xcomp, type, ca_Cx3xcomp: $i > $o).
% 5.30/2.14 tff(cp5xcomp, type, cp5xcomp: $i > $o).
% 5.30/2.14 tff('#skF_10', type, '#skF_10': $i > $i).
% 5.30/2.14 tff(ra_Px7, type, ra_Px7: ($i * $i) > $o).
% 5.30/2.14 tff(ca_Cx2, type, ca_Cx2: $i > $o).
% 5.30/2.14 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 5.30/2.14 tff(ra_Px1, type, ra_Px1: ($i * $i) > $o).
% 5.30/2.14 tff(ca_Ax14, type, ca_Ax14: $i > $o).
% 5.30/2.14 tff(cp3, type, cp3: $i > $o).
% 5.30/2.14 tff('#skF_13', type, '#skF_13': $i > $i).
% 5.30/2.14 tff(ca_Cx1, type, ca_Cx1: $i > $o).
% 5.30/2.14 tff(xsd_string, type, xsd_string: $i > $o).
% 5.30/2.14 tff('#skF_17', type, '#skF_17': $i > $i).
% 5.30/2.14 tff('#skF_3', type, '#skF_3': $i > $i).
% 5.30/2.14 tff('#skF_11', type, '#skF_11': $i > $i).
% 5.30/2.14 tff('#skF_14', type, '#skF_14': $i > $i).
% 5.30/2.14 tff(cp2xcomp, type, cp2xcomp: $i > $o).
% 5.30/2.14 tff('#skF_12', type, '#skF_12': $i > $i).
% 5.30/2.14 tff(ra_Px3, type, ra_Px3: ($i * $i) > $o).
% 5.30/2.14 tff(cp2, type, cp2: $i > $o).
% 5.30/2.14 tff('#skF_6', type, '#skF_6': $i > $i).
% 5.30/2.14 tff(cowlNothing, type, cowlNothing: $i > $o).
% 5.30/2.14 tff(i2003_11_14_17_16_14536, type, i2003_11_14_17_16_14536: $i).
% 5.30/2.14 tff(cp1, type, cp1: $i > $o).
% 5.30/2.14 tff(ra_Px4, type, ra_Px4: ($i * $i) > $o).
% 5.30/2.14
% 5.30/2.14 %Saturated clause set:
% 5.30/2.15 tff(c_804, plain, (![Y0_147, X_308]: (Y0_147=X_308 | ~rr('#skF_1'(X_308), Y0_147) | ~ca_Ax14('#skF_1'(X_308)) | ~cSatisfiable(X_308)))).
% 5.30/2.15 tff(c_937, plain, (![X_99, X_323]: (X_99=X_323 | ~ca_Ax14('#skF_1'(X_99)) | ~rinvR(X_323, '#skF_1'(X_99)) | ~cSatisfiable(X_99)))).
% 5.30/2.15 tff(c_718, plain, (![Y_177, X_176]: (rr(Y_177, '#skF_11'(Y_177)) | ca_Ax14(Y_177) | ~cp1(X_176) | ~rinvR(X_176, Y_177)))).
% 5.30/2.15 tff(c_766, plain, (![Y_177, X_176]: ('#skF_10'(Y_177)!='#skF_11'(Y_177) | ca_Ax14(Y_177) | ~cp1(X_176) | ~rinvR(X_176, Y_177)))).
% 5.30/2.15 tff(c_862, plain, (![X_314, X_176, Y_177]: (X_314=X_176 | ~ca_Ax14(Y_177) | ~rinvR(X_314, Y_177) | ~rinvR(X_176, Y_177)))).
% 5.30/2.15 tff(c_684, plain, (![Y_177, X_176]: (rr(Y_177, '#skF_10'(Y_177)) | ca_Ax14(Y_177) | ~cp1(X_176) | ~rinvR(X_176, Y_177)))).
% 5.30/2.15 tff(c_593, plain, (![X_249]: (ca_Cx1(X_249) | ~cp4xcomp(X_249) | ~cp3xcomp(X_249) | ~cp2xcomp(X_249) | cp5(X_249)))).
% 5.30/2.15 tff(c_891, plain, (![X_257]: (ca_Cx1(X_257) | ~cp2xcomp(X_257) | ~ca_Cx3(X_257) | cp3(X_257)))).
% 5.30/2.15 tff(c_880, plain, (![X_167]: (ca_Cx1(X_167) | ~cp3xcomp(X_167) | ~cp2xcomp(X_167) | ~ca_Cx3(X_167)))).
% 5.30/2.15 tff(c_634, plain, (![Y0_286, X_176, Y_177]: (Y0_286=X_176 | ~rr(Y_177, Y0_286) | ~ca_Ax14(Y_177) | ~rinvR(X_176, Y_177)))).
% 5.30/2.15 tff(c_843, plain, (![X_243]: (ca_Cx1(X_243) | ~ca_Cx2(X_243) | cp2(X_243)))).
% 5.30/2.15 tff(c_834, plain, (![X_162]: (ca_Cx1(X_162) | ~cp2xcomp(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.15 tff(c_747, plain, (![X_301]: (rr('#skF_1'(X_301), X_301) | ~ca_Ax14('#skF_1'(X_301)) | ~cSatisfiable(X_301)))).
% 5.30/2.15 tff(c_778, plain, (![X_99]: (cp1(X_99) | ~cSatisfiable(X_99)))).
% 5.30/2.15 tff(c_772, plain, (![X_99]: (ca_Cx1(X_99) | ~cSatisfiable(X_99)))).
% 5.30/2.15 tff(c_140, plain, (![X_139, Y_146]: ('#skF_10'(X_139)!='#skF_11'(X_139) | ca_Ax14(X_139) | ~cp1(Y_146) | ~rr(X_139, Y_146)))).
% 5.30/2.15 tff(c_734, plain, (![X_99]: ('#skF_12'('#skF_1'(X_99))=X_99 | ~cSatisfiable(X_99)))).
% 5.30/2.15 tff(c_693, plain, (![X_176, Y_177]: (X_176='#skF_12'(Y_177) | ~ca_Ax14(Y_177) | ~rinvR(X_176, Y_177)))).
% 5.30/2.15 tff(c_142, plain, (![X_139, Y_146]: (rr(X_139, '#skF_11'(X_139)) | ca_Ax14(X_139) | ~cp1(Y_146) | ~rr(X_139, Y_146)))).
% 5.30/2.15 tff(c_555, plain, (![X_249]: (ca_Cx2(X_249) | ~cp4xcomp(X_249) | ~cp3xcomp(X_249) | cp5(X_249)))).
% 5.30/2.15 tff(c_635, plain, (![Y0_286, X_139]: (Y0_286='#skF_12'(X_139) | ~rr(X_139, Y0_286) | ~ca_Ax14(X_139)))).
% 5.30/2.15 tff(c_144, plain, (![X_139, Y_146]: (rr(X_139, '#skF_10'(X_139)) | ca_Ax14(X_139) | ~cp1(Y_146) | ~rr(X_139, Y_146)))).
% 5.30/2.15 tff(c_663, plain, (![X_257]: (ca_Cx2(X_257) | ~ca_Cx3(X_257) | cp3(X_257)))).
% 5.30/2.15 tff(c_652, plain, (![X_167]: (ca_Cx2(X_167) | ~cp3xcomp(X_167) | ~ca_Cx3(X_167)))).
% 5.30/2.15 tff(c_134, plain, (![Y1_148, Y0_147, X_139]: (Y1_148=Y0_147 | ~rr(X_139, Y1_148) | ~rr(X_139, Y0_147) | ~ca_Ax14(X_139)))).
% 5.30/2.15 tff(c_627, plain, (![X_153]: (ca_Cx2(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.15 tff(c_150, plain, (![X_153]: (ca_Cx1(X_153) | ~cp4xcomp(X_153) | ~cp3xcomp(X_153) | ~cp2xcomp(X_153) | ~cp5xcomp(X_153)))).
% 5.30/2.15 tff(c_434, plain, (![X_249]: (ca_Cx3(X_249) | ~cp4xcomp(X_249) | cp5(X_249)))).
% 5.30/2.15 tff(c_168, plain, (![X_162]: (ca_Cx2(X_162) | ~cp4xcomp(X_162) | ~cp3xcomp(X_162) | ~cp5xcomp(X_162)))).
% 5.30/2.15 tff(c_536, plain, (![X_162]: (ca_Cx3(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.15 tff(c_517, plain, (![X_153]: (ca_Cx3(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.15 tff(c_500, plain, (![X_251]: (cSatisfiable('#skF_12'(X_251)) | ~ca_Ax14(X_251)))).
% 5.30/2.15 tff(c_88, plain, (![X_99, Y_102]: (cSatisfiable(X_99) | ~ca_Ax14(Y_102) | ~rinvR(X_99, Y_102)))).
% 5.30/2.15 tff(c_369, plain, (![X_251]: (rinvR('#skF_12'(X_251), X_251) | ~ca_Ax14(X_251)))).
% 5.30/2.15 tff(c_481, plain, (![X_153]: (~cp5(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.15 tff(c_480, plain, (![X_162]: (~cp5(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.15 tff(c_194, plain, (![Y_177, X_176]: (rr(Y_177, X_176) | ~rinvR(X_176, Y_177)))).
% 5.30/2.16 tff(c_482, plain, (![X_167]: (~cp5(X_167) | ~ca_Cx3(X_167)))).
% 5.30/2.16 tff(c_479, plain, (![X_126]: (~cp5(X_126) | ~cp4(X_126)))).
% 5.30/2.16 tff(c_460, plain, (![X_263]: (~cp5(X_263) | ~cp5xcomp(X_263)))).
% 5.30/2.16 tff(c_130, plain, (![X_135]: (ra_Px4(X_135, '#skF_9'(X_135)) | ~cp5xcomp(X_135)))).
% 5.30/2.16 tff(c_447, plain, (![X_261]: (ca_Cx3xcomp(X_261) | ca_Cx3(X_261)))).
% 5.30/2.16 tff(c_188, plain, (![X_168]: (ca_Cx3(X_168) | ra_Px3(X_168, '#skF_17'(X_168))))).
% 5.30/2.16 tff(c_180, plain, (![X_167]: (ca_Cx3(X_167) | ~cp4xcomp(X_167) | ~cp5xcomp(X_167)))).
% 5.30/2.16 tff(c_402, plain, (![X_153]: (~cp2(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.16 tff(c_411, plain, (![X_257]: (cp3(X_257) | cp3xcomp(X_257)))).
% 5.30/2.16 tff(c_114, plain, (![X_118]: (cp3xcomp(X_118) | ra_Px6(X_118, '#skF_5'(X_118))))).
% 5.30/2.16 tff(c_392, plain, (![X_255]: (~cp2xcomp(X_255) | ~cp2(X_255)))).
% 5.30/2.16 tff(c_96, plain, (![X_104]: (ra_Px5(X_104, '#skF_2'(X_104)) | ~cp2(X_104)))).
% 5.30/2.16 tff(c_379, plain, (![X_253]: (~ca_Cx2(X_253) | ~ca_Cx2xcomp(X_253)))).
% 5.30/2.16 tff(c_176, plain, (![X_163]: (ra_Px2(X_163, '#skF_16'(X_163)) | ~ca_Cx2xcomp(X_163)))).
% 5.30/2.16 tff(c_92, plain, (![X_99]: (rinvR(X_99, '#skF_1'(X_99)) | ~cSatisfiable(X_99)))).
% 5.30/2.16 tff(c_138, plain, (![X_139]: (rr(X_139, '#skF_12'(X_139)) | ~ca_Ax14(X_139)))).
% 5.30/2.16 tff(c_363, plain, (![X_249]: (cp5xcomp(X_249) | cp5(X_249)))).
% 5.30/2.16 tff(c_128, plain, (![X_131]: (cp5(X_131) | ra_Px4(X_131, '#skF_8'(X_131))))).
% 5.30/2.16 tff(c_348, plain, (![X_247]: (ca_Cx1(X_247) | ca_Cx1xcomp(X_247)))).
% 5.30/2.16 tff(c_162, plain, (![X_154]: (ca_Cx1xcomp(X_154) | ra_Px1(X_154, '#skF_14'(X_154))))).
% 5.30/2.16 tff(c_196, plain, (![X_176, Y_177]: (rinvR(X_176, Y_177) | ~rr(Y_177, X_176)))).
% 5.30/2.16 tff(c_338, plain, (![X_243]: (cp2(X_243) | cp2xcomp(X_243)))).
% 5.30/2.16 tff(c_104, plain, (![X_109]: (cp2xcomp(X_109) | ra_Px5(X_109, '#skF_3'(X_109))))).
% 5.30/2.16 tff(c_316, plain, (![X_153]: (~cp3(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.16 tff(c_326, plain, (![X_240]: (~ca_Cx3(X_240) | ~ca_Cx3xcomp(X_240)))).
% 5.30/2.16 tff(c_190, plain, (![X_172]: (ra_Px3(X_172, '#skF_18'(X_172)) | ~ca_Cx3xcomp(X_172)))).
% 5.30/2.16 tff(c_315, plain, (![X_162]: (~cp3(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.16 tff(c_307, plain, (![X_236]: (~ca_Cx1xcomp(X_236) | ~ca_Cx1(X_236)))).
% 5.30/2.16 tff(c_297, plain, (![X_235]: (~cp3xcomp(X_235) | ~cp3(X_235)))).
% 5.30/2.16 tff(c_146, plain, (![X_149]: (ra_Px1(X_149, '#skF_13'(X_149)) | ~ca_Cx1(X_149)))).
% 5.30/2.16 tff(c_106, plain, (![X_113]: (ra_Px6(X_113, '#skF_4'(X_113)) | ~cp3(X_113)))).
% 5.30/2.16 tff(c_287, plain, (![X_233]: (ca_Cx2xcomp(X_233) | ca_Cx2(X_233)))).
% 5.30/2.16 tff(c_166, plain, (![X_158]: (ca_Cx2(X_158) | ra_Px2(X_158, '#skF_15'(X_158))))).
% 5.30/2.16 tff(c_262, plain, (![X_167]: (~cp4(X_167) | ~ca_Cx3(X_167)))).
% 5.30/2.16 tff(c_272, plain, (![X_230]: (cp4xcomp(X_230) | cp4(X_230)))).
% 5.30/2.16 tff(c_118, plain, (![X_122]: (cp4(X_122) | ra_Px7(X_122, '#skF_6'(X_122))))).
% 5.30/2.16 tff(c_261, plain, (![X_162]: (~cp4(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.16 tff(c_260, plain, (![X_153]: (~cp4(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.16 tff(c_249, plain, (![X_226]: (~cp4(X_226) | ~cp4xcomp(X_226)))).
% 5.30/2.16 tff(c_122, plain, (![X_127]: (ra_Px7(X_127, '#skF_7'(X_127)) | ~cp4xcomp(X_127)))).
% 5.30/2.16 tff(c_226, plain, (![X_199]: (ca_Cx1('#skF_12'(X_199)) | ~ca_Ax14(X_199)))).
% 5.30/2.16 tff(c_102, plain, (![X_109, Y_112]: (~ra_Px5(X_109, Y_112) | ~cp2xcomp(X_109)))).
% 5.30/2.16 tff(c_186, plain, (![X_168, Y_171]: (~ra_Px3(X_168, Y_171) | ~ca_Cx3(X_168)))).
% 5.30/2.16 tff(c_148, plain, (![X_149, Y0_152]: (ca_Cx1(X_149) | ~ra_Px1(X_149, Y0_152)))).
% 5.30/2.16 tff(c_98, plain, (![X_104, Y0_107]: (cp2(X_104) | ~ra_Px5(X_104, Y0_107)))).
% 5.30/2.16 tff(c_124, plain, (![X_127, Y0_130]: (cp4xcomp(X_127) | ~ra_Px7(X_127, Y0_130)))).
% 5.30/2.16 tff(c_178, plain, (![X_163, Y0_166]: (ca_Cx2xcomp(X_163) | ~ra_Px2(X_163, Y0_166)))).
% 5.30/2.16 tff(c_116, plain, (![X_122, Y_125]: (~ra_Px7(X_122, Y_125) | ~cp4(X_122)))).
% 5.30/2.16 tff(c_90, plain, (![X_99]: (ca_Ax14('#skF_1'(X_99)) | ~cSatisfiable(X_99)))).
% 5.30/2.16 tff(c_126, plain, (![X_131, Y_134]: (~ra_Px4(X_131, Y_134) | ~cp5(X_131)))).
% 5.30/2.16 tff(c_164, plain, (![X_158, Y_161]: (~ra_Px2(X_158, Y_161) | ~ca_Cx2(X_158)))).
% 5.30/2.16 tff(c_160, plain, (![X_154, Y_157]: (~ra_Px1(X_154, Y_157) | ~ca_Cx1xcomp(X_154)))).
% 5.30/2.16 tff(c_192, plain, (![X_172, Y0_175]: (ca_Cx3xcomp(X_172) | ~ra_Px3(X_172, Y0_175)))).
% 5.30/2.16 tff(c_132, plain, (![X_135, Y0_138]: (cp5xcomp(X_135) | ~ra_Px4(X_135, Y0_138)))).
% 5.30/2.16 tff(c_136, plain, (![X_139]: (cp1('#skF_12'(X_139)) | ~ca_Ax14(X_139)))).
% 5.30/2.16 tff(c_112, plain, (![X_118, Y_121]: (~ra_Px6(X_118, Y_121) | ~cp3xcomp(X_118)))).
% 5.30/2.16 tff(c_108, plain, (![X_113, Y0_116]: (cp3(X_113) | ~ra_Px6(X_113, Y0_116)))).
% 5.30/2.16 tff(c_94, plain, (![X_103]: (ca_Cx1(X_103) | ~cp1(X_103)))).
% 5.30/2.16 tff(c_172, plain, (![X_162]: (cp3xcomp(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.16 tff(c_100, plain, (![X_108]: (ca_Cx2(X_108) | ~cp2(X_108)))).
% 5.30/2.16 tff(c_152, plain, (![X_153]: (cp4xcomp(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.16 tff(c_154, plain, (![X_153]: (cp3xcomp(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.16 tff(c_110, plain, (![X_117]: (ca_Cx3(X_117) | ~cp3(X_117)))).
% 5.30/2.16 tff(c_156, plain, (![X_153]: (cp2xcomp(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.16 tff(c_120, plain, (![X_126]: (cp5xcomp(X_126) | ~cp4(X_126)))).
% 5.30/2.16 tff(c_86, plain, (![X_98]: (xsd_string(X_98) | xsd_integer(X_98)))).
% 5.30/2.16 tff(c_84, plain, (![X_98]: (~xsd_integer(X_98) | ~xsd_string(X_98)))).
% 5.30/2.17 tff(c_174, plain, (![X_162]: (cp5xcomp(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.17 tff(c_170, plain, (![X_162]: (cp4xcomp(X_162) | ~ca_Cx2(X_162)))).
% 5.30/2.17 tff(c_158, plain, (![X_153]: (cp5xcomp(X_153) | ~ca_Cx1(X_153)))).
% 5.30/2.17 tff(c_182, plain, (![X_167]: (cp4xcomp(X_167) | ~ca_Cx3(X_167)))).
% 5.30/2.17 tff(c_184, plain, (![X_167]: (cp5xcomp(X_167) | ~ca_Cx3(X_167)))).
% 5.30/2.17 tff(c_80, plain, (![X_97]: (cowlThing(X_97)))).
% 5.30/2.17 tff(c_82, plain, (![X_97]: (~cowlNothing(X_97)))).
% 5.30/2.17 tff(c_198, plain, (cSatisfiable(i2003_11_14_17_16_14536))).
% 5.30/2.17 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.30/2.17
%------------------------------------------------------------------------------