%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP151^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n013.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 : Thu Oct 9 01:47:07 PM UTC 2025
% Result : Theorem 24.12s 24.37s
% Output : Proof 24.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14 % Problem : ITP151^1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.35 % Computer : n013.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed Oct 8 17:50:53 EDT 2025
% 0.12/0.35 % CPUTime :
% 24.12/24.37 % SZS status Theorem
% 24.12/24.37 % Mode: mode485:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=4.:SINE_DEPTH=0
% 24.12/24.37 % Inferences: 1385
% 24.12/24.37 % SZS output start Proof
% 24.12/24.37 thf(conj_2,conjecture,((polyno578545843gree_a @ p) = zero_zero_nat)).
% 24.12/24.37 thf(h0,negated_conjecture,(~(((polyno578545843gree_a @ p) = zero_zero_nat))),inference(assume_negation,[status(cth)],[conj_2])).
% 24.12/24.37 thf(ax2513, axiom, (~(p21)|p1|~(p174)|~(p21)), file('<stdin>', ax2513)).
% 24.12/24.37 thf(pax2014, axiom, (p2014=>![X1:nat]:((X1)=(fpolyno578545843gree_a @ fp)=>~((fpolyno578545843gree_a @ fp)=(X1)))), file('<stdin>', pax2014)).
% 24.12/24.37 thf(ax2759, axiom, ~(p1), file('<stdin>', ax2759)).
% 24.12/24.37 thf(ax2573, axiom, (~(p2)|p181), file('<stdin>', ax2573)).
% 24.12/24.37 thf(ax851, axiom, (~(p7)|p1391), file('<stdin>', ax851)).
% 24.12/24.37 thf(nax174, axiom, (p174<=(fzero_zero_nat)=(fpolyno578545843gree_a @ fp)), file('<stdin>', nax174)).
% 24.12/24.37 thf(ax2739, axiom, p21, file('<stdin>', ax2739)).
% 24.12/24.37 thf(nax2014, axiom, (p2014<=![X1:nat]:((X1)=(fpolyno578545843gree_a @ fp)=>~((fpolyno578545843gree_a @ fp)=(X1)))), file('<stdin>', nax2014)).
% 24.12/24.37 thf(ax2535, axiom, (~(p181)|p1|p180), file('<stdin>', ax2535)).
% 24.12/24.37 thf(ax2758, axiom, p2, file('<stdin>', ax2758)).
% 24.12/24.37 thf(ax406, axiom, (~(p1391)|p1861), file('<stdin>', ax406)).
% 24.12/24.37 thf(ax2753, axiom, p7, file('<stdin>', ax2753)).
% 24.12/24.37 thf(ax838, axiom, (~(p7)|p1404), file('<stdin>', ax838)).
% 24.12/24.37 thf(ax407, axiom, (~(p1861)|~(p180)|p1860), file('<stdin>', ax407)).
% 24.12/24.37 thf(pax1404, axiom, (p1404=>![X1:nat]:(~((fzero_zero_nat)=(fpolyno578545843gree_a @ fp))=>(![X2:nat]:(ford_less_nat @ fzero_zero_nat @ X2=>((X2)=(fpolyno578545843gree_a @ fp)=>~(![X3:nat]:(ford_less_nat @ X3 @ X2=>~((X3)=(fpolyno578545843gree_a @ fp))))))=>~((X1)=(fpolyno578545843gree_a @ fp))))), file('<stdin>', pax1404)).
% 24.12/24.37 thf(pax12, axiom, (p12=>![X253:nat]:~(ford_less_nat @ X253 @ X253)), file('<stdin>', pax12)).
% 24.12/24.37 thf(ax408, axiom, (~(p1860)|~(p1859)|p1256), file('<stdin>', ax408)).
% 24.12/24.37 thf(pax1256, axiom, (p1256=>ford_less_nat @ (fpolyno578545843gree_a @ fp) @ (fpolyno578545843gree_a @ fp)), file('<stdin>', pax1256)).
% 24.12/24.37 thf(ax2748, axiom, p12, file('<stdin>', ax2748)).
% 24.12/24.37 thf(nax1859, axiom, (p1859<=![X1:nat]:(ford_less_nat @ fzero_zero_nat @ X1=>(~(ford_less_nat @ X1 @ (fpolyno578545843gree_a @ fp))=>~(![X2:nat]:(ford_less_nat @ X2 @ X1=>ford_less_nat @ X2 @ (fpolyno578545843gree_a @ fp)))))), file('<stdin>', nax1859)).
% 24.12/24.37 thf(pax9, axiom, (p9=>![X253:nat, X252:nat]:(~((X253)=(X252))=>(~(ford_less_nat @ X253 @ X252)=>ford_less_nat @ X252 @ X253))), file('<stdin>', pax9)).
% 24.12/24.37 thf(pax20, axiom, (p20=>![X251:polyno727731844poly_a, X252:nat]:(fpolyno1372495879olyh_a @ X251 @ (fsuc @ X252)=>(fpolyno578545843gree_a @ X251)=(fzero_zero_nat))), file('<stdin>', pax20)).
% 24.12/24.37 thf(pax32, axiom, (p32=>![X248:nat]:(~((X248)=(fzero_zero_nat))=>~(![X245:nat]:~((X248)=(fsuc @ X245))))), file('<stdin>', pax32)).
% 24.12/24.37 thf(ax2751, axiom, p9, file('<stdin>', ax2751)).
% 24.12/24.37 thf(ax2740, axiom, p20, file('<stdin>', ax2740)).
% 24.12/24.37 thf(ax2728, axiom, p32, file('<stdin>', ax2728)).
% 24.12/24.37 thf(pax173, axiom, (p173=>fpolyno1372495879olyh_a @ fp @ fn), file('<stdin>', pax173)).
% 24.12/24.37 thf(pax172, axiom, (p172=>ford_less_nat @ fzero_zero_nat @ fn), file('<stdin>', pax172)).
% 24.12/24.37 thf(ax2587, axiom, p173, file('<stdin>', ax2587)).
% 24.12/24.37 thf(pax3, axiom, (p3=>![X253:nat]:~(ford_less_nat @ X253 @ fzero_zero_nat)), file('<stdin>', pax3)).
% 24.12/24.37 thf(ax2588, axiom, p172, file('<stdin>', ax2588)).
% 24.12/24.37 thf(ax2757, axiom, p3, file('<stdin>', ax2757)).
% 24.12/24.37 thf(c_0_32, plain, (~p21|p1|~p174|~p21), inference(fof_simplification,[status(thm)],[ax2513])).
% 24.12/24.37 thf(c_0_33, plain, ![X1200:nat]:(~p2014|((X1200)!=(fpolyno578545843gree_a @ fp)|(fpolyno578545843gree_a @ fp)!=(X1200))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax2014])])])])).
% 24.12/24.37 thf(c_0_34, plain, (p1|~p21|~p174|~p21), inference(split_conjunct,[status(thm)],[c_0_32])).
% 24.12/24.37 thf(c_0_35, plain, ~p1, inference(fof_simplification,[status(thm)],[ax2759])).
% 24.12/24.37 thf(c_0_36, plain, ![X1:nat]:(~p2014|(X1)!=(fpolyno578545843gree_a @ fp)|(fpolyno578545843gree_a @ fp)!=(X1)), inference(split_conjunct,[status(thm)],[c_0_33])).
% 24.12/24.37 thf(c_0_37, plain, (~p2|p181), inference(fof_simplification,[status(thm)],[ax2573])).
% 24.12/24.37 thf(c_0_38, plain, (~p7|p1391), inference(fof_simplification,[status(thm)],[ax851])).
% 24.12/24.37 thf(c_0_39, plain, ((fzero_zero_nat)!=(fpolyno578545843gree_a @ fp)|p174), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax174])])).
% 24.12/24.37 thf(c_0_40, plain, (p1|~p21|~p174), inference(cn,[status(thm)],[c_0_34])).
% 24.12/24.37 thf(c_0_41, plain, p21, inference(split_conjunct,[status(thm)],[ax2739])).
% 24.12/24.37 thf(c_0_42, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_35])).
% 24.12/24.37 thf(c_0_43, plain, (((esk474_0)=(fpolyno578545843gree_a @ fp)|p2014)&((fpolyno578545843gree_a @ fp)=(esk474_0)|p2014)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2014])])])])])).
% 24.12/24.37 thf(c_0_44, plain, ![X1:nat]:((X1)!=(fpolyno578545843gree_a @ fp)|~p2014), inference(cn,[status(thm)],[c_0_36])).
% 24.12/24.37 thf(c_0_45, plain, (~p181|p1|p180), inference(fof_simplification,[status(thm)],[ax2535])).
% 24.12/24.37 thf(c_0_46, plain, (p181|~p2), inference(split_conjunct,[status(thm)],[c_0_37])).
% 24.12/24.37 thf(c_0_47, plain, p2, inference(split_conjunct,[status(thm)],[ax2758])).
% 24.12/24.37 thf(c_0_48, plain, (~p1391|p1861), inference(fof_simplification,[status(thm)],[ax406])).
% 24.12/24.37 thf(c_0_49, plain, (p1391|~p7), inference(split_conjunct,[status(thm)],[c_0_38])).
% 24.12/24.37 thf(c_0_50, plain, p7, inference(split_conjunct,[status(thm)],[ax2753])).
% 24.12/24.37 thf(c_0_51, plain, (~p7|p1404), inference(fof_simplification,[status(thm)],[ax838])).
% 24.12/24.37 thf(c_0_52, plain, (p174|(fzero_zero_nat)!=(fpolyno578545843gree_a @ fp)), inference(split_conjunct,[status(thm)],[c_0_39])).
% 24.12/24.37 thf(c_0_53, plain, ~p174, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_41])]), c_0_42])).
% 24.12/24.37 thf(c_0_54, plain, ((esk474_0)=(fpolyno578545843gree_a @ fp)|p2014), inference(split_conjunct,[status(thm)],[c_0_43])).
% 24.12/24.37 thf(c_0_55, plain, ~p2014, inference(er,[status(thm)],[c_0_44])).
% 24.12/24.37 thf(c_0_56, plain, (~p1861|~p180|p1860), inference(fof_simplification,[status(thm)],[ax407])).
% 24.12/24.37 thf(c_0_57, plain, (p1|p180|~p181), inference(split_conjunct,[status(thm)],[c_0_45])).
% 24.12/24.37 thf(c_0_58, plain, p181, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])])).
% 24.12/24.37 thf(c_0_59, plain, (p1861|~p1391), inference(split_conjunct,[status(thm)],[c_0_48])).
% 24.12/24.37 thf(c_0_60, plain, p1391, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50])])).
% 24.12/24.37 thf(c_0_61, plain, ![X2939:nat, X2940:nat]:((ford_less_nat @ fzero_zero_nat @ esk1343_0|(X2940)!=(fpolyno578545843gree_a @ fp)|(fzero_zero_nat)=(fpolyno578545843gree_a @ fp)|~p1404)&(((esk1343_0)=(fpolyno578545843gree_a @ fp)|(X2940)!=(fpolyno578545843gree_a @ fp)|(fzero_zero_nat)=(fpolyno578545843gree_a @ fp)|~p1404)&(~ford_less_nat @ X2939 @ esk1343_0|(X2939)!=(fpolyno578545843gree_a @ fp)|(X2940)!=(fpolyno578545843gree_a @ fp)|(fzero_zero_nat)=(fpolyno578545843gree_a @ fp)|~p1404))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax1404])])])])])])])).
% 24.12/24.37 thf(c_0_62, plain, (p1404|~p7), inference(split_conjunct,[status(thm)],[c_0_51])).
% 24.12/24.37 thf(c_0_63, plain, (fpolyno578545843gree_a @ fp)!=(fzero_zero_nat), inference(sr,[status(thm)],[c_0_52, c_0_53])).
% 24.12/24.37 thf(c_0_64, plain, (fpolyno578545843gree_a @ fp)=(esk474_0), inference(sr,[status(thm)],[c_0_54, c_0_55])).
% 24.12/24.37 thf(c_0_65, plain, ![X4316:nat]:(~p12|~ford_less_nat @ X4316 @ X4316), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax12])])])])).
% 24.12/24.37 thf(c_0_66, plain, (~p1860|~p1859|p1256), inference(fof_simplification,[status(thm)],[ax408])).
% 24.12/24.37 thf(c_0_67, plain, (p1860|~p1861|~p180), inference(split_conjunct,[status(thm)],[c_0_56])).
% 24.12/24.37 thf(c_0_68, plain, p180, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_57, c_0_58])]), c_0_42])).
% 24.12/24.37 thf(c_0_69, plain, p1861, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_60])])).
% 24.12/24.37 thf(c_0_70, plain, (~p1256|ford_less_nat @ (fpolyno578545843gree_a @ fp) @ (fpolyno578545843gree_a @ fp)), inference(fof_nnf,[status(thm)],[pax1256])).
% 24.12/24.37 thf(c_0_71, plain, ![X1:nat]:((esk1343_0)=(fpolyno578545843gree_a @ fp)|(fzero_zero_nat)=(fpolyno578545843gree_a @ fp)|(X1)!=(fpolyno578545843gree_a @ fp)|~p1404), inference(split_conjunct,[status(thm)],[c_0_61])).
% 24.12/24.37 thf(c_0_72, plain, p1404, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_62, c_0_50])])).
% 24.12/24.37 thf(c_0_73, plain, (esk474_0)!=(fzero_zero_nat), inference(rw,[status(thm)],[c_0_63, c_0_64])).
% 24.12/24.37 thf(c_0_74, plain, ![X1:nat]:(~p12|~ford_less_nat @ X1 @ X1), inference(split_conjunct,[status(thm)],[c_0_65])).
% 24.12/24.37 thf(c_0_75, plain, p12, inference(split_conjunct,[status(thm)],[ax2748])).
% 24.12/24.37 thf(c_0_76, plain, ![X1783:nat]:((ford_less_nat @ fzero_zero_nat @ esk765_0|p1859)&((~ford_less_nat @ esk765_0 @ (fpolyno578545843gree_a @ fp)|p1859)&(~ford_less_nat @ X1783 @ esk765_0|ford_less_nat @ X1783 @ (fpolyno578545843gree_a @ fp)|p1859))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1859])])])])])])).
% 24.12/24.37 thf(c_0_77, plain, (p1256|~p1860|~p1859), inference(split_conjunct,[status(thm)],[c_0_66])).
% 24.12/24.37 thf(c_0_78, plain, p1860, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_68]), c_0_69])])).
% 24.12/24.37 thf(c_0_79, plain, (ford_less_nat @ (fpolyno578545843gree_a @ fp) @ (fpolyno578545843gree_a @ fp)|~p1256), inference(split_conjunct,[status(thm)],[c_0_70])).
% 24.12/24.37 thf(c_0_80, plain, (esk474_0)=(esk1343_0), inference(er,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_64]), c_0_64]), c_0_64]), c_0_72])]), c_0_73])])).
% 24.12/24.37 thf(c_0_81, plain, ![X1:nat]:~ford_less_nat @ X1 @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_74, c_0_75])])).
% 24.12/24.37 thf(c_0_82, plain, ![X1:nat]:(ford_less_nat @ X1 @ (fpolyno578545843gree_a @ fp)|p1859|~ford_less_nat @ X1 @ esk765_0), inference(split_conjunct,[status(thm)],[c_0_76])).
% 24.12/24.37 thf(c_0_83, plain, (p1256|~p1859), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_77, c_0_78])])).
% 24.12/24.37 thf(c_0_84, plain, ~p1256, inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_79, c_0_64]), c_0_80]), c_0_64]), c_0_80]), c_0_81])).
% 24.12/24.37 thf(c_0_85, plain, (p1859|~ford_less_nat @ esk765_0 @ (fpolyno578545843gree_a @ fp)), inference(split_conjunct,[status(thm)],[c_0_76])).
% 24.12/24.37 thf(c_0_86, plain, ![X1:nat]:(ford_less_nat @ X1 @ esk1343_0|p1859|~ford_less_nat @ X1 @ esk765_0), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_64]), c_0_80])).
% 24.12/24.37 thf(c_0_87, plain, ~p1859, inference(sr,[status(thm)],[c_0_83, c_0_84])).
% 24.12/24.37 thf(c_0_88, plain, ![X4318:nat, X4319:nat]:(~p9|((X4318)=(X4319)|(ford_less_nat @ X4318 @ X4319|ford_less_nat @ X4319 @ X4318))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax9])])])])).
% 24.12/24.37 thf(c_0_89, plain, (p1859|~ford_less_nat @ esk765_0 @ esk474_0), inference(rw,[status(thm)],[c_0_85, c_0_64])).
% 24.12/24.37 thf(c_0_90, plain, ![X4298:polyno727731844poly_a, X4299:nat]:(~p20|(~fpolyno1372495879olyh_a @ X4298 @ (fsuc @ X4299)|(fpolyno578545843gree_a @ X4298)=(fzero_zero_nat))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax20])])])).
% 24.12/24.37 thf(c_0_91, plain, ![X4272:nat]:(~p32|((X4272)=(fzero_zero_nat)|(X4272)=(fsuc @ (esk2010_1 @ X4272)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax32])])])])])).
% 24.12/24.37 thf(c_0_92, plain, ![X1:nat]:(ford_less_nat @ X1 @ esk1343_0|~ford_less_nat @ X1 @ esk765_0), inference(sr,[status(thm)],[c_0_86, c_0_87])).
% 24.12/24.37 thf(c_0_93, plain, ![X2:nat, X1:nat]:((X1)=(X2)|ford_less_nat @ X1 @ X2|ford_less_nat @ X2 @ X1|~p9), inference(split_conjunct,[status(thm)],[c_0_88])).
% 24.12/24.37 thf(c_0_94, plain, p9, inference(split_conjunct,[status(thm)],[ax2751])).
% 24.12/24.37 thf(c_0_95, plain, (p1859|~ford_less_nat @ esk765_0 @ esk1343_0), inference(rw,[status(thm)],[c_0_89, c_0_80])).
% 24.12/24.37 thf(c_0_96, plain, ![X251:polyno727731844poly_a, X1:nat]:((fpolyno578545843gree_a @ X251)=(fzero_zero_nat)|~p20|~fpolyno1372495879olyh_a @ X251 @ (fsuc @ X1)), inference(split_conjunct,[status(thm)],[c_0_90])).
% 24.12/24.37 thf(c_0_97, plain, p20, inference(split_conjunct,[status(thm)],[ax2740])).
% 24.12/24.37 thf(c_0_98, plain, ![X1:nat]:((X1)=(fzero_zero_nat)|(X1)=(fsuc @ (esk2010_1 @ X1))|~p32), inference(split_conjunct,[status(thm)],[c_0_91])).
% 24.12/24.37 thf(c_0_99, plain, p32, inference(split_conjunct,[status(thm)],[ax2728])).
% 24.12/24.37 thf(c_0_100, plain, (~p173|fpolyno1372495879olyh_a @ fp @ fn), inference(fof_nnf,[status(thm)],[pax173])).
% 24.12/24.37 thf(c_0_101, plain, ~ford_less_nat @ esk1343_0 @ esk765_0, inference(spm,[status(thm)],[c_0_81, c_0_92])).
% 24.12/24.37 thf(c_0_102, plain, ![X2:nat, X1:nat]:((X1)=(X2)|ford_less_nat @ X1 @ X2|ford_less_nat @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_93, c_0_94])])).
% 24.12/24.37 thf(c_0_103, plain, ~ford_less_nat @ esk765_0 @ esk1343_0, inference(sr,[status(thm)],[c_0_95, c_0_87])).
% 24.12/24.37 thf(c_0_104, plain, (~p172|ford_less_nat @ fzero_zero_nat @ fn), inference(fof_nnf,[status(thm)],[pax172])).
% 24.12/24.37 thf(c_0_105, plain, ![X251:polyno727731844poly_a, X1:nat]:((fpolyno578545843gree_a @ X251)=(fzero_zero_nat)|~fpolyno1372495879olyh_a @ X251 @ (fsuc @ X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97])])).
% 24.12/24.37 thf(c_0_106, plain, ![X1:nat]:((fsuc @ (esk2010_1 @ X1))=(X1)|(X1)=(fzero_zero_nat)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 24.12/24.37 thf(c_0_107, plain, (fpolyno1372495879olyh_a @ fp @ fn|~p173), inference(split_conjunct,[status(thm)],[c_0_100])).
% 24.12/24.37 thf(c_0_108, plain, p173, inference(split_conjunct,[status(thm)],[ax2587])).
% 24.12/24.37 thf(c_0_109, plain, (esk1343_0)!=(fzero_zero_nat), inference(rw,[status(thm)],[c_0_73, c_0_80])).
% 24.12/24.37 thf(c_0_110, plain, (esk1343_0)=(esk765_0), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_102]), c_0_103])).
% 24.12/24.37 thf(c_0_111, plain, ![X4328:nat]:(~p3|~ford_less_nat @ X4328 @ fzero_zero_nat), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax3])])])])).
% 24.12/24.37 thf(c_0_112, plain, (ford_less_nat @ fzero_zero_nat @ fn|~p172), inference(split_conjunct,[status(thm)],[c_0_104])).
% 24.12/24.37 thf(c_0_113, plain, p172, inference(split_conjunct,[status(thm)],[ax2588])).
% 24.12/24.37 thf(c_0_114, plain, ![X251:polyno727731844poly_a, X1:nat]:((fpolyno578545843gree_a @ X251)=(fzero_zero_nat)|(X1)=(fzero_zero_nat)|~fpolyno1372495879olyh_a @ X251 @ X1), inference(spm,[status(thm)],[c_0_105, c_0_106])).
% 24.12/24.37 thf(c_0_115, plain, fpolyno1372495879olyh_a @ fp @ fn, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_107, c_0_108])])).
% 24.12/24.37 thf(c_0_116, plain, (esk765_0)!=(fzero_zero_nat), inference(rw,[status(thm)],[c_0_109, c_0_110])).
% 24.12/24.37 thf(c_0_117, plain, ![X1:nat]:(~p3|~ford_less_nat @ X1 @ fzero_zero_nat), inference(split_conjunct,[status(thm)],[c_0_111])).
% 24.12/24.37 thf(c_0_118, plain, p3, inference(split_conjunct,[status(thm)],[ax2757])).
% 24.12/24.37 thf(c_0_119, plain, ford_less_nat @ fzero_zero_nat @ fn, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_112, c_0_113])])).
% 24.12/24.37 thf(c_0_120, plain, (fn)=(fzero_zero_nat), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_114, c_0_115]), c_0_64]), c_0_80]), c_0_110]), c_0_116])).
% 24.12/24.37 thf(c_0_121, plain, ![X1:nat]:~ford_less_nat @ X1 @ fzero_zero_nat, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_117, c_0_118])])).
% 24.12/24.37 thf(c_0_122, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_119, c_0_120]), c_0_121]), ['proof']).
% 24.12/24.37 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 24.12/24.37 thf(0,theorem,((polyno578545843gree_a @ p) = zero_zero_nat),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 24.12/24.37 % SZS output end Proof
%------------------------------------------------------------------------------