%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU788^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 : n005.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:50:00 PM UTC 2025
% Result : Theorem 101.09s 101.07s
% Output : Proof 101.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU788^2 : TPTP v9.2.0. Released v3.7.0.
% 0.03/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.35 % Computer : n005.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 8 21:29:53 EDT 2025
% 0.14/0.35 % CPUTime :
% 101.09/101.07 % SZS status Theorem
% 101.09/101.07 % Mode: mode478
% 101.09/101.07 % Inferences: 550
% 101.09/101.07 % SZS output start Proof
% 101.09/101.07 thf(ty_subset, type, subset : ($i>$i>$o)).
% 101.09/101.07 thf(ty_eigen__2, type, eigen__2 : $i).
% 101.09/101.07 thf(ty_eigen__1, type, eigen__1 : $i).
% 101.09/101.07 thf(ty_eigen__0, type, eigen__0 : $i).
% 101.09/101.07 thf(ty_breln1, type, breln1 : ($i>$i>$o)).
% 101.09/101.07 thf(ty_kpair, type, kpair : ($i>$i>$i)).
% 101.09/101.07 thf(ty_in, type, in : ($i>$i>$o)).
% 101.09/101.07 thf(ty_binunion, type, binunion : ($i>$i>$i)).
% 101.09/101.07 thf(def_setextsub,definition,(setextsub = (![X1:$i]:(![X2:$i]:(((subset @ X1) @ X2) => (((subset @ X2) @ X1) => (X1 = X2))))))).
% 101.09/101.07 thf(def_subbreln1,definition,(subbreln1 = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))) => ((subset @ X2) @ X3))))))))).
% 101.09/101.07 thf(def_breln1unionprop,definition,(breln1unionprop = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ ((binunion @ X2) @ X3))))))))).
% 101.09/101.07 thf(def_breln1unionIL,definition,(breln1unionIL = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))))).
% 101.09/101.07 thf(def_breln1unionIR,definition,(breln1unionIR = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))))).
% 101.09/101.07 thf(def_breln1unionE,definition,(breln1unionE = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))))).
% 101.09/101.07 thf(breln1unionCommutes,conjecture,((![X1:$i]:(![X2:$i]:(((subset @ X1) @ X2) => (((subset @ X2) @ X1) => (X1 = X2))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))) => ((subset @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ ((binunion @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2)))))))))))))).
% 101.09/101.07 thf(h0,negated_conjecture,(~(((![X1:$i]:(![X2:$i]:(((subset @ X1) @ X2) => (((subset @ X2) @ X1) => (X1 = X2))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))) => ((subset @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ ((binunion @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))))))))))),inference(assume_negation,[status(cth)],[breln1unionCommutes])).
% 101.09/101.07 thf(h1,assumption,(![X1:$i]:(![X2:$i]:(((subset @ X1) @ X2) => (((subset @ X2) @ X1) => (X1 = X2))))),introduced(assumption,[])).
% 101.09/101.07 thf(h2,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))) => ((subset @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ ((binunion @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2)))))))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h3,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))) => ((subset @ X2) @ X3))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h4,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ ((binunion @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h5,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ ((binunion @ X2) @ X3))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h6,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2)))))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h7,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h8,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h9,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h10,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2)))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h11,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h12,assumption,(~((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h13,assumption,(~((![X1:$i]:(((breln1 @ eigen__0) @ X1) => (![X2:$i]:(((breln1 @ eigen__0) @ X2) => (((binunion @ X1) @ X2) = ((binunion @ X2) @ X1)))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h14,assumption,(~((((breln1 @ eigen__0) @ eigen__1) => (![X1:$i]:(((breln1 @ eigen__0) @ X1) => (((binunion @ eigen__1) @ X1) = ((binunion @ X1) @ eigen__1))))))),introduced(assumption,[])).
% 101.09/101.07 thf(h15,assumption,((breln1 @ eigen__0) @ eigen__1),introduced(assumption,[])).
% 101.09/101.07 thf(h16,assumption,(~((![X1:$i]:(((breln1 @ eigen__0) @ X1) => (((binunion @ eigen__1) @ X1) = ((binunion @ X1) @ eigen__1)))))),introduced(assumption,[])).
% 101.09/101.07 thf(h17,assumption,(~((((breln1 @ eigen__0) @ eigen__2) => (((binunion @ eigen__1) @ eigen__2) = ((binunion @ eigen__2) @ eigen__1))))),introduced(assumption,[])).
% 101.09/101.07 thf(h18,assumption,((breln1 @ eigen__0) @ eigen__2),introduced(assumption,[])).
% 101.09/101.07 thf(h19,assumption,(~((((binunion @ eigen__1) @ eigen__2) = ((binunion @ eigen__2) @ eigen__1)))),introduced(assumption,[])).
% 101.09/101.07 thf(ax921, axiom, (~(p7)|p47), file('<stdin>', ax921)).
% 101.09/101.07 thf(ax919, axiom, (~(p47)|p49), file('<stdin>', ax919)).
% 101.09/101.07 thf(ax961, axiom, p7, file('<stdin>', ax961)).
% 101.09/101.07 thf(ax922, axiom, (~(p47)|p46), file('<stdin>', ax922)).
% 101.09/101.07 thf(ax912, axiom, (~(p8)|p56), file('<stdin>', ax912)).
% 101.09/101.07 thf(ax920, axiom, (~(p49)|~(p2)|p48), file('<stdin>', ax920)).
% 101.09/101.07 thf(ax923, axiom, (~(p46)|~(p3)|p45), file('<stdin>', ax923)).
% 101.09/101.07 thf(ax701, axiom, (~(p56)|p266), file('<stdin>', ax701)).
% 101.09/101.07 thf(ax960, axiom, p8, file('<stdin>', ax960)).
% 101.09/101.07 thf(ax769, axiom, (~(p197)|~(p3)|p196), file('<stdin>', ax769)).
% 101.09/101.07 thf(ax768, axiom, (~(p48)|p197), file('<stdin>', ax768)).
% 101.09/101.07 thf(ax966, axiom, p2, file('<stdin>', ax966)).
% 101.09/101.07 thf(ax773, axiom, (~(p45)|p192), file('<stdin>', ax773)).
% 101.09/101.07 thf(ax965, axiom, p3, file('<stdin>', ax965)).
% 101.09/101.07 thf(ax930, axiom, (~(p6)|p38), file('<stdin>', ax930)).
% 101.09/101.07 thf(ax695, axiom, (~(p266)|~(p196)|p272), file('<stdin>', ax695)).
% 101.09/101.07 thf(ax774, axiom, (~(p192)|~(p2)|p191), file('<stdin>', ax774)).
% 101.09/101.07 thf(ax700, axiom, (~(p56)|p267), file('<stdin>', ax700)).
% 101.09/101.07 thf(ax931, axiom, (~(p38)|p37), file('<stdin>', ax931)).
% 101.09/101.07 thf(ax962, axiom, p6, file('<stdin>', ax962)).
% 101.09/101.07 thf(ax928, axiom, (~(p38)|p40), file('<stdin>', ax928)).
% 101.09/101.07 thf(ax948, axiom, (~(p4)|p20), file('<stdin>', ax948)).
% 101.09/101.07 thf(ax675, axiom, (~(p267)|~(p191)|p300), file('<stdin>', ax675)).
% 101.09/101.07 thf(ax932, axiom, (~(p37)|~(p3)|p36), file('<stdin>', ax932)).
% 101.09/101.07 thf(ax939, axiom, (~(p5)|p29), file('<stdin>', ax939)).
% 101.09/101.07 thf(ax929, axiom, (~(p40)|~(p2)|p39), file('<stdin>', ax929)).
% 101.09/101.07 thf(ax946, axiom, (~(p20)|p22), file('<stdin>', ax946)).
% 101.09/101.07 thf(ax964, axiom, p4, file('<stdin>', ax964)).
% 101.09/101.07 thf(pax9, axiom, (p9=>![X1:$i, X2:$i]:(fsubset @ X1 @ X2=>(fsubset @ X2 @ X1=>(X1)=(X2)))), file('<stdin>', pax9)).
% 101.09/101.07 thf(nax1, axiom, (p1<=(fbinunion @ f__1 @ f__2)=(fbinunion @ f__2 @ f__1)), file('<stdin>', nax1)).
% 101.09/101.07 thf(ax967, axiom, ~(p1), file('<stdin>', ax967)).
% 101.09/101.07 thf(ax696, axiom, (~(p272)|p271), file('<stdin>', ax696)).
% 101.09/101.07 thf(pax191, axiom, (p191=>fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)), file('<stdin>', pax191)).
% 101.09/101.07 thf(ax949, axiom, (~(p20)|p19), file('<stdin>', ax949)).
% 101.09/101.07 thf(ax676, axiom, (~(p300)|p299), file('<stdin>', ax676)).
% 101.09/101.07 thf(pax196, axiom, (p196=>fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)), file('<stdin>', pax196)).
% 101.09/101.07 thf(ax809, axiom, (~(p36)|p157), file('<stdin>', ax809)).
% 101.09/101.07 thf(ax940, axiom, (~(p29)|p28), file('<stdin>', ax940)).
% 101.09/101.07 thf(ax963, axiom, p5, file('<stdin>', ax963)).
% 101.09/101.07 thf(ax804, axiom, (~(p39)|p162), file('<stdin>', ax804)).
% 101.09/101.07 thf(ax937, axiom, (~(p29)|p31), file('<stdin>', ax937)).
% 101.09/101.07 thf(ax947, axiom, (~(p22)|~(p2)|p21), file('<stdin>', ax947)).
% 101.09/101.07 thf(ax959, axiom, p9, file('<stdin>', ax959)).
% 101.09/101.07 thf(pax64, axiom, (p64=>fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)), file('<stdin>', pax64)).
% 101.09/101.07 thf(pax271, axiom, (p271=>(fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)=>(![X1:$i]:(fin @ X1 @ f__0=>![X2:$i]:(fin @ X2 @ f__0=>(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__2 @ f__1)=>fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__1 @ f__2))))=>fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)))), file('<stdin>', pax271)).
% 101.09/101.07 thf(ax950, axiom, (~(p19)|~(p3)|p18), file('<stdin>', ax950)).
% 101.09/101.07 thf(pax799, axiom, (p799=>(fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)=>(fbinunion @ f__2 @ f__1)=(fbinunion @ f__1 @ f__2))), file('<stdin>', pax799)).
% 101.09/101.07 thf(pax299, axiom, (p299=>(fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)=>(![X1:$i]:(fin @ X1 @ f__0=>![X2:$i]:(fin @ X2 @ f__0=>(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__1 @ f__2)=>fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__2 @ f__1))))=>fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)))), file('<stdin>', pax299)).
% 101.09/101.07 thf(ax810, axiom, (~(p157)|~(p2)|p156), file('<stdin>', ax810)).
% 101.09/101.07 thf(ax941, axiom, (~(p28)|~(p3)|p27), file('<stdin>', ax941)).
% 101.09/101.07 thf(ax805, axiom, (~(p162)|~(p3)|p161), file('<stdin>', ax805)).
% 101.09/101.07 thf(ax938, axiom, (~(p31)|~(p2)|p30), file('<stdin>', ax938)).
% 101.09/101.07 thf(pax21, axiom, (p21=>![X1:$i]:(fbreln1 @ f__0 @ X1=>![X2:$i]:(fin @ X2 @ f__0=>![X3:$i]:(fin @ X3 @ f__0=>(fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__2 @ X1)=>(~(fin @ (fkpair @ X2 @ X3) @ f__2)=>fin @ (fkpair @ X2 @ X3) @ X1)))))), file('<stdin>', pax21)).
% 101.09/101.07 thf(pax3, axiom, (p3=>fbreln1 @ f__0 @ f__1), file('<stdin>', pax3)).
% 101.09/101.07 thf(pax18, axiom, (p18=>![X1:$i]:(fbreln1 @ f__0 @ X1=>![X2:$i]:(fin @ X2 @ f__0=>![X3:$i]:(fin @ X3 @ f__0=>(fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__1 @ X1)=>(~(fin @ (fkpair @ X2 @ X3) @ f__1)=>fin @ (fkpair @ X2 @ X3) @ X1)))))), file('<stdin>', pax18)).
% 101.09/101.07 thf(pax2, axiom, (p2=>fbreln1 @ f__0 @ f__2), file('<stdin>', pax2)).
% 101.09/101.07 thf(pax156, axiom, (p156=>![X1:$i]:(fin @ X1 @ f__0=>![X2:$i]:(fin @ X2 @ f__0=>(fin @ (fkpair @ X1 @ X2) @ f__1=>fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__1 @ f__2))))), file('<stdin>', pax156)).
% 101.09/101.07 thf(pax27, axiom, (p27=>![X1:$i]:(fbreln1 @ f__0 @ X1=>![X2:$i]:(fin @ X2 @ f__0=>![X3:$i]:(fin @ X3 @ f__0=>(fin @ (fkpair @ X2 @ X3) @ X1=>fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__1 @ X1)))))), file('<stdin>', pax27)).
% 101.09/101.07 thf(pax161, axiom, (p161=>![X1:$i]:(fin @ X1 @ f__0=>![X2:$i]:(fin @ X2 @ f__0=>(fin @ (fkpair @ X1 @ X2) @ f__2=>fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__2 @ f__1))))), file('<stdin>', pax161)).
% 101.09/101.07 thf(pax30, axiom, (p30=>![X1:$i]:(fbreln1 @ f__0 @ X1=>![X2:$i]:(fin @ X2 @ f__0=>![X3:$i]:(fin @ X3 @ f__0=>(fin @ (fkpair @ X2 @ X3) @ X1=>fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__2 @ X1)))))), file('<stdin>', pax30)).
% 101.09/101.07 thf(nax64, axiom, (p64<=fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)), file('<stdin>', nax64)).
% 101.09/101.07 thf(nax799, axiom, (p799<=(fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)=>(fbinunion @ f__2 @ f__1)=(fbinunion @ f__1 @ f__2))), file('<stdin>', nax799)).
% 101.09/101.07 thf(c_0_62, plain, (~p7|p47), inference(fof_simplification,[status(thm)],[ax921])).
% 101.09/101.07 thf(c_0_63, plain, (~p47|p49), inference(fof_simplification,[status(thm)],[ax919])).
% 101.09/101.07 thf(c_0_64, plain, (p47|~p7), inference(split_conjunct,[status(thm)],[c_0_62])).
% 101.09/101.07 thf(c_0_65, plain, p7, inference(split_conjunct,[status(thm)],[ax961])).
% 101.09/101.07 thf(c_0_66, plain, (~p47|p46), inference(fof_simplification,[status(thm)],[ax922])).
% 101.09/101.07 thf(c_0_67, plain, (~p8|p56), inference(fof_simplification,[status(thm)],[ax912])).
% 101.09/101.07 thf(c_0_68, plain, (~p49|~p2|p48), inference(fof_simplification,[status(thm)],[ax920])).
% 101.09/101.07 thf(c_0_69, plain, (p49|~p47), inference(split_conjunct,[status(thm)],[c_0_63])).
% 101.09/101.07 thf(c_0_70, plain, p47, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65])])).
% 101.09/101.07 thf(c_0_71, plain, (~p46|~p3|p45), inference(fof_simplification,[status(thm)],[ax923])).
% 101.09/101.07 thf(c_0_72, plain, (p46|~p47), inference(split_conjunct,[status(thm)],[c_0_66])).
% 101.09/101.07 thf(c_0_73, plain, (~p56|p266), inference(fof_simplification,[status(thm)],[ax701])).
% 101.09/101.07 thf(c_0_74, plain, (p56|~p8), inference(split_conjunct,[status(thm)],[c_0_67])).
% 101.09/101.07 thf(c_0_75, plain, p8, inference(split_conjunct,[status(thm)],[ax960])).
% 101.09/101.07 thf(c_0_76, plain, (~p197|~p3|p196), inference(fof_simplification,[status(thm)],[ax769])).
% 101.09/101.07 thf(c_0_77, plain, (~p48|p197), inference(fof_simplification,[status(thm)],[ax768])).
% 101.09/101.07 thf(c_0_78, plain, (p48|~p49|~p2), inference(split_conjunct,[status(thm)],[c_0_68])).
% 101.09/101.07 thf(c_0_79, plain, p2, inference(split_conjunct,[status(thm)],[ax966])).
% 101.09/101.07 thf(c_0_80, plain, p49, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70])])).
% 101.09/101.07 thf(c_0_81, plain, (~p45|p192), inference(fof_simplification,[status(thm)],[ax773])).
% 101.09/101.07 thf(c_0_82, plain, (p45|~p46|~p3), inference(split_conjunct,[status(thm)],[c_0_71])).
% 101.09/101.07 thf(c_0_83, plain, p3, inference(split_conjunct,[status(thm)],[ax965])).
% 101.09/101.07 thf(c_0_84, plain, p46, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_70])])).
% 101.09/101.07 thf(c_0_85, plain, (~p6|p38), inference(fof_simplification,[status(thm)],[ax930])).
% 101.09/101.07 thf(c_0_86, plain, (~p266|~p196|p272), inference(fof_simplification,[status(thm)],[ax695])).
% 101.09/101.07 thf(c_0_87, plain, (p266|~p56), inference(split_conjunct,[status(thm)],[c_0_73])).
% 101.09/101.07 thf(c_0_88, plain, p56, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_74, c_0_75])])).
% 101.09/101.07 thf(c_0_89, plain, (p196|~p197|~p3), inference(split_conjunct,[status(thm)],[c_0_76])).
% 101.09/101.07 thf(c_0_90, plain, (p197|~p48), inference(split_conjunct,[status(thm)],[c_0_77])).
% 101.09/101.07 thf(c_0_91, plain, p48, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_79]), c_0_80])])).
% 101.09/101.07 thf(c_0_92, plain, (~p192|~p2|p191), inference(fof_simplification,[status(thm)],[ax774])).
% 101.09/101.07 thf(c_0_93, plain, (p192|~p45), inference(split_conjunct,[status(thm)],[c_0_81])).
% 101.09/101.07 thf(c_0_94, plain, p45, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83]), c_0_84])])).
% 101.09/101.07 thf(c_0_95, plain, (~p56|p267), inference(fof_simplification,[status(thm)],[ax700])).
% 101.09/101.07 thf(c_0_96, plain, (~p38|p37), inference(fof_simplification,[status(thm)],[ax931])).
% 101.09/101.07 thf(c_0_97, plain, (p38|~p6), inference(split_conjunct,[status(thm)],[c_0_85])).
% 101.09/101.07 thf(c_0_98, plain, p6, inference(split_conjunct,[status(thm)],[ax962])).
% 101.09/101.07 thf(c_0_99, plain, (~p38|p40), inference(fof_simplification,[status(thm)],[ax928])).
% 101.09/101.07 thf(c_0_100, plain, (~p4|p20), inference(fof_simplification,[status(thm)],[ax948])).
% 101.09/101.07 thf(c_0_101, plain, (p272|~p266|~p196), inference(split_conjunct,[status(thm)],[c_0_86])).
% 101.09/101.07 thf(c_0_102, plain, p266, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_87, c_0_88])])).
% 101.09/101.07 thf(c_0_103, plain, (p196|~p197), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_89, c_0_83])])).
% 101.09/101.07 thf(c_0_104, plain, p197, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_90, c_0_91])])).
% 101.09/101.07 thf(c_0_105, plain, (~p267|~p191|p300), inference(fof_simplification,[status(thm)],[ax675])).
% 101.09/101.07 thf(c_0_106, plain, (p191|~p192|~p2), inference(split_conjunct,[status(thm)],[c_0_92])).
% 101.09/101.07 thf(c_0_107, plain, p192, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_93, c_0_94])])).
% 101.09/101.07 thf(c_0_108, plain, (p267|~p56), inference(split_conjunct,[status(thm)],[c_0_95])).
% 101.09/101.07 thf(c_0_109, plain, (~p37|~p3|p36), inference(fof_simplification,[status(thm)],[ax932])).
% 101.09/101.07 thf(c_0_110, plain, (p37|~p38), inference(split_conjunct,[status(thm)],[c_0_96])).
% 101.09/101.07 thf(c_0_111, plain, p38, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_97, c_0_98])])).
% 101.09/101.07 thf(c_0_112, plain, (~p5|p29), inference(fof_simplification,[status(thm)],[ax939])).
% 101.09/101.07 thf(c_0_113, plain, (~p40|~p2|p39), inference(fof_simplification,[status(thm)],[ax929])).
% 101.09/101.07 thf(c_0_114, plain, (p40|~p38), inference(split_conjunct,[status(thm)],[c_0_99])).
% 101.09/101.07 thf(c_0_115, plain, (~p20|p22), inference(fof_simplification,[status(thm)],[ax946])).
% 101.09/101.07 thf(c_0_116, plain, (p20|~p4), inference(split_conjunct,[status(thm)],[c_0_100])).
% 101.09/101.07 thf(c_0_117, plain, p4, inference(split_conjunct,[status(thm)],[ax964])).
% 101.09/101.07 thf(c_0_118, plain, ![X2862:$i, X2863:$i]:(~p9|(~fsubset @ X2862 @ X2863|(~fsubset @ X2863 @ X2862|(X2862)=(X2863)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax9])])])).
% 101.09/101.07 thf(c_0_119, plain, ((fbinunion @ f__1 @ f__2)!=(fbinunion @ f__2 @ f__1)|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 101.09/101.07 thf(c_0_120, plain, ~p1, inference(fof_simplification,[status(thm)],[ax967])).
% 101.09/101.07 thf(c_0_121, plain, (~p272|p271), inference(fof_simplification,[status(thm)],[ax696])).
% 101.09/101.07 thf(c_0_122, plain, (p272|~p196), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_101, c_0_102])])).
% 101.09/101.07 thf(c_0_123, plain, p196, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_103, c_0_104])])).
% 101.09/101.07 thf(c_0_124, plain, (~p191|fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)), inference(fof_nnf,[status(thm)],[pax191])).
% 101.09/101.07 thf(c_0_125, plain, (~p20|p19), inference(fof_simplification,[status(thm)],[ax949])).
% 101.09/101.07 thf(c_0_126, plain, (~p300|p299), inference(fof_simplification,[status(thm)],[ax676])).
% 101.09/101.07 thf(c_0_127, plain, (p300|~p267|~p191), inference(split_conjunct,[status(thm)],[c_0_105])).
% 101.09/101.07 thf(c_0_128, plain, p191, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_106, c_0_79]), c_0_107])])).
% 101.09/101.07 thf(c_0_129, plain, p267, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_108, c_0_88])])).
% 101.09/101.07 thf(c_0_130, plain, (~p196|fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)), inference(fof_nnf,[status(thm)],[pax196])).
% 101.09/101.07 thf(c_0_131, plain, (~p36|p157), inference(fof_simplification,[status(thm)],[ax809])).
% 101.09/101.07 thf(c_0_132, plain, (p36|~p37|~p3), inference(split_conjunct,[status(thm)],[c_0_109])).
% 101.09/101.07 thf(c_0_133, plain, p37, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_110, c_0_111])])).
% 101.09/101.07 thf(c_0_134, plain, (~p29|p28), inference(fof_simplification,[status(thm)],[ax940])).
% 101.09/101.07 thf(c_0_135, plain, (p29|~p5), inference(split_conjunct,[status(thm)],[c_0_112])).
% 101.09/101.07 thf(c_0_136, plain, p5, inference(split_conjunct,[status(thm)],[ax963])).
% 101.09/101.07 thf(c_0_137, plain, (~p39|p162), inference(fof_simplification,[status(thm)],[ax804])).
% 101.09/101.07 thf(c_0_138, plain, (p39|~p40|~p2), inference(split_conjunct,[status(thm)],[c_0_113])).
% 101.09/101.07 thf(c_0_139, plain, p40, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_114, c_0_111])])).
% 101.09/101.07 thf(c_0_140, plain, (~p29|p31), inference(fof_simplification,[status(thm)],[ax937])).
% 101.09/101.07 thf(c_0_141, plain, (~p22|~p2|p21), inference(fof_simplification,[status(thm)],[ax947])).
% 101.09/101.07 thf(c_0_142, plain, (p22|~p20), inference(split_conjunct,[status(thm)],[c_0_115])).
% 101.09/101.07 thf(c_0_143, plain, p20, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_116, c_0_117])])).
% 101.09/101.07 thf(c_0_144, plain, ![X2:$i, X1:$i]:((X1)=(X2)|~p9|~fsubset @ X1 @ X2|~fsubset @ X2 @ X1), inference(split_conjunct,[status(thm)],[c_0_118])).
% 101.09/101.07 thf(c_0_145, plain, p9, inference(split_conjunct,[status(thm)],[ax959])).
% 101.09/101.07 thf(c_0_146, plain, (~p64|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)), inference(fof_nnf,[status(thm)],[pax64])).
% 101.09/101.07 thf(c_0_147, plain, (p1|(fbinunion @ f__1 @ f__2)!=(fbinunion @ f__2 @ f__1)), inference(split_conjunct,[status(thm)],[c_0_119])).
% 101.09/101.07 thf(c_0_148, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_120])).
% 101.09/101.07 thf(c_0_149, plain, ((fin @ esk871_0 @ f__0|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271)&((fin @ esk872_0 @ f__0|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271)&((fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__2 @ f__1)|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271)&(~fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__1 @ f__2)|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax271])])])])).
% 101.09/101.07 thf(c_0_150, plain, (p271|~p272), inference(split_conjunct,[status(thm)],[c_0_121])).
% 101.09/101.07 thf(c_0_151, plain, p272, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_122, c_0_123])])).
% 101.09/101.07 thf(c_0_152, plain, (fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p191), inference(split_conjunct,[status(thm)],[c_0_124])).
% 101.09/101.07 thf(c_0_153, plain, (~p19|~p3|p18), inference(fof_simplification,[status(thm)],[ax950])).
% 101.09/101.07 thf(c_0_154, plain, (p19|~p20), inference(split_conjunct,[status(thm)],[c_0_125])).
% 101.09/101.07 thf(c_0_155, plain, (~p799|(~fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|(fbinunion @ f__2 @ f__1)=(fbinunion @ f__1 @ f__2))), inference(fof_nnf,[status(thm)],[pax799])).
% 101.09/101.07 thf(c_0_156, plain, ((fin @ esk826_0 @ f__0|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299)&((fin @ esk827_0 @ f__0|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299)&((fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__1 @ f__2)|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299)&(~fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__2 @ f__1)|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax299])])])])).
% 101.09/101.07 thf(c_0_157, plain, (p299|~p300), inference(split_conjunct,[status(thm)],[c_0_126])).
% 101.09/101.07 thf(c_0_158, plain, p300, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_127, c_0_128]), c_0_129])])).
% 101.09/101.07 thf(c_0_159, plain, (fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p196), inference(split_conjunct,[status(thm)],[c_0_130])).
% 101.09/101.07 thf(c_0_160, plain, (~p157|~p2|p156), inference(fof_simplification,[status(thm)],[ax810])).
% 101.09/101.07 thf(c_0_161, plain, (p157|~p36), inference(split_conjunct,[status(thm)],[c_0_131])).
% 101.09/101.07 thf(c_0_162, plain, p36, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_132, c_0_83]), c_0_133])])).
% 101.09/101.07 thf(c_0_163, plain, (~p28|~p3|p27), inference(fof_simplification,[status(thm)],[ax941])).
% 101.09/101.07 thf(c_0_164, plain, (p28|~p29), inference(split_conjunct,[status(thm)],[c_0_134])).
% 101.09/101.07 thf(c_0_165, plain, p29, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_135, c_0_136])])).
% 101.09/101.07 thf(c_0_166, plain, (~p162|~p3|p161), inference(fof_simplification,[status(thm)],[ax805])).
% 101.09/101.07 thf(c_0_167, plain, (p162|~p39), inference(split_conjunct,[status(thm)],[c_0_137])).
% 101.09/101.07 thf(c_0_168, plain, p39, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_138, c_0_79]), c_0_139])])).
% 101.09/101.07 thf(c_0_169, plain, (~p31|~p2|p30), inference(fof_simplification,[status(thm)],[ax938])).
% 101.09/101.07 thf(c_0_170, plain, (p31|~p29), inference(split_conjunct,[status(thm)],[c_0_140])).
% 101.09/101.07 thf(c_0_171, plain, ![X2828:$i, X2829:$i, X2830:$i]:(~p21|(~fbreln1 @ f__0 @ X2828|(~fin @ X2829 @ f__0|(~fin @ X2830 @ f__0|(~fin @ (fkpair @ X2829 @ X2830) @ (fbinunion @ f__2 @ X2828)|(fin @ (fkpair @ X2829 @ X2830) @ f__2|fin @ (fkpair @ X2829 @ X2830) @ X2828)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax21])])])])).
% 101.09/101.07 thf(c_0_172, plain, (p21|~p22|~p2), inference(split_conjunct,[status(thm)],[c_0_141])).
% 101.09/101.07 thf(c_0_173, plain, p22, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_142, c_0_143])])).
% 101.09/101.07 thf(c_0_174, plain, ![X1:$i, X2:$i]:((X1)=(X2)|~fsubset @ X2 @ X1|~fsubset @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_144, c_0_145])])).
% 101.09/101.07 thf(c_0_175, plain, (fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~p64), inference(split_conjunct,[status(thm)],[c_0_146])).
% 101.09/101.07 thf(c_0_176, plain, (fbinunion @ f__2 @ f__1)!=(fbinunion @ f__1 @ f__2), inference(sr,[status(thm)],[c_0_147, c_0_148])).
% 101.09/101.07 thf(c_0_177, plain, (fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__2 @ f__1)|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271), inference(split_conjunct,[status(thm)],[c_0_149])).
% 101.09/101.07 thf(c_0_178, plain, p271, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_150, c_0_151])])).
% 101.09/101.07 thf(c_0_179, plain, fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_152, c_0_128])])).
% 101.09/101.07 thf(c_0_180, plain, (~p3|fbreln1 @ f__0 @ f__1), inference(fof_nnf,[status(thm)],[pax3])).
% 101.09/101.07 thf(c_0_181, plain, ![X2848:$i, X2849:$i, X2850:$i]:(~p18|(~fbreln1 @ f__0 @ X2848|(~fin @ X2849 @ f__0|(~fin @ X2850 @ f__0|(~fin @ (fkpair @ X2849 @ X2850) @ (fbinunion @ f__1 @ X2848)|(fin @ (fkpair @ X2849 @ X2850) @ f__1|fin @ (fkpair @ X2849 @ X2850) @ X2848)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax18])])])])).
% 101.09/101.07 thf(c_0_182, plain, (p18|~p19|~p3), inference(split_conjunct,[status(thm)],[c_0_153])).
% 101.09/101.07 thf(c_0_183, plain, p19, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_154, c_0_143])])).
% 101.09/101.07 thf(c_0_184, plain, ((fbinunion @ f__2 @ f__1)=(fbinunion @ f__1 @ f__2)|~p799|~fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)), inference(split_conjunct,[status(thm)],[c_0_155])).
% 101.09/101.07 thf(c_0_185, plain, (fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__1 @ f__2)|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299), inference(split_conjunct,[status(thm)],[c_0_156])).
% 101.09/101.07 thf(c_0_186, plain, p299, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_157, c_0_158])])).
% 101.09/101.07 thf(c_0_187, plain, fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_159, c_0_123])])).
% 101.09/101.07 thf(c_0_188, plain, (~p2|fbreln1 @ f__0 @ f__2), inference(fof_nnf,[status(thm)],[pax2])).
% 101.09/101.07 thf(c_0_189, plain, (fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271), inference(split_conjunct,[status(thm)],[c_0_149])).
% 101.09/101.07 thf(c_0_190, plain, ![X2164:$i, X2165:$i]:(~p156|(~fin @ X2164 @ f__0|(~fin @ X2165 @ f__0|(~fin @ (fkpair @ X2164 @ X2165) @ f__1|fin @ (fkpair @ X2164 @ X2165) @ (fbinunion @ f__1 @ f__2))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax156])])])).
% 101.09/101.07 thf(c_0_191, plain, (p156|~p157|~p2), inference(split_conjunct,[status(thm)],[c_0_160])).
% 101.09/101.07 thf(c_0_192, plain, p157, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_161, c_0_162])])).
% 101.09/101.07 thf(c_0_193, plain, (fin @ esk871_0 @ f__0|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271), inference(split_conjunct,[status(thm)],[c_0_149])).
% 101.09/101.07 thf(c_0_194, plain, (fin @ esk872_0 @ f__0|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fbreln1 @ f__0 @ (fbinunion @ f__1 @ f__2)|~p271), inference(split_conjunct,[status(thm)],[c_0_149])).
% 101.09/101.07 thf(c_0_195, plain, ![X2784:$i, X2785:$i, X2786:$i]:(~p27|(~fbreln1 @ f__0 @ X2784|(~fin @ X2785 @ f__0|(~fin @ X2786 @ f__0|(~fin @ (fkpair @ X2785 @ X2786) @ X2784|fin @ (fkpair @ X2785 @ X2786) @ (fbinunion @ f__1 @ X2784)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax27])])])).
% 101.09/101.07 thf(c_0_196, plain, (p27|~p28|~p3), inference(split_conjunct,[status(thm)],[c_0_163])).
% 101.09/101.07 thf(c_0_197, plain, p28, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_164, c_0_165])])).
% 101.09/101.07 thf(c_0_198, plain, (fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299), inference(split_conjunct,[status(thm)],[c_0_156])).
% 101.09/101.07 thf(c_0_199, plain, ![X2144:$i, X2145:$i]:(~p161|(~fin @ X2144 @ f__0|(~fin @ X2145 @ f__0|(~fin @ (fkpair @ X2144 @ X2145) @ f__2|fin @ (fkpair @ X2144 @ X2145) @ (fbinunion @ f__2 @ f__1))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax161])])])).
% 101.09/101.07 thf(c_0_200, plain, (p161|~p162|~p3), inference(split_conjunct,[status(thm)],[c_0_166])).
% 101.09/101.07 thf(c_0_201, plain, p162, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167, c_0_168])])).
% 101.09/101.07 thf(c_0_202, plain, (fin @ esk826_0 @ f__0|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299), inference(split_conjunct,[status(thm)],[c_0_156])).
% 101.09/101.07 thf(c_0_203, plain, (fin @ esk827_0 @ f__0|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fbreln1 @ f__0 @ (fbinunion @ f__2 @ f__1)|~p299), inference(split_conjunct,[status(thm)],[c_0_156])).
% 101.09/101.07 thf(c_0_204, plain, ![X2764:$i, X2765:$i, X2766:$i]:(~p30|(~fbreln1 @ f__0 @ X2764|(~fin @ X2765 @ f__0|(~fin @ X2766 @ f__0|(~fin @ (fkpair @ X2765 @ X2766) @ X2764|fin @ (fkpair @ X2765 @ X2766) @ (fbinunion @ f__2 @ X2764)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax30])])])).
% 101.09/101.07 thf(c_0_205, plain, (p30|~p31|~p2), inference(split_conjunct,[status(thm)],[c_0_169])).
% 101.09/101.07 thf(c_0_206, plain, p31, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_170, c_0_165])])).
% 101.09/101.07 thf(c_0_207, plain, ![X3:$i, X2:$i, X1:$i]:(fin @ (fkpair @ X2 @ X3) @ f__2|fin @ (fkpair @ X2 @ X3) @ X1|~p21|~fbreln1 @ f__0 @ X1|~fin @ X2 @ f__0|~fin @ X3 @ f__0|~fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__2 @ X1)), inference(split_conjunct,[status(thm)],[c_0_171])).
% 101.09/101.07 thf(c_0_208, plain, p21, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_172, c_0_79]), c_0_173])])).
% 101.09/101.07 thf(c_0_209, plain, (~fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~p64), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_174, c_0_175]), c_0_176])).
% 101.09/101.07 thf(c_0_210, plain, (fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__2 @ f__1)|fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_177, c_0_178]), c_0_179])])).
% 101.09/101.07 thf(c_0_211, plain, (fbreln1 @ f__0 @ f__1|~p3), inference(split_conjunct,[status(thm)],[c_0_180])).
% 101.09/101.07 thf(c_0_212, plain, ![X3:$i, X2:$i, X1:$i]:(fin @ (fkpair @ X2 @ X3) @ f__1|fin @ (fkpair @ X2 @ X3) @ X1|~p18|~fbreln1 @ f__0 @ X1|~fin @ X2 @ f__0|~fin @ X3 @ f__0|~fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__1 @ X1)), inference(split_conjunct,[status(thm)],[c_0_181])).
% 101.09/101.07 thf(c_0_213, plain, p18, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_182, c_0_83]), c_0_183])])).
% 101.09/101.07 thf(c_0_214, plain, (~fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~p799), inference(sr,[status(thm)],[c_0_184, c_0_176])).
% 101.09/101.07 thf(c_0_215, plain, (fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__1 @ f__2)|fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_185, c_0_186]), c_0_187])])).
% 101.09/101.07 thf(c_0_216, plain, (fbreln1 @ f__0 @ f__2|~p2), inference(split_conjunct,[status(thm)],[c_0_188])).
% 101.09/101.07 thf(c_0_217, plain, (~fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|p64), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax64])])).
% 101.09/101.07 thf(c_0_218, plain, (fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|~fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__1 @ f__2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_189, c_0_178]), c_0_179])])).
% 101.09/101.07 thf(c_0_219, plain, ![X1:$i, X2:$i]:(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__1 @ f__2)|~p156|~fin @ X1 @ f__0|~fin @ X2 @ f__0|~fin @ (fkpair @ X1 @ X2) @ f__1), inference(split_conjunct,[status(thm)],[c_0_190])).
% 101.09/101.07 thf(c_0_220, plain, p156, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_191, c_0_79]), c_0_192])])).
% 101.09/101.07 thf(c_0_221, plain, (fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|fin @ esk871_0 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_193, c_0_178]), c_0_179])])).
% 101.09/101.07 thf(c_0_222, plain, (fsubset @ (fbinunion @ f__2 @ f__1) @ (fbinunion @ f__1 @ f__2)|fin @ esk872_0 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_194, c_0_178]), c_0_179])])).
% 101.09/101.07 thf(c_0_223, plain, ![X3:$i, X2:$i, X1:$i]:(fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__1 @ X1)|~p27|~fbreln1 @ f__0 @ X1|~fin @ X2 @ f__0|~fin @ X3 @ f__0|~fin @ (fkpair @ X2 @ X3) @ X1), inference(split_conjunct,[status(thm)],[c_0_195])).
% 101.09/101.07 thf(c_0_224, plain, p27, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_196, c_0_83]), c_0_197])])).
% 101.09/101.07 thf(c_0_225, plain, (fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|~fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__2 @ f__1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_198, c_0_186]), c_0_187])])).
% 101.09/101.07 thf(c_0_226, plain, ![X1:$i, X2:$i]:(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__2 @ f__1)|~p161|~fin @ X1 @ f__0|~fin @ X2 @ f__0|~fin @ (fkpair @ X1 @ X2) @ f__2), inference(split_conjunct,[status(thm)],[c_0_199])).
% 101.09/101.07 thf(c_0_227, plain, p161, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_200, c_0_83]), c_0_201])])).
% 101.09/101.07 thf(c_0_228, plain, (fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|fin @ esk826_0 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_202, c_0_186]), c_0_187])])).
% 101.09/101.07 thf(c_0_229, plain, (fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|fin @ esk827_0 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_203, c_0_186]), c_0_187])])).
% 101.09/101.07 thf(c_0_230, plain, ![X3:$i, X2:$i, X1:$i]:(fin @ (fkpair @ X2 @ X3) @ (fbinunion @ f__2 @ X1)|~p30|~fbreln1 @ f__0 @ X1|~fin @ X2 @ f__0|~fin @ X3 @ f__0|~fin @ (fkpair @ X2 @ X3) @ X1), inference(split_conjunct,[status(thm)],[c_0_204])).
% 101.09/101.07 thf(c_0_231, plain, p30, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_205, c_0_79]), c_0_206])])).
% 101.09/101.07 thf(c_0_232, plain, ((fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|p799)&((fbinunion @ f__2 @ f__1)!=(fbinunion @ f__1 @ f__2)|p799)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax799])])])).
% 101.09/101.07 thf(c_0_233, plain, ![X1:$i, X2:$i, X3:$i]:(fin @ (fkpair @ X1 @ X2) @ f__2|fin @ (fkpair @ X1 @ X2) @ X3|~fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__2 @ X3)|~fin @ X2 @ f__0|~fin @ X1 @ f__0|~fbreln1 @ f__0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_207, c_0_208])])).
% 101.09/101.07 thf(c_0_234, plain, (fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__2 @ f__1)|~p64), inference(spm,[status(thm)],[c_0_209, c_0_210])).
% 101.09/101.07 thf(c_0_235, plain, fbreln1 @ f__0 @ f__1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_211, c_0_83])])).
% 101.09/101.07 thf(c_0_236, plain, ![X1:$i, X2:$i, X3:$i]:(fin @ (fkpair @ X1 @ X2) @ f__1|fin @ (fkpair @ X1 @ X2) @ X3|~fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__1 @ X3)|~fin @ X2 @ f__0|~fin @ X1 @ f__0|~fbreln1 @ f__0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_212, c_0_213])])).
% 101.09/101.07 thf(c_0_237, plain, (fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__1 @ f__2)|~p799), inference(spm,[status(thm)],[c_0_214, c_0_215])).
% 101.09/101.07 thf(c_0_238, plain, fbreln1 @ f__0 @ f__2, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_216, c_0_79])])).
% 101.09/101.07 thf(c_0_239, plain, (p64|~fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)), inference(split_conjunct,[status(thm)],[c_0_217])).
% 101.09/101.07 thf(c_0_240, plain, (~fin @ (fkpair @ esk871_0 @ esk872_0) @ (fbinunion @ f__1 @ f__2)|~p64), inference(spm,[status(thm)],[c_0_209, c_0_218])).
% 101.09/101.07 thf(c_0_241, plain, ![X2:$i, X1:$i]:(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__1 @ f__2)|~fin @ (fkpair @ X1 @ X2) @ f__1|~fin @ X2 @ f__0|~fin @ X1 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_219, c_0_220])])).
% 101.09/101.07 thf(c_0_242, plain, (fin @ esk871_0 @ f__0|~p64), inference(spm,[status(thm)],[c_0_209, c_0_221])).
% 101.09/101.07 thf(c_0_243, plain, (fin @ esk872_0 @ f__0|~p64), inference(spm,[status(thm)],[c_0_209, c_0_222])).
% 101.09/101.07 thf(c_0_244, plain, ![X1:$i, X2:$i, X3:$i]:(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__1 @ X3)|~fin @ (fkpair @ X1 @ X2) @ X3|~fin @ X2 @ f__0|~fin @ X1 @ f__0|~fbreln1 @ f__0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_223, c_0_224])])).
% 101.09/101.07 thf(c_0_245, plain, (~fin @ (fkpair @ esk826_0 @ esk827_0) @ (fbinunion @ f__2 @ f__1)|~p799), inference(spm,[status(thm)],[c_0_214, c_0_225])).
% 101.09/101.07 thf(c_0_246, plain, ![X2:$i, X1:$i]:(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__2 @ f__1)|~fin @ (fkpair @ X1 @ X2) @ f__2|~fin @ X2 @ f__0|~fin @ X1 @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_226, c_0_227])])).
% 101.09/101.07 thf(c_0_247, plain, (fin @ esk826_0 @ f__0|~p799), inference(spm,[status(thm)],[c_0_214, c_0_228])).
% 101.09/101.07 thf(c_0_248, plain, (fin @ esk827_0 @ f__0|~p799), inference(spm,[status(thm)],[c_0_214, c_0_229])).
% 101.09/101.07 thf(c_0_249, plain, ![X1:$i, X2:$i, X3:$i]:(fin @ (fkpair @ X1 @ X2) @ (fbinunion @ f__2 @ X3)|~fin @ (fkpair @ X1 @ X2) @ X3|~fin @ X2 @ f__0|~fin @ X1 @ f__0|~fbreln1 @ f__0 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_230, c_0_231])])).
% 101.09/101.07 thf(c_0_250, plain, (fsubset @ (fbinunion @ f__1 @ f__2) @ (fbinunion @ f__2 @ f__1)|p799), inference(split_conjunct,[status(thm)],[c_0_232])).
% 101.09/101.07 thf(c_0_251, plain, (fin @ (fkpair @ esk871_0 @ esk872_0) @ f__2|fin @ (fkpair @ esk871_0 @ esk872_0) @ f__1|~fin @ esk872_0 @ f__0|~fin @ esk871_0 @ f__0|~p64), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_233, c_0_234]), c_0_235])])).
% 101.09/101.07 thf(c_0_252, plain, (fin @ (fkpair @ esk826_0 @ esk827_0) @ f__1|fin @ (fkpair @ esk826_0 @ esk827_0) @ f__2|~fin @ esk827_0 @ f__0|~fin @ esk826_0 @ f__0|~p799), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_236, c_0_237]), c_0_238])])).
% 101.09/101.07 thf(c_0_253, plain, (fin @ esk827_0 @ f__0|p64), inference(spm,[status(thm)],[c_0_239, c_0_229])).
% 101.09/101.07 thf(c_0_254, plain, (fin @ esk826_0 @ f__0|p64), inference(spm,[status(thm)],[c_0_239, c_0_228])).
% 101.09/101.07 thf(c_0_255, plain, (~fin @ (fkpair @ esk871_0 @ esk872_0) @ f__1|~p64), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_240, c_0_241]), c_0_242]), c_0_243])).
% 101.09/101.07 thf(c_0_256, plain, (~fin @ (fkpair @ esk871_0 @ esk872_0) @ f__2|~p64), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_240, c_0_244]), c_0_238])]), c_0_242]), c_0_243])).
% 101.09/101.07 thf(c_0_257, plain, (~fin @ (fkpair @ esk826_0 @ esk827_0) @ f__2|~p799), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_245, c_0_246]), c_0_247]), c_0_248])).
% 101.09/101.07 thf(c_0_258, plain, (~fin @ (fkpair @ esk826_0 @ esk827_0) @ f__1|~p799), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_245, c_0_249]), c_0_235])]), c_0_247]), c_0_248])).
% 101.09/101.07 thf(c_0_259, plain, (p799|p64), inference(spm,[status(thm)],[c_0_239, c_0_250])).
% 101.09/101.07 thf(c_0_260, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_251, c_0_252, c_0_253, c_0_254, c_0_255, c_0_256, c_0_257, c_0_258, c_0_243, c_0_242, c_0_259]), ['proof']).
% 101.09/101.07 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h18,h19,h17,h15,h16,h14,h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0])],[])).
% 101.09/101.07 thf(2,plain,$false,inference(tab_negimp,[status(thm),assumptions([h17,h15,h16,h14,h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h18,h19])],[h17,1,h18,h19])).
% 101.09/101.07 thf(3,plain,$false,inference(tab_negall,[status(thm),assumptions([h15,h16,h14,h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h17]),tab_negall(eigenvar,eigen__2)],[h16,2,h17])).
% 101.09/101.07 thf(4,plain,$false,inference(tab_negimp,[status(thm),assumptions([h14,h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h15,h16])],[h14,3,h15,h16])).
% 101.09/101.07 thf(5,plain,$false,inference(tab_negall,[status(thm),assumptions([h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h14]),tab_negall(eigenvar,eigen__1)],[h13,4,h14])).
% 101.09/101.07 thf(6,plain,$false,inference(tab_negall,[status(thm),assumptions([h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h13]),tab_negall(eigenvar,eigen__0)],[h12,5,h13])).
% 101.09/101.07 thf(7,plain,$false,inference(tab_negimp,[status(thm),assumptions([h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h11,h12])],[h10,6,h11,h12])).
% 101.09/101.07 thf(8,plain,$false,inference(tab_negimp,[status(thm),assumptions([h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h9,h10])],[h8,7,h9,h10])).
% 101.09/101.07 thf(9,plain,$false,inference(tab_negimp,[status(thm),assumptions([h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h7,h8])],[h6,8,h7,h8])).
% 101.09/101.07 thf(10,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h4,h1,h2,h0]),tab_negimp(discharge,[h5,h6])],[h4,9,h5,h6])).
% 101.09/101.07 thf(11,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h2,h0]),tab_negimp(discharge,[h3,h4])],[h2,10,h3,h4])).
% 101.09/101.07 thf(12,plain,$false,inference(tab_negimp,[status(thm),assumptions([h0]),tab_negimp(discharge,[h1,h2])],[h0,11,h1,h2])).
% 101.09/101.07 thf(0,theorem,((![X1:$i]:(![X2:$i]:(((subset @ X1) @ X2) => (((subset @ X2) @ X1) => (X1 = X2))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))) => ((subset @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ ((binunion @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X2) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ X3) => ((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)))))))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X1) => (((in @ ((kpair @ X4) @ X5)) @ ((binunion @ X2) @ X3)) => ((~(((in @ ((kpair @ X4) @ X5)) @ X2))) => ((in @ ((kpair @ X4) @ X5)) @ X3)))))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[12,h0])).
% 101.09/101.07 % SZS output end Proof
%------------------------------------------------------------------------------