%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO651-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/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 : n016.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:02 PM UTC 2025
% Result : Unsatisfiable 20.80s 10.47s
% Output : CNFRefutation 21.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYO651-1 : TPTP v9.0.0. Released v7.3.0.
% 0.11/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 : n016.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 : Wed Apr 9 09:41:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 20.80/10.47 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.80/10.48
% 20.80/10.48 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.80/10.48 %$ iLEQ > LE > E > #nlpp > suc > s > f > z > 0
% 20.80/10.48
% 20.80/10.48 %Foreground sorts:
% 20.80/10.48
% 20.80/10.48
% 20.80/10.48 %Background operators:
% 20.80/10.48
% 20.80/10.48
% 20.80/10.48 %Foreground operators:
% 20.80/10.48 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 20.80/10.48 tff(s, type, s: $i > $i).
% 20.80/10.48 tff(f, type, f: $i > $i).
% 20.80/10.48 tff(0, type, 0: $i).
% 20.80/10.48 tff(LE, type, LE: ($i * $i) > $o).
% 20.80/10.48 tff(suc, type, suc: $i > $i).
% 20.80/10.48 tff(z, type, z: $i).
% 20.80/10.48 tff(E, type, E: ($i * $i) > $o).
% 20.80/10.48
% 21.07/10.51 tff(f_724, axiom, (![A]: LE(f(A), s(0))), file('unknown', unknown)).
% 21.07/10.51 tff(f_2857, axiom, (![B_5]: ((~LE(f(B_5), s(0)) | E(0, f(B_5))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 21.07/10.51 tff(f_1969, axiom, ~LE(f(z), 0), file('unknown', unknown)).
% 21.07/10.51 tff(f_596, axiom, (![B_5]: ((~LE(f(suc(B_5)), s(0)) | E(0, f(suc(B_5)))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 21.07/10.51 tff(f_1871, axiom, (![B_5]: ((~LE(f(suc(suc(B_5))), s(0)) | E(0, f(suc(suc(B_5))))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 21.07/10.51 tff(f_3646, axiom, (![A_1]: (((~E(0, f(A_1)) | ~E(0, f(suc(A_1)))) | E(f(A_1), f(suc(A_1)))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 21.07/10.51 tff(f_3006, axiom, (![B_5]: ((~LE(f(suc(suc(suc(B_5)))), s(0)) | E(0, f(suc(suc(suc(B_5)))))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 21.07/10.51 tff(f_3330, axiom, (![A_1]: (((((~E(0, f(suc(suc(A_1)))) | ~E(0, f(suc(A_1)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(A_1))) | E(f(A_1), f(suc(suc(A_1))))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 21.07/10.51 tff(f_2196, axiom, (![B_5]: ((~LE(f(suc(suc(suc(suc(B_5))))), s(0)) | E(0, f(suc(suc(suc(suc(B_5))))))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 21.07/10.51 tff(f_2292, axiom, (![A_1]: (((((((~E(0, f(suc(suc(suc(A_1))))) | ~E(0, f(suc(A_1)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~E(f(A_1), f(suc(A_1)))) | E(f(A_1), f(suc(suc(suc(A_1)))))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 21.07/10.51 tff(f_189, axiom, (![A_1]: ((((((((~E(0, f(suc(suc(suc(A_1))))) | ~E(0, f(suc(A_1)))) | ~E(f(A_1), f(suc(suc(suc(A_1)))))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(suc(suc(suc(suc(A_1))))))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 21.07/10.51 tff(f_1504, axiom, (![A_1, B_6, B_7]: ((((((((((~iLEQ(suc(A_1), suc(B_6)) | ~E(0, f(suc(B_7)))) | ~E(0, f(suc(A_1)))) | ~E(0, f(A_1))) | ~iLEQ(suc(B_6), suc(B_7))) | ~E(0, f(B_6))) | ~E(0, f(B_7))) | ~E(0, f(suc(B_6)))) | E(f(A_1), f(suc(A_1)))) | E(f(B_6), f(suc(B_6)))) | E(f(B_7), f(suc(B_7))))), file('unknown', unknown)).
% 21.07/10.51 tff(f_1288, axiom, (![B_6, A_1, B_7]: ((((((((((((((((~E(0, f(suc(suc(B_6)))) | ~iLEQ(suc(A_1), suc(B_6))) | ~E(0, f(suc(B_7)))) | ~E(0, f(suc(A_1)))) | ~E(f(B_7), f(suc(B_7)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(0, f(suc(suc(B_7))))) | ~iLEQ(suc(B_6), suc(B_7))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(B_6))) | ~E(0, f(B_7))) | ~E(f(B_6), f(suc(B_6)))) | ~E(0, f(suc(B_6)))) | E(f(A_1), f(suc(suc(A_1))))) | E(f(B_6), f(suc(suc(B_6))))) | E(f(B_7), f(suc(suc(B_7)))))), file('unknown', unknown)).
% 21.07/10.51 tff(f_1044, axiom, (![A_1, B_6, B_7]: ((((((((((((((((((((((~E(0, f(suc(suc(suc(A_1))))) | ~E(0, f(suc(suc(B_6))))) | ~iLEQ(suc(A_1), suc(B_6))) | ~E(0, f(suc(B_7)))) | ~E(0, f(suc(A_1)))) | ~E(f(B_7), f(suc(B_7)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(0, f(suc(suc(B_7))))) | ~E(0, f(suc(suc(suc(B_6)))))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~iLEQ(suc(B_6), suc(B_7))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(B_6))) | ~E(f(B_7), f(suc(suc(B_7))))) | ~E(f(B_6), f(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(B_7)))))) | ~E(0, f(B_7))) | ~E(f(B_6), f(suc(B_6)))) | ~E(0, f(suc(B_6)))) | E(f(A_1), f(suc(suc(suc(A_1)))))) | E(f(B_6), f(suc(suc(suc(B_6)))))) | E(f(B_7), f(suc(suc(suc(B_7))))))), file('unknown', unknown)).
% 21.07/10.51 tff(f_3208, axiom, (![A_1, B_6, B_7]: (((((((((((((((((((((((((~E(0, f(suc(suc(suc(A_1))))) | ~E(0, f(suc(suc(B_6))))) | ~iLEQ(suc(A_1), suc(B_6))) | ~E(0, f(suc(B_7)))) | ~E(0, f(suc(A_1)))) | ~E(f(B_7), f(suc(B_7)))) | ~E(f(A_1), f(suc(suc(suc(A_1)))))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(A_1))) | ~E(0, f(suc(suc(B_7))))) | ~E(0, f(suc(suc(suc(B_6)))))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~iLEQ(suc(B_6), suc(B_7))) | ~E(f(A_1), f(suc(A_1)))) | ~E(0, f(suc(suc(suc(suc(B_6))))))) | ~E(f(B_6), f(suc(suc(suc(B_6)))))) | ~E(f(B_7), f(suc(suc(suc(B_7)))))) | ~E(0, f(B_6))) | ~E(f(B_7), f(suc(suc(B_7))))) | ~E(f(B_6), f(suc(suc(B_6))))) | ~E(0, f(suc(suc(suc(B_7)))))) | ~E(0, f(B_7))) | ~E(0, f(suc(suc(suc(suc(B_7))))))) | ~E(0, f(suc(suc(suc(suc(A_1))))))) | ~E(f(B_6), f(suc(B_6)))) | ~E(0, f(suc(B_6))))), file('unknown', unknown)).
% 21.07/10.51 tff(c_28, plain, (![A_36]: (LE(f(A_36), s(0)))), inference(cnfTransformation, [status(thm)], [f_724])).
% 21.07/10.51 tff(c_114, plain, (![B_5_154]: (LE(f(B_5_154), 0) | E(0, f(B_5_154)) | ~LE(f(B_5_154), s(0)))), inference(cnfTransformation, [status(thm)], [f_2857])).
% 21.07/10.51 tff(c_162, plain, (![B_5_204]: (LE(f(B_5_204), 0) | E(0, f(B_5_204)))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_114])).
% 21.07/10.51 tff(c_78, plain, (~LE(f(z), 0)), inference(cnfTransformation, [status(thm)], [f_1969])).
% 21.07/10.51 tff(c_166, plain, (E(0, f(z))), inference(resolution, [status(thm)], [c_162, c_78])).
% 21.07/10.51 tff(c_22, plain, (![B_5_29]: (LE(f(B_5_29), 0) | E(0, f(suc(B_5_29))) | ~LE(f(suc(B_5_29)), s(0)))), inference(cnfTransformation, [status(thm)], [f_596])).
% 21.07/10.51 tff(c_160, plain, (![B_5_29]: (LE(f(B_5_29), 0) | E(0, f(suc(B_5_29))))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_22])).
% 21.07/10.51 tff(c_72, plain, (![B_5_100]: (LE(f(B_5_100), 0) | E(0, f(suc(suc(B_5_100)))) | ~LE(f(suc(suc(B_5_100))), s(0)))), inference(cnfTransformation, [status(thm)], [f_1871])).
% 21.07/10.51 tff(c_156, plain, (![B_5_100]: (LE(f(B_5_100), 0) | E(0, f(suc(suc(B_5_100)))))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_72])).
% 21.07/10.51 tff(c_148, plain, (![A_1_199]: (iLEQ(suc(A_1_199), suc(A_1_199)) | E(f(A_1_199), f(suc(A_1_199))) | ~E(0, f(suc(A_1_199))) | ~E(0, f(A_1_199)))), inference(cnfTransformation, [status(thm)], [f_3646])).
% 21.07/10.51 tff(c_122, plain, (![B_5_164]: (LE(f(B_5_164), 0) | E(0, f(suc(suc(suc(B_5_164))))) | ~LE(f(suc(suc(suc(B_5_164)))), s(0)))), inference(cnfTransformation, [status(thm)], [f_3006])).
% 21.07/10.51 tff(c_154, plain, (![B_5_164]: (LE(f(B_5_164), 0) | E(0, f(suc(suc(suc(B_5_164))))))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_122])).
% 21.07/10.51 tff(c_134, plain, (![A_1_180]: (iLEQ(suc(A_1_180), suc(A_1_180)) | E(f(A_1_180), f(suc(suc(A_1_180)))) | ~E(0, f(A_1_180)) | ~E(f(A_1_180), f(suc(A_1_180))) | ~E(0, f(suc(A_1_180))) | ~E(0, f(suc(suc(A_1_180)))))), inference(cnfTransformation, [status(thm)], [f_3330])).
% 21.07/10.51 tff(c_88, plain, (![B_5_119]: (LE(f(B_5_119), 0) | E(0, f(suc(suc(suc(suc(B_5_119)))))) | ~LE(f(suc(suc(suc(suc(B_5_119))))), s(0)))), inference(cnfTransformation, [status(thm)], [f_2196])).
% 21.07/10.51 tff(c_158, plain, (![B_5_119]: (LE(f(B_5_119), 0) | E(0, f(suc(suc(suc(suc(B_5_119)))))))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_88])).
% 21.07/10.51 tff(c_92, plain, (![A_1_123]: (iLEQ(suc(A_1_123), suc(A_1_123)) | E(f(A_1_123), f(suc(suc(suc(A_1_123))))) | ~E(f(A_1_123), f(suc(A_1_123))) | ~E(f(A_1_123), f(suc(suc(A_1_123)))) | ~E(0, f(A_1_123)) | ~E(0, f(suc(suc(A_1_123)))) | ~E(0, f(suc(A_1_123))) | ~E(0, f(suc(suc(suc(A_1_123))))))), inference(cnfTransformation, [status(thm)], [f_2292])).
% 21.07/10.51 tff(c_175, plain, (![A_1_215]: (iLEQ(suc(A_1_215), suc(A_1_215)) | ~E(0, f(suc(suc(suc(suc(A_1_215)))))) | ~E(f(A_1_215), f(suc(A_1_215))) | ~E(f(A_1_215), f(suc(suc(A_1_215)))) | ~E(0, f(A_1_215)) | ~E(0, f(suc(suc(A_1_215)))) | ~E(f(A_1_215), f(suc(suc(suc(A_1_215))))) | ~E(0, f(suc(A_1_215))) | ~E(0, f(suc(suc(suc(A_1_215))))))), inference(cnfTransformation, [status(thm)], [f_189])).
% 21.07/10.51 tff(c_180, plain, (![A_1_216]: (~E(0, f(suc(suc(suc(suc(A_1_216)))))) | iLEQ(suc(A_1_216), suc(A_1_216)) | ~E(f(A_1_216), f(suc(A_1_216))) | ~E(f(A_1_216), f(suc(suc(A_1_216)))) | ~E(0, f(A_1_216)) | ~E(0, f(suc(suc(A_1_216)))) | ~E(0, f(suc(A_1_216))) | ~E(0, f(suc(suc(suc(A_1_216))))))), inference(resolution, [status(thm)], [c_92, c_175])).
% 21.07/10.51 tff(c_196, plain, (![B_5_217]: (iLEQ(suc(B_5_217), suc(B_5_217)) | ~E(f(B_5_217), f(suc(B_5_217))) | ~E(f(B_5_217), f(suc(suc(B_5_217)))) | ~E(0, f(B_5_217)) | ~E(0, f(suc(suc(B_5_217)))) | ~E(0, f(suc(B_5_217))) | ~E(0, f(suc(suc(suc(B_5_217))))) | LE(f(B_5_217), 0))), inference(resolution, [status(thm)], [c_158, c_180])).
% 21.07/10.51 tff(c_202, plain, (![A_1_221]: (~E(0, f(suc(suc(suc(A_1_221))))) | LE(f(A_1_221), 0) | iLEQ(suc(A_1_221), suc(A_1_221)) | ~E(0, f(A_1_221)) | ~E(f(A_1_221), f(suc(A_1_221))) | ~E(0, f(suc(A_1_221))) | ~E(0, f(suc(suc(A_1_221)))))), inference(resolution, [status(thm)], [c_134, c_196])).
% 21.07/10.51 tff(c_217, plain, (![B_5_222]: (iLEQ(suc(B_5_222), suc(B_5_222)) | ~E(0, f(B_5_222)) | ~E(f(B_5_222), f(suc(B_5_222))) | ~E(0, f(suc(B_5_222))) | ~E(0, f(suc(suc(B_5_222)))) | LE(f(B_5_222), 0))), inference(resolution, [status(thm)], [c_154, c_202])).
% 21.07/10.51 tff(c_222, plain, (![A_1_223]: (~E(0, f(suc(suc(A_1_223)))) | LE(f(A_1_223), 0) | iLEQ(suc(A_1_223), suc(A_1_223)) | ~E(0, f(suc(A_1_223))) | ~E(0, f(A_1_223)))), inference(resolution, [status(thm)], [c_148, c_217])).
% 21.07/10.51 tff(c_234, plain, (![B_5_100]: (iLEQ(suc(B_5_100), suc(B_5_100)) | ~E(0, f(suc(B_5_100))) | ~E(0, f(B_5_100)) | LE(f(B_5_100), 0))), inference(resolution, [status(thm)], [c_156, c_222])).
% 21.07/10.51 tff(c_237, plain, (![B_5_227]: (iLEQ(suc(B_5_227), suc(B_5_227)) | ~E(0, f(suc(B_5_227))) | ~E(0, f(B_5_227)) | LE(f(B_5_227), 0))), inference(resolution, [status(thm)], [c_156, c_222])).
% 21.07/10.51 tff(c_58, plain, (![B_7_81, B_6_80, A_1_79]: (E(f(B_7_81), f(suc(B_7_81))) | E(f(B_6_80), f(suc(B_6_80))) | E(f(A_1_79), f(suc(A_1_79))) | ~E(0, f(suc(B_6_80))) | ~E(0, f(B_7_81)) | ~E(0, f(B_6_80)) | ~iLEQ(suc(B_6_80), suc(B_7_81)) | ~E(0, f(A_1_79)) | ~E(0, f(suc(A_1_79))) | ~E(0, f(suc(B_7_81))) | ~iLEQ(suc(A_1_79), suc(B_6_80)))), inference(cnfTransformation, [status(thm)], [f_1504])).
% 21.07/10.51 tff(c_251, plain, (![B_5_231, A_1_232]: (E(f(B_5_231), f(suc(B_5_231))) | E(f(A_1_232), f(suc(A_1_232))) | ~E(0, f(A_1_232)) | ~E(0, f(suc(A_1_232))) | ~iLEQ(suc(A_1_232), suc(B_5_231)) | ~E(0, f(suc(B_5_231))) | ~E(0, f(B_5_231)) | LE(f(B_5_231), 0))), inference(resolution, [status(thm)], [c_237, c_58])).
% 21.07/10.51 tff(c_254, plain, (![B_5_100]: (E(f(B_5_100), f(suc(B_5_100))) | ~E(0, f(suc(B_5_100))) | ~E(0, f(B_5_100)) | LE(f(B_5_100), 0))), inference(resolution, [status(thm)], [c_234, c_251])).
% 21.07/10.51 tff(c_590, plain, (![B_7_291, B_6_292, A_1_293]: (E(f(B_7_291), f(suc(suc(B_7_291)))) | E(f(B_6_292), f(suc(suc(B_6_292)))) | E(f(A_1_293), f(suc(suc(A_1_293)))) | ~E(0, f(suc(B_6_292))) | ~E(f(B_6_292), f(suc(B_6_292))) | ~E(0, f(B_7_291)) | ~E(0, f(B_6_292)) | ~E(f(A_1_293), f(suc(A_1_293))) | ~iLEQ(suc(B_6_292), suc(B_7_291)) | ~E(0, f(suc(suc(B_7_291)))) | ~E(0, f(A_1_293)) | ~E(0, f(suc(suc(A_1_293)))) | ~E(f(B_7_291), f(suc(B_7_291))) | ~E(0, f(suc(A_1_293))) | ~E(0, f(suc(B_7_291))) | ~iLEQ(suc(A_1_293), suc(B_6_292)) | ~E(0, f(suc(suc(B_6_292)))))), inference(cnfTransformation, [status(thm)], [f_1288])).
% 21.07/10.51 tff(c_616, plain, (![B_5_297, A_1_298]: (E(f(B_5_297), f(suc(suc(B_5_297)))) | E(f(A_1_298), f(suc(suc(A_1_298)))) | ~E(f(A_1_298), f(suc(A_1_298))) | ~E(0, f(A_1_298)) | ~E(0, f(suc(suc(A_1_298)))) | ~E(f(B_5_297), f(suc(B_5_297))) | ~E(0, f(suc(A_1_298))) | ~iLEQ(suc(A_1_298), suc(B_5_297)) | ~E(0, f(suc(suc(B_5_297)))) | ~E(0, f(suc(B_5_297))) | ~E(0, f(B_5_297)) | LE(f(B_5_297), 0))), inference(resolution, [status(thm)], [c_234, c_590])).
% 21.07/10.51 tff(c_628, plain, (![B_5_100]: (E(f(B_5_100), f(suc(suc(B_5_100)))) | ~E(f(B_5_100), f(suc(B_5_100))) | ~E(0, f(suc(suc(B_5_100)))) | ~E(0, f(suc(B_5_100))) | ~E(0, f(B_5_100)) | LE(f(B_5_100), 0))), inference(resolution, [status(thm)], [c_234, c_616])).
% 21.07/10.51 tff(c_1117, plain, (![B_7_439, B_6_440, A_1_441]: (E(f(B_7_439), f(suc(suc(suc(B_7_439))))) | E(f(B_6_440), f(suc(suc(suc(B_6_440))))) | E(f(A_1_441), f(suc(suc(suc(A_1_441))))) | ~E(0, f(suc(B_6_440))) | ~E(f(B_6_440), f(suc(B_6_440))) | ~E(0, f(B_7_439)) | ~E(0, f(suc(suc(suc(B_7_439))))) | ~E(f(B_6_440), f(suc(suc(B_6_440)))) | ~E(f(B_7_439), f(suc(suc(B_7_439)))) | ~E(0, f(B_6_440)) | ~E(f(A_1_441), f(suc(A_1_441))) | ~iLEQ(suc(B_6_440), suc(B_7_439)) | ~E(f(A_1_441), f(suc(suc(A_1_441)))) | ~E(0, f(suc(suc(suc(B_6_440))))) | ~E(0, f(suc(suc(B_7_439)))) | ~E(0, f(A_1_441)) | ~E(0, f(suc(suc(A_1_441)))) | ~E(f(B_7_439), f(suc(B_7_439))) | ~E(0, f(suc(A_1_441))) | ~E(0, f(suc(B_7_439))) | ~iLEQ(suc(A_1_441), suc(B_6_440)) | ~E(0, f(suc(suc(B_6_440)))) | ~E(0, f(suc(suc(suc(A_1_441))))))), inference(cnfTransformation, [status(thm)], [f_1044])).
% 21.07/10.51 tff(c_1130, plain, (![B_5_442, A_1_443]: (E(f(B_5_442), f(suc(suc(suc(B_5_442))))) | E(f(A_1_443), f(suc(suc(suc(A_1_443))))) | ~E(f(B_5_442), f(suc(suc(B_5_442)))) | ~E(f(A_1_443), f(suc(A_1_443))) | ~E(f(A_1_443), f(suc(suc(A_1_443)))) | ~E(0, f(suc(suc(suc(B_5_442))))) | ~E(0, f(A_1_443)) | ~E(0, f(suc(suc(A_1_443)))) | ~E(f(B_5_442), f(suc(B_5_442))) | ~E(0, f(suc(A_1_443))) | ~iLEQ(suc(A_1_443), suc(B_5_442)) | ~E(0, f(suc(suc(B_5_442)))) | ~E(0, f(suc(suc(suc(A_1_443))))) | ~E(0, f(suc(B_5_442))) | ~E(0, f(B_5_442)) | LE(f(B_5_442), 0))), inference(resolution, [status(thm)], [c_234, c_1117])).
% 21.07/10.51 tff(c_1142, plain, (![B_5_100]: (E(f(B_5_100), f(suc(suc(suc(B_5_100))))) | ~E(f(B_5_100), f(suc(suc(B_5_100)))) | ~E(f(B_5_100), f(suc(B_5_100))) | ~E(0, f(suc(suc(B_5_100)))) | ~E(0, f(suc(suc(suc(B_5_100))))) | ~E(0, f(suc(B_5_100))) | ~E(0, f(B_5_100)) | LE(f(B_5_100), 0))), inference(resolution, [status(thm)], [c_234, c_1130])).
% 21.07/10.51 tff(c_1745, plain, (![B_6_520, A_1_521, B_7_522]: (~E(0, f(suc(B_6_520))) | ~E(f(B_6_520), f(suc(B_6_520))) | ~E(0, f(suc(suc(suc(suc(A_1_521)))))) | ~E(0, f(suc(suc(suc(suc(B_7_522)))))) | ~E(0, f(B_7_522)) | ~E(0, f(suc(suc(suc(B_7_522))))) | ~E(f(B_6_520), f(suc(suc(B_6_520)))) | ~E(f(B_7_522), f(suc(suc(B_7_522)))) | ~E(0, f(B_6_520)) | ~E(f(B_7_522), f(suc(suc(suc(B_7_522))))) | ~E(f(B_6_520), f(suc(suc(suc(B_6_520))))) | ~E(0, f(suc(suc(suc(suc(B_6_520)))))) | ~E(f(A_1_521), f(suc(A_1_521))) | ~iLEQ(suc(B_6_520), suc(B_7_522)) | ~E(f(A_1_521), f(suc(suc(A_1_521)))) | ~E(0, f(suc(suc(suc(B_6_520))))) | ~E(0, f(suc(suc(B_7_522)))) | ~E(0, f(A_1_521)) | ~E(0, f(suc(suc(A_1_521)))) | ~E(f(A_1_521), f(suc(suc(suc(A_1_521))))) | ~E(f(B_7_522), f(suc(B_7_522))) | ~E(0, f(suc(A_1_521))) | ~E(0, f(suc(B_7_522))) | ~iLEQ(suc(A_1_521), suc(B_6_520)) | ~E(0, f(suc(suc(B_6_520)))) | ~E(0, f(suc(suc(suc(A_1_521))))))), inference(cnfTransformation, [status(thm)], [f_3208])).
% 21.07/10.51 tff(c_5904, plain, (![B_6_1358, A_1_1359, B_5_1360]: (~E(0, f(suc(B_6_1358))) | ~E(f(B_6_1358), f(suc(B_6_1358))) | ~E(0, f(suc(suc(suc(suc(A_1_1359)))))) | ~E(0, f(suc(suc(suc(suc(B_5_1360)))))) | ~E(f(B_6_1358), f(suc(suc(B_6_1358)))) | ~E(0, f(B_6_1358)) | ~E(f(B_6_1358), f(suc(suc(suc(B_6_1358))))) | ~E(0, f(suc(suc(suc(suc(B_6_1358)))))) | ~E(f(A_1_1359), f(suc(A_1_1359))) | ~iLEQ(suc(B_6_1358), suc(B_5_1360)) | ~E(f(A_1_1359), f(suc(suc(A_1_1359)))) | ~E(0, f(suc(suc(suc(B_6_1358))))) | ~E(0, f(A_1_1359)) | ~E(0, f(suc(suc(A_1_1359)))) | ~E(f(A_1_1359), f(suc(suc(suc(A_1_1359))))) | ~E(0, f(suc(A_1_1359))) | ~iLEQ(suc(A_1_1359), suc(B_6_1358)) | ~E(0, f(suc(suc(B_6_1358)))) | ~E(0, f(suc(suc(suc(A_1_1359))))) | ~E(f(B_5_1360), f(suc(suc(B_5_1360)))) | ~E(f(B_5_1360), f(suc(B_5_1360))) | ~E(0, f(suc(suc(B_5_1360)))) | ~E(0, f(suc(suc(suc(B_5_1360))))) | ~E(0, f(suc(B_5_1360))) | ~E(0, f(B_5_1360)) | LE(f(B_5_1360), 0))), inference(resolution, [status(thm)], [c_1142, c_1745])).
% 21.07/10.51 tff(c_6701, plain, (![B_6_1477, A_1_1478, B_5_1479]: (~E(0, f(suc(B_6_1477))) | ~E(f(B_6_1477), f(suc(B_6_1477))) | ~E(0, f(suc(suc(suc(suc(A_1_1478)))))) | ~E(f(B_6_1477), f(suc(suc(B_6_1477)))) | ~E(0, f(B_6_1477)) | ~E(f(B_6_1477), f(suc(suc(suc(B_6_1477))))) | ~E(0, f(suc(suc(suc(suc(B_6_1477)))))) | ~E(f(A_1_1478), f(suc(A_1_1478))) | ~iLEQ(suc(B_6_1477), suc(B_5_1479)) | ~E(f(A_1_1478), f(suc(suc(A_1_1478)))) | ~E(0, f(suc(suc(suc(B_6_1477))))) | ~E(0, f(A_1_1478)) | ~E(0, f(suc(suc(A_1_1478)))) | ~E(f(A_1_1478), f(suc(suc(suc(A_1_1478))))) | ~E(0, f(suc(A_1_1478))) | ~iLEQ(suc(A_1_1478), suc(B_6_1477)) | ~E(0, f(suc(suc(B_6_1477)))) | ~E(0, f(suc(suc(suc(A_1_1478))))) | ~E(f(B_5_1479), f(suc(suc(B_5_1479)))) | ~E(f(B_5_1479), f(suc(B_5_1479))) | ~E(0, f(suc(suc(B_5_1479)))) | ~E(0, f(suc(suc(suc(B_5_1479))))) | ~E(0, f(suc(B_5_1479))) | ~E(0, f(B_5_1479)) | LE(f(B_5_1479), 0))), inference(resolution, [status(thm)], [c_158, c_5904])).
% 21.07/10.51 tff(c_7009, plain, (![A_1_1525, B_5_1526, B_5_1527]: (~E(0, f(suc(suc(suc(suc(A_1_1525)))))) | ~E(0, f(suc(suc(suc(suc(B_5_1526)))))) | ~E(f(A_1_1525), f(suc(A_1_1525))) | ~iLEQ(suc(B_5_1526), suc(B_5_1527)) | ~E(f(A_1_1525), f(suc(suc(A_1_1525)))) | ~E(0, f(A_1_1525)) | ~E(0, f(suc(suc(A_1_1525)))) | ~E(f(A_1_1525), f(suc(suc(suc(A_1_1525))))) | ~E(0, f(suc(A_1_1525))) | ~iLEQ(suc(A_1_1525), suc(B_5_1526)) | ~E(0, f(suc(suc(suc(A_1_1525))))) | ~E(f(B_5_1527), f(suc(suc(B_5_1527)))) | ~E(f(B_5_1527), f(suc(B_5_1527))) | ~E(0, f(suc(suc(B_5_1527)))) | ~E(0, f(suc(suc(suc(B_5_1527))))) | ~E(0, f(suc(B_5_1527))) | ~E(0, f(B_5_1527)) | LE(f(B_5_1527), 0) | ~E(f(B_5_1526), f(suc(suc(B_5_1526)))) | ~E(f(B_5_1526), f(suc(B_5_1526))) | ~E(0, f(suc(suc(B_5_1526)))) | ~E(0, f(suc(suc(suc(B_5_1526))))) | ~E(0, f(suc(B_5_1526))) | ~E(0, f(B_5_1526)) | LE(f(B_5_1526), 0))), inference(resolution, [status(thm)], [c_1142, c_6701])).
% 21.07/10.51 tff(c_7025, plain, (![A_1_1528, B_5_1529, B_5_1530]: (~E(0, f(suc(suc(suc(suc(A_1_1528)))))) | ~E(f(A_1_1528), f(suc(A_1_1528))) | ~iLEQ(suc(B_5_1529), suc(B_5_1530)) | ~E(f(A_1_1528), f(suc(suc(A_1_1528)))) | ~E(0, f(A_1_1528)) | ~E(0, f(suc(suc(A_1_1528)))) | ~E(f(A_1_1528), f(suc(suc(suc(A_1_1528))))) | ~E(0, f(suc(A_1_1528))) | ~iLEQ(suc(A_1_1528), suc(B_5_1529)) | ~E(0, f(suc(suc(suc(A_1_1528))))) | ~E(f(B_5_1530), f(suc(suc(B_5_1530)))) | ~E(f(B_5_1530), f(suc(B_5_1530))) | ~E(0, f(suc(suc(B_5_1530)))) | ~E(0, f(suc(suc(suc(B_5_1530))))) | ~E(0, f(suc(B_5_1530))) | ~E(0, f(B_5_1530)) | LE(f(B_5_1530), 0) | ~E(f(B_5_1529), f(suc(suc(B_5_1529)))) | ~E(f(B_5_1529), f(suc(B_5_1529))) | ~E(0, f(suc(suc(B_5_1529)))) | ~E(0, f(suc(suc(suc(B_5_1529))))) | ~E(0, f(suc(B_5_1529))) | ~E(0, f(B_5_1529)) | LE(f(B_5_1529), 0))), inference(resolution, [status(thm)], [c_158, c_7009])).
% 21.07/10.51 tff(c_7032, plain, (![A_1_1531, B_5_1532]: (~E(0, f(suc(suc(suc(suc(A_1_1531)))))) | ~E(f(A_1_1531), f(suc(A_1_1531))) | ~E(f(A_1_1531), f(suc(suc(A_1_1531)))) | ~E(0, f(A_1_1531)) | ~E(0, f(suc(suc(A_1_1531)))) | ~E(f(A_1_1531), f(suc(suc(suc(A_1_1531))))) | ~E(0, f(suc(A_1_1531))) | ~iLEQ(suc(A_1_1531), suc(B_5_1532)) | ~E(0, f(suc(suc(suc(A_1_1531))))) | ~E(f(B_5_1532), f(suc(suc(B_5_1532)))) | ~E(f(B_5_1532), f(suc(B_5_1532))) | ~E(0, f(suc(suc(B_5_1532)))) | ~E(0, f(suc(suc(suc(B_5_1532))))) | ~E(0, f(suc(B_5_1532))) | ~E(0, f(B_5_1532)) | LE(f(B_5_1532), 0))), inference(resolution, [status(thm)], [c_234, c_7025])).
% 21.07/10.51 tff(c_7042, plain, (![B_5_1533, B_5_1534]: (~E(0, f(suc(suc(suc(suc(B_5_1533)))))) | ~iLEQ(suc(B_5_1533), suc(B_5_1534)) | ~E(f(B_5_1534), f(suc(suc(B_5_1534)))) | ~E(f(B_5_1534), f(suc(B_5_1534))) | ~E(0, f(suc(suc(B_5_1534)))) | ~E(0, f(suc(suc(suc(B_5_1534))))) | ~E(0, f(suc(B_5_1534))) | ~E(0, f(B_5_1534)) | LE(f(B_5_1534), 0) | ~E(f(B_5_1533), f(suc(suc(B_5_1533)))) | ~E(f(B_5_1533), f(suc(B_5_1533))) | ~E(0, f(suc(suc(B_5_1533)))) | ~E(0, f(suc(suc(suc(B_5_1533))))) | ~E(0, f(suc(B_5_1533))) | ~E(0, f(B_5_1533)) | LE(f(B_5_1533), 0))), inference(resolution, [status(thm)], [c_1142, c_7032])).
% 21.07/10.51 tff(c_7058, plain, (![B_5_1535, B_5_1536]: (~iLEQ(suc(B_5_1535), suc(B_5_1536)) | ~E(f(B_5_1536), f(suc(suc(B_5_1536)))) | ~E(f(B_5_1536), f(suc(B_5_1536))) | ~E(0, f(suc(suc(B_5_1536)))) | ~E(0, f(suc(suc(suc(B_5_1536))))) | ~E(0, f(suc(B_5_1536))) | ~E(0, f(B_5_1536)) | LE(f(B_5_1536), 0) | ~E(f(B_5_1535), f(suc(suc(B_5_1535)))) | ~E(f(B_5_1535), f(suc(B_5_1535))) | ~E(0, f(suc(suc(B_5_1535)))) | ~E(0, f(suc(suc(suc(B_5_1535))))) | ~E(0, f(suc(B_5_1535))) | ~E(0, f(B_5_1535)) | LE(f(B_5_1535), 0))), inference(resolution, [status(thm)], [c_158, c_7042])).
% 21.07/10.51 tff(c_7065, plain, (![B_5_1537]: (~E(f(B_5_1537), f(suc(suc(B_5_1537)))) | ~E(f(B_5_1537), f(suc(B_5_1537))) | ~E(0, f(suc(suc(B_5_1537)))) | ~E(0, f(suc(suc(suc(B_5_1537))))) | ~E(0, f(suc(B_5_1537))) | ~E(0, f(B_5_1537)) | LE(f(B_5_1537), 0))), inference(resolution, [status(thm)], [c_234, c_7058])).
% 21.07/10.51 tff(c_7078, plain, (![B_5_1538]: (~E(0, f(suc(suc(suc(B_5_1538))))) | ~E(f(B_5_1538), f(suc(B_5_1538))) | ~E(0, f(suc(suc(B_5_1538)))) | ~E(0, f(suc(B_5_1538))) | ~E(0, f(B_5_1538)) | LE(f(B_5_1538), 0))), inference(resolution, [status(thm)], [c_628, c_7065])).
% 21.07/10.51 tff(c_7093, plain, (![B_5_1539]: (~E(f(B_5_1539), f(suc(B_5_1539))) | ~E(0, f(suc(suc(B_5_1539)))) | ~E(0, f(suc(B_5_1539))) | ~E(0, f(B_5_1539)) | LE(f(B_5_1539), 0))), inference(resolution, [status(thm)], [c_154, c_7078])).
% 21.07/10.51 tff(c_7106, plain, (![B_5_1540]: (~E(0, f(suc(suc(B_5_1540)))) | ~E(0, f(suc(B_5_1540))) | ~E(0, f(B_5_1540)) | LE(f(B_5_1540), 0))), inference(resolution, [status(thm)], [c_254, c_7093])).
% 21.07/10.51 tff(c_7123, plain, (![B_5_1541]: (~E(0, f(suc(B_5_1541))) | ~E(0, f(B_5_1541)) | LE(f(B_5_1541), 0))), inference(resolution, [status(thm)], [c_156, c_7106])).
% 21.07/10.51 tff(c_7140, plain, (![B_5_1542]: (~E(0, f(B_5_1542)) | LE(f(B_5_1542), 0))), inference(resolution, [status(thm)], [c_160, c_7123])).
% 21.07/10.51 tff(c_7143, plain, (~E(0, f(z))), inference(resolution, [status(thm)], [c_7140, c_78])).
% 21.07/10.51 tff(c_7147, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_166, c_7143])).
% 21.07/10.51 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------