%------------------------------------------------------------------------------
% File : Lash---1.13
% Problem : SEU856^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : lash -P picomus -M modes -p tstp -t %d %s
% Computer : n031.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:42:02 PM UTC 2025
% Result : Theorem 0.12s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU856^5 : TPTP v9.2.0. Released v4.0.0.
% 0.11/0.12 % Command : lash -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n031.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Oct 8 20:45:38 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.40 % SZS status Theorem
% 0.12/0.40 % Mode: cade22grackle2xfee4
% 0.12/0.40 % Steps: 46
% 0.12/0.40 % SZS output start Proof
% 0.12/0.40 thf(ty_a, type, a : $tType).
% 0.12/0.40 thf(ty_eigen__0, type, eigen__0 : (a>$o)).
% 0.12/0.40 thf(ty_eigen__3, type, eigen__3 : a).
% 0.12/0.40 thf(ty_eigen__1, type, eigen__1 : (a>$o)).
% 0.12/0.40 thf(sP1,plain,sP1 <=> (eigen__1 @ eigen__3),introduced(definition,[new_symbols(definition,[sP1])])).
% 0.12/0.40 thf(sP2,plain,sP2 <=> ((^[X1:a]:(((eigen__1 @ X1) => (eigen__0 @ X1)) => (~(((eigen__0 @ X1) => (eigen__1 @ X1)))))) = (^[X1:a]:$false)),introduced(definition,[new_symbols(definition,[sP2])])).
% 0.12/0.40 thf(sP3,plain,sP3 <=> (eigen__0 @ eigen__3),introduced(definition,[new_symbols(definition,[sP3])])).
% 0.12/0.40 thf(sP4,plain,sP4 <=> (sP3 => sP1),introduced(definition,[new_symbols(definition,[sP4])])).
% 0.12/0.40 thf(sP5,plain,sP5 <=> (![X1:a]:(~((((eigen__1 @ X1) => (eigen__0 @ X1)) => (~(((eigen__0 @ X1) => (eigen__1 @ X1)))))))),introduced(definition,[new_symbols(definition,[sP5])])).
% 0.12/0.40 thf(sP6,plain,sP6 <=> (sP1 => sP3),introduced(definition,[new_symbols(definition,[sP6])])).
% 0.12/0.40 thf(sP7,plain,sP7 <=> (sP6 => (~(sP4))),introduced(definition,[new_symbols(definition,[sP7])])).
% 0.12/0.40 thf(cGAZING_THM46_pme,conjecture,(![X1:a>$o]:(![X2:a>$o]:((X1 = X2) = ((^[X3:a]:(((X2 @ X3) => (X1 @ X3)) => (~(((X1 @ X3) => (X2 @ X3)))))) = (^[X3:a]:$false)))))).
% 0.12/0.40 thf(h0,negated_conjecture,(~((![X1:a>$o]:(![X2:a>$o]:((X1 = X2) = ((^[X3:a]:(((X2 @ X3) => (X1 @ X3)) => (~(((X1 @ X3) => (X2 @ X3)))))) = (^[X3:a]:$false))))))),inference(assume_negation,[status(cth)],[cGAZING_THM46_pme])).
% 0.12/0.40 thf(h1,assumption,(~((![X1:a>$o]:((eigen__0 = X1) = ((^[X2:a]:(((X1 @ X2) => (eigen__0 @ X2)) => (~(((eigen__0 @ X2) => (X1 @ X2)))))) = (^[X2:a]:$false)))))),introduced(assumption,[])).
% 0.12/0.40 thf(h2,assumption,(~(((eigen__0 = eigen__1) = sP2))),introduced(assumption,[])).
% 0.12/0.40 thf(h3,assumption,(~((![X1:a]:((eigen__0 @ X1) = (eigen__1 @ X1))))),introduced(assumption,[])).
% 0.12/0.40 thf(h4,assumption,(~((sP3 = sP1))),introduced(assumption,[])).
% 0.12/0.40 thf(h5,assumption,sP3,introduced(assumption,[])).
% 0.12/0.40 thf(h6,assumption,sP1,introduced(assumption,[])).
% 0.12/0.40 thf(h7,assumption,(~(sP3)),introduced(assumption,[])).
% 0.12/0.40 thf(h8,assumption,(~(sP1)),introduced(assumption,[])).
% 0.12/0.40 thf(1,plain,((~(sP4) | ~(sP3)) | sP1),inference(prop_rule,[status(thm)],[])).
% 0.12/0.40 thf(2,plain,(sP7 | sP4),inference(prop_rule,[status(thm)],[])).
% 0.12/0.40 thf(3,plain,(~(sP5) | ~(sP7)),inference(all_rule,[status(thm)],[])).
% 0.12/0.40 thf(4,plain,(~(sP2) | sP5),inference(prop_rule,[status(thm)],[])).
% 0.12/0.40 1:300: Could not find hyp name
% 0.12/0.40 s = eq:a>$o (\_:a.imp (imp (__1 ^0) (__0 ^0)) (imp (imp (__0 ^0) (__1 ^0)) False)) (\_:a.False)
% 0.12/0.40 hyp:
% 0.12/0.40 [325] h5: __0 __3
% 0.12/0.40 [329] h6: imp (__1 __3) False
% 0.12/0.40 [328] h4: imp (eq:$o (__0 __3) (__1 __3)) False
% 0.12/0.40 [323] h3: imp (Pi:a (\_:a.eq:$o (__0 ^0) (__1 ^0))) False
% 0.12/0.40 [302] h2: imp (eq:$o (eq:a>$o __0 __1) (eq:a>$o (\_:a.imp (imp (__1 ^0) (__0 ^0)) (imp (imp (__0 ^0) (__1 ^0)) False)) (\_:a.False))) False
% 0.12/0.40 [291] h1: imp (Pi:a>$o (\_:a>$o.eq:$o (eq:a>$o __0 ^0) (eq:a>$o (\_:a.imp (imp (^1 ^0) (__0 ^0)) (imp (imp (__0 ^0) (^1 ^0)) False)) (\_:a.False)))) False
% 0.12/0.40 [279] h0: imp (Pi:a>$o (\_:a>$o.Pi:a>$o (\_:a>$o.eq:$o (eq:a>$o ^1 ^0) (eq:a>$o (\_:a.imp (imp (^1 ^0) (^2 ^0)) (imp (imp (^2 ^0) (^1 ^0)) False)) (\_:a.False))))) False
% 0.12/0.40 % SZS status Error
% 0.12/0.40 Exception: Failure("Could not find hyp name")
% 0.18/0.44 % SZS status Theorem
% 0.18/0.44 % Mode: cade22grackle2x798d
% 0.18/0.44 % Steps: 96
%------------------------------------------------------------------------------