%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEV196^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n027.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:56:27 PM UTC 2025
% Result : Theorem 23.73s 23.90s
% Output : Proof 23.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV196^5 : TPTP v9.2.0. Released v4.0.0.
% 0.12/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 19:10:53 EDT 2025
% 0.19/0.34 % CPUTime :
% 23.73/23.90 % SZS status Theorem
% 23.73/23.90 % Mode: mode371
% 23.73/23.90 % Inferences: 6
% 23.73/23.90 % SZS output start Proof
% 23.73/23.90 thf(cS_JOIN_LEM2_pme,conjecture,(![X1:a>a>a>$o]:((~(((~($false)) => (~((![X2:a]:(![X3:a]:(![X4:a]:(((~((((X2 = c0) => (~((X3 = X4)))) => (~(((X3 = c0) => (~((X2 = X4))))))))) => (~((![X5:a]:(![X6:a]:(![X7:a]:(![X8:a]:(![X9:a]:(![X10:a]:((~(((~(((~(((X2 = ((cP @ X5) @ X6)) => (~((X3 = ((cP @ X7) @ X8))))))) => (~((X4 = ((cP @ X9) @ X10))))))) => (~((((X1 @ X5) @ X7) @ X9)))))) => (~((((X1 @ X6) @ X8) @ X10))))))))))))) => (((X1 @ X2) @ X3) @ X4)))))))))) => (((X1 @ ((cP @ x) @ c0)) @ ((cP @ c0) @ y)) @ ((cP @ x) @ y))))).
% 23.73/23.90 thf(h0,negated_conjecture,(~((![X1:a>a>a>$o]:((~(((~($false)) => (~((![X2:a]:(![X3:a]:(![X4:a]:(((~((((X2 = c0) => (~((X3 = X4)))) => (~(((X3 = c0) => (~((X2 = X4))))))))) => (~((![X5:a]:(![X6:a]:(![X7:a]:(![X8:a]:(![X9:a]:(![X10:a]:((~(((~(((~(((X2 = ((cP @ X5) @ X6)) => (~((X3 = ((cP @ X7) @ X8))))))) => (~((X4 = ((cP @ X9) @ X10))))))) => (~((((X1 @ X5) @ X7) @ X9)))))) => (~((((X1 @ X6) @ X8) @ X10))))))))))))) => (((X1 @ X2) @ X3) @ X4)))))))))) => (((X1 @ ((cP @ x) @ c0)) @ ((cP @ c0) @ y)) @ ((cP @ x) @ y)))))),inference(assume_negation,[status(cth)],[cS_JOIN_LEM2_pme])).
% 23.73/23.90 thf(ax8, axiom, (p1|~(p2)), file('<stdin>', ax8)).
% 23.73/23.90 thf(ax9, axiom, ~(p1), file('<stdin>', ax9)).
% 23.73/23.90 thf(nax2, axiom, (p2<=(~((~(~$true)=>~(![X1:a, X2:a, X3:a]:((~((((X1)=(fc0)=>~((X2)=(X3)))=>~(((X2)=(fc0)=>~((X1)=(X3))))))=>~(![X4:a, X5:a, X6:a, X7:a, X8:a, X9:a]:(~((~((~(((X1)=(fcP @ X4 @ X5)=>~((X2)=(fcP @ X6 @ X7))))=>~((X3)=(fcP @ X8 @ X9))))=>~(f__0 @ X4 @ X6 @ X8)))=>~(f__0 @ X5 @ X7 @ X9))))=>f__0 @ X1 @ X2 @ X3))))=>f__0 @ (fcP @ fx @ fc0) @ (fcP @ fc0 @ fy) @ (fcP @ fx @ fy))), file('<stdin>', nax2)).
% 23.73/23.90 thf(c_0_3, plain, (p1|~p2), inference(fof_simplification,[status(thm)],[ax8])).
% 23.73/23.90 thf(c_0_4, plain, ~p1, inference(fof_simplification,[status(thm)],[ax9])).
% 23.73/23.90 thf(c_0_5, plain, ![X125:a, X126:a, X127:a, X128:a, X129:a, X130:a, X131:a, X132:a, X133:a]:(((((X125)!=(fc0)|(X126)!=(X127)|f__0 @ X125 @ X126 @ X127|p2)&((X126)!=(fc0)|(X125)!=(X127)|f__0 @ X125 @ X126 @ X127|p2))&((X125)!=(fcP @ X128 @ X129)|(X126)!=(fcP @ X130 @ X131)|(X127)!=(fcP @ X132 @ X133)|~f__0 @ X128 @ X130 @ X132|~f__0 @ X129 @ X131 @ X133|f__0 @ X125 @ X126 @ X127|p2))&(~f__0 @ (fcP @ fx @ fc0) @ (fcP @ fc0 @ fy) @ (fcP @ fx @ fy)|p2)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])])])])])).
% 23.73/23.90 thf(c_0_6, plain, (p1|~p2), inference(split_conjunct,[status(thm)],[c_0_3])).
% 23.73/23.90 thf(c_0_7, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_4])).
% 23.73/23.90 thf(c_0_8, plain, (p2|~f__0 @ (fcP @ fx @ fc0) @ (fcP @ fc0 @ fy) @ (fcP @ fx @ fy)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 23.73/23.90 thf(c_0_9, plain, ~p2, inference(sr,[status(thm)],[c_0_6, c_0_7])).
% 23.73/23.90 thf(c_0_10, plain, ![X1:a, X2:a, X4:a, X5:a, X3:a, X7:a, X6:a, X8:a, X9:a]:(f__0 @ X1 @ X4 @ X7|p2|(X1)!=(fcP @ X2 @ X3)|(X4)!=(fcP @ X5 @ X6)|(X7)!=(fcP @ X8 @ X9)|~f__0 @ X2 @ X5 @ X8|~f__0 @ X3 @ X6 @ X9), inference(split_conjunct,[status(thm)],[c_0_5])).
% 23.73/23.90 thf(c_0_11, plain, ![X1:a, X2:a, X3:a]:(f__0 @ X1 @ X2 @ X3|p2|(X1)!=(fc0)|(X2)!=(X3)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 23.73/23.90 thf(c_0_12, plain, ![X1:a, X2:a, X3:a]:(f__0 @ X2 @ X1 @ X3|p2|(X1)!=(fc0)|(X2)!=(X3)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 23.73/23.90 thf(c_0_13, plain, ~f__0 @ (fcP @ fx @ fc0) @ (fcP @ fc0 @ fy) @ (fcP @ fx @ fy), inference(sr,[status(thm)],[c_0_8, c_0_9])).
% 23.73/23.90 thf(c_0_14, plain, ![X2:a, X1:a, X4:a, X3:a, X6:a, X5:a]:(f__0 @ (fcP @ X1 @ X2) @ (fcP @ X3 @ X4) @ (fcP @ X5 @ X6)|~f__0 @ X2 @ X4 @ X6|~f__0 @ X1 @ X3 @ X5), inference(er,[status(thm)],[inference(er,[status(thm)],[inference(er,[status(thm)],[inference(sr,[status(thm)],[c_0_10, c_0_9])])])])).
% 23.73/23.90 thf(c_0_15, plain, ![X1:a]:f__0 @ fc0 @ X1 @ X1, inference(er,[status(thm)],[inference(er,[status(thm)],[inference(sr,[status(thm)],[c_0_11, c_0_9])])])).
% 23.73/23.90 thf(c_0_16, plain, ![X1:a]:f__0 @ X1 @ fc0 @ X1, inference(er,[status(thm)],[inference(er,[status(thm)],[inference(sr,[status(thm)],[c_0_12, c_0_9])])])).
% 23.73/23.90 thf(c_0_17, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13, c_0_14]), c_0_15]), c_0_16])]), ['proof']).
% 23.73/23.90 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.73/23.90 thf(0,theorem,(![X1:a>a>a>$o]:((~(((~($false)) => (~((![X2:a]:(![X3:a]:(![X4:a]:(((~((((X2 = c0) => (~((X3 = X4)))) => (~(((X3 = c0) => (~((X2 = X4))))))))) => (~((![X5:a]:(![X6:a]:(![X7:a]:(![X8:a]:(![X9:a]:(![X10:a]:((~(((~(((~(((X2 = ((cP @ X5) @ X6)) => (~((X3 = ((cP @ X7) @ X8))))))) => (~((X4 = ((cP @ X9) @ X10))))))) => (~((((X1 @ X5) @ X7) @ X9)))))) => (~((((X1 @ X6) @ X8) @ X10))))))))))))) => (((X1 @ X2) @ X3) @ X4)))))))))) => (((X1 @ ((cP @ x) @ c0)) @ ((cP @ c0) @ y)) @ ((cP @ x) @ y)))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 23.73/23.90 % SZS output end Proof
%------------------------------------------------------------------------------