%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU939^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 : 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:53:00 PM UTC 2025
% Result : Theorem 23.85s 23.91s
% Output : Proof 23.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU939^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.33 % Computer : n017.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:38:08 EDT 2025
% 0.12/0.33 % CPUTime :
% 23.85/23.91 % SZS status Theorem
% 23.85/23.91 % Mode: mode371
% 23.85/23.91 % Inferences: 1577
% 23.85/23.91 % SZS output start Proof
% 23.85/23.91 thf(cTHM112B,conjecture,(![X1:$i>$o]:(~((![X2:($i>$i)>$i>$o]:(![X3:($i>$i)>$i>$o]:((![X4:$i]:((~(((X2 @ (^[X5:$i]:X5)) @ X4))) => ((X3 @ (^[X5:$i]:X5)) @ X4))) => (~((![X4:$i>$i]:(![X5:$i>$i]:((~(((![X6:$i]:((~(((X2 @ X4) @ X6))) => ((X3 @ X4) @ X6))) => (~((![X6:$i]:((~(((X2 @ X5) @ X6))) => ((X3 @ X5) @ X6)))))))) => (~(((![X6:$i]:((~(((X2 @ (^[X7:$i]:(X4 @ (X5 @ X7)))) @ X6))) => ((X3 @ (^[X7:$i]:(X4 @ (X5 @ X7)))) @ X6))) => (~((![X6:$i]:((X1 @ X6) => (X1 @ (X4 @ X6))))))))))))))))))))).
% 23.85/23.91 thf(h0,negated_conjecture,(~((![X1:$i>$o]:(~((![X2:($i>$i)>$i>$o]:(![X3:($i>$i)>$i>$o]:((![X4:$i]:((~(((X2 @ (^[X5:$i]:X5)) @ X4))) => ((X3 @ (^[X5:$i]:X5)) @ X4))) => (~((![X4:$i>$i]:(![X5:$i>$i]:((~(((![X6:$i]:((~(((X2 @ X4) @ X6))) => ((X3 @ X4) @ X6))) => (~((![X6:$i]:((~(((X2 @ X5) @ X6))) => ((X3 @ X5) @ X6)))))))) => (~(((![X6:$i]:((~(((X2 @ (^[X7:$i]:(X4 @ (X5 @ X7)))) @ X6))) => ((X3 @ (^[X7:$i]:(X4 @ (X5 @ X7)))) @ X6))) => (~((![X6:$i]:((X1 @ X6) => (X1 @ (X4 @ X6)))))))))))))))))))))),inference(assume_negation,[status(cth)],[cTHM112B])).
% 23.85/23.91 thf(ax131, axiom, ~(p1), file('<stdin>', ax131)).
% 23.85/23.91 thf(ax128, axiom, (~(p2)|p4), file('<stdin>', ax128)).
% 23.85/23.91 thf(ax130, axiom, (p1|p2), file('<stdin>', ax130)).
% 23.85/23.91 thf(pax132, axiom, (p132=>(![X7:$i]:(~((X7)=(X7))=>(X7)=(X7))=>~(![X8:$i > $i, X3:$i > $i]:(~((![X4:$i]:(~((X4)=(X8 @ X4))=>(X4)=(X8 @ X4))=>~(![X4:$i]:(~((X4)=(X3 @ X4))=>(X4)=(X3 @ X4)))))=>~((![X4:$i]:(~((X4)=(X8 @ (X3 @ X4)))=>(X4)=(X8 @ (X3 @ X4)))=>~(![X4:$i]:(f__0 @ X4=>f__0 @ (X8 @ X4))))))))), file('<stdin>', pax132)).
% 23.85/23.91 thf(ax0, axiom, (~(p4)|p132), file('<stdin>', ax0)).
% 23.85/23.91 thf(c_0_5, plain, ~p1, inference(fof_simplification,[status(thm)],[ax131])).
% 23.85/23.91 thf(c_0_6, plain, (~p2|p4), inference(fof_simplification,[status(thm)],[ax128])).
% 23.85/23.91 thf(c_0_7, plain, (p1|p2), inference(split_conjunct,[status(thm)],[ax130])).
% 23.85/23.91 thf(c_0_8, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_5])).
% 23.85/23.91 thf(c_0_9, plain, ![X60:$i, X61:$i]:(((((X60)=(esk9_0 @ X60)|(X60)=(esk9_0 @ X60)|(esk8_0)!=(esk8_0)|~p132)&((X61)=(esk10_0 @ X61)|(X61)=(esk10_0 @ X61)|(esk8_0)!=(esk8_0)|~p132))&(((f__0 @ esk12_0|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132)&(~f__0 @ (esk9_0 @ esk12_0)|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132))&((f__0 @ esk12_0|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132)&(~f__0 @ (esk9_0 @ esk12_0)|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132))))&((((X60)=(esk9_0 @ X60)|(X60)=(esk9_0 @ X60)|(esk8_0)!=(esk8_0)|~p132)&((X61)=(esk10_0 @ X61)|(X61)=(esk10_0 @ X61)|(esk8_0)!=(esk8_0)|~p132))&(((f__0 @ esk12_0|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132)&(~f__0 @ (esk9_0 @ esk12_0)|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132))&((f__0 @ esk12_0|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132)&(~f__0 @ (esk9_0 @ esk12_0)|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax132])])])])])])).
% 23.85/23.91 thf(c_0_10, plain, (~p4|p132), inference(fof_simplification,[status(thm)],[ax0])).
% 23.85/23.91 thf(c_0_11, plain, (p4|~p2), inference(split_conjunct,[status(thm)],[c_0_6])).
% 23.85/23.91 thf(c_0_12, plain, p2, inference(sr,[status(thm)],[c_0_7, c_0_8])).
% 23.85/23.91 thf(c_0_13, plain, ![X1:$i]:((X1)=(esk10_0 @ X1)|(X1)=(esk10_0 @ X1)|(esk8_0)!=(esk8_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.85/23.91 thf(c_0_14, plain, (p132|~p4), inference(split_conjunct,[status(thm)],[c_0_10])).
% 23.85/23.91 thf(c_0_15, plain, p4, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_12])])).
% 23.85/23.91 thf(c_0_16, plain, ![X1:$i]:((X1)=(esk9_0 @ X1)|(X1)=(esk9_0 @ X1)|(esk8_0)!=(esk8_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.85/23.91 thf(c_0_17, plain, (~f__0 @ (esk9_0 @ esk12_0)|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.85/23.91 thf(c_0_18, plain, ![X1:$i]:((X1)=(esk10_0 @ X1)|~p132), inference(cn,[status(thm)],[c_0_13])).
% 23.85/23.91 thf(c_0_19, plain, p132, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
% 23.85/23.91 thf(c_0_20, plain, ![X1:$i]:((X1)=(esk9_0 @ X1)|~p132), inference(cn,[status(thm)],[c_0_16])).
% 23.85/23.91 thf(c_0_21, plain, (f__0 @ esk12_0|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|(esk8_0)!=(esk8_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.85/23.91 thf(c_0_22, plain, ((esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|~p132|~f__0 @ (esk9_0 @ esk12_0)), inference(cn,[status(thm)],[c_0_17])).
% 23.85/23.91 thf(c_0_23, plain, ![X1:$i]:(esk10_0 @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 23.85/23.91 thf(c_0_24, plain, ![X1:$i]:(esk9_0 @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_19])])).
% 23.85/23.91 thf(c_0_25, plain, (f__0 @ esk12_0|(esk11_0)!=(esk9_0 @ (esk10_0 @ esk11_0))|~p132), inference(cn,[status(thm)],[c_0_21])).
% 23.85/23.91 thf(c_0_26, plain, ~f__0 @ esk12_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23]), c_0_24]), c_0_19]), c_0_24])])).
% 23.85/23.91 thf(c_0_27, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_23]), c_0_24]), c_0_19])]), c_0_26]), ['proof']).
% 23.85/23.91 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.85/23.91 thf(0,theorem,(![X1:$i>$o]:(~((![X2:($i>$i)>$i>$o]:(![X3:($i>$i)>$i>$o]:((![X4:$i]:((~(((X2 @ (^[X5:$i]:X5)) @ X4))) => ((X3 @ (^[X5:$i]:X5)) @ X4))) => (~((![X4:$i>$i]:(![X5:$i>$i]:((~(((![X6:$i]:((~(((X2 @ X4) @ X6))) => ((X3 @ X4) @ X6))) => (~((![X6:$i]:((~(((X2 @ X5) @ X6))) => ((X3 @ X5) @ X6)))))))) => (~(((![X6:$i]:((~(((X2 @ (^[X7:$i]:(X4 @ (X5 @ X7)))) @ X6))) => ((X3 @ (^[X7:$i]:(X4 @ (X5 @ X7)))) @ X6))) => (~((![X6:$i]:((X1 @ X6) => (X1 @ (X4 @ X6)))))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 23.85/23.91 % SZS output end Proof
%------------------------------------------------------------------------------