%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ALG253^2 : TPTP v9.2.0. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n025.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:12:12 PM UTC 2025
% Result : Theorem 76.82s 77.08s
% Output : Proof 76.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : ALG253^2 : TPTP v9.2.0. Bugfixed v5.2.0.
% 0.04/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.35 % Computer : n025.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 8 23:35:38 EDT 2025
% 0.13/0.35 % CPUTime :
% 76.82/77.08 % SZS status Theorem
% 76.82/77.08 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 76.82/77.08 % Inferences: 20
% 76.82/77.08 % SZS output start Proof
% 76.82/77.08 thf(def_axvarid,definition,(axvarid = (![X1:term]:(((sub @ X1) @ id) = X1)))).
% 76.82/77.08 thf(def_induction2lem,definition,(induction2lem = (![X1:term>$o]:((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => (![X2:term]:(![X3:subst]:((![X4:term]:((var @ X4) => (X1 @ ((sub @ X4) @ X3)))) => (X1 @ ((sub @ X2) @ X3)))))))))).
% 76.82/77.08 thf(def_induction2,definition,(induction2 = (![X1:term>$o]:((![X2:term]:((var @ X2) => (X1 @ X2))) => ((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => ((!!) @ X1))))))).
% 76.82/77.08 thf(def_induction2_lthm,definition,(induction2_lthm = (axvarid => (induction2lem => induction2)))).
% 76.82/77.08 thf(thm,conjecture,((![X1:term]:(((sub @ X1) @ id) = X1)) => ((![X1:term>$o]:((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => (![X2:term]:(![X3:subst]:((![X4:term]:((var @ X4) => (X1 @ ((sub @ X4) @ X3)))) => (X1 @ ((sub @ X2) @ X3)))))))) => (![X1:term>$o]:((![X2:term]:((var @ X2) => (X1 @ X2))) => ((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => ((!!) @ X1)))))))).
% 76.82/77.08 thf(h0,negated_conjecture,(~(((![X1:term]:(((sub @ X1) @ id) = X1)) => ((![X1:term>$o]:((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => (![X2:term]:(![X3:subst]:((![X4:term]:((var @ X4) => (X1 @ ((sub @ X4) @ X3)))) => (X1 @ ((sub @ X2) @ X3)))))))) => (![X1:term>$o]:((![X2:term]:((var @ X2) => (X1 @ X2))) => ((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => ((!!) @ X1))))))))),inference(assume_negation,[status(cth)],[thm])).
% 76.82/77.08 thf(ax25, axiom, (p1|~(p3)), file('<stdin>', ax25)).
% 76.82/77.08 thf(ax27, axiom, ~(p1), file('<stdin>', ax27)).
% 76.82/77.08 thf(ax23, axiom, (p3|~(p5)), file('<stdin>', ax23)).
% 76.82/77.08 thf(ax5, axiom, (~(p4)|p23), file('<stdin>', ax5)).
% 76.82/77.08 thf(ax24, axiom, (p3|p4), file('<stdin>', ax24)).
% 76.82/77.08 thf(ax22, axiom, (p5|~(p6)), file('<stdin>', ax22)).
% 76.82/77.08 thf(ax18, axiom, (p8|~(p10)), file('<stdin>', ax18)).
% 76.82/77.08 thf(ax6, axiom, (~(p23)|~(p9)|p22), file('<stdin>', ax6)).
% 76.82/77.08 thf(ax20, axiom, (p6|~(p8)), file('<stdin>', ax20)).
% 76.82/77.08 thf(ax17, axiom, (p10|p11), file('<stdin>', ax17)).
% 76.82/77.08 thf(ax19, axiom, (p8|p9), file('<stdin>', ax19)).
% 76.82/77.08 thf(ax16, axiom, (p10|~(p12)), file('<stdin>', ax16)).
% 76.82/77.08 thf(ax15, axiom, (p12|~(p13)), file('<stdin>', ax15)).
% 76.82/77.08 thf(ax7, axiom, (~(p22)|~(p11)|p21), file('<stdin>', ax7)).
% 76.82/77.08 thf(pax21, axiom, (p21=>![X1:term, X18:subst]:(![X4:term]:(fvar @ X4=>f__0 @ (fsub @ X4 @ X18))=>f__0 @ (fsub @ X1 @ X18))), file('<stdin>', pax21)).
% 76.82/77.08 thf(pax2, axiom, (p2=>![X1:term]:(fsub @ X1 @ fid)=(X1)), file('<stdin>', pax2)).
% 76.82/77.08 thf(ax26, axiom, (p1|p2), file('<stdin>', ax26)).
% 76.82/77.08 thf(pax7, axiom, (p7=>![X1:term]:(fvar @ X1=>f__0 @ X1)), file('<stdin>', pax7)).
% 76.82/77.08 thf(ax21, axiom, (p6|p7), file('<stdin>', ax21)).
% 76.82/77.08 thf(nax13, axiom, (p13<=f__0 @ f__1), file('<stdin>', nax13)).
% 76.82/77.08 thf(c_0_20, plain, (p1|~p3), inference(fof_simplification,[status(thm)],[ax25])).
% 76.82/77.08 thf(c_0_21, plain, ~p1, inference(fof_simplification,[status(thm)],[ax27])).
% 76.82/77.08 thf(c_0_22, plain, (p1|~p3), inference(split_conjunct,[status(thm)],[c_0_20])).
% 76.82/77.08 thf(c_0_23, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_21])).
% 76.82/77.08 thf(c_0_24, plain, (p3|~p5), inference(fof_simplification,[status(thm)],[ax23])).
% 76.82/77.08 thf(c_0_25, plain, (~p4|p23), inference(fof_simplification,[status(thm)],[ax5])).
% 76.82/77.08 thf(c_0_26, plain, (p3|p4), inference(split_conjunct,[status(thm)],[ax24])).
% 76.82/77.08 thf(c_0_27, plain, ~p3, inference(sr,[status(thm)],[c_0_22, c_0_23])).
% 76.82/77.08 thf(c_0_28, plain, (p5|~p6), inference(fof_simplification,[status(thm)],[ax22])).
% 76.82/77.08 thf(c_0_29, plain, (p3|~p5), inference(split_conjunct,[status(thm)],[c_0_24])).
% 76.82/77.08 thf(c_0_30, plain, (p8|~p10), inference(fof_simplification,[status(thm)],[ax18])).
% 76.82/77.08 thf(c_0_31, plain, (~p23|~p9|p22), inference(fof_simplification,[status(thm)],[ax6])).
% 76.82/77.08 thf(c_0_32, plain, (p23|~p4), inference(split_conjunct,[status(thm)],[c_0_25])).
% 76.82/77.08 thf(c_0_33, plain, p4, inference(sr,[status(thm)],[c_0_26, c_0_27])).
% 76.82/77.08 thf(c_0_34, plain, (p6|~p8), inference(fof_simplification,[status(thm)],[ax20])).
% 76.82/77.08 thf(c_0_35, plain, (p5|~p6), inference(split_conjunct,[status(thm)],[c_0_28])).
% 76.82/77.08 thf(c_0_36, plain, ~p5, inference(sr,[status(thm)],[c_0_29, c_0_27])).
% 76.82/77.08 thf(c_0_37, plain, (p8|~p10), inference(split_conjunct,[status(thm)],[c_0_30])).
% 76.82/77.08 thf(c_0_38, plain, (p10|p11), inference(split_conjunct,[status(thm)],[ax17])).
% 76.82/77.08 thf(c_0_39, plain, (p22|~p23|~p9), inference(split_conjunct,[status(thm)],[c_0_31])).
% 76.82/77.08 thf(c_0_40, plain, p23, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_33])])).
% 76.82/77.08 thf(c_0_41, plain, (p6|~p8), inference(split_conjunct,[status(thm)],[c_0_34])).
% 76.82/77.08 thf(c_0_42, plain, (p8|p9), inference(split_conjunct,[status(thm)],[ax19])).
% 76.82/77.08 thf(c_0_43, plain, ~p6, inference(sr,[status(thm)],[c_0_35, c_0_36])).
% 76.82/77.08 thf(c_0_44, plain, (p10|~p12), inference(fof_simplification,[status(thm)],[ax16])).
% 76.82/77.08 thf(c_0_45, plain, (p12|~p13), inference(fof_simplification,[status(thm)],[ax15])).
% 76.82/77.08 thf(c_0_46, plain, (~p22|~p11|p21), inference(fof_simplification,[status(thm)],[ax7])).
% 76.82/77.08 thf(c_0_47, plain, (p11|p8), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 76.82/77.08 thf(c_0_48, plain, (p22|~p9), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 76.82/77.08 thf(c_0_49, plain, p9, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43])).
% 76.82/77.08 thf(c_0_50, plain, (p10|~p12), inference(split_conjunct,[status(thm)],[c_0_44])).
% 76.82/77.08 thf(c_0_51, plain, (p12|~p13), inference(split_conjunct,[status(thm)],[c_0_45])).
% 76.82/77.08 thf(c_0_52, plain, ![X50:term, X51:subst]:((fvar @ (esk16_2 @ X50 @ X51)|f__0 @ (fsub @ X50 @ X51)|~p21)&(~f__0 @ (fsub @ (esk16_2 @ X50 @ X51) @ X51)|f__0 @ (fsub @ X50 @ X51)|~p21)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax21])])])])])).
% 76.82/77.08 thf(c_0_53, plain, (p21|~p22|~p11), inference(split_conjunct,[status(thm)],[c_0_46])).
% 76.82/77.08 thf(c_0_54, plain, p11, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_47]), c_0_43])).
% 76.82/77.08 thf(c_0_55, plain, p22, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])).
% 76.82/77.08 thf(c_0_56, plain, ![X74:term]:(~p2|(fsub @ X74 @ fid)=(X74)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax2])])])).
% 76.82/77.08 thf(c_0_57, plain, (p1|p2), inference(split_conjunct,[status(thm)],[ax26])).
% 76.82/77.08 thf(c_0_58, plain, ![X72:term]:(~p7|(~fvar @ X72|f__0 @ X72)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 76.82/77.08 thf(c_0_59, plain, (p6|p7), inference(split_conjunct,[status(thm)],[ax21])).
% 76.82/77.08 thf(c_0_60, plain, (p10|~p13), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 76.82/77.08 thf(c_0_61, plain, ![X1:term, X3:subst]:(f__0 @ (fsub @ X1 @ X3)|~f__0 @ (fsub @ (esk16_2 @ X1 @ X3) @ X3)|~p21), inference(split_conjunct,[status(thm)],[c_0_52])).
% 76.82/77.08 thf(c_0_62, plain, p21, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54]), c_0_55])])).
% 76.82/77.08 thf(c_0_63, plain, ![X1:term]:((fsub @ X1 @ fid)=(X1)|~p2), inference(split_conjunct,[status(thm)],[c_0_56])).
% 76.82/77.08 thf(c_0_64, plain, p2, inference(sr,[status(thm)],[c_0_57, c_0_23])).
% 76.82/77.08 thf(c_0_65, plain, ![X1:term]:(f__0 @ X1|~p7|~fvar @ X1), inference(split_conjunct,[status(thm)],[c_0_58])).
% 76.82/77.08 thf(c_0_66, plain, p7, inference(sr,[status(thm)],[c_0_59, c_0_43])).
% 76.82/77.08 thf(c_0_67, plain, ![X1:term, X3:subst]:(fvar @ (esk16_2 @ X1 @ X3)|f__0 @ (fsub @ X1 @ X3)|~p21), inference(split_conjunct,[status(thm)],[c_0_52])).
% 76.82/77.08 thf(c_0_68, plain, (~f__0 @ f__1|p13), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])).
% 76.82/77.08 thf(c_0_69, plain, (p8|~p13), inference(spm,[status(thm)],[c_0_37, c_0_60])).
% 76.82/77.08 thf(c_0_70, plain, ![X1:term, X3:subst]:(f__0 @ (fsub @ X1 @ X3)|~f__0 @ (fsub @ (esk16_2 @ X1 @ X3) @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 76.82/77.08 thf(c_0_71, plain, ![X1:term]:(fsub @ X1 @ fid)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 76.82/77.08 thf(c_0_72, plain, ![X1:term]:(f__0 @ X1|~fvar @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66])])).
% 76.82/77.08 thf(c_0_73, plain, ![X1:term, X3:subst]:(fvar @ (esk16_2 @ X1 @ X3)|f__0 @ (fsub @ X1 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_62])])).
% 76.82/77.08 thf(c_0_74, plain, (p13|~f__0 @ f__1), inference(split_conjunct,[status(thm)],[c_0_68])).
% 76.82/77.08 thf(c_0_75, plain, ~p13, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_69]), c_0_43])).
% 76.82/77.08 thf(c_0_76, plain, ![X1:term]:(f__0 @ X1|~f__0 @ (esk16_2 @ X1 @ fid)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_71]), c_0_71])).
% 76.82/77.08 thf(c_0_77, plain, ![X1:term, X3:subst]:(f__0 @ (fsub @ X1 @ X3)|f__0 @ (esk16_2 @ X1 @ X3)), inference(spm,[status(thm)],[c_0_72, c_0_73])).
% 76.82/77.08 thf(c_0_78, plain, ~f__0 @ f__1, inference(sr,[status(thm)],[c_0_74, c_0_75])).
% 76.82/77.08 thf(c_0_79, plain, ![X1:term]:f__0 @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_77]), c_0_71])])).
% 76.82/77.08 thf(c_0_80, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_79])]), ['proof']).
% 76.82/77.08 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 76.82/77.08 thf(0,theorem,((![X1:term]:(((sub @ X1) @ id) = X1)) => ((![X1:term>$o]:((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => (![X2:term]:(![X3:subst]:((![X4:term]:((var @ X4) => (X1 @ ((sub @ X4) @ X3)))) => (X1 @ ((sub @ X2) @ X3)))))))) => (![X1:term>$o]:((![X2:term]:((var @ X2) => (X1 @ X2))) => ((![X2:term]:(![X3:term]:((X1 @ X2) => ((X1 @ X3) => (X1 @ ((ap @ X2) @ X3)))))) => ((![X2:term]:((![X3:term]:((X1 @ X3) => (X1 @ ((sub @ X2) @ ((push @ X3) @ id))))) => (X1 @ (lam @ X2)))) => ((!!) @ X1))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 76.82/77.08 % SZS output end Proof
%------------------------------------------------------------------------------