%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU792^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 : n017.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:04 PM UTC 2025
% Result : Theorem 40.44s 39.26s
% Output : Proof 40.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : SEU792^2 : TPTP v9.2.0. Released v3.7.0.
% 0.07/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.36 % Computer : n017.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed Oct 8 21:19:53 EDT 2025
% 0.13/0.36 % CPUTime :
% 40.44/39.26 % SZS status Theorem
% 40.44/39.26 % Mode: mode484
% 40.44/39.26 % Inferences: 75
% 40.44/39.26 % SZS output start Proof
% 40.44/39.26 thf(ty_eigen__2, type, eigen__2 : $i).
% 40.44/39.26 thf(ty_breln1invset, type, breln1invset : ($i>$i>$i)).
% 40.44/39.26 thf(ty_eigen__1, type, eigen__1 : $i).
% 40.44/39.26 thf(ty_eigen__0, type, eigen__0 : $i).
% 40.44/39.26 thf(ty_breln1, type, breln1 : ($i>$i>$o)).
% 40.44/39.26 thf(ty_eigen__3, type, eigen__3 : $i).
% 40.44/39.26 thf(ty_breln1compset, type, breln1compset : ($i>$i>$i>$i)).
% 40.44/39.26 thf(ty_binunion, type, binunion : ($i>$i>$i)).
% 40.44/39.26 thf(def_breln1invprop,definition,(breln1invprop = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => ((breln1 @ X1) @ ((breln1invset @ X1) @ X2))))))).
% 40.44/39.26 thf(def_breln1compprop,definition,(breln1compprop = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ (((breln1compset @ X1) @ X2) @ X3))))))))).
% 40.44/39.26 thf(def_breln1unionCommutes,definition,(breln1unionCommutes = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))))).
% 40.44/39.26 thf(def_woz2Ex,definition,(woz2Ex = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))))).
% 40.44/39.26 thf(def_woz2W,definition,(woz2W = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))))).
% 40.44/39.26 thf(def_woz2A,definition,(woz2A = (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))))).
% 40.44/39.26 thf(woz2B,conjecture,((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => ((breln1 @ X1) @ ((breln1invset @ X1) @ X2))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ (((breln1compset @ X1) @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2))))))))))))))))))).
% 40.44/39.26 thf(h0,negated_conjecture,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => ((breln1 @ X1) @ ((breln1invset @ X1) @ X2))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ (((breln1compset @ X1) @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2)))))))))))))))))))),inference(assume_negation,[status(cth)],[woz2B])).
% 40.44/39.26 thf(h1,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => ((breln1 @ X1) @ ((breln1invset @ X1) @ X2))))),introduced(assumption,[])).
% 40.44/39.26 thf(h2,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ (((breln1compset @ X1) @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2))))))))))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h3,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ (((breln1compset @ X1) @ X2) @ X3))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h4,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2)))))))))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h5,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h6,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2))))))))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h7,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))),introduced(assumption,[])).
% 40.44/39.26 thf(h8,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2)))))))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h9,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h10,assumption,(~(((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2))))))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h11,assumption,(![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h12,assumption,(~((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2)))))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h13,assumption,(~((![X1:$i]:(((breln1 @ eigen__0) @ X1) => (![X2:$i]:(((breln1 @ eigen__0) @ X2) => (![X3:$i]:(((breln1 @ eigen__0) @ X3) => ((((breln1compset @ eigen__0) @ ((binunion @ X1) @ X2)) @ X3) = ((binunion @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X3)) @ ((breln1invset @ eigen__0) @ X2)))) @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X3)) @ ((breln1invset @ eigen__0) @ X1))))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h14,assumption,(~((((breln1 @ eigen__0) @ eigen__1) => (![X1:$i]:(((breln1 @ eigen__0) @ X1) => (![X2:$i]:(((breln1 @ eigen__0) @ X2) => ((((breln1compset @ eigen__0) @ ((binunion @ eigen__1) @ X1)) @ X2) = ((binunion @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X2)) @ ((breln1invset @ eigen__0) @ X1)))) @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X2)) @ ((breln1invset @ eigen__0) @ eigen__1)))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h15,assumption,((breln1 @ eigen__0) @ eigen__1),introduced(assumption,[])).
% 40.44/39.26 thf(h16,assumption,(~((![X1:$i]:(((breln1 @ eigen__0) @ X1) => (![X2:$i]:(((breln1 @ eigen__0) @ X2) => ((((breln1compset @ eigen__0) @ ((binunion @ eigen__1) @ X1)) @ X2) = ((binunion @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X2)) @ ((breln1invset @ eigen__0) @ X1)))) @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X2)) @ ((breln1invset @ eigen__0) @ eigen__1))))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h17,assumption,(~((((breln1 @ eigen__0) @ eigen__2) => (![X1:$i]:(((breln1 @ eigen__0) @ X1) => ((((breln1compset @ eigen__0) @ ((binunion @ eigen__1) @ eigen__2)) @ X1) = ((binunion @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X1)) @ ((breln1invset @ eigen__0) @ eigen__2)))) @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X1)) @ ((breln1invset @ eigen__0) @ eigen__1)))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h18,assumption,((breln1 @ eigen__0) @ eigen__2),introduced(assumption,[])).
% 40.44/39.26 thf(h19,assumption,(~((![X1:$i]:(((breln1 @ eigen__0) @ X1) => ((((breln1compset @ eigen__0) @ ((binunion @ eigen__1) @ eigen__2)) @ X1) = ((binunion @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X1)) @ ((breln1invset @ eigen__0) @ eigen__2)))) @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ X1)) @ ((breln1invset @ eigen__0) @ eigen__1))))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h20,assumption,(~((((breln1 @ eigen__0) @ eigen__3) => ((((breln1compset @ eigen__0) @ ((binunion @ eigen__1) @ eigen__2)) @ eigen__3) = ((binunion @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ eigen__3)) @ ((breln1invset @ eigen__0) @ eigen__2)))) @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ eigen__3)) @ ((breln1invset @ eigen__0) @ eigen__1)))))))),introduced(assumption,[])).
% 40.44/39.26 thf(h21,assumption,((breln1 @ eigen__0) @ eigen__3),introduced(assumption,[])).
% 40.44/39.26 thf(h22,assumption,(~(((((breln1compset @ eigen__0) @ ((binunion @ eigen__1) @ eigen__2)) @ eigen__3) = ((binunion @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ eigen__3)) @ ((breln1invset @ eigen__0) @ eigen__2)))) @ ((breln1invset @ eigen__0) @ (((breln1compset @ eigen__0) @ ((breln1invset @ eigen__0) @ eigen__3)) @ ((breln1invset @ eigen__0) @ eigen__1))))))),introduced(assumption,[])).
% 40.44/39.26 thf(nax1, axiom, (p1<=(fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3)=(fbinunion @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__2))) @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__1))))), file('<stdin>', nax1)).
% 40.44/39.26 thf(ax999, axiom, ~(p1), file('<stdin>', ax999)).
% 40.44/39.26 thf(pax6, axiom, (p6=>![X1:$i, X2:$i]:(fbreln1 @ X1 @ X2=>![X3:$i]:(fbreln1 @ X1 @ X3=>(fbreln1invset @ X1 @ (fbreln1compset @ X1 @ X2 @ X3))=(fbreln1compset @ X1 @ (fbreln1invset @ X1 @ X3) @ (fbreln1invset @ X1 @ X2))))), file('<stdin>', pax6)).
% 40.44/39.26 thf(pax2, axiom, (p2=>fbreln1 @ f__0 @ f__3), file('<stdin>', pax2)).
% 40.44/39.26 thf(pax3, axiom, (p3=>fbreln1 @ f__0 @ f__2), file('<stdin>', pax3)).
% 40.44/39.26 thf(pax7, axiom, (p7=>![X1:$i, X2:$i]:(fbreln1 @ X1 @ X2=>(X2)=(fbreln1invset @ X1 @ (fbreln1invset @ X1 @ X2)))), file('<stdin>', pax7)).
% 40.44/39.26 thf(pax9, axiom, (p9=>![X1:$i, X2:$i]:(fbreln1 @ X1 @ X2=>![X3:$i]:(fbreln1 @ X1 @ X3=>fbreln1 @ X1 @ (fbreln1compset @ X1 @ X2 @ X3)))), file('<stdin>', pax9)).
% 40.44/39.26 thf(ax994, axiom, p6, file('<stdin>', ax994)).
% 40.44/39.26 thf(ax998, axiom, p2, file('<stdin>', ax998)).
% 40.44/39.26 thf(ax997, axiom, p3, file('<stdin>', ax997)).
% 40.44/39.26 thf(ax993, axiom, p7, file('<stdin>', ax993)).
% 40.44/39.26 thf(ax991, axiom, p9, file('<stdin>', ax991)).
% 40.44/39.26 thf(ax931, axiom, (~(p8)|p68), file('<stdin>', ax931)).
% 40.44/39.26 thf(pax4, axiom, (p4=>fbreln1 @ f__0 @ f__1), file('<stdin>', pax4)).
% 40.44/39.26 thf(ax176, axiom, (~(p68)|p823), file('<stdin>', ax176)).
% 40.44/39.26 thf(ax992, axiom, p8, file('<stdin>', ax992)).
% 40.44/39.26 thf(ax996, axiom, p4, file('<stdin>', ax996)).
% 40.44/39.26 thf(pax823, axiom, (p823=>(fbreln1 @ f__0 @ f__1=>![X1:$i]:(fbreln1 @ f__0 @ X1=>(fbinunion @ f__1 @ X1)=(fbinunion @ X1 @ f__1)))), file('<stdin>', pax823)).
% 40.44/39.26 thf(pax5, axiom, (p5=>![X1:$i, X2:$i]:(fbreln1 @ X1 @ X2=>![X3:$i]:(fbreln1 @ X1 @ X3=>![X4:$i]:(fbreln1 @ X1 @ X4=>(fbreln1compset @ X1 @ (fbinunion @ X2 @ X3) @ X4)=(fbinunion @ (fbreln1compset @ X1 @ X2 @ X4) @ (fbreln1compset @ X1 @ X3 @ X4)))))), file('<stdin>', pax5)).
% 40.44/39.26 thf(ax995, axiom, p5, file('<stdin>', ax995)).
% 40.44/39.26 thf(c_0_20, plain, ((fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3)!=(fbinunion @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__2))) @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__1))))|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 40.44/39.26 thf(c_0_21, plain, ~p1, inference(fof_simplification,[status(thm)],[ax999])).
% 40.44/39.26 thf(c_0_22, plain, ![X2141:$i, X2142:$i, X2143:$i]:(~p6|(~fbreln1 @ X2141 @ X2142|(~fbreln1 @ X2141 @ X2143|(fbreln1invset @ X2141 @ (fbreln1compset @ X2141 @ X2142 @ X2143))=(fbreln1compset @ X2141 @ (fbreln1invset @ X2141 @ X2143) @ (fbreln1invset @ X2141 @ X2142))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 40.44/39.26 thf(c_0_23, plain, (~p2|fbreln1 @ f__0 @ f__3), inference(fof_nnf,[status(thm)],[pax2])).
% 40.44/39.26 thf(c_0_24, plain, (~p3|fbreln1 @ f__0 @ f__2), inference(fof_nnf,[status(thm)],[pax3])).
% 40.44/39.26 thf(c_0_25, plain, ![X2137:$i, X2138:$i]:(~p7|(~fbreln1 @ X2137 @ X2138|(X2138)=(fbreln1invset @ X2137 @ (fbreln1invset @ X2137 @ X2138)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 40.44/39.26 thf(c_0_26, plain, ![X2125:$i, X2126:$i, X2127:$i]:(~p9|(~fbreln1 @ X2125 @ X2126|(~fbreln1 @ X2125 @ X2127|fbreln1 @ X2125 @ (fbreln1compset @ X2125 @ X2126 @ X2127)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax9])])])).
% 40.44/39.26 thf(c_0_27, plain, (p1|(fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3)!=(fbinunion @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__2))) @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__1))))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 40.44/39.26 thf(c_0_28, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_21])).
% 40.44/39.26 thf(c_0_29, plain, ![X1:$i, X2:$i, X3:$i]:((fbreln1invset @ X1 @ (fbreln1compset @ X1 @ X2 @ X3))=(fbreln1compset @ X1 @ (fbreln1invset @ X1 @ X3) @ (fbreln1invset @ X1 @ X2))|~p6|~fbreln1 @ X1 @ X2|~fbreln1 @ X1 @ X3), inference(split_conjunct,[status(thm)],[c_0_22])).
% 40.44/39.26 thf(c_0_30, plain, p6, inference(split_conjunct,[status(thm)],[ax994])).
% 40.44/39.26 thf(c_0_31, plain, (fbreln1 @ f__0 @ f__3|~p2), inference(split_conjunct,[status(thm)],[c_0_23])).
% 40.44/39.26 thf(c_0_32, plain, p2, inference(split_conjunct,[status(thm)],[ax998])).
% 40.44/39.26 thf(c_0_33, plain, (fbreln1 @ f__0 @ f__2|~p3), inference(split_conjunct,[status(thm)],[c_0_24])).
% 40.44/39.26 thf(c_0_34, plain, p3, inference(split_conjunct,[status(thm)],[ax997])).
% 40.44/39.26 thf(c_0_35, plain, ![X1:$i, X2:$i]:((X2)=(fbreln1invset @ X1 @ (fbreln1invset @ X1 @ X2))|~p7|~fbreln1 @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_25])).
% 40.44/39.26 thf(c_0_36, plain, p7, inference(split_conjunct,[status(thm)],[ax993])).
% 40.44/39.26 thf(c_0_37, plain, ![X1:$i, X2:$i, X3:$i]:(fbreln1 @ X1 @ (fbreln1compset @ X1 @ X2 @ X3)|~p9|~fbreln1 @ X1 @ X2|~fbreln1 @ X1 @ X3), inference(split_conjunct,[status(thm)],[c_0_26])).
% 40.44/39.26 thf(c_0_38, plain, p9, inference(split_conjunct,[status(thm)],[ax991])).
% 40.44/39.26 thf(c_0_39, plain, (~p8|p68), inference(fof_simplification,[status(thm)],[ax931])).
% 40.44/39.26 thf(c_0_40, plain, (fbinunion @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__2))) @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__1))))!=(fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3), inference(sr,[status(thm)],[c_0_27, c_0_28])).
% 40.44/39.26 thf(c_0_41, plain, ![X1:$i, X2:$i, X3:$i]:((fbreln1compset @ X1 @ (fbreln1invset @ X1 @ X2) @ (fbreln1invset @ X1 @ X3))=(fbreln1invset @ X1 @ (fbreln1compset @ X1 @ X3 @ X2))|~fbreln1 @ X1 @ X2|~fbreln1 @ X1 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 40.44/39.26 thf(c_0_42, plain, fbreln1 @ f__0 @ f__3, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 40.44/39.26 thf(c_0_43, plain, fbreln1 @ f__0 @ f__2, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 40.44/39.26 thf(c_0_44, plain, ![X1:$i, X2:$i]:((fbreln1invset @ X1 @ (fbreln1invset @ X1 @ X2))=(X2)|~fbreln1 @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 40.44/39.26 thf(c_0_45, plain, ![X1:$i, X3:$i, X2:$i]:(fbreln1 @ X1 @ (fbreln1compset @ X1 @ X2 @ X3)|~fbreln1 @ X1 @ X3|~fbreln1 @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 40.44/39.26 thf(c_0_46, plain, (~p4|fbreln1 @ f__0 @ f__1), inference(fof_nnf,[status(thm)],[pax4])).
% 40.44/39.26 thf(c_0_47, plain, (~p68|p823), inference(fof_simplification,[status(thm)],[ax176])).
% 40.44/39.26 thf(c_0_48, plain, (p68|~p8), inference(split_conjunct,[status(thm)],[c_0_39])).
% 40.44/39.26 thf(c_0_49, plain, p8, inference(split_conjunct,[status(thm)],[ax992])).
% 40.44/39.26 thf(c_0_50, plain, (fbinunion @ (fbreln1invset @ f__0 @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ f__2 @ f__3))) @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__1))))!=(fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_42]), c_0_43])])).
% 40.44/39.26 thf(c_0_51, plain, ![X1:$i, X3:$i, X2:$i]:((fbreln1invset @ X1 @ (fbreln1invset @ X1 @ (fbreln1compset @ X1 @ X2 @ X3)))=(fbreln1compset @ X1 @ X2 @ X3)|~fbreln1 @ X1 @ X3|~fbreln1 @ X1 @ X2), inference(spm,[status(thm)],[c_0_44, c_0_45])).
% 40.44/39.26 thf(c_0_52, plain, (fbreln1 @ f__0 @ f__1|~p4), inference(split_conjunct,[status(thm)],[c_0_46])).
% 40.44/39.26 thf(c_0_53, plain, p4, inference(split_conjunct,[status(thm)],[ax996])).
% 40.44/39.26 thf(c_0_54, plain, ![X359:$i]:(~p823|(~fbreln1 @ f__0 @ f__1|(~fbreln1 @ f__0 @ X359|(fbinunion @ f__1 @ X359)=(fbinunion @ X359 @ f__1)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax823])])])).
% 40.44/39.26 thf(c_0_55, plain, (p823|~p68), inference(split_conjunct,[status(thm)],[c_0_47])).
% 40.44/39.26 thf(c_0_56, plain, p68, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])).
% 40.44/39.26 thf(c_0_57, plain, (fbinunion @ (fbreln1compset @ f__0 @ f__2 @ f__3) @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ (fbreln1invset @ f__0 @ f__3) @ (fbreln1invset @ f__0 @ f__1))))!=(fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_42]), c_0_43])])).
% 40.44/39.26 thf(c_0_58, plain, fbreln1 @ f__0 @ f__1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_53])])).
% 40.44/39.26 thf(c_0_59, plain, ![X2147:$i, X2148:$i, X2149:$i, X2150:$i]:(~p5|(~fbreln1 @ X2147 @ X2148|(~fbreln1 @ X2147 @ X2149|(~fbreln1 @ X2147 @ X2150|(fbreln1compset @ X2147 @ (fbinunion @ X2148 @ X2149) @ X2150)=(fbinunion @ (fbreln1compset @ X2147 @ X2148 @ X2150) @ (fbreln1compset @ X2147 @ X2149 @ X2150)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax5])])])).
% 40.44/39.26 thf(c_0_60, plain, ![X1:$i]:((fbinunion @ f__1 @ X1)=(fbinunion @ X1 @ f__1)|~p823|~fbreln1 @ f__0 @ f__1|~fbreln1 @ f__0 @ X1), inference(split_conjunct,[status(thm)],[c_0_54])).
% 40.44/39.26 thf(c_0_61, plain, p823, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56])])).
% 40.44/39.26 thf(c_0_62, plain, (fbinunion @ (fbreln1compset @ f__0 @ f__2 @ f__3) @ (fbreln1invset @ f__0 @ (fbreln1invset @ f__0 @ (fbreln1compset @ f__0 @ f__1 @ f__3))))!=(fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_41]), c_0_42]), c_0_58])])).
% 40.44/39.26 thf(c_0_63, plain, ![X1:$i, X3:$i, X2:$i, X4:$i]:((fbreln1compset @ X1 @ (fbinunion @ X2 @ X3) @ X4)=(fbinunion @ (fbreln1compset @ X1 @ X2 @ X4) @ (fbreln1compset @ X1 @ X3 @ X4))|~p5|~fbreln1 @ X1 @ X2|~fbreln1 @ X1 @ X3|~fbreln1 @ X1 @ X4), inference(split_conjunct,[status(thm)],[c_0_59])).
% 40.44/39.26 thf(c_0_64, plain, p5, inference(split_conjunct,[status(thm)],[ax995])).
% 40.44/39.26 thf(c_0_65, plain, ![X1:$i]:((fbinunion @ f__1 @ X1)=(fbinunion @ X1 @ f__1)|~fbreln1 @ f__0 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_61]), c_0_58])])).
% 40.44/39.26 thf(c_0_66, plain, (fbinunion @ (fbreln1compset @ f__0 @ f__2 @ f__3) @ (fbreln1compset @ f__0 @ f__1 @ f__3))!=(fbreln1compset @ f__0 @ (fbinunion @ f__1 @ f__2) @ f__3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_51]), c_0_42]), c_0_58])])).
% 40.44/39.26 thf(c_0_67, plain, ![X1:$i, X3:$i, X4:$i, X2:$i]:((fbinunion @ (fbreln1compset @ X1 @ X2 @ X3) @ (fbreln1compset @ X1 @ X4 @ X3))=(fbreln1compset @ X1 @ (fbinunion @ X2 @ X4) @ X3)|~fbreln1 @ X1 @ X3|~fbreln1 @ X1 @ X4|~fbreln1 @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 40.44/39.26 thf(c_0_68, plain, (fbinunion @ f__2 @ f__1)=(fbinunion @ f__1 @ f__2), inference(spm,[status(thm)],[c_0_65, c_0_43])).
% 40.44/39.26 thf(c_0_69, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_67]), c_0_68]), c_0_42]), c_0_58]), c_0_43])]), ['proof']).
% 40.44/39.26 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h21,h22,h20,h18,h19,h17,h15,h16,h14,h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0])],[])).
% 40.44/39.26 thf(2,plain,$false,inference(tab_negimp,[status(thm),assumptions([h20,h18,h19,h17,h15,h16,h14,h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h21,h22])],[h20,1,h21,h22])).
% 40.44/39.26 thf(3,plain,$false,inference(tab_negall,[status(thm),assumptions([h18,h19,h17,h15,h16,h14,h13,h11,h12,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h20]),tab_negall(eigenvar,eigen__3)],[h19,2,h20])).
% 40.44/39.26 thf(4,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,3,h18,h19])).
% 40.44/39.26 thf(5,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,4,h17])).
% 40.44/39.26 thf(6,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,5,h15,h16])).
% 40.44/39.26 thf(7,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,6,h14])).
% 40.44/39.26 thf(8,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,7,h13])).
% 40.44/39.26 thf(9,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,8,h11,h12])).
% 40.44/39.26 thf(10,plain,$false,inference(tab_negimp,[status(thm),assumptions([h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h9,h10])],[h8,9,h9,h10])).
% 40.44/39.26 thf(11,plain,$false,inference(tab_negimp,[status(thm),assumptions([h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h7,h8])],[h6,10,h7,h8])).
% 40.44/39.26 thf(12,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h4,h1,h2,h0]),tab_negimp(discharge,[h5,h6])],[h4,11,h5,h6])).
% 40.44/39.26 thf(13,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h2,h0]),tab_negimp(discharge,[h3,h4])],[h2,12,h3,h4])).
% 40.44/39.26 thf(14,plain,$false,inference(tab_negimp,[status(thm),assumptions([h0]),tab_negimp(discharge,[h1,h2])],[h0,13,h1,h2])).
% 40.44/39.26 thf(0,theorem,((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => ((breln1 @ X1) @ ((breln1invset @ X1) @ X2))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => ((breln1 @ X1) @ (((breln1compset @ X1) @ X2) @ X3))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((binunion @ X2) @ X3) = ((binunion @ X3) @ X2))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (X2 = ((breln1invset @ X1) @ ((breln1invset @ X1) @ X2)))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (((breln1invset @ X1) @ (((breln1compset @ X1) @ X2) @ X3)) = (((breln1compset @ X1) @ ((breln1invset @ X1) @ X3)) @ ((breln1invset @ X1) @ X2)))))))) => ((![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ (((breln1compset @ X1) @ X2) @ X4)) @ (((breln1compset @ X1) @ X3) @ X4)))))))))) => (![X1:$i]:(![X2:$i]:(((breln1 @ X1) @ X2) => (![X3:$i]:(((breln1 @ X1) @ X3) => (![X4:$i]:(((breln1 @ X1) @ X4) => ((((breln1compset @ X1) @ ((binunion @ X2) @ X3)) @ X4) = ((binunion @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X3)))) @ ((breln1invset @ X1) @ (((breln1compset @ X1) @ ((breln1invset @ X1) @ X4)) @ ((breln1invset @ X1) @ X2)))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[14,h0])).
% 40.44/39.26 % SZS output end Proof
%------------------------------------------------------------------------------