%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO631-1 : TPTP v9.0.0. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n023.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:00 PM UTC 2025
% Result : Unsatisfiable 19.55s 10.59s
% Output : CNFRefutation 20.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.12 % Problem : SYO631-1 : TPTP v9.0.0. Released v7.1.0.
% 0.11/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 09:38:24 EDT 2025
% 0.13/0.34 % CPUTime :
% 19.55/10.59 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.81/10.65
% 19.81/10.65 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.81/10.66 %$ iLEQ > LE > E > #nlpp > s > g > f > 0
% 19.81/10.66
% 19.81/10.66 %Foreground sorts:
% 19.81/10.66
% 19.81/10.66
% 19.81/10.66 %Background operators:
% 19.81/10.66
% 19.81/10.66
% 19.81/10.66 %Foreground operators:
% 19.81/10.66 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 19.81/10.66 tff(s, type, s: $i > $i).
% 19.81/10.66 tff(f, type, f: $i > $i).
% 19.81/10.66 tff(g, type, g: $i > $i).
% 19.81/10.66 tff(0, type, 0: $i).
% 19.81/10.66 tff(LE, type, LE: ($i * $i) > $o).
% 19.81/10.66 tff(E, type, E: ($i * $i) > $o).
% 19.81/10.66
% 20.26/10.72 tff(f_229, axiom, (![A]: (E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A)) | LE(f(A), s(s(s(s(s(s(s(s(s(s(0))))))))))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_297, axiom, (![A_29]: iLEQ(A_29, g(A_29))), file('unknown', unknown)).
% 20.26/10.72 tff(f_54, axiom, (![A_1, B_0]: (((~LE(f(A_1), s(s(s(s(s(s(s(s(s(s(0))))))))))) | ~iLEQ(A_1, B_0)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(B_0))) | LE(f(B_0), s(s(s(s(s(s(s(s(s(0)))))))))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_102, axiom, (![A_4, B_2]: (((~LE(f(A_4), s(s(s(s(s(s(s(s(s(0)))))))))) | ~iLEQ(A_4, B_2)) | E(s(s(s(s(s(s(s(s(0)))))))), f(B_2))) | LE(f(B_2), s(s(s(s(s(s(s(s(0))))))))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_129, axiom, (![A_7, B_4]: (((~LE(f(A_7), s(s(s(s(s(s(s(s(0))))))))) | ~iLEQ(A_7, B_4)) | E(s(s(s(s(s(s(s(0))))))), f(B_4))) | LE(f(B_4), s(s(s(s(s(s(s(0)))))))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_250, axiom, (![A_10, B_6]: (((~LE(f(A_10), s(s(s(s(s(s(s(0)))))))) | ~iLEQ(A_10, B_6)) | E(s(s(s(s(s(s(0)))))), f(B_6))) | LE(f(B_6), s(s(s(s(s(s(0))))))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_84, axiom, (![A_13, B_8]: (((~LE(f(A_13), s(s(s(s(s(s(0))))))) | ~iLEQ(A_13, B_8)) | E(s(s(s(s(s(0))))), f(B_8))) | LE(f(B_8), s(s(s(s(s(0)))))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_299, axiom, (![A_29]: iLEQ(A_29, A_29)), file('unknown', unknown)).
% 20.26/10.72 tff(f_220, axiom, (![A_16, B_10]: (((~LE(f(A_16), s(s(s(s(s(0)))))) | ~iLEQ(A_16, B_10)) | E(s(s(s(s(0)))), f(B_10))) | LE(f(B_10), s(s(s(s(0))))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_295, axiom, (![A_14]: ~E(f(A_14), f(g(A_14)))), file('unknown', unknown)).
% 20.26/10.72 tff(f_198, axiom, (![A_2]: ((~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2)) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(g(A_2)))) | E(f(A_2), f(g(A_2))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_32, axiom, (![A_5]: ((~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_5)) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_5)))) | E(f(A_5), f(g(A_5))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_292, axiom, (![A_8]: ((~E(s(s(s(s(s(s(s(s(0)))))))), f(A_8)) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_8)))) | E(f(A_8), f(g(A_8))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_67, axiom, (![A_11]: ((~E(s(s(s(s(s(s(s(0))))))), f(A_11)) | ~E(s(s(s(s(s(s(s(0))))))), f(g(A_11)))) | E(f(A_11), f(g(A_11))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_115, axiom, (![A_14]: ((~E(s(s(s(s(s(s(0)))))), f(A_14)) | ~E(s(s(s(s(s(s(0)))))), f(g(A_14)))) | E(f(A_14), f(g(A_14))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_157, axiom, (![A_17]: ((~E(s(s(s(s(s(0))))), f(A_17)) | ~E(s(s(s(s(s(0))))), f(g(A_17)))) | E(f(A_17), f(g(A_17))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_44, axiom, (![A_19, B_12]: (((~LE(f(A_19), s(s(s(s(0))))) | ~iLEQ(A_19, B_12)) | E(s(s(s(0))), f(B_12))) | LE(f(B_12), s(s(s(0)))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_275, axiom, (![A_22, B_14]: (((~LE(f(A_22), s(s(s(0)))) | ~iLEQ(A_22, B_14)) | E(s(s(0)), f(B_14))) | LE(f(B_14), s(s(0))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_141, axiom, (![A_25, B_16]: (((~LE(f(A_25), s(s(0))) | ~iLEQ(A_25, B_16)) | E(s(0), f(B_16))) | LE(f(B_16), s(0)))), file('unknown', unknown)).
% 20.26/10.72 tff(f_281, axiom, (![A_30]: ~LE(f(A_30), 0)), file('unknown', unknown)).
% 20.26/10.72 tff(f_190, axiom, (![A_28, B_18]: (((~LE(f(A_28), s(0)) | ~iLEQ(A_28, B_18)) | E(0, f(B_18))) | LE(f(B_18), 0))), file('unknown', unknown)).
% 20.26/10.72 tff(f_262, axiom, (![A_20]: ((~E(s(s(s(s(0)))), f(A_20)) | ~E(s(s(s(s(0)))), f(g(A_20)))) | E(f(A_20), f(g(A_20))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_92, axiom, (![A_23]: ((~E(s(s(s(0))), f(A_23)) | ~E(s(s(s(0))), f(g(A_23)))) | E(f(A_23), f(g(A_23))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_149, axiom, (![A_26]: ((~E(s(s(0)), f(A_26)) | ~E(s(s(0)), f(g(A_26)))) | E(f(A_26), f(g(A_26))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_210, axiom, (![A_29]: ((~E(s(0), f(A_29)) | ~E(s(0), f(g(A_29)))) | E(f(A_29), f(g(A_29))))), file('unknown', unknown)).
% 20.26/10.72 tff(f_168, axiom, (![A_30]: ((~E(0, f(A_30)) | ~E(0, f(g(A_30)))) | E(f(A_30), f(g(A_30))))), file('unknown', unknown)).
% 20.26/10.72 tff(c_78, plain, (![A_47]: (LE(f(A_47), s(s(s(s(s(s(s(s(s(s(0))))))))))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(cnfTransformation, [status(thm)], [f_229])).
% 20.26/10.72 tff(c_112, plain, (![A_29_66]: (iLEQ(A_29_66, g(A_29_66)))), inference(cnfTransformation, [status(thm)], [f_297])).
% 20.26/10.72 tff(c_310, plain, (![B_0_126, A_1_127]: (LE(f(B_0_126), s(s(s(s(s(s(s(s(s(0)))))))))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(B_0_126)) | ~iLEQ(A_1_127, B_0_126) | ~LE(f(A_1_127), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(cnfTransformation, [status(thm)], [f_54])).
% 20.26/10.72 tff(c_315, plain, (![A_29_66]: (LE(f(g(A_29_66)), s(s(s(s(s(s(s(s(s(0)))))))))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_112, c_310])).
% 20.26/10.72 tff(c_296, plain, (![B_2_121, A_4_122]: (LE(f(B_2_121), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(B_2_121)) | ~iLEQ(A_4_122, B_2_121) | ~LE(f(A_4_122), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(cnfTransformation, [status(thm)], [f_102])).
% 20.26/10.72 tff(c_301, plain, (![A_29_66]: (LE(f(g(A_29_66)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_112, c_296])).
% 20.26/10.72 tff(c_289, plain, (![B_4_119, A_7_120]: (LE(f(B_4_119), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(B_4_119)) | ~iLEQ(A_7_120, B_4_119) | ~LE(f(A_7_120), s(s(s(s(s(s(s(s(0))))))))))), inference(cnfTransformation, [status(thm)], [f_129])).
% 20.26/10.72 tff(c_294, plain, (![A_29_66]: (LE(f(g(A_29_66)), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_112, c_289])).
% 20.26/10.72 tff(c_266, plain, (![B_6_113, A_10_114]: (LE(f(B_6_113), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(B_6_113)) | ~iLEQ(A_10_114, B_6_113) | ~LE(f(A_10_114), s(s(s(s(s(s(s(0)))))))))), inference(cnfTransformation, [status(thm)], [f_250])).
% 20.26/10.72 tff(c_271, plain, (![A_29_66]: (LE(f(g(A_29_66)), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_112, c_266])).
% 20.26/10.72 tff(c_258, plain, (![B_8_110, A_13_111]: (LE(f(B_8_110), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(B_8_110)) | ~iLEQ(A_13_111, B_8_110) | ~LE(f(A_13_111), s(s(s(s(s(s(0))))))))), inference(cnfTransformation, [status(thm)], [f_84])).
% 20.26/10.72 tff(c_273, plain, (![A_29_115]: (LE(f(g(A_29_115)), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(A_29_115))) | ~LE(f(A_29_115), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_112, c_258])).
% 20.26/10.72 tff(c_114, plain, (![A_29_67]: (iLEQ(A_29_67, A_29_67))), inference(cnfTransformation, [status(thm)], [f_299])).
% 20.26/10.72 tff(c_228, plain, (![B_10_101, A_16_102]: (LE(f(B_10_101), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(B_10_101)) | ~iLEQ(A_16_102, B_10_101) | ~LE(f(A_16_102), s(s(s(s(s(0)))))))), inference(cnfTransformation, [status(thm)], [f_220])).
% 20.26/10.72 tff(c_234, plain, (![A_29_67]: (LE(f(A_29_67), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(A_29_67)) | ~LE(f(A_29_67), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_114, c_228])).
% 20.26/10.72 tff(c_317, plain, (![A_29_128]: (LE(f(g(A_29_128)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_29_128))) | E(s(s(s(s(s(0))))), f(g(A_29_128))) | ~LE(f(A_29_128), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_273, c_234])).
% 20.26/10.72 tff(c_401, plain, (![A_29_144]: (LE(f(g(g(A_29_144))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(A_29_144)))) | E(s(s(s(s(s(0))))), f(g(g(A_29_144)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_144))) | ~LE(f(A_29_144), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_317])).
% 20.26/10.72 tff(c_506, plain, (![A_29_161]: (LE(f(g(g(g(A_29_161)))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(A_29_161))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_29_161))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_161)))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_161))) | ~LE(f(A_29_161), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_294, c_401])).
% 20.26/10.72 tff(c_860, plain, (![A_29_195]: (LE(f(g(g(g(g(A_29_195))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_29_195)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_29_195)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_195))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_195)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_195))) | ~LE(f(A_29_195), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_506])).
% 20.26/10.72 tff(c_1702, plain, (![A_29_249]: (LE(f(g(g(g(g(g(A_29_249)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_29_249))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_29_249))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_29_249)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_249))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_249)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_249))) | ~LE(f(A_29_249), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_860])).
% 20.26/10.72 tff(c_1742, plain, (![A_253]: (LE(f(g(g(g(g(g(A_253)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_253))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_253))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_253)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_253))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_253)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_253))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_253)))), inference(resolution, [status(thm)], [c_78, c_1702])).
% 20.26/10.72 tff(c_337, plain, (![A_29_132]: (LE(f(A_29_132), s(s(s(s(s(s(s(s(s(0)))))))))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_29_132)) | ~LE(f(A_29_132), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_114, c_310])).
% 20.26/10.72 tff(c_347, plain, (![A_134]: (LE(f(A_134), s(s(s(s(s(s(s(s(s(0)))))))))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_134)) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_134)))), inference(resolution, [status(thm)], [c_78, c_337])).
% 20.26/10.72 tff(c_110, plain, (![A_14_65]: (~E(f(A_14_65), f(g(A_14_65))))), inference(cnfTransformation, [status(thm)], [f_295])).
% 20.26/10.72 tff(c_64, plain, (![A_2_39]: (E(f(A_2_39), f(g(A_2_39))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(g(A_2_39))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_39)))), inference(cnfTransformation, [status(thm)], [f_198])).
% 20.26/10.72 tff(c_127, plain, (![A_2_39]: (~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(g(A_2_39))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_39)))), inference(negUnitSimplification, [status(thm)], [c_110, c_64])).
% 20.26/10.72 tff(c_351, plain, (![A_2_39]: (~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_39)) | LE(f(g(A_2_39)), s(s(s(s(s(s(s(s(s(0)))))))))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_39))))), inference(resolution, [status(thm)], [c_347, c_127])).
% 20.26/10.72 tff(c_867, plain, (![A_2_39]: (LE(f(g(g(g(g(g(A_2_39)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_2_39))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_2_39))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_2_39)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_39))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_39)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_39)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_39))))), inference(resolution, [status(thm)], [c_351, c_860])).
% 20.26/10.72 tff(c_1793, plain, (![A_256]: (LE(f(g(g(g(g(g(A_256)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_256))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_256))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_256)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_256))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_256)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_256))))), inference(resolution, [status(thm)], [c_1742, c_867])).
% 20.26/10.72 tff(c_342, plain, (![A_29_133]: (LE(f(g(A_29_133)), s(s(s(s(s(s(s(s(s(0)))))))))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_133))) | ~LE(f(A_29_133), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_112, c_310])).
% 20.26/10.72 tff(c_302, plain, (![A_29_67]: (LE(f(A_29_67), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(A_29_67)) | ~LE(f(A_29_67), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_114, c_296])).
% 20.26/10.72 tff(c_396, plain, (![A_29_143]: (LE(f(g(A_29_143)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_143))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_143))) | ~LE(f(A_29_143), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_342, c_302])).
% 20.26/10.72 tff(c_400, plain, (![A_47]: (LE(f(g(A_47)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(resolution, [status(thm)], [c_78, c_396])).
% 20.26/10.72 tff(c_362, plain, (![A_2_137]: (~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_137)) | LE(f(g(A_2_137)), s(s(s(s(s(s(s(s(s(0)))))))))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_137))))), inference(resolution, [status(thm)], [c_347, c_127])).
% 20.26/10.72 tff(c_416, plain, (![A_2_147]: (LE(f(g(A_2_147)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_2_147))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_147)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_147))))), inference(resolution, [status(thm)], [c_362, c_302])).
% 20.26/10.72 tff(c_425, plain, (![A_148]: (LE(f(g(A_148)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_400, c_416])).
% 20.26/10.72 tff(c_2, plain, (![A_5_1]: (E(f(A_5_1), f(g(A_5_1))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_5_1))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_5_1)))), inference(cnfTransformation, [status(thm)], [f_32])).
% 20.26/10.72 tff(c_146, plain, (![A_5_1]: (~E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_5_1))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_5_1)))), inference(negUnitSimplification, [status(thm)], [c_110, c_2])).
% 20.26/10.72 tff(c_429, plain, (![A_148]: (~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | LE(f(g(A_148)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_425, c_146])).
% 20.26/10.72 tff(c_513, plain, (![A_148]: (LE(f(g(g(g(g(A_148))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_148)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_148)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_148)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_429, c_506])).
% 20.26/10.72 tff(c_1814, plain, (![A_257]: (LE(f(g(g(g(g(g(A_257)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_257))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_257))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_257)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_257))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_257)))))), inference(resolution, [status(thm)], [c_1793, c_513])).
% 20.26/10.72 tff(c_327, plain, (![A_29_130]: (LE(f(g(A_29_130)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_130))) | ~LE(f(A_29_130), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_112, c_296])).
% 20.26/10.72 tff(c_295, plain, (![A_29_67]: (LE(f(A_29_67), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(A_29_67)) | ~LE(f(A_29_67), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_114, c_289])).
% 20.26/10.72 tff(c_382, plain, (![A_29_141]: (LE(f(g(A_29_141)), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_141))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_141))) | ~LE(f(A_29_141), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_327, c_295])).
% 20.26/10.72 tff(c_487, plain, (![A_29_158]: (LE(f(g(g(A_29_158))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_158)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_158)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_158))) | ~LE(f(A_29_158), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_382])).
% 20.26/10.72 tff(c_497, plain, (![A_160]: (LE(f(g(g(A_160))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_160)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_160)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_160))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_160)))), inference(resolution, [status(thm)], [c_78, c_487])).
% 20.26/10.72 tff(c_389, plain, (![A_2_39]: (LE(f(g(g(A_2_39))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_2_39)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_39)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_39)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_39))))), inference(resolution, [status(thm)], [c_351, c_382])).
% 20.26/10.72 tff(c_515, plain, (![A_162]: (LE(f(g(g(A_162))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_162)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_162)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_162))))), inference(resolution, [status(thm)], [c_497, c_389])).
% 20.26/10.72 tff(c_430, plain, (![A_149]: (~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_149)) | LE(f(g(A_149)), s(s(s(s(s(s(s(s(0))))))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_149))))), inference(resolution, [status(thm)], [c_425, c_146])).
% 20.26/10.72 tff(c_438, plain, (![A_149]: (LE(f(g(A_149)), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_149))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_149)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_149))))), inference(resolution, [status(thm)], [c_430, c_295])).
% 20.26/10.72 tff(c_528, plain, (![A_163]: (LE(f(g(g(A_163))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_163)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_163)))))), inference(resolution, [status(thm)], [c_515, c_438])).
% 20.26/10.72 tff(c_108, plain, (![A_8_64]: (E(f(A_8_64), f(g(A_8_64))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_8_64))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(A_8_64)))), inference(cnfTransformation, [status(thm)], [f_292])).
% 20.26/10.72 tff(c_115, plain, (![A_8_64]: (~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_8_64))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(A_8_64)))), inference(negUnitSimplification, [status(thm)], [c_110, c_108])).
% 20.26/10.72 tff(c_533, plain, (![A_164]: (~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_164))) | LE(f(g(g(A_164))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_164)))))), inference(resolution, [status(thm)], [c_528, c_115])).
% 20.26/10.72 tff(c_321, plain, (![A_29_66]: (LE(f(g(g(A_29_66))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(A_29_66)))) | E(s(s(s(s(s(0))))), f(g(g(A_29_66)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_317])).
% 20.26/10.72 tff(c_547, plain, (![A_164]: (LE(f(g(g(g(g(A_164))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_164)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_164)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_164))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_164))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_164)))))), inference(resolution, [status(thm)], [c_533, c_321])).
% 20.26/10.72 tff(c_1840, plain, (![A_259]: (LE(f(g(g(g(g(g(A_259)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_259))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_259))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_259)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_259))))))), inference(resolution, [status(thm)], [c_1814, c_547])).
% 20.26/10.72 tff(c_304, plain, (![A_29_124]: (LE(f(g(A_29_124)), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_124))) | ~LE(f(A_29_124), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_112, c_289])).
% 20.26/10.72 tff(c_272, plain, (![A_29_67]: (LE(f(A_29_67), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(A_29_67)) | ~LE(f(A_29_67), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_114, c_266])).
% 20.26/10.72 tff(c_372, plain, (![A_29_139]: (LE(f(g(A_29_139)), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_139))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_139))) | ~LE(f(A_29_139), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_304, c_272])).
% 20.26/10.72 tff(c_463, plain, (![A_29_154]: (LE(f(g(g(A_29_154))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_154)))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_154)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_154))) | ~LE(f(A_29_154), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_372])).
% 20.26/10.72 tff(c_630, plain, (![A_29_177]: (LE(f(g(g(g(A_29_177)))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_177))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_177))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_177)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_177))) | ~LE(f(A_29_177), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_463])).
% 20.26/10.72 tff(c_634, plain, (![A_47]: (LE(f(g(g(g(A_47)))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_47))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_47))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_47)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(resolution, [status(thm)], [c_78, c_630])).
% 20.26/10.72 tff(c_691, plain, (![A_2_182]: (LE(f(g(g(g(A_2_182)))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_2_182))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_182))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_182)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_182)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_182))))), inference(resolution, [status(thm)], [c_351, c_463])).
% 20.26/10.72 tff(c_700, plain, (![A_183]: (LE(f(g(g(g(A_183)))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_183))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_183))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_183)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_183))))), inference(resolution, [status(thm)], [c_634, c_691])).
% 20.26/10.72 tff(c_308, plain, (![A_29_124]: (LE(f(g(A_29_124)), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_124))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_124))) | ~LE(f(A_29_124), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_304, c_272])).
% 20.26/10.72 tff(c_437, plain, (![A_149]: (LE(f(g(g(A_149))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_149)))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_149)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_149)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_149))))), inference(resolution, [status(thm)], [c_430, c_308])).
% 20.26/10.72 tff(c_717, plain, (![A_184]: (LE(f(g(g(g(A_184)))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_184))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_184))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_184)))))), inference(resolution, [status(thm)], [c_700, c_437])).
% 20.26/10.72 tff(c_549, plain, (![A_164]: (LE(f(g(g(A_164))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_164)))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_164))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_164)))))), inference(resolution, [status(thm)], [c_533, c_272])).
% 20.26/10.72 tff(c_734, plain, (![A_185]: (LE(f(g(g(g(A_185)))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_185))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_185))))))), inference(resolution, [status(thm)], [c_717, c_549])).
% 20.26/10.72 tff(c_14, plain, (![A_11_9]: (E(f(A_11_9), f(g(A_11_9))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(A_11_9))) | ~E(s(s(s(s(s(s(s(0))))))), f(A_11_9)))), inference(cnfTransformation, [status(thm)], [f_67])).
% 20.26/10.72 tff(c_143, plain, (![A_11_9]: (~E(s(s(s(s(s(s(s(0))))))), f(g(A_11_9))) | ~E(s(s(s(s(s(s(s(0))))))), f(A_11_9)))), inference(negUnitSimplification, [status(thm)], [c_110, c_14])).
% 20.26/10.72 tff(c_739, plain, (![A_186]: (~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | LE(f(g(g(g(A_186)))), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_734, c_143])).
% 20.26/10.72 tff(c_277, plain, (![A_29_115]: (LE(f(g(A_29_115)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_29_115))) | E(s(s(s(s(s(0))))), f(g(A_29_115))) | ~LE(f(A_29_115), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_273, c_234])).
% 20.26/10.72 tff(c_766, plain, (![A_186]: (LE(f(g(g(g(g(A_186))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_186)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_186)))))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_739, c_277])).
% 20.26/10.72 tff(c_1861, plain, (![A_260]: (LE(f(g(g(g(g(g(A_260)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_260))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_260))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_260)))))))), inference(resolution, [status(thm)], [c_1840, c_766])).
% 20.26/10.72 tff(c_279, plain, (![A_29_117]: (LE(f(g(A_29_117)), s(s(s(s(s(s(0))))))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_117))) | ~LE(f(A_29_117), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_112, c_266])).
% 20.26/10.72 tff(c_264, plain, (![A_29_67]: (LE(f(A_29_67), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(A_29_67)) | ~LE(f(A_29_67), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_114, c_258])).
% 20.26/10.72 tff(c_357, plain, (![A_29_136]: (LE(f(g(A_29_136)), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(A_29_136))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_136))) | ~LE(f(A_29_136), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_279, c_264])).
% 20.26/10.72 tff(c_449, plain, (![A_29_152]: (LE(f(g(g(A_29_152))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(A_29_152)))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_152)))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_152))) | ~LE(f(A_29_152), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_294, c_357])).
% 20.26/10.72 tff(c_575, plain, (![A_29_170]: (LE(f(g(g(g(A_29_170)))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_29_170))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_170))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_170)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_170))) | ~LE(f(A_29_170), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_449])).
% 20.26/10.72 tff(c_1046, plain, (![A_29_209]: (LE(f(g(g(g(g(A_29_209))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_29_209)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_29_209)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_209))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_209)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_209))) | ~LE(f(A_29_209), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_575])).
% 20.26/10.72 tff(c_1050, plain, (![A_47]: (LE(f(g(g(g(g(A_47))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_47)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_47)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_47))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_47)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(resolution, [status(thm)], [c_78, c_1046])).
% 20.26/10.72 tff(c_1178, plain, (![A_2_217]: (LE(f(g(g(g(g(A_2_217))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_2_217)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_2_217)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_217))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_217)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_217)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_217))))), inference(resolution, [status(thm)], [c_351, c_575])).
% 20.26/10.72 tff(c_1187, plain, (![A_218]: (LE(f(g(g(g(g(A_218))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_218)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_218)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_218))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_218)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_218))))), inference(resolution, [status(thm)], [c_1050, c_1178])).
% 20.26/10.72 tff(c_456, plain, (![A_148]: (LE(f(g(g(g(A_148)))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_148)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_429, c_449])).
% 20.26/10.72 tff(c_1208, plain, (![A_219]: (LE(f(g(g(g(g(A_219))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_219)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_219)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_219))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_219)))))), inference(resolution, [status(thm)], [c_1187, c_456])).
% 20.26/10.72 tff(c_283, plain, (![A_29_117]: (LE(f(g(A_29_117)), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(A_29_117))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_117))) | ~LE(f(A_29_117), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_279, c_264])).
% 20.26/10.72 tff(c_548, plain, (![A_164]: (LE(f(g(g(g(A_164)))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_164))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_164))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_164))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_164)))))), inference(resolution, [status(thm)], [c_533, c_283])).
% 20.26/10.72 tff(c_1229, plain, (![A_220]: (LE(f(g(g(g(g(A_220))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_220)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_220)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_220))))))), inference(resolution, [status(thm)], [c_1208, c_548])).
% 20.26/10.72 tff(c_767, plain, (![A_186]: (LE(f(g(g(g(A_186)))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_186))))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_739, c_264])).
% 20.26/10.72 tff(c_1263, plain, (![A_222]: (LE(f(g(g(g(g(A_222))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_222)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_222)))))))), inference(resolution, [status(thm)], [c_1229, c_767])).
% 20.26/10.72 tff(c_32, plain, (![A_14_20]: (E(f(A_14_20), f(g(A_14_20))) | ~E(s(s(s(s(s(s(0)))))), f(g(A_14_20))) | ~E(s(s(s(s(s(s(0)))))), f(A_14_20)))), inference(cnfTransformation, [status(thm)], [f_115])).
% 20.26/10.72 tff(c_138, plain, (![A_14_20]: (~E(s(s(s(s(s(s(0)))))), f(g(A_14_20))) | ~E(s(s(s(s(s(s(0)))))), f(A_14_20)))), inference(negUnitSimplification, [status(thm)], [c_110, c_32])).
% 20.26/10.72 tff(c_1276, plain, (![A_223]: (~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_223))))) | LE(f(g(g(g(g(A_223))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_223)))))))), inference(resolution, [status(thm)], [c_1263, c_138])).
% 20.26/10.72 tff(c_1300, plain, (![A_223]: (LE(f(g(g(g(g(A_223))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_223)))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_223))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_223)))))))), inference(resolution, [status(thm)], [c_1276, c_234])).
% 20.26/10.72 tff(c_1888, plain, (![A_260]: (LE(f(g(g(g(g(g(A_260)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_260))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_260))))))))), inference(resolution, [status(thm)], [c_1861, c_1300])).
% 20.26/10.72 tff(c_1890, plain, (![A_261]: (LE(f(g(g(g(g(g(A_261)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_261))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_261))))))))), inference(resolution, [status(thm)], [c_1861, c_1300])).
% 20.26/10.72 tff(c_46, plain, (![A_17_29]: (E(f(A_17_29), f(g(A_17_29))) | ~E(s(s(s(s(s(0))))), f(g(A_17_29))) | ~E(s(s(s(s(s(0))))), f(A_17_29)))), inference(cnfTransformation, [status(thm)], [f_157])).
% 20.26/10.72 tff(c_133, plain, (![A_17_29]: (~E(s(s(s(s(s(0))))), f(g(A_17_29))) | ~E(s(s(s(s(s(0))))), f(A_17_29)))), inference(negUnitSimplification, [status(thm)], [c_110, c_46])).
% 20.26/10.72 tff(c_1903, plain, (![A_262]: (~E(s(s(s(s(s(0))))), f(g(g(g(g(A_262)))))) | LE(f(g(g(g(g(g(A_262)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_262))))))))), inference(resolution, [status(thm)], [c_1890, c_133])).
% 20.26/10.72 tff(c_209, plain, (![B_12_95, A_19_96]: (LE(f(B_12_95), s(s(s(0)))) | E(s(s(s(0))), f(B_12_95)) | ~iLEQ(A_19_96, B_12_95) | ~LE(f(A_19_96), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_44])).
% 20.26/10.72 tff(c_214, plain, (![A_29_66]: (LE(f(g(A_29_66)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_112, c_209])).
% 20.26/10.72 tff(c_186, plain, (![B_14_89, A_22_90]: (LE(f(B_14_89), s(s(0))) | E(s(s(0)), f(B_14_89)) | ~iLEQ(A_22_90, B_14_89) | ~LE(f(A_22_90), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_275])).
% 20.26/10.72 tff(c_194, plain, (![A_29_92]: (LE(f(g(A_29_92)), s(s(0))) | E(s(s(0)), f(g(A_29_92))) | ~LE(f(A_29_92), s(s(s(0)))))), inference(resolution, [status(thm)], [c_112, c_186])).
% 20.26/10.72 tff(c_162, plain, (![B_16_78, A_25_79]: (LE(f(B_16_78), s(0)) | E(s(0), f(B_16_78)) | ~iLEQ(A_25_79, B_16_78) | ~LE(f(A_25_79), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_141])).
% 20.26/10.72 tff(c_173, plain, (![A_29_84]: (LE(f(g(A_29_84)), s(0)) | E(s(0), f(g(A_29_84))) | ~LE(f(A_29_84), s(s(0))))), inference(resolution, [status(thm)], [c_112, c_162])).
% 20.26/10.72 tff(c_104, plain, (![A_30_62]: (~LE(f(A_30_62), 0))), inference(cnfTransformation, [status(thm)], [f_281])).
% 20.26/10.72 tff(c_62, plain, (![B_18_38, A_28_37]: (LE(f(B_18_38), 0) | E(0, f(B_18_38)) | ~iLEQ(A_28_37, B_18_38) | ~LE(f(A_28_37), s(0)))), inference(cnfTransformation, [status(thm)], [f_190])).
% 20.26/10.72 tff(c_153, plain, (![B_18_74, A_28_75]: (E(0, f(B_18_74)) | ~iLEQ(A_28_75, B_18_74) | ~LE(f(A_28_75), s(0)))), inference(negUnitSimplification, [status(thm)], [c_104, c_62])).
% 20.26/10.72 tff(c_158, plain, (![A_29_66]: (E(0, f(g(A_29_66))) | ~LE(f(A_29_66), s(0)))), inference(resolution, [status(thm)], [c_112, c_153])).
% 20.26/10.72 tff(c_180, plain, (![A_29_84]: (E(0, f(g(g(A_29_84)))) | E(s(0), f(g(A_29_84))) | ~LE(f(A_29_84), s(s(0))))), inference(resolution, [status(thm)], [c_173, c_158])).
% 20.26/10.72 tff(c_247, plain, (![A_29_107]: (E(0, f(g(g(g(A_29_107))))) | E(s(0), f(g(g(A_29_107)))) | E(s(s(0)), f(g(A_29_107))) | ~LE(f(A_29_107), s(s(s(0)))))), inference(resolution, [status(thm)], [c_194, c_180])).
% 20.26/10.72 tff(c_251, plain, (![A_29_66]: (E(0, f(g(g(g(g(A_29_66)))))) | E(s(0), f(g(g(g(A_29_66))))) | E(s(s(0)), f(g(g(A_29_66)))) | E(s(s(s(0))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_214, c_247])).
% 20.26/10.72 tff(c_2079, plain, (![A_274]: (E(0, f(g(g(g(g(g(g(g(g(g(A_274))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_274)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_274))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_274)))))))) | ~E(s(s(s(s(s(0))))), f(g(g(g(g(A_274)))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_274))))))))), inference(resolution, [status(thm)], [c_1903, c_251])).
% 20.26/10.72 tff(c_2086, plain, (![A_260]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_260)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_260))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_260)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_260))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_260)))))))) | LE(f(g(g(g(g(g(A_260)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_260))))))))), inference(resolution, [status(thm)], [c_1888, c_2079])).
% 20.26/10.72 tff(c_263, plain, (![A_29_66]: (LE(f(g(A_29_66)), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_112, c_258])).
% 20.26/10.72 tff(c_236, plain, (![A_29_104]: (LE(f(g(A_29_104)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_29_104))) | ~LE(f(A_29_104), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_112, c_228])).
% 20.26/10.72 tff(c_215, plain, (![A_29_67]: (LE(f(A_29_67), s(s(s(0)))) | E(s(s(s(0))), f(A_29_67)) | ~LE(f(A_29_67), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_114, c_209])).
% 20.26/10.72 tff(c_284, plain, (![A_29_118]: (LE(f(g(A_29_118)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_29_118))) | E(s(s(s(s(0)))), f(g(A_29_118))) | ~LE(f(A_29_118), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_236, c_215])).
% 20.26/10.72 tff(c_377, plain, (![A_29_140]: (LE(f(g(g(A_29_140))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(A_29_140)))) | E(s(s(s(s(0)))), f(g(g(A_29_140)))) | E(s(s(s(s(s(0))))), f(g(A_29_140))) | ~LE(f(A_29_140), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_284])).
% 20.26/10.72 tff(c_477, plain, (![A_29_156]: (LE(f(g(g(g(A_29_156)))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(A_29_156))))) | E(s(s(s(s(0)))), f(g(g(g(A_29_156))))) | E(s(s(s(s(s(0))))), f(g(g(A_29_156)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_156))) | ~LE(f(A_29_156), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_377])).
% 20.26/10.72 tff(c_768, plain, (![A_29_187]: (LE(f(g(g(g(g(A_29_187))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(A_29_187)))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_29_187)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_29_187))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_187)))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_187))) | ~LE(f(A_29_187), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_294, c_477])).
% 20.26/10.72 tff(c_1319, plain, (![A_29_226]: (LE(f(g(g(g(g(g(A_29_226)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_29_226))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_29_226))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_29_226)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_226))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_226)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_226))) | ~LE(f(A_29_226), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_768])).
% 20.26/10.72 tff(c_2689, plain, (![A_29_304]: (LE(f(g(g(g(g(g(g(A_29_304))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_29_304)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_29_304)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_29_304))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_29_304)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_304))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_304)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_304))) | ~LE(f(A_29_304), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_1319])).
% 20.26/10.72 tff(c_2693, plain, (![A_47]: (LE(f(g(g(g(g(g(g(A_47))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_47)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_47)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_47))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_47)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_47))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_47)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(resolution, [status(thm)], [c_78, c_2689])).
% 20.26/10.72 tff(c_2882, plain, (![A_2_313]: (LE(f(g(g(g(g(g(g(A_2_313))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_2_313)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_2_313)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_2_313))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_2_313)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_313))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_313)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_313)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_313))))), inference(resolution, [status(thm)], [c_351, c_1319])).
% 20.26/10.72 tff(c_3102, plain, (![A_325]: (LE(f(g(g(g(g(g(g(A_325))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_325)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_325)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_325))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_325)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_325))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_325)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_325))))), inference(resolution, [status(thm)], [c_2693, c_2882])).
% 20.26/10.72 tff(c_779, plain, (![A_148]: (LE(f(g(g(g(g(g(A_148)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_148))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_148))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_148)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_148)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_429, c_768])).
% 20.26/10.72 tff(c_3131, plain, (![A_326]: (LE(f(g(g(g(g(g(g(A_326))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_326)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_326)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_326))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_326)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_326))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_326)))))), inference(resolution, [status(thm)], [c_3102, c_779])).
% 20.26/10.72 tff(c_381, plain, (![A_29_66]: (LE(f(g(g(g(A_29_66)))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(A_29_66))))) | E(s(s(s(s(0)))), f(g(g(g(A_29_66))))) | E(s(s(s(s(s(0))))), f(g(g(A_29_66)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_377])).
% 20.26/10.72 tff(c_546, plain, (![A_164]: (LE(f(g(g(g(g(g(A_164)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_164))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_164))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_164)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_164))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_164))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_164)))))), inference(resolution, [status(thm)], [c_533, c_381])).
% 20.26/10.72 tff(c_3156, plain, (![A_327]: (LE(f(g(g(g(g(g(g(A_327))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_327)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_327)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_327))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_327)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_327))))))), inference(resolution, [status(thm)], [c_3131, c_546])).
% 20.26/10.72 tff(c_288, plain, (![A_29_66]: (LE(f(g(g(A_29_66))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(A_29_66)))) | E(s(s(s(s(0)))), f(g(g(A_29_66)))) | E(s(s(s(s(s(0))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_284])).
% 20.26/10.72 tff(c_765, plain, (![A_186]: (LE(f(g(g(g(g(g(A_186)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_186))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_186))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_186)))))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_739, c_288])).
% 20.26/10.72 tff(c_3189, plain, (![A_328]: (LE(f(g(g(g(g(g(g(A_328))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_328)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_328)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_328))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_328)))))))), inference(resolution, [status(thm)], [c_3156, c_765])).
% 20.26/10.72 tff(c_240, plain, (![A_29_104]: (LE(f(g(A_29_104)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_29_104))) | E(s(s(s(s(0)))), f(g(A_29_104))) | ~LE(f(A_29_104), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_236, c_215])).
% 20.26/10.72 tff(c_1299, plain, (![A_223]: (LE(f(g(g(g(g(g(A_223)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_223))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_223))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_223))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_223)))))))), inference(resolution, [status(thm)], [c_1276, c_240])).
% 20.26/10.72 tff(c_3218, plain, (![A_329]: (LE(f(g(g(g(g(g(g(A_329))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_329)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_329)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_329))))))))), inference(resolution, [status(thm)], [c_3189, c_1299])).
% 20.26/10.72 tff(c_1923, plain, (![A_262]: (LE(f(g(g(g(g(g(A_262)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_262))))))) | ~E(s(s(s(s(s(0))))), f(g(g(g(g(A_262)))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_262))))))))), inference(resolution, [status(thm)], [c_1903, c_215])).
% 20.26/10.72 tff(c_3243, plain, (![A_330]: (LE(f(g(g(g(g(g(g(A_330))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_330)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_330)))))))))), inference(resolution, [status(thm)], [c_3218, c_1923])).
% 20.26/10.72 tff(c_96, plain, (![A_20_57]: (E(f(A_20_57), f(g(A_20_57))) | ~E(s(s(s(s(0)))), f(g(A_20_57))) | ~E(s(s(s(s(0)))), f(A_20_57)))), inference(cnfTransformation, [status(thm)], [f_262])).
% 20.26/10.72 tff(c_116, plain, (![A_20_57]: (~E(s(s(s(s(0)))), f(g(A_20_57))) | ~E(s(s(s(s(0)))), f(A_20_57)))), inference(negUnitSimplification, [status(thm)], [c_110, c_96])).
% 20.26/10.72 tff(c_3292, plain, (![A_331]: (~E(s(s(s(s(0)))), f(g(g(g(g(g(A_331))))))) | LE(f(g(g(g(g(g(g(A_331))))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_331)))))))))), inference(resolution, [status(thm)], [c_3243, c_116])).
% 20.26/10.72 tff(c_204, plain, (![A_29_92]: (E(0, f(g(g(g(A_29_92))))) | E(s(0), f(g(g(A_29_92)))) | E(s(s(0)), f(g(A_29_92))) | ~LE(f(A_29_92), s(s(s(0)))))), inference(resolution, [status(thm)], [c_194, c_180])).
% 20.26/10.72 tff(c_3384, plain, (![A_335]: (E(0, f(g(g(g(g(g(g(g(g(g(A_335))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_335)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_335))))))))) | ~E(s(s(s(s(0)))), f(g(g(g(g(g(A_335))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_335)))))))))), inference(resolution, [status(thm)], [c_3292, c_204])).
% 20.26/10.72 tff(c_3404, plain, (![A_260]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_260)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_260))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_260)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_260))))))))) | LE(f(g(g(g(g(g(A_260)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_260))))))))), inference(resolution, [status(thm)], [c_2086, c_3384])).
% 20.26/10.72 tff(c_233, plain, (![A_29_66]: (LE(f(g(A_29_66)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_112, c_228])).
% 20.26/10.72 tff(c_218, plain, (![A_29_99]: (LE(f(g(A_29_99)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_29_99))) | ~LE(f(A_29_99), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_112, c_209])).
% 20.26/10.72 tff(c_192, plain, (![A_29_67]: (LE(f(A_29_67), s(s(0))) | E(s(s(0)), f(A_29_67)) | ~LE(f(A_29_67), s(s(s(0)))))), inference(resolution, [status(thm)], [c_114, c_186])).
% 20.26/10.72 tff(c_253, plain, (![A_29_109]: (LE(f(g(A_29_109)), s(s(0))) | E(s(s(0)), f(g(A_29_109))) | E(s(s(s(0))), f(g(A_29_109))) | ~LE(f(A_29_109), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_218, c_192])).
% 20.26/10.72 tff(c_367, plain, (![A_29_138]: (LE(f(g(g(A_29_138))), s(s(0))) | E(s(s(0)), f(g(g(A_29_138)))) | E(s(s(s(0))), f(g(g(A_29_138)))) | E(s(s(s(s(0)))), f(g(A_29_138))) | ~LE(f(A_29_138), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_253])).
% 20.26/10.72 tff(c_458, plain, (![A_29_153]: (LE(f(g(g(g(A_29_153)))), s(s(0))) | E(s(s(0)), f(g(g(g(A_29_153))))) | E(s(s(s(0))), f(g(g(g(A_29_153))))) | E(s(s(s(s(0)))), f(g(g(A_29_153)))) | E(s(s(s(s(s(0))))), f(g(A_29_153))) | ~LE(f(A_29_153), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_367])).
% 20.26/10.72 tff(c_589, plain, (![A_29_172]: (LE(f(g(g(g(g(A_29_172))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(A_29_172)))))) | E(s(s(s(0))), f(g(g(g(g(A_29_172)))))) | E(s(s(s(s(0)))), f(g(g(g(A_29_172))))) | E(s(s(s(s(s(0))))), f(g(g(A_29_172)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_172))) | ~LE(f(A_29_172), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_458])).
% 20.26/10.72 tff(c_953, plain, (![A_29_204]: (LE(f(g(g(g(g(g(A_29_204)))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(A_29_204))))))) | E(s(s(s(0))), f(g(g(g(g(g(A_29_204))))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_29_204)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_29_204))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_204)))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_204))) | ~LE(f(A_29_204), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_294, c_589])).
% 20.26/10.72 tff(c_2200, plain, (![A_29_283]: (LE(f(g(g(g(g(g(g(A_29_283))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_29_283)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_29_283)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_29_283))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_29_283)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_283))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_283)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_283))) | ~LE(f(A_29_283), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_953])).
% 20.26/10.72 tff(c_4397, plain, (![A_29_388]: (LE(f(g(g(g(g(g(g(g(A_29_388)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_29_388))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_29_388))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_29_388)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_29_388))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_29_388)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_388))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_388)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_388))) | ~LE(f(A_29_388), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_2200])).
% 20.26/10.72 tff(c_4402, plain, (![A_389]: (LE(f(g(g(g(g(g(g(g(A_389)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_389))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_389))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_389)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_389))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_389)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_389))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_389)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_389))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_389)))), inference(resolution, [status(thm)], [c_78, c_4397])).
% 20.26/10.72 tff(c_2207, plain, (![A_2_39]: (LE(f(g(g(g(g(g(g(g(A_2_39)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_2_39))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_2_39))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_2_39)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_2_39))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_2_39)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_39))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_39)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_39)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_39))))), inference(resolution, [status(thm)], [c_351, c_2200])).
% 20.26/10.72 tff(c_4420, plain, (![A_391]: (LE(f(g(g(g(g(g(g(g(A_391)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_391))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_391))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_391)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_391))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_391)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_391))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_391)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_391))))), inference(resolution, [status(thm)], [c_4402, c_2207])).
% 20.26/10.72 tff(c_960, plain, (![A_148]: (LE(f(g(g(g(g(g(g(A_148))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_148)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_148)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_148))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_148)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_148)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_429, c_953])).
% 20.26/10.72 tff(c_7531, plain, (![A_522]: (LE(f(g(g(g(g(g(g(g(A_522)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_522))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_522))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_522)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_522))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_522)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_522))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_522)))))), inference(resolution, [status(thm)], [c_4420, c_960])).
% 20.26/10.72 tff(c_532, plain, (![A_163]: (~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_163))) | LE(f(g(g(A_163))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_163)))))), inference(resolution, [status(thm)], [c_528, c_115])).
% 20.26/10.72 tff(c_596, plain, (![A_163]: (LE(f(g(g(g(g(g(g(A_163))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_163)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_163)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_163))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_163)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_163))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_163))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_163)))))), inference(resolution, [status(thm)], [c_532, c_589])).
% 20.26/10.72 tff(c_7568, plain, (![A_523]: (LE(f(g(g(g(g(g(g(g(A_523)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_523))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_523))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_523)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_523))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_523)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_523))))))), inference(resolution, [status(thm)], [c_7531, c_596])).
% 20.26/10.72 tff(c_371, plain, (![A_29_66]: (LE(f(g(g(g(A_29_66)))), s(s(0))) | E(s(s(0)), f(g(g(g(A_29_66))))) | E(s(s(s(0))), f(g(g(g(A_29_66))))) | E(s(s(s(s(0)))), f(g(g(A_29_66)))) | E(s(s(s(s(s(0))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_367])).
% 20.26/10.72 tff(c_764, plain, (![A_186]: (LE(f(g(g(g(g(g(g(A_186))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_186)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_186)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_186))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_186)))))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_739, c_371])).
% 20.26/10.72 tff(c_7601, plain, (![A_524]: (LE(f(g(g(g(g(g(g(g(A_524)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_524))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_524))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_524)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_524))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_524)))))))), inference(resolution, [status(thm)], [c_7568, c_764])).
% 20.26/10.72 tff(c_257, plain, (![A_29_66]: (LE(f(g(g(A_29_66))), s(s(0))) | E(s(s(0)), f(g(g(A_29_66)))) | E(s(s(s(0))), f(g(g(A_29_66)))) | E(s(s(s(s(0)))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_253])).
% 20.26/10.72 tff(c_1298, plain, (![A_223]: (LE(f(g(g(g(g(g(g(A_223))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_223)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_223)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_223))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_223))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_223)))))))), inference(resolution, [status(thm)], [c_1276, c_257])).
% 20.26/10.72 tff(c_7630, plain, (![A_525]: (LE(f(g(g(g(g(g(g(g(A_525)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_525))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_525))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_525)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_525))))))))), inference(resolution, [status(thm)], [c_7601, c_1298])).
% 20.26/10.72 tff(c_222, plain, (![A_29_99]: (LE(f(g(A_29_99)), s(s(0))) | E(s(s(0)), f(g(A_29_99))) | E(s(s(s(0))), f(g(A_29_99))) | ~LE(f(A_29_99), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_218, c_192])).
% 20.26/10.72 tff(c_1922, plain, (![A_262]: (LE(f(g(g(g(g(g(g(A_262))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_262)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_262)))))))) | ~E(s(s(s(s(s(0))))), f(g(g(g(g(A_262)))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_262))))))))), inference(resolution, [status(thm)], [c_1903, c_222])).
% 20.26/10.72 tff(c_7708, plain, (![A_527]: (LE(f(g(g(g(g(g(g(g(A_527)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_527))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_527))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_527)))))))))), inference(resolution, [status(thm)], [c_7630, c_1922])).
% 20.26/10.72 tff(c_3308, plain, (![A_331]: (LE(f(g(g(g(g(g(g(A_331))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_331)))))))) | ~E(s(s(s(s(0)))), f(g(g(g(g(g(A_331))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_331)))))))))), inference(resolution, [status(thm)], [c_3292, c_192])).
% 20.26/10.72 tff(c_7729, plain, (![A_528]: (LE(f(g(g(g(g(g(g(g(A_528)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_528))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_528))))))))))), inference(resolution, [status(thm)], [c_7708, c_3308])).
% 20.26/10.72 tff(c_24, plain, (![A_23_15]: (E(f(A_23_15), f(g(A_23_15))) | ~E(s(s(s(0))), f(g(A_23_15))) | ~E(s(s(s(0))), f(A_23_15)))), inference(cnfTransformation, [status(thm)], [f_92])).
% 20.26/10.72 tff(c_140, plain, (![A_23_15]: (~E(s(s(s(0))), f(g(A_23_15))) | ~E(s(s(s(0))), f(A_23_15)))), inference(negUnitSimplification, [status(thm)], [c_110, c_24])).
% 20.26/10.72 tff(c_7810, plain, (![A_529]: (~E(s(s(s(0))), f(g(g(g(g(g(g(A_529)))))))) | LE(f(g(g(g(g(g(g(g(A_529)))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_529))))))))))), inference(resolution, [status(thm)], [c_7729, c_140])).
% 20.26/10.72 tff(c_7897, plain, (![A_532]: (E(0, f(g(g(g(g(g(g(g(g(g(A_532))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_532)))))))))) | ~E(s(s(s(0))), f(g(g(g(g(g(g(A_532)))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_532))))))))))), inference(resolution, [status(thm)], [c_7810, c_180])).
% 20.26/10.72 tff(c_7928, plain, (![A_260]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_260)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_260))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_260)))))))))) | LE(f(g(g(g(g(g(A_260)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_260))))))))), inference(resolution, [status(thm)], [c_3404, c_7897])).
% 20.26/10.72 tff(c_168, plain, (![A_29_67]: (LE(f(A_29_67), s(0)) | E(s(0), f(A_29_67)) | ~LE(f(A_29_67), s(s(0))))), inference(resolution, [status(thm)], [c_114, c_162])).
% 20.26/10.72 tff(c_223, plain, (![A_29_100]: (LE(f(g(A_29_100)), s(0)) | E(s(0), f(g(A_29_100))) | E(s(s(0)), f(g(A_29_100))) | ~LE(f(A_29_100), s(s(s(0)))))), inference(resolution, [status(thm)], [c_194, c_168])).
% 20.26/10.72 tff(c_322, plain, (![A_29_129]: (LE(f(g(g(A_29_129))), s(0)) | E(s(0), f(g(g(A_29_129)))) | E(s(s(0)), f(g(g(A_29_129)))) | E(s(s(s(0))), f(g(A_29_129))) | ~LE(f(A_29_129), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_214, c_223])).
% 20.26/10.72 tff(c_391, plain, (![A_29_142]: (LE(f(g(g(g(A_29_142)))), s(0)) | E(s(0), f(g(g(g(A_29_142))))) | E(s(s(0)), f(g(g(g(A_29_142))))) | E(s(s(s(0))), f(g(g(A_29_142)))) | E(s(s(s(s(0)))), f(g(A_29_142))) | ~LE(f(A_29_142), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_322])).
% 20.26/10.72 tff(c_565, plain, (![A_29_168]: (LE(f(g(g(g(g(A_29_168))))), s(0)) | E(s(0), f(g(g(g(g(A_29_168)))))) | E(s(s(0)), f(g(g(g(g(A_29_168)))))) | E(s(s(s(0))), f(g(g(g(A_29_168))))) | E(s(s(s(s(0)))), f(g(g(A_29_168)))) | E(s(s(s(s(s(0))))), f(g(A_29_168))) | ~LE(f(A_29_168), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_391])).
% 20.26/10.72 tff(c_874, plain, (![A_29_197]: (LE(f(g(g(g(g(g(A_29_197)))))), s(0)) | E(s(0), f(g(g(g(g(g(A_29_197))))))) | E(s(s(0)), f(g(g(g(g(g(A_29_197))))))) | E(s(s(s(0))), f(g(g(g(g(A_29_197)))))) | E(s(s(s(s(0)))), f(g(g(g(A_29_197))))) | E(s(s(s(s(s(0))))), f(g(g(A_29_197)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_197))) | ~LE(f(A_29_197), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_565])).
% 20.26/10.72 tff(c_2088, plain, (![A_29_275]: (LE(f(g(g(g(g(g(g(A_29_275))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(A_29_275)))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_29_275)))))))) | E(s(s(s(0))), f(g(g(g(g(g(A_29_275))))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_29_275)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_29_275))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_275)))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_275))) | ~LE(f(A_29_275), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_294, c_874])).
% 20.26/10.72 tff(c_3725, plain, (![A_29_364]: (LE(f(g(g(g(g(g(g(g(A_29_364)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_29_364))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_29_364))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_29_364)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_29_364))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_29_364)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_364))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_364)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_364))) | ~LE(f(A_29_364), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_2088])).
% 20.26/10.72 tff(c_5531, plain, (![A_29_434]: (LE(f(g(g(g(g(g(g(g(g(A_29_434))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_29_434)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_29_434)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_29_434))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_29_434)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_29_434))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_29_434)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_434))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_434)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_434))) | ~LE(f(A_29_434), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_3725])).
% 20.26/10.72 tff(c_5535, plain, (![A_47]: (LE(f(g(g(g(g(g(g(g(g(A_47))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_47)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_47)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_47))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_47)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_47))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_47)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_47))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_47)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(resolution, [status(thm)], [c_78, c_5531])).
% 20.26/10.72 tff(c_5639, plain, (![A_2_438]: (LE(f(g(g(g(g(g(g(g(g(A_2_438))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_2_438)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_2_438)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_2_438))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_2_438)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_2_438))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_2_438)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_438))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_438)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_438)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_438))))), inference(resolution, [status(thm)], [c_351, c_3725])).
% 20.26/10.72 tff(c_9217, plain, (![A_592]: (LE(f(g(g(g(g(g(g(g(g(A_592))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_592)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_592)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_592))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_592)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_592))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_592)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_592))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_592)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_592))))), inference(resolution, [status(thm)], [c_5535, c_5639])).
% 20.26/10.72 tff(c_2095, plain, (![A_148]: (LE(f(g(g(g(g(g(g(g(A_148)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_148))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_148))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_148)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_148))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_148)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_148)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_429, c_2088])).
% 20.26/10.72 tff(c_12283, plain, (![A_686]: (LE(f(g(g(g(g(g(g(g(g(A_686))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_686)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_686)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_686))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_686)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_686))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_686)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_686))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_686)))))), inference(resolution, [status(thm)], [c_9217, c_2095])).
% 20.26/10.72 tff(c_885, plain, (![A_163]: (LE(f(g(g(g(g(g(g(g(A_163)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_163))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_163))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_163)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_163))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_163)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_163))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_163))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_163)))))), inference(resolution, [status(thm)], [c_532, c_874])).
% 20.26/10.72 tff(c_12861, plain, (![A_700]: (LE(f(g(g(g(g(g(g(g(g(A_700))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_700)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_700)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_700))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_700)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_700))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_700)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_700))))))), inference(resolution, [status(thm)], [c_12283, c_885])).
% 20.26/10.72 tff(c_395, plain, (![A_29_66]: (LE(f(g(g(g(g(A_29_66))))), s(0)) | E(s(0), f(g(g(g(g(A_29_66)))))) | E(s(s(0)), f(g(g(g(g(A_29_66)))))) | E(s(s(s(0))), f(g(g(g(A_29_66))))) | E(s(s(s(s(0)))), f(g(g(A_29_66)))) | E(s(s(s(s(s(0))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_391])).
% 20.26/10.72 tff(c_763, plain, (![A_186]: (LE(f(g(g(g(g(g(g(g(A_186)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_186))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_186))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_186)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_186))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_186)))))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_739, c_395])).
% 20.26/10.72 tff(c_12898, plain, (![A_701]: (LE(f(g(g(g(g(g(g(g(g(A_701))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_701)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_701)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_701))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_701)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_701))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_701)))))))), inference(resolution, [status(thm)], [c_12861, c_763])).
% 20.26/10.72 tff(c_326, plain, (![A_29_66]: (LE(f(g(g(g(A_29_66)))), s(0)) | E(s(0), f(g(g(g(A_29_66))))) | E(s(s(0)), f(g(g(g(A_29_66))))) | E(s(s(s(0))), f(g(g(A_29_66)))) | E(s(s(s(s(0)))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_322])).
% 20.26/10.72 tff(c_1297, plain, (![A_223]: (LE(f(g(g(g(g(g(g(g(A_223)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_223))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_223))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_223)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_223))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_223))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_223)))))))), inference(resolution, [status(thm)], [c_1276, c_326])).
% 20.26/10.72 tff(c_13694, plain, (![A_729]: (LE(f(g(g(g(g(g(g(g(g(A_729))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_729)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_729)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_729))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_729)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_729))))))))), inference(resolution, [status(thm)], [c_12898, c_1297])).
% 20.26/10.72 tff(c_227, plain, (![A_29_66]: (LE(f(g(g(A_29_66))), s(0)) | E(s(0), f(g(g(A_29_66)))) | E(s(s(0)), f(g(g(A_29_66)))) | E(s(s(s(0))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_214, c_223])).
% 20.26/10.72 tff(c_1921, plain, (![A_262]: (LE(f(g(g(g(g(g(g(g(A_262)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_262))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_262))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_262)))))))) | ~E(s(s(s(s(s(0))))), f(g(g(g(g(A_262)))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_262))))))))), inference(resolution, [status(thm)], [c_1903, c_227])).
% 20.26/10.72 tff(c_13719, plain, (![A_730]: (LE(f(g(g(g(g(g(g(g(g(A_730))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_730)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_730)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_730))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_730)))))))))), inference(resolution, [status(thm)], [c_13694, c_1921])).
% 20.26/10.72 tff(c_206, plain, (![A_29_92]: (LE(f(g(A_29_92)), s(0)) | E(s(0), f(g(A_29_92))) | E(s(s(0)), f(g(A_29_92))) | ~LE(f(A_29_92), s(s(s(0)))))), inference(resolution, [status(thm)], [c_194, c_168])).
% 20.26/10.72 tff(c_3307, plain, (![A_331]: (LE(f(g(g(g(g(g(g(g(A_331)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_331))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_331))))))))) | ~E(s(s(s(s(0)))), f(g(g(g(g(g(A_331))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_331)))))))))), inference(resolution, [status(thm)], [c_3292, c_206])).
% 20.26/10.72 tff(c_13877, plain, (![A_736]: (LE(f(g(g(g(g(g(g(g(g(A_736))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_736)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_736)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_736))))))))))), inference(resolution, [status(thm)], [c_13719, c_3307])).
% 20.26/10.72 tff(c_7822, plain, (![A_529]: (LE(f(g(g(g(g(g(g(g(A_529)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_529))))))))) | ~E(s(s(s(0))), f(g(g(g(g(g(g(A_529)))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_529))))))))))), inference(resolution, [status(thm)], [c_7810, c_168])).
% 20.26/10.72 tff(c_13894, plain, (![A_737]: (LE(f(g(g(g(g(g(g(g(g(A_737))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_737)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_737)))))))))))), inference(resolution, [status(thm)], [c_13877, c_7822])).
% 20.26/10.72 tff(c_44, plain, (![A_26_28]: (E(f(A_26_28), f(g(A_26_28))) | ~E(s(s(0)), f(g(A_26_28))) | ~E(s(s(0)), f(A_26_28)))), inference(cnfTransformation, [status(thm)], [f_149])).
% 20.26/10.72 tff(c_134, plain, (![A_26_28]: (~E(s(s(0)), f(g(A_26_28))) | ~E(s(s(0)), f(A_26_28)))), inference(negUnitSimplification, [status(thm)], [c_110, c_44])).
% 20.26/10.72 tff(c_13955, plain, (![A_738]: (~E(s(s(0)), f(g(g(g(g(g(g(g(A_738))))))))) | LE(f(g(g(g(g(g(g(g(g(A_738))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_738)))))))))))), inference(resolution, [status(thm)], [c_13894, c_134])).
% 20.26/10.72 tff(c_13997, plain, (![A_740]: (E(0, f(g(g(g(g(g(g(g(g(g(A_740))))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_740))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_740)))))))))))), inference(resolution, [status(thm)], [c_13955, c_158])).
% 20.26/10.72 tff(c_14026, plain, (![A_260]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_260)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_260))))))))))) | LE(f(g(g(g(g(g(A_260)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_260))))))))), inference(resolution, [status(thm)], [c_7928, c_13997])).
% 20.26/10.72 tff(c_159, plain, (![A_29_67]: (E(0, f(A_29_67)) | ~LE(f(A_29_67), s(0)))), inference(resolution, [status(thm)], [c_114, c_153])).
% 20.26/10.72 tff(c_181, plain, (![A_29_84]: (E(0, f(g(A_29_84))) | E(s(0), f(g(A_29_84))) | ~LE(f(A_29_84), s(s(0))))), inference(resolution, [status(thm)], [c_173, c_159])).
% 20.26/10.72 tff(c_241, plain, (![A_29_105]: (E(0, f(g(g(A_29_105)))) | E(s(0), f(g(g(A_29_105)))) | E(s(s(0)), f(g(A_29_105))) | ~LE(f(A_29_105), s(s(s(0)))))), inference(resolution, [status(thm)], [c_194, c_181])).
% 20.26/10.72 tff(c_332, plain, (![A_29_131]: (E(0, f(g(g(g(A_29_131))))) | E(s(0), f(g(g(g(A_29_131))))) | E(s(s(0)), f(g(g(A_29_131)))) | E(s(s(s(0))), f(g(A_29_131))) | ~LE(f(A_29_131), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_214, c_241])).
% 20.26/10.72 tff(c_406, plain, (![A_29_145]: (E(0, f(g(g(g(g(A_29_145)))))) | E(s(0), f(g(g(g(g(A_29_145)))))) | E(s(s(0)), f(g(g(g(A_29_145))))) | E(s(s(s(0))), f(g(g(A_29_145)))) | E(s(s(s(s(0)))), f(g(A_29_145))) | ~LE(f(A_29_145), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_332])).
% 20.26/10.72 tff(c_570, plain, (![A_29_169]: (E(0, f(g(g(g(g(g(A_29_169))))))) | E(s(0), f(g(g(g(g(g(A_29_169))))))) | E(s(s(0)), f(g(g(g(g(A_29_169)))))) | E(s(s(s(0))), f(g(g(g(A_29_169))))) | E(s(s(s(s(0)))), f(g(g(A_29_169)))) | E(s(s(s(s(s(0))))), f(g(A_29_169))) | ~LE(f(A_29_169), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_406])).
% 20.26/10.72 tff(c_887, plain, (![A_29_198]: (E(0, f(g(g(g(g(g(g(A_29_198)))))))) | E(s(0), f(g(g(g(g(g(g(A_29_198)))))))) | E(s(s(0)), f(g(g(g(g(g(A_29_198))))))) | E(s(s(s(0))), f(g(g(g(g(A_29_198)))))) | E(s(s(s(s(0)))), f(g(g(g(A_29_198))))) | E(s(s(s(s(s(0))))), f(g(g(A_29_198)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_198))) | ~LE(f(A_29_198), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_570])).
% 20.26/10.72 tff(c_2983, plain, (![A_29_318]: (E(0, f(g(g(g(g(g(g(g(A_29_318))))))))) | E(s(0), f(g(g(g(g(g(g(g(A_29_318))))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_29_318)))))))) | E(s(s(s(0))), f(g(g(g(g(g(A_29_318))))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_29_318)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_29_318))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_318)))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_318))) | ~LE(f(A_29_318), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_294, c_887])).
% 20.26/10.72 tff(c_4411, plain, (![A_29_390]: (E(0, f(g(g(g(g(g(g(g(g(A_29_390)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_29_390)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_29_390))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_29_390)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_29_390))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_29_390)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_390))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_390)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_390))) | ~LE(f(A_29_390), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_2983])).
% 20.26/10.72 tff(c_7047, plain, (![A_29_502]: (E(0, f(g(g(g(g(g(g(g(g(g(A_29_502))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_29_502))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_29_502)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_29_502))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_29_502)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_29_502))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_29_502)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_502))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_502)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_502))) | ~LE(f(A_29_502), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_4411])).
% 20.26/10.72 tff(c_7051, plain, (![A_47]: (E(0, f(g(g(g(g(g(g(g(g(g(A_47))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_47))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_47)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_47))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_47)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_47))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_47)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_47))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_47)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(resolution, [status(thm)], [c_78, c_7047])).
% 20.26/10.72 tff(c_7061, plain, (![A_2_504]: (E(0, f(g(g(g(g(g(g(g(g(g(A_2_504))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_2_504))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_2_504)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_2_504))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_2_504)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_2_504))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_2_504)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_504))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_504)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_504)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_504))))), inference(resolution, [status(thm)], [c_351, c_4411])).
% 20.26/10.72 tff(c_13612, plain, (![A_727]: (E(0, f(g(g(g(g(g(g(g(g(g(A_727))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_727))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_727)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_727))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_727)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_727))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_727)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_727))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_727)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_727))))), inference(resolution, [status(thm)], [c_7051, c_7061])).
% 20.26/10.72 tff(c_2990, plain, (![A_148]: (E(0, f(g(g(g(g(g(g(g(g(A_148)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_148)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_148))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_148)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_148))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_148)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_148)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_429, c_2983])).
% 20.26/10.72 tff(c_15237, plain, (![A_792]: (E(0, f(g(g(g(g(g(g(g(g(g(A_792))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_792))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_792)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_792))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_792)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_792))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_792)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_792))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_792)))))), inference(resolution, [status(thm)], [c_13612, c_2990])).
% 20.26/10.72 tff(c_898, plain, (![A_163]: (E(0, f(g(g(g(g(g(g(g(g(A_163)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_163)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_163))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_163)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_163))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_163)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_163))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_163))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_163)))))), inference(resolution, [status(thm)], [c_532, c_887])).
% 20.26/10.72 tff(c_15411, plain, (![A_798]: (E(0, f(g(g(g(g(g(g(g(g(g(A_798))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_798))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_798)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_798))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_798)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_798))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_798)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_798))))))), inference(resolution, [status(thm)], [c_15237, c_898])).
% 20.26/10.72 tff(c_410, plain, (![A_29_66]: (E(0, f(g(g(g(g(g(A_29_66))))))) | E(s(0), f(g(g(g(g(g(A_29_66))))))) | E(s(s(0)), f(g(g(g(g(A_29_66)))))) | E(s(s(s(0))), f(g(g(g(A_29_66))))) | E(s(s(s(s(0)))), f(g(g(A_29_66)))) | E(s(s(s(s(s(0))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_406])).
% 20.26/10.72 tff(c_762, plain, (![A_186]: (E(0, f(g(g(g(g(g(g(g(g(A_186)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_186)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_186))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_186)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_186))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_186)))))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_739, c_410])).
% 20.26/10.72 tff(c_15452, plain, (![A_799]: (E(0, f(g(g(g(g(g(g(g(g(g(A_799))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_799))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_799)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_799))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_799)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_799))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_799)))))))), inference(resolution, [status(thm)], [c_15411, c_762])).
% 20.26/10.72 tff(c_336, plain, (![A_29_66]: (E(0, f(g(g(g(g(A_29_66)))))) | E(s(0), f(g(g(g(g(A_29_66)))))) | E(s(s(0)), f(g(g(g(A_29_66))))) | E(s(s(s(0))), f(g(g(A_29_66)))) | E(s(s(s(s(0)))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_332])).
% 20.26/10.72 tff(c_1296, plain, (![A_223]: (E(0, f(g(g(g(g(g(g(g(g(A_223)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_223)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_223))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_223)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_223))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_223))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_223)))))))), inference(resolution, [status(thm)], [c_1276, c_336])).
% 20.26/10.72 tff(c_15518, plain, (![A_801]: (E(0, f(g(g(g(g(g(g(g(g(g(A_801))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_801))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_801)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_801))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_801)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_801))))))))), inference(resolution, [status(thm)], [c_15452, c_1296])).
% 20.26/10.72 tff(c_245, plain, (![A_29_66]: (E(0, f(g(g(g(A_29_66))))) | E(s(0), f(g(g(g(A_29_66))))) | E(s(s(0)), f(g(g(A_29_66)))) | E(s(s(s(0))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_214, c_241])).
% 20.26/10.72 tff(c_1920, plain, (![A_262]: (E(0, f(g(g(g(g(g(g(g(g(A_262)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_262)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_262))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_262)))))))) | ~E(s(s(s(s(s(0))))), f(g(g(g(g(A_262)))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_262))))))))), inference(resolution, [status(thm)], [c_1903, c_245])).
% 20.26/10.72 tff(c_15543, plain, (![A_802]: (E(0, f(g(g(g(g(g(g(g(g(g(A_802))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_802))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_802)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_802))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_802)))))))))), inference(resolution, [status(thm)], [c_15518, c_1920])).
% 20.26/10.72 tff(c_205, plain, (![A_29_92]: (E(0, f(g(g(A_29_92)))) | E(s(0), f(g(g(A_29_92)))) | E(s(s(0)), f(g(A_29_92))) | ~LE(f(A_29_92), s(s(s(0)))))), inference(resolution, [status(thm)], [c_194, c_181])).
% 20.26/10.72 tff(c_3306, plain, (![A_331]: (E(0, f(g(g(g(g(g(g(g(g(A_331)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_331)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_331))))))))) | ~E(s(s(s(s(0)))), f(g(g(g(g(g(A_331))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_331)))))))))), inference(resolution, [status(thm)], [c_3292, c_205])).
% 20.26/10.72 tff(c_15564, plain, (![A_803]: (E(0, f(g(g(g(g(g(g(g(g(g(A_803))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_803))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_803)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_803))))))))))), inference(resolution, [status(thm)], [c_15543, c_3306])).
% 20.26/10.72 tff(c_7821, plain, (![A_529]: (E(0, f(g(g(g(g(g(g(g(g(A_529)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_529)))))))))) | ~E(s(s(s(0))), f(g(g(g(g(g(g(A_529)))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_529))))))))))), inference(resolution, [status(thm)], [c_7810, c_181])).
% 20.26/10.72 tff(c_15648, plain, (![A_807]: (E(0, f(g(g(g(g(g(g(g(g(g(A_807))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_807))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_807)))))))))))), inference(resolution, [status(thm)], [c_15564, c_7821])).
% 20.26/10.72 tff(c_13963, plain, (![A_738]: (E(0, f(g(g(g(g(g(g(g(g(A_738)))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_738))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_738)))))))))))), inference(resolution, [status(thm)], [c_13955, c_159])).
% 20.26/10.72 tff(c_15661, plain, (![A_808]: (E(0, f(g(g(g(g(g(g(g(g(g(A_808))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_808))))))))))))), inference(resolution, [status(thm)], [c_15648, c_13963])).
% 20.26/10.72 tff(c_70, plain, (![A_29_42]: (E(f(A_29_42), f(g(A_29_42))) | ~E(s(0), f(g(A_29_42))) | ~E(s(0), f(A_29_42)))), inference(cnfTransformation, [status(thm)], [f_210])).
% 20.26/10.72 tff(c_124, plain, (![A_29_42]: (~E(s(0), f(g(A_29_42))) | ~E(s(0), f(A_29_42)))), inference(negUnitSimplification, [status(thm)], [c_110, c_70])).
% 20.26/10.72 tff(c_15698, plain, (![A_809]: (~E(s(0), f(g(g(g(g(g(g(g(g(A_809)))))))))) | E(0, f(g(g(g(g(g(g(g(g(g(A_809))))))))))))), inference(resolution, [status(thm)], [c_15661, c_124])).
% 20.26/10.72 tff(c_15722, plain, (![A_260]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_260)))))))))))) | LE(f(g(g(g(g(g(A_260)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_260))))))))), inference(resolution, [status(thm)], [c_14026, c_15698])).
% 20.26/10.72 tff(c_1248, plain, (![A_220]: (LE(f(g(g(g(g(A_220))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_220)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_220)))))))), inference(resolution, [status(thm)], [c_1229, c_767])).
% 20.26/10.72 tff(c_352, plain, (![A_29_135]: (E(0, f(g(g(g(g(A_29_135)))))) | E(s(0), f(g(g(g(A_29_135))))) | E(s(s(0)), f(g(g(A_29_135)))) | E(s(s(s(0))), f(g(A_29_135))) | ~LE(f(A_29_135), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_214, c_247])).
% 20.26/10.72 tff(c_356, plain, (![A_29_66]: (E(0, f(g(g(g(g(g(A_29_66))))))) | E(s(0), f(g(g(g(g(A_29_66)))))) | E(s(s(0)), f(g(g(g(A_29_66))))) | E(s(s(s(0))), f(g(g(A_29_66)))) | E(s(s(s(s(0)))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_352])).
% 20.26/10.72 tff(c_1475, plain, (![A_238]: (E(0, f(g(g(g(g(g(g(g(g(g(A_238))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_238)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_238))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_238)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_238))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_238))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_238)))))))), inference(resolution, [status(thm)], [c_1276, c_356])).
% 20.26/10.72 tff(c_9258, plain, (![A_593]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_593)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_593))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_593)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_593))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_593)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_593))))))) | LE(f(g(g(g(g(A_593))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_593)))))))), inference(resolution, [status(thm)], [c_1248, c_1475])).
% 20.26/10.72 tff(c_1919, plain, (![A_262]: (E(0, f(g(g(g(g(g(g(g(g(g(A_262))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_262)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_262))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_262)))))))) | ~E(s(s(s(s(s(0))))), f(g(g(g(g(A_262)))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_262))))))))), inference(resolution, [status(thm)], [c_1903, c_251])).
% 20.26/10.72 tff(c_9283, plain, (![A_594]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_594)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_594))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_594)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_594))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_594)))))))) | LE(f(g(g(g(g(A_594))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_594)))))))), inference(resolution, [status(thm)], [c_9258, c_1919])).
% 20.26/10.72 tff(c_3305, plain, (![A_331]: (E(0, f(g(g(g(g(g(g(g(g(g(A_331))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_331)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_331))))))))) | ~E(s(s(s(s(0)))), f(g(g(g(g(g(A_331))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_331)))))))))), inference(resolution, [status(thm)], [c_3292, c_204])).
% 20.26/10.72 tff(c_9337, plain, (![A_596]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_596)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_596))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_596)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_596))))))))) | LE(f(g(g(g(g(A_596))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_596)))))))), inference(resolution, [status(thm)], [c_9283, c_3305])).
% 20.26/10.72 tff(c_7820, plain, (![A_529]: (E(0, f(g(g(g(g(g(g(g(g(g(A_529))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_529)))))))))) | ~E(s(s(s(0))), f(g(g(g(g(g(g(A_529)))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_529))))))))))), inference(resolution, [status(thm)], [c_7810, c_180])).
% 20.26/10.72 tff(c_9350, plain, (![A_596]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_596)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_596))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_596)))))))))) | LE(f(g(g(g(g(A_596))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_596)))))))), inference(resolution, [status(thm)], [c_9337, c_7820])).
% 20.26/10.72 tff(c_526, plain, (![A_162]: (LE(f(g(g(A_162))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_162)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_162)))))), inference(resolution, [status(thm)], [c_515, c_438])).
% 20.26/10.72 tff(c_5904, plain, (![A_447]: (LE(f(g(g(g(g(g(g(g(A_447)))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(A_447))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_447))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_447)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_447))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_447)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_447))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_447))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_447)))))), inference(resolution, [status(thm)], [c_532, c_874])).
% 20.26/10.72 tff(c_9085, plain, (![A_588]: (LE(f(g(g(g(g(g(g(g(g(A_588))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_588)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_588)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_588))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_588)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_588))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_588)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_588))))) | LE(f(g(g(A_588))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_588)))))), inference(resolution, [status(thm)], [c_526, c_5904])).
% 20.26/10.72 tff(c_11035, plain, (![A_654]: (LE(f(g(g(g(g(g(g(g(g(A_654))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_654)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_654)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_654))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_654)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_654))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_654)))))) | LE(f(g(g(A_654))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_654)))))), inference(resolution, [status(thm)], [c_9085, c_763])).
% 20.26/10.72 tff(c_11064, plain, (![A_655]: (LE(f(g(g(g(g(g(g(g(g(A_655))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_655)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_655)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_655))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_655)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_655))))))) | LE(f(g(g(A_655))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_655)))))), inference(resolution, [status(thm)], [c_11035, c_1297])).
% 20.26/10.72 tff(c_11089, plain, (![A_656]: (LE(f(g(g(g(g(g(g(g(g(A_656))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_656)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_656)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_656))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_656)))))))) | LE(f(g(g(A_656))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_656)))))), inference(resolution, [status(thm)], [c_11064, c_1921])).
% 20.26/10.72 tff(c_11110, plain, (![A_657]: (LE(f(g(g(g(g(g(g(g(g(A_657))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_657)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_657)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_657))))))))) | LE(f(g(g(A_657))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_657)))))), inference(resolution, [status(thm)], [c_11089, c_3307])).
% 20.26/10.72 tff(c_11127, plain, (![A_658]: (LE(f(g(g(g(g(g(g(g(g(A_658))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_658)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_658)))))))))) | LE(f(g(g(A_658))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_658)))))), inference(resolution, [status(thm)], [c_11110, c_7822])).
% 20.26/10.72 tff(c_11180, plain, (![A_659]: (~E(s(s(0)), f(g(g(g(g(g(g(g(A_659))))))))) | LE(f(g(g(g(g(g(g(g(g(A_659))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_659)))))))))) | LE(f(g(g(A_659))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_659)))))), inference(resolution, [status(thm)], [c_11127, c_134])).
% 20.26/10.72 tff(c_11222, plain, (![A_661]: (E(0, f(g(g(g(g(g(g(g(g(g(A_661))))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_661))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_661)))))))))) | LE(f(g(g(A_661))), s(s(s(s(s(s(s(0)))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_661)))))), inference(resolution, [status(thm)], [c_11180, c_158])).
% 20.26/10.72 tff(c_11643, plain, (![A_670]: (LE(f(g(g(g(A_670)))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_670))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_670))))) | E(0, f(g(g(g(g(g(g(g(g(g(A_670))))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_670))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_670)))))))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_670)))))), inference(resolution, [status(thm)], [c_11222, c_283])).
% 20.26/10.72 tff(c_11686, plain, (![A_670]: (LE(f(g(g(g(A_670)))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_670))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_670))))) | E(0, f(g(g(g(g(g(g(g(g(g(A_670))))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_670))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_670)))))))))))), inference(resolution, [status(thm)], [c_11643, c_767])).
% 20.26/10.72 tff(c_12927, plain, (![A_702]: (~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_702))))) | LE(f(g(g(g(g(g(g(g(g(A_702))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_702)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_702)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_702))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_702)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_702))))))))), inference(resolution, [status(thm)], [c_12898, c_138])).
% 20.26/10.72 tff(c_12952, plain, (![A_703]: (~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_703))))) | LE(f(g(g(g(g(g(g(g(g(A_703))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_703)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_703)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_703))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_703)))))))))), inference(resolution, [status(thm)], [c_12927, c_1921])).
% 20.26/10.72 tff(c_12973, plain, (![A_704]: (~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_704))))) | LE(f(g(g(g(g(g(g(g(g(A_704))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_704)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_704)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_704))))))))))), inference(resolution, [status(thm)], [c_12952, c_3307])).
% 20.26/10.72 tff(c_12990, plain, (![A_705]: (~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_705))))) | LE(f(g(g(g(g(g(g(g(g(A_705))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_705)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_705)))))))))))), inference(resolution, [status(thm)], [c_12973, c_7822])).
% 20.26/10.72 tff(c_13067, plain, (![A_706]: (~E(s(s(0)), f(g(g(g(g(g(g(g(A_706))))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_706))))) | LE(f(g(g(g(g(g(g(g(g(A_706))))))))), s(0)) | E(s(0), f(g(g(g(g(g(g(g(g(A_706)))))))))))), inference(resolution, [status(thm)], [c_12990, c_134])).
% 20.26/10.72 tff(c_13130, plain, (![A_709]: (E(0, f(g(g(g(g(g(g(g(g(g(A_709))))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_709))))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_709))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_709)))))))))))), inference(resolution, [status(thm)], [c_13067, c_158])).
% 20.26/10.72 tff(c_13254, plain, (![A_713]: (LE(f(g(g(g(A_713)))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_713))))) | E(0, f(g(g(g(g(g(g(g(g(g(A_713))))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_713))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_713)))))))))))), inference(resolution, [status(thm)], [c_11686, c_13130])).
% 20.26/10.72 tff(c_13308, plain, (![A_596]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_596)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_596))))))))))) | LE(f(g(g(g(g(A_596))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_596)))))))), inference(resolution, [status(thm)], [c_9350, c_13254])).
% 20.26/10.72 tff(c_15887, plain, (![A_822]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_822)))))))))))) | LE(f(g(g(g(g(A_822))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_822)))))))), inference(resolution, [status(thm)], [c_13308, c_15698])).
% 20.26/10.72 tff(c_50, plain, (![A_30_31]: (E(f(A_30_31), f(g(A_30_31))) | ~E(0, f(g(A_30_31))) | ~E(0, f(A_30_31)))), inference(cnfTransformation, [status(thm)], [f_168])).
% 20.26/10.72 tff(c_132, plain, (![A_30_31]: (~E(0, f(g(A_30_31))) | ~E(0, f(A_30_31)))), inference(negUnitSimplification, [status(thm)], [c_110, c_50])).
% 20.26/10.72 tff(c_15896, plain, (![A_823]: (~E(0, f(g(g(g(g(g(g(g(g(g(A_823))))))))))) | LE(f(g(g(g(g(A_823))))), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_823)))))))), inference(resolution, [status(thm)], [c_15887, c_132])).
% 20.26/10.72 tff(c_15920, plain, (![A_823]: (LE(f(g(g(g(g(A_823))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_823)))))) | ~E(0, f(g(g(g(g(g(g(g(g(g(A_823))))))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_823)))))))), inference(resolution, [status(thm)], [c_15896, c_234])).
% 20.26/10.72 tff(c_444, plain, (![A_29_151]: (E(0, f(g(g(g(g(g(A_29_151))))))) | E(s(0), f(g(g(g(g(A_29_151)))))) | E(s(s(0)), f(g(g(g(A_29_151))))) | E(s(s(s(0))), f(g(g(A_29_151)))) | E(s(s(s(s(0)))), f(g(A_29_151))) | ~LE(f(A_29_151), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_233, c_352])).
% 20.26/10.72 tff(c_584, plain, (![A_29_171]: (E(0, f(g(g(g(g(g(g(A_29_171)))))))) | E(s(0), f(g(g(g(g(g(A_29_171))))))) | E(s(s(0)), f(g(g(g(g(A_29_171)))))) | E(s(s(s(0))), f(g(g(g(A_29_171))))) | E(s(s(s(s(0)))), f(g(g(A_29_171)))) | E(s(s(s(s(s(0))))), f(g(A_29_171))) | ~LE(f(A_29_171), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_444])).
% 20.26/10.72 tff(c_930, plain, (![A_29_201]: (E(0, f(g(g(g(g(g(g(g(A_29_201))))))))) | E(s(0), f(g(g(g(g(g(g(A_29_201)))))))) | E(s(s(0)), f(g(g(g(g(g(A_29_201))))))) | E(s(s(s(0))), f(g(g(g(g(A_29_201)))))) | E(s(s(s(s(0)))), f(g(g(g(A_29_201))))) | E(s(s(s(s(s(0))))), f(g(g(A_29_201)))) | E(s(s(s(s(s(s(0)))))), f(g(A_29_201))) | ~LE(f(A_29_201), s(s(s(s(s(s(s(0)))))))))), inference(resolution, [status(thm)], [c_271, c_584])).
% 20.26/10.72 tff(c_3083, plain, (![A_29_322]: (E(0, f(g(g(g(g(g(g(g(g(A_29_322)))))))))) | E(s(0), f(g(g(g(g(g(g(g(A_29_322))))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_29_322)))))))) | E(s(s(s(0))), f(g(g(g(g(g(A_29_322))))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_29_322)))))) | E(s(s(s(s(s(0))))), f(g(g(g(A_29_322))))) | E(s(s(s(s(s(s(0)))))), f(g(g(A_29_322)))) | E(s(s(s(s(s(s(s(0))))))), f(g(A_29_322))) | ~LE(f(A_29_322), s(s(s(s(s(s(s(s(0))))))))))), inference(resolution, [status(thm)], [c_294, c_930])).
% 20.26/10.72 tff(c_4901, plain, (![A_29_408]: (E(0, f(g(g(g(g(g(g(g(g(g(A_29_408))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_29_408)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_29_408))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_29_408)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_29_408))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_29_408)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_29_408))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_29_408)))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_29_408))) | ~LE(f(A_29_408), s(s(s(s(s(s(s(s(s(0)))))))))))), inference(resolution, [status(thm)], [c_301, c_3083])).
% 20.26/10.72 tff(c_7334, plain, (![A_29_513]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_29_513)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_29_513))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_29_513)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_29_513))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_29_513)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_29_513))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_29_513)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_29_513))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_29_513)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_29_513))) | ~LE(f(A_29_513), s(s(s(s(s(s(s(s(s(s(0))))))))))))), inference(resolution, [status(thm)], [c_315, c_4901])).
% 20.26/10.72 tff(c_7338, plain, (![A_47]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_47)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_47))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_47)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_47))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_47)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_47))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_47)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_47))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_47)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_47))) | E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_47)))), inference(resolution, [status(thm)], [c_78, c_7334])).
% 20.26/10.72 tff(c_7477, plain, (![A_2_520]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_2_520)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_2_520))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_2_520)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_2_520))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_2_520)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_2_520))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_2_520)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_2_520))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_2_520)))) | ~E(s(s(s(s(s(s(s(s(s(s(0)))))))))), f(A_2_520)) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_2_520))))), inference(resolution, [status(thm)], [c_351, c_4901])).
% 20.26/10.72 tff(c_13653, plain, (![A_728]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_728)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_728))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_728)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_728))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_728)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_728))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_728)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_728))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_728)))) | E(s(s(s(s(s(s(s(s(s(0))))))))), f(g(A_728))))), inference(resolution, [status(thm)], [c_7338, c_7477])).
% 20.26/10.72 tff(c_3090, plain, (![A_148]: (E(0, f(g(g(g(g(g(g(g(g(g(A_148))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_148)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_148))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_148)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_148))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_148)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_148))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_148)))) | ~E(s(s(s(s(s(s(s(s(s(0))))))))), f(A_148)) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_148))))), inference(resolution, [status(thm)], [c_429, c_3083])).
% 20.26/10.72 tff(c_15481, plain, (![A_800]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_800)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_800))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_800)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_800))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_800)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_800))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_800)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_800))))) | E(s(s(s(s(s(s(s(s(0)))))))), f(g(g(A_800)))))), inference(resolution, [status(thm)], [c_13653, c_3090])).
% 20.26/10.72 tff(c_941, plain, (![A_163]: (E(0, f(g(g(g(g(g(g(g(g(g(A_163))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_163)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_163))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_163)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_163))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_163)))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_163))))) | ~E(s(s(s(s(s(s(s(s(0)))))))), f(g(A_163))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(A_163)))))), inference(resolution, [status(thm)], [c_532, c_930])).
% 20.26/10.72 tff(c_16241, plain, (![A_836]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_836)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_836))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_836)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_836))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_836)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_836))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_836)))))) | E(s(s(s(s(s(s(s(0))))))), f(g(g(g(A_836))))))), inference(resolution, [status(thm)], [c_15481, c_941])).
% 20.26/10.72 tff(c_448, plain, (![A_29_66]: (E(0, f(g(g(g(g(g(g(A_29_66)))))))) | E(s(0), f(g(g(g(g(g(A_29_66))))))) | E(s(s(0)), f(g(g(g(g(A_29_66)))))) | E(s(s(s(0))), f(g(g(g(A_29_66))))) | E(s(s(s(s(0)))), f(g(g(A_29_66)))) | E(s(s(s(s(s(0))))), f(g(A_29_66))) | ~LE(f(A_29_66), s(s(s(s(s(s(0))))))))), inference(resolution, [status(thm)], [c_263, c_444])).
% 20.26/10.72 tff(c_761, plain, (![A_186]: (E(0, f(g(g(g(g(g(g(g(g(g(A_186))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_186)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_186))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_186)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_186))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_186)))))) | ~E(s(s(s(s(s(s(s(0))))))), f(g(g(A_186)))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(A_186))))))), inference(resolution, [status(thm)], [c_739, c_448])).
% 20.26/10.72 tff(c_16278, plain, (![A_837]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_837)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_837))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_837)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_837))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_837)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_837))))))) | E(s(s(s(s(s(s(0)))))), f(g(g(g(g(A_837)))))))), inference(resolution, [status(thm)], [c_16241, c_761])).
% 20.26/10.72 tff(c_1295, plain, (![A_223]: (E(0, f(g(g(g(g(g(g(g(g(g(A_223))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_223)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_223))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_223)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_223))))))) | ~E(s(s(s(s(s(s(0)))))), f(g(g(g(A_223))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(A_223)))))))), inference(resolution, [status(thm)], [c_1276, c_356])).
% 20.26/10.72 tff(c_16307, plain, (![A_838]: (E(0, f(g(g(g(g(g(g(g(g(g(g(A_838)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_838))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_838)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_838))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_838)))))))) | E(s(s(s(s(s(0))))), f(g(g(g(g(g(A_838))))))))), inference(resolution, [status(thm)], [c_16278, c_1295])).
% 20.26/10.72 tff(c_16332, plain, (![A_839]: (~E(s(s(s(s(s(0))))), f(g(g(g(g(A_839)))))) | E(0, f(g(g(g(g(g(g(g(g(g(g(A_839)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_839))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_839)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_839))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(g(A_839)))))))))), inference(resolution, [status(thm)], [c_16307, c_133])).
% 20.26/10.72 tff(c_16353, plain, (![A_840]: (~E(s(s(s(s(s(0))))), f(g(g(g(g(A_840)))))) | E(0, f(g(g(g(g(g(g(g(g(g(g(A_840)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_840))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_840)))))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(g(A_840))))))))))), inference(resolution, [status(thm)], [c_16332, c_3305])).
% 20.26/10.72 tff(c_16370, plain, (![A_841]: (~E(s(s(s(s(s(0))))), f(g(g(g(g(A_841)))))) | E(0, f(g(g(g(g(g(g(g(g(g(g(A_841)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_841))))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(g(A_841)))))))))))), inference(resolution, [status(thm)], [c_16353, c_7820])).
% 20.26/10.72 tff(c_13962, plain, (![A_738]: (E(0, f(g(g(g(g(g(g(g(g(g(A_738))))))))))) | ~E(s(s(0)), f(g(g(g(g(g(g(g(A_738))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_738)))))))))))), inference(resolution, [status(thm)], [c_13955, c_158])).
% 20.26/10.72 tff(c_16383, plain, (![A_842]: (~E(s(s(s(s(s(0))))), f(g(g(g(g(A_842)))))) | E(0, f(g(g(g(g(g(g(g(g(g(g(A_842)))))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(g(A_842))))))))))))), inference(resolution, [status(thm)], [c_16370, c_13962])).
% 20.26/10.72 tff(c_15697, plain, (![A_808]: (~E(s(0), f(g(g(g(g(g(g(g(g(A_808)))))))))) | E(0, f(g(g(g(g(g(g(g(g(g(A_808))))))))))))), inference(resolution, [status(thm)], [c_15661, c_124])).
% 20.26/10.72 tff(c_16392, plain, (![A_843]: (~E(s(s(s(s(s(0))))), f(g(g(g(g(A_843)))))) | E(0, f(g(g(g(g(g(g(g(g(g(g(A_843)))))))))))))), inference(resolution, [status(thm)], [c_16383, c_15697])).
% 20.26/10.72 tff(c_16417, plain, (![A_844]: (~E(0, f(g(g(g(g(g(g(g(g(g(A_844))))))))))) | ~E(s(s(s(s(s(0))))), f(g(g(g(g(A_844)))))))), inference(resolution, [status(thm)], [c_16392, c_132])).
% 20.26/10.72 tff(c_16430, plain, (![A_845]: (LE(f(g(g(g(g(A_845))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_845)))))) | ~E(0, f(g(g(g(g(g(g(g(g(g(A_845))))))))))))), inference(resolution, [status(thm)], [c_15920, c_16417])).
% 20.26/10.72 tff(c_16463, plain, (![A_846]: (LE(f(g(g(g(g(g(A_846)))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_846))))))))), inference(resolution, [status(thm)], [c_15722, c_16430])).
% 20.26/10.72 tff(c_16527, plain, (![A_850]: (LE(f(g(g(g(g(g(g(A_850))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_850)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_850)))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_850))))))))), inference(resolution, [status(thm)], [c_16463, c_222])).
% 20.26/10.72 tff(c_16484, plain, (![A_847]: (LE(f(g(g(g(g(g(A_847)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_847))))))) | E(s(s(s(s(0)))), f(g(g(g(g(g(A_847))))))))), inference(resolution, [status(thm)], [c_16463, c_215])).
% 20.26/10.72 tff(c_16505, plain, (![A_848]: (~E(s(s(s(s(0)))), f(g(g(g(g(A_848)))))) | LE(f(g(g(g(g(g(A_848)))))), s(s(s(0)))) | E(s(s(s(0))), f(g(g(g(g(g(A_848))))))))), inference(resolution, [status(thm)], [c_16484, c_116])).
% 20.26/10.72 tff(c_16521, plain, (![A_848]: (LE(f(g(g(g(g(g(A_848)))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(A_848))))))) | ~E(s(s(s(s(0)))), f(g(g(g(g(A_848)))))) | E(s(s(s(0))), f(g(g(g(g(g(A_848))))))))), inference(resolution, [status(thm)], [c_16505, c_192])).
% 20.26/10.72 tff(c_16548, plain, (![A_851]: (LE(f(g(g(g(g(g(g(A_851))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_851)))))))) | E(s(s(s(0))), f(g(g(g(g(g(g(A_851)))))))))), inference(resolution, [status(thm)], [c_16527, c_16521])).
% 20.26/10.72 tff(c_16621, plain, (![A_860]: (E(0, f(g(g(g(g(g(g(g(g(A_860)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_860)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(g(A_860))))))))) | LE(f(g(g(g(g(g(g(A_860))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_860)))))))))), inference(resolution, [status(thm)], [c_16548, c_7821])).
% 20.26/10.72 tff(c_16634, plain, (![A_861]: (E(0, f(g(g(g(g(g(g(g(g(A_861)))))))))) | E(s(0), f(g(g(g(g(g(g(g(g(A_861)))))))))) | LE(f(g(g(g(g(g(g(A_861))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_861)))))))))), inference(resolution, [status(thm)], [c_16621, c_13963])).
% 20.26/10.72 tff(c_16656, plain, (![A_863]: (E(0, f(g(g(g(g(g(g(g(g(g(A_863))))))))))) | E(0, f(g(g(g(g(g(g(g(g(A_863)))))))))) | LE(f(g(g(g(g(g(g(A_863))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_863)))))))))), inference(resolution, [status(thm)], [c_16634, c_15697])).
% 20.26/10.72 tff(c_16428, plain, (![A_823]: (LE(f(g(g(g(g(A_823))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_823)))))) | ~E(0, f(g(g(g(g(g(g(g(g(g(A_823))))))))))))), inference(resolution, [status(thm)], [c_15920, c_16417])).
% 20.26/10.72 tff(c_16699, plain, (![A_866]: (LE(f(g(g(g(g(A_866))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_866)))))) | E(0, f(g(g(g(g(g(g(g(g(A_866)))))))))) | LE(f(g(g(g(g(g(g(A_866))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_866)))))))))), inference(resolution, [status(thm)], [c_16656, c_16428])).
% 20.26/10.72 tff(c_16712, plain, (![A_867]: (E(s(0), f(g(g(g(g(g(g(g(A_867))))))))) | LE(f(g(g(g(g(A_867))))), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_867)))))) | E(0, f(g(g(g(g(g(g(g(g(A_867)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_867)))))))))), inference(resolution, [status(thm)], [c_16699, c_180])).
% 20.26/10.72 tff(c_16733, plain, (![A_868]: (E(s(s(s(0))), f(g(g(g(g(g(A_868))))))) | E(s(0), f(g(g(g(g(g(g(g(A_868))))))))) | E(s(s(s(s(0)))), f(g(g(g(g(A_868)))))) | E(0, f(g(g(g(g(g(g(g(g(A_868)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_868)))))))))), inference(resolution, [status(thm)], [c_16712, c_251])).
% 20.26/10.72 tff(c_16518, plain, (![A_848]: (E(0, f(g(g(g(g(g(g(g(g(A_848)))))))))) | E(s(0), f(g(g(g(g(g(g(g(A_848))))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_848)))))))) | ~E(s(s(s(s(0)))), f(g(g(g(g(A_848)))))) | E(s(s(s(0))), f(g(g(g(g(g(A_848))))))))), inference(resolution, [status(thm)], [c_16505, c_204])).
% 20.26/10.72 tff(c_16754, plain, (![A_869]: (E(s(s(s(0))), f(g(g(g(g(g(A_869))))))) | E(s(0), f(g(g(g(g(g(g(g(A_869))))))))) | E(0, f(g(g(g(g(g(g(g(g(A_869)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_869)))))))))), inference(resolution, [status(thm)], [c_16733, c_16518])).
% 20.26/10.72 tff(c_16565, plain, (![A_852]: (~E(s(s(s(0))), f(g(g(g(g(g(A_852))))))) | LE(f(g(g(g(g(g(g(A_852))))))), s(s(0))) | E(s(s(0)), f(g(g(g(g(g(g(A_852)))))))))), inference(resolution, [status(thm)], [c_16548, c_140])).
% 20.26/10.72 tff(c_16575, plain, (![A_852]: (E(0, f(g(g(g(g(g(g(g(g(A_852)))))))))) | E(s(0), f(g(g(g(g(g(g(g(A_852))))))))) | ~E(s(s(s(0))), f(g(g(g(g(g(A_852))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_852)))))))))), inference(resolution, [status(thm)], [c_16565, c_180])).
% 20.26/10.72 tff(c_16771, plain, (![A_870]: (E(s(0), f(g(g(g(g(g(g(g(A_870))))))))) | E(0, f(g(g(g(g(g(g(g(g(A_870)))))))))) | E(s(s(0)), f(g(g(g(g(g(g(A_870)))))))))), inference(resolution, [status(thm)], [c_16754, c_16575])).
% 20.26/10.72 tff(c_16835, plain, (![A_874]: (E(s(0), f(g(g(g(g(g(g(g(g(A_874)))))))))) | E(0, f(g(g(g(g(g(g(g(g(g(A_874))))))))))))), inference(resolution, [status(thm)], [c_16771, c_13962])).
% 20.26/10.72 tff(c_16886, plain, (![A_875]: (E(0, f(g(g(g(g(g(g(g(g(g(A_875))))))))))))), inference(resolution, [status(thm)], [c_16835, c_15697])).
% 20.26/10.72 tff(c_16890, plain, (![A_875]: (~E(0, f(g(g(g(g(g(g(g(g(A_875)))))))))))), inference(resolution, [status(thm)], [c_16886, c_132])).
% 20.26/10.72 tff(c_16846, plain, (![A_874]: (E(0, f(g(g(g(g(g(g(g(g(g(A_874))))))))))))), inference(resolution, [status(thm)], [c_16835, c_15697])).
% 20.26/10.72 tff(c_16906, plain, $false, inference(negUnitSimplification, [status(thm)], [c_16890, c_16846])).
% 20.26/10.72 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------