%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP061^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 : n011.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:51 PM UTC 2025
% Result : Theorem 170.61s 170.27s
% Output : Proof 170.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ITP061^1 : TPTP v9.2.0. Released v7.5.0.
% 0.06/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.33 % Computer : n011.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Oct 8 18:23:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 170.61/170.27 % SZS status Theorem
% 170.61/170.27 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 170.61/170.27 % Inferences: 49
% 170.61/170.27 % SZS output start Proof
% 170.61/170.27 thf(conj_0,conjecture,(occM2 = ((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index))) @ one_one_nat))).
% 170.61/170.27 thf(h0,negated_conjecture,(~((occM2 = ((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index))) @ one_one_nat)))),inference(assume_negation,[status(cth)],[conj_0])).
% 170.61/170.27 thf(pax47, axiom, (p47=>![X42:nat, X52:nat]:(ford_less_nat @ X42 @ X52=>~(ford_less_nat @ X52 @ X42))), file('<stdin>', pax47)).
% 170.61/170.27 thf(pax150, axiom, (p150=>![X33:nat, X34:nat]:(ford_less_nat @ (fsuc @ X33) @ X34=>~(![X35:nat]:(ford_less_nat @ X33 @ X35=>~((X34)=(fsuc @ X35)))))), file('<stdin>', pax150)).
% 170.61/170.27 thf(pax159, axiom, (p159=>![X33:nat]:(fminus_minus_nat @ (fsuc @ X33) @ fone_one_nat)=(X33)), file('<stdin>', pax159)).
% 170.61/170.27 thf(pax156, axiom, (p156=>![X33:nat, X34:nat]:(ford_less_nat @ X33 @ X34=>ford_less_eq_nat @ (fsuc @ X33) @ X34)), file('<stdin>', pax156)).
% 170.61/170.27 thf(pax175, axiom, (p175=>ford_less_nat @ foccM2 @ (fsize_s1406904903t_unit @ (ffe @ findex))), file('<stdin>', pax175)).
% 170.61/170.27 thf(ax387, axiom, p47, file('<stdin>', ax387)).
% 170.61/170.27 thf(ax284, axiom, p150, file('<stdin>', ax284)).
% 170.61/170.27 thf(ax275, axiom, p159, file('<stdin>', ax275)).
% 170.61/170.27 thf(pax25, axiom, (p25=>![X42:nat, X60:nat]:(ford_less_eq_nat @ X42 @ X60=>(~((X42)=(X60))=>ford_less_nat @ X42 @ X60))), file('<stdin>', pax25)).
% 170.61/170.27 thf(pax174, axiom, (p174=>ford_less_eq_nat @ (fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat) @ foccM2), file('<stdin>', pax174)).
% 170.61/170.27 thf(nax1, axiom, (p1<=(foccM2)=(fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat)), file('<stdin>', nax1)).
% 170.61/170.27 thf(ax433, axiom, ~(p1), file('<stdin>', ax433)).
% 170.61/170.27 thf(ax278, axiom, p156, file('<stdin>', ax278)).
% 170.61/170.27 thf(ax259, axiom, p175, file('<stdin>', ax259)).
% 170.61/170.27 thf(ax409, axiom, p25, file('<stdin>', ax409)).
% 170.61/170.27 thf(ax260, axiom, p174, file('<stdin>', ax260)).
% 170.61/170.27 thf(pax51, axiom, (p51=>![X42:nat]:~(ford_less_nat @ X42 @ X42)), file('<stdin>', pax51)).
% 170.61/170.27 thf(ax383, axiom, p51, file('<stdin>', ax383)).
% 170.61/170.27 thf(c_0_18, plain, ![X511:nat, X512:nat]:(~p47|(~ford_less_nat @ X511 @ X512|~ford_less_nat @ X512 @ X511)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax47])])])])).
% 170.61/170.27 thf(c_0_19, plain, ![X209:nat, X210:nat]:((ford_less_nat @ X209 @ (esk70_2 @ X209 @ X210)|~ford_less_nat @ (fsuc @ X209) @ X210|~p150)&((X210)=(fsuc @ (esk70_2 @ X209 @ X210))|~ford_less_nat @ (fsuc @ X209) @ X210|~p150)), 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)],[pax150])])])])])])).
% 170.61/170.27 thf(c_0_20, plain, ![X175:nat]:(~p159|(fminus_minus_nat @ (fsuc @ X175) @ fone_one_nat)=(X175)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax159])])])).
% 170.61/170.27 thf(c_0_21, plain, ![X187:nat, X188:nat]:(~p156|(~ford_less_nat @ X187 @ X188|ford_less_eq_nat @ (fsuc @ X187) @ X188)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax156])])])).
% 170.61/170.27 thf(c_0_22, plain, (~p175|ford_less_nat @ foccM2 @ (fsize_s1406904903t_unit @ (ffe @ findex))), inference(fof_nnf,[status(thm)],[pax175])).
% 170.61/170.27 thf(c_0_23, plain, ![X2:nat, X1:nat]:(~p47|~ford_less_nat @ X1 @ X2|~ford_less_nat @ X2 @ X1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 170.61/170.27 thf(c_0_24, plain, p47, inference(split_conjunct,[status(thm)],[ax387])).
% 170.61/170.27 thf(c_0_25, plain, ![X1:nat, X2:nat]:(ford_less_nat @ X1 @ (esk70_2 @ X1 @ X2)|~ford_less_nat @ (fsuc @ X1) @ X2|~p150), inference(split_conjunct,[status(thm)],[c_0_19])).
% 170.61/170.27 thf(c_0_26, plain, p150, inference(split_conjunct,[status(thm)],[ax284])).
% 170.61/170.27 thf(c_0_27, plain, ![X1:nat]:((fminus_minus_nat @ (fsuc @ X1) @ fone_one_nat)=(X1)|~p159), inference(split_conjunct,[status(thm)],[c_0_20])).
% 170.61/170.27 thf(c_0_28, plain, p159, inference(split_conjunct,[status(thm)],[ax275])).
% 170.61/170.27 thf(c_0_29, plain, ![X2:nat, X1:nat]:((X1)=(fsuc @ (esk70_2 @ X2 @ X1))|~ford_less_nat @ (fsuc @ X2) @ X1|~p150), inference(split_conjunct,[status(thm)],[c_0_19])).
% 170.61/170.27 thf(c_0_30, plain, ![X611:nat, X612:nat]:(~p25|(~ford_less_eq_nat @ X611 @ X612|((X611)=(X612)|ford_less_nat @ X611 @ X612))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax25])])])])).
% 170.61/170.27 thf(c_0_31, plain, (~p174|ford_less_eq_nat @ (fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat) @ foccM2), inference(fof_nnf,[status(thm)],[pax174])).
% 170.61/170.27 thf(c_0_32, plain, ((foccM2)!=(fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat)|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 170.61/170.27 thf(c_0_33, plain, ~p1, inference(fof_simplification,[status(thm)],[ax433])).
% 170.61/170.27 thf(c_0_34, plain, ![X1:nat, X2:nat]:(ford_less_eq_nat @ (fsuc @ X1) @ X2|~p156|~ford_less_nat @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_21])).
% 170.61/170.27 thf(c_0_35, plain, p156, inference(split_conjunct,[status(thm)],[ax278])).
% 170.61/170.27 thf(c_0_36, plain, (ford_less_nat @ foccM2 @ (fsize_s1406904903t_unit @ (ffe @ findex))|~p175), inference(split_conjunct,[status(thm)],[c_0_22])).
% 170.61/170.27 thf(c_0_37, plain, p175, inference(split_conjunct,[status(thm)],[ax259])).
% 170.61/170.27 thf(c_0_38, plain, ![X2:nat, X1:nat]:(~ford_less_nat @ X1 @ X2|~ford_less_nat @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 170.61/170.27 thf(c_0_39, plain, ![X1:nat, X2:nat]:(ford_less_nat @ X1 @ (esk70_2 @ X1 @ X2)|~ford_less_nat @ (fsuc @ X1) @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 170.61/170.27 thf(c_0_40, plain, ![X1:nat]:(fminus_minus_nat @ (fsuc @ X1) @ fone_one_nat)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28])])).
% 170.61/170.27 thf(c_0_41, plain, ![X1:nat, X2:nat]:((fsuc @ (esk70_2 @ X1 @ X2))=(X2)|~ford_less_nat @ (fsuc @ X1) @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_26])])).
% 170.61/170.27 thf(c_0_42, plain, ![X1:nat, X2:nat]:((X1)=(X2)|ford_less_nat @ X1 @ X2|~p25|~ford_less_eq_nat @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_30])).
% 170.61/170.27 thf(c_0_43, plain, p25, inference(split_conjunct,[status(thm)],[ax409])).
% 170.61/170.27 thf(c_0_44, plain, (ford_less_eq_nat @ (fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat) @ foccM2|~p174), inference(split_conjunct,[status(thm)],[c_0_31])).
% 170.61/170.27 thf(c_0_45, plain, p174, inference(split_conjunct,[status(thm)],[ax260])).
% 170.61/170.27 thf(c_0_46, plain, (p1|(foccM2)!=(fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 170.61/170.27 thf(c_0_47, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_33])).
% 170.61/170.27 thf(c_0_48, plain, ![X1:nat, X2:nat]:(ford_less_eq_nat @ (fsuc @ X1) @ X2|~ford_less_nat @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 170.61/170.27 thf(c_0_49, plain, ford_less_nat @ foccM2 @ (fsize_s1406904903t_unit @ (ffe @ findex)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 170.61/170.27 thf(c_0_50, plain, ![X1:nat, X2:nat]:(~ford_less_nat @ (esk70_2 @ X1 @ X2) @ X1|~ford_less_nat @ (fsuc @ X1) @ X2), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 170.61/170.27 thf(c_0_51, plain, ![X1:nat, X2:nat]:((esk70_2 @ X1 @ X2)=(fminus_minus_nat @ X2 @ fone_one_nat)|~ford_less_nat @ (fsuc @ X1) @ X2), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 170.61/170.27 thf(c_0_52, plain, ![X1:nat, X2:nat]:((X1)=(X2)|ford_less_nat @ X1 @ X2|~ford_less_eq_nat @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 170.61/170.27 thf(c_0_53, plain, ford_less_eq_nat @ (fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat) @ foccM2, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_45])])).
% 170.61/170.27 thf(c_0_54, plain, (fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat)!=(foccM2), inference(sr,[status(thm)],[c_0_46, c_0_47])).
% 170.61/170.27 thf(c_0_55, plain, ford_less_eq_nat @ (fsuc @ foccM2) @ (fsize_s1406904903t_unit @ (ffe @ findex)), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 170.61/170.27 thf(c_0_56, plain, ![X2:nat, X1:nat]:(~ford_less_nat @ (fminus_minus_nat @ X1 @ fone_one_nat) @ X2|~ford_less_nat @ (fsuc @ X2) @ X1), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 170.61/170.27 thf(c_0_57, plain, ford_less_nat @ (fminus_minus_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fone_one_nat) @ foccM2, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_53]), c_0_54])).
% 170.61/170.27 thf(c_0_58, plain, ![X495:nat]:(~p51|~ford_less_nat @ X495 @ X495), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax51])])])])).
% 170.61/170.27 thf(c_0_59, plain, ((fsize_s1406904903t_unit @ (ffe @ findex))=(fsuc @ foccM2)|ford_less_nat @ (fsuc @ foccM2) @ (fsize_s1406904903t_unit @ (ffe @ findex))), inference(spm,[status(thm)],[c_0_52, c_0_55])).
% 170.61/170.27 thf(c_0_60, plain, ~ford_less_nat @ (fsuc @ foccM2) @ (fsize_s1406904903t_unit @ (ffe @ findex)), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 170.61/170.27 thf(c_0_61, plain, ![X1:nat]:(~p51|~ford_less_nat @ X1 @ X1), inference(split_conjunct,[status(thm)],[c_0_58])).
% 170.61/170.27 thf(c_0_62, plain, p51, inference(split_conjunct,[status(thm)],[ax383])).
% 170.61/170.27 thf(c_0_63, plain, (fsize_s1406904903t_unit @ (ffe @ findex))=(fsuc @ foccM2), inference(sr,[status(thm)],[c_0_59, c_0_60])).
% 170.61/170.27 thf(c_0_64, plain, ![X1:nat]:~ford_less_nat @ X1 @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 170.61/170.27 thf(c_0_65, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_57, c_0_63]), c_0_40]), c_0_64]), ['proof']).
% 170.61/170.27 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 170.61/170.27 thf(0,theorem,(occM2 = ((minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index))) @ one_one_nat)),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 170.61/170.27 % SZS output end Proof
%------------------------------------------------------------------------------