%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP026^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 : n018.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:46:44 PM UTC 2025
% Result : Theorem 165.64s 165.47s
% Output : Proof 165.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.11 % Problem : ITP026^1 : TPTP v9.2.0. Released v7.5.0.
% 0.04/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n018.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 Oct 8 18:43:23 EDT 2025
% 0.12/0.33 % CPUTime :
% 165.64/165.47 % SZS status Theorem
% 165.64/165.47 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 165.64/165.47 % Inferences: 0
% 165.64/165.47 % SZS output start Proof
% 165.64/165.47 thf(conj_21,conjecture,((member_a @ (g @ xa)) @ h1)).
% 165.64/165.47 thf(h0,negated_conjecture,(~(((member_a @ (g @ xa)) @ h1))),inference(assume_negation,[status(cth)],[conj_21])).
% 165.64/165.47 thf(pax60, axiom, (p60=>![X1:nat, X2:nat]:ford_less_eq_nat @ (fminus_minus_nat @ X1 @ X2) @ X1), file('<stdin>', pax60)).
% 165.64/165.47 thf(pax23, axiom, (p23=>![X14:nat]:(fminus_minus_nat @ X14 @ fzero_zero_nat)=(X14)), file('<stdin>', pax23)).
% 165.64/165.47 thf(pax87, axiom, (p87=>![X1:nat, X2:nat]:((fsuc @ X1)=(fsuc @ X2)=>(X1)=(X2))), file('<stdin>', pax87)).
% 165.64/165.47 thf(pax73, axiom, (p73=>![X1:nat]:(~((X1)=(fzero_zero_nat))=>~(![X2:nat]:~((X1)=(fsuc @ X2))))), file('<stdin>', pax73)).
% 165.64/165.47 thf(pax67, axiom, (p67=>![X1:nat]:~((fzero_zero_nat)=(fsuc @ X1))), file('<stdin>', pax67)).
% 165.64/165.47 thf(pax41, axiom, (p41=>![X9:nat, X2:nat]:(ford_less_eq_nat @ X9 @ X2=>(fminus_minus_nat @ (fsuc @ X2) @ X9)=(fsuc @ (fminus_minus_nat @ X2 @ X9)))), file('<stdin>', pax41)).
% 165.64/165.47 thf(pax22, axiom, (p22=>![X14:nat]:(fminus_minus_nat @ X14 @ X14)=(fzero_zero_nat)), file('<stdin>', pax22)).
% 165.64/165.47 thf(ax28, axiom, p60, file('<stdin>', ax28)).
% 165.64/165.47 thf(ax65, axiom, p23, file('<stdin>', ax65)).
% 165.64/165.47 thf(ax1, axiom, p87, file('<stdin>', ax1)).
% 165.64/165.47 thf(ax15, axiom, p73, file('<stdin>', ax15)).
% 165.64/165.47 thf(ax21, axiom, p67, file('<stdin>', ax21)).
% 165.64/165.47 thf(pax45, axiom, (p45=>![X9:nat]:(ford_less_nat @ fzero_zero_nat @ X9=>~(![X2:nat]:~((X9)=(fsuc @ X2))))), file('<stdin>', pax45)).
% 165.64/165.47 thf(ax47, axiom, p41, file('<stdin>', ax47)).
% 165.64/165.47 thf(ax66, axiom, p22, file('<stdin>', ax66)).
% 165.64/165.47 thf(ax43, axiom, p45, file('<stdin>', ax43)).
% 165.64/165.47 thf(pax79, axiom, (p79=>![X1:nat, X2:nat]:(ford_less_eq_nat @ (fsuc @ X1) @ X2=>~(![X3:nat]:~((X2)=(fsuc @ X3))))), file('<stdin>', pax79)).
% 165.64/165.47 thf(ax9, axiom, p79, file('<stdin>', ax9)).
% 165.64/165.47 thf(pax6, axiom, (p6=>ford_less_nat @ fzero_zero_nat @ fm2), file('<stdin>', pax6)).
% 165.64/165.47 thf(pax37, axiom, (p37=>![X9:nat, X2:nat]:(ford_less_nat @ X9 @ X2=>(fsuc @ (fminus_minus_nat @ X2 @ (fsuc @ X9)))=(fminus_minus_nat @ X2 @ X9))), file('<stdin>', pax37)).
% 165.64/165.47 thf(ax82, axiom, p6, file('<stdin>', ax82)).
% 165.64/165.47 thf(ax51, axiom, p37, file('<stdin>', ax51)).
% 165.64/165.47 thf(pax63, axiom, (p63=>![X1:nat]:(~((X1)=(fzero_zero_nat))=>ford_less_nat @ fzero_zero_nat @ X1)), file('<stdin>', pax63)).
% 165.64/165.47 thf(pax78, axiom, (p78=>![X1:nat, X2:nat]:(ford_less_eq_nat @ X1 @ X2=>ford_less_eq_nat @ X1 @ (fsuc @ X2))), file('<stdin>', pax78)).
% 165.64/165.47 thf(ax25, axiom, p63, file('<stdin>', ax25)).
% 165.64/165.47 thf(pax18, axiom, (p18=>![X16:nat]:(ford_less_eq_nat @ X16 @ fm2=>![X17:nat]:(ford_less_eq_nat @ X17 @ fm2=>((fg @ X16)=(fg @ X17)=>(X16)=(X17))))), file('<stdin>', pax18)).
% 165.64/165.47 thf(pax16, axiom, (p16=>(fg @ fm2)=(fh2)), file('<stdin>', pax16)).
% 165.64/165.47 thf(nax1, axiom, (p1<=fmember_a @ (fg @ fxa) @ fh1), file('<stdin>', nax1)).
% 165.64/165.47 thf(ax87, axiom, ~(p1), file('<stdin>', ax87)).
% 165.64/165.47 thf(ax10, axiom, p78, file('<stdin>', ax10)).
% 165.64/165.47 thf(ax70, axiom, p18, file('<stdin>', ax70)).
% 165.64/165.47 thf(ax72, axiom, p16, file('<stdin>', ax72)).
% 165.64/165.47 thf(pax2, axiom, (p2=>(~((fg @ fxa)=(fh2))=>fmember_a @ (fg @ fxa) @ fh1)), file('<stdin>', pax2)).
% 165.64/165.47 thf(pax3, axiom, (p3=>ford_less_eq_nat @ fxa @ (fminus_minus_nat @ fm2 @ (fsuc @ fzero_zero_nat))), file('<stdin>', pax3)).
% 165.64/165.47 thf(pax81, axiom, (p81=>![X1:nat]:~(ford_less_eq_nat @ (fsuc @ X1) @ X1)), file('<stdin>', pax81)).
% 165.64/165.47 thf(ax86, axiom, p2, file('<stdin>', ax86)).
% 165.64/165.47 thf(ax85, axiom, p3, file('<stdin>', ax85)).
% 165.64/165.47 thf(ax7, axiom, p81, file('<stdin>', ax7)).
% 165.64/165.47 thf(c_0_38, plain, ![X84:nat, X85:nat]:(~p60|ford_less_eq_nat @ (fminus_minus_nat @ X84 @ X85) @ X84), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax60])])])).
% 165.64/165.47 thf(c_0_39, plain, ![X200:nat]:(~p23|(fminus_minus_nat @ X200 @ fzero_zero_nat)=(X200)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax23])])])).
% 165.64/165.47 thf(c_0_40, plain, ![X26:nat, X27:nat]:(~p87|((fsuc @ X26)!=(fsuc @ X27)|(X26)=(X27))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax87])])])).
% 165.64/165.47 thf(c_0_41, plain, ![X58:nat]:(~p73|((X58)=(fzero_zero_nat)|(X58)=(fsuc @ (esk21_1 @ X58)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax73])])])])])).
% 165.64/165.47 thf(c_0_42, plain, ![X68:nat]:(~p67|(fzero_zero_nat)!=(fsuc @ X68)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax67])])])])).
% 165.64/165.47 thf(c_0_43, plain, ![X152:nat, X153:nat]:(~p41|(~ford_less_eq_nat @ X152 @ X153|(fminus_minus_nat @ (fsuc @ X153) @ X152)=(fsuc @ (fminus_minus_nat @ X153 @ X152)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax41])])])).
% 165.64/165.47 thf(c_0_44, plain, ![X202:nat]:(~p22|(fminus_minus_nat @ X202 @ X202)=(fzero_zero_nat)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 165.64/165.47 thf(c_0_45, plain, ![X2:nat, X1:nat]:(ford_less_eq_nat @ (fminus_minus_nat @ X1 @ X2) @ X1|~p60), inference(split_conjunct,[status(thm)],[c_0_38])).
% 165.64/165.47 thf(c_0_46, plain, p60, inference(split_conjunct,[status(thm)],[ax28])).
% 165.64/165.47 thf(c_0_47, plain, ![X1:nat]:((fminus_minus_nat @ X1 @ fzero_zero_nat)=(X1)|~p23), inference(split_conjunct,[status(thm)],[c_0_39])).
% 165.64/165.47 thf(c_0_48, plain, p23, inference(split_conjunct,[status(thm)],[ax65])).
% 165.64/165.47 thf(c_0_49, plain, ![X1:nat, X2:nat]:((X1)=(X2)|~p87|(fsuc @ X1)!=(fsuc @ X2)), inference(split_conjunct,[status(thm)],[c_0_40])).
% 165.64/165.47 thf(c_0_50, plain, p87, inference(split_conjunct,[status(thm)],[ax1])).
% 165.64/165.47 thf(c_0_51, plain, ![X1:nat]:((X1)=(fzero_zero_nat)|(X1)=(fsuc @ (esk21_1 @ X1))|~p73), inference(split_conjunct,[status(thm)],[c_0_41])).
% 165.64/165.47 thf(c_0_52, plain, p73, inference(split_conjunct,[status(thm)],[ax15])).
% 165.64/165.47 thf(c_0_53, plain, ![X1:nat]:(~p67|(fzero_zero_nat)!=(fsuc @ X1)), inference(split_conjunct,[status(thm)],[c_0_42])).
% 165.64/165.47 thf(c_0_54, plain, p67, inference(split_conjunct,[status(thm)],[ax21])).
% 165.64/165.47 thf(c_0_55, plain, ![X148:nat]:(~p45|(~ford_less_nat @ fzero_zero_nat @ X148|(X148)=(fsuc @ (esk66_1 @ X148)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax45])])])])])).
% 165.64/165.47 thf(c_0_56, plain, ![X1:nat, X2:nat]:((fminus_minus_nat @ (fsuc @ X2) @ X1)=(fsuc @ (fminus_minus_nat @ X2 @ X1))|~p41|~ford_less_eq_nat @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_43])).
% 165.64/165.47 thf(c_0_57, plain, p41, inference(split_conjunct,[status(thm)],[ax47])).
% 165.64/165.47 thf(c_0_58, plain, ![X1:nat]:((fminus_minus_nat @ X1 @ X1)=(fzero_zero_nat)|~p22), inference(split_conjunct,[status(thm)],[c_0_44])).
% 165.64/165.47 thf(c_0_59, plain, p22, inference(split_conjunct,[status(thm)],[ax66])).
% 165.64/165.47 thf(c_0_60, plain, ![X2:nat, X1:nat]:ford_less_eq_nat @ (fminus_minus_nat @ X1 @ X2) @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46])])).
% 165.64/165.47 thf(c_0_61, plain, ![X1:nat]:(fminus_minus_nat @ X1 @ fzero_zero_nat)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_48])])).
% 165.64/165.47 thf(c_0_62, plain, ![X1:nat, X2:nat]:((X1)=(X2)|(fsuc @ X1)!=(fsuc @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50])])).
% 165.64/165.47 thf(c_0_63, plain, ![X1:nat]:((fsuc @ (esk21_1 @ X1))=(X1)|(X1)=(fzero_zero_nat)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_52])])).
% 165.64/165.47 thf(c_0_64, plain, ![X1:nat]:(fsuc @ X1)!=(fzero_zero_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 165.64/165.47 thf(c_0_65, plain, ![X1:nat]:((X1)=(fsuc @ (esk66_1 @ X1))|~p45|~ford_less_nat @ fzero_zero_nat @ X1), inference(split_conjunct,[status(thm)],[c_0_55])).
% 165.64/165.47 thf(c_0_66, plain, p45, inference(split_conjunct,[status(thm)],[ax43])).
% 165.64/165.47 thf(c_0_67, plain, ![X38:nat, X39:nat]:(~p79|(~ford_less_eq_nat @ (fsuc @ X38) @ X39|(X39)=(fsuc @ (esk11_2 @ X38 @ X39)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax79])])])])])).
% 165.64/165.47 thf(c_0_68, plain, ![X2:nat, X1:nat]:((fsuc @ (fminus_minus_nat @ X1 @ X2))=(fminus_minus_nat @ (fsuc @ X1) @ X2)|~ford_less_eq_nat @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 165.64/165.47 thf(c_0_69, plain, ![X1:nat]:(fminus_minus_nat @ X1 @ X1)=(fzero_zero_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_59])])).
% 165.64/165.47 thf(c_0_70, plain, ![X1:nat]:ford_less_eq_nat @ X1 @ X1, inference(spm,[status(thm)],[c_0_60, c_0_61])).
% 165.64/165.47 thf(c_0_71, plain, ![X1:nat]:(esk21_1 @ (fsuc @ X1))=(X1), inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63])]), c_0_64])).
% 165.64/165.47 thf(c_0_72, plain, ![X1:nat]:((fsuc @ (esk66_1 @ X1))=(X1)|~ford_less_nat @ fzero_zero_nat @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66])])).
% 165.64/165.47 thf(c_0_73, plain, ![X1:nat, X2:nat]:((X2)=(fsuc @ (esk11_2 @ X1 @ X2))|~p79|~ford_less_eq_nat @ (fsuc @ X1) @ X2), inference(split_conjunct,[status(thm)],[c_0_67])).
% 165.64/165.47 thf(c_0_74, plain, p79, inference(split_conjunct,[status(thm)],[ax9])).
% 165.64/165.47 thf(c_0_75, plain, ![X1:nat]:(fminus_minus_nat @ (fsuc @ X1) @ X1)=(fsuc @ fzero_zero_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_69]), c_0_70])])).
% 165.64/165.47 thf(c_0_76, plain, ![X1:nat]:((esk66_1 @ X1)=(esk21_1 @ X1)|~ford_less_nat @ fzero_zero_nat @ X1), inference(spm,[status(thm)],[c_0_71, c_0_72])).
% 165.64/165.47 thf(c_0_77, plain, (~p6|ford_less_nat @ fzero_zero_nat @ fm2), inference(fof_nnf,[status(thm)],[pax6])).
% 165.64/165.47 thf(c_0_78, plain, ![X166:nat, X167:nat]:(~p37|(~ford_less_nat @ X166 @ X167|(fsuc @ (fminus_minus_nat @ X167 @ (fsuc @ X166)))=(fminus_minus_nat @ X167 @ X166))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax37])])])).
% 165.64/165.47 thf(c_0_79, plain, ![X1:nat, X2:nat]:((fsuc @ (esk11_2 @ X1 @ X2))=(X2)|~ford_less_eq_nat @ (fsuc @ X1) @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74])])).
% 165.64/165.47 thf(c_0_80, plain, ![X1:nat]:ford_less_eq_nat @ (fsuc @ fzero_zero_nat) @ (fsuc @ X1), inference(spm,[status(thm)],[c_0_60, c_0_75])).
% 165.64/165.47 thf(c_0_81, plain, ![X1:nat]:((fsuc @ (esk21_1 @ X1))=(X1)|~ford_less_nat @ fzero_zero_nat @ X1), inference(spm,[status(thm)],[c_0_72, c_0_76])).
% 165.64/165.47 thf(c_0_82, plain, (ford_less_nat @ fzero_zero_nat @ fm2|~p6), inference(split_conjunct,[status(thm)],[c_0_77])).
% 165.64/165.47 thf(c_0_83, plain, p6, inference(split_conjunct,[status(thm)],[ax82])).
% 165.64/165.47 thf(c_0_84, plain, ![X1:nat, X2:nat]:((fsuc @ (fminus_minus_nat @ X2 @ (fsuc @ X1)))=(fminus_minus_nat @ X2 @ X1)|~p37|~ford_less_nat @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_78])).
% 165.64/165.47 thf(c_0_85, plain, p37, inference(split_conjunct,[status(thm)],[ax51])).
% 165.64/165.47 thf(c_0_86, plain, ![X76:nat]:(~p63|((X76)=(fzero_zero_nat)|ford_less_nat @ fzero_zero_nat @ X76)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax63])])])])).
% 165.64/165.47 thf(c_0_87, plain, ![X44:nat, X45:nat]:(~p78|(~ford_less_eq_nat @ X44 @ X45|ford_less_eq_nat @ X44 @ (fsuc @ X45))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax78])])])).
% 165.64/165.47 thf(c_0_88, plain, ![X1:nat, X2:nat]:((esk11_2 @ X1 @ X2)=(esk21_1 @ X2)|~ford_less_eq_nat @ (fsuc @ X1) @ X2), inference(spm,[status(thm)],[c_0_71, c_0_79])).
% 165.64/165.47 thf(c_0_89, plain, ![X1:nat]:(ford_less_eq_nat @ (fsuc @ fzero_zero_nat) @ X1|~ford_less_nat @ fzero_zero_nat @ X1), inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 165.64/165.47 thf(c_0_90, plain, ford_less_nat @ fzero_zero_nat @ fm2, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83])])).
% 165.64/165.47 thf(c_0_91, plain, ![X2:nat, X1:nat]:((fsuc @ (fminus_minus_nat @ X1 @ (fsuc @ X2)))=(fminus_minus_nat @ X1 @ X2)|~ford_less_nat @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_84, c_0_85])])).
% 165.79/165.47 thf(c_0_92, plain, ![X1:nat]:((X1)=(fzero_zero_nat)|ford_less_nat @ fzero_zero_nat @ X1|~p63), inference(split_conjunct,[status(thm)],[c_0_86])).
% 165.79/165.47 thf(c_0_93, plain, p63, inference(split_conjunct,[status(thm)],[ax25])).
% 165.79/165.47 thf(c_0_94, plain, ![X206:nat, X207:nat]:(~p18|(~ford_less_eq_nat @ X206 @ fm2|(~ford_less_eq_nat @ X207 @ fm2|((fg @ X206)!=(fg @ X207)|(X206)=(X207))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax18])])])).
% 165.79/165.47 thf(c_0_95, plain, (~p16|(fg @ fm2)=(fh2)), inference(fof_nnf,[status(thm)],[pax16])).
% 165.79/165.47 thf(c_0_96, plain, (~fmember_a @ (fg @ fxa) @ fh1|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 165.79/165.47 thf(c_0_97, plain, ~p1, inference(fof_simplification,[status(thm)],[ax87])).
% 165.79/165.47 thf(c_0_98, plain, ![X1:nat, X2:nat]:(ford_less_eq_nat @ X1 @ (fsuc @ X2)|~p78|~ford_less_eq_nat @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_87])).
% 165.79/165.47 thf(c_0_99, plain, p78, inference(split_conjunct,[status(thm)],[ax10])).
% 165.79/165.47 thf(c_0_100, plain, ![X2:nat, X1:nat]:((fsuc @ (esk21_1 @ X1))=(X1)|~ford_less_eq_nat @ (fsuc @ X2) @ X1), inference(spm,[status(thm)],[c_0_79, c_0_88])).
% 165.79/165.47 thf(c_0_101, plain, ford_less_eq_nat @ (fsuc @ fzero_zero_nat) @ fm2, inference(spm,[status(thm)],[c_0_89, c_0_90])).
% 165.79/165.47 thf(c_0_102, plain, ![X3:nat, X2:nat, X1:nat]:((fminus_minus_nat @ X1 @ (fsuc @ X2))=(X3)|(fminus_minus_nat @ X1 @ X2)!=(fsuc @ X3)|~ford_less_nat @ X2 @ X1), inference(spm,[status(thm)],[c_0_62, c_0_91])).
% 165.79/165.47 thf(c_0_103, plain, ![X1:nat]:((X1)=(fzero_zero_nat)|ford_less_nat @ fzero_zero_nat @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_92, c_0_93])])).
% 165.79/165.47 thf(c_0_104, plain, ![X1:nat, X2:nat]:((X1)=(X2)|~p18|~ford_less_eq_nat @ X1 @ fm2|~ford_less_eq_nat @ X2 @ fm2|(fg @ X1)!=(fg @ X2)), inference(split_conjunct,[status(thm)],[c_0_94])).
% 165.79/165.47 thf(c_0_105, plain, p18, inference(split_conjunct,[status(thm)],[ax70])).
% 165.79/165.47 thf(c_0_106, plain, ((fg @ fm2)=(fh2)|~p16), inference(split_conjunct,[status(thm)],[c_0_95])).
% 165.79/165.47 thf(c_0_107, plain, p16, inference(split_conjunct,[status(thm)],[ax72])).
% 165.79/165.47 thf(c_0_108, plain, (~p2|((fg @ fxa)=(fh2)|fmember_a @ (fg @ fxa) @ fh1)), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax2])])).
% 165.79/165.47 thf(c_0_109, plain, (p1|~fmember_a @ (fg @ fxa) @ fh1), inference(split_conjunct,[status(thm)],[c_0_96])).
% 165.79/165.47 thf(c_0_110, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_97])).
% 165.79/165.47 thf(c_0_111, plain, ![X1:nat, X2:nat]:(ford_less_eq_nat @ X1 @ (fsuc @ X2)|~ford_less_eq_nat @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 165.79/165.47 thf(c_0_112, plain, (fsuc @ (esk21_1 @ fm2))=(fm2), inference(spm,[status(thm)],[c_0_100, c_0_101])).
% 165.79/165.47 thf(c_0_113, plain, ![X1:nat]:(fminus_minus_nat @ (fsuc @ X1) @ (fsuc @ fzero_zero_nat))=(X1), inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_103]), c_0_61])]), c_0_64])).
% 165.79/165.47 thf(c_0_114, plain, (~p3|ford_less_eq_nat @ fxa @ (fminus_minus_nat @ fm2 @ (fsuc @ fzero_zero_nat))), inference(fof_nnf,[status(thm)],[pax3])).
% 165.79/165.47 thf(c_0_115, plain, ![X36:nat]:(~p81|~ford_less_eq_nat @ (fsuc @ X36) @ X36), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax81])])])])).
% 165.79/165.47 thf(c_0_116, plain, ![X2:nat, X1:nat]:((X1)=(X2)|(fg @ X1)!=(fg @ X2)|~ford_less_eq_nat @ X2 @ fm2|~ford_less_eq_nat @ X1 @ fm2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104, c_0_105])])).
% 165.79/165.47 thf(c_0_117, plain, (fg @ fm2)=(fh2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_106, c_0_107])])).
% 165.79/165.47 thf(c_0_118, plain, ((fg @ fxa)=(fh2)|fmember_a @ (fg @ fxa) @ fh1|~p2), inference(split_conjunct,[status(thm)],[c_0_108])).
% 165.79/165.47 thf(c_0_119, plain, p2, inference(split_conjunct,[status(thm)],[ax86])).
% 165.79/165.47 thf(c_0_120, plain, ~fmember_a @ (fg @ fxa) @ fh1, inference(sr,[status(thm)],[c_0_109, c_0_110])).
% 165.79/165.47 thf(c_0_121, plain, ![X1:nat]:(ford_less_eq_nat @ X1 @ fm2|~ford_less_eq_nat @ X1 @ (esk21_1 @ fm2)), inference(spm,[status(thm)],[c_0_111, c_0_112])).
% 165.79/165.47 thf(c_0_122, plain, (esk21_1 @ fm2)=(fminus_minus_nat @ fm2 @ (fsuc @ fzero_zero_nat)), inference(spm,[status(thm)],[c_0_113, c_0_112])).
% 165.79/165.47 thf(c_0_123, plain, (ford_less_eq_nat @ fxa @ (fminus_minus_nat @ fm2 @ (fsuc @ fzero_zero_nat))|~p3), inference(split_conjunct,[status(thm)],[c_0_114])).
% 165.79/165.47 thf(c_0_124, plain, p3, inference(split_conjunct,[status(thm)],[ax85])).
% 165.79/165.47 thf(c_0_125, plain, ![X1:nat]:(~p81|~ford_less_eq_nat @ (fsuc @ X1) @ X1), inference(split_conjunct,[status(thm)],[c_0_115])).
% 165.79/165.47 thf(c_0_126, plain, p81, inference(split_conjunct,[status(thm)],[ax7])).
% 165.79/165.47 thf(c_0_127, plain, ![X1:nat]:((X1)=(fm2)|(fg @ X1)!=(fh2)|~ford_less_eq_nat @ X1 @ fm2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116, c_0_117]), c_0_70])])).
% 165.79/165.47 thf(c_0_128, plain, (fg @ fxa)=(fh2), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_118, c_0_119])]), c_0_120])).
% 165.79/165.47 thf(c_0_129, plain, ![X1:nat]:(ford_less_eq_nat @ X1 @ fm2|~ford_less_eq_nat @ X1 @ (fminus_minus_nat @ fm2 @ (fsuc @ fzero_zero_nat))), inference(rw,[status(thm)],[c_0_121, c_0_122])).
% 165.79/165.47 thf(c_0_130, plain, ford_less_eq_nat @ fxa @ (fminus_minus_nat @ fm2 @ (fsuc @ fzero_zero_nat)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_123, c_0_124])])).
% 165.79/165.47 thf(c_0_131, plain, ![X1:nat]:~ford_less_eq_nat @ (fsuc @ X1) @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_125, c_0_126])])).
% 165.79/165.47 thf(c_0_132, plain, ((fxa)=(fm2)|~ford_less_eq_nat @ fxa @ fm2), inference(spm,[status(thm)],[c_0_127, c_0_128])).
% 165.79/165.47 thf(c_0_133, plain, ford_less_eq_nat @ fxa @ fm2, inference(spm,[status(thm)],[c_0_129, c_0_130])).
% 165.79/165.47 thf(c_0_134, plain, ~ford_less_eq_nat @ fm2 @ (esk21_1 @ fm2), inference(spm,[status(thm)],[c_0_131, c_0_112])).
% 165.79/165.47 thf(c_0_135, plain, (fxa)=(fm2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_132, c_0_133])])).
% 165.79/165.47 thf(c_0_136, plain, ~ford_less_eq_nat @ fm2 @ (fminus_minus_nat @ fm2 @ (fsuc @ fzero_zero_nat)), inference(rw,[status(thm)],[c_0_134, c_0_122])).
% 165.79/165.47 thf(c_0_137, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_130, c_0_135]), c_0_136]), ['proof']).
% 165.79/165.47 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 165.79/165.47 thf(0,theorem,((member_a @ (g @ xa)) @ h1),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 165.79/165.47 % SZS output end Proof
%------------------------------------------------------------------------------