%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO669-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 : 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 10:38:05 PM UTC 2025
% Result : Unsatisfiable 45.45s 34.82s
% Output : CNFRefutation 45.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO669-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.34 % Computer : n010.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:42:49 EDT 2025
% 0.12/0.34 % CPUTime :
% 45.45/34.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 45.64/34.84
% 45.64/34.84 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 45.64/34.85 %$ iLEQ > LE > E > #nlpp > suc > s > f > z > 0
% 45.64/34.85
% 45.64/34.85 %Foreground sorts:
% 45.64/34.85
% 45.64/34.85
% 45.64/34.85 %Background operators:
% 45.64/34.85
% 45.64/34.85
% 45.64/34.85 %Foreground operators:
% 45.64/34.85 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 45.64/34.85 tff(s, type, s: $i > $i).
% 45.64/34.85 tff(f, type, f: $i > $i).
% 45.64/34.85 tff(0, type, 0: $i).
% 45.64/34.85 tff(LE, type, LE: ($i * $i) > $o).
% 45.64/34.85 tff(suc, type, suc: $i > $i).
% 45.64/34.85 tff(z, type, z: $i).
% 45.64/34.85 tff(E, type, E: ($i * $i) > $o).
% 45.64/34.85
% 45.64/34.88 tff(f_246, axiom, (![A]: LE(f(A), s(s(s(0))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_801, axiom, (![B_3]: ((~LE(f(B_3), s(s(s(0)))) | E(s(s(0)), f(B_3))) | LE(f(B_3), s(s(0))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_682, axiom, (![B_7]: ((~LE(f(B_7), s(s(0))) | E(s(0), f(B_7))) | LE(f(B_7), s(0)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_636, axiom, (![B_3]: ((~LE(f(suc(B_3)), s(s(s(0)))) | E(s(s(0)), f(suc(B_3)))) | LE(f(B_3), s(s(0))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_256, axiom, (![A_1]: (((~E(s(s(0)), f(A_1)) | ~E(s(s(0)), f(suc(A_1)))) | E(f(A_1), f(suc(A_1)))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_118, axiom, (![B_3]: ((~LE(f(suc(suc(B_3))), s(s(s(0)))) | E(s(s(0)), f(suc(suc(B_3))))) | LE(f(B_3), s(s(0))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_76, axiom, (![A_1]: (((((~E(s(s(0)), f(suc(suc(A_1)))) | ~E(s(s(0)), f(suc(A_1)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(s(s(0)), f(A_1))) | E(f(A_1), f(suc(suc(A_1))))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_60, axiom, (![B_3]: ((~LE(f(suc(suc(suc(B_3)))), s(s(s(0)))) | E(s(s(0)), f(suc(suc(suc(B_3)))))) | LE(f(B_3), s(s(0))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_215, axiom, (![A_1]: ((((((~E(s(s(0)), f(A_1)) | ~E(s(s(0)), f(suc(A_1)))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~E(s(s(0)), f(suc(suc(suc(A_1)))))) | ~E(f(A_1), f(suc(A_1)))) | ~E(s(s(0)), f(suc(suc(A_1))))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_701, axiom, (![A_1, B_4]: ((((((~E(s(s(0)), f(A_1)) | ~E(s(s(0)), f(suc(A_1)))) | ~iLEQ(suc(A_1), suc(B_4))) | ~E(s(s(0)), f(suc(B_4)))) | ~E(s(s(0)), f(B_4))) | E(f(A_1), f(suc(A_1)))) | E(f(B_4), f(suc(B_4))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_917, axiom, (![A_1, B_4]: ((((((((((~E(s(s(0)), f(A_1)) | ~E(f(B_4), f(suc(B_4)))) | ~E(s(s(0)), f(suc(A_1)))) | ~iLEQ(suc(A_1), suc(B_4))) | ~E(s(s(0)), f(suc(suc(B_4))))) | ~E(s(s(0)), f(suc(B_4)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(s(s(0)), f(suc(suc(A_1))))) | ~E(s(s(0)), f(B_4))) | E(f(A_1), f(suc(suc(A_1))))) | E(f(B_4), f(suc(suc(B_4)))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_675, axiom, (![A_1, B_4]: ((((((((((((~E(s(s(0)), f(A_1)) | ~E(f(B_4), f(suc(B_4)))) | ~E(s(s(0)), f(suc(A_1)))) | ~E(f(B_4), f(suc(suc(B_4))))) | ~iLEQ(suc(A_1), suc(B_4))) | ~E(s(s(0)), f(suc(suc(B_4))))) | ~E(f(A_1), f(suc(suc(A_1))))) | ~E(s(s(0)), f(suc(suc(suc(A_1)))))) | ~E(s(s(0)), f(suc(B_4)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(s(s(0)), f(suc(suc(suc(B_4)))))) | ~E(s(s(0)), f(suc(suc(A_1))))) | ~E(s(s(0)), f(B_4)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_157, axiom, (![B_10]: ((~LE(f(B_10), s(0)) | E(0, f(B_10))) | LE(f(B_10), 0))), file('unknown', unknown)).
% 45.64/34.88 tff(f_164, axiom, (![B_7]: ((~LE(f(suc(B_7)), s(s(0))) | E(s(0), f(suc(B_7)))) | LE(f(B_7), s(0)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_581, axiom, (![A_2]: (((~E(s(0), f(A_2)) | ~E(s(0), f(suc(A_2)))) | E(f(A_2), f(suc(A_2)))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_737, axiom, (![B_7]: ((~LE(f(suc(suc(B_7))), s(s(0))) | E(s(0), f(suc(suc(B_7))))) | LE(f(B_7), s(0)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_794, axiom, (![A_2]: (((((~E(s(0), f(suc(suc(A_2)))) | ~E(s(0), f(suc(A_2)))) | ~E(f(A_2), f(suc(A_2)))) | ~E(s(0), f(A_2))) | E(f(A_2), f(suc(suc(A_2))))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_980, axiom, (![B_7]: ((~LE(f(suc(suc(suc(B_7)))), s(s(0))) | E(s(0), f(suc(suc(suc(B_7)))))) | LE(f(B_7), s(0)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_53, axiom, (![A_2]: ((((((~E(f(A_2), f(suc(suc(A_2)))) | ~E(s(0), f(suc(A_2)))) | ~E(s(0), f(suc(suc(A_2))))) | ~E(s(0), f(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(A_2)))) | ~E(s(0), f(A_2))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_455, axiom, (![A_2, B_8]: ((((((~E(s(0), f(suc(A_2))) | ~E(s(0), f(B_8))) | ~E(s(0), f(suc(B_8)))) | ~E(s(0), f(A_2))) | ~iLEQ(suc(A_2), suc(B_8))) | E(f(A_2), f(suc(A_2)))) | E(f(B_8), f(suc(B_8))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_368, axiom, (![A_2, B_8]: ((((((((((~E(s(0), f(suc(A_2))) | ~E(s(0), f(B_8))) | ~E(s(0), f(suc(suc(B_8))))) | ~E(s(0), f(suc(B_8)))) | ~E(s(0), f(suc(suc(A_2))))) | ~E(f(B_8), f(suc(B_8)))) | ~E(f(A_2), f(suc(A_2)))) | ~E(s(0), f(A_2))) | ~iLEQ(suc(A_2), suc(B_8))) | E(f(A_2), f(suc(suc(A_2))))) | E(f(B_8), f(suc(suc(B_8)))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_407, axiom, (![A_2, B_8]: ((((((((((((~E(f(A_2), f(suc(suc(A_2)))) | ~E(s(0), f(suc(A_2)))) | ~E(s(0), f(B_8))) | ~E(s(0), f(suc(suc(B_8))))) | ~E(f(B_8), f(suc(suc(B_8))))) | ~E(s(0), f(suc(B_8)))) | ~E(s(0), f(suc(suc(A_2))))) | ~E(f(B_8), f(suc(B_8)))) | ~E(s(0), f(suc(suc(suc(B_8)))))) | ~E(s(0), f(suc(suc(suc(A_2)))))) | ~E(f(A_2), f(suc(A_2)))) | ~E(s(0), f(A_2))) | ~iLEQ(suc(A_2), suc(B_8)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_919, axiom, ~LE(f(z), 0), file('unknown', unknown)).
% 45.64/34.88 tff(f_292, axiom, (![B_10]: ((~LE(f(suc(B_10)), s(0)) | E(0, f(suc(B_10)))) | LE(f(B_10), 0))), file('unknown', unknown)).
% 45.64/34.88 tff(f_462, 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)).
% 45.64/34.88 tff(f_33, axiom, (![A_3]: (((~E(0, f(A_3)) | ~E(0, f(suc(A_3)))) | E(f(A_3), f(suc(A_3)))) | iLEQ(suc(A_3), suc(A_3)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_125, 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)).
% 45.64/34.88 tff(f_753, axiom, (![A_3]: (((((~E(0, f(suc(suc(A_3)))) | ~E(0, f(suc(A_3)))) | ~E(f(A_3), f(suc(A_3)))) | ~E(0, f(A_3))) | E(f(A_3), f(suc(suc(A_3))))) | iLEQ(suc(A_3), suc(A_3)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_312, axiom, (![A_3]: ((((((~E(f(A_3), f(suc(suc(A_3)))) | ~E(0, f(suc(suc(suc(A_3)))))) | ~E(0, f(A_3))) | ~E(0, f(suc(suc(A_3))))) | ~E(0, f(suc(A_3)))) | ~E(f(A_3), f(suc(A_3)))) | iLEQ(suc(A_3), suc(A_3)))), file('unknown', unknown)).
% 45.64/34.88 tff(f_629, axiom, (![B_11, A_3]: ((((((~E(0, f(suc(B_11))) | ~E(0, f(B_11))) | ~E(0, f(A_3))) | ~E(0, f(suc(A_3)))) | ~iLEQ(suc(A_3), suc(B_11))) | E(f(A_3), f(suc(A_3)))) | E(f(B_11), f(suc(B_11))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_195, axiom, (![B_11, A_3]: ((((((((((~E(0, f(suc(B_11))) | ~E(0, f(suc(suc(B_11))))) | ~E(0, f(B_11))) | ~E(0, f(A_3))) | ~E(0, f(suc(suc(A_3))))) | ~E(0, f(suc(A_3)))) | ~E(f(A_3), f(suc(A_3)))) | ~iLEQ(suc(A_3), suc(B_11))) | ~E(f(B_11), f(suc(B_11)))) | E(f(A_3), f(suc(suc(A_3))))) | E(f(B_11), f(suc(suc(B_11)))))), file('unknown', unknown)).
% 45.64/34.88 tff(f_501, axiom, (![B_11, A_3]: ((((((((((((~E(0, f(suc(B_11))) | ~E(0, f(suc(suc(suc(B_11)))))) | ~E(0, f(suc(suc(B_11))))) | ~E(0, f(B_11))) | ~E(f(A_3), f(suc(suc(A_3))))) | ~E(f(B_11), f(suc(suc(B_11))))) | ~E(0, f(suc(suc(suc(A_3)))))) | ~E(0, f(A_3))) | ~E(0, f(suc(suc(A_3))))) | ~E(0, f(suc(A_3)))) | ~E(f(A_3), f(suc(A_3)))) | ~iLEQ(suc(A_3), suc(B_11))) | ~E(f(B_11), f(suc(B_11))))), file('unknown', unknown)).
% 45.64/34.88 tff(c_28, plain, (![A_18]: (LE(f(A_18), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_246])).
% 45.64/34.88 tff(c_80, plain, (![B_3_59]: (LE(f(B_3_59), s(s(0))) | E(s(s(0)), f(B_3_59)) | ~LE(f(B_3_59), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_801])).
% 45.64/34.88 tff(c_104, plain, (![B_3_59]: (LE(f(B_3_59), s(s(0))) | E(s(s(0)), f(B_3_59)))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_80])).
% 45.64/34.88 tff(c_116, plain, (![B_7_84]: (LE(f(B_7_84), s(0)) | E(s(0), f(B_7_84)) | ~LE(f(B_7_84), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_682])).
% 45.64/34.88 tff(c_120, plain, (![B_3_59]: (LE(f(B_3_59), s(0)) | E(s(0), f(B_3_59)) | E(s(s(0)), f(B_3_59)))), inference(resolution, [status(thm)], [c_104, c_116])).
% 45.64/34.88 tff(c_62, plain, (![B_3_46]: (LE(f(B_3_46), s(s(0))) | E(s(s(0)), f(suc(B_3_46))) | ~LE(f(suc(B_3_46)), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_636])).
% 45.64/34.88 tff(c_102, plain, (![B_3_46]: (LE(f(B_3_46), s(s(0))) | E(s(s(0)), f(suc(B_3_46))))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_62])).
% 45.64/34.88 tff(c_143, plain, (![A_1_95]: (iLEQ(suc(A_1_95), suc(A_1_95)) | E(f(A_1_95), f(suc(A_1_95))) | ~E(s(s(0)), f(suc(A_1_95))) | ~E(s(s(0)), f(A_1_95)))), inference(cnfTransformation, [status(thm)], [f_256])).
% 45.64/34.88 tff(c_162, plain, (![B_3_46]: (iLEQ(suc(B_3_46), suc(B_3_46)) | E(f(B_3_46), f(suc(B_3_46))) | ~E(s(s(0)), f(B_3_46)) | LE(f(B_3_46), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_143])).
% 45.64/34.88 tff(c_12, plain, (![B_3_7]: (LE(f(B_3_7), s(s(0))) | E(s(s(0)), f(suc(suc(B_3_7)))) | ~LE(f(suc(suc(B_3_7))), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_118])).
% 45.64/34.88 tff(c_106, plain, (![B_3_7]: (LE(f(B_3_7), s(s(0))) | E(s(s(0)), f(suc(suc(B_3_7)))))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_12])).
% 45.64/34.88 tff(c_283, plain, (![A_1_114]: (iLEQ(suc(A_1_114), suc(A_1_114)) | E(f(A_1_114), f(suc(suc(A_1_114)))) | ~E(s(s(0)), f(A_1_114)) | ~E(f(A_1_114), f(suc(A_1_114))) | ~E(s(s(0)), f(suc(A_1_114))) | ~E(s(s(0)), f(suc(suc(A_1_114)))))), inference(cnfTransformation, [status(thm)], [f_76])).
% 45.64/34.88 tff(c_308, plain, (![B_3_115]: (iLEQ(suc(B_3_115), suc(B_3_115)) | E(f(B_3_115), f(suc(suc(B_3_115)))) | ~E(s(s(0)), f(B_3_115)) | ~E(f(B_3_115), f(suc(B_3_115))) | ~E(s(s(0)), f(suc(B_3_115))) | LE(f(B_3_115), s(s(0))))), inference(resolution, [status(thm)], [c_106, c_283])).
% 45.64/34.88 tff(c_330, plain, (![B_3_46]: (iLEQ(suc(B_3_46), suc(B_3_46)) | E(f(B_3_46), f(suc(suc(B_3_46)))) | ~E(s(s(0)), f(B_3_46)) | ~E(f(B_3_46), f(suc(B_3_46))) | LE(f(B_3_46), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_308])).
% 45.64/34.88 tff(c_6, plain, (![B_3_3]: (LE(f(B_3_3), s(s(0))) | E(s(s(0)), f(suc(suc(suc(B_3_3))))) | ~LE(f(suc(suc(suc(B_3_3)))), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_60])).
% 45.64/34.88 tff(c_108, plain, (![B_3_3]: (LE(f(B_3_3), s(s(0))) | E(s(s(0)), f(suc(suc(suc(B_3_3))))))), inference(demodulation, [status(thm), theory('equality')], [c_28, c_6])).
% 45.64/34.88 tff(c_433, plain, (![A_1_132]: (iLEQ(suc(A_1_132), suc(A_1_132)) | ~E(s(s(0)), f(suc(suc(A_1_132)))) | ~E(f(A_1_132), f(suc(A_1_132))) | ~E(s(s(0)), f(suc(suc(suc(A_1_132))))) | ~E(f(A_1_132), f(suc(suc(A_1_132)))) | ~E(s(s(0)), f(suc(A_1_132))) | ~E(s(s(0)), f(A_1_132)))), inference(cnfTransformation, [status(thm)], [f_215])).
% 45.64/34.88 tff(c_510, plain, (![B_3_140]: (iLEQ(suc(B_3_140), suc(B_3_140)) | ~E(s(s(0)), f(suc(suc(B_3_140)))) | ~E(f(B_3_140), f(suc(B_3_140))) | ~E(f(B_3_140), f(suc(suc(B_3_140)))) | ~E(s(s(0)), f(suc(B_3_140))) | ~E(s(s(0)), f(B_3_140)) | LE(f(B_3_140), s(s(0))))), inference(resolution, [status(thm)], [c_108, c_433])).
% 45.64/34.88 tff(c_536, plain, (![B_3_143]: (iLEQ(suc(B_3_143), suc(B_3_143)) | ~E(f(B_3_143), f(suc(B_3_143))) | ~E(f(B_3_143), f(suc(suc(B_3_143)))) | ~E(s(s(0)), f(suc(B_3_143))) | ~E(s(s(0)), f(B_3_143)) | LE(f(B_3_143), s(s(0))))), inference(resolution, [status(thm)], [c_106, c_510])).
% 45.64/34.88 tff(c_555, plain, (![B_3_144]: (~E(s(s(0)), f(suc(B_3_144))) | iLEQ(suc(B_3_144), suc(B_3_144)) | ~E(s(s(0)), f(B_3_144)) | ~E(f(B_3_144), f(suc(B_3_144))) | LE(f(B_3_144), s(s(0))))), inference(resolution, [status(thm)], [c_330, c_536])).
% 45.64/34.88 tff(c_578, plain, (![B_3_145]: (iLEQ(suc(B_3_145), suc(B_3_145)) | ~E(s(s(0)), f(B_3_145)) | ~E(f(B_3_145), f(suc(B_3_145))) | LE(f(B_3_145), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_555])).
% 45.64/34.88 tff(c_618, plain, (![B_3_146]: (iLEQ(suc(B_3_146), suc(B_3_146)) | ~E(s(s(0)), f(B_3_146)) | LE(f(B_3_146), s(s(0))))), inference(resolution, [status(thm)], [c_162, c_578])).
% 45.64/34.88 tff(c_360, plain, (![B_4_123, A_1_124]: (E(f(B_4_123), f(suc(B_4_123))) | E(f(A_1_124), f(suc(A_1_124))) | ~E(s(s(0)), f(B_4_123)) | ~E(s(s(0)), f(suc(B_4_123))) | ~iLEQ(suc(A_1_124), suc(B_4_123)) | ~E(s(s(0)), f(suc(A_1_124))) | ~E(s(s(0)), f(A_1_124)))), inference(cnfTransformation, [status(thm)], [f_701])).
% 45.64/34.88 tff(c_382, plain, (![B_3_46, A_1_124]: (E(f(B_3_46), f(suc(B_3_46))) | E(f(A_1_124), f(suc(A_1_124))) | ~E(s(s(0)), f(B_3_46)) | ~iLEQ(suc(A_1_124), suc(B_3_46)) | ~E(s(s(0)), f(suc(A_1_124))) | ~E(s(s(0)), f(A_1_124)) | LE(f(B_3_46), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_360])).
% 45.64/34.88 tff(c_686, plain, (![B_3_151]: (E(f(B_3_151), f(suc(B_3_151))) | ~E(s(s(0)), f(suc(B_3_151))) | ~E(s(s(0)), f(B_3_151)) | LE(f(B_3_151), s(s(0))))), inference(resolution, [status(thm)], [c_618, c_382])).
% 45.64/34.88 tff(c_708, plain, (![B_3_46]: (E(f(B_3_46), f(suc(B_3_46))) | ~E(s(s(0)), f(B_3_46)) | LE(f(B_3_46), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_686])).
% 45.64/34.88 tff(c_616, plain, (![B_3_46]: (iLEQ(suc(B_3_46), suc(B_3_46)) | ~E(s(s(0)), f(B_3_46)) | LE(f(B_3_46), s(s(0))))), inference(resolution, [status(thm)], [c_162, c_578])).
% 45.64/34.88 tff(c_955, plain, (![B_4_189, A_1_190]: (E(f(B_4_189), f(suc(suc(B_4_189)))) | E(f(A_1_190), f(suc(suc(A_1_190)))) | ~E(s(s(0)), f(B_4_189)) | ~E(s(s(0)), f(suc(suc(A_1_190)))) | ~E(f(A_1_190), f(suc(A_1_190))) | ~E(s(s(0)), f(suc(B_4_189))) | ~E(s(s(0)), f(suc(suc(B_4_189)))) | ~iLEQ(suc(A_1_190), suc(B_4_189)) | ~E(s(s(0)), f(suc(A_1_190))) | ~E(f(B_4_189), f(suc(B_4_189))) | ~E(s(s(0)), f(A_1_190)))), inference(cnfTransformation, [status(thm)], [f_917])).
% 45.64/34.88 tff(c_3807, plain, (![B_4_306, B_3_307]: (E(f(B_4_306), f(suc(suc(B_4_306)))) | E(f(B_3_307), f(suc(suc(B_3_307)))) | ~E(s(s(0)), f(B_4_306)) | ~E(f(B_3_307), f(suc(B_3_307))) | ~E(s(s(0)), f(suc(B_4_306))) | ~E(s(s(0)), f(suc(suc(B_4_306)))) | ~iLEQ(suc(B_3_307), suc(B_4_306)) | ~E(s(s(0)), f(suc(B_3_307))) | ~E(f(B_4_306), f(suc(B_4_306))) | ~E(s(s(0)), f(B_3_307)) | LE(f(B_3_307), s(s(0))))), inference(resolution, [status(thm)], [c_106, c_955])).
% 45.64/34.88 tff(c_18294, plain, (![B_3_603, B_3_604]: (E(f(B_3_603), f(suc(suc(B_3_603)))) | E(f(B_3_604), f(suc(suc(B_3_604)))) | ~E(s(s(0)), f(B_3_603)) | ~E(f(B_3_604), f(suc(B_3_604))) | ~E(s(s(0)), f(suc(B_3_603))) | ~iLEQ(suc(B_3_604), suc(B_3_603)) | ~E(s(s(0)), f(suc(B_3_604))) | ~E(f(B_3_603), f(suc(B_3_603))) | ~E(s(s(0)), f(B_3_604)) | LE(f(B_3_604), s(s(0))) | LE(f(B_3_603), s(s(0))))), inference(resolution, [status(thm)], [c_106, c_3807])).
% 45.64/34.88 tff(c_18317, plain, (![B_3_605, B_3_606]: (E(f(B_3_605), f(suc(suc(B_3_605)))) | E(f(B_3_606), f(suc(suc(B_3_606)))) | ~E(s(s(0)), f(B_3_605)) | ~E(f(B_3_606), f(suc(B_3_606))) | ~iLEQ(suc(B_3_606), suc(B_3_605)) | ~E(s(s(0)), f(suc(B_3_606))) | ~E(f(B_3_605), f(suc(B_3_605))) | ~E(s(s(0)), f(B_3_606)) | LE(f(B_3_606), s(s(0))) | LE(f(B_3_605), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_18294])).
% 45.64/34.88 tff(c_18507, plain, (![B_3_607]: (E(f(B_3_607), f(suc(suc(B_3_607)))) | ~E(s(s(0)), f(suc(B_3_607))) | ~E(f(B_3_607), f(suc(B_3_607))) | ~E(s(s(0)), f(B_3_607)) | LE(f(B_3_607), s(s(0))))), inference(resolution, [status(thm)], [c_616, c_18317])).
% 45.64/34.88 tff(c_18529, plain, (![B_3_46]: (E(f(B_3_46), f(suc(suc(B_3_46)))) | ~E(f(B_3_46), f(suc(B_3_46))) | ~E(s(s(0)), f(B_3_46)) | LE(f(B_3_46), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_18507])).
% 45.64/34.88 tff(c_1973, plain, (![B_4_225, A_1_226]: (~E(s(s(0)), f(B_4_225)) | ~E(s(s(0)), f(suc(suc(A_1_226)))) | ~E(s(s(0)), f(suc(suc(suc(B_4_225))))) | ~E(f(A_1_226), f(suc(A_1_226))) | ~E(s(s(0)), f(suc(B_4_225))) | ~E(s(s(0)), f(suc(suc(suc(A_1_226))))) | ~E(f(A_1_226), f(suc(suc(A_1_226)))) | ~E(s(s(0)), f(suc(suc(B_4_225)))) | ~iLEQ(suc(A_1_226), suc(B_4_225)) | ~E(f(B_4_225), f(suc(suc(B_4_225)))) | ~E(s(s(0)), f(suc(A_1_226))) | ~E(f(B_4_225), f(suc(B_4_225))) | ~E(s(s(0)), f(A_1_226)))), inference(cnfTransformation, [status(thm)], [f_675])).
% 45.64/34.88 tff(c_5995, plain, (![B_3_374, A_1_375]: (~E(s(s(0)), f(B_3_374)) | ~E(s(s(0)), f(suc(suc(A_1_375)))) | ~E(f(A_1_375), f(suc(A_1_375))) | ~E(s(s(0)), f(suc(B_3_374))) | ~E(s(s(0)), f(suc(suc(suc(A_1_375))))) | ~E(f(A_1_375), f(suc(suc(A_1_375)))) | ~E(s(s(0)), f(suc(suc(B_3_374)))) | ~iLEQ(suc(A_1_375), suc(B_3_374)) | ~E(f(B_3_374), f(suc(suc(B_3_374)))) | ~E(s(s(0)), f(suc(A_1_375))) | ~E(f(B_3_374), f(suc(B_3_374))) | ~E(s(s(0)), f(A_1_375)) | LE(f(B_3_374), s(s(0))))), inference(resolution, [status(thm)], [c_108, c_1973])).
% 45.64/34.88 tff(c_53615, plain, (![B_3_1037, B_3_1038]: (~E(s(s(0)), f(B_3_1037)) | ~E(s(s(0)), f(suc(suc(B_3_1038)))) | ~E(f(B_3_1038), f(suc(B_3_1038))) | ~E(s(s(0)), f(suc(B_3_1037))) | ~E(f(B_3_1038), f(suc(suc(B_3_1038)))) | ~E(s(s(0)), f(suc(suc(B_3_1037)))) | ~iLEQ(suc(B_3_1038), suc(B_3_1037)) | ~E(f(B_3_1037), f(suc(suc(B_3_1037)))) | ~E(s(s(0)), f(suc(B_3_1038))) | ~E(f(B_3_1037), f(suc(B_3_1037))) | ~E(s(s(0)), f(B_3_1038)) | LE(f(B_3_1037), s(s(0))) | LE(f(B_3_1038), s(s(0))))), inference(resolution, [status(thm)], [c_108, c_5995])).
% 45.64/34.88 tff(c_64297, plain, (![B_3_1132, B_3_1133]: (~E(s(s(0)), f(B_3_1132)) | ~E(f(B_3_1133), f(suc(B_3_1133))) | ~E(s(s(0)), f(suc(B_3_1132))) | ~E(f(B_3_1133), f(suc(suc(B_3_1133)))) | ~E(s(s(0)), f(suc(suc(B_3_1132)))) | ~iLEQ(suc(B_3_1133), suc(B_3_1132)) | ~E(f(B_3_1132), f(suc(suc(B_3_1132)))) | ~E(s(s(0)), f(suc(B_3_1133))) | ~E(f(B_3_1132), f(suc(B_3_1132))) | ~E(s(s(0)), f(B_3_1133)) | LE(f(B_3_1132), s(s(0))) | LE(f(B_3_1133), s(s(0))))), inference(resolution, [status(thm)], [c_106, c_53615])).
% 45.64/34.88 tff(c_64526, plain, (![B_3_1134, B_3_1135]: (~E(s(s(0)), f(B_3_1134)) | ~E(s(s(0)), f(suc(B_3_1134))) | ~E(s(s(0)), f(suc(suc(B_3_1134)))) | ~iLEQ(suc(B_3_1135), suc(B_3_1134)) | ~E(f(B_3_1134), f(suc(suc(B_3_1134)))) | ~E(s(s(0)), f(suc(B_3_1135))) | ~E(f(B_3_1134), f(suc(B_3_1134))) | LE(f(B_3_1134), s(s(0))) | ~E(f(B_3_1135), f(suc(B_3_1135))) | ~E(s(s(0)), f(B_3_1135)) | LE(f(B_3_1135), s(s(0))))), inference(resolution, [status(thm)], [c_18529, c_64297])).
% 45.64/34.88 tff(c_64551, plain, (![B_3_1136, B_3_1137]: (~E(s(s(0)), f(B_3_1136)) | ~E(s(s(0)), f(suc(B_3_1136))) | ~iLEQ(suc(B_3_1137), suc(B_3_1136)) | ~E(f(B_3_1136), f(suc(suc(B_3_1136)))) | ~E(s(s(0)), f(suc(B_3_1137))) | ~E(f(B_3_1136), f(suc(B_3_1136))) | ~E(f(B_3_1137), f(suc(B_3_1137))) | ~E(s(s(0)), f(B_3_1137)) | LE(f(B_3_1137), s(s(0))) | LE(f(B_3_1136), s(s(0))))), inference(resolution, [status(thm)], [c_106, c_64526])).
% 45.64/34.88 tff(c_64574, plain, (![B_3_1138, B_3_1139]: (~E(s(s(0)), f(B_3_1138)) | ~iLEQ(suc(B_3_1139), suc(B_3_1138)) | ~E(f(B_3_1138), f(suc(suc(B_3_1138)))) | ~E(s(s(0)), f(suc(B_3_1139))) | ~E(f(B_3_1138), f(suc(B_3_1138))) | ~E(f(B_3_1139), f(suc(B_3_1139))) | ~E(s(s(0)), f(B_3_1139)) | LE(f(B_3_1139), s(s(0))) | LE(f(B_3_1138), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_64551])).
% 45.64/34.88 tff(c_64885, plain, (![B_3_1142]: (~E(f(B_3_1142), f(suc(suc(B_3_1142)))) | ~E(s(s(0)), f(suc(B_3_1142))) | ~E(f(B_3_1142), f(suc(B_3_1142))) | ~E(s(s(0)), f(B_3_1142)) | LE(f(B_3_1142), s(s(0))))), inference(resolution, [status(thm)], [c_616, c_64574])).
% 45.64/34.88 tff(c_65114, plain, (![B_3_1143]: (~E(s(s(0)), f(suc(B_3_1143))) | ~E(f(B_3_1143), f(suc(B_3_1143))) | ~E(s(s(0)), f(B_3_1143)) | LE(f(B_3_1143), s(s(0))))), inference(resolution, [status(thm)], [c_18529, c_64885])).
% 45.64/34.88 tff(c_65137, plain, (![B_3_1144]: (~E(f(B_3_1144), f(suc(B_3_1144))) | ~E(s(s(0)), f(B_3_1144)) | LE(f(B_3_1144), s(s(0))))), inference(resolution, [status(thm)], [c_102, c_65114])).
% 45.64/34.88 tff(c_65447, plain, (![B_3_1145]: (~E(s(s(0)), f(B_3_1145)) | LE(f(B_3_1145), s(s(0))))), inference(resolution, [status(thm)], [c_708, c_65137])).
% 45.64/34.88 tff(c_66, plain, (![B_7_49]: (LE(f(B_7_49), s(0)) | E(s(0), f(B_7_49)) | ~LE(f(B_7_49), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_682])).
% 45.64/34.88 tff(c_65464, plain, (![B_3_1146]: (LE(f(B_3_1146), s(0)) | E(s(0), f(B_3_1146)) | ~E(s(s(0)), f(B_3_1146)))), inference(resolution, [status(thm)], [c_65447, c_66])).
% 45.64/34.88 tff(c_65493, plain, (![B_3_1147]: (LE(f(B_3_1147), s(0)) | E(s(0), f(B_3_1147)))), inference(resolution, [status(thm)], [c_120, c_65464])).
% 45.64/34.88 tff(c_18, plain, (![B_10_11]: (LE(f(B_10_11), 0) | E(0, f(B_10_11)) | ~LE(f(B_10_11), s(0)))), inference(cnfTransformation, [status(thm)], [f_157])).
% 45.64/34.88 tff(c_65509, plain, (![B_3_1147]: (LE(f(B_3_1147), 0) | E(0, f(B_3_1147)) | E(s(0), f(B_3_1147)))), inference(resolution, [status(thm)], [c_65493, c_18])).
% 45.64/34.88 tff(c_123, plain, (![B_7_87]: (LE(f(B_7_87), s(0)) | E(s(0), f(suc(B_7_87))) | ~LE(f(suc(B_7_87)), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_164])).
% 45.64/34.88 tff(c_127, plain, (![B_7_87]: (LE(f(B_7_87), s(0)) | E(s(0), f(suc(B_7_87))) | E(s(s(0)), f(suc(B_7_87))))), inference(resolution, [status(thm)], [c_104, c_123])).
% 45.64/34.88 tff(c_20, plain, (![B_7_12]: (LE(f(B_7_12), s(0)) | E(s(0), f(suc(B_7_12))) | ~LE(f(suc(B_7_12)), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_164])).
% 45.64/34.88 tff(c_65630, plain, (![B_7_1151]: (LE(f(B_7_1151), s(0)) | E(s(0), f(suc(B_7_1151))) | ~E(s(s(0)), f(suc(B_7_1151))))), inference(resolution, [status(thm)], [c_65447, c_20])).
% 45.64/34.88 tff(c_65651, plain, (![B_7_87]: (LE(f(B_7_87), s(0)) | E(s(0), f(suc(B_7_87))))), inference(resolution, [status(thm)], [c_127, c_65630])).
% 45.64/34.88 tff(c_65693, plain, (![B_7_1153]: (LE(f(B_7_1153), s(0)) | E(s(0), f(suc(B_7_1153))))), inference(resolution, [status(thm)], [c_127, c_65630])).
% 45.64/34.88 tff(c_56, plain, (![A_2_41]: (iLEQ(suc(A_2_41), suc(A_2_41)) | E(f(A_2_41), f(suc(A_2_41))) | ~E(s(0), f(suc(A_2_41))) | ~E(s(0), f(A_2_41)))), inference(cnfTransformation, [status(thm)], [f_581])).
% 45.64/34.88 tff(c_65732, plain, (![B_7_1153]: (iLEQ(suc(B_7_1153), suc(B_7_1153)) | E(f(B_7_1153), f(suc(B_7_1153))) | ~E(s(0), f(B_7_1153)) | LE(f(B_7_1153), s(0)))), inference(resolution, [status(thm)], [c_65693, c_56])).
% 45.64/34.88 tff(c_131, plain, (![B_7_91]: (LE(f(B_7_91), s(0)) | E(s(0), f(suc(suc(B_7_91)))) | ~LE(f(suc(suc(B_7_91))), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_737])).
% 45.64/34.88 tff(c_135, plain, (![B_7_91]: (LE(f(B_7_91), s(0)) | E(s(0), f(suc(suc(B_7_91)))) | E(s(s(0)), f(suc(suc(B_7_91)))))), inference(resolution, [status(thm)], [c_104, c_131])).
% 45.64/34.88 tff(c_72, plain, (![B_7_54]: (LE(f(B_7_54), s(0)) | E(s(0), f(suc(suc(B_7_54)))) | ~LE(f(suc(suc(B_7_54))), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_737])).
% 45.64/34.88 tff(c_65733, plain, (![B_7_1154]: (LE(f(B_7_1154), s(0)) | E(s(0), f(suc(suc(B_7_1154)))) | ~E(s(s(0)), f(suc(suc(B_7_1154)))))), inference(resolution, [status(thm)], [c_65447, c_72])).
% 45.64/34.88 tff(c_65754, plain, (![B_7_1155]: (LE(f(B_7_1155), s(0)) | E(s(0), f(suc(suc(B_7_1155)))))), inference(resolution, [status(thm)], [c_135, c_65733])).
% 45.64/34.88 tff(c_78, plain, (![A_2_58]: (iLEQ(suc(A_2_58), suc(A_2_58)) | E(f(A_2_58), f(suc(suc(A_2_58)))) | ~E(s(0), f(A_2_58)) | ~E(f(A_2_58), f(suc(A_2_58))) | ~E(s(0), f(suc(A_2_58))) | ~E(s(0), f(suc(suc(A_2_58)))))), inference(cnfTransformation, [status(thm)], [f_794])).
% 45.64/34.88 tff(c_65791, plain, (![B_7_1155]: (iLEQ(suc(B_7_1155), suc(B_7_1155)) | E(f(B_7_1155), f(suc(suc(B_7_1155)))) | ~E(s(0), f(B_7_1155)) | ~E(f(B_7_1155), f(suc(B_7_1155))) | ~E(s(0), f(suc(B_7_1155))) | LE(f(B_7_1155), s(0)))), inference(resolution, [status(thm)], [c_65754, c_78])).
% 45.64/34.88 tff(c_65750, plain, (![B_7_91]: (LE(f(B_7_91), s(0)) | E(s(0), f(suc(suc(B_7_91)))))), inference(resolution, [status(thm)], [c_135, c_65733])).
% 45.64/34.88 tff(c_137, plain, (![B_7_93]: (LE(f(B_7_93), s(0)) | E(s(0), f(suc(suc(suc(B_7_93))))) | ~LE(f(suc(suc(suc(B_7_93)))), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_980])).
% 45.64/34.88 tff(c_141, plain, (![B_7_93]: (LE(f(B_7_93), s(0)) | E(s(0), f(suc(suc(suc(B_7_93))))) | E(s(s(0)), f(suc(suc(suc(B_7_93))))))), inference(resolution, [status(thm)], [c_104, c_137])).
% 45.64/34.88 tff(c_96, plain, (![B_7_72]: (LE(f(B_7_72), s(0)) | E(s(0), f(suc(suc(suc(B_7_72))))) | ~LE(f(suc(suc(suc(B_7_72)))), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_980])).
% 45.64/34.88 tff(c_65794, plain, (![B_7_1157]: (LE(f(B_7_1157), s(0)) | E(s(0), f(suc(suc(suc(B_7_1157))))) | ~E(s(s(0)), f(suc(suc(suc(B_7_1157))))))), inference(resolution, [status(thm)], [c_65447, c_96])).
% 45.64/34.88 tff(c_65811, plain, (![B_7_1158]: (LE(f(B_7_1158), s(0)) | E(s(0), f(suc(suc(suc(B_7_1158))))))), inference(resolution, [status(thm)], [c_141, c_65794])).
% 45.64/34.88 tff(c_4, plain, (![A_2_2]: (iLEQ(suc(A_2_2), suc(A_2_2)) | ~E(s(0), f(A_2_2)) | ~E(f(A_2_2), f(suc(A_2_2))) | ~E(s(0), f(suc(suc(suc(A_2_2))))) | ~E(s(0), f(suc(suc(A_2_2)))) | ~E(s(0), f(suc(A_2_2))) | ~E(f(A_2_2), f(suc(suc(A_2_2)))))), inference(cnfTransformation, [status(thm)], [f_53])).
% 45.64/34.88 tff(c_65859, plain, (![B_7_1169]: (iLEQ(suc(B_7_1169), suc(B_7_1169)) | ~E(s(0), f(B_7_1169)) | ~E(f(B_7_1169), f(suc(B_7_1169))) | ~E(s(0), f(suc(suc(B_7_1169)))) | ~E(s(0), f(suc(B_7_1169))) | ~E(f(B_7_1169), f(suc(suc(B_7_1169)))) | LE(f(B_7_1169), s(0)))), inference(resolution, [status(thm)], [c_65811, c_4])).
% 45.64/34.88 tff(c_65884, plain, (![B_7_1170]: (iLEQ(suc(B_7_1170), suc(B_7_1170)) | ~E(s(0), f(B_7_1170)) | ~E(f(B_7_1170), f(suc(B_7_1170))) | ~E(s(0), f(suc(B_7_1170))) | ~E(f(B_7_1170), f(suc(suc(B_7_1170)))) | LE(f(B_7_1170), s(0)))), inference(resolution, [status(thm)], [c_65750, c_65859])).
% 45.64/34.88 tff(c_65973, plain, (![B_7_1171]: (iLEQ(suc(B_7_1171), suc(B_7_1171)) | ~E(s(0), f(B_7_1171)) | ~E(f(B_7_1171), f(suc(B_7_1171))) | ~E(s(0), f(suc(B_7_1171))) | LE(f(B_7_1171), s(0)))), inference(resolution, [status(thm)], [c_65791, c_65884])).
% 45.64/34.88 tff(c_66048, plain, (![B_7_1173]: (~E(s(0), f(suc(B_7_1173))) | iLEQ(suc(B_7_1173), suc(B_7_1173)) | ~E(s(0), f(B_7_1173)) | LE(f(B_7_1173), s(0)))), inference(resolution, [status(thm)], [c_65732, c_65973])).
% 45.64/34.88 tff(c_66071, plain, (![B_7_1174]: (iLEQ(suc(B_7_1174), suc(B_7_1174)) | ~E(s(0), f(B_7_1174)) | LE(f(B_7_1174), s(0)))), inference(resolution, [status(thm)], [c_65651, c_66048])).
% 45.64/34.88 tff(c_46, plain, (![B_8_33, A_2_32]: (E(f(B_8_33), f(suc(B_8_33))) | E(f(A_2_32), f(suc(A_2_32))) | ~iLEQ(suc(A_2_32), suc(B_8_33)) | ~E(s(0), f(A_2_32)) | ~E(s(0), f(suc(B_8_33))) | ~E(s(0), f(B_8_33)) | ~E(s(0), f(suc(A_2_32))))), inference(cnfTransformation, [status(thm)], [f_455])).
% 45.64/34.88 tff(c_66150, plain, (![B_7_1175]: (E(f(B_7_1175), f(suc(B_7_1175))) | ~E(s(0), f(suc(B_7_1175))) | ~E(s(0), f(B_7_1175)) | LE(f(B_7_1175), s(0)))), inference(resolution, [status(thm)], [c_66071, c_46])).
% 45.64/34.88 tff(c_66168, plain, (![B_7_87]: (E(f(B_7_87), f(suc(B_7_87))) | ~E(s(0), f(B_7_87)) | LE(f(B_7_87), s(0)))), inference(resolution, [status(thm)], [c_65651, c_66150])).
% 45.64/34.88 tff(c_40, plain, (![B_8_27, A_2_26]: (E(f(B_8_27), f(suc(suc(B_8_27)))) | E(f(A_2_26), f(suc(suc(A_2_26)))) | ~iLEQ(suc(A_2_26), suc(B_8_27)) | ~E(s(0), f(A_2_26)) | ~E(f(A_2_26), f(suc(A_2_26))) | ~E(f(B_8_27), f(suc(B_8_27))) | ~E(s(0), f(suc(suc(A_2_26)))) | ~E(s(0), f(suc(B_8_27))) | ~E(s(0), f(suc(suc(B_8_27)))) | ~E(s(0), f(B_8_27)) | ~E(s(0), f(suc(A_2_26))))), inference(cnfTransformation, [status(thm)], [f_368])).
% 45.64/34.88 tff(c_66174, plain, (![B_7_1177]: (E(f(B_7_1177), f(suc(suc(B_7_1177)))) | ~E(f(B_7_1177), f(suc(B_7_1177))) | ~E(s(0), f(suc(suc(B_7_1177)))) | ~E(s(0), f(suc(B_7_1177))) | ~E(s(0), f(B_7_1177)) | LE(f(B_7_1177), s(0)))), inference(resolution, [status(thm)], [c_66071, c_40])).
% 45.64/34.88 tff(c_66193, plain, (![B_7_91]: (E(f(B_7_91), f(suc(suc(B_7_91)))) | ~E(f(B_7_91), f(suc(B_7_91))) | ~E(s(0), f(suc(B_7_91))) | ~E(s(0), f(B_7_91)) | LE(f(B_7_91), s(0)))), inference(resolution, [status(thm)], [c_65750, c_66174])).
% 45.64/34.88 tff(c_65807, plain, (![B_7_93]: (LE(f(B_7_93), s(0)) | E(s(0), f(suc(suc(suc(B_7_93))))))), inference(resolution, [status(thm)], [c_141, c_65794])).
% 45.64/34.88 tff(c_42, plain, (![A_2_28, B_8_29]: (~iLEQ(suc(A_2_28), suc(B_8_29)) | ~E(s(0), f(A_2_28)) | ~E(f(A_2_28), f(suc(A_2_28))) | ~E(s(0), f(suc(suc(suc(A_2_28))))) | ~E(s(0), f(suc(suc(suc(B_8_29))))) | ~E(f(B_8_29), f(suc(B_8_29))) | ~E(s(0), f(suc(suc(A_2_28)))) | ~E(s(0), f(suc(B_8_29))) | ~E(f(B_8_29), f(suc(suc(B_8_29)))) | ~E(s(0), f(suc(suc(B_8_29)))) | ~E(s(0), f(B_8_29)) | ~E(s(0), f(suc(A_2_28))) | ~E(f(A_2_28), f(suc(suc(A_2_28)))))), inference(cnfTransformation, [status(thm)], [f_407])).
% 45.64/34.88 tff(c_67340, plain, (![B_7_1212]: (~E(s(0), f(suc(suc(suc(B_7_1212))))) | ~E(f(B_7_1212), f(suc(B_7_1212))) | ~E(s(0), f(suc(suc(B_7_1212)))) | ~E(s(0), f(suc(B_7_1212))) | ~E(f(B_7_1212), f(suc(suc(B_7_1212)))) | ~E(s(0), f(B_7_1212)) | LE(f(B_7_1212), s(0)))), inference(resolution, [status(thm)], [c_66071, c_42])).
% 45.64/34.88 tff(c_67371, plain, (![B_7_1214]: (~E(f(B_7_1214), f(suc(B_7_1214))) | ~E(s(0), f(suc(suc(B_7_1214)))) | ~E(s(0), f(suc(B_7_1214))) | ~E(f(B_7_1214), f(suc(suc(B_7_1214)))) | ~E(s(0), f(B_7_1214)) | LE(f(B_7_1214), s(0)))), inference(resolution, [status(thm)], [c_65807, c_67340])).
% 45.64/34.88 tff(c_67396, plain, (![B_7_1215]: (~E(f(B_7_1215), f(suc(B_7_1215))) | ~E(s(0), f(suc(B_7_1215))) | ~E(f(B_7_1215), f(suc(suc(B_7_1215)))) | ~E(s(0), f(B_7_1215)) | LE(f(B_7_1215), s(0)))), inference(resolution, [status(thm)], [c_65750, c_67371])).
% 45.64/34.88 tff(c_67493, plain, (![B_7_1216]: (~E(f(B_7_1216), f(suc(B_7_1216))) | ~E(s(0), f(suc(B_7_1216))) | ~E(s(0), f(B_7_1216)) | LE(f(B_7_1216), s(0)))), inference(resolution, [status(thm)], [c_66193, c_67396])).
% 45.64/34.88 tff(c_67557, plain, (![B_7_1217]: (~E(s(0), f(suc(B_7_1217))) | ~E(s(0), f(B_7_1217)) | LE(f(B_7_1217), s(0)))), inference(resolution, [status(thm)], [c_66168, c_67493])).
% 45.64/34.88 tff(c_67586, plain, (![B_7_1218]: (~E(s(0), f(B_7_1218)) | LE(f(B_7_1218), s(0)))), inference(resolution, [status(thm)], [c_65651, c_67557])).
% 45.64/34.88 tff(c_67603, plain, (![B_7_1219]: (LE(f(B_7_1219), 0) | E(0, f(B_7_1219)) | ~E(s(0), f(B_7_1219)))), inference(resolution, [status(thm)], [c_67586, c_18])).
% 45.64/34.88 tff(c_67632, plain, (![B_3_1220]: (LE(f(B_3_1220), 0) | E(0, f(B_3_1220)))), inference(resolution, [status(thm)], [c_65509, c_67603])).
% 45.64/34.88 tff(c_90, plain, (~LE(f(z), 0)), inference(cnfTransformation, [status(thm)], [f_919])).
% 45.64/34.88 tff(c_67636, plain, (E(0, f(z))), inference(resolution, [status(thm)], [c_67632, c_90])).
% 45.64/34.88 tff(c_34, plain, (![B_10_22]: (LE(f(B_10_22), 0) | E(0, f(suc(B_10_22))) | ~LE(f(suc(B_10_22)), s(0)))), inference(cnfTransformation, [status(thm)], [f_292])).
% 45.64/34.88 tff(c_65508, plain, (![B_10_22]: (LE(f(B_10_22), 0) | E(0, f(suc(B_10_22))) | E(s(0), f(suc(B_10_22))))), inference(resolution, [status(thm)], [c_65493, c_34])).
% 45.64/34.88 tff(c_67637, plain, (![B_10_1221]: (LE(f(B_10_1221), 0) | E(0, f(suc(B_10_1221))) | ~E(s(0), f(suc(B_10_1221))))), inference(resolution, [status(thm)], [c_67586, c_34])).
% 45.64/34.88 tff(c_67661, plain, (![B_10_22]: (LE(f(B_10_22), 0) | E(0, f(suc(B_10_22))))), inference(resolution, [status(thm)], [c_65508, c_67637])).
% 45.64/34.88 tff(c_48, plain, (![B_10_34]: (LE(f(B_10_34), 0) | E(0, f(suc(suc(B_10_34)))) | ~LE(f(suc(suc(B_10_34))), s(0)))), inference(cnfTransformation, [status(thm)], [f_462])).
% 45.64/34.88 tff(c_65507, plain, (![B_10_34]: (LE(f(B_10_34), 0) | E(0, f(suc(suc(B_10_34)))) | E(s(0), f(suc(suc(B_10_34)))))), inference(resolution, [status(thm)], [c_65493, c_48])).
% 45.64/34.88 tff(c_67667, plain, (![B_10_1223]: (LE(f(B_10_1223), 0) | E(0, f(suc(suc(B_10_1223)))) | ~E(s(0), f(suc(suc(B_10_1223)))))), inference(resolution, [status(thm)], [c_67586, c_48])).
% 45.64/34.88 tff(c_67687, plain, (![B_10_34]: (LE(f(B_10_34), 0) | E(0, f(suc(suc(B_10_34)))))), inference(resolution, [status(thm)], [c_65507, c_67667])).
% 45.64/34.88 tff(c_2, plain, (![A_3_1]: (iLEQ(suc(A_3_1), suc(A_3_1)) | E(f(A_3_1), f(suc(A_3_1))) | ~E(0, f(suc(A_3_1))) | ~E(0, f(A_3_1)))), inference(cnfTransformation, [status(thm)], [f_33])).
% 45.64/34.88 tff(c_14, plain, (![B_10_8]: (LE(f(B_10_8), 0) | E(0, f(suc(suc(suc(B_10_8))))) | ~LE(f(suc(suc(suc(B_10_8)))), s(0)))), inference(cnfTransformation, [status(thm)], [f_125])).
% 45.64/34.88 tff(c_65506, plain, (![B_10_8]: (LE(f(B_10_8), 0) | E(0, f(suc(suc(suc(B_10_8))))) | E(s(0), f(suc(suc(suc(B_10_8))))))), inference(resolution, [status(thm)], [c_65493, c_14])).
% 45.64/34.88 tff(c_67693, plain, (![B_10_1225]: (LE(f(B_10_1225), 0) | E(0, f(suc(suc(suc(B_10_1225))))) | ~E(s(0), f(suc(suc(suc(B_10_1225))))))), inference(resolution, [status(thm)], [c_67586, c_14])).
% 45.64/34.88 tff(c_67710, plain, (![B_10_1226]: (LE(f(B_10_1226), 0) | E(0, f(suc(suc(suc(B_10_1226))))))), inference(resolution, [status(thm)], [c_65506, c_67693])).
% 45.64/34.88 tff(c_74, plain, (![A_3_55]: (iLEQ(suc(A_3_55), suc(A_3_55)) | E(f(A_3_55), f(suc(suc(A_3_55)))) | ~E(0, f(A_3_55)) | ~E(f(A_3_55), f(suc(A_3_55))) | ~E(0, f(suc(A_3_55))) | ~E(0, f(suc(suc(A_3_55)))))), inference(cnfTransformation, [status(thm)], [f_753])).
% 45.64/34.88 tff(c_344, plain, (![A_3_119]: (iLEQ(suc(A_3_119), suc(A_3_119)) | ~E(f(A_3_119), f(suc(A_3_119))) | ~E(0, f(suc(A_3_119))) | ~E(0, f(suc(suc(A_3_119)))) | ~E(0, f(A_3_119)) | ~E(0, f(suc(suc(suc(A_3_119))))) | ~E(f(A_3_119), f(suc(suc(A_3_119)))))), inference(cnfTransformation, [status(thm)], [f_312])).
% 45.64/34.88 tff(c_356, plain, (![A_3_55]: (~E(0, f(suc(suc(suc(A_3_55))))) | iLEQ(suc(A_3_55), suc(A_3_55)) | ~E(0, f(A_3_55)) | ~E(f(A_3_55), f(suc(A_3_55))) | ~E(0, f(suc(A_3_55))) | ~E(0, f(suc(suc(A_3_55)))))), inference(resolution, [status(thm)], [c_74, c_344])).
% 45.64/34.88 tff(c_67714, plain, (![B_10_1227]: (iLEQ(suc(B_10_1227), suc(B_10_1227)) | ~E(0, f(B_10_1227)) | ~E(f(B_10_1227), f(suc(B_10_1227))) | ~E(0, f(suc(B_10_1227))) | ~E(0, f(suc(suc(B_10_1227)))) | LE(f(B_10_1227), 0))), inference(resolution, [status(thm)], [c_67710, c_356])).
% 45.64/34.88 tff(c_67735, plain, (![A_3_1228]: (~E(0, f(suc(suc(A_3_1228)))) | LE(f(A_3_1228), 0) | iLEQ(suc(A_3_1228), suc(A_3_1228)) | ~E(0, f(suc(A_3_1228))) | ~E(0, f(A_3_1228)))), inference(resolution, [status(thm)], [c_2, c_67714])).
% 45.64/34.88 tff(c_67746, plain, (![B_10_1229]: (iLEQ(suc(B_10_1229), suc(B_10_1229)) | ~E(0, f(suc(B_10_1229))) | ~E(0, f(B_10_1229)) | LE(f(B_10_1229), 0))), inference(resolution, [status(thm)], [c_67687, c_67735])).
% 45.64/34.88 tff(c_60, plain, (![B_11_44, A_3_45]: (E(f(B_11_44), f(suc(B_11_44))) | E(f(A_3_45), f(suc(A_3_45))) | ~iLEQ(suc(A_3_45), suc(B_11_44)) | ~E(0, f(suc(A_3_45))) | ~E(0, f(A_3_45)) | ~E(0, f(B_11_44)) | ~E(0, f(suc(B_11_44))))), inference(cnfTransformation, [status(thm)], [f_629])).
% 45.64/34.88 tff(c_67824, plain, (![B_10_1229]: (E(f(B_10_1229), f(suc(B_10_1229))) | ~E(0, f(suc(B_10_1229))) | ~E(0, f(B_10_1229)) | LE(f(B_10_1229), 0))), inference(resolution, [status(thm)], [c_67746, c_60])).
% 45.64/34.88 tff(c_67709, plain, (![B_10_8]: (LE(f(B_10_8), 0) | E(0, f(suc(suc(suc(B_10_8))))))), inference(resolution, [status(thm)], [c_65506, c_67693])).
% 45.64/34.88 tff(c_22, plain, (![B_11_13, A_3_14]: (E(f(B_11_13), f(suc(suc(B_11_13)))) | E(f(A_3_14), f(suc(suc(A_3_14)))) | ~E(f(B_11_13), f(suc(B_11_13))) | ~iLEQ(suc(A_3_14), suc(B_11_13)) | ~E(f(A_3_14), f(suc(A_3_14))) | ~E(0, f(suc(A_3_14))) | ~E(0, f(suc(suc(A_3_14)))) | ~E(0, f(A_3_14)) | ~E(0, f(B_11_13)) | ~E(0, f(suc(suc(B_11_13)))) | ~E(0, f(suc(B_11_13))))), inference(cnfTransformation, [status(thm)], [f_195])).
% 45.64/34.88 tff(c_67814, plain, (![B_10_1229]: (E(f(B_10_1229), f(suc(suc(B_10_1229)))) | ~E(f(B_10_1229), f(suc(B_10_1229))) | ~E(0, f(suc(suc(B_10_1229)))) | ~E(0, f(suc(B_10_1229))) | ~E(0, f(B_10_1229)) | LE(f(B_10_1229), 0))), inference(resolution, [status(thm)], [c_67746, c_22])).
% 45.64/34.88 tff(c_50, plain, (![B_11_35, A_3_36]: (~E(f(B_11_35), f(suc(B_11_35))) | ~iLEQ(suc(A_3_36), suc(B_11_35)) | ~E(f(A_3_36), f(suc(A_3_36))) | ~E(0, f(suc(A_3_36))) | ~E(0, f(suc(suc(A_3_36)))) | ~E(0, f(A_3_36)) | ~E(0, f(suc(suc(suc(A_3_36))))) | ~E(f(B_11_35), f(suc(suc(B_11_35)))) | ~E(f(A_3_36), f(suc(suc(A_3_36)))) | ~E(0, f(B_11_35)) | ~E(0, f(suc(suc(B_11_35)))) | ~E(0, f(suc(suc(suc(B_11_35))))) | ~E(0, f(suc(B_11_35))))), inference(cnfTransformation, [status(thm)], [f_501])).
% 45.64/34.88 tff(c_68047, plain, (![B_10_1241]: (~E(f(B_10_1241), f(suc(B_10_1241))) | ~E(f(B_10_1241), f(suc(suc(B_10_1241)))) | ~E(0, f(suc(suc(B_10_1241)))) | ~E(0, f(suc(suc(suc(B_10_1241))))) | ~E(0, f(suc(B_10_1241))) | ~E(0, f(B_10_1241)) | LE(f(B_10_1241), 0))), inference(resolution, [status(thm)], [c_67746, c_50])).
% 45.64/34.88 tff(c_68072, plain, (![B_10_1242]: (~E(0, f(suc(suc(suc(B_10_1242))))) | ~E(f(B_10_1242), f(suc(B_10_1242))) | ~E(0, f(suc(suc(B_10_1242)))) | ~E(0, f(suc(B_10_1242))) | ~E(0, f(B_10_1242)) | LE(f(B_10_1242), 0))), inference(resolution, [status(thm)], [c_67814, c_68047])).
% 45.64/34.88 tff(c_68084, plain, (![B_10_1243]: (~E(f(B_10_1243), f(suc(B_10_1243))) | ~E(0, f(suc(suc(B_10_1243)))) | ~E(0, f(suc(B_10_1243))) | ~E(0, f(B_10_1243)) | LE(f(B_10_1243), 0))), inference(resolution, [status(thm)], [c_67709, c_68072])).
% 45.64/34.88 tff(c_68117, plain, (![B_10_1244]: (~E(0, f(suc(suc(B_10_1244)))) | ~E(0, f(suc(B_10_1244))) | ~E(0, f(B_10_1244)) | LE(f(B_10_1244), 0))), inference(resolution, [status(thm)], [c_67824, c_68084])).
% 45.64/34.88 tff(c_68130, plain, (![B_10_1245]: (~E(0, f(suc(B_10_1245))) | ~E(0, f(B_10_1245)) | LE(f(B_10_1245), 0))), inference(resolution, [status(thm)], [c_67687, c_68117])).
% 45.64/34.88 tff(c_68143, plain, (![B_10_1246]: (~E(0, f(B_10_1246)) | LE(f(B_10_1246), 0))), inference(resolution, [status(thm)], [c_67661, c_68130])).
% 45.64/34.88 tff(c_68146, plain, (~E(0, f(z))), inference(resolution, [status(thm)], [c_68143, c_90])).
% 45.64/34.88 tff(c_68150, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_67636, c_68146])).
% 45.64/34.88 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------