%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO657-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 : n029.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 7.09s 2.73s
% Output : CNFRefutation 7.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO657-1 : TPTP v9.0.0. Released v7.3.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.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % 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:41:34 EDT 2025
% 0.12/0.34 % CPUTime :
% 7.09/2.73 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.09/2.74
% 7.09/2.74 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.09/2.75 %$ iLEQ > LE > E > #nlpp > suc > s > f > z > 0
% 7.09/2.75
% 7.09/2.75 %Foreground sorts:
% 7.09/2.75
% 7.09/2.75
% 7.09/2.75 %Background operators:
% 7.09/2.75
% 7.09/2.75
% 7.09/2.75 %Foreground operators:
% 7.09/2.75 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 7.09/2.75 tff(s, type, s: $i > $i).
% 7.09/2.75 tff(f, type, f: $i > $i).
% 7.09/2.75 tff(0, type, 0: $i).
% 7.09/2.75 tff(LE, type, LE: ($i * $i) > $o).
% 7.09/2.75 tff(suc, type, suc: $i > $i).
% 7.09/2.75 tff(z, type, z: $i).
% 7.09/2.75 tff(E, type, E: ($i * $i) > $o).
% 7.09/2.75
% 7.48/2.78 tff(f_51, axiom, (![A]: LE(f(A), s(s(0)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_114, axiom, (![B_2]: ((~LE(f(B_2), s(s(0))) | E(s(0), f(B_2))) | LE(f(B_2), s(0)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_121, axiom, (![B_5]: ((~LE(f(B_5), s(0)) | E(0, f(B_5))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 7.48/2.78 tff(f_218, axiom, (![B_2]: ((~LE(f(suc(B_2)), s(s(0))) | E(s(0), f(suc(B_2)))) | LE(f(B_2), s(0)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_49, axiom, (![B_2]: ((~LE(f(suc(suc(B_2))), s(s(0))) | E(s(0), f(suc(suc(B_2))))) | LE(f(B_2), s(0)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_61, axiom, (![A_1]: (((~E(s(0), f(A_1)) | ~E(s(0), f(suc(A_1)))) | E(f(A_1), f(suc(A_1)))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_251, axiom, (![A_1]: ((((~E(s(0), f(suc(suc(A_1)))) | ~E(s(0), f(suc(A_1)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(s(0), f(A_1))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_237, axiom, (![A_1, B_3]: ((((((~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(A_1))) | ~E(s(0), f(suc(A_1)))) | ~E(s(0), f(suc(B_3)))) | ~E(s(0), f(B_3))) | E(f(A_1), f(suc(A_1)))) | E(f(B_3), f(suc(B_3))))), file('unknown', unknown)).
% 7.48/2.78 tff(f_301, axiom, (![A_1, B_3]: ((((((((~iLEQ(suc(A_1), suc(B_3)) | ~E(s(0), f(suc(suc(A_1))))) | ~E(s(0), f(A_1))) | ~E(s(0), f(suc(suc(B_3))))) | ~E(s(0), f(suc(A_1)))) | ~E(s(0), f(suc(B_3)))) | ~E(s(0), f(B_3))) | ~E(f(B_3), f(suc(B_3)))) | ~E(f(A_1), f(suc(A_1))))), file('unknown', unknown)).
% 7.48/2.78 tff(f_211, axiom, ~LE(f(z), 0), file('unknown', unknown)).
% 7.48/2.78 tff(f_202, axiom, (![B_5]: ((~LE(f(suc(B_5)), s(0)) | E(0, f(suc(B_5)))) | LE(f(B_5), 0))), file('unknown', unknown)).
% 7.48/2.78 tff(f_209, 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)).
% 7.48/2.78 tff(f_168, axiom, (![A_2]: (((~E(0, f(A_2)) | ~E(0, f(suc(A_2)))) | E(f(A_2), f(suc(A_2)))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_135, axiom, (![A_2]: ((((~E(0, f(suc(suc(A_2)))) | ~E(0, f(suc(A_2)))) | ~E(f(A_2), f(suc(A_2)))) | ~E(0, f(A_2))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 7.48/2.78 tff(f_42, axiom, (![A_2, B_6]: ((((((~E(0, f(suc(A_2))) | ~E(0, f(A_2))) | ~iLEQ(suc(A_2), suc(B_6))) | ~E(0, f(B_6))) | ~E(0, f(suc(B_6)))) | E(f(A_2), f(suc(A_2)))) | E(f(B_6), f(suc(B_6))))), file('unknown', unknown)).
% 7.48/2.78 tff(f_195, axiom, (![A_2, B_6]: ((((((((~E(0, f(suc(A_2))) | ~E(0, f(suc(suc(B_6))))) | ~E(0, f(suc(suc(A_2))))) | ~E(0, f(A_2))) | ~iLEQ(suc(A_2), suc(B_6))) | ~E(0, f(B_6))) | ~E(f(A_2), f(suc(A_2)))) | ~E(f(B_6), f(suc(B_6)))) | ~E(0, f(suc(B_6))))), file('unknown', unknown)).
% 7.48/2.78 tff(c_6, plain, (![A_4]: (LE(f(A_4), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_51])).
% 7.48/2.78 tff(c_14, plain, (![B_2_10]: (LE(f(B_2_10), s(0)) | E(s(0), f(B_2_10)) | ~LE(f(B_2_10), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_114])).
% 7.48/2.78 tff(c_42, plain, (![B_2_10]: (LE(f(B_2_10), s(0)) | E(s(0), f(B_2_10)))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_14])).
% 7.48/2.78 tff(c_51, plain, (![B_5_32]: (LE(f(B_5_32), 0) | E(0, f(B_5_32)) | ~LE(f(B_5_32), s(0)))), inference(cnfTransformation, [status(thm)], [f_121])).
% 7.48/2.78 tff(c_55, plain, (![B_2_10]: (LE(f(B_2_10), 0) | E(0, f(B_2_10)) | E(s(0), f(B_2_10)))), inference(resolution, [status(thm)], [c_42, c_51])).
% 7.48/2.78 tff(c_32, plain, (![B_2_20]: (LE(f(B_2_20), s(0)) | E(s(0), f(suc(B_2_20))) | ~LE(f(suc(B_2_20)), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_218])).
% 7.48/2.78 tff(c_44, plain, (![B_2_20]: (LE(f(B_2_20), s(0)) | E(s(0), f(suc(B_2_20))))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_32])).
% 7.48/2.78 tff(c_4, plain, (![B_2_3]: (LE(f(B_2_3), s(0)) | E(s(0), f(suc(suc(B_2_3)))) | ~LE(f(suc(suc(B_2_3))), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_49])).
% 7.48/2.78 tff(c_46, plain, (![B_2_3]: (LE(f(B_2_3), s(0)) | E(s(0), f(suc(suc(B_2_3)))))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_4])).
% 7.48/2.78 tff(c_70, plain, (![A_1_39]: (iLEQ(suc(A_1_39), suc(A_1_39)) | E(f(A_1_39), f(suc(A_1_39))) | ~E(s(0), f(suc(A_1_39))) | ~E(s(0), f(A_1_39)))), inference(cnfTransformation, [status(thm)], [f_61])).
% 7.48/2.78 tff(c_86, plain, (![B_2_20]: (iLEQ(suc(B_2_20), suc(B_2_20)) | E(f(B_2_20), f(suc(B_2_20))) | ~E(s(0), f(B_2_20)) | LE(f(B_2_20), s(0)))), inference(resolution, [status(thm)], [c_44, c_70])).
% 7.48/2.78 tff(c_105, plain, (![A_1_46]: (iLEQ(suc(A_1_46), suc(A_1_46)) | ~E(s(0), f(A_1_46)) | ~E(f(A_1_46), f(suc(A_1_46))) | ~E(s(0), f(suc(A_1_46))) | ~E(s(0), f(suc(suc(A_1_46)))))), inference(cnfTransformation, [status(thm)], [f_251])).
% 7.48/2.78 tff(c_121, plain, (![B_2_47]: (~E(s(0), f(suc(B_2_47))) | ~E(s(0), f(suc(suc(B_2_47)))) | iLEQ(suc(B_2_47), suc(B_2_47)) | ~E(s(0), f(B_2_47)) | LE(f(B_2_47), s(0)))), inference(resolution, [status(thm)], [c_86, c_105])).
% 7.48/2.78 tff(c_140, plain, (![B_2_48]: (~E(s(0), f(suc(B_2_48))) | iLEQ(suc(B_2_48), suc(B_2_48)) | ~E(s(0), f(B_2_48)) | LE(f(B_2_48), s(0)))), inference(resolution, [status(thm)], [c_46, c_121])).
% 7.48/2.78 tff(c_156, plain, (![B_2_20]: (iLEQ(suc(B_2_20), suc(B_2_20)) | ~E(s(0), f(B_2_20)) | LE(f(B_2_20), s(0)))), inference(resolution, [status(thm)], [c_44, c_140])).
% 7.48/2.78 tff(c_166, plain, (![B_3_53, A_1_54]: (E(f(B_3_53), f(suc(B_3_53))) | E(f(A_1_54), f(suc(A_1_54))) | ~E(s(0), f(B_3_53)) | ~E(s(0), f(suc(B_3_53))) | ~E(s(0), f(suc(A_1_54))) | ~E(s(0), f(A_1_54)) | ~iLEQ(suc(A_1_54), suc(B_3_53)))), inference(cnfTransformation, [status(thm)], [f_237])).
% 7.48/2.78 tff(c_531, plain, (![B_2_85, A_1_86]: (E(f(B_2_85), f(suc(B_2_85))) | E(f(A_1_86), f(suc(A_1_86))) | ~E(s(0), f(B_2_85)) | ~E(s(0), f(suc(A_1_86))) | ~E(s(0), f(A_1_86)) | ~iLEQ(suc(A_1_86), suc(B_2_85)) | LE(f(B_2_85), s(0)))), inference(resolution, [status(thm)], [c_44, c_166])).
% 7.48/2.78 tff(c_603, plain, (![B_2_90, B_2_91]: (E(f(B_2_90), f(suc(B_2_90))) | E(f(B_2_91), f(suc(B_2_91))) | ~E(s(0), f(B_2_90)) | ~E(s(0), f(B_2_91)) | ~iLEQ(suc(B_2_91), suc(B_2_90)) | LE(f(B_2_90), s(0)) | LE(f(B_2_91), s(0)))), inference(resolution, [status(thm)], [c_44, c_531])).
% 7.48/2.78 tff(c_618, plain, (![B_2_20]: (E(f(B_2_20), f(suc(B_2_20))) | ~E(s(0), f(B_2_20)) | LE(f(B_2_20), s(0)))), inference(resolution, [status(thm)], [c_156, c_603])).
% 7.48/2.78 tff(c_639, plain, (![B_2_94]: (E(f(B_2_94), f(suc(B_2_94))) | ~E(s(0), f(B_2_94)) | LE(f(B_2_94), s(0)))), inference(resolution, [status(thm)], [c_156, c_603])).
% 7.48/2.78 tff(c_40, plain, (![A_1_26, B_3_27]: (~E(f(A_1_26), f(suc(A_1_26))) | ~E(f(B_3_27), f(suc(B_3_27))) | ~E(s(0), f(B_3_27)) | ~E(s(0), f(suc(B_3_27))) | ~E(s(0), f(suc(A_1_26))) | ~E(s(0), f(suc(suc(B_3_27)))) | ~E(s(0), f(A_1_26)) | ~E(s(0), f(suc(suc(A_1_26)))) | ~iLEQ(suc(A_1_26), suc(B_3_27)))), inference(cnfTransformation, [status(thm)], [f_301])).
% 7.48/2.78 tff(c_1837, plain, (![B_3_168, B_2_169]: (~E(f(B_3_168), f(suc(B_3_168))) | ~E(s(0), f(B_3_168)) | ~E(s(0), f(suc(B_3_168))) | ~E(s(0), f(suc(B_2_169))) | ~E(s(0), f(suc(suc(B_3_168)))) | ~E(s(0), f(suc(suc(B_2_169)))) | ~iLEQ(suc(B_2_169), suc(B_3_168)) | ~E(s(0), f(B_2_169)) | LE(f(B_2_169), s(0)))), inference(resolution, [status(thm)], [c_639, c_40])).
% 7.48/2.78 tff(c_1886, plain, (![B_2_170, B_2_171]: (~E(s(0), f(suc(B_2_170))) | ~E(s(0), f(suc(B_2_171))) | ~E(s(0), f(suc(suc(B_2_170)))) | ~E(s(0), f(suc(suc(B_2_171)))) | ~iLEQ(suc(B_2_171), suc(B_2_170)) | ~E(s(0), f(B_2_171)) | LE(f(B_2_171), s(0)) | ~E(s(0), f(B_2_170)) | LE(f(B_2_170), s(0)))), inference(resolution, [status(thm)], [c_618, c_1837])).
% 7.48/2.78 tff(c_1905, plain, (![B_2_172, B_2_173]: (~E(s(0), f(suc(B_2_172))) | ~E(s(0), f(suc(B_2_173))) | ~E(s(0), f(suc(suc(B_2_173)))) | ~iLEQ(suc(B_2_173), suc(B_2_172)) | ~E(s(0), f(B_2_173)) | LE(f(B_2_173), s(0)) | ~E(s(0), f(B_2_172)) | LE(f(B_2_172), s(0)))), inference(resolution, [status(thm)], [c_46, c_1886])).
% 7.48/2.78 tff(c_1922, plain, (![B_2_174, B_2_175]: (~E(s(0), f(suc(B_2_174))) | ~E(s(0), f(suc(suc(B_2_174)))) | ~iLEQ(suc(B_2_174), suc(B_2_175)) | ~E(s(0), f(B_2_174)) | LE(f(B_2_174), s(0)) | ~E(s(0), f(B_2_175)) | LE(f(B_2_175), s(0)))), inference(resolution, [status(thm)], [c_44, c_1905])).
% 7.48/2.78 tff(c_1941, plain, (![B_2_176, B_2_177]: (~E(s(0), f(suc(B_2_176))) | ~iLEQ(suc(B_2_176), suc(B_2_177)) | ~E(s(0), f(B_2_176)) | ~E(s(0), f(B_2_177)) | LE(f(B_2_177), s(0)) | LE(f(B_2_176), s(0)))), inference(resolution, [status(thm)], [c_46, c_1922])).
% 7.48/2.78 tff(c_1958, plain, (![B_2_178, B_2_179]: (~iLEQ(suc(B_2_178), suc(B_2_179)) | ~E(s(0), f(B_2_178)) | ~E(s(0), f(B_2_179)) | LE(f(B_2_179), s(0)) | LE(f(B_2_178), s(0)))), inference(resolution, [status(thm)], [c_44, c_1941])).
% 7.48/2.78 tff(c_2056, plain, (![B_2_182]: (~E(s(0), f(B_2_182)) | LE(f(B_2_182), s(0)))), inference(resolution, [status(thm)], [c_156, c_1958])).
% 7.48/2.78 tff(c_16, plain, (![B_5_11]: (LE(f(B_5_11), 0) | E(0, f(B_5_11)) | ~LE(f(B_5_11), s(0)))), inference(cnfTransformation, [status(thm)], [f_121])).
% 7.48/2.78 tff(c_2069, plain, (![B_2_183]: (LE(f(B_2_183), 0) | E(0, f(B_2_183)) | ~E(s(0), f(B_2_183)))), inference(resolution, [status(thm)], [c_2056, c_16])).
% 7.48/2.78 tff(c_2090, plain, (![B_2_184]: (LE(f(B_2_184), 0) | E(0, f(B_2_184)))), inference(resolution, [status(thm)], [c_55, c_2069])).
% 7.48/2.78 tff(c_30, plain, (~LE(f(z), 0)), inference(cnfTransformation, [status(thm)], [f_211])).
% 7.48/2.78 tff(c_2094, plain, (E(0, f(z))), inference(resolution, [status(thm)], [c_2090, c_30])).
% 7.48/2.78 tff(c_57, plain, (![B_5_34]: (LE(f(B_5_34), 0) | E(0, f(suc(B_5_34))) | ~LE(f(suc(B_5_34)), s(0)))), inference(cnfTransformation, [status(thm)], [f_202])).
% 7.48/2.78 tff(c_61, plain, (![B_5_34]: (LE(f(B_5_34), 0) | E(0, f(suc(B_5_34))) | E(s(0), f(suc(B_5_34))))), inference(resolution, [status(thm)], [c_42, c_57])).
% 7.48/2.78 tff(c_26, plain, (![B_5_18]: (LE(f(B_5_18), 0) | E(0, f(suc(B_5_18))) | ~LE(f(suc(B_5_18)), s(0)))), inference(cnfTransformation, [status(thm)], [f_202])).
% 7.48/2.78 tff(c_2095, plain, (![B_5_185]: (LE(f(B_5_185), 0) | E(0, f(suc(B_5_185))) | ~E(s(0), f(suc(B_5_185))))), inference(resolution, [status(thm)], [c_2056, c_26])).
% 7.48/2.78 tff(c_2109, plain, (![B_5_34]: (LE(f(B_5_34), 0) | E(0, f(suc(B_5_34))))), inference(resolution, [status(thm)], [c_61, c_2095])).
% 7.48/2.78 tff(c_63, plain, (![B_5_36]: (LE(f(B_5_36), 0) | E(0, f(suc(suc(B_5_36)))) | ~LE(f(suc(suc(B_5_36))), s(0)))), inference(cnfTransformation, [status(thm)], [f_209])).
% 7.48/2.78 tff(c_67, plain, (![B_5_36]: (LE(f(B_5_36), 0) | E(0, f(suc(suc(B_5_36)))) | E(s(0), f(suc(suc(B_5_36)))))), inference(resolution, [status(thm)], [c_42, c_63])).
% 7.48/2.78 tff(c_28, plain, (![B_5_19]: (LE(f(B_5_19), 0) | E(0, f(suc(suc(B_5_19)))) | ~LE(f(suc(suc(B_5_19))), s(0)))), inference(cnfTransformation, [status(thm)], [f_209])).
% 7.48/2.78 tff(c_2117, plain, (![B_5_187]: (LE(f(B_5_187), 0) | E(0, f(suc(suc(B_5_187)))) | ~E(s(0), f(suc(suc(B_5_187)))))), inference(resolution, [status(thm)], [c_2056, c_28])).
% 7.48/2.78 tff(c_2127, plain, (![B_5_36]: (LE(f(B_5_36), 0) | E(0, f(suc(suc(B_5_36)))))), inference(resolution, [status(thm)], [c_67, c_2117])).
% 7.48/2.78 tff(c_2130, plain, (![B_5_188]: (LE(f(B_5_188), 0) | E(0, f(suc(suc(B_5_188)))))), inference(resolution, [status(thm)], [c_67, c_2117])).
% 7.48/2.78 tff(c_22, plain, (![A_2_15]: (iLEQ(suc(A_2_15), suc(A_2_15)) | E(f(A_2_15), f(suc(A_2_15))) | ~E(0, f(suc(A_2_15))) | ~E(0, f(A_2_15)))), inference(cnfTransformation, [status(thm)], [f_168])).
% 7.48/2.78 tff(c_89, plain, (![A_2_42]: (iLEQ(suc(A_2_42), suc(A_2_42)) | ~E(0, f(A_2_42)) | ~E(f(A_2_42), f(suc(A_2_42))) | ~E(0, f(suc(A_2_42))) | ~E(0, f(suc(suc(A_2_42)))))), inference(cnfTransformation, [status(thm)], [f_135])).
% 7.48/2.78 tff(c_101, plain, (![A_2_15]: (~E(0, f(suc(suc(A_2_15)))) | iLEQ(suc(A_2_15), suc(A_2_15)) | ~E(0, f(suc(A_2_15))) | ~E(0, f(A_2_15)))), inference(resolution, [status(thm)], [c_22, c_89])).
% 7.48/2.78 tff(c_2133, plain, (![B_5_188]: (iLEQ(suc(B_5_188), suc(B_5_188)) | ~E(0, f(suc(B_5_188))) | ~E(0, f(B_5_188)) | LE(f(B_5_188), 0))), inference(resolution, [status(thm)], [c_2130, c_101])).
% 7.48/2.78 tff(c_2134, plain, (![B_5_189]: (iLEQ(suc(B_5_189), suc(B_5_189)) | ~E(0, f(suc(B_5_189))) | ~E(0, f(B_5_189)) | LE(f(B_5_189), 0))), inference(resolution, [status(thm)], [c_2130, c_101])).
% 7.48/2.78 tff(c_2, plain, (![B_6_2, A_2_1]: (E(f(B_6_2), f(suc(B_6_2))) | E(f(A_2_1), f(suc(A_2_1))) | ~E(0, f(suc(B_6_2))) | ~E(0, f(B_6_2)) | ~iLEQ(suc(A_2_1), suc(B_6_2)) | ~E(0, f(A_2_1)) | ~E(0, f(suc(A_2_1))))), inference(cnfTransformation, [status(thm)], [f_42])).
% 7.48/2.78 tff(c_2145, plain, (![B_5_189]: (E(f(B_5_189), f(suc(B_5_189))) | ~E(0, f(suc(B_5_189))) | ~E(0, f(B_5_189)) | LE(f(B_5_189), 0))), inference(resolution, [status(thm)], [c_2134, c_2])).
% 7.48/2.78 tff(c_2158, plain, (![B_5_191]: (E(f(B_5_191), f(suc(B_5_191))) | ~E(0, f(suc(B_5_191))) | ~E(0, f(B_5_191)) | LE(f(B_5_191), 0))), inference(resolution, [status(thm)], [c_2134, c_2])).
% 7.48/2.78 tff(c_24, plain, (![B_6_17, A_2_16]: (~E(0, f(suc(B_6_17))) | ~E(f(B_6_17), f(suc(B_6_17))) | ~E(f(A_2_16), f(suc(A_2_16))) | ~E(0, f(B_6_17)) | ~iLEQ(suc(A_2_16), suc(B_6_17)) | ~E(0, f(A_2_16)) | ~E(0, f(suc(suc(A_2_16)))) | ~E(0, f(suc(suc(B_6_17)))) | ~E(0, f(suc(A_2_16))))), inference(cnfTransformation, [status(thm)], [f_195])).
% 7.48/2.78 tff(c_2249, plain, (![A_2_203, B_5_204]: (~E(f(A_2_203), f(suc(A_2_203))) | ~iLEQ(suc(A_2_203), suc(B_5_204)) | ~E(0, f(A_2_203)) | ~E(0, f(suc(suc(A_2_203)))) | ~E(0, f(suc(suc(B_5_204)))) | ~E(0, f(suc(A_2_203))) | ~E(0, f(suc(B_5_204))) | ~E(0, f(B_5_204)) | LE(f(B_5_204), 0))), inference(resolution, [status(thm)], [c_2158, c_24])).
% 7.48/2.78 tff(c_2275, plain, (![B_5_207, B_5_208]: (~iLEQ(suc(B_5_207), suc(B_5_208)) | ~E(0, f(suc(suc(B_5_207)))) | ~E(0, f(suc(suc(B_5_208)))) | ~E(0, f(suc(B_5_208))) | ~E(0, f(B_5_208)) | LE(f(B_5_208), 0) | ~E(0, f(suc(B_5_207))) | ~E(0, f(B_5_207)) | LE(f(B_5_207), 0))), inference(resolution, [status(thm)], [c_2145, c_2249])).
% 7.48/2.78 tff(c_2282, plain, (![B_5_209]: (~E(0, f(suc(suc(B_5_209)))) | ~E(0, f(suc(B_5_209))) | ~E(0, f(B_5_209)) | LE(f(B_5_209), 0))), inference(resolution, [status(thm)], [c_2133, c_2275])).
% 7.48/2.78 tff(c_2291, plain, (![B_5_210]: (~E(0, f(suc(B_5_210))) | ~E(0, f(B_5_210)) | LE(f(B_5_210), 0))), inference(resolution, [status(thm)], [c_2127, c_2282])).
% 7.48/2.78 tff(c_2300, plain, (![B_5_211]: (~E(0, f(B_5_211)) | LE(f(B_5_211), 0))), inference(resolution, [status(thm)], [c_2109, c_2291])).
% 7.48/2.78 tff(c_2303, plain, (~E(0, f(z))), inference(resolution, [status(thm)], [c_2300, c_30])).
% 7.48/2.78 tff(c_2307, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_2094, c_2303])).
% 7.48/2.78 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------