%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SYO269^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 : 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:25:15 PM UTC 2025
% Result : Theorem 23.89s 23.94s
% Output : Proof 23.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYO269^5 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.12 % Command : satallax -E eprover-ho -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 00:37:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 23.89/23.94 % SZS status Theorem
% 23.89/23.94 % Mode: mode371
% 23.89/23.94 % Inferences: 1577
% 23.89/23.94 % SZS output start Proof
% 23.89/23.94 thf(cTHM112D,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 @ 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.89/23.94 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 @ 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)],[cTHM112D])).
% 23.89/23.94 thf(ax131, axiom, ~(p1), file('<stdin>', ax131)).
% 23.89/23.94 thf(ax128, axiom, (~(p2)|p4), file('<stdin>', ax128)).
% 23.89/23.94 thf(ax130, axiom, (p1|p2), file('<stdin>', ax130)).
% 23.89/23.94 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)=(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.89/23.94 thf(ax0, axiom, (~(p4)|p132), file('<stdin>', ax0)).
% 23.89/23.94 thf(c_0_5, plain, ~p1, inference(fof_simplification,[status(thm)],[ax131])).
% 23.89/23.94 thf(c_0_6, plain, (~p2|p4), inference(fof_simplification,[status(thm)],[ax128])).
% 23.89/23.94 thf(c_0_7, plain, (p1|p2), inference(split_conjunct,[status(thm)],[ax130])).
% 23.89/23.94 thf(c_0_8, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_5])).
% 23.89/23.94 thf(c_0_9, plain, ![X62:$i, X63:$i, X64:$i]:((((((X62)=(esk10_0 @ X62)|(X62)=(esk10_0 @ X62)|(esk9_0)!=(esk9_0)|~p132)&((X63)=(esk10_0 @ X63)|(X63)=(esk10_0 @ X63)|(esk9_0)!=(esk9_0)|~p132))&((X64)=(esk11_0 @ X64)|(X64)=(esk11_0 @ X64)|(esk9_0)!=(esk9_0)|~p132))&(((f__0 @ esk13_0|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132)&(~f__0 @ (esk10_0 @ esk13_0)|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132))&((f__0 @ esk13_0|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132)&(~f__0 @ (esk10_0 @ esk13_0)|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132))))&(((((X62)=(esk10_0 @ X62)|(X62)=(esk10_0 @ X62)|(esk9_0)!=(esk9_0)|~p132)&((X63)=(esk10_0 @ X63)|(X63)=(esk10_0 @ X63)|(esk9_0)!=(esk9_0)|~p132))&((X64)=(esk11_0 @ X64)|(X64)=(esk11_0 @ X64)|(esk9_0)!=(esk9_0)|~p132))&(((f__0 @ esk13_0|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132)&(~f__0 @ (esk10_0 @ esk13_0)|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132))&((f__0 @ esk13_0|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132)&(~f__0 @ (esk10_0 @ esk13_0)|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_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.89/23.94 thf(c_0_10, plain, (~p4|p132), inference(fof_simplification,[status(thm)],[ax0])).
% 23.89/23.94 thf(c_0_11, plain, (p4|~p2), inference(split_conjunct,[status(thm)],[c_0_6])).
% 23.89/23.94 thf(c_0_12, plain, p2, inference(sr,[status(thm)],[c_0_7, c_0_8])).
% 23.89/23.94 thf(c_0_13, plain, ![X1:$i]:((X1)=(esk11_0 @ X1)|(X1)=(esk11_0 @ X1)|(esk9_0)!=(esk9_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.89/23.94 thf(c_0_14, plain, (p132|~p4), inference(split_conjunct,[status(thm)],[c_0_10])).
% 23.89/23.94 thf(c_0_15, plain, p4, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_12])])).
% 23.89/23.94 thf(c_0_16, plain, ![X1:$i]:((X1)=(esk10_0 @ X1)|(X1)=(esk10_0 @ X1)|(esk9_0)!=(esk9_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.89/23.94 thf(c_0_17, plain, (~f__0 @ (esk10_0 @ esk13_0)|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.89/23.94 thf(c_0_18, plain, ![X1:$i]:((X1)=(esk11_0 @ X1)|~p132), inference(cn,[status(thm)],[c_0_13])).
% 23.89/23.94 thf(c_0_19, plain, p132, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
% 23.89/23.94 thf(c_0_20, plain, ![X1:$i]:((X1)=(esk10_0 @ X1)|~p132), inference(cn,[status(thm)],[c_0_16])).
% 23.89/23.94 thf(c_0_21, plain, (f__0 @ esk13_0|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|(esk9_0)!=(esk9_0)|~p132), inference(split_conjunct,[status(thm)],[c_0_9])).
% 23.89/23.94 thf(c_0_22, plain, ((esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|~p132|~f__0 @ (esk10_0 @ esk13_0)), inference(cn,[status(thm)],[c_0_17])).
% 23.89/23.94 thf(c_0_23, plain, ![X1:$i]:(esk11_0 @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 23.89/23.94 thf(c_0_24, plain, ![X1:$i]:(esk10_0 @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_19])])).
% 23.89/23.94 thf(c_0_25, plain, (f__0 @ esk13_0|(esk12_0)!=(esk10_0 @ (esk11_0 @ esk12_0))|~p132), inference(cn,[status(thm)],[c_0_21])).
% 23.89/23.94 thf(c_0_26, plain, ~f__0 @ esk13_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.89/23.94 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.89/23.94 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.89/23.94 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 @ 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.89/23.94 % SZS output end Proof
%------------------------------------------------------------------------------