%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU655^2 : TPTP v9.2.0. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n019.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 02:44:39 PM UTC 2025
% Result : Theorem 109.05s 108.13s
% Output : Proof 109.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU655^2 : TPTP v9.2.0. Released v3.7.0.
% 0.06/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 21:01:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 109.05/108.13 % SZS status Theorem
% 109.05/108.13 % Mode: mode447
% 109.05/108.13 % Inferences: 32
% 109.05/108.13 % SZS output start Proof
% 109.05/108.13 thf(ty_kfst, type, kfst : ($i>$i)).
% 109.05/108.13 thf(ty_eigen__2, type, eigen__2 : $i).
% 109.05/108.13 thf(ty_setunion, type, setunion : ($i>$i)).
% 109.05/108.13 thf(ty_eigen__1, type, eigen__1 : $i).
% 109.05/108.13 thf(ty_eigen__0, type, eigen__0 : $i).
% 109.05/108.13 thf(ty_emptyset, type, emptyset : $i).
% 109.05/108.13 thf(ty_dsetconstr, type, dsetconstr : ($i>($i>$o)>$i)).
% 109.05/108.13 thf(ty_in, type, in : ($i>$i>$o)).
% 109.05/108.13 thf(ty_setadjoin, type, setadjoin : ($i>$i>$i)).
% 109.05/108.13 thf(def_iskpair,definition,(iskpair = (^[X1:$i]:(~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))))))))))).
% 109.05/108.13 thf(def_kpair,definition,(kpair = (^[X1:$i]:(^[X2:$i]:((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)))))).
% 109.05/108.13 thf(def_singleton,definition,(singleton = (^[X1:$i]:(~((![X2:$i]:(((in @ X2) @ X1) => (~((X1 = ((setadjoin @ X2) @ emptyset))))))))))).
% 109.05/108.13 thf(def_ex1,definition,(ex1 = (^[X1:$i]:(^[X2:$i>$o]:(singleton @ ((dsetconstr @ X1) @ X2)))))).
% 109.05/108.13 thf(def_ex1I,definition,(ex1I = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => ((X2 @ X4) => (X4 = X3)))) => ((ex1 @ X1) @ X2))))))))).
% 109.05/108.13 thf(def_kfstpairEq,definition,(kfstpairEq = (![X1:$i]:(![X2:$i]:((kfst @ ((kpair @ X1) @ X2)) = X1))))).
% 109.05/108.13 thf(def_setukpairinjR,definition,(setukpairinjR = (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((kpair @ X1) @ X2) = ((kpair @ X3) @ X4)) => (X2 = X4)))))))).
% 109.05/108.13 thf(ksndsingleton,conjecture,((![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => ((X2 @ X4) => (X4 = X3)))) => (~((![X4:$i]:(((in @ X4) @ ((dsetconstr @ X1) @ X2)) => (~((((dsetconstr @ X1) @ X2) = ((setadjoin @ X4) @ emptyset)))))))))))))) => ((![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))) => ((![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => (X2 = X4)))))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (~((![X2:$i]:(((in @ X2) @ ((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))) = ((setadjoin @ X2) @ emptyset)))))))))))))).
% 109.05/108.13 thf(h0,negated_conjecture,(~(((![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => ((X2 @ X4) => (X4 = X3)))) => (~((![X4:$i]:(((in @ X4) @ ((dsetconstr @ X1) @ X2)) => (~((((dsetconstr @ X1) @ X2) = ((setadjoin @ X4) @ emptyset)))))))))))))) => ((![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))) => ((![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => (X2 = X4)))))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (~((![X2:$i]:(((in @ X2) @ ((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))) = ((setadjoin @ X2) @ emptyset))))))))))))))),inference(assume_negation,[status(cth)],[ksndsingleton])).
% 109.05/108.13 thf(h1,assumption,(![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => ((X2 @ X4) => (X4 = X3)))) => (~((![X4:$i]:(((in @ X4) @ ((dsetconstr @ X1) @ X2)) => (~((((dsetconstr @ X1) @ X2) = ((setadjoin @ X4) @ emptyset)))))))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h2,assumption,(~(((![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))) => ((![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => (X2 = X4)))))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (~((![X2:$i]:(((in @ X2) @ ((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))) = ((setadjoin @ X2) @ emptyset)))))))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h3,assumption,(![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))),introduced(assumption,[])).
% 109.05/108.13 thf(h4,assumption,(~(((![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => (X2 = X4)))))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (~((![X2:$i]:(((in @ X2) @ ((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))) = ((setadjoin @ X2) @ emptyset))))))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h5,assumption,(![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => (X2 = X4)))))),introduced(assumption,[])).
% 109.05/108.13 thf(h6,assumption,(~((![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (~((![X2:$i]:(((in @ X2) @ ((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))) = ((setadjoin @ X2) @ emptyset)))))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h7,assumption,(~(((~((![X1:$i]:(((in @ X1) @ (setunion @ eigen__0)) => (![X2:$i]:(((in @ X2) @ (setunion @ eigen__0)) => (~((eigen__0 = ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))))))))))) => (~((![X1:$i]:(((in @ X1) @ ((dsetconstr @ (setunion @ eigen__0)) @ (^[X2:$i]:(eigen__0 = ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ eigen__0)) @ (^[X2:$i]:(eigen__0 = ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))))) = ((setadjoin @ X1) @ emptyset))))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h8,assumption,(~((![X1:$i]:(((in @ X1) @ (setunion @ eigen__0)) => (![X2:$i]:(((in @ X2) @ (setunion @ eigen__0)) => (~((eigen__0 = ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h9,assumption,(![X1:$i]:(((in @ X1) @ ((dsetconstr @ (setunion @ eigen__0)) @ (^[X2:$i]:(eigen__0 = ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ eigen__0)) @ (^[X2:$i]:(eigen__0 = ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ eigen__0)) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))))) = ((setadjoin @ X1) @ emptyset)))))),introduced(assumption,[])).
% 109.05/108.13 thf(h10,assumption,(~((((in @ eigen__1) @ (setunion @ eigen__0)) => (![X1:$i]:(((in @ X1) @ (setunion @ eigen__0)) => (~((eigen__0 = ((setadjoin @ ((setadjoin @ eigen__1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ eigen__1) @ ((setadjoin @ X1) @ emptyset))) @ emptyset)))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h11,assumption,((in @ eigen__1) @ (setunion @ eigen__0)),introduced(assumption,[])).
% 109.05/108.13 thf(h12,assumption,(~((![X1:$i]:(((in @ X1) @ (setunion @ eigen__0)) => (~((eigen__0 = ((setadjoin @ ((setadjoin @ eigen__1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ eigen__1) @ ((setadjoin @ X1) @ emptyset))) @ emptyset))))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h13,assumption,(~((((in @ eigen__2) @ (setunion @ eigen__0)) => (~((eigen__0 = ((setadjoin @ ((setadjoin @ eigen__1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ eigen__1) @ ((setadjoin @ eigen__2) @ emptyset))) @ emptyset)))))))),introduced(assumption,[])).
% 109.05/108.13 thf(h14,assumption,((in @ eigen__2) @ (setunion @ eigen__0)),introduced(assumption,[])).
% 109.05/108.13 thf(h15,assumption,(eigen__0 = ((setadjoin @ ((setadjoin @ eigen__1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ eigen__1) @ ((setadjoin @ eigen__2) @ emptyset))) @ emptyset))),introduced(assumption,[])).
% 109.05/108.13 thf(ax150, axiom, (~(p7)|p23), file('<stdin>', ax150)).
% 109.05/108.13 thf(ax151, axiom, (~(p23)|p22), file('<stdin>', ax151)).
% 109.05/108.13 thf(ax166, axiom, p7, file('<stdin>', ax166)).
% 109.05/108.13 thf(ax146, axiom, (~(p22)|p28), file('<stdin>', ax146)).
% 109.05/108.13 thf(ax147, axiom, (~(p28)|~(p3)|p27), file('<stdin>', ax147)).
% 109.05/108.13 thf(pax6, axiom, (p6=>![X1:$i, X2:$i]:(fkfst @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X1)), file('<stdin>', pax6)).
% 109.05/108.13 thf(pax2, axiom, (p2=>(f__0)=(fsetadjoin @ (fsetadjoin @ f__1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__1 @ (fsetadjoin @ f__2 @ femptyset)) @ femptyset))), file('<stdin>', pax2)).
% 109.05/108.13 thf(ax149, axiom, (~(p26)|~(p25)|~(p1)), file('<stdin>', ax149)).
% 109.05/108.13 thf(ax148, axiom, (~(p27)|~(p24)|p26), file('<stdin>', ax148)).
% 109.05/108.13 thf(ax170, axiom, p3, file('<stdin>', ax170)).
% 109.05/108.13 thf(ax167, axiom, p6, file('<stdin>', ax167)).
% 109.05/108.13 thf(ax171, axiom, p2, file('<stdin>', ax171)).
% 109.05/108.13 thf(ax172, axiom, p1, file('<stdin>', ax172)).
% 109.05/108.13 thf(nax24, axiom, (p24<=(f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__2 @ femptyset)) @ femptyset))), file('<stdin>', nax24)).
% 109.05/108.13 thf(nax125, axiom, (p125<=(f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))), file('<stdin>', nax125)).
% 109.05/108.13 thf(nax110, axiom, (p110<=(fin @ f__4 @ (fsetunion @ f__0)=>((f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))=>(f__4)=(f__2)))), file('<stdin>', nax110)).
% 109.05/108.13 thf(ax62, axiom, (p25|~(p110)), file('<stdin>', ax62)).
% 109.05/108.13 thf(pax5, axiom, (p5=>![X1:$i, X2:$i, X3:$i, X4:$i]:((fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ X3 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X3 @ (fsetadjoin @ X4 @ femptyset)) @ femptyset))=>(X2)=(X4))), file('<stdin>', pax5)).
% 109.05/108.13 thf(pax125, axiom, (p125=>(f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))), file('<stdin>', pax125)).
% 109.05/108.13 thf(ax168, axiom, p5, file('<stdin>', ax168)).
% 109.05/108.13 thf(c_0_20, plain, (~p7|p23), inference(fof_simplification,[status(thm)],[ax150])).
% 109.05/108.13 thf(c_0_21, plain, (~p23|p22), inference(fof_simplification,[status(thm)],[ax151])).
% 109.05/108.13 thf(c_0_22, plain, (p23|~p7), inference(split_conjunct,[status(thm)],[c_0_20])).
% 109.05/108.13 thf(c_0_23, plain, p7, inference(split_conjunct,[status(thm)],[ax166])).
% 109.05/108.13 thf(c_0_24, plain, (~p22|p28), inference(fof_simplification,[status(thm)],[ax146])).
% 109.05/108.13 thf(c_0_25, plain, (p22|~p23), inference(split_conjunct,[status(thm)],[c_0_21])).
% 109.05/108.13 thf(c_0_26, plain, p23, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 109.05/108.13 thf(c_0_27, plain, (~p28|~p3|p27), inference(fof_simplification,[status(thm)],[ax147])).
% 109.05/108.13 thf(c_0_28, plain, (p28|~p22), inference(split_conjunct,[status(thm)],[c_0_24])).
% 109.05/108.13 thf(c_0_29, plain, p22, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 109.05/108.13 thf(c_0_30, plain, ![X235:$i, X236:$i]:(~p6|(fkfst @ (fsetadjoin @ (fsetadjoin @ X235 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X235 @ (fsetadjoin @ X236 @ femptyset)) @ femptyset)))=(X235)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 109.05/108.13 thf(c_0_31, plain, (~p2|(f__0)=(fsetadjoin @ (fsetadjoin @ f__1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__1 @ (fsetadjoin @ f__2 @ femptyset)) @ femptyset))), inference(fof_nnf,[status(thm)],[pax2])).
% 109.05/108.13 thf(c_0_32, plain, (~p26|~p25|~p1), inference(fof_simplification,[status(thm)],[ax149])).
% 109.05/108.13 thf(c_0_33, plain, (~p27|~p24|p26), inference(fof_simplification,[status(thm)],[ax148])).
% 109.05/108.13 thf(c_0_34, plain, (p27|~p28|~p3), inference(split_conjunct,[status(thm)],[c_0_27])).
% 109.05/108.13 thf(c_0_35, plain, p3, inference(split_conjunct,[status(thm)],[ax170])).
% 109.05/108.13 thf(c_0_36, plain, p28, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 109.05/108.13 thf(c_0_37, plain, ![X2:$i, X1:$i]:((fkfst @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X1)|~p6), inference(split_conjunct,[status(thm)],[c_0_30])).
% 109.05/108.13 thf(c_0_38, plain, p6, inference(split_conjunct,[status(thm)],[ax167])).
% 109.05/108.13 thf(c_0_39, plain, ((f__0)=(fsetadjoin @ (fsetadjoin @ f__1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__1 @ (fsetadjoin @ f__2 @ femptyset)) @ femptyset))|~p2), inference(split_conjunct,[status(thm)],[c_0_31])).
% 109.05/108.13 thf(c_0_40, plain, p2, inference(split_conjunct,[status(thm)],[ax171])).
% 109.05/108.13 thf(c_0_41, plain, (~p26|~p25|~p1), inference(split_conjunct,[status(thm)],[c_0_32])).
% 109.05/108.13 thf(c_0_42, plain, p1, inference(split_conjunct,[status(thm)],[ax172])).
% 109.05/108.13 thf(c_0_43, plain, (p26|~p27|~p24), inference(split_conjunct,[status(thm)],[c_0_33])).
% 109.05/108.13 thf(c_0_44, plain, p27, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35]), c_0_36])])).
% 109.05/108.13 thf(c_0_45, plain, ((f__0)!=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__2 @ femptyset)) @ femptyset))|p24), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax24])])).
% 109.05/108.13 thf(c_0_46, plain, ![X2:$i, X1:$i]:(fkfst @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 109.05/108.13 thf(c_0_47, plain, (fsetadjoin @ (fsetadjoin @ f__1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__1 @ (fsetadjoin @ f__2 @ femptyset)) @ femptyset))=(f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 109.05/108.13 thf(c_0_48, plain, (~p25|~p26), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42])])).
% 109.05/108.13 thf(c_0_49, plain, (p26|~p24), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 109.05/108.13 thf(c_0_50, plain, (p24|(f__0)!=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__2 @ femptyset)) @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_45])).
% 109.05/108.13 thf(c_0_51, plain, (fkfst @ f__0)=(f__1), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 109.05/108.13 thf(c_0_52, plain, ((f__0)!=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))|p125), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax125])])).
% 109.05/108.13 thf(c_0_53, plain, ((fin @ f__4 @ (fsetunion @ f__0)|p110)&(((f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))|p110)&((f__4)!=(f__2)|p110))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax110])])])).
% 109.05/108.13 thf(c_0_54, plain, (~p25|~p24), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 109.05/108.13 thf(c_0_55, plain, p24, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51]), c_0_51]), c_0_47])])).
% 109.05/108.13 thf(c_0_56, plain, (p25|~p110), inference(fof_simplification,[status(thm)],[ax62])).
% 109.05/108.13 thf(c_0_57, plain, (p125|(f__0)!=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_52])).
% 109.05/108.13 thf(c_0_58, plain, ((f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))|p110), inference(split_conjunct,[status(thm)],[c_0_53])).
% 109.05/108.13 thf(c_0_59, plain, ~p25, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 109.05/108.13 thf(c_0_60, plain, (p25|~p110), inference(split_conjunct,[status(thm)],[c_0_56])).
% 109.05/108.13 thf(c_0_61, plain, ![X239:$i, X240:$i, X241:$i, X242:$i]:(~p5|((fsetadjoin @ (fsetadjoin @ X239 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X239 @ (fsetadjoin @ X240 @ femptyset)) @ femptyset))!=(fsetadjoin @ (fsetadjoin @ X241 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X241 @ (fsetadjoin @ X242 @ femptyset)) @ femptyset))|(X240)=(X242))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax5])])])).
% 109.05/108.13 thf(c_0_62, plain, (~p125|(f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))), inference(fof_nnf,[status(thm)],[pax125])).
% 109.05/108.13 thf(c_0_63, plain, (p110|p125), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 109.05/108.13 thf(c_0_64, plain, ~p110, inference(spm,[status(thm)],[c_0_59, c_0_60])).
% 109.05/108.13 thf(c_0_65, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((X2)=(X4)|~p5|(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))!=(fsetadjoin @ (fsetadjoin @ X3 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X3 @ (fsetadjoin @ X4 @ femptyset)) @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_61])).
% 109.05/108.13 thf(c_0_66, plain, p5, inference(split_conjunct,[status(thm)],[ax168])).
% 109.05/108.13 thf(c_0_67, plain, ((f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))|~p125), inference(split_conjunct,[status(thm)],[c_0_62])).
% 109.05/108.13 thf(c_0_68, plain, p125, inference(sr,[status(thm)],[c_0_63, c_0_64])).
% 109.05/108.13 thf(c_0_69, plain, ![X1:$i, X4:$i, X3:$i, X2:$i]:((X1)=(X2)|(fsetadjoin @ (fsetadjoin @ X3 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X3 @ (fsetadjoin @ X1 @ femptyset)) @ femptyset))!=(fsetadjoin @ (fsetadjoin @ X4 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X4 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66])])).
% 109.05/108.13 thf(c_0_70, plain, (fsetadjoin @ (fsetadjoin @ f__1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__1 @ (fsetadjoin @ f__4 @ femptyset)) @ femptyset))=(f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_51]), c_0_51]), c_0_68])])).
% 109.05/108.13 thf(c_0_71, plain, (p110|(f__4)!=(f__2)), inference(split_conjunct,[status(thm)],[c_0_53])).
% 109.05/108.13 thf(c_0_72, plain, ![X2:$i, X1:$i]:((X1)=(f__4)|(fsetadjoin @ (fsetadjoin @ X2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X2 @ (fsetadjoin @ X1 @ femptyset)) @ femptyset))!=(f__0)), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 109.05/108.13 thf(c_0_73, plain, (f__4)!=(f__2), inference(spm,[status(thm)],[c_0_64, c_0_71])).
% 109.05/108.13 thf(c_0_74, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_47]), c_0_73]), ['proof']).
% 109.05/108.13 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h14,h15,h13,h11,h12,h10,h8,h9,h7,h5,h6,h3,h4,h1,h2,h0])],[])).
% 109.05/108.13 thf(2,plain,$false,inference(tab_negimp,[status(thm),assumptions([h13,h11,h12,h10,h8,h9,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h14,h15])],[h13,1,h14,h15])).
% 109.05/108.13 thf(3,plain,$false,inference(tab_negall,[status(thm),assumptions([h11,h12,h10,h8,h9,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h13]),tab_negall(eigenvar,eigen__2)],[h12,2,h13])).
% 109.05/108.13 thf(4,plain,$false,inference(tab_negimp,[status(thm),assumptions([h10,h8,h9,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h11,h12])],[h10,3,h11,h12])).
% 109.05/108.13 thf(5,plain,$false,inference(tab_negall,[status(thm),assumptions([h8,h9,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h10]),tab_negall(eigenvar,eigen__1)],[h8,4,h10])).
% 109.05/108.13 thf(6,plain,$false,inference(tab_negimp,[status(thm),assumptions([h7,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h8,h9])],[h7,5,h8,h9])).
% 109.05/108.13 thf(7,plain,$false,inference(tab_negall,[status(thm),assumptions([h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h7]),tab_negall(eigenvar,eigen__0)],[h6,6,h7])).
% 109.05/108.13 thf(8,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h4,h1,h2,h0]),tab_negimp(discharge,[h5,h6])],[h4,7,h5,h6])).
% 109.05/108.13 thf(9,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h2,h0]),tab_negimp(discharge,[h3,h4])],[h2,8,h3,h4])).
% 109.05/108.13 thf(10,plain,$false,inference(tab_negimp,[status(thm),assumptions([h0]),tab_negimp(discharge,[h1,h2])],[h0,9,h1,h2])).
% 109.05/108.13 thf(0,theorem,((![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => ((X2 @ X4) => (X4 = X3)))) => (~((![X4:$i]:(((in @ X4) @ ((dsetconstr @ X1) @ X2)) => (~((((dsetconstr @ X1) @ X2) = ((setadjoin @ X4) @ emptyset)))))))))))))) => ((![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))) => ((![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => (X2 = X4)))))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (~((![X2:$i]:(((in @ X2) @ ((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))) => (~((((dsetconstr @ (setunion @ X1)) @ (^[X3:$i]:(X1 = ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))) = ((setadjoin @ X2) @ emptyset))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[10,h0])).
% 109.05/108.13 % SZS output end Proof
%------------------------------------------------------------------------------