%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO653-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 : n008.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:03 PM UTC 2025
% Result : Unsatisfiable 14.62s 4.58s
% Output : CNFRefutation 14.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYO653-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.33 % Computer : n008.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.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Apr 9 09:41:17 EDT 2025
% 0.13/0.34 % CPUTime :
% 14.62/4.58 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.62/4.58
% 14.62/4.58 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.74/4.59 %$ iLEQ > LE > E > #nlpp > suc > s > f > z > 0
% 14.74/4.59
% 14.74/4.59 %Foreground sorts:
% 14.74/4.59
% 14.74/4.59
% 14.74/4.59 %Background operators:
% 14.74/4.59
% 14.74/4.59
% 14.74/4.59 %Foreground operators:
% 14.74/4.59 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 14.74/4.59 tff(s, type, s: $i > $i).
% 14.74/4.59 tff(f, type, f: $i > $i).
% 14.74/4.59 tff(0, type, 0: $i).
% 14.74/4.59 tff(LE, type, LE: ($i * $i) > $o).
% 14.74/4.59 tff(suc, type, suc: $i > $i).
% 14.74/4.59 tff(z, type, z: $i).
% 14.74/4.59 tff(E, type, E: ($i * $i) > $o).
% 14.74/4.59
% 14.74/4.61 tff(f_1680, axiom, (![A]: LE(f(A), s(0))), file('unknown', unknown)).
% 14.74/4.61 tff(f_3136, axiom, (![B_10]: ((~LE(f(B_10), s(0)) | E(0, f(B_10))) | LE(f(B_10), 0))), file('unknown', unknown)).
% 14.74/4.61 tff(f_1202, axiom, ~LE(f(z), 0), file('unknown', unknown)).
% 14.74/4.61 tff(f_2926, axiom, (![B_10]: ((~LE(f(suc(B_10)), s(0)) | E(0, f(suc(B_10)))) | LE(f(B_10), 0))), file('unknown', unknown)).
% 14.74/4.61 tff(f_4371, axiom, (![B_10]: ((~LE(f(suc(suc(B_10))), s(0)) | E(0, f(suc(suc(B_10))))) | LE(f(B_10), 0))), file('unknown', unknown)).
% 14.74/4.61 tff(f_4810, 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)).
% 14.74/4.61 tff(f_3411, axiom, (![B_10]: ((~LE(f(suc(suc(suc(B_10)))), s(0)) | E(0, f(suc(suc(suc(B_10)))))) | LE(f(B_10), 0))), file('unknown', unknown)).
% 14.74/4.61 tff(f_1200, 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)).
% 14.74/4.61 tff(f_4631, 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)))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 14.74/4.61 tff(f_543, axiom, (![B_11, B_12, B_13, A_1]: ((((((((((((((~E(0, f(suc(B_11))) | ~iLEQ(suc(B_12), suc(B_13))) | ~E(0, f(suc(A_1)))) | ~E(0, f(B_11))) | ~E(0, f(A_1))) | ~E(0, f(B_13))) | ~E(0, f(suc(B_12)))) | ~iLEQ(suc(A_1), suc(B_11))) | ~E(0, f(suc(B_13)))) | ~E(0, f(B_12))) | ~iLEQ(suc(B_11), suc(B_12))) | E(f(A_1), f(suc(A_1)))) | E(f(B_11), f(suc(B_11)))) | E(f(B_12), f(suc(B_12)))) | E(f(B_13), f(suc(B_13))))), file('unknown', unknown)).
% 14.74/4.61 tff(f_3992, axiom, (![B_11, B_12, B_13, A_1]: ((((((((((((((((((((((~E(0, f(suc(B_11))) | ~iLEQ(suc(B_12), suc(B_13))) | ~E(0, f(suc(suc(B_11))))) | ~E(0, f(suc(A_1)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(B_11))) | ~E(0, f(A_1))) | ~E(0, f(B_13))) | ~E(0, f(suc(B_12)))) | ~E(f(B_12), f(suc(B_12)))) | ~E(0, f(suc(suc(B_12))))) | ~E(f(A_1), f(suc(A_1)))) | ~E(f(B_11), f(suc(B_11)))) | ~iLEQ(suc(A_1), suc(B_11))) | ~E(0, f(suc(B_13)))) | ~E(0, f(B_12))) | ~E(0, f(suc(suc(B_13))))) | ~E(f(B_13), f(suc(B_13)))) | ~iLEQ(suc(B_11), suc(B_12))) | E(f(A_1), f(suc(suc(A_1))))) | E(f(B_11), f(suc(suc(B_11))))) | E(f(B_12), f(suc(suc(B_12))))) | E(f(B_13), f(suc(suc(B_13)))))), file('unknown', unknown)).
% 14.74/4.61 tff(f_3284, axiom, (![A_1, B_11, B_12, B_13]: ((((((((((((((((((((((((((~E(0, f(suc(suc(suc(A_1))))) | ~E(0, f(suc(B_11)))) | ~E(0, f(suc(suc(suc(B_11)))))) | ~iLEQ(suc(B_12), suc(B_13))) | ~E(0, f(suc(suc(B_11))))) | ~E(0, f(suc(A_1)))) | ~E(0, f(suc(suc(A_1))))) | ~E(0, f(B_11))) | ~E(0, f(A_1))) | ~E(0, f(B_13))) | ~E(f(B_11), f(suc(suc(B_11))))) | ~E(0, f(suc(B_12)))) | ~E(f(B_13), f(suc(suc(B_13))))) | ~E(f(B_12), f(suc(suc(B_12))))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~E(f(B_12), f(suc(B_12)))) | ~E(0, f(suc(suc(B_12))))) | ~E(f(A_1), f(suc(A_1)))) | ~E(f(B_11), f(suc(B_11)))) | ~iLEQ(suc(A_1), suc(B_11))) | ~E(0, f(suc(B_13)))) | ~E(0, f(B_12))) | ~E(0, f(suc(suc(suc(B_13)))))) | ~E(0, f(suc(suc(B_13))))) | ~E(f(B_13), f(suc(B_13)))) | ~E(0, f(suc(suc(suc(B_12)))))) | ~iLEQ(suc(B_11), suc(B_12)))), file('unknown', unknown)).
% 14.74/4.61 tff(c_60, plain, (![A_110]: (LE(f(A_110), s(0)))), inference(cnfTransformation, [status(thm)], [f_1680])).
% 14.74/4.61 tff(c_108, plain, (![B_10_200]: (LE(f(B_10_200), 0) | E(0, f(B_10_200)) | ~LE(f(B_10_200), s(0)))), inference(cnfTransformation, [status(thm)], [f_3136])).
% 14.74/4.61 tff(c_190, plain, (![B_10_334]: (LE(f(B_10_334), 0) | E(0, f(B_10_334)))), inference(demodulation, [status(thm), theory('equality')], [c_60, c_108])).
% 14.74/4.61 tff(c_42, plain, (~LE(f(z), 0)), inference(cnfTransformation, [status(thm)], [f_1202])).
% 14.74/4.61 tff(c_194, plain, (E(0, f(z))), inference(resolution, [status(thm)], [c_190, c_42])).
% 14.74/4.61 tff(c_100, plain, (![B_10_187]: (LE(f(B_10_187), 0) | E(0, f(suc(B_10_187))) | ~LE(f(suc(B_10_187)), s(0)))), inference(cnfTransformation, [status(thm)], [f_2926])).
% 14.74/4.61 tff(c_184, plain, (![B_10_187]: (LE(f(B_10_187), 0) | E(0, f(suc(B_10_187))))), inference(demodulation, [status(thm), theory('equality')], [c_60, c_100])).
% 14.74/4.61 tff(c_150, plain, (![B_10_278]: (LE(f(B_10_278), 0) | E(0, f(suc(suc(B_10_278)))) | ~LE(f(suc(suc(B_10_278))), s(0)))), inference(cnfTransformation, [status(thm)], [f_4371])).
% 14.74/4.61 tff(c_188, plain, (![B_10_278]: (LE(f(B_10_278), 0) | E(0, f(suc(suc(B_10_278)))))), inference(demodulation, [status(thm), theory('equality')], [c_60, c_150])).
% 14.74/4.61 tff(c_168, plain, (![A_1_308]: (iLEQ(suc(A_1_308), suc(A_1_308)) | E(f(A_1_308), f(suc(A_1_308))) | ~E(0, f(suc(A_1_308))) | ~E(0, f(A_1_308)))), inference(cnfTransformation, [status(thm)], [f_4810])).
% 14.74/4.61 tff(c_118, plain, (![B_10_217]: (LE(f(B_10_217), 0) | E(0, f(suc(suc(suc(B_10_217))))) | ~LE(f(suc(suc(suc(B_10_217)))), s(0)))), inference(cnfTransformation, [status(thm)], [f_3411])).
% 14.74/4.61 tff(c_186, plain, (![B_10_217]: (LE(f(B_10_217), 0) | E(0, f(suc(suc(suc(B_10_217))))))), inference(demodulation, [status(thm), theory('equality')], [c_60, c_118])).
% 14.74/4.61 tff(c_40, plain, (![A_1_77]: (iLEQ(suc(A_1_77), suc(A_1_77)) | E(f(A_1_77), f(suc(suc(A_1_77)))) | ~E(0, f(A_1_77)) | ~E(f(A_1_77), f(suc(A_1_77))) | ~E(0, f(suc(A_1_77))) | ~E(0, f(suc(suc(A_1_77)))))), inference(cnfTransformation, [status(thm)], [f_1200])).
% 14.74/4.61 tff(c_200, plain, (![A_1_340]: (iLEQ(suc(A_1_340), suc(A_1_340)) | ~E(f(A_1_340), f(suc(A_1_340))) | ~E(f(A_1_340), f(suc(suc(A_1_340)))) | ~E(0, f(A_1_340)) | ~E(0, f(suc(suc(A_1_340)))) | ~E(0, f(suc(A_1_340))) | ~E(0, f(suc(suc(suc(A_1_340))))))), inference(cnfTransformation, [status(thm)], [f_4631])).
% 14.74/4.61 tff(c_205, plain, (![A_1_341]: (~E(0, f(suc(suc(suc(A_1_341))))) | iLEQ(suc(A_1_341), suc(A_1_341)) | ~E(0, f(A_1_341)) | ~E(f(A_1_341), f(suc(A_1_341))) | ~E(0, f(suc(A_1_341))) | ~E(0, f(suc(suc(A_1_341)))))), inference(resolution, [status(thm)], [c_40, c_200])).
% 14.74/4.61 tff(c_217, plain, (![B_10_342]: (iLEQ(suc(B_10_342), suc(B_10_342)) | ~E(0, f(B_10_342)) | ~E(f(B_10_342), f(suc(B_10_342))) | ~E(0, f(suc(B_10_342))) | ~E(0, f(suc(suc(B_10_342)))) | LE(f(B_10_342), 0))), inference(resolution, [status(thm)], [c_186, c_205])).
% 14.74/4.61 tff(c_222, plain, (![A_1_343]: (~E(0, f(suc(suc(A_1_343)))) | LE(f(A_1_343), 0) | iLEQ(suc(A_1_343), suc(A_1_343)) | ~E(0, f(suc(A_1_343))) | ~E(0, f(A_1_343)))), inference(resolution, [status(thm)], [c_168, c_217])).
% 14.74/4.61 tff(c_231, plain, (![B_10_278]: (iLEQ(suc(B_10_278), suc(B_10_278)) | ~E(0, f(suc(B_10_278))) | ~E(0, f(B_10_278)) | LE(f(B_10_278), 0))), inference(resolution, [status(thm)], [c_188, c_222])).
% 14.74/4.61 tff(c_234, plain, (![B_13_345, B_12_346, B_11_347, A_1_348]: (E(f(B_13_345), f(suc(B_13_345))) | E(f(B_12_346), f(suc(B_12_346))) | E(f(B_11_347), f(suc(B_11_347))) | E(f(A_1_348), f(suc(A_1_348))) | ~iLEQ(suc(B_11_347), suc(B_12_346)) | ~E(0, f(B_12_346)) | ~E(0, f(suc(B_13_345))) | ~iLEQ(suc(A_1_348), suc(B_11_347)) | ~E(0, f(suc(B_12_346))) | ~E(0, f(B_13_345)) | ~E(0, f(A_1_348)) | ~E(0, f(B_11_347)) | ~E(0, f(suc(A_1_348))) | ~iLEQ(suc(B_12_346), suc(B_13_345)) | ~E(0, f(suc(B_11_347))))), inference(cnfTransformation, [status(thm)], [f_543])).
% 14.74/4.61 tff(c_276, plain, (![B_13_358, B_10_359, A_1_360]: (E(f(B_13_358), f(suc(B_13_358))) | E(f(B_10_359), f(suc(B_10_359))) | E(f(A_1_360), f(suc(A_1_360))) | ~E(0, f(suc(B_13_358))) | ~iLEQ(suc(A_1_360), suc(B_10_359)) | ~E(0, f(B_13_358)) | ~E(0, f(A_1_360)) | ~E(0, f(suc(A_1_360))) | ~iLEQ(suc(B_10_359), suc(B_13_358)) | ~E(0, f(suc(B_10_359))) | ~E(0, f(B_10_359)) | LE(f(B_10_359), 0))), inference(resolution, [status(thm)], [c_231, c_234])).
% 14.74/4.61 tff(c_296, plain, (![B_13_365, B_10_366]: (E(f(B_13_365), f(suc(B_13_365))) | E(f(B_10_366), f(suc(B_10_366))) | ~E(0, f(suc(B_13_365))) | ~E(0, f(B_13_365)) | ~iLEQ(suc(B_10_366), suc(B_13_365)) | ~E(0, f(suc(B_10_366))) | ~E(0, f(B_10_366)) | LE(f(B_10_366), 0))), inference(resolution, [status(thm)], [c_231, c_276])).
% 14.74/4.61 tff(c_305, plain, (![B_10_278]: (E(f(B_10_278), f(suc(B_10_278))) | ~E(0, f(suc(B_10_278))) | ~E(0, f(B_10_278)) | LE(f(B_10_278), 0))), inference(resolution, [status(thm)], [c_231, c_296])).
% 14.74/4.61 tff(c_989, plain, (![B_13_615, B_12_616, B_11_617, A_1_618]: (E(f(B_13_615), f(suc(suc(B_13_615)))) | E(f(B_12_616), f(suc(suc(B_12_616)))) | E(f(B_11_617), f(suc(suc(B_11_617)))) | E(f(A_1_618), f(suc(suc(A_1_618)))) | ~iLEQ(suc(B_11_617), suc(B_12_616)) | ~E(f(B_13_615), f(suc(B_13_615))) | ~E(0, f(suc(suc(B_13_615)))) | ~E(0, f(B_12_616)) | ~E(0, f(suc(B_13_615))) | ~iLEQ(suc(A_1_618), suc(B_11_617)) | ~E(f(B_11_617), f(suc(B_11_617))) | ~E(f(A_1_618), f(suc(A_1_618))) | ~E(0, f(suc(suc(B_12_616)))) | ~E(f(B_12_616), f(suc(B_12_616))) | ~E(0, f(suc(B_12_616))) | ~E(0, f(B_13_615)) | ~E(0, f(A_1_618)) | ~E(0, f(B_11_617)) | ~E(0, f(suc(suc(A_1_618)))) | ~E(0, f(suc(A_1_618))) | ~E(0, f(suc(suc(B_11_617)))) | ~iLEQ(suc(B_12_616), suc(B_13_615)) | ~E(0, f(suc(B_11_617))))), inference(cnfTransformation, [status(thm)], [f_3992])).
% 14.74/4.61 tff(c_999, plain, (![B_13_619, B_10_620, A_1_621]: (E(f(B_13_619), f(suc(suc(B_13_619)))) | E(f(B_10_620), f(suc(suc(B_10_620)))) | E(f(A_1_621), f(suc(suc(A_1_621)))) | ~E(f(B_13_619), f(suc(B_13_619))) | ~E(0, f(suc(suc(B_13_619)))) | ~E(0, f(suc(B_13_619))) | ~iLEQ(suc(A_1_621), suc(B_10_620)) | ~E(f(A_1_621), f(suc(A_1_621))) | ~E(f(B_10_620), f(suc(B_10_620))) | ~E(0, f(B_13_619)) | ~E(0, f(A_1_621)) | ~E(0, f(suc(suc(A_1_621)))) | ~E(0, f(suc(A_1_621))) | ~E(0, f(suc(suc(B_10_620)))) | ~iLEQ(suc(B_10_620), suc(B_13_619)) | ~E(0, f(suc(B_10_620))) | ~E(0, f(B_10_620)) | LE(f(B_10_620), 0))), inference(resolution, [status(thm)], [c_231, c_989])).
% 14.74/4.61 tff(c_1019, plain, (![B_13_626, B_10_627]: (E(f(B_13_626), f(suc(suc(B_13_626)))) | E(f(B_10_627), f(suc(suc(B_10_627)))) | ~E(f(B_13_626), f(suc(B_13_626))) | ~E(0, f(suc(suc(B_13_626)))) | ~E(0, f(suc(B_13_626))) | ~E(f(B_10_627), f(suc(B_10_627))) | ~E(0, f(B_13_626)) | ~E(0, f(suc(suc(B_10_627)))) | ~iLEQ(suc(B_10_627), suc(B_13_626)) | ~E(0, f(suc(B_10_627))) | ~E(0, f(B_10_627)) | LE(f(B_10_627), 0))), inference(resolution, [status(thm)], [c_231, c_999])).
% 14.74/4.61 tff(c_1028, plain, (![B_10_278]: (E(f(B_10_278), f(suc(suc(B_10_278)))) | ~E(f(B_10_278), f(suc(B_10_278))) | ~E(0, f(suc(suc(B_10_278)))) | ~E(0, f(suc(B_10_278))) | ~E(0, f(B_10_278)) | LE(f(B_10_278), 0))), inference(resolution, [status(thm)], [c_231, c_1019])).
% 14.74/4.61 tff(c_1614, plain, (![B_11_821, B_12_822, B_13_823, A_1_824]: (~iLEQ(suc(B_11_821), suc(B_12_822)) | ~E(0, f(suc(suc(suc(B_12_822))))) | ~E(f(B_13_823), f(suc(B_13_823))) | ~E(0, f(suc(suc(B_13_823)))) | ~E(0, f(suc(suc(suc(B_13_823))))) | ~E(0, f(B_12_822)) | ~E(0, f(suc(B_13_823))) | ~iLEQ(suc(A_1_824), suc(B_11_821)) | ~E(f(B_11_821), f(suc(B_11_821))) | ~E(f(A_1_824), f(suc(A_1_824))) | ~E(0, f(suc(suc(B_12_822)))) | ~E(f(B_12_822), f(suc(B_12_822))) | ~E(f(A_1_824), f(suc(suc(A_1_824)))) | ~E(f(B_12_822), f(suc(suc(B_12_822)))) | ~E(f(B_13_823), f(suc(suc(B_13_823)))) | ~E(0, f(suc(B_12_822))) | ~E(f(B_11_821), f(suc(suc(B_11_821)))) | ~E(0, f(B_13_823)) | ~E(0, f(A_1_824)) | ~E(0, f(B_11_821)) | ~E(0, f(suc(suc(A_1_824)))) | ~E(0, f(suc(A_1_824))) | ~E(0, f(suc(suc(B_11_821)))) | ~iLEQ(suc(B_12_822), suc(B_13_823)) | ~E(0, f(suc(suc(suc(B_11_821))))) | ~E(0, f(suc(B_11_821))) | ~E(0, f(suc(suc(suc(A_1_824))))))), inference(cnfTransformation, [status(thm)], [f_3284])).
% 14.74/4.61 tff(c_1768, plain, (![B_13_857, A_1_858, B_10_859]: (~E(f(B_13_857), f(suc(B_13_857))) | ~E(0, f(suc(suc(B_13_857)))) | ~E(0, f(suc(suc(suc(B_13_857))))) | ~E(0, f(suc(B_13_857))) | ~iLEQ(suc(A_1_858), suc(B_10_859)) | ~E(f(A_1_858), f(suc(A_1_858))) | ~E(f(B_10_859), f(suc(B_10_859))) | ~E(f(A_1_858), f(suc(suc(A_1_858)))) | ~E(f(B_13_857), f(suc(suc(B_13_857)))) | ~E(f(B_10_859), f(suc(suc(B_10_859)))) | ~E(0, f(B_13_857)) | ~E(0, f(A_1_858)) | ~E(0, f(suc(suc(A_1_858)))) | ~E(0, f(suc(A_1_858))) | ~E(0, f(suc(suc(B_10_859)))) | ~iLEQ(suc(B_10_859), suc(B_13_857)) | ~E(0, f(suc(suc(suc(B_10_859))))) | ~E(0, f(suc(suc(suc(A_1_858))))) | ~E(0, f(suc(B_10_859))) | ~E(0, f(B_10_859)) | LE(f(B_10_859), 0))), inference(resolution, [status(thm)], [c_231, c_1614])).
% 14.74/4.61 tff(c_1825, plain, (![B_13_869, B_10_870]: (~E(f(B_13_869), f(suc(B_13_869))) | ~E(0, f(suc(suc(B_13_869)))) | ~E(0, f(suc(suc(suc(B_13_869))))) | ~E(0, f(suc(B_13_869))) | ~E(f(B_10_870), f(suc(B_10_870))) | ~E(f(B_13_869), f(suc(suc(B_13_869)))) | ~E(f(B_10_870), f(suc(suc(B_10_870)))) | ~E(0, f(B_13_869)) | ~E(0, f(suc(suc(B_10_870)))) | ~iLEQ(suc(B_10_870), suc(B_13_869)) | ~E(0, f(suc(suc(suc(B_10_870))))) | ~E(0, f(suc(B_10_870))) | ~E(0, f(B_10_870)) | LE(f(B_10_870), 0))), inference(resolution, [status(thm)], [c_231, c_1768])).
% 14.74/4.61 tff(c_1838, plain, (![B_10_871, B_10_872]: (~E(0, f(suc(suc(suc(B_10_871))))) | ~E(f(B_10_872), f(suc(B_10_872))) | ~E(f(B_10_872), f(suc(suc(B_10_872)))) | ~E(0, f(suc(suc(B_10_872)))) | ~iLEQ(suc(B_10_872), suc(B_10_871)) | ~E(0, f(suc(suc(suc(B_10_872))))) | ~E(0, f(suc(B_10_872))) | ~E(0, f(B_10_872)) | LE(f(B_10_872), 0) | ~E(f(B_10_871), f(suc(B_10_871))) | ~E(0, f(suc(suc(B_10_871)))) | ~E(0, f(suc(B_10_871))) | ~E(0, f(B_10_871)) | LE(f(B_10_871), 0))), inference(resolution, [status(thm)], [c_1028, c_1825])).
% 14.74/4.61 tff(c_1850, plain, (![B_10_873, B_10_874]: (~E(f(B_10_873), f(suc(B_10_873))) | ~E(f(B_10_873), f(suc(suc(B_10_873)))) | ~E(0, f(suc(suc(B_10_873)))) | ~iLEQ(suc(B_10_873), suc(B_10_874)) | ~E(0, f(suc(suc(suc(B_10_873))))) | ~E(0, f(suc(B_10_873))) | ~E(0, f(B_10_873)) | LE(f(B_10_873), 0) | ~E(f(B_10_874), f(suc(B_10_874))) | ~E(0, f(suc(suc(B_10_874)))) | ~E(0, f(suc(B_10_874))) | ~E(0, f(B_10_874)) | LE(f(B_10_874), 0))), inference(resolution, [status(thm)], [c_186, c_1838])).
% 14.74/4.61 tff(c_1863, plain, (![B_10_875, B_10_876]: (~iLEQ(suc(B_10_875), suc(B_10_876)) | ~E(0, f(suc(suc(suc(B_10_875))))) | ~E(f(B_10_876), f(suc(B_10_876))) | ~E(0, f(suc(suc(B_10_876)))) | ~E(0, f(suc(B_10_876))) | ~E(0, f(B_10_876)) | LE(f(B_10_876), 0) | ~E(f(B_10_875), f(suc(B_10_875))) | ~E(0, f(suc(suc(B_10_875)))) | ~E(0, f(suc(B_10_875))) | ~E(0, f(B_10_875)) | LE(f(B_10_875), 0))), inference(resolution, [status(thm)], [c_1028, c_1850])).
% 14.74/4.61 tff(c_1873, plain, (![B_10_877]: (~E(0, f(suc(suc(suc(B_10_877))))) | ~E(f(B_10_877), f(suc(B_10_877))) | ~E(0, f(suc(suc(B_10_877)))) | ~E(0, f(suc(B_10_877))) | ~E(0, f(B_10_877)) | LE(f(B_10_877), 0))), inference(resolution, [status(thm)], [c_231, c_1863])).
% 14.74/4.61 tff(c_1885, plain, (![B_10_878]: (~E(f(B_10_878), f(suc(B_10_878))) | ~E(0, f(suc(suc(B_10_878)))) | ~E(0, f(suc(B_10_878))) | ~E(0, f(B_10_878)) | LE(f(B_10_878), 0))), inference(resolution, [status(thm)], [c_186, c_1873])).
% 14.74/4.61 tff(c_1902, plain, (![B_10_879]: (~E(0, f(suc(suc(B_10_879)))) | ~E(0, f(suc(B_10_879))) | ~E(0, f(B_10_879)) | LE(f(B_10_879), 0))), inference(resolution, [status(thm)], [c_305, c_1885])).
% 14.74/4.61 tff(c_1915, plain, (![B_10_880]: (~E(0, f(suc(B_10_880))) | ~E(0, f(B_10_880)) | LE(f(B_10_880), 0))), inference(resolution, [status(thm)], [c_188, c_1902])).
% 14.74/4.61 tff(c_1928, plain, (![B_10_881]: (~E(0, f(B_10_881)) | LE(f(B_10_881), 0))), inference(resolution, [status(thm)], [c_184, c_1915])).
% 14.74/4.61 tff(c_1931, plain, (~E(0, f(z))), inference(resolution, [status(thm)], [c_1928, c_42])).
% 14.74/4.61 tff(c_1935, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_194, c_1931])).
% 14.74/4.61 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------