%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO683-1 : TPTP v9.0.0. Released v7.3.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 10:38:06 PM UTC 2025
% Result : Unsatisfiable 6.28s 2.49s
% Output : CNFRefutation 6.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SYO683-1 : TPTP v9.0.0. Released v7.3.0.
% 0.10/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.12/0.34 % Computer : n028.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 09:43:05 EDT 2025
% 0.12/0.34 % CPUTime :
% 6.28/2.49 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.28/2.50
% 6.28/2.50 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.64/2.51 %$ iLEQ > LE > E > #nlpp > suc > s > f > z > 0
% 6.64/2.51
% 6.64/2.51 %Foreground sorts:
% 6.64/2.51
% 6.64/2.51
% 6.64/2.51 %Background operators:
% 6.64/2.51
% 6.64/2.51
% 6.64/2.51 %Foreground operators:
% 6.64/2.51 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 6.64/2.51 tff(s, type, s: $i > $i).
% 6.64/2.51 tff(f, type, f: $i > $i).
% 6.64/2.51 tff(0, type, 0: $i).
% 6.64/2.51 tff(LE, type, LE: ($i * $i) > $o).
% 6.64/2.51 tff(suc, type, suc: $i > $i).
% 6.64/2.51 tff(z, type, z: $i).
% 6.64/2.51 tff(E, type, E: ($i * $i) > $o).
% 6.64/2.51
% 6.64/2.54 tff(f_41, axiom, (![A]: LE(f(A), s(s(s(s(0)))))), file('unknown', unknown)).
% 6.64/2.54 tff(f_170, axiom, (![B_158]: ((~LE(f(B_158), s(s(s(s(0))))) | E(s(s(s(0))), f(B_158))) | LE(f(B_158), s(s(s(0)))))), file('unknown', unknown)).
% 6.64/2.54 tff(f_105, axiom, (![B_247]: ((~LE(f(B_247), s(s(s(0)))) | E(s(s(0)), f(B_247))) | LE(f(B_247), s(s(0))))), file('unknown', unknown)).
% 6.64/2.54 tff(f_112, axiom, (![B_158]: ((~LE(f(suc(B_158)), s(s(s(s(0))))) | E(s(s(s(0))), f(suc(B_158)))) | LE(f(B_158), s(s(s(0)))))), file('unknown', unknown)).
% 6.64/2.54 tff(f_178, axiom, (![A_1]: ((~E(s(s(s(0))), f(A_1)) | ~E(s(s(s(0))), f(suc(A_1)))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_91, axiom, (![B_160, B_159, A_1, B_161, B_162]: (((((((((((((~E(s(s(s(0))), f(suc(B_159))) | ~E(s(s(s(0))), f(B_162))) | ~iLEQ(suc(B_160), suc(B_161))) | ~E(s(s(s(0))), f(suc(B_162)))) | ~E(s(s(s(0))), f(B_159))) | ~E(s(s(s(0))), f(B_161))) | ~E(s(s(s(0))), f(B_160))) | ~iLEQ(suc(B_159), suc(B_160))) | ~E(s(s(s(0))), f(A_1))) | ~E(s(s(s(0))), f(suc(B_161)))) | ~iLEQ(suc(B_161), suc(B_162))) | ~E(s(s(s(0))), f(suc(B_160)))) | ~E(s(s(s(0))), f(suc(A_1)))) | ~iLEQ(suc(A_1), suc(B_159)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_192, axiom, (![B_291]: ((~LE(f(B_291), s(s(0))) | E(s(0), f(B_291))) | LE(f(B_291), s(0)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_98, axiom, (![B_247]: ((~LE(f(suc(B_247)), s(s(s(0)))) | E(s(s(0)), f(suc(B_247)))) | LE(f(B_247), s(s(0))))), file('unknown', unknown)).
% 6.64/2.54 tff(f_49, axiom, (![A_2]: ((~E(s(s(0)), f(A_2)) | ~E(s(s(0)), f(suc(A_2)))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_163, axiom, (![B_249, B_251, B_250, B_248, A_2]: (((((((((((((~E(s(s(0)), f(suc(B_249))) | ~E(s(s(0)), f(B_250))) | ~iLEQ(suc(A_2), suc(B_248))) | ~E(s(s(0)), f(B_248))) | ~E(s(s(0)), f(suc(B_251)))) | ~iLEQ(suc(B_249), suc(B_250))) | ~E(s(s(0)), f(suc(A_2)))) | ~E(s(s(0)), f(B_251))) | ~E(s(s(0)), f(suc(B_248)))) | ~E(s(s(0)), f(suc(B_250)))) | ~iLEQ(suc(B_248), suc(B_249))) | ~E(s(s(0)), f(B_249))) | ~E(s(s(0)), f(A_2))) | ~iLEQ(suc(B_250), suc(B_251)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_241, axiom, (![B_309]: ((~LE(f(B_309), s(0)) | E(0, f(B_309))) | LE(f(B_309), 0))), file('unknown', unknown)).
% 6.64/2.54 tff(f_185, axiom, (![B_291]: ((~LE(f(suc(B_291)), s(s(0))) | E(s(0), f(suc(B_291)))) | LE(f(B_291), s(0)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_39, axiom, (![A_3]: ((~E(s(0), f(A_3)) | ~E(s(0), f(suc(A_3)))) | iLEQ(suc(A_3), suc(A_3)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_283, axiom, (![B_292, B_295, B_293, A_3, B_294]: (((((((((((((~E(s(0), f(suc(B_294))) | ~E(s(0), f(B_295))) | ~E(s(0), f(suc(B_295)))) | ~E(s(0), f(suc(B_292)))) | ~E(s(0), f(suc(A_3)))) | ~E(s(0), f(B_294))) | ~E(s(0), f(B_292))) | ~iLEQ(suc(A_3), suc(B_292))) | ~E(s(0), f(B_293))) | ~iLEQ(suc(B_294), suc(B_295))) | ~E(s(0), f(A_3))) | ~E(s(0), f(suc(B_293)))) | ~iLEQ(suc(B_293), suc(B_294))) | ~iLEQ(suc(B_292), suc(B_293)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_114, axiom, ~LE(f(z), 0), file('unknown', unknown)).
% 6.64/2.54 tff(f_121, axiom, (![B_309]: ((~LE(f(suc(B_309)), s(0)) | E(0, f(suc(B_309)))) | LE(f(B_309), 0))), file('unknown', unknown)).
% 6.64/2.54 tff(f_31, axiom, (![A_4]: ((~E(0, f(A_4)) | ~E(0, f(suc(A_4)))) | iLEQ(suc(A_4), suc(A_4)))), file('unknown', unknown)).
% 6.64/2.54 tff(f_234, axiom, (![B_312, B_310, B_311, A_4, B_313]: (((((((((((((~E(0, f(suc(B_310))) | ~E(0, f(suc(B_311)))) | ~E(0, f(B_311))) | ~E(0, f(suc(B_313)))) | ~E(0, f(B_310))) | ~E(0, f(B_312))) | ~E(0, f(suc(B_312)))) | ~E(0, f(B_313))) | ~iLEQ(suc(B_311), suc(B_312))) | ~iLEQ(suc(B_310), suc(B_311))) | ~iLEQ(suc(A_4), suc(B_310))) | ~E(0, f(suc(A_4)))) | ~iLEQ(suc(B_312), suc(B_313))) | ~E(0, f(A_4)))), file('unknown', unknown)).
% 6.64/2.54 tff(c_6, plain, (![A_3]: (LE(f(A_3), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_41])).
% 6.64/2.54 tff(c_24, plain, (![B_158_19]: (LE(f(B_158_19), s(s(s(0)))) | E(s(s(s(0))), f(B_158_19)) | ~LE(f(B_158_19), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_170])).
% 6.64/2.54 tff(c_40, plain, (![B_158_19]: (LE(f(B_158_19), s(s(s(0)))) | E(s(s(s(0))), f(B_158_19)))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_24])).
% 6.64/2.54 tff(c_51, plain, (![B_247_44]: (LE(f(B_247_44), s(s(0))) | E(s(s(0)), f(B_247_44)) | ~LE(f(B_247_44), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_105])).
% 6.64/2.54 tff(c_55, plain, (![B_158_19]: (LE(f(B_158_19), s(s(0))) | E(s(s(0)), f(B_158_19)) | E(s(s(s(0))), f(B_158_19)))), inference(resolution, [status(thm)], [c_40, c_51])).
% 6.64/2.54 tff(c_16, plain, (![B_158_12]: (LE(f(B_158_12), s(s(s(0)))) | E(s(s(s(0))), f(suc(B_158_12))) | ~LE(f(suc(B_158_12)), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_112])).
% 6.64/2.54 tff(c_38, plain, (![B_158_12]: (LE(f(B_158_12), s(s(s(0)))) | E(s(s(s(0))), f(suc(B_158_12))))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_16])).
% 6.64/2.54 tff(c_57, plain, (![A_1_46]: (iLEQ(suc(A_1_46), suc(A_1_46)) | ~E(s(s(s(0))), f(suc(A_1_46))) | ~E(s(s(s(0))), f(A_1_46)))), inference(cnfTransformation, [status(thm)], [f_178])).
% 6.64/2.54 tff(c_64, plain, (![B_158_12]: (iLEQ(suc(B_158_12), suc(B_158_12)) | ~E(s(s(s(0))), f(B_158_12)) | LE(f(B_158_12), s(s(s(0)))))), inference(resolution, [status(thm)], [c_38, c_57])).
% 6.64/2.54 tff(c_245, plain, (![B_159_80, A_1_79, B_160_78, B_162_81, B_161_77]: (~iLEQ(suc(A_1_79), suc(B_159_80)) | ~E(s(s(s(0))), f(suc(A_1_79))) | ~E(s(s(s(0))), f(suc(B_160_78))) | ~iLEQ(suc(B_161_77), suc(B_162_81)) | ~E(s(s(s(0))), f(suc(B_161_77))) | ~E(s(s(s(0))), f(A_1_79)) | ~iLEQ(suc(B_159_80), suc(B_160_78)) | ~E(s(s(s(0))), f(B_160_78)) | ~E(s(s(s(0))), f(B_161_77)) | ~E(s(s(s(0))), f(B_159_80)) | ~E(s(s(s(0))), f(suc(B_162_81))) | ~iLEQ(suc(B_160_78), suc(B_161_77)) | ~E(s(s(s(0))), f(B_162_81)) | ~E(s(s(s(0))), f(suc(B_159_80))))), inference(cnfTransformation, [status(thm)], [f_91])).
% 6.64/2.54 tff(c_624, plain, (![B_160_114, B_161_115, B_162_116, B_158_117]: (~E(s(s(s(0))), f(suc(B_160_114))) | ~iLEQ(suc(B_161_115), suc(B_162_116)) | ~E(s(s(s(0))), f(suc(B_161_115))) | ~iLEQ(suc(B_158_117), suc(B_160_114)) | ~E(s(s(s(0))), f(B_160_114)) | ~E(s(s(s(0))), f(B_161_115)) | ~E(s(s(s(0))), f(suc(B_162_116))) | ~iLEQ(suc(B_160_114), suc(B_161_115)) | ~E(s(s(s(0))), f(B_162_116)) | ~E(s(s(s(0))), f(suc(B_158_117))) | ~E(s(s(s(0))), f(B_158_117)) | LE(f(B_158_117), s(s(s(0)))))), inference(resolution, [status(thm)], [c_64, c_245])).
% 6.64/2.54 tff(c_760, plain, (![B_161_131, B_162_132, B_158_133, B_158_134]: (~iLEQ(suc(B_161_131), suc(B_162_132)) | ~E(s(s(s(0))), f(suc(B_161_131))) | ~iLEQ(suc(B_158_133), suc(B_158_134)) | ~E(s(s(s(0))), f(B_158_134)) | ~E(s(s(s(0))), f(B_161_131)) | ~E(s(s(s(0))), f(suc(B_162_132))) | ~iLEQ(suc(B_158_134), suc(B_161_131)) | ~E(s(s(s(0))), f(B_162_132)) | ~E(s(s(s(0))), f(suc(B_158_133))) | ~E(s(s(s(0))), f(B_158_133)) | LE(f(B_158_133), s(s(s(0)))) | LE(f(B_158_134), s(s(s(0)))))), inference(resolution, [status(thm)], [c_38, c_624])).
% 6.64/2.54 tff(c_794, plain, (![B_158_135, B_158_136, B_158_137]: (~iLEQ(suc(B_158_135), suc(B_158_136)) | ~E(s(s(s(0))), f(B_158_136)) | ~E(s(s(s(0))), f(suc(B_158_137))) | ~iLEQ(suc(B_158_136), suc(B_158_137)) | ~E(s(s(s(0))), f(suc(B_158_135))) | ~E(s(s(s(0))), f(B_158_135)) | LE(f(B_158_135), s(s(s(0)))) | LE(f(B_158_136), s(s(s(0)))) | ~E(s(s(s(0))), f(B_158_137)) | LE(f(B_158_137), s(s(s(0)))))), inference(resolution, [status(thm)], [c_64, c_760])).
% 6.64/2.54 tff(c_828, plain, (![B_158_138, B_158_139]: (~E(s(s(s(0))), f(suc(B_158_138))) | ~iLEQ(suc(B_158_139), suc(B_158_138)) | ~E(s(s(s(0))), f(suc(B_158_139))) | ~E(s(s(s(0))), f(B_158_138)) | LE(f(B_158_138), s(s(s(0)))) | ~E(s(s(s(0))), f(B_158_139)) | LE(f(B_158_139), s(s(s(0)))))), inference(resolution, [status(thm)], [c_64, c_794])).
% 6.64/2.54 tff(c_839, plain, (![B_158_140, B_158_141]: (~iLEQ(suc(B_158_140), suc(B_158_141)) | ~E(s(s(s(0))), f(suc(B_158_140))) | ~E(s(s(s(0))), f(B_158_141)) | ~E(s(s(s(0))), f(B_158_140)) | LE(f(B_158_140), s(s(s(0)))) | LE(f(B_158_141), s(s(s(0)))))), inference(resolution, [status(thm)], [c_38, c_828])).
% 6.64/2.54 tff(c_873, plain, (![B_158_142]: (~E(s(s(s(0))), f(suc(B_158_142))) | ~E(s(s(s(0))), f(B_158_142)) | LE(f(B_158_142), s(s(s(0)))))), inference(resolution, [status(thm)], [c_64, c_839])).
% 6.64/2.54 tff(c_886, plain, (![B_158_143]: (~E(s(s(s(0))), f(B_158_143)) | LE(f(B_158_143), s(s(s(0)))))), inference(resolution, [status(thm)], [c_38, c_873])).
% 6.64/2.54 tff(c_14, plain, (![B_247_11]: (LE(f(B_247_11), s(s(0))) | E(s(s(0)), f(B_247_11)) | ~LE(f(B_247_11), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_105])).
% 6.64/2.54 tff(c_895, plain, (![B_158_144]: (LE(f(B_158_144), s(s(0))) | E(s(s(0)), f(B_158_144)) | ~E(s(s(s(0))), f(B_158_144)))), inference(resolution, [status(thm)], [c_886, c_14])).
% 6.64/2.54 tff(c_908, plain, (![B_158_145]: (LE(f(B_158_145), s(s(0))) | E(s(s(0)), f(B_158_145)))), inference(resolution, [status(thm)], [c_55, c_895])).
% 6.64/2.54 tff(c_30, plain, (![B_291_22]: (LE(f(B_291_22), s(0)) | E(s(0), f(B_291_22)) | ~LE(f(B_291_22), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_192])).
% 6.64/2.54 tff(c_916, plain, (![B_158_145]: (LE(f(B_158_145), s(0)) | E(s(0), f(B_158_145)) | E(s(s(0)), f(B_158_145)))), inference(resolution, [status(thm)], [c_908, c_30])).
% 6.64/2.54 tff(c_70, plain, (![B_247_48]: (LE(f(B_247_48), s(s(0))) | E(s(s(0)), f(suc(B_247_48))) | ~LE(f(suc(B_247_48)), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_98])).
% 6.64/2.54 tff(c_78, plain, (![B_247_48]: (LE(f(B_247_48), s(s(0))) | E(s(s(0)), f(suc(B_247_48))) | E(s(s(s(0))), f(suc(B_247_48))))), inference(resolution, [status(thm)], [c_40, c_70])).
% 6.64/2.54 tff(c_12, plain, (![B_247_10]: (LE(f(B_247_10), s(s(0))) | E(s(s(0)), f(suc(B_247_10))) | ~LE(f(suc(B_247_10)), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_98])).
% 6.64/2.54 tff(c_926, plain, (![B_247_148]: (LE(f(B_247_148), s(s(0))) | E(s(s(0)), f(suc(B_247_148))) | ~E(s(s(s(0))), f(suc(B_247_148))))), inference(resolution, [status(thm)], [c_886, c_12])).
% 6.64/2.54 tff(c_933, plain, (![B_247_48]: (LE(f(B_247_48), s(s(0))) | E(s(s(0)), f(suc(B_247_48))))), inference(resolution, [status(thm)], [c_78, c_926])).
% 6.64/2.54 tff(c_948, plain, (![B_247_150]: (LE(f(B_247_150), s(s(0))) | E(s(s(0)), f(suc(B_247_150))))), inference(resolution, [status(thm)], [c_78, c_926])).
% 6.64/2.54 tff(c_8, plain, (![A_2_4]: (iLEQ(suc(A_2_4), suc(A_2_4)) | ~E(s(s(0)), f(suc(A_2_4))) | ~E(s(s(0)), f(A_2_4)))), inference(cnfTransformation, [status(thm)], [f_49])).
% 6.64/2.54 tff(c_954, plain, (![B_247_150]: (iLEQ(suc(B_247_150), suc(B_247_150)) | ~E(s(s(0)), f(B_247_150)) | LE(f(B_247_150), s(s(0))))), inference(resolution, [status(thm)], [c_948, c_8])).
% 6.64/2.54 tff(c_955, plain, (![B_247_151]: (iLEQ(suc(B_247_151), suc(B_247_151)) | ~E(s(s(0)), f(B_247_151)) | LE(f(B_247_151), s(s(0))))), inference(resolution, [status(thm)], [c_948, c_8])).
% 6.64/2.54 tff(c_22, plain, (![B_248_17, B_251_15, B_250_16, B_249_14, A_2_18]: (~iLEQ(suc(B_250_16), suc(B_251_15)) | ~E(s(s(0)), f(A_2_18)) | ~E(s(s(0)), f(B_249_14)) | ~iLEQ(suc(B_248_17), suc(B_249_14)) | ~E(s(s(0)), f(suc(B_250_16))) | ~E(s(s(0)), f(suc(B_248_17))) | ~E(s(s(0)), f(B_251_15)) | ~E(s(s(0)), f(suc(A_2_18))) | ~iLEQ(suc(B_249_14), suc(B_250_16)) | ~E(s(s(0)), f(suc(B_251_15))) | ~E(s(s(0)), f(B_248_17)) | ~iLEQ(suc(A_2_18), suc(B_248_17)) | ~E(s(s(0)), f(B_250_16)) | ~E(s(s(0)), f(suc(B_249_14))))), inference(cnfTransformation, [status(thm)], [f_163])).
% 6.64/2.54 tff(c_1103, plain, (![A_2_166, B_249_167, B_248_168, B_247_169]: (~E(s(s(0)), f(A_2_166)) | ~E(s(s(0)), f(B_249_167)) | ~iLEQ(suc(B_248_168), suc(B_249_167)) | ~E(s(s(0)), f(suc(B_248_168))) | ~E(s(s(0)), f(suc(A_2_166))) | ~iLEQ(suc(B_249_167), suc(B_247_169)) | ~E(s(s(0)), f(suc(B_247_169))) | ~E(s(s(0)), f(B_248_168)) | ~iLEQ(suc(A_2_166), suc(B_248_168)) | ~E(s(s(0)), f(suc(B_249_167))) | ~E(s(s(0)), f(B_247_169)) | LE(f(B_247_169), s(s(0))))), inference(resolution, [status(thm)], [c_955, c_22])).
% 6.64/2.54 tff(c_1212, plain, (![A_2_180, B_247_181, B_247_182]: (~E(s(s(0)), f(A_2_180)) | ~E(s(s(0)), f(suc(A_2_180))) | ~iLEQ(suc(B_247_181), suc(B_247_182)) | ~E(s(s(0)), f(suc(B_247_182))) | ~iLEQ(suc(A_2_180), suc(B_247_181)) | ~E(s(s(0)), f(suc(B_247_181))) | ~E(s(s(0)), f(B_247_182)) | LE(f(B_247_182), s(s(0))) | ~E(s(s(0)), f(B_247_181)) | LE(f(B_247_181), s(s(0))))), inference(resolution, [status(thm)], [c_954, c_1103])).
% 6.64/2.54 tff(c_1223, plain, (![B_247_183, B_247_184, B_247_185]: (~E(s(s(0)), f(B_247_183)) | ~iLEQ(suc(B_247_184), suc(B_247_185)) | ~E(s(s(0)), f(suc(B_247_185))) | ~iLEQ(suc(B_247_183), suc(B_247_184)) | ~E(s(s(0)), f(suc(B_247_184))) | ~E(s(s(0)), f(B_247_185)) | LE(f(B_247_185), s(s(0))) | ~E(s(s(0)), f(B_247_184)) | LE(f(B_247_184), s(s(0))) | LE(f(B_247_183), s(s(0))))), inference(resolution, [status(thm)], [c_933, c_1212])).
% 6.64/2.54 tff(c_1248, plain, (![B_247_186, B_247_187]: (~E(s(s(0)), f(B_247_186)) | ~iLEQ(suc(B_247_186), suc(B_247_187)) | ~E(s(s(0)), f(suc(B_247_187))) | LE(f(B_247_186), s(s(0))) | ~E(s(s(0)), f(B_247_187)) | LE(f(B_247_187), s(s(0))))), inference(resolution, [status(thm)], [c_954, c_1223])).
% 6.64/2.54 tff(c_1273, plain, (![B_247_188]: (~E(s(s(0)), f(suc(B_247_188))) | ~E(s(s(0)), f(B_247_188)) | LE(f(B_247_188), s(s(0))))), inference(resolution, [status(thm)], [c_954, c_1248])).
% 6.64/2.54 tff(c_1311, plain, (![B_247_193]: (~E(s(s(0)), f(B_247_193)) | LE(f(B_247_193), s(s(0))))), inference(resolution, [status(thm)], [c_933, c_1273])).
% 6.64/2.54 tff(c_1320, plain, (![B_247_194]: (LE(f(B_247_194), s(0)) | E(s(0), f(B_247_194)) | ~E(s(s(0)), f(B_247_194)))), inference(resolution, [status(thm)], [c_1311, c_30])).
% 6.64/2.54 tff(c_1333, plain, (![B_158_195]: (LE(f(B_158_195), s(0)) | E(s(0), f(B_158_195)))), inference(resolution, [status(thm)], [c_916, c_1320])).
% 6.64/2.54 tff(c_34, plain, (![B_309_28]: (LE(f(B_309_28), 0) | E(0, f(B_309_28)) | ~LE(f(B_309_28), s(0)))), inference(cnfTransformation, [status(thm)], [f_241])).
% 6.64/2.54 tff(c_1341, plain, (![B_158_195]: (LE(f(B_158_195), 0) | E(0, f(B_158_195)) | E(s(0), f(B_158_195)))), inference(resolution, [status(thm)], [c_1333, c_34])).
% 6.64/2.54 tff(c_28, plain, (![B_291_21]: (LE(f(B_291_21), s(0)) | E(s(0), f(suc(B_291_21))) | ~LE(f(suc(B_291_21)), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_185])).
% 6.64/2.54 tff(c_915, plain, (![B_291_21]: (LE(f(B_291_21), s(0)) | E(s(0), f(suc(B_291_21))) | E(s(s(0)), f(suc(B_291_21))))), inference(resolution, [status(thm)], [c_908, c_28])).
% 6.64/2.54 tff(c_1351, plain, (![B_291_198]: (LE(f(B_291_198), s(0)) | E(s(0), f(suc(B_291_198))) | ~E(s(s(0)), f(suc(B_291_198))))), inference(resolution, [status(thm)], [c_1311, c_28])).
% 6.64/2.54 tff(c_1359, plain, (![B_291_21]: (LE(f(B_291_21), s(0)) | E(s(0), f(suc(B_291_21))))), inference(resolution, [status(thm)], [c_915, c_1351])).
% 6.64/2.54 tff(c_1360, plain, (![B_291_199]: (LE(f(B_291_199), s(0)) | E(s(0), f(suc(B_291_199))))), inference(resolution, [status(thm)], [c_915, c_1351])).
% 6.64/2.54 tff(c_4, plain, (![A_3_2]: (iLEQ(suc(A_3_2), suc(A_3_2)) | ~E(s(0), f(suc(A_3_2))) | ~E(s(0), f(A_3_2)))), inference(cnfTransformation, [status(thm)], [f_39])).
% 6.64/2.54 tff(c_1363, plain, (![B_291_199]: (iLEQ(suc(B_291_199), suc(B_291_199)) | ~E(s(0), f(B_291_199)) | LE(f(B_291_199), s(0)))), inference(resolution, [status(thm)], [c_1360, c_4])).
% 6.64/2.54 tff(c_1364, plain, (![B_291_200]: (iLEQ(suc(B_291_200), suc(B_291_200)) | ~E(s(0), f(B_291_200)) | LE(f(B_291_200), s(0)))), inference(resolution, [status(thm)], [c_1360, c_4])).
% 6.64/2.54 tff(c_36, plain, (![B_295_30, B_293_31, B_294_33, B_292_29, A_3_32]: (~iLEQ(suc(B_292_29), suc(B_293_31)) | ~iLEQ(suc(B_293_31), suc(B_294_33)) | ~E(s(0), f(suc(B_293_31))) | ~E(s(0), f(A_3_32)) | ~iLEQ(suc(B_294_33), suc(B_295_30)) | ~E(s(0), f(B_293_31)) | ~iLEQ(suc(A_3_32), suc(B_292_29)) | ~E(s(0), f(B_292_29)) | ~E(s(0), f(B_294_33)) | ~E(s(0), f(suc(A_3_32))) | ~E(s(0), f(suc(B_292_29))) | ~E(s(0), f(suc(B_295_30))) | ~E(s(0), f(B_295_30)) | ~E(s(0), f(suc(B_294_33))))), inference(cnfTransformation, [status(thm)], [f_283])).
% 6.64/2.54 tff(c_1394, plain, (![B_291_203, B_294_204, A_3_205, B_295_206]: (~iLEQ(suc(B_291_203), suc(B_294_204)) | ~E(s(0), f(A_3_205)) | ~iLEQ(suc(B_294_204), suc(B_295_206)) | ~iLEQ(suc(A_3_205), suc(B_291_203)) | ~E(s(0), f(B_294_204)) | ~E(s(0), f(suc(A_3_205))) | ~E(s(0), f(suc(B_291_203))) | ~E(s(0), f(suc(B_295_206))) | ~E(s(0), f(B_295_206)) | ~E(s(0), f(suc(B_294_204))) | ~E(s(0), f(B_291_203)) | LE(f(B_291_203), s(0)))), inference(resolution, [status(thm)], [c_1364, c_36])).
% 6.64/2.54 tff(c_1404, plain, (![A_3_207, B_291_208, B_295_209]: (~E(s(0), f(A_3_207)) | ~iLEQ(suc(B_291_208), suc(B_295_209)) | ~iLEQ(suc(A_3_207), suc(B_291_208)) | ~E(s(0), f(suc(A_3_207))) | ~E(s(0), f(suc(B_295_209))) | ~E(s(0), f(B_295_209)) | ~E(s(0), f(suc(B_291_208))) | ~E(s(0), f(B_291_208)) | LE(f(B_291_208), s(0)))), inference(resolution, [status(thm)], [c_1363, c_1394])).
% 6.64/2.54 tff(c_1414, plain, (![A_3_210, B_291_211]: (~E(s(0), f(A_3_210)) | ~iLEQ(suc(A_3_210), suc(B_291_211)) | ~E(s(0), f(suc(A_3_210))) | ~E(s(0), f(suc(B_291_211))) | ~E(s(0), f(B_291_211)) | LE(f(B_291_211), s(0)))), inference(resolution, [status(thm)], [c_1363, c_1404])).
% 6.64/2.54 tff(c_1424, plain, (![B_291_212]: (~E(s(0), f(suc(B_291_212))) | ~E(s(0), f(B_291_212)) | LE(f(B_291_212), s(0)))), inference(resolution, [status(thm)], [c_1363, c_1414])).
% 6.64/2.54 tff(c_1447, plain, (![B_291_217]: (~E(s(0), f(B_291_217)) | LE(f(B_291_217), s(0)))), inference(resolution, [status(thm)], [c_1359, c_1424])).
% 6.64/2.54 tff(c_1456, plain, (![B_291_218]: (LE(f(B_291_218), 0) | E(0, f(B_291_218)) | ~E(s(0), f(B_291_218)))), inference(resolution, [status(thm)], [c_1447, c_34])).
% 6.64/2.54 tff(c_1469, plain, (![B_158_219]: (LE(f(B_158_219), 0) | E(0, f(B_158_219)))), inference(resolution, [status(thm)], [c_1341, c_1456])).
% 6.64/2.54 tff(c_18, plain, (~LE(f(z), 0)), inference(cnfTransformation, [status(thm)], [f_114])).
% 6.64/2.54 tff(c_1473, plain, (E(0, f(z))), inference(resolution, [status(thm)], [c_1469, c_18])).
% 6.64/2.54 tff(c_20, plain, (![B_309_13]: (LE(f(B_309_13), 0) | E(0, f(suc(B_309_13))) | ~LE(f(suc(B_309_13)), s(0)))), inference(cnfTransformation, [status(thm)], [f_121])).
% 6.64/2.54 tff(c_1340, plain, (![B_309_13]: (LE(f(B_309_13), 0) | E(0, f(suc(B_309_13))) | E(s(0), f(suc(B_309_13))))), inference(resolution, [status(thm)], [c_1333, c_20])).
% 6.64/2.54 tff(c_1474, plain, (![B_309_220]: (LE(f(B_309_220), 0) | E(0, f(suc(B_309_220))) | ~E(s(0), f(suc(B_309_220))))), inference(resolution, [status(thm)], [c_1447, c_20])).
% 6.64/2.54 tff(c_1483, plain, (![B_309_221]: (LE(f(B_309_221), 0) | E(0, f(suc(B_309_221))))), inference(resolution, [status(thm)], [c_1340, c_1474])).
% 6.64/2.54 tff(c_2, plain, (![A_4_1]: (iLEQ(suc(A_4_1), suc(A_4_1)) | ~E(0, f(suc(A_4_1))) | ~E(0, f(A_4_1)))), inference(cnfTransformation, [status(thm)], [f_31])).
% 6.64/2.54 tff(c_99, plain, (![B_311_53, B_313_55, B_312_52, B_310_56, A_4_54]: (~E(0, f(A_4_54)) | ~iLEQ(suc(B_312_52), suc(B_313_55)) | ~E(0, f(suc(A_4_54))) | ~iLEQ(suc(A_4_54), suc(B_310_56)) | ~iLEQ(suc(B_310_56), suc(B_311_53)) | ~iLEQ(suc(B_311_53), suc(B_312_52)) | ~E(0, f(B_313_55)) | ~E(0, f(suc(B_312_52))) | ~E(0, f(B_312_52)) | ~E(0, f(B_310_56)) | ~E(0, f(suc(B_313_55))) | ~E(0, f(B_311_53)) | ~E(0, f(suc(B_311_53))) | ~E(0, f(suc(B_310_56))))), inference(cnfTransformation, [status(thm)], [f_234])).
% 6.64/2.54 tff(c_315, plain, (![A_4_85, B_310_86, B_311_87, A_4_88]: (~E(0, f(A_4_85)) | ~E(0, f(suc(A_4_85))) | ~iLEQ(suc(A_4_85), suc(B_310_86)) | ~iLEQ(suc(B_310_86), suc(B_311_87)) | ~iLEQ(suc(B_311_87), suc(A_4_88)) | ~E(0, f(B_310_86)) | ~E(0, f(B_311_87)) | ~E(0, f(suc(B_311_87))) | ~E(0, f(suc(B_310_86))) | ~E(0, f(suc(A_4_88))) | ~E(0, f(A_4_88)))), inference(resolution, [status(thm)], [c_2, c_99])).
% 6.64/2.54 tff(c_352, plain, (![A_4_89, B_311_90, A_4_91]: (~iLEQ(suc(A_4_89), suc(B_311_90)) | ~iLEQ(suc(B_311_90), suc(A_4_91)) | ~E(0, f(B_311_90)) | ~E(0, f(suc(B_311_90))) | ~E(0, f(suc(A_4_91))) | ~E(0, f(A_4_91)) | ~E(0, f(suc(A_4_89))) | ~E(0, f(A_4_89)))), inference(resolution, [status(thm)], [c_2, c_315])).
% 6.64/2.54 tff(c_389, plain, (![A_4_92, A_4_93]: (~iLEQ(suc(A_4_92), suc(A_4_93)) | ~E(0, f(suc(A_4_93))) | ~E(0, f(A_4_93)) | ~E(0, f(suc(A_4_92))) | ~E(0, f(A_4_92)))), inference(resolution, [status(thm)], [c_2, c_352])).
% 6.64/2.54 tff(c_437, plain, (![A_4_1]: (~E(0, f(suc(A_4_1))) | ~E(0, f(A_4_1)))), inference(resolution, [status(thm)], [c_2, c_389])).
% 6.64/2.54 tff(c_1488, plain, (![B_309_222]: (~E(0, f(B_309_222)) | LE(f(B_309_222), 0))), inference(resolution, [status(thm)], [c_1483, c_437])).
% 6.64/2.54 tff(c_1491, plain, (~E(0, f(z))), inference(resolution, [status(thm)], [c_1488, c_18])).
% 6.64/2.54 tff(c_1495, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_1473, c_1491])).
% 6.64/2.54 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------