%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP054^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 : n004.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:50 PM UTC 2025
% Result : Theorem 109.55s 109.49s
% Output : Proof 109.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : ITP054^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.11/0.33 % Computer : n004.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Wed Oct 8 18:31:38 EDT 2025
% 0.11/0.33 % CPUTime :
% 109.55/109.49 % SZS status Theorem
% 109.55/109.49 % Mode: mode505:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=256:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 109.55/109.49 % Inferences: 10
% 109.55/109.49 % SZS output start Proof
% 109.55/109.49 thf(conj_0,conjecture,((ord_less_nat @ n1) @ (size_s1406904903t_unit @ (fe @ index)))).
% 109.55/109.49 thf(h0,negated_conjecture,(~(((ord_less_nat @ n1) @ (size_s1406904903t_unit @ (fe @ index))))),inference(assume_negation,[status(cth)],[conj_0])).
% 109.55/109.49 thf(pax12, axiom, (p12=>![X48:nat]:~(ford_less_nat @ X48 @ X48)), file('<stdin>', pax12)).
% 109.55/109.49 thf(pax30, axiom, (p30=>![X48:nat, X49:nat]:(ford_less_nat @ X48 @ X49=>ford_less_nat @ X48 @ (fsuc @ X49))), file('<stdin>', pax30)).
% 109.55/109.49 thf(ax135, axiom, p12, file('<stdin>', ax135)).
% 109.55/109.49 thf(ax117, axiom, p30, file('<stdin>', ax117)).
% 109.55/109.49 thf(pax22, axiom, (p22=>![X48:nat, X49:nat, X31:nat]:(ford_less_nat @ X48 @ X49=>(ford_less_nat @ X49 @ X31=>ford_less_nat @ (fsuc @ X48) @ X31))), file('<stdin>', pax22)).
% 109.55/109.49 thf(pax3, axiom, (p3=>ford_less_nat @ fnMsg @ (fsize_s1406904903t_unit @ (ffe @ findex))), file('<stdin>', pax3)).
% 109.55/109.49 thf(nax2, axiom, (p2<=ford_less_nat @ fnMsg @ fn1), file('<stdin>', nax2)).
% 109.55/109.49 thf(ax145, axiom, ~(p2), file('<stdin>', ax145)).
% 109.55/109.49 thf(pax44, axiom, (p44=>![X40:nat, X41:nat]:(~((X40)=(X41))=>(~(ford_less_nat @ X40 @ X41)=>ford_less_nat @ X41 @ X40))), file('<stdin>', pax44)).
% 109.55/109.49 thf(ax125, axiom, p22, file('<stdin>', ax125)).
% 109.55/109.49 thf(ax144, axiom, p3, file('<stdin>', ax144)).
% 109.55/109.49 thf(ax103, axiom, p44, file('<stdin>', ax103)).
% 109.55/109.49 thf(nax1, axiom, (p1<=ford_less_nat @ fn1 @ (fsize_s1406904903t_unit @ (ffe @ findex))), file('<stdin>', nax1)).
% 109.55/109.49 thf(ax146, axiom, ~(p1), file('<stdin>', ax146)).
% 109.55/109.49 thf(c_0_14, plain, ![X331:nat]:(~p12|~ford_less_nat @ X331 @ X331), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax12])])])])).
% 109.55/109.49 thf(c_0_15, plain, ![X299:nat, X300:nat]:(~p30|(~ford_less_nat @ X299 @ X300|ford_less_nat @ X299 @ (fsuc @ X300))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax30])])])).
% 109.55/109.49 thf(c_0_16, plain, ![X1:nat]:(~p12|~ford_less_nat @ X1 @ X1), inference(split_conjunct,[status(thm)],[c_0_14])).
% 109.55/109.49 thf(c_0_17, plain, p12, inference(split_conjunct,[status(thm)],[ax135])).
% 109.55/109.49 thf(c_0_18, plain, ![X1:nat, X3:nat]:(ford_less_nat @ X1 @ (fsuc @ X3)|~p30|~ford_less_nat @ X1 @ X3), inference(split_conjunct,[status(thm)],[c_0_15])).
% 109.55/109.49 thf(c_0_19, plain, p30, inference(split_conjunct,[status(thm)],[ax117])).
% 109.55/109.49 thf(c_0_20, plain, ![X311:nat, X312:nat, X313:nat]:(~p22|(~ford_less_nat @ X311 @ X312|(~ford_less_nat @ X312 @ X313|ford_less_nat @ (fsuc @ X311) @ X313))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 109.55/109.49 thf(c_0_21, plain, (~p3|ford_less_nat @ fnMsg @ (fsize_s1406904903t_unit @ (ffe @ findex))), inference(fof_nnf,[status(thm)],[pax3])).
% 109.55/109.49 thf(c_0_22, plain, (~ford_less_nat @ fnMsg @ fn1|p2), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])])).
% 109.55/109.49 thf(c_0_23, plain, ~p2, inference(fof_simplification,[status(thm)],[ax145])).
% 109.55/109.49 thf(c_0_24, plain, ![X251:nat, X252:nat]:(~p44|((X251)=(X252)|(ford_less_nat @ X251 @ X252|ford_less_nat @ X252 @ X251))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax44])])])])).
% 109.55/109.49 thf(c_0_25, plain, ![X1:nat]:~ford_less_nat @ X1 @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17])])).
% 109.55/109.49 thf(c_0_26, plain, ![X1:nat, X3:nat]:(ford_less_nat @ X1 @ (fsuc @ X3)|~ford_less_nat @ X1 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 109.55/109.49 thf(c_0_27, plain, ![X1:nat, X3:nat, X4:nat]:(ford_less_nat @ (fsuc @ X1) @ X4|~p22|~ford_less_nat @ X1 @ X3|~ford_less_nat @ X3 @ X4), inference(split_conjunct,[status(thm)],[c_0_20])).
% 109.55/109.49 thf(c_0_28, plain, p22, inference(split_conjunct,[status(thm)],[ax125])).
% 109.55/109.49 thf(c_0_29, plain, (ford_less_nat @ fnMsg @ (fsize_s1406904903t_unit @ (ffe @ findex))|~p3), inference(split_conjunct,[status(thm)],[c_0_21])).
% 109.55/109.49 thf(c_0_30, plain, p3, inference(split_conjunct,[status(thm)],[ax144])).
% 109.55/109.49 thf(c_0_31, plain, (p2|~ford_less_nat @ fnMsg @ fn1), inference(split_conjunct,[status(thm)],[c_0_22])).
% 109.55/109.49 thf(c_0_32, plain, ~p2, inference(split_conjunct,[status(thm)],[c_0_23])).
% 109.55/109.49 thf(c_0_33, plain, ![X3:nat, X1:nat]:((X1)=(X3)|ford_less_nat @ X1 @ X3|ford_less_nat @ X3 @ X1|~p44), inference(split_conjunct,[status(thm)],[c_0_24])).
% 109.55/109.49 thf(c_0_34, plain, p44, inference(split_conjunct,[status(thm)],[ax103])).
% 109.55/109.49 thf(c_0_35, plain, ![X1:nat]:~ford_less_nat @ (fsuc @ X1) @ X1, inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 109.55/109.49 thf(c_0_36, plain, ![X1:nat, X3:nat, X4:nat]:(ford_less_nat @ (fsuc @ X1) @ X3|~ford_less_nat @ X4 @ X3|~ford_less_nat @ X1 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28])])).
% 109.55/109.49 thf(c_0_37, plain, ford_less_nat @ fnMsg @ (fsize_s1406904903t_unit @ (ffe @ findex)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 109.55/109.49 thf(c_0_38, plain, ~ford_less_nat @ fnMsg @ fn1, inference(sr,[status(thm)],[c_0_31, c_0_32])).
% 109.55/109.49 thf(c_0_39, plain, ![X3:nat, X1:nat]:((X1)=(X3)|ford_less_nat @ X1 @ X3|ford_less_nat @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 109.55/109.49 thf(c_0_40, plain, ![X1:nat]:~ford_less_nat @ (fsuc @ (fsuc @ X1)) @ X1, inference(spm,[status(thm)],[c_0_35, c_0_26])).
% 109.55/109.49 thf(c_0_41, plain, ![X1:nat]:(ford_less_nat @ (fsuc @ X1) @ (fsize_s1406904903t_unit @ (ffe @ findex))|~ford_less_nat @ X1 @ fnMsg), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 109.55/109.49 thf(c_0_42, plain, ((fnMsg)=(fn1)|ford_less_nat @ fn1 @ fnMsg), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 109.55/109.49 thf(c_0_43, plain, (~ford_less_nat @ fn1 @ (fsize_s1406904903t_unit @ (ffe @ findex))|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 109.55/109.49 thf(c_0_44, plain, ~p1, inference(fof_simplification,[status(thm)],[ax146])).
% 109.55/109.49 thf(c_0_45, plain, ~ford_less_nat @ (fsuc @ (fsize_s1406904903t_unit @ (ffe @ findex))) @ fnMsg, inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 109.55/109.49 thf(c_0_46, plain, ![X1:nat]:((fnMsg)=(fn1)|ford_less_nat @ (fsuc @ X1) @ fnMsg|~ford_less_nat @ X1 @ fn1), inference(spm,[status(thm)],[c_0_36, c_0_42])).
% 109.55/109.49 thf(c_0_47, plain, (p1|~ford_less_nat @ fn1 @ (fsize_s1406904903t_unit @ (ffe @ findex))), inference(split_conjunct,[status(thm)],[c_0_43])).
% 109.55/109.49 thf(c_0_48, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_44])).
% 109.55/109.49 thf(c_0_49, plain, ((fnMsg)=(fn1)|~ford_less_nat @ (fsize_s1406904903t_unit @ (ffe @ findex)) @ fn1), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 109.55/109.49 thf(c_0_50, plain, ~ford_less_nat @ fn1 @ (fsize_s1406904903t_unit @ (ffe @ findex)), inference(sr,[status(thm)],[c_0_47, c_0_48])).
% 109.55/109.49 thf(c_0_51, plain, ((fsize_s1406904903t_unit @ (ffe @ findex))=(fn1)|(fnMsg)=(fn1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_39]), c_0_50])).
% 109.55/109.49 thf(c_0_52, plain, (fnMsg)=(fn1), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_51]), c_0_38])).
% 109.55/109.49 thf(c_0_53, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_52]), c_0_50]), ['proof']).
% 109.55/109.49 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 109.55/109.49 thf(0,theorem,((ord_less_nat @ n1) @ (size_s1406904903t_unit @ (fe @ index))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 109.55/109.49 % SZS output end Proof
%------------------------------------------------------------------------------