%------------------------------------------------------------------------------
% File : Lash---1.13
% Problem : SYO042^2 : TPTP v9.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : lash -P picomus -M modes -p tstp -t %d %s
% Computer : n014.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 03:22:34 PM UTC 2025
% Result : Theorem 0.19s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYO042^2 : TPTP v9.2.0. Released v4.1.0.
% 0.03/0.13 % Command : lash -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n014.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Oct 9 01:36:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.19/0.38 % SZS status Theorem
% 0.19/0.38 % Mode: cade22grackle2xfee4
% 0.19/0.38 % Steps: 70
% 0.19/0.38 % SZS output start Proof
% 0.19/0.38 thf(ty_p, type, p : (($o>$o)>$o)).
% 0.19/0.38 thf(ty_x, type, x : $o).
% 0.19/0.38 thf(ty_g, type, g : ($o>$o)).
% 0.19/0.38 thf(ty_y, type, y : $o).
% 0.19/0.38 thf(sP1,plain,sP1 <=> y,introduced(definition,[new_symbols(definition,[sP1])])).
% 0.19/0.38 thf(sP2,plain,sP2 <=> x,introduced(definition,[new_symbols(definition,[sP2])])).
% 0.19/0.38 thf(4,conjecture,((~(((~(((~(((~((sP2 = sP1))) => (~(((g @ sP2) = sP1)))))) => (~(((g @ sP1) = sP2)))))) => (~((p @ g)))))) => (p @ (^[X1:$o]:(~(X1)))))).
% 0.19/0.38 thf(h0,negated_conjecture,(~(((~(((~(((~(((~((sP2 = sP1))) => (~(((g @ sP2) = sP1)))))) => (~(((g @ sP1) = sP2)))))) => (~((p @ g)))))) => (p @ (^[X1:$o]:(~(X1))))))),inference(assume_negation,[status(cth)],[4])).
% 0.19/0.38 thf(h1,assumption,(~(((~(((~(((~((sP2 = sP1))) => (~(((g @ sP2) = sP1)))))) => (~(((g @ sP1) = sP2)))))) => (~((p @ g)))))),introduced(assumption,[])).
% 0.19/0.38 thf(h2,assumption,(~((p @ (^[X1:$o]:(~(X1)))))),introduced(assumption,[])).
% 0.19/0.38 thf(h3,assumption,(~(((~(((~((sP2 = sP1))) => (~(((g @ sP2) = sP1)))))) => (~(((g @ sP1) = sP2)))))),introduced(assumption,[])).
% 0.19/0.38 thf(h4,assumption,(p @ g),introduced(assumption,[])).
% 0.19/0.38 thf(h5,assumption,(~(((~((sP2 = sP1))) => (~(((g @ sP2) = sP1)))))),introduced(assumption,[])).
% 0.19/0.38 thf(h6,assumption,((g @ sP1) = sP2),introduced(assumption,[])).
% 0.19/0.38 thf(h7,assumption,(~((sP2 = sP1))),introduced(assumption,[])).
% 0.19/0.38 thf(h8,assumption,((g @ sP2) = sP1),introduced(assumption,[])).
% 0.19/0.38 thf(h9,assumption,sP2,introduced(assumption,[])).
% 0.19/0.38 thf(h10,assumption,sP1,introduced(assumption,[])).
% 0.19/0.38 thf(h11,assumption,(~(sP2)),introduced(assumption,[])).
% 0.19/0.38 thf(h12,assumption,(~(sP1)),introduced(assumption,[])).
% 0.19/0.38 thf(h13,assumption,(g @ sP2),introduced(assumption,[])).
% 0.19/0.38 thf(h14,assumption,(~((g @ sP2))),introduced(assumption,[])).
% 0.19/0.38 thf(h15,assumption,(g @ sP1),introduced(assumption,[])).
% 0.19/0.38 thf(h16,assumption,(~((g @ sP1))),introduced(assumption,[])).
% 0.19/0.38 thf(1,plain,$false,inference(tab_conflict,[status(thm),assumptions([h15,h9,h13,h10,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0])],[h10,h10])).
% 0.19/0.38 thf(2,plain,$false,inference(tab_conflict,[status(thm),assumptions([h16,h11,h13,h10,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0])],[h10,h10])).
% 0.19/0.38 thf(3,plain,$false,inference(tab_bq,[status(thm),assumptions([h13,h10,h9,h10,h7,h8,h5,h6,h3,h4,h1,h2,h0]),tab_bq(discharge,[h15,h9]),tab_bq(discharge,[h16,h11])],[h6,1,2,h15,h9,h16,h11])).
% 0.19/0.38 3:288: Could not find hyp name
% 0.19/0.38 s = imp x False
% 0.19/0.38 hyp:
% 0.19/0.38 [290] h14: imp (g x) False
% 0.19/0.38 [287] h12: imp y False
% 0.19/0.38 [265] h9: x
% 0.19/0.38 [287] h10: imp y False
% 0.19/0.38 [278] h7: imp (eq:$o x y) False
% 0.19/0.38 [275] h8: eq:$o (g x) y
% 0.19/0.38 [280] h5: imp (imp (imp (eq:$o x y) False) (imp (eq:$o (g x) y) False)) False
% 0.19/0.38 [272] h6: eq:$o (g y) x
% 0.19/0.38 [282] h3: imp (imp (imp (imp (imp (eq:$o x y) False) (imp (eq:$o (g x) y) False)) False) (imp (eq:$o (g y) x) False)) False
% 0.19/0.38 [269] h4: p g
% 0.19/0.38 [284] h1: imp (imp (imp (imp (imp (imp (imp (eq:$o x y) False) (imp (eq:$o (g x) y) False)) False) (imp (eq:$o (g y) x) False)) False) (imp (p g) False)) False
% 0.19/0.38 [268] h2: imp (p (\_:$o.imp ^0 False)) False
% 0.19/0.38 [286] h0: imp (imp (imp (imp (imp (imp (imp (imp (imp (eq:$o x y) False) (imp (eq:$o (g x) y) False)) False) (imp (eq:$o (g y) x) False)) False) (imp (p g) False)) False) (p (\_:$o.imp ^0 False))) False
% 0.19/0.38 % SZS status Error
% 0.19/0.38 Exception: Failure("Could not find hyp name")
% 0.19/0.40 % SZS status Theorem
% 0.19/0.40 % Mode: cade22grackle2x798d
% 0.19/0.40 % Steps: 66
%------------------------------------------------------------------------------