%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO681-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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 10:38:06 PM UTC 2025
% Result : Unsatisfiable 268.15s 251.16s
% Output : CNFRefutation 268.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYO681-1 : TPTP v9.0.0. Released v7.3.0.
% 0.06/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.14/0.34 % Computer : n012.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Apr 9 09:42:29 EDT 2025
% 0.14/0.34 % CPUTime :
% 268.15/251.16 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 268.15/251.19
% 268.15/251.19 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 268.15/251.19 %$ iLEQ > LE > E > #nlpp > suc > s > f > z > 0
% 268.15/251.19
% 268.15/251.19 %Foreground sorts:
% 268.15/251.19
% 268.15/251.19
% 268.15/251.19 %Background operators:
% 268.15/251.19
% 268.15/251.19
% 268.15/251.19 %Foreground operators:
% 268.15/251.19 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 268.15/251.19 tff(s, type, s: $i > $i).
% 268.15/251.19 tff(f, type, f: $i > $i).
% 268.15/251.19 tff(0, type, 0: $i).
% 268.15/251.19 tff(LE, type, LE: ($i * $i) > $o).
% 268.15/251.19 tff(suc, type, suc: $i > $i).
% 268.15/251.19 tff(z, type, z: $i).
% 268.15/251.19 tff(E, type, E: ($i * $i) > $o).
% 268.15/251.19
% 268.43/251.23 tff(f_66, axiom, (![A]: LE(f(A), s(s(s(s(0)))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_30, axiom, (![B_23]: ((~LE(f(B_23), s(s(s(s(0))))) | E(s(s(s(0))), f(B_23))) | LE(f(B_23), s(s(s(0)))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_175, axiom, (![B_41]: ((~LE(f(B_41), s(s(s(0)))) | E(s(s(0)), f(B_41))) | LE(f(B_41), s(s(0))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_1035, axiom, (![B_23]: ((~LE(f(suc(B_23)), s(s(s(s(0))))) | E(s(s(s(0))), f(suc(B_23)))) | LE(f(B_23), s(s(s(0)))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_646, axiom, (![B_23]: ((~LE(f(suc(suc(B_23))), s(s(s(s(0))))) | E(s(s(s(0))), f(suc(suc(B_23))))) | LE(f(B_23), s(s(s(0)))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_734, axiom, (![A_1]: (((~E(s(s(s(0))), f(A_1)) | ~E(s(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)).
% 268.43/251.23 tff(f_831, axiom, (![A_1]: ((((~E(s(s(s(0))), f(suc(suc(A_1)))) | ~E(s(s(s(0))), f(suc(A_1)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(s(s(s(0))), f(A_1))) | iLEQ(suc(A_1), suc(A_1)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_366, axiom, (![B_24, B_25, A_1]: ((((((((((~iLEQ(suc(B_24), suc(B_25)) | ~E(s(s(s(0))), f(B_25))) | ~E(s(s(s(0))), f(B_24))) | ~iLEQ(suc(A_1), suc(B_24))) | ~E(s(s(s(0))), f(A_1))) | ~E(s(s(s(0))), f(suc(B_24)))) | ~E(s(s(s(0))), f(suc(B_25)))) | ~E(s(s(s(0))), f(suc(A_1)))) | E(f(A_1), f(suc(A_1)))) | E(f(B_24), f(suc(B_24)))) | E(f(B_25), f(suc(B_25))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_911, axiom, (![B_24, B_25, A_1]: (((((((((((((~iLEQ(suc(B_24), suc(B_25)) | ~E(s(s(s(0))), f(suc(suc(B_24))))) | ~E(s(s(s(0))), f(B_25))) | ~E(f(B_24), f(suc(B_24)))) | ~E(s(s(s(0))), f(B_24))) | ~iLEQ(suc(A_1), suc(B_24))) | ~E(s(s(s(0))), f(A_1))) | ~E(s(s(s(0))), f(suc(suc(A_1))))) | ~E(f(B_25), f(suc(B_25)))) | ~E(f(A_1), f(suc(A_1)))) | ~E(s(s(s(0))), f(suc(B_24)))) | ~E(s(s(s(0))), f(suc(suc(B_25))))) | ~E(s(s(s(0))), f(suc(B_25)))) | ~E(s(s(s(0))), f(suc(A_1))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_1028, axiom, (![B_53]: ((~LE(f(B_53), s(s(0))) | E(s(0), f(B_53))) | LE(f(B_53), s(0)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_779, axiom, (![B_41]: ((~LE(f(suc(B_41)), s(s(s(0)))) | E(s(s(0)), f(suc(B_41)))) | LE(f(B_41), s(s(0))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_226, axiom, (![B_41]: ((~LE(f(suc(suc(B_41))), s(s(s(0)))) | E(s(s(0)), f(suc(suc(B_41))))) | LE(f(B_41), s(s(0))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_1121, axiom, (![A_2]: (((~E(s(s(0)), f(A_2)) | ~E(s(s(0)), f(suc(A_2)))) | E(f(A_2), f(suc(A_2)))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_189, axiom, (![A_2]: ((((~E(s(s(0)), f(suc(suc(A_2)))) | ~E(s(s(0)), f(suc(A_2)))) | ~E(f(A_2), f(suc(A_2)))) | ~E(s(s(0)), f(A_2))) | iLEQ(suc(A_2), suc(A_2)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_477, axiom, (![B_42, B_43, A_2]: ((((((((((~E(s(s(0)), f(suc(B_42))) | ~E(s(s(0)), f(B_42))) | ~iLEQ(suc(B_42), suc(B_43))) | ~E(s(s(0)), f(suc(A_2)))) | ~E(s(s(0)), f(suc(B_43)))) | ~iLEQ(suc(A_2), suc(B_42))) | ~E(s(s(0)), f(B_43))) | ~E(s(s(0)), f(A_2))) | E(f(A_2), f(suc(A_2)))) | E(f(B_42), f(suc(B_42)))) | E(f(B_43), f(suc(B_43))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_438, axiom, (![B_42, B_43, A_2]: (((((((((((((~E(s(s(0)), f(suc(B_42))) | ~E(f(B_43), f(suc(B_43)))) | ~E(s(s(0)), f(B_42))) | ~iLEQ(suc(B_42), suc(B_43))) | ~E(s(s(0)), f(suc(suc(B_42))))) | ~E(s(s(0)), f(suc(suc(B_43))))) | ~E(s(s(0)), f(suc(A_2)))) | ~E(s(s(0)), f(suc(B_43)))) | ~iLEQ(suc(A_2), suc(B_42))) | ~E(s(s(0)), f(B_43))) | ~E(s(s(0)), f(suc(suc(A_2))))) | ~E(f(B_42), f(suc(B_42)))) | ~E(s(s(0)), f(A_2))) | ~E(f(A_2), f(suc(A_2))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_447, axiom, (![B_60]: ((~LE(f(B_60), s(0)) | E(0, f(B_60))) | LE(f(B_60), 0))), file('unknown', unknown)).
% 268.43/251.23 tff(f_556, axiom, (![B_53]: ((~LE(f(suc(B_53)), s(s(0))) | E(s(0), f(suc(B_53)))) | LE(f(B_53), s(0)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_1283, axiom, (![B_53]: ((~LE(f(suc(suc(B_53))), s(s(0))) | E(s(0), f(suc(suc(B_53))))) | LE(f(B_53), s(0)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_656, axiom, (![A_3]: (((~E(s(0), f(A_3)) | ~E(s(0), f(suc(A_3)))) | E(f(A_3), f(suc(A_3)))) | iLEQ(suc(A_3), suc(A_3)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_608, axiom, (![A_3]: ((((~E(s(0), f(suc(suc(A_3)))) | ~E(s(0), f(suc(A_3)))) | ~E(f(A_3), f(suc(A_3)))) | ~E(s(0), f(A_3))) | iLEQ(suc(A_3), suc(A_3)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_396, axiom, (![B_54, B_55, A_3]: ((((((((((~iLEQ(suc(B_54), suc(B_55)) | ~E(s(0), f(suc(A_3)))) | ~iLEQ(suc(A_3), suc(B_54))) | ~E(s(0), f(suc(B_55)))) | ~E(s(0), f(A_3))) | ~E(s(0), f(B_55))) | ~E(s(0), f(suc(B_54)))) | ~E(s(0), f(B_54))) | E(f(A_3), f(suc(A_3)))) | E(f(B_54), f(suc(B_54)))) | E(f(B_55), f(suc(B_55))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_987, axiom, (![B_54, B_55, A_3]: (((((((((((((~iLEQ(suc(B_54), suc(B_55)) | ~E(s(0), f(suc(A_3)))) | ~E(f(B_55), f(suc(B_55)))) | ~iLEQ(suc(A_3), suc(B_54))) | ~E(s(0), f(suc(B_55)))) | ~E(s(0), f(suc(suc(B_54))))) | ~E(f(B_54), f(suc(B_54)))) | ~E(f(A_3), f(suc(A_3)))) | ~E(s(0), f(A_3))) | ~E(s(0), f(B_55))) | ~E(s(0), f(suc(suc(B_55))))) | ~E(s(0), f(suc(B_54)))) | ~E(s(0), f(suc(suc(A_3))))) | ~E(s(0), f(B_54)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_440, axiom, ~LE(f(z), 0), file('unknown', unknown)).
% 268.43/251.23 tff(f_1276, axiom, (![B_60]: ((~LE(f(suc(B_60)), s(0)) | E(0, f(suc(B_60)))) | LE(f(B_60), 0))), file('unknown', unknown)).
% 268.43/251.23 tff(f_615, axiom, (![B_60]: ((~LE(f(suc(suc(B_60))), s(0)) | E(0, f(suc(suc(B_60))))) | LE(f(B_60), 0))), file('unknown', unknown)).
% 268.43/251.23 tff(f_625, axiom, (![A_4]: (((~E(0, f(A_4)) | ~E(0, f(suc(A_4)))) | E(f(A_4), f(suc(A_4)))) | iLEQ(suc(A_4), suc(A_4)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_639, axiom, (![A_4]: ((((~E(0, f(suc(suc(A_4)))) | ~E(0, f(suc(A_4)))) | ~E(f(A_4), f(suc(A_4)))) | ~E(0, f(A_4))) | iLEQ(suc(A_4), suc(A_4)))), file('unknown', unknown)).
% 268.43/251.23 tff(f_219, axiom, (![B_61, B_62, A_4]: ((((((((((~E(0, f(suc(B_61))) | ~iLEQ(suc(B_61), suc(B_62))) | ~iLEQ(suc(A_4), suc(B_61))) | ~E(0, f(suc(B_62)))) | ~E(0, f(B_61))) | ~E(0, f(suc(A_4)))) | ~E(0, f(B_62))) | ~E(0, f(A_4))) | E(f(A_4), f(suc(A_4)))) | E(f(B_61), f(suc(B_61)))) | E(f(B_62), f(suc(B_62))))), file('unknown', unknown)).
% 268.43/251.23 tff(f_1231, axiom, (![B_61, B_62, A_4]: (((((((((((((~E(0, f(suc(B_61))) | ~iLEQ(suc(B_61), suc(B_62))) | ~E(f(A_4), f(suc(A_4)))) | ~iLEQ(suc(A_4), suc(B_61))) | ~E(0, f(suc(B_62)))) | ~E(0, f(suc(suc(A_4))))) | ~E(f(B_62), f(suc(B_62)))) | ~E(0, f(B_61))) | ~E(0, f(suc(suc(B_62))))) | ~E(0, f(suc(A_4)))) | ~E(0, f(B_62))) | ~E(0, f(suc(suc(B_61))))) | ~E(f(B_61), f(suc(B_61)))) | ~E(0, f(A_4)))), file('unknown', unknown)).
% 268.43/251.23 tff(c_6, plain, (![A_5]: (LE(f(A_5), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_66])).
% 268.43/251.23 tff(c_2, plain, (![B_23_1]: (LE(f(B_23_1), s(s(s(0)))) | E(s(s(s(0))), f(B_23_1)) | ~LE(f(B_23_1), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_30])).
% 268.43/251.23 tff(c_114, plain, (![B_23_1]: (LE(f(B_23_1), s(s(s(0)))) | E(s(s(s(0))), f(B_23_1)))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_2])).
% 268.43/251.23 tff(c_124, plain, (![B_41_127]: (LE(f(B_41_127), s(s(0))) | E(s(s(0)), f(B_41_127)) | ~LE(f(B_41_127), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_175])).
% 268.43/251.23 tff(c_128, plain, (![B_23_1]: (LE(f(B_23_1), s(s(0))) | E(s(s(0)), f(B_23_1)) | E(s(s(s(0))), f(B_23_1)))), inference(resolution, [status(thm)], [c_114, c_124])).
% 268.43/251.23 tff(c_86, plain, (![B_23_90]: (LE(f(B_23_90), s(s(s(0)))) | E(s(s(s(0))), f(suc(B_23_90))) | ~LE(f(suc(B_23_90)), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_1035])).
% 268.43/251.23 tff(c_110, plain, (![B_23_90]: (LE(f(B_23_90), s(s(s(0)))) | E(s(s(s(0))), f(suc(B_23_90))))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_86])).
% 268.43/251.23 tff(c_56, plain, (![B_23_57]: (LE(f(B_23_57), s(s(s(0)))) | E(s(s(s(0))), f(suc(suc(B_23_57)))) | ~LE(f(suc(suc(B_23_57))), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_646])).
% 268.43/251.23 tff(c_112, plain, (![B_23_57]: (LE(f(B_23_57), s(s(s(0)))) | E(s(s(s(0))), f(suc(suc(B_23_57)))))), inference(demodulation, [status(thm), theory('equality')], [c_6, c_56])).
% 268.43/251.23 tff(c_146, plain, (![A_1_137]: (iLEQ(suc(A_1_137), suc(A_1_137)) | E(f(A_1_137), f(suc(A_1_137))) | ~E(s(s(s(0))), f(suc(A_1_137))) | ~E(s(s(s(0))), f(A_1_137)))), inference(cnfTransformation, [status(thm)], [f_734])).
% 268.43/251.23 tff(c_162, plain, (![B_23_90]: (iLEQ(suc(B_23_90), suc(B_23_90)) | E(f(B_23_90), f(suc(B_23_90))) | ~E(s(s(s(0))), f(B_23_90)) | LE(f(B_23_90), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_146])).
% 268.43/251.23 tff(c_237, plain, (![A_1_146]: (iLEQ(suc(A_1_146), suc(A_1_146)) | ~E(s(s(s(0))), f(A_1_146)) | ~E(f(A_1_146), f(suc(A_1_146))) | ~E(s(s(s(0))), f(suc(A_1_146))) | ~E(s(s(s(0))), f(suc(suc(A_1_146)))))), inference(cnfTransformation, [status(thm)], [f_831])).
% 268.43/251.23 tff(c_368, plain, (![B_23_166]: (~E(s(s(s(0))), f(suc(B_23_166))) | ~E(s(s(s(0))), f(suc(suc(B_23_166)))) | iLEQ(suc(B_23_166), suc(B_23_166)) | ~E(s(s(s(0))), f(B_23_166)) | LE(f(B_23_166), s(s(s(0)))))), inference(resolution, [status(thm)], [c_162, c_237])).
% 268.43/251.23 tff(c_388, plain, (![B_23_170]: (~E(s(s(s(0))), f(suc(B_23_170))) | iLEQ(suc(B_23_170), suc(B_23_170)) | ~E(s(s(s(0))), f(B_23_170)) | LE(f(B_23_170), s(s(s(0)))))), inference(resolution, [status(thm)], [c_112, c_368])).
% 268.43/251.23 tff(c_404, plain, (![B_23_90]: (iLEQ(suc(B_23_90), suc(B_23_90)) | ~E(s(s(s(0))), f(B_23_90)) | LE(f(B_23_90), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_388])).
% 268.43/251.23 tff(c_686, plain, (![B_25_209, B_24_210, A_1_211]: (E(f(B_25_209), f(suc(B_25_209))) | E(f(B_24_210), f(suc(B_24_210))) | E(f(A_1_211), f(suc(A_1_211))) | ~E(s(s(s(0))), f(suc(A_1_211))) | ~E(s(s(s(0))), f(suc(B_25_209))) | ~E(s(s(s(0))), f(suc(B_24_210))) | ~E(s(s(s(0))), f(A_1_211)) | ~iLEQ(suc(A_1_211), suc(B_24_210)) | ~E(s(s(s(0))), f(B_24_210)) | ~E(s(s(s(0))), f(B_25_209)) | ~iLEQ(suc(B_24_210), suc(B_25_209)))), inference(cnfTransformation, [status(thm)], [f_366])).
% 268.43/251.23 tff(c_1959, plain, (![B_25_319, B_24_320, B_23_321]: (E(f(B_25_319), f(suc(B_25_319))) | E(f(B_24_320), f(suc(B_24_320))) | E(f(B_23_321), f(suc(B_23_321))) | ~E(s(s(s(0))), f(suc(B_25_319))) | ~E(s(s(s(0))), f(suc(B_24_320))) | ~E(s(s(s(0))), f(B_23_321)) | ~iLEQ(suc(B_23_321), suc(B_24_320)) | ~E(s(s(s(0))), f(B_24_320)) | ~E(s(s(s(0))), f(B_25_319)) | ~iLEQ(suc(B_24_320), suc(B_25_319)) | LE(f(B_23_321), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_686])).
% 268.43/251.23 tff(c_5561, plain, (![B_23_459, B_24_460, B_23_461]: (E(f(B_23_459), f(suc(B_23_459))) | E(f(B_24_460), f(suc(B_24_460))) | E(f(B_23_461), f(suc(B_23_461))) | ~E(s(s(s(0))), f(suc(B_24_460))) | ~E(s(s(s(0))), f(B_23_461)) | ~iLEQ(suc(B_23_461), suc(B_24_460)) | ~E(s(s(s(0))), f(B_24_460)) | ~E(s(s(s(0))), f(B_23_459)) | ~iLEQ(suc(B_24_460), suc(B_23_459)) | LE(f(B_23_461), s(s(s(0)))) | LE(f(B_23_459), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_1959])).
% 268.43/251.23 tff(c_8818, plain, (![B_23_558, B_23_559, B_23_560]: (E(f(B_23_558), f(suc(B_23_558))) | E(f(B_23_559), f(suc(B_23_559))) | E(f(B_23_560), f(suc(B_23_560))) | ~E(s(s(s(0))), f(B_23_560)) | ~iLEQ(suc(B_23_560), suc(B_23_559)) | ~E(s(s(s(0))), f(B_23_559)) | ~E(s(s(s(0))), f(B_23_558)) | ~iLEQ(suc(B_23_559), suc(B_23_558)) | LE(f(B_23_560), s(s(s(0)))) | LE(f(B_23_558), s(s(s(0)))) | LE(f(B_23_559), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_5561])).
% 268.43/251.23 tff(c_8969, plain, (![B_23_561, B_23_562]: (E(f(B_23_561), f(suc(B_23_561))) | E(f(B_23_562), f(suc(B_23_562))) | ~E(s(s(s(0))), f(B_23_561)) | ~iLEQ(suc(B_23_562), suc(B_23_561)) | LE(f(B_23_561), s(s(s(0)))) | ~E(s(s(s(0))), f(B_23_562)) | LE(f(B_23_562), s(s(s(0)))))), inference(resolution, [status(thm)], [c_404, c_8818])).
% 268.43/251.23 tff(c_9119, plain, (![B_23_90]: (E(f(B_23_90), f(suc(B_23_90))) | ~E(s(s(s(0))), f(B_23_90)) | LE(f(B_23_90), s(s(s(0)))))), inference(resolution, [status(thm)], [c_404, c_8969])).
% 268.43/251.23 tff(c_1848, plain, (![A_1_311, B_25_312, B_24_313]: (~E(s(s(s(0))), f(suc(A_1_311))) | ~E(s(s(s(0))), f(suc(B_25_312))) | ~E(s(s(s(0))), f(suc(suc(B_25_312)))) | ~E(s(s(s(0))), f(suc(B_24_313))) | ~E(f(A_1_311), f(suc(A_1_311))) | ~E(f(B_25_312), f(suc(B_25_312))) | ~E(s(s(s(0))), f(suc(suc(A_1_311)))) | ~E(s(s(s(0))), f(A_1_311)) | ~iLEQ(suc(A_1_311), suc(B_24_313)) | ~E(s(s(s(0))), f(B_24_313)) | ~E(f(B_24_313), f(suc(B_24_313))) | ~E(s(s(s(0))), f(B_25_312)) | ~E(s(s(s(0))), f(suc(suc(B_24_313)))) | ~iLEQ(suc(B_24_313), suc(B_25_312)))), inference(cnfTransformation, [status(thm)], [f_911])).
% 268.43/251.23 tff(c_5076, plain, (![A_1_446, B_23_447, B_24_448]: (~E(s(s(s(0))), f(suc(A_1_446))) | ~E(s(s(s(0))), f(suc(B_23_447))) | ~E(s(s(s(0))), f(suc(B_24_448))) | ~E(f(A_1_446), f(suc(A_1_446))) | ~E(f(B_23_447), f(suc(B_23_447))) | ~E(s(s(s(0))), f(suc(suc(A_1_446)))) | ~E(s(s(s(0))), f(A_1_446)) | ~iLEQ(suc(A_1_446), suc(B_24_448)) | ~E(s(s(s(0))), f(B_24_448)) | ~E(f(B_24_448), f(suc(B_24_448))) | ~E(s(s(s(0))), f(B_23_447)) | ~E(s(s(s(0))), f(suc(suc(B_24_448)))) | ~iLEQ(suc(B_24_448), suc(B_23_447)) | LE(f(B_23_447), s(s(s(0)))))), inference(resolution, [status(thm)], [c_112, c_1848])).
% 268.43/251.23 tff(c_16773, plain, (![A_1_746, B_24_747, B_23_748]: (~E(s(s(s(0))), f(suc(A_1_746))) | ~E(s(s(s(0))), f(suc(B_24_747))) | ~E(f(A_1_746), f(suc(A_1_746))) | ~E(f(B_23_748), f(suc(B_23_748))) | ~E(s(s(s(0))), f(suc(suc(A_1_746)))) | ~E(s(s(s(0))), f(A_1_746)) | ~iLEQ(suc(A_1_746), suc(B_24_747)) | ~E(s(s(s(0))), f(B_24_747)) | ~E(f(B_24_747), f(suc(B_24_747))) | ~E(s(s(s(0))), f(B_23_748)) | ~E(s(s(s(0))), f(suc(suc(B_24_747)))) | ~iLEQ(suc(B_24_747), suc(B_23_748)) | LE(f(B_23_748), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_5076])).
% 268.43/251.23 tff(c_99204, plain, (![B_23_2247, B_24_2248, B_23_2249]: (~E(s(s(s(0))), f(suc(B_23_2247))) | ~E(s(s(s(0))), f(suc(B_24_2248))) | ~E(f(B_23_2249), f(suc(B_23_2249))) | ~E(s(s(s(0))), f(suc(suc(B_23_2247)))) | ~iLEQ(suc(B_23_2247), suc(B_24_2248)) | ~E(s(s(s(0))), f(B_24_2248)) | ~E(f(B_24_2248), f(suc(B_24_2248))) | ~E(s(s(s(0))), f(B_23_2249)) | ~E(s(s(s(0))), f(suc(suc(B_24_2248)))) | ~iLEQ(suc(B_24_2248), suc(B_23_2249)) | LE(f(B_23_2249), s(s(s(0)))) | ~E(s(s(s(0))), f(B_23_2247)) | LE(f(B_23_2247), s(s(s(0)))))), inference(resolution, [status(thm)], [c_9119, c_16773])).
% 268.43/251.23 tff(c_99400, plain, (![B_23_2250, B_24_2251, B_23_2252]: (~E(s(s(s(0))), f(suc(B_23_2250))) | ~E(s(s(s(0))), f(suc(B_24_2251))) | ~E(s(s(s(0))), f(suc(suc(B_23_2250)))) | ~iLEQ(suc(B_23_2250), suc(B_24_2251)) | ~E(s(s(s(0))), f(B_24_2251)) | ~E(f(B_24_2251), f(suc(B_24_2251))) | ~E(s(s(s(0))), f(suc(suc(B_24_2251)))) | ~iLEQ(suc(B_24_2251), suc(B_23_2252)) | ~E(s(s(s(0))), f(B_23_2250)) | LE(f(B_23_2250), s(s(s(0)))) | ~E(s(s(s(0))), f(B_23_2252)) | LE(f(B_23_2252), s(s(s(0)))))), inference(resolution, [status(thm)], [c_9119, c_99204])).
% 268.43/251.23 tff(c_99419, plain, (![B_23_2253, B_24_2254, B_23_2255]: (~E(s(s(s(0))), f(suc(B_23_2253))) | ~E(s(s(s(0))), f(suc(B_24_2254))) | ~iLEQ(suc(B_23_2253), suc(B_24_2254)) | ~E(s(s(s(0))), f(B_24_2254)) | ~E(f(B_24_2254), f(suc(B_24_2254))) | ~E(s(s(s(0))), f(suc(suc(B_24_2254)))) | ~iLEQ(suc(B_24_2254), suc(B_23_2255)) | ~E(s(s(s(0))), f(B_23_2253)) | ~E(s(s(s(0))), f(B_23_2255)) | LE(f(B_23_2255), s(s(s(0)))) | LE(f(B_23_2253), s(s(s(0)))))), inference(resolution, [status(thm)], [c_112, c_99400])).
% 268.43/251.23 tff(c_99436, plain, (![B_24_2256, B_23_2257, B_23_2258]: (~E(s(s(s(0))), f(suc(B_24_2256))) | ~iLEQ(suc(B_23_2257), suc(B_24_2256)) | ~E(s(s(s(0))), f(B_24_2256)) | ~E(f(B_24_2256), f(suc(B_24_2256))) | ~E(s(s(s(0))), f(suc(suc(B_24_2256)))) | ~iLEQ(suc(B_24_2256), suc(B_23_2258)) | ~E(s(s(s(0))), f(B_23_2257)) | ~E(s(s(s(0))), f(B_23_2258)) | LE(f(B_23_2258), s(s(s(0)))) | LE(f(B_23_2257), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_99419])).
% 268.43/251.23 tff(c_99677, plain, (![B_23_2259, B_23_2260]: (~E(s(s(s(0))), f(suc(B_23_2259))) | ~E(f(B_23_2259), f(suc(B_23_2259))) | ~E(s(s(s(0))), f(suc(suc(B_23_2259)))) | ~iLEQ(suc(B_23_2259), suc(B_23_2260)) | ~E(s(s(s(0))), f(B_23_2260)) | LE(f(B_23_2260), s(s(s(0)))) | ~E(s(s(s(0))), f(B_23_2259)) | LE(f(B_23_2259), s(s(s(0)))))), inference(resolution, [status(thm)], [c_404, c_99436])).
% 268.43/251.23 tff(c_99873, plain, (![B_23_2261, B_23_2262]: (~E(s(s(s(0))), f(suc(B_23_2261))) | ~E(s(s(s(0))), f(suc(suc(B_23_2261)))) | ~iLEQ(suc(B_23_2261), suc(B_23_2262)) | ~E(s(s(s(0))), f(B_23_2262)) | LE(f(B_23_2262), s(s(s(0)))) | ~E(s(s(s(0))), f(B_23_2261)) | LE(f(B_23_2261), s(s(s(0)))))), inference(resolution, [status(thm)], [c_9119, c_99677])).
% 268.43/251.23 tff(c_99892, plain, (![B_23_2263, B_23_2264]: (~E(s(s(s(0))), f(suc(B_23_2263))) | ~iLEQ(suc(B_23_2263), suc(B_23_2264)) | ~E(s(s(s(0))), f(B_23_2264)) | LE(f(B_23_2264), s(s(s(0)))) | ~E(s(s(s(0))), f(B_23_2263)) | LE(f(B_23_2263), s(s(s(0)))))), inference(resolution, [status(thm)], [c_112, c_99873])).
% 268.43/251.23 tff(c_99930, plain, (![B_23_2268, B_23_2269]: (~iLEQ(suc(B_23_2268), suc(B_23_2269)) | ~E(s(s(s(0))), f(B_23_2269)) | LE(f(B_23_2269), s(s(s(0)))) | ~E(s(s(s(0))), f(B_23_2268)) | LE(f(B_23_2268), s(s(s(0)))))), inference(resolution, [status(thm)], [c_110, c_99892])).
% 268.43/251.23 tff(c_100171, plain, (![B_23_2270]: (~E(s(s(s(0))), f(B_23_2270)) | LE(f(B_23_2270), s(s(s(0)))))), inference(resolution, [status(thm)], [c_404, c_99930])).
% 268.43/251.23 tff(c_14, plain, (![B_41_15]: (LE(f(B_41_15), s(s(0))) | E(s(s(0)), f(B_41_15)) | ~LE(f(B_41_15), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_175])).
% 268.43/251.23 tff(c_100184, plain, (![B_23_2271]: (LE(f(B_23_2271), s(s(0))) | E(s(s(0)), f(B_23_2271)) | ~E(s(s(s(0))), f(B_23_2271)))), inference(resolution, [status(thm)], [c_100171, c_14])).
% 268.43/251.23 tff(c_100226, plain, (![B_23_2273]: (LE(f(B_23_2273), s(s(0))) | E(s(s(0)), f(B_23_2273)))), inference(resolution, [status(thm)], [c_128, c_100184])).
% 268.43/251.23 tff(c_84, plain, (![B_53_89]: (LE(f(B_53_89), s(0)) | E(s(0), f(B_53_89)) | ~LE(f(B_53_89), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_1028])).
% 268.43/251.23 tff(c_100238, plain, (![B_23_2273]: (LE(f(B_23_2273), s(0)) | E(s(0), f(B_23_2273)) | E(s(s(0)), f(B_23_2273)))), inference(resolution, [status(thm)], [c_100226, c_84])).
% 268.43/251.23 tff(c_132, plain, (![B_41_131]: (LE(f(B_41_131), s(s(0))) | E(s(s(0)), f(suc(B_41_131))) | ~LE(f(suc(B_41_131)), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_779])).
% 268.43/251.23 tff(c_136, plain, (![B_41_131]: (LE(f(B_41_131), s(s(0))) | E(s(s(0)), f(suc(B_41_131))) | E(s(s(s(0))), f(suc(B_41_131))))), inference(resolution, [status(thm)], [c_114, c_132])).
% 268.43/251.23 tff(c_68, plain, (![B_41_69]: (LE(f(B_41_69), s(s(0))) | E(s(s(0)), f(suc(B_41_69))) | ~LE(f(suc(B_41_69)), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_779])).
% 268.43/251.23 tff(c_100205, plain, (![B_41_2272]: (LE(f(B_41_2272), s(s(0))) | E(s(s(0)), f(suc(B_41_2272))) | ~E(s(s(s(0))), f(suc(B_41_2272))))), inference(resolution, [status(thm)], [c_100171, c_68])).
% 268.43/251.23 tff(c_100222, plain, (![B_41_131]: (LE(f(B_41_131), s(s(0))) | E(s(s(0)), f(suc(B_41_131))))), inference(resolution, [status(thm)], [c_136, c_100205])).
% 268.43/251.23 tff(c_139, plain, (![B_41_134]: (LE(f(B_41_134), s(s(0))) | E(s(s(0)), f(suc(suc(B_41_134)))) | ~LE(f(suc(suc(B_41_134))), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_226])).
% 268.43/251.23 tff(c_143, plain, (![B_41_134]: (LE(f(B_41_134), s(s(0))) | E(s(s(0)), f(suc(suc(B_41_134)))) | E(s(s(s(0))), f(suc(suc(B_41_134)))))), inference(resolution, [status(thm)], [c_114, c_139])).
% 268.43/251.23 tff(c_20, plain, (![B_41_20]: (LE(f(B_41_20), s(s(0))) | E(s(s(0)), f(suc(suc(B_41_20)))) | ~LE(f(suc(suc(B_41_20))), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_226])).
% 268.43/251.23 tff(c_100734, plain, (![B_41_2278]: (LE(f(B_41_2278), s(s(0))) | E(s(s(0)), f(suc(suc(B_41_2278)))) | ~E(s(s(s(0))), f(suc(suc(B_41_2278)))))), inference(resolution, [status(thm)], [c_100171, c_20])).
% 268.43/251.23 tff(c_100744, plain, (![B_41_134]: (LE(f(B_41_134), s(s(0))) | E(s(s(0)), f(suc(suc(B_41_134)))))), inference(resolution, [status(thm)], [c_143, c_100734])).
% 268.43/251.23 tff(c_100239, plain, (![B_41_2274]: (LE(f(B_41_2274), s(s(0))) | E(s(s(0)), f(suc(B_41_2274))))), inference(resolution, [status(thm)], [c_136, c_100205])).
% 268.43/251.23 tff(c_92, plain, (![A_2_97]: (iLEQ(suc(A_2_97), suc(A_2_97)) | E(f(A_2_97), f(suc(A_2_97))) | ~E(s(s(0)), f(suc(A_2_97))) | ~E(s(s(0)), f(A_2_97)))), inference(cnfTransformation, [status(thm)], [f_1121])).
% 268.43/251.23 tff(c_100863, plain, (![B_41_2280]: (iLEQ(suc(B_41_2280), suc(B_41_2280)) | E(f(B_41_2280), f(suc(B_41_2280))) | ~E(s(s(0)), f(B_41_2280)) | LE(f(B_41_2280), s(s(0))))), inference(resolution, [status(thm)], [c_100239, c_92])).
% 268.43/251.23 tff(c_16, plain, (![A_2_16]: (iLEQ(suc(A_2_16), suc(A_2_16)) | ~E(s(s(0)), f(A_2_16)) | ~E(f(A_2_16), f(suc(A_2_16))) | ~E(s(s(0)), f(suc(A_2_16))) | ~E(s(s(0)), f(suc(suc(A_2_16)))))), inference(cnfTransformation, [status(thm)], [f_189])).
% 268.43/251.23 tff(c_101142, plain, (![B_41_2286]: (~E(s(s(0)), f(suc(B_41_2286))) | ~E(s(s(0)), f(suc(suc(B_41_2286)))) | iLEQ(suc(B_41_2286), suc(B_41_2286)) | ~E(s(s(0)), f(B_41_2286)) | LE(f(B_41_2286), s(s(0))))), inference(resolution, [status(thm)], [c_100863, c_16])).
% 268.43/251.23 tff(c_101161, plain, (![B_41_2287]: (~E(s(s(0)), f(suc(B_41_2287))) | iLEQ(suc(B_41_2287), suc(B_41_2287)) | ~E(s(s(0)), f(B_41_2287)) | LE(f(B_41_2287), s(s(0))))), inference(resolution, [status(thm)], [c_100744, c_101142])).
% 268.43/251.23 tff(c_101177, plain, (![B_41_131]: (iLEQ(suc(B_41_131), suc(B_41_131)) | ~E(s(s(0)), f(B_41_131)) | LE(f(B_41_131), s(s(0))))), inference(resolution, [status(thm)], [c_100222, c_101161])).
% 268.43/251.23 tff(c_101178, plain, (![B_41_2288]: (iLEQ(suc(B_41_2288), suc(B_41_2288)) | ~E(s(s(0)), f(B_41_2288)) | LE(f(B_41_2288), s(s(0))))), inference(resolution, [status(thm)], [c_100222, c_101161])).
% 268.43/251.23 tff(c_38, plain, (![B_43_41, B_42_40, A_2_42]: (E(f(B_43_41), f(suc(B_43_41))) | E(f(B_42_40), f(suc(B_42_40))) | E(f(A_2_42), f(suc(A_2_42))) | ~E(s(s(0)), f(A_2_42)) | ~E(s(s(0)), f(B_43_41)) | ~iLEQ(suc(A_2_42), suc(B_42_40)) | ~E(s(s(0)), f(suc(B_43_41))) | ~E(s(s(0)), f(suc(A_2_42))) | ~iLEQ(suc(B_42_40), suc(B_43_41)) | ~E(s(s(0)), f(B_42_40)) | ~E(s(s(0)), f(suc(B_42_40))))), inference(cnfTransformation, [status(thm)], [f_477])).
% 268.43/251.23 tff(c_104454, plain, (![B_43_2354, B_41_2355]: (E(f(B_43_2354), f(suc(B_43_2354))) | E(f(B_41_2355), f(suc(B_41_2355))) | ~E(s(s(0)), f(B_43_2354)) | ~E(s(s(0)), f(suc(B_43_2354))) | ~iLEQ(suc(B_41_2355), suc(B_43_2354)) | ~E(s(s(0)), f(suc(B_41_2355))) | ~E(s(s(0)), f(B_41_2355)) | LE(f(B_41_2355), s(s(0))))), inference(resolution, [status(thm)], [c_101178, c_38])).
% 268.43/251.23 tff(c_104635, plain, (![B_41_2358, B_41_2359]: (E(f(B_41_2358), f(suc(B_41_2358))) | E(f(B_41_2359), f(suc(B_41_2359))) | ~E(s(s(0)), f(B_41_2358)) | ~iLEQ(suc(B_41_2359), suc(B_41_2358)) | ~E(s(s(0)), f(suc(B_41_2359))) | ~E(s(s(0)), f(B_41_2359)) | LE(f(B_41_2359), s(s(0))) | LE(f(B_41_2358), s(s(0))))), inference(resolution, [status(thm)], [c_100222, c_104454])).
% 268.43/251.23 tff(c_104747, plain, (![B_41_2360]: (E(f(B_41_2360), f(suc(B_41_2360))) | ~E(s(s(0)), f(suc(B_41_2360))) | ~E(s(s(0)), f(B_41_2360)) | LE(f(B_41_2360), s(s(0))))), inference(resolution, [status(thm)], [c_101177, c_104635])).
% 268.43/251.23 tff(c_104763, plain, (![B_41_131]: (E(f(B_41_131), f(suc(B_41_131))) | ~E(s(s(0)), f(B_41_131)) | LE(f(B_41_131), s(s(0))))), inference(resolution, [status(thm)], [c_100222, c_104747])).
% 268.43/251.23 tff(c_104764, plain, (![B_41_2361]: (E(f(B_41_2361), f(suc(B_41_2361))) | ~E(s(s(0)), f(B_41_2361)) | LE(f(B_41_2361), s(s(0))))), inference(resolution, [status(thm)], [c_100222, c_104747])).
% 268.43/251.23 tff(c_32, plain, (![A_2_38, B_42_36, B_43_37]: (~E(f(A_2_38), f(suc(A_2_38))) | ~E(s(s(0)), f(A_2_38)) | ~E(f(B_42_36), f(suc(B_42_36))) | ~E(s(s(0)), f(suc(suc(A_2_38)))) | ~E(s(s(0)), f(B_43_37)) | ~iLEQ(suc(A_2_38), suc(B_42_36)) | ~E(s(s(0)), f(suc(B_43_37))) | ~E(s(s(0)), f(suc(A_2_38))) | ~E(s(s(0)), f(suc(suc(B_43_37)))) | ~E(s(s(0)), f(suc(suc(B_42_36)))) | ~iLEQ(suc(B_42_36), suc(B_43_37)) | ~E(s(s(0)), f(B_42_36)) | ~E(f(B_43_37), f(suc(B_43_37))) | ~E(s(s(0)), f(suc(B_42_36))))), inference(cnfTransformation, [status(thm)], [f_438])).
% 268.43/251.23 tff(c_128929, plain, (![B_42_2965, B_41_2966, B_43_2967]: (~E(f(B_42_2965), f(suc(B_42_2965))) | ~E(s(s(0)), f(suc(suc(B_41_2966)))) | ~E(s(s(0)), f(B_43_2967)) | ~iLEQ(suc(B_41_2966), suc(B_42_2965)) | ~E(s(s(0)), f(suc(B_43_2967))) | ~E(s(s(0)), f(suc(B_41_2966))) | ~E(s(s(0)), f(suc(suc(B_43_2967)))) | ~E(s(s(0)), f(suc(suc(B_42_2965)))) | ~iLEQ(suc(B_42_2965), suc(B_43_2967)) | ~E(s(s(0)), f(B_42_2965)) | ~E(f(B_43_2967), f(suc(B_43_2967))) | ~E(s(s(0)), f(suc(B_42_2965))) | ~E(s(s(0)), f(B_41_2966)) | LE(f(B_41_2966), s(s(0))))), inference(resolution, [status(thm)], [c_104764, c_32])).
% 268.43/251.23 tff(c_129065, plain, (![B_41_2968, B_43_2969, B_41_2970]: (~E(s(s(0)), f(suc(suc(B_41_2968)))) | ~E(s(s(0)), f(B_43_2969)) | ~iLEQ(suc(B_41_2968), suc(B_41_2970)) | ~E(s(s(0)), f(suc(B_43_2969))) | ~E(s(s(0)), f(suc(B_41_2968))) | ~E(s(s(0)), f(suc(suc(B_43_2969)))) | ~E(s(s(0)), f(suc(suc(B_41_2970)))) | ~iLEQ(suc(B_41_2970), suc(B_43_2969)) | ~E(f(B_43_2969), f(suc(B_43_2969))) | ~E(s(s(0)), f(suc(B_41_2970))) | ~E(s(s(0)), f(B_41_2968)) | LE(f(B_41_2968), s(s(0))) | ~E(s(s(0)), f(B_41_2970)) | LE(f(B_41_2970), s(s(0))))), inference(resolution, [status(thm)], [c_104763, c_128929])).
% 268.43/251.23 tff(c_129084, plain, (![B_43_2971, B_41_2972, B_41_2973]: (~E(s(s(0)), f(B_43_2971)) | ~iLEQ(suc(B_41_2972), suc(B_41_2973)) | ~E(s(s(0)), f(suc(B_43_2971))) | ~E(s(s(0)), f(suc(B_41_2972))) | ~E(s(s(0)), f(suc(suc(B_43_2971)))) | ~E(s(s(0)), f(suc(suc(B_41_2973)))) | ~iLEQ(suc(B_41_2973), suc(B_43_2971)) | ~E(f(B_43_2971), f(suc(B_43_2971))) | ~E(s(s(0)), f(suc(B_41_2973))) | ~E(s(s(0)), f(B_41_2972)) | ~E(s(s(0)), f(B_41_2973)) | LE(f(B_41_2973), s(s(0))) | LE(f(B_41_2972), s(s(0))))), inference(resolution, [status(thm)], [c_100744, c_129065])).
% 268.43/251.23 tff(c_129233, plain, (![B_43_2977, B_41_2978]: (~E(s(s(0)), f(B_43_2977)) | ~E(s(s(0)), f(suc(B_43_2977))) | ~E(s(s(0)), f(suc(suc(B_43_2977)))) | ~E(s(s(0)), f(suc(suc(B_41_2978)))) | ~iLEQ(suc(B_41_2978), suc(B_43_2977)) | ~E(f(B_43_2977), f(suc(B_43_2977))) | ~E(s(s(0)), f(suc(B_41_2978))) | ~E(s(s(0)), f(B_41_2978)) | LE(f(B_41_2978), s(s(0))))), inference(resolution, [status(thm)], [c_101177, c_129084])).
% 268.43/251.23 tff(c_129252, plain, (![B_41_2979, B_41_2980]: (~E(s(s(0)), f(B_41_2979)) | ~E(s(s(0)), f(suc(B_41_2979))) | ~E(s(s(0)), f(suc(suc(B_41_2980)))) | ~iLEQ(suc(B_41_2980), suc(B_41_2979)) | ~E(f(B_41_2979), f(suc(B_41_2979))) | ~E(s(s(0)), f(suc(B_41_2980))) | ~E(s(s(0)), f(B_41_2980)) | LE(f(B_41_2980), s(s(0))) | LE(f(B_41_2979), s(s(0))))), inference(resolution, [status(thm)], [c_100744, c_129233])).
% 268.43/251.23 tff(c_129269, plain, (![B_41_2981, B_41_2982]: (~E(s(s(0)), f(B_41_2981)) | ~E(s(s(0)), f(suc(suc(B_41_2982)))) | ~iLEQ(suc(B_41_2982), suc(B_41_2981)) | ~E(f(B_41_2981), f(suc(B_41_2981))) | ~E(s(s(0)), f(suc(B_41_2982))) | ~E(s(s(0)), f(B_41_2982)) | LE(f(B_41_2982), s(s(0))) | LE(f(B_41_2981), s(s(0))))), inference(resolution, [status(thm)], [c_100222, c_129252])).
% 268.43/251.23 tff(c_129288, plain, (![B_41_2983, B_41_2984]: (~E(s(s(0)), f(B_41_2983)) | ~iLEQ(suc(B_41_2984), suc(B_41_2983)) | ~E(f(B_41_2983), f(suc(B_41_2983))) | ~E(s(s(0)), f(suc(B_41_2984))) | ~E(s(s(0)), f(B_41_2984)) | LE(f(B_41_2983), s(s(0))) | LE(f(B_41_2984), s(s(0))))), inference(resolution, [status(thm)], [c_100744, c_129269])).
% 268.43/251.23 tff(c_129418, plain, (![B_41_2985]: (~E(f(B_41_2985), f(suc(B_41_2985))) | ~E(s(s(0)), f(suc(B_41_2985))) | ~E(s(s(0)), f(B_41_2985)) | LE(f(B_41_2985), s(s(0))))), inference(resolution, [status(thm)], [c_101177, c_129288])).
% 268.43/251.23 tff(c_129554, plain, (![B_41_2986]: (~E(s(s(0)), f(suc(B_41_2986))) | ~E(s(s(0)), f(B_41_2986)) | LE(f(B_41_2986), s(s(0))))), inference(resolution, [status(thm)], [c_104763, c_129418])).
% 268.43/251.23 tff(c_129575, plain, (![B_41_2987]: (~E(s(s(0)), f(B_41_2987)) | LE(f(B_41_2987), s(s(0))))), inference(resolution, [status(thm)], [c_100222, c_129554])).
% 268.43/251.23 tff(c_129588, plain, (![B_41_2988]: (LE(f(B_41_2988), s(0)) | E(s(0), f(B_41_2988)) | ~E(s(s(0)), f(B_41_2988)))), inference(resolution, [status(thm)], [c_129575, c_84])).
% 268.43/251.23 tff(c_129630, plain, (![B_23_2990]: (LE(f(B_23_2990), s(0)) | E(s(0), f(B_23_2990)))), inference(resolution, [status(thm)], [c_100238, c_129588])).
% 268.43/251.23 tff(c_36, plain, (![B_60_39]: (LE(f(B_60_39), 0) | E(0, f(B_60_39)) | ~LE(f(B_60_39), s(0)))), inference(cnfTransformation, [status(thm)], [f_447])).
% 268.43/251.23 tff(c_129642, plain, (![B_23_2990]: (LE(f(B_23_2990), 0) | E(0, f(B_23_2990)) | E(s(0), f(B_23_2990)))), inference(resolution, [status(thm)], [c_129630, c_36])).
% 268.43/251.23 tff(c_44, plain, (![B_53_49]: (LE(f(B_53_49), s(0)) | E(s(0), f(suc(B_53_49))) | ~LE(f(suc(B_53_49)), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_556])).
% 268.43/251.23 tff(c_100237, plain, (![B_53_49]: (LE(f(B_53_49), s(0)) | E(s(0), f(suc(B_53_49))) | E(s(s(0)), f(suc(B_53_49))))), inference(resolution, [status(thm)], [c_100226, c_44])).
% 268.43/251.23 tff(c_129609, plain, (![B_53_2989]: (LE(f(B_53_2989), s(0)) | E(s(0), f(suc(B_53_2989))) | ~E(s(s(0)), f(suc(B_53_2989))))), inference(resolution, [status(thm)], [c_129575, c_44])).
% 268.43/251.23 tff(c_129627, plain, (![B_53_49]: (LE(f(B_53_49), s(0)) | E(s(0), f(suc(B_53_49))))), inference(resolution, [status(thm)], [c_100237, c_129609])).
% 268.43/251.23 tff(c_104, plain, (![B_53_111]: (LE(f(B_53_111), s(0)) | E(s(0), f(suc(suc(B_53_111)))) | ~LE(f(suc(suc(B_53_111))), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_1283])).
% 268.43/251.23 tff(c_100236, plain, (![B_53_111]: (LE(f(B_53_111), s(0)) | E(s(0), f(suc(suc(B_53_111)))) | E(s(s(0)), f(suc(suc(B_53_111)))))), inference(resolution, [status(thm)], [c_100226, c_104])).
% 268.43/251.23 tff(c_129840, plain, (![B_53_2995]: (LE(f(B_53_2995), s(0)) | E(s(0), f(suc(suc(B_53_2995)))) | ~E(s(s(0)), f(suc(suc(B_53_2995)))))), inference(resolution, [status(thm)], [c_129575, c_104])).
% 268.43/251.23 tff(c_129851, plain, (![B_53_111]: (LE(f(B_53_111), s(0)) | E(s(0), f(suc(suc(B_53_111)))))), inference(resolution, [status(thm)], [c_100236, c_129840])).
% 268.43/251.23 tff(c_129643, plain, (![B_53_2991]: (LE(f(B_53_2991), s(0)) | E(s(0), f(suc(B_53_2991))))), inference(resolution, [status(thm)], [c_100237, c_129609])).
% 268.43/251.23 tff(c_58, plain, (![A_3_58]: (iLEQ(suc(A_3_58), suc(A_3_58)) | E(f(A_3_58), f(suc(A_3_58))) | ~E(s(0), f(suc(A_3_58))) | ~E(s(0), f(A_3_58)))), inference(cnfTransformation, [status(thm)], [f_656])).
% 268.43/251.23 tff(c_129897, plain, (![B_53_2997]: (iLEQ(suc(B_53_2997), suc(B_53_2997)) | E(f(B_53_2997), f(suc(B_53_2997))) | ~E(s(0), f(B_53_2997)) | LE(f(B_53_2997), s(0)))), inference(resolution, [status(thm)], [c_129643, c_58])).
% 268.43/251.23 tff(c_48, plain, (![A_3_53]: (iLEQ(suc(A_3_53), suc(A_3_53)) | ~E(s(0), f(A_3_53)) | ~E(f(A_3_53), f(suc(A_3_53))) | ~E(s(0), f(suc(A_3_53))) | ~E(s(0), f(suc(suc(A_3_53)))))), inference(cnfTransformation, [status(thm)], [f_608])).
% 268.43/251.23 tff(c_130117, plain, (![B_53_3001]: (~E(s(0), f(suc(B_53_3001))) | ~E(s(0), f(suc(suc(B_53_3001)))) | iLEQ(suc(B_53_3001), suc(B_53_3001)) | ~E(s(0), f(B_53_3001)) | LE(f(B_53_3001), s(0)))), inference(resolution, [status(thm)], [c_129897, c_48])).
% 268.43/251.23 tff(c_130191, plain, (![B_53_3003]: (~E(s(0), f(suc(B_53_3003))) | iLEQ(suc(B_53_3003), suc(B_53_3003)) | ~E(s(0), f(B_53_3003)) | LE(f(B_53_3003), s(0)))), inference(resolution, [status(thm)], [c_129851, c_130117])).
% 268.43/251.23 tff(c_130207, plain, (![B_53_49]: (iLEQ(suc(B_53_49), suc(B_53_49)) | ~E(s(0), f(B_53_49)) | LE(f(B_53_49), s(0)))), inference(resolution, [status(thm)], [c_129627, c_130191])).
% 268.43/251.23 tff(c_30, plain, (![B_55_34, B_54_33, A_3_35]: (E(f(B_55_34), f(suc(B_55_34))) | E(f(B_54_33), f(suc(B_54_33))) | E(f(A_3_35), f(suc(A_3_35))) | ~E(s(0), f(B_54_33)) | ~E(s(0), f(suc(B_54_33))) | ~E(s(0), f(B_55_34)) | ~E(s(0), f(A_3_35)) | ~E(s(0), f(suc(B_55_34))) | ~iLEQ(suc(A_3_35), suc(B_54_33)) | ~E(s(0), f(suc(A_3_35))) | ~iLEQ(suc(B_54_33), suc(B_55_34)))), inference(cnfTransformation, [status(thm)], [f_396])).
% 268.43/251.23 tff(c_131884, plain, (![B_55_3058, B_53_3059, A_3_3060]: (E(f(B_55_3058), f(suc(B_55_3058))) | E(f(B_53_3059), f(suc(B_53_3059))) | E(f(A_3_3060), f(suc(A_3_3060))) | ~E(s(0), f(B_53_3059)) | ~E(s(0), f(B_55_3058)) | ~E(s(0), f(A_3_3060)) | ~E(s(0), f(suc(B_55_3058))) | ~iLEQ(suc(A_3_3060), suc(B_53_3059)) | ~E(s(0), f(suc(A_3_3060))) | ~iLEQ(suc(B_53_3059), suc(B_55_3058)) | LE(f(B_53_3059), s(0)))), inference(resolution, [status(thm)], [c_129643, c_30])).
% 268.43/251.23 tff(c_131909, plain, (![B_53_3063, B_53_3064, A_3_3065]: (E(f(B_53_3063), f(suc(B_53_3063))) | E(f(B_53_3064), f(suc(B_53_3064))) | E(f(A_3_3065), f(suc(A_3_3065))) | ~E(s(0), f(B_53_3064)) | ~E(s(0), f(B_53_3063)) | ~E(s(0), f(A_3_3065)) | ~iLEQ(suc(A_3_3065), suc(B_53_3064)) | ~E(s(0), f(suc(A_3_3065))) | ~iLEQ(suc(B_53_3064), suc(B_53_3063)) | LE(f(B_53_3064), s(0)) | LE(f(B_53_3063), s(0)))), inference(resolution, [status(thm)], [c_129627, c_131884])).
% 268.43/251.23 tff(c_131973, plain, (![B_53_3066, B_53_3067]: (E(f(B_53_3066), f(suc(B_53_3066))) | E(f(B_53_3067), f(suc(B_53_3067))) | ~E(s(0), f(B_53_3066)) | ~E(s(0), f(suc(B_53_3067))) | ~iLEQ(suc(B_53_3067), suc(B_53_3066)) | LE(f(B_53_3066), s(0)) | ~E(s(0), f(B_53_3067)) | LE(f(B_53_3067), s(0)))), inference(resolution, [status(thm)], [c_130207, c_131909])).
% 268.43/251.23 tff(c_132059, plain, (![B_53_3070, B_53_3071]: (E(f(B_53_3070), f(suc(B_53_3070))) | E(f(B_53_3071), f(suc(B_53_3071))) | ~E(s(0), f(B_53_3070)) | ~iLEQ(suc(B_53_3071), suc(B_53_3070)) | LE(f(B_53_3070), s(0)) | ~E(s(0), f(B_53_3071)) | LE(f(B_53_3071), s(0)))), inference(resolution, [status(thm)], [c_129627, c_131973])).
% 268.43/251.23 tff(c_132118, plain, (![B_53_49]: (E(f(B_53_49), f(suc(B_53_49))) | ~E(s(0), f(B_53_49)) | LE(f(B_53_49), s(0)))), inference(resolution, [status(thm)], [c_130207, c_132059])).
% 268.43/251.23 tff(c_129853, plain, (![B_53_2996]: (LE(f(B_53_2996), s(0)) | E(s(0), f(suc(suc(B_53_2996)))))), inference(resolution, [status(thm)], [c_100236, c_129840])).
% 268.43/251.23 tff(c_80, plain, (![B_54_83, A_3_85, B_55_84]: (~E(s(0), f(B_54_83)) | ~E(s(0), f(suc(suc(A_3_85)))) | ~E(s(0), f(suc(B_54_83))) | ~E(s(0), f(suc(suc(B_55_84)))) | ~E(s(0), f(B_55_84)) | ~E(s(0), f(A_3_85)) | ~E(f(A_3_85), f(suc(A_3_85))) | ~E(f(B_54_83), f(suc(B_54_83))) | ~E(s(0), f(suc(suc(B_54_83)))) | ~E(s(0), f(suc(B_55_84))) | ~iLEQ(suc(A_3_85), suc(B_54_83)) | ~E(f(B_55_84), f(suc(B_55_84))) | ~E(s(0), f(suc(A_3_85))) | ~iLEQ(suc(B_54_83), suc(B_55_84)))), inference(cnfTransformation, [status(thm)], [f_987])).
% 268.43/251.23 tff(c_143800, plain, (![B_54_3713, B_55_3714, B_53_3715]: (~E(s(0), f(B_54_3713)) | ~E(s(0), f(suc(B_54_3713))) | ~E(s(0), f(suc(suc(B_55_3714)))) | ~E(s(0), f(B_55_3714)) | ~E(s(0), f(B_53_3715)) | ~E(f(B_53_3715), f(suc(B_53_3715))) | ~E(f(B_54_3713), f(suc(B_54_3713))) | ~E(s(0), f(suc(suc(B_54_3713)))) | ~E(s(0), f(suc(B_55_3714))) | ~iLEQ(suc(B_53_3715), suc(B_54_3713)) | ~E(f(B_55_3714), f(suc(B_55_3714))) | ~E(s(0), f(suc(B_53_3715))) | ~iLEQ(suc(B_54_3713), suc(B_55_3714)) | LE(f(B_53_3715), s(0)))), inference(resolution, [status(thm)], [c_129853, c_80])).
% 268.43/251.23 tff(c_144060, plain, (![B_54_3731, B_53_3732, B_53_3733]: (~E(s(0), f(B_54_3731)) | ~E(s(0), f(suc(B_54_3731))) | ~E(s(0), f(B_53_3732)) | ~E(s(0), f(B_53_3733)) | ~E(f(B_53_3733), f(suc(B_53_3733))) | ~E(f(B_54_3731), f(suc(B_54_3731))) | ~E(s(0), f(suc(suc(B_54_3731)))) | ~E(s(0), f(suc(B_53_3732))) | ~iLEQ(suc(B_53_3733), suc(B_54_3731)) | ~E(f(B_53_3732), f(suc(B_53_3732))) | ~E(s(0), f(suc(B_53_3733))) | ~iLEQ(suc(B_54_3731), suc(B_53_3732)) | LE(f(B_53_3733), s(0)) | LE(f(B_53_3732), s(0)))), inference(resolution, [status(thm)], [c_129851, c_143800])).
% 268.43/251.23 tff(c_144139, plain, (![B_54_3734, B_53_3735, B_53_3736]: (~E(s(0), f(B_54_3734)) | ~E(s(0), f(suc(B_54_3734))) | ~E(s(0), f(B_53_3735)) | ~E(f(B_54_3734), f(suc(B_54_3734))) | ~E(s(0), f(suc(suc(B_54_3734)))) | ~E(s(0), f(suc(B_53_3735))) | ~iLEQ(suc(B_53_3736), suc(B_54_3734)) | ~E(f(B_53_3735), f(suc(B_53_3735))) | ~E(s(0), f(suc(B_53_3736))) | ~iLEQ(suc(B_54_3734), suc(B_53_3735)) | LE(f(B_53_3735), s(0)) | ~E(s(0), f(B_53_3736)) | LE(f(B_53_3736), s(0)))), inference(resolution, [status(thm)], [c_132118, c_144060])).
% 268.43/251.23 tff(c_144218, plain, (![B_53_3737, B_53_3738, B_53_3739]: (~E(s(0), f(suc(B_53_3737))) | ~E(s(0), f(B_53_3738)) | ~E(s(0), f(suc(suc(B_53_3737)))) | ~E(s(0), f(suc(B_53_3738))) | ~iLEQ(suc(B_53_3739), suc(B_53_3737)) | ~E(f(B_53_3738), f(suc(B_53_3738))) | ~E(s(0), f(suc(B_53_3739))) | ~iLEQ(suc(B_53_3737), suc(B_53_3738)) | LE(f(B_53_3738), s(0)) | ~E(s(0), f(B_53_3739)) | LE(f(B_53_3739), s(0)) | ~E(s(0), f(B_53_3737)) | LE(f(B_53_3737), s(0)))), inference(resolution, [status(thm)], [c_132118, c_144139])).
% 268.43/251.23 tff(c_144237, plain, (![B_53_3740, B_53_3741, B_53_3742]: (~E(s(0), f(suc(B_53_3740))) | ~E(s(0), f(B_53_3741)) | ~E(s(0), f(suc(B_53_3741))) | ~iLEQ(suc(B_53_3742), suc(B_53_3740)) | ~E(f(B_53_3741), f(suc(B_53_3741))) | ~E(s(0), f(suc(B_53_3742))) | ~iLEQ(suc(B_53_3740), suc(B_53_3741)) | LE(f(B_53_3741), s(0)) | ~E(s(0), f(B_53_3742)) | LE(f(B_53_3742), s(0)) | ~E(s(0), f(B_53_3740)) | LE(f(B_53_3740), s(0)))), inference(resolution, [status(thm)], [c_129851, c_144218])).
% 268.43/251.23 tff(c_144254, plain, (![B_53_3743, B_53_3744, B_53_3745]: (~E(s(0), f(B_53_3743)) | ~E(s(0), f(suc(B_53_3743))) | ~iLEQ(suc(B_53_3744), suc(B_53_3745)) | ~E(f(B_53_3743), f(suc(B_53_3743))) | ~E(s(0), f(suc(B_53_3744))) | ~iLEQ(suc(B_53_3745), suc(B_53_3743)) | LE(f(B_53_3743), s(0)) | ~E(s(0), f(B_53_3744)) | LE(f(B_53_3744), s(0)) | ~E(s(0), f(B_53_3745)) | LE(f(B_53_3745), s(0)))), inference(resolution, [status(thm)], [c_129627, c_144237])).
% 268.43/251.23 tff(c_144271, plain, (![B_53_3746, B_53_3747, B_53_3748]: (~E(s(0), f(B_53_3746)) | ~iLEQ(suc(B_53_3747), suc(B_53_3748)) | ~E(f(B_53_3746), f(suc(B_53_3746))) | ~E(s(0), f(suc(B_53_3747))) | ~iLEQ(suc(B_53_3748), suc(B_53_3746)) | ~E(s(0), f(B_53_3747)) | LE(f(B_53_3747), s(0)) | ~E(s(0), f(B_53_3748)) | LE(f(B_53_3748), s(0)) | LE(f(B_53_3746), s(0)))), inference(resolution, [status(thm)], [c_129627, c_144254])).
% 268.43/251.23 tff(c_144335, plain, (![B_53_3749, B_53_3750]: (~E(s(0), f(B_53_3749)) | ~E(f(B_53_3749), f(suc(B_53_3749))) | ~E(s(0), f(suc(B_53_3750))) | ~iLEQ(suc(B_53_3750), suc(B_53_3749)) | LE(f(B_53_3749), s(0)) | ~E(s(0), f(B_53_3750)) | LE(f(B_53_3750), s(0)))), inference(resolution, [status(thm)], [c_130207, c_144271])).
% 268.43/251.23 tff(c_144414, plain, (![B_53_3751, B_53_3752]: (~E(s(0), f(suc(B_53_3751))) | ~iLEQ(suc(B_53_3751), suc(B_53_3752)) | ~E(s(0), f(B_53_3751)) | LE(f(B_53_3751), s(0)) | ~E(s(0), f(B_53_3752)) | LE(f(B_53_3752), s(0)))), inference(resolution, [status(thm)], [c_132118, c_144335])).
% 268.43/251.23 tff(c_144448, plain, (![B_53_3756, B_53_3757]: (~iLEQ(suc(B_53_3756), suc(B_53_3757)) | ~E(s(0), f(B_53_3756)) | ~E(s(0), f(B_53_3757)) | LE(f(B_53_3757), s(0)) | LE(f(B_53_3756), s(0)))), inference(resolution, [status(thm)], [c_129627, c_144414])).
% 268.43/251.23 tff(c_144533, plain, (![B_53_3758]: (~E(s(0), f(B_53_3758)) | LE(f(B_53_3758), s(0)))), inference(resolution, [status(thm)], [c_130207, c_144448])).
% 268.43/251.23 tff(c_144546, plain, (![B_53_3759]: (LE(f(B_53_3759), 0) | E(0, f(B_53_3759)) | ~E(s(0), f(B_53_3759)))), inference(resolution, [status(thm)], [c_144533, c_36])).
% 268.43/251.23 tff(c_144567, plain, (![B_23_3760]: (LE(f(B_23_3760), 0) | E(0, f(B_23_3760)))), inference(resolution, [status(thm)], [c_129642, c_144546])).
% 268.43/251.23 tff(c_34, plain, (~LE(f(z), 0)), inference(cnfTransformation, [status(thm)], [f_440])).
% 268.43/251.23 tff(c_144571, plain, (E(0, f(z))), inference(resolution, [status(thm)], [c_144567, c_34])).
% 268.43/251.23 tff(c_102, plain, (![B_60_110]: (LE(f(B_60_110), 0) | E(0, f(suc(B_60_110))) | ~LE(f(suc(B_60_110)), s(0)))), inference(cnfTransformation, [status(thm)], [f_1276])).
% 268.43/251.23 tff(c_129641, plain, (![B_60_110]: (LE(f(B_60_110), 0) | E(0, f(suc(B_60_110))) | E(s(0), f(suc(B_60_110))))), inference(resolution, [status(thm)], [c_129630, c_102])).
% 268.43/251.23 tff(c_144572, plain, (![B_60_3761]: (LE(f(B_60_3761), 0) | E(0, f(suc(B_60_3761))) | ~E(s(0), f(suc(B_60_3761))))), inference(resolution, [status(thm)], [c_144533, c_102])).
% 268.43/251.23 tff(c_144587, plain, (![B_60_110]: (LE(f(B_60_110), 0) | E(0, f(suc(B_60_110))))), inference(resolution, [status(thm)], [c_129641, c_144572])).
% 268.43/251.23 tff(c_50, plain, (![B_60_54]: (LE(f(B_60_54), 0) | E(0, f(suc(suc(B_60_54)))) | ~LE(f(suc(suc(B_60_54))), s(0)))), inference(cnfTransformation, [status(thm)], [f_615])).
% 268.43/251.23 tff(c_129640, plain, (![B_60_54]: (LE(f(B_60_54), 0) | E(0, f(suc(suc(B_60_54)))) | E(s(0), f(suc(suc(B_60_54)))))), inference(resolution, [status(thm)], [c_129630, c_50])).
% 268.43/251.23 tff(c_144594, plain, (![B_60_3763]: (LE(f(B_60_3763), 0) | E(0, f(suc(suc(B_60_3763)))) | ~E(s(0), f(suc(suc(B_60_3763)))))), inference(resolution, [status(thm)], [c_144533, c_50])).
% 268.43/251.23 tff(c_144607, plain, (![B_60_3764]: (LE(f(B_60_3764), 0) | E(0, f(suc(suc(B_60_3764)))))), inference(resolution, [status(thm)], [c_129640, c_144594])).
% 268.43/251.23 tff(c_52, plain, (![A_4_55]: (iLEQ(suc(A_4_55), suc(A_4_55)) | E(f(A_4_55), f(suc(A_4_55))) | ~E(0, f(suc(A_4_55))) | ~E(0, f(A_4_55)))), inference(cnfTransformation, [status(thm)], [f_625])).
% 268.43/251.23 tff(c_173, plain, (![A_4_139]: (iLEQ(suc(A_4_139), suc(A_4_139)) | ~E(0, f(A_4_139)) | ~E(f(A_4_139), f(suc(A_4_139))) | ~E(0, f(suc(A_4_139))) | ~E(0, f(suc(suc(A_4_139)))))), inference(cnfTransformation, [status(thm)], [f_639])).
% 268.43/251.23 tff(c_181, plain, (![A_4_55]: (~E(0, f(suc(suc(A_4_55)))) | iLEQ(suc(A_4_55), suc(A_4_55)) | ~E(0, f(suc(A_4_55))) | ~E(0, f(A_4_55)))), inference(resolution, [status(thm)], [c_52, c_173])).
% 268.43/251.23 tff(c_144610, plain, (![B_60_3764]: (iLEQ(suc(B_60_3764), suc(B_60_3764)) | ~E(0, f(suc(B_60_3764))) | ~E(0, f(B_60_3764)) | LE(f(B_60_3764), 0))), inference(resolution, [status(thm)], [c_144607, c_181])).
% 268.43/251.23 tff(c_144605, plain, (![B_60_54]: (LE(f(B_60_54), 0) | E(0, f(suc(suc(B_60_54)))))), inference(resolution, [status(thm)], [c_129640, c_144594])).
% 268.43/251.23 tff(c_144611, plain, (![B_60_3765]: (iLEQ(suc(B_60_3765), suc(B_60_3765)) | ~E(0, f(suc(B_60_3765))) | ~E(0, f(B_60_3765)) | LE(f(B_60_3765), 0))), inference(resolution, [status(thm)], [c_144607, c_181])).
% 268.43/251.23 tff(c_18, plain, (![B_62_18, B_61_17, A_4_19]: (E(f(B_62_18), f(suc(B_62_18))) | E(f(B_61_17), f(suc(B_61_17))) | E(f(A_4_19), f(suc(A_4_19))) | ~E(0, f(A_4_19)) | ~E(0, f(B_62_18)) | ~E(0, f(suc(A_4_19))) | ~E(0, f(B_61_17)) | ~E(0, f(suc(B_62_18))) | ~iLEQ(suc(A_4_19), suc(B_61_17)) | ~iLEQ(suc(B_61_17), suc(B_62_18)) | ~E(0, f(suc(B_61_17))))), inference(cnfTransformation, [status(thm)], [f_219])).
% 268.43/251.23 tff(c_144697, plain, (![B_62_3767, B_60_3768]: (E(f(B_62_3767), f(suc(B_62_3767))) | E(f(B_60_3768), f(suc(B_60_3768))) | ~E(0, f(B_62_3767)) | ~E(0, f(suc(B_62_3767))) | ~iLEQ(suc(B_60_3768), suc(B_62_3767)) | ~E(0, f(suc(B_60_3768))) | ~E(0, f(B_60_3768)) | LE(f(B_60_3768), 0))), inference(resolution, [status(thm)], [c_144611, c_18])).
% 268.43/251.23 tff(c_144703, plain, (![B_60_3764]: (E(f(B_60_3764), f(suc(B_60_3764))) | ~E(0, f(suc(B_60_3764))) | ~E(0, f(B_60_3764)) | LE(f(B_60_3764), 0))), inference(resolution, [status(thm)], [c_144610, c_144697])).
% 268.43/251.23 tff(c_144704, plain, (![B_60_3769]: (E(f(B_60_3769), f(suc(B_60_3769))) | ~E(0, f(suc(B_60_3769))) | ~E(0, f(B_60_3769)) | LE(f(B_60_3769), 0))), inference(resolution, [status(thm)], [c_144610, c_144697])).
% 268.43/251.23 tff(c_98, plain, (![A_4_106, B_61_104, B_62_105]: (~E(0, f(A_4_106)) | ~E(f(B_61_104), f(suc(B_61_104))) | ~E(0, f(suc(suc(B_61_104)))) | ~E(0, f(B_62_105)) | ~E(0, f(suc(A_4_106))) | ~E(0, f(suc(suc(B_62_105)))) | ~E(0, f(B_61_104)) | ~E(f(B_62_105), f(suc(B_62_105))) | ~E(0, f(suc(suc(A_4_106)))) | ~E(0, f(suc(B_62_105))) | ~iLEQ(suc(A_4_106), suc(B_61_104)) | ~E(f(A_4_106), f(suc(A_4_106))) | ~iLEQ(suc(B_61_104), suc(B_62_105)) | ~E(0, f(suc(B_61_104))))), inference(cnfTransformation, [status(thm)], [f_1231])).
% 268.43/251.23 tff(c_145128, plain, (![A_4_3866, B_60_3867, B_62_3868]: (~E(0, f(A_4_3866)) | ~E(0, f(suc(suc(B_60_3867)))) | ~E(0, f(B_62_3868)) | ~E(0, f(suc(A_4_3866))) | ~E(0, f(suc(suc(B_62_3868)))) | ~E(f(B_62_3868), f(suc(B_62_3868))) | ~E(0, f(suc(suc(A_4_3866)))) | ~E(0, f(suc(B_62_3868))) | ~iLEQ(suc(A_4_3866), suc(B_60_3867)) | ~E(f(A_4_3866), f(suc(A_4_3866))) | ~iLEQ(suc(B_60_3867), suc(B_62_3868)) | ~E(0, f(suc(B_60_3867))) | ~E(0, f(B_60_3867)) | LE(f(B_60_3867), 0))), inference(resolution, [status(thm)], [c_144704, c_98])).
% 268.43/251.23 tff(c_145143, plain, (![A_4_3872, B_62_3873, B_60_3874]: (~E(0, f(A_4_3872)) | ~E(0, f(B_62_3873)) | ~E(0, f(suc(A_4_3872))) | ~E(0, f(suc(suc(B_62_3873)))) | ~E(f(B_62_3873), f(suc(B_62_3873))) | ~E(0, f(suc(suc(A_4_3872)))) | ~E(0, f(suc(B_62_3873))) | ~iLEQ(suc(A_4_3872), suc(B_60_3874)) | ~E(f(A_4_3872), f(suc(A_4_3872))) | ~iLEQ(suc(B_60_3874), suc(B_62_3873)) | ~E(0, f(suc(B_60_3874))) | ~E(0, f(B_60_3874)) | LE(f(B_60_3874), 0))), inference(resolution, [status(thm)], [c_144605, c_145128])).
% 268.43/251.23 tff(c_145165, plain, (![A_4_3875, B_60_3876, B_60_3877]: (~E(0, f(A_4_3875)) | ~E(0, f(suc(A_4_3875))) | ~E(0, f(suc(suc(B_60_3876)))) | ~E(0, f(suc(suc(A_4_3875)))) | ~iLEQ(suc(A_4_3875), suc(B_60_3877)) | ~E(f(A_4_3875), f(suc(A_4_3875))) | ~iLEQ(suc(B_60_3877), suc(B_60_3876)) | ~E(0, f(suc(B_60_3877))) | ~E(0, f(B_60_3877)) | LE(f(B_60_3877), 0) | ~E(0, f(suc(B_60_3876))) | ~E(0, f(B_60_3876)) | LE(f(B_60_3876), 0))), inference(resolution, [status(thm)], [c_144703, c_145143])).
% 268.43/251.23 tff(c_145173, plain, (![A_4_3878, B_60_3879, B_60_3880]: (~E(0, f(A_4_3878)) | ~E(0, f(suc(A_4_3878))) | ~E(0, f(suc(suc(A_4_3878)))) | ~iLEQ(suc(A_4_3878), suc(B_60_3879)) | ~E(f(A_4_3878), f(suc(A_4_3878))) | ~iLEQ(suc(B_60_3879), suc(B_60_3880)) | ~E(0, f(suc(B_60_3879))) | ~E(0, f(B_60_3879)) | LE(f(B_60_3879), 0) | ~E(0, f(suc(B_60_3880))) | ~E(0, f(B_60_3880)) | LE(f(B_60_3880), 0))), inference(resolution, [status(thm)], [c_144605, c_145165])).
% 268.43/251.23 tff(c_145180, plain, (![B_60_3881, B_60_3882]: (~E(0, f(suc(suc(B_60_3881)))) | ~E(f(B_60_3881), f(suc(B_60_3881))) | ~iLEQ(suc(B_60_3881), suc(B_60_3882)) | ~E(0, f(suc(B_60_3882))) | ~E(0, f(B_60_3882)) | LE(f(B_60_3882), 0) | ~E(0, f(suc(B_60_3881))) | ~E(0, f(B_60_3881)) | LE(f(B_60_3881), 0))), inference(resolution, [status(thm)], [c_144610, c_145173])).
% 268.43/251.23 tff(c_145202, plain, (![B_60_3883, B_60_3884]: (~E(0, f(suc(suc(B_60_3883)))) | ~iLEQ(suc(B_60_3883), suc(B_60_3884)) | ~E(0, f(suc(B_60_3884))) | ~E(0, f(B_60_3884)) | LE(f(B_60_3884), 0) | ~E(0, f(suc(B_60_3883))) | ~E(0, f(B_60_3883)) | LE(f(B_60_3883), 0))), inference(resolution, [status(thm)], [c_144703, c_145180])).
% 268.43/251.23 tff(c_145210, plain, (![B_60_3885, B_60_3886]: (~iLEQ(suc(B_60_3885), suc(B_60_3886)) | ~E(0, f(suc(B_60_3886))) | ~E(0, f(B_60_3886)) | LE(f(B_60_3886), 0) | ~E(0, f(suc(B_60_3885))) | ~E(0, f(B_60_3885)) | LE(f(B_60_3885), 0))), inference(resolution, [status(thm)], [c_144605, c_145202])).
% 268.43/251.23 tff(c_145219, plain, (![B_60_3887]: (~E(0, f(suc(B_60_3887))) | ~E(0, f(B_60_3887)) | LE(f(B_60_3887), 0))), inference(resolution, [status(thm)], [c_144610, c_145210])).
% 268.43/251.23 tff(c_145228, plain, (![B_60_3888]: (~E(0, f(B_60_3888)) | LE(f(B_60_3888), 0))), inference(resolution, [status(thm)], [c_144587, c_145219])).
% 268.43/251.23 tff(c_145231, plain, (~E(0, f(z))), inference(resolution, [status(thm)], [c_145228, c_34])).
% 268.43/251.23 tff(c_145235, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_144571, c_145231])).
% 268.43/251.23 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------