%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO630-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : 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 5.84s 2.40s
% Output : CNFRefutation 6.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.12 % Problem : SYO630-1 : TPTP v9.0.0. Released v7.1.0.
% 0.02/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Apr 9 09:38:24 EDT 2025
% 0.12/0.33 % CPUTime :
% 5.84/2.40 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/2.41
% 5.84/2.41 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.84/2.42 %$ iLEQ > LE > E > #nlpp > s > g > f > 0
% 5.84/2.42
% 5.84/2.42 %Foreground sorts:
% 5.84/2.42
% 5.84/2.42
% 5.84/2.42 %Background operators:
% 5.84/2.42
% 5.84/2.42
% 5.84/2.42 %Foreground operators:
% 5.84/2.42 tff(iLEQ, type, iLEQ: ($i * $i) > $o).
% 5.84/2.42 tff(s, type, s: $i > $i).
% 5.84/2.42 tff(f, type, f: $i > $i).
% 5.84/2.42 tff(g, type, g: $i > $i).
% 5.84/2.42 tff(0, type, 0: $i).
% 5.84/2.42 tff(LE, type, LE: ($i * $i) > $o).
% 5.84/2.42 tff(E, type, E: ($i * $i) > $o).
% 5.84/2.42
% 6.25/2.46 tff(f_28, axiom, (![A]: (E(s(s(s(s(s(0))))), f(A)) | LE(f(A), s(s(s(s(s(0)))))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_143, axiom, (![A_8]: iLEQ(A_8, g(A_8))), file('unknown', unknown)).
% 6.25/2.46 tff(f_110, axiom, (![A_1, B_0]: (((~LE(f(A_1), s(s(s(s(s(0)))))) | ~iLEQ(A_1, B_0)) | E(s(s(s(s(0)))), f(B_0))) | LE(f(B_0), s(s(s(s(0))))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_120, axiom, (![A_4, B_2]: (((~LE(f(A_4), s(s(s(s(0))))) | ~iLEQ(A_4, B_2)) | E(s(s(s(0))), f(B_2))) | LE(f(B_2), s(s(s(0)))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_100, axiom, (![A_7, B_4]: (((~LE(f(A_7), s(s(s(0)))) | ~iLEQ(A_7, B_4)) | E(s(s(0)), f(B_4))) | LE(f(B_4), s(s(0))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_174, axiom, (![A_10, B_6]: (((~LE(f(A_10), s(s(0))) | ~iLEQ(A_10, B_6)) | E(s(0), f(B_6))) | LE(f(B_6), s(0)))), file('unknown', unknown)).
% 6.25/2.46 tff(f_50, axiom, (![A_15]: ~LE(f(A_15), 0)), file('unknown', unknown)).
% 6.25/2.46 tff(f_47, axiom, (![A_13, B_8]: (((~LE(f(A_13), s(0)) | ~iLEQ(A_13, B_8)) | E(0, f(B_8))) | LE(f(B_8), 0))), file('unknown', unknown)).
% 6.25/2.46 tff(f_153, axiom, (![A_11]: iLEQ(A_11, A_11)), file('unknown', unknown)).
% 6.25/2.46 tff(f_164, axiom, (![A_14]: ~E(f(A_14), f(g(A_14)))), file('unknown', unknown)).
% 6.25/2.46 tff(f_63, axiom, (![A_2]: ((~E(s(s(s(s(s(0))))), f(A_2)) | ~E(s(s(s(s(s(0))))), f(g(A_2)))) | E(f(A_2), f(g(A_2))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_161, axiom, (![A_5]: ((~E(s(s(s(s(0)))), f(A_5)) | ~E(s(s(s(s(0)))), f(g(A_5)))) | E(f(A_5), f(g(A_5))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_71, axiom, (![A_8]: ((~E(s(s(s(0))), f(A_8)) | ~E(s(s(s(0))), f(g(A_8)))) | E(f(A_8), f(g(A_8))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_79, axiom, (![A_11]: ((~E(s(s(0)), f(A_11)) | ~E(s(s(0)), f(g(A_11)))) | E(f(A_11), f(g(A_11))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_87, axiom, (![A_14]: ((~E(s(0), f(A_14)) | ~E(s(0), f(g(A_14)))) | E(f(A_14), f(g(A_14))))), file('unknown', unknown)).
% 6.25/2.46 tff(f_141, axiom, (![A_15]: ((~E(0, f(A_15)) | ~E(0, f(g(A_15)))) | E(f(A_15), f(g(A_15))))), file('unknown', unknown)).
% 6.25/2.46 tff(c_2, plain, (![A_1]: (LE(f(A_1), s(s(s(s(s(0)))))) | E(s(s(s(s(s(0))))), f(A_1)))), inference(cnfTransformation, [status(thm)], [f_28])).
% 6.25/2.46 tff(c_50, plain, (![A_8_29]: (iLEQ(A_8_29, g(A_8_29)))), inference(cnfTransformation, [status(thm)], [f_143])).
% 6.25/2.46 tff(c_155, plain, (![B_0_67, A_1_68]: (LE(f(B_0_67), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(B_0_67)) | ~iLEQ(A_1_68, B_0_67) | ~LE(f(A_1_68), s(s(s(s(s(0)))))))), inference(cnfTransformation, [status(thm)], [f_110])).
% 6.25/2.46 tff(c_160, plain, (![A_8_29]: (LE(f(g(A_8_29)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_8_29))) | ~LE(f(A_8_29), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_50, c_155])).
% 6.25/2.46 tff(c_127, plain, (![B_2_60, A_4_61]: (LE(f(B_2_60), s(s(s(0)))) | E(s(s(s(0))), f(B_2_60)) | ~iLEQ(A_4_61, B_2_60) | ~LE(f(A_4_61), s(s(s(s(0))))))), inference(cnfTransformation, [status(thm)], [f_120])).
% 6.25/2.46 tff(c_132, plain, (![A_8_29]: (LE(f(g(A_8_29)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_8_29))) | ~LE(f(A_8_29), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_50, c_127])).
% 6.25/2.46 tff(c_109, plain, (![B_4_55, A_7_56]: (LE(f(B_4_55), s(s(0))) | E(s(s(0)), f(B_4_55)) | ~iLEQ(A_7_56, B_4_55) | ~LE(f(A_7_56), s(s(s(0)))))), inference(cnfTransformation, [status(thm)], [f_100])).
% 6.25/2.46 tff(c_136, plain, (![A_8_64]: (LE(f(g(A_8_64)), s(s(0))) | E(s(s(0)), f(g(A_8_64))) | ~LE(f(A_8_64), s(s(s(0)))))), inference(resolution, [status(thm)], [c_50, c_109])).
% 6.25/2.46 tff(c_102, plain, (![B_6_53, A_10_54]: (LE(f(B_6_53), s(0)) | E(s(0), f(B_6_53)) | ~iLEQ(A_10_54, B_6_53) | ~LE(f(A_10_54), s(s(0))))), inference(cnfTransformation, [status(thm)], [f_174])).
% 6.25/2.46 tff(c_117, plain, (![A_8_58]: (LE(f(g(A_8_58)), s(0)) | E(s(0), f(g(A_8_58))) | ~LE(f(A_8_58), s(s(0))))), inference(resolution, [status(thm)], [c_50, c_102])).
% 6.25/2.46 tff(c_14, plain, (![A_15_8]: (~LE(f(A_15_8), 0))), inference(cnfTransformation, [status(thm)], [f_50])).
% 6.25/2.46 tff(c_12, plain, (![B_8_7, A_13_6]: (LE(f(B_8_7), 0) | E(0, f(B_8_7)) | ~iLEQ(A_13_6, B_8_7) | ~LE(f(A_13_6), s(0)))), inference(cnfTransformation, [status(thm)], [f_47])).
% 6.25/2.46 tff(c_88, plain, (![B_8_44, A_13_45]: (E(0, f(B_8_44)) | ~iLEQ(A_13_45, B_8_44) | ~LE(f(A_13_45), s(0)))), inference(negUnitSimplification, [status(thm)], [c_14, c_12])).
% 6.25/2.46 tff(c_93, plain, (![A_8_29]: (E(0, f(g(A_8_29))) | ~LE(f(A_8_29), s(0)))), inference(resolution, [status(thm)], [c_50, c_88])).
% 6.25/2.46 tff(c_124, plain, (![A_8_58]: (E(0, f(g(g(A_8_58)))) | E(s(0), f(g(A_8_58))) | ~LE(f(A_8_58), s(s(0))))), inference(resolution, [status(thm)], [c_117, c_93])).
% 6.25/2.46 tff(c_192, plain, (![A_8_75]: (E(0, f(g(g(g(A_8_75))))) | E(s(0), f(g(g(A_8_75)))) | E(s(s(0)), f(g(A_8_75))) | ~LE(f(A_8_75), s(s(s(0)))))), inference(resolution, [status(thm)], [c_136, c_124])).
% 6.25/2.46 tff(c_285, plain, (![A_8_88]: (E(0, f(g(g(g(g(A_8_88)))))) | E(s(0), f(g(g(g(A_8_88))))) | E(s(s(0)), f(g(g(A_8_88)))) | E(s(s(s(0))), f(g(A_8_88))) | ~LE(f(A_8_88), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_132, c_192])).
% 6.25/2.46 tff(c_605, plain, (![A_8_124]: (E(0, f(g(g(g(g(g(A_8_124))))))) | E(s(0), f(g(g(g(g(A_8_124)))))) | E(s(s(0)), f(g(g(g(A_8_124))))) | E(s(s(s(0))), f(g(g(A_8_124)))) | E(s(s(s(s(0)))), f(g(A_8_124))) | ~LE(f(A_8_124), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_160, c_285])).
% 6.25/2.46 tff(c_777, plain, (![A_136]: (E(0, f(g(g(g(g(g(A_136))))))) | E(s(0), f(g(g(g(g(A_136)))))) | E(s(s(0)), f(g(g(g(A_136))))) | E(s(s(s(0))), f(g(g(A_136)))) | E(s(s(s(s(0)))), f(g(A_136))) | E(s(s(s(s(s(0))))), f(A_136)))), inference(resolution, [status(thm)], [c_2, c_605])).
% 6.25/2.46 tff(c_58, plain, (![A_11_33]: (iLEQ(A_11_33, A_11_33))), inference(cnfTransformation, [status(thm)], [f_153])).
% 6.25/2.46 tff(c_162, plain, (![A_11_69]: (LE(f(A_11_69), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(A_11_69)) | ~LE(f(A_11_69), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_58, c_155])).
% 6.25/2.46 tff(c_167, plain, (![A_70]: (LE(f(A_70), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(A_70)) | E(s(s(s(s(s(0))))), f(A_70)))), inference(resolution, [status(thm)], [c_2, c_162])).
% 6.25/2.46 tff(c_62, plain, (![A_14_35]: (~E(f(A_14_35), f(g(A_14_35))))), inference(cnfTransformation, [status(thm)], [f_164])).
% 6.25/2.46 tff(c_20, plain, (![A_2_11]: (E(f(A_2_11), f(g(A_2_11))) | ~E(s(s(s(s(s(0))))), f(g(A_2_11))) | ~E(s(s(s(s(s(0))))), f(A_2_11)))), inference(cnfTransformation, [status(thm)], [f_63])).
% 6.25/2.46 tff(c_76, plain, (![A_2_11]: (~E(s(s(s(s(s(0))))), f(g(A_2_11))) | ~E(s(s(s(s(s(0))))), f(A_2_11)))), inference(negUnitSimplification, [status(thm)], [c_62, c_20])).
% 6.25/2.46 tff(c_171, plain, (![A_2_11]: (~E(s(s(s(s(s(0))))), f(A_2_11)) | LE(f(g(A_2_11)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_2_11))))), inference(resolution, [status(thm)], [c_167, c_76])).
% 6.25/2.46 tff(c_292, plain, (![A_2_11]: (E(0, f(g(g(g(g(g(A_2_11))))))) | E(s(0), f(g(g(g(g(A_2_11)))))) | E(s(s(0)), f(g(g(g(A_2_11))))) | E(s(s(s(0))), f(g(g(A_2_11)))) | ~E(s(s(s(s(s(0))))), f(A_2_11)) | E(s(s(s(s(0)))), f(g(A_2_11))))), inference(resolution, [status(thm)], [c_171, c_285])).
% 6.25/2.46 tff(c_905, plain, (![A_148]: (E(0, f(g(g(g(g(g(A_148))))))) | E(s(0), f(g(g(g(g(A_148)))))) | E(s(s(0)), f(g(g(g(A_148))))) | E(s(s(s(0))), f(g(g(A_148)))) | E(s(s(s(s(0)))), f(g(A_148))))), inference(resolution, [status(thm)], [c_777, c_292])).
% 6.25/2.46 tff(c_177, plain, (![A_8_72]: (LE(f(g(A_8_72)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_8_72))) | ~LE(f(A_8_72), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_50, c_155])).
% 6.25/2.46 tff(c_133, plain, (![A_11_33]: (LE(f(A_11_33), s(s(s(0)))) | E(s(s(s(0))), f(A_11_33)) | ~LE(f(A_11_33), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_58, c_127])).
% 6.25/2.46 tff(c_206, plain, (![A_8_77]: (LE(f(g(A_8_77)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_8_77))) | E(s(s(s(s(0)))), f(g(A_8_77))) | ~LE(f(A_8_77), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_177, c_133])).
% 6.25/2.46 tff(c_210, plain, (![A_1]: (LE(f(g(A_1)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_1))) | E(s(s(s(s(0)))), f(g(A_1))) | E(s(s(s(s(s(0))))), f(A_1)))), inference(resolution, [status(thm)], [c_2, c_206])).
% 6.25/2.46 tff(c_182, plain, (![A_2_73]: (~E(s(s(s(s(s(0))))), f(A_2_73)) | LE(f(g(A_2_73)), s(s(s(s(0))))) | E(s(s(s(s(0)))), f(g(A_2_73))))), inference(resolution, [status(thm)], [c_167, c_76])).
% 6.25/2.46 tff(c_216, plain, (![A_2_79]: (LE(f(g(A_2_79)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_2_79))) | ~E(s(s(s(s(s(0))))), f(A_2_79)) | E(s(s(s(s(0)))), f(g(A_2_79))))), inference(resolution, [status(thm)], [c_182, c_133])).
% 6.25/2.46 tff(c_225, plain, (![A_80]: (LE(f(g(A_80)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_80))) | E(s(s(s(s(0)))), f(g(A_80))))), inference(resolution, [status(thm)], [c_210, c_216])).
% 6.25/2.46 tff(c_60, plain, (![A_5_34]: (E(f(A_5_34), f(g(A_5_34))) | ~E(s(s(s(s(0)))), f(g(A_5_34))) | ~E(s(s(s(s(0)))), f(A_5_34)))), inference(cnfTransformation, [status(thm)], [f_161])).
% 6.25/2.46 tff(c_65, plain, (![A_5_34]: (~E(s(s(s(s(0)))), f(g(A_5_34))) | ~E(s(s(s(s(0)))), f(A_5_34)))), inference(negUnitSimplification, [status(thm)], [c_62, c_60])).
% 6.25/2.46 tff(c_230, plain, (![A_81]: (~E(s(s(s(s(0)))), f(A_81)) | LE(f(g(A_81)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_81))))), inference(resolution, [status(thm)], [c_225, c_65])).
% 6.25/2.46 tff(c_146, plain, (![A_8_64]: (E(0, f(g(g(g(A_8_64))))) | E(s(0), f(g(g(A_8_64)))) | E(s(s(0)), f(g(A_8_64))) | ~LE(f(A_8_64), s(s(s(0)))))), inference(resolution, [status(thm)], [c_136, c_124])).
% 6.25/2.46 tff(c_243, plain, (![A_81]: (E(0, f(g(g(g(g(A_81)))))) | E(s(0), f(g(g(g(A_81))))) | E(s(s(0)), f(g(g(A_81)))) | ~E(s(s(s(s(0)))), f(A_81)) | E(s(s(s(0))), f(g(A_81))))), inference(resolution, [status(thm)], [c_230, c_146])).
% 6.25/2.46 tff(c_926, plain, (![A_149]: (E(0, f(g(g(g(g(g(A_149))))))) | E(s(0), f(g(g(g(g(A_149)))))) | E(s(s(0)), f(g(g(g(A_149))))) | E(s(s(s(0))), f(g(g(A_149)))))), inference(resolution, [status(thm)], [c_905, c_243])).
% 6.25/2.46 tff(c_150, plain, (![A_8_66]: (LE(f(g(A_8_66)), s(s(s(0)))) | E(s(s(s(0))), f(g(A_8_66))) | ~LE(f(A_8_66), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_50, c_127])).
% 6.25/2.46 tff(c_115, plain, (![A_11_33]: (LE(f(A_11_33), s(s(0))) | E(s(s(0)), f(A_11_33)) | ~LE(f(A_11_33), s(s(s(0)))))), inference(resolution, [status(thm)], [c_58, c_109])).
% 6.25/2.46 tff(c_197, plain, (![A_8_76]: (LE(f(g(A_8_76)), s(s(0))) | E(s(s(0)), f(g(A_8_76))) | E(s(s(s(0))), f(g(A_8_76))) | ~LE(f(A_8_76), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_150, c_115])).
% 6.25/2.46 tff(c_280, plain, (![A_8_87]: (LE(f(g(g(A_8_87))), s(s(0))) | E(s(s(0)), f(g(g(A_8_87)))) | E(s(s(s(0))), f(g(g(A_8_87)))) | E(s(s(s(s(0)))), f(g(A_8_87))) | ~LE(f(A_8_87), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_160, c_197])).
% 6.25/2.46 tff(c_284, plain, (![A_1]: (LE(f(g(g(A_1))), s(s(0))) | E(s(s(0)), f(g(g(A_1)))) | E(s(s(s(0))), f(g(g(A_1)))) | E(s(s(s(s(0)))), f(g(A_1))) | E(s(s(s(s(s(0))))), f(A_1)))), inference(resolution, [status(thm)], [c_2, c_280])).
% 6.25/2.46 tff(c_309, plain, (![A_2_92]: (LE(f(g(g(A_2_92))), s(s(0))) | E(s(s(0)), f(g(g(A_2_92)))) | E(s(s(s(0))), f(g(g(A_2_92)))) | ~E(s(s(s(s(s(0))))), f(A_2_92)) | E(s(s(s(s(0)))), f(g(A_2_92))))), inference(resolution, [status(thm)], [c_171, c_197])).
% 6.25/2.46 tff(c_318, plain, (![A_93]: (LE(f(g(g(A_93))), s(s(0))) | E(s(s(0)), f(g(g(A_93)))) | E(s(s(s(0))), f(g(g(A_93)))) | E(s(s(s(s(0)))), f(g(A_93))))), inference(resolution, [status(thm)], [c_284, c_309])).
% 6.25/2.46 tff(c_246, plain, (![A_81]: (LE(f(g(A_81)), s(s(0))) | E(s(s(0)), f(g(A_81))) | ~E(s(s(s(s(0)))), f(A_81)) | E(s(s(s(0))), f(g(A_81))))), inference(resolution, [status(thm)], [c_230, c_115])).
% 6.25/2.46 tff(c_339, plain, (![A_94]: (LE(f(g(g(A_94))), s(s(0))) | E(s(s(0)), f(g(g(A_94)))) | E(s(s(s(0))), f(g(g(A_94)))))), inference(resolution, [status(thm)], [c_318, c_246])).
% 6.25/2.46 tff(c_22, plain, (![A_8_12]: (E(f(A_8_12), f(g(A_8_12))) | ~E(s(s(s(0))), f(g(A_8_12))) | ~E(s(s(s(0))), f(A_8_12)))), inference(cnfTransformation, [status(thm)], [f_71])).
% 6.25/2.46 tff(c_75, plain, (![A_8_12]: (~E(s(s(s(0))), f(g(A_8_12))) | ~E(s(s(s(0))), f(A_8_12)))), inference(negUnitSimplification, [status(thm)], [c_62, c_22])).
% 6.25/2.46 tff(c_344, plain, (![A_95]: (~E(s(s(s(0))), f(g(A_95))) | LE(f(g(g(A_95))), s(s(0))) | E(s(s(0)), f(g(g(A_95)))))), inference(resolution, [status(thm)], [c_339, c_75])).
% 6.25/2.46 tff(c_354, plain, (![A_95]: (E(0, f(g(g(g(g(A_95)))))) | E(s(0), f(g(g(g(A_95))))) | ~E(s(s(s(0))), f(g(A_95))) | E(s(s(0)), f(g(g(A_95)))))), inference(resolution, [status(thm)], [c_344, c_124])).
% 6.25/2.46 tff(c_943, plain, (![A_150]: (E(0, f(g(g(g(g(g(A_150))))))) | E(s(0), f(g(g(g(g(A_150)))))) | E(s(s(0)), f(g(g(g(A_150))))))), inference(resolution, [status(thm)], [c_926, c_354])).
% 6.25/2.46 tff(c_108, plain, (![A_11_33]: (LE(f(A_11_33), s(0)) | E(s(0), f(A_11_33)) | ~LE(f(A_11_33), s(s(0))))), inference(resolution, [status(thm)], [c_58, c_102])).
% 6.25/2.46 tff(c_172, plain, (![A_8_71]: (LE(f(g(A_8_71)), s(0)) | E(s(0), f(g(A_8_71))) | E(s(s(0)), f(g(A_8_71))) | ~LE(f(A_8_71), s(s(s(0)))))), inference(resolution, [status(thm)], [c_136, c_108])).
% 6.25/2.46 tff(c_252, plain, (![A_8_83]: (LE(f(g(g(A_8_83))), s(0)) | E(s(0), f(g(g(A_8_83)))) | E(s(s(0)), f(g(g(A_8_83)))) | E(s(s(s(0))), f(g(A_8_83))) | ~LE(f(A_8_83), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_132, c_172])).
% 6.25/2.46 tff(c_357, plain, (![A_8_96]: (LE(f(g(g(g(A_8_96)))), s(0)) | E(s(0), f(g(g(g(A_8_96))))) | E(s(s(0)), f(g(g(g(A_8_96))))) | E(s(s(s(0))), f(g(g(A_8_96)))) | E(s(s(s(s(0)))), f(g(A_8_96))) | ~LE(f(A_8_96), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_160, c_252])).
% 6.25/2.46 tff(c_361, plain, (![A_1]: (LE(f(g(g(g(A_1)))), s(0)) | E(s(0), f(g(g(g(A_1))))) | E(s(s(0)), f(g(g(g(A_1))))) | E(s(s(s(0))), f(g(g(A_1)))) | E(s(s(s(s(0)))), f(g(A_1))) | E(s(s(s(s(s(0))))), f(A_1)))), inference(resolution, [status(thm)], [c_2, c_357])).
% 6.25/2.46 tff(c_397, plain, (![A_2_104]: (LE(f(g(g(g(A_2_104)))), s(0)) | E(s(0), f(g(g(g(A_2_104))))) | E(s(s(0)), f(g(g(g(A_2_104))))) | E(s(s(s(0))), f(g(g(A_2_104)))) | ~E(s(s(s(s(s(0))))), f(A_2_104)) | E(s(s(s(s(0)))), f(g(A_2_104))))), inference(resolution, [status(thm)], [c_171, c_252])).
% 6.25/2.46 tff(c_406, plain, (![A_105]: (LE(f(g(g(g(A_105)))), s(0)) | E(s(0), f(g(g(g(A_105))))) | E(s(s(0)), f(g(g(g(A_105))))) | E(s(s(s(0))), f(g(g(A_105)))) | E(s(s(s(s(0)))), f(g(A_105))))), inference(resolution, [status(thm)], [c_361, c_397])).
% 6.25/2.46 tff(c_148, plain, (![A_8_64]: (LE(f(g(A_8_64)), s(0)) | E(s(0), f(g(A_8_64))) | E(s(s(0)), f(g(A_8_64))) | ~LE(f(A_8_64), s(s(s(0)))))), inference(resolution, [status(thm)], [c_136, c_108])).
% 6.25/2.46 tff(c_245, plain, (![A_81]: (LE(f(g(g(A_81))), s(0)) | E(s(0), f(g(g(A_81)))) | E(s(s(0)), f(g(g(A_81)))) | ~E(s(s(s(s(0)))), f(A_81)) | E(s(s(s(0))), f(g(A_81))))), inference(resolution, [status(thm)], [c_230, c_148])).
% 6.25/2.46 tff(c_427, plain, (![A_106]: (LE(f(g(g(g(A_106)))), s(0)) | E(s(0), f(g(g(g(A_106))))) | E(s(s(0)), f(g(g(g(A_106))))) | E(s(s(s(0))), f(g(g(A_106)))))), inference(resolution, [status(thm)], [c_406, c_245])).
% 6.25/2.46 tff(c_356, plain, (![A_95]: (LE(f(g(g(A_95))), s(0)) | E(s(0), f(g(g(A_95)))) | ~E(s(s(s(0))), f(g(A_95))) | E(s(s(0)), f(g(g(A_95)))))), inference(resolution, [status(thm)], [c_344, c_108])).
% 6.25/2.46 tff(c_444, plain, (![A_107]: (LE(f(g(g(g(A_107)))), s(0)) | E(s(0), f(g(g(g(A_107))))) | E(s(s(0)), f(g(g(g(A_107))))))), inference(resolution, [status(thm)], [c_427, c_356])).
% 6.25/2.46 tff(c_24, plain, (![A_11_13]: (E(f(A_11_13), f(g(A_11_13))) | ~E(s(s(0)), f(g(A_11_13))) | ~E(s(s(0)), f(A_11_13)))), inference(cnfTransformation, [status(thm)], [f_79])).
% 6.25/2.46 tff(c_74, plain, (![A_11_13]: (~E(s(s(0)), f(g(A_11_13))) | ~E(s(s(0)), f(A_11_13)))), inference(negUnitSimplification, [status(thm)], [c_62, c_24])).
% 6.25/2.46 tff(c_449, plain, (![A_108]: (~E(s(s(0)), f(g(g(A_108)))) | LE(f(g(g(g(A_108)))), s(0)) | E(s(0), f(g(g(g(A_108))))))), inference(resolution, [status(thm)], [c_444, c_74])).
% 6.25/2.46 tff(c_456, plain, (![A_108]: (E(0, f(g(g(g(g(A_108)))))) | ~E(s(s(0)), f(g(g(A_108)))) | E(s(0), f(g(g(g(A_108))))))), inference(resolution, [status(thm)], [c_449, c_93])).
% 6.25/2.46 tff(c_956, plain, (![A_151]: (E(0, f(g(g(g(g(g(A_151))))))) | E(s(0), f(g(g(g(g(A_151)))))))), inference(resolution, [status(thm)], [c_943, c_456])).
% 6.25/2.46 tff(c_94, plain, (![A_11_33]: (E(0, f(A_11_33)) | ~LE(f(A_11_33), s(0)))), inference(resolution, [status(thm)], [c_58, c_88])).
% 6.25/2.46 tff(c_125, plain, (![A_8_58]: (E(0, f(g(A_8_58))) | E(s(0), f(g(A_8_58))) | ~LE(f(A_8_58), s(s(0))))), inference(resolution, [status(thm)], [c_117, c_94])).
% 6.25/2.46 tff(c_187, plain, (![A_8_74]: (E(0, f(g(g(A_8_74)))) | E(s(0), f(g(g(A_8_74)))) | E(s(s(0)), f(g(A_8_74))) | ~LE(f(A_8_74), s(s(s(0)))))), inference(resolution, [status(thm)], [c_136, c_125])).
% 6.25/2.46 tff(c_266, plain, (![A_8_85]: (E(0, f(g(g(g(A_8_85))))) | E(s(0), f(g(g(g(A_8_85))))) | E(s(s(0)), f(g(g(A_8_85)))) | E(s(s(s(0))), f(g(A_8_85))) | ~LE(f(A_8_85), s(s(s(s(0))))))), inference(resolution, [status(thm)], [c_132, c_187])).
% 6.25/2.46 tff(c_600, plain, (![A_8_123]: (E(0, f(g(g(g(g(A_8_123)))))) | E(s(0), f(g(g(g(g(A_8_123)))))) | E(s(s(0)), f(g(g(g(A_8_123))))) | E(s(s(s(0))), f(g(g(A_8_123)))) | E(s(s(s(s(0)))), f(g(A_8_123))) | ~LE(f(A_8_123), s(s(s(s(s(0)))))))), inference(resolution, [status(thm)], [c_160, c_266])).
% 6.25/2.46 tff(c_653, plain, (![A_128]: (E(0, f(g(g(g(g(A_128)))))) | E(s(0), f(g(g(g(g(A_128)))))) | E(s(s(0)), f(g(g(g(A_128))))) | E(s(s(s(0))), f(g(g(A_128)))) | E(s(s(s(s(0)))), f(g(A_128))) | E(s(s(s(s(s(0))))), f(A_128)))), inference(resolution, [status(thm)], [c_2, c_600])).
% 6.25/2.46 tff(c_273, plain, (![A_2_11]: (E(0, f(g(g(g(g(A_2_11)))))) | E(s(0), f(g(g(g(g(A_2_11)))))) | E(s(s(0)), f(g(g(g(A_2_11))))) | E(s(s(s(0))), f(g(g(A_2_11)))) | ~E(s(s(s(s(s(0))))), f(A_2_11)) | E(s(s(s(s(0)))), f(g(A_2_11))))), inference(resolution, [status(thm)], [c_171, c_266])).
% 6.25/2.46 tff(c_726, plain, (![A_133]: (E(0, f(g(g(g(g(A_133)))))) | E(s(0), f(g(g(g(g(A_133)))))) | E(s(s(0)), f(g(g(g(A_133))))) | E(s(s(s(0))), f(g(g(A_133)))) | E(s(s(s(s(0)))), f(g(A_133))))), inference(resolution, [status(thm)], [c_653, c_273])).
% 6.25/2.46 tff(c_147, plain, (![A_8_64]: (E(0, f(g(g(A_8_64)))) | E(s(0), f(g(g(A_8_64)))) | E(s(s(0)), f(g(A_8_64))) | ~LE(f(A_8_64), s(s(s(0)))))), inference(resolution, [status(thm)], [c_136, c_125])).
% 6.25/2.46 tff(c_244, plain, (![A_81]: (E(0, f(g(g(g(A_81))))) | E(s(0), f(g(g(g(A_81))))) | E(s(s(0)), f(g(g(A_81)))) | ~E(s(s(s(s(0)))), f(A_81)) | E(s(s(s(0))), f(g(A_81))))), inference(resolution, [status(thm)], [c_230, c_147])).
% 6.25/2.46 tff(c_747, plain, (![A_134]: (E(0, f(g(g(g(g(A_134)))))) | E(s(0), f(g(g(g(g(A_134)))))) | E(s(s(0)), f(g(g(g(A_134))))) | E(s(s(s(0))), f(g(g(A_134)))))), inference(resolution, [status(thm)], [c_726, c_244])).
% 6.25/2.46 tff(c_355, plain, (![A_95]: (E(0, f(g(g(g(A_95))))) | E(s(0), f(g(g(g(A_95))))) | ~E(s(s(s(0))), f(g(A_95))) | E(s(s(0)), f(g(g(A_95)))))), inference(resolution, [status(thm)], [c_344, c_125])).
% 6.25/2.46 tff(c_764, plain, (![A_135]: (E(0, f(g(g(g(g(A_135)))))) | E(s(0), f(g(g(g(g(A_135)))))) | E(s(s(0)), f(g(g(g(A_135))))))), inference(resolution, [status(thm)], [c_747, c_355])).
% 6.25/2.46 tff(c_457, plain, (![A_108]: (E(0, f(g(g(g(A_108))))) | ~E(s(s(0)), f(g(g(A_108)))) | E(s(0), f(g(g(g(A_108))))))), inference(resolution, [status(thm)], [c_449, c_94])).
% 6.25/2.46 tff(c_786, plain, (![A_137]: (E(0, f(g(g(g(g(A_137)))))) | E(s(0), f(g(g(g(g(A_137)))))))), inference(resolution, [status(thm)], [c_764, c_457])).
% 6.25/2.46 tff(c_26, plain, (![A_14_14]: (E(f(A_14_14), f(g(A_14_14))) | ~E(s(0), f(g(A_14_14))) | ~E(s(0), f(A_14_14)))), inference(cnfTransformation, [status(thm)], [f_87])).
% 6.25/2.46 tff(c_73, plain, (![A_14_14]: (~E(s(0), f(g(A_14_14))) | ~E(s(0), f(A_14_14)))), inference(negUnitSimplification, [status(thm)], [c_62, c_26])).
% 6.25/2.46 tff(c_802, plain, (![A_137]: (~E(s(0), f(g(g(g(A_137))))) | E(0, f(g(g(g(g(A_137)))))))), inference(resolution, [status(thm)], [c_786, c_73])).
% 6.25/2.46 tff(c_969, plain, (![A_152]: (E(0, f(g(g(g(g(g(A_152))))))))), inference(resolution, [status(thm)], [c_956, c_802])).
% 6.25/2.46 tff(c_48, plain, (![A_15_28]: (E(f(A_15_28), f(g(A_15_28))) | ~E(0, f(g(A_15_28))) | ~E(0, f(A_15_28)))), inference(cnfTransformation, [status(thm)], [f_141])).
% 6.25/2.46 tff(c_67, plain, (![A_15_28]: (~E(0, f(g(A_15_28))) | ~E(0, f(A_15_28)))), inference(negUnitSimplification, [status(thm)], [c_62, c_48])).
% 6.25/2.46 tff(c_981, plain, (![A_152]: (~E(0, f(g(g(g(g(A_152)))))))), inference(resolution, [status(thm)], [c_969, c_67])).
% 6.25/2.46 tff(c_963, plain, (![A_151]: (E(0, f(g(g(g(g(g(A_151))))))))), inference(resolution, [status(thm)], [c_956, c_802])).
% 6.25/2.46 tff(c_989, plain, $false, inference(negUnitSimplification, [status(thm)], [c_981, c_963])).
% 6.25/2.46 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------