%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU940^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 : n007.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 24.36s 24.11s
% Output : Proof 24.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU940^5 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n007.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 : Wed Oct 8 21:11:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 24.36/24.11 % SZS status Theorem
% 24.36/24.11 % Mode: mode371
% 24.36/24.11 % Inferences: 17708
% 24.36/24.11 % SZS output start Proof
% 24.36/24.11 thf(cTHM112A_pme,conjecture,(![X1:$i>$o]:(~((![X2:($i>$i)>$o]:((X2 @ (^[X3:$i]:X3)) => (~((![X3:$i>$i]:(![X4:$i>$i]:((~(((X2 @ X3) => (~((X2 @ X4)))))) => (~(((X2 @ (^[X5:$i]:(X3 @ (X4 @ X5)))) => (~((![X5:$i]:((X1 @ X5) => (X1 @ (X3 @ X5)))))))))))))))))))).
% 24.36/24.11 thf(h0,negated_conjecture,(~((![X1:$i>$o]:(~((![X2:($i>$i)>$o]:((X2 @ (^[X3:$i]:X3)) => (~((![X3:$i>$i]:(![X4:$i>$i]:((~(((X2 @ X3) => (~((X2 @ X4)))))) => (~(((X2 @ (^[X5:$i]:(X3 @ (X4 @ X5)))) => (~((![X5:$i]:((X1 @ X5) => (X1 @ (X3 @ X5))))))))))))))))))))),inference(assume_negation,[status(cth)],[cTHM112A_pme])).
% 24.36/24.11 thf(ax208, axiom, ~(p1), file('<stdin>', ax208)).
% 24.36/24.11 thf(ax181, axiom, (~(p2)|p26), file('<stdin>', ax181)).
% 24.36/24.11 thf(ax207, axiom, (p1|p2), file('<stdin>', ax207)).
% 24.36/24.11 thf(ax143, axiom, (~(p26)|~(p61)|~(p62)), file('<stdin>', ax143)).
% 24.36/24.11 thf(ax140, axiom, (p62|~(p64)), file('<stdin>', ax140)).
% 24.36/24.11 thf(ax142, axiom, p61, file('<stdin>', ax142)).
% 24.36/24.11 thf(ax139, axiom, (p64|~(p65)), file('<stdin>', ax139)).
% 24.36/24.11 thf(ax138, axiom, (p65|~(p66)), file('<stdin>', ax138)).
% 24.36/24.11 thf(ax120, axiom, (~(p69)|p83), file('<stdin>', ax120)).
% 24.36/24.11 thf(ax135, axiom, (p66|p69), file('<stdin>', ax135)).
% 24.36/24.11 thf(pax83, axiom, (p83=>![X7:$i]:(f__6 @ X7)=(X7)), file('<stdin>', pax83)).
% 24.36/24.11 thf(ax126, axiom, (~(p68)|p78), file('<stdin>', ax126)).
% 24.36/24.11 thf(ax136, axiom, (p66|p68), file('<stdin>', ax136)).
% 24.36/24.11 thf(nax88, axiom, (p88<=![X7:$i]:(f__5 @ (f__6 @ X7))=(X7)), file('<stdin>', nax88)).
% 24.36/24.11 thf(pax78, axiom, (p78=>![X9:$i]:(f__5 @ X9)=(X9)), file('<stdin>', pax78)).
% 24.36/24.11 thf(ax134, axiom, (~(p67)|~(p70)|~(p71)), file('<stdin>', ax134)).
% 24.36/24.11 thf(ax137, axiom, (p65|p67), file('<stdin>', ax137)).
% 24.36/24.11 thf(ax114, axiom, (p70|~(p88)), file('<stdin>', ax114)).
% 24.36/24.11 thf(nax89, axiom, (p89<=(f__0 @ f__7=>f__0 @ (f__5 @ f__7))), file('<stdin>', nax89)).
% 24.36/24.11 thf(ax113, axiom, (p71|~(p89)), file('<stdin>', ax113)).
% 24.36/24.11 thf(c_0_20, plain, ~p1, inference(fof_simplification,[status(thm)],[ax208])).
% 24.36/24.11 thf(c_0_21, plain, (~p2|p26), inference(fof_simplification,[status(thm)],[ax181])).
% 24.36/24.11 thf(c_0_22, plain, (p1|p2), inference(split_conjunct,[status(thm)],[ax207])).
% 24.36/24.11 thf(c_0_23, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_20])).
% 24.36/24.11 thf(c_0_24, plain, (~p26|~p61|~p62), inference(fof_simplification,[status(thm)],[ax143])).
% 24.36/24.11 thf(c_0_25, plain, (p26|~p2), inference(split_conjunct,[status(thm)],[c_0_21])).
% 24.36/24.11 thf(c_0_26, plain, p2, inference(sr,[status(thm)],[c_0_22, c_0_23])).
% 24.36/24.11 thf(c_0_27, plain, (p62|~p64), inference(fof_simplification,[status(thm)],[ax140])).
% 24.36/24.11 thf(c_0_28, plain, (~p26|~p61|~p62), inference(split_conjunct,[status(thm)],[c_0_24])).
% 24.36/24.11 thf(c_0_29, plain, p26, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 24.36/24.11 thf(c_0_30, plain, p61, inference(split_conjunct,[status(thm)],[ax142])).
% 24.36/24.11 thf(c_0_31, plain, (p64|~p65), inference(fof_simplification,[status(thm)],[ax139])).
% 24.36/24.11 thf(c_0_32, plain, (p62|~p64), inference(split_conjunct,[status(thm)],[c_0_27])).
% 24.36/24.11 thf(c_0_33, plain, ~p62, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29]), c_0_30])])).
% 24.36/24.11 thf(c_0_34, plain, (p65|~p66), inference(fof_simplification,[status(thm)],[ax138])).
% 24.36/24.11 thf(c_0_35, plain, (p64|~p65), inference(split_conjunct,[status(thm)],[c_0_31])).
% 24.36/24.11 thf(c_0_36, plain, ~p64, inference(sr,[status(thm)],[c_0_32, c_0_33])).
% 24.36/24.11 thf(c_0_37, plain, (~p69|p83), inference(fof_simplification,[status(thm)],[ax120])).
% 24.36/24.11 thf(c_0_38, plain, (p65|~p66), inference(split_conjunct,[status(thm)],[c_0_34])).
% 24.36/24.11 thf(c_0_39, plain, (p66|p69), inference(split_conjunct,[status(thm)],[ax135])).
% 24.36/24.11 thf(c_0_40, plain, ~p65, inference(sr,[status(thm)],[c_0_35, c_0_36])).
% 24.36/24.11 thf(c_0_41, plain, ![X37:$i]:(~p83|(f__6 @ X37)=(X37)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax83])])])).
% 24.36/24.11 thf(c_0_42, plain, (p83|~p69), inference(split_conjunct,[status(thm)],[c_0_37])).
% 24.36/24.11 thf(c_0_43, plain, p69, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40])).
% 24.36/24.11 thf(c_0_44, plain, (~p68|p78), inference(fof_simplification,[status(thm)],[ax126])).
% 24.36/24.11 thf(c_0_45, plain, (p66|p68), inference(split_conjunct,[status(thm)],[ax136])).
% 24.36/24.11 thf(c_0_46, plain, ((f__5 @ (f__6 @ esk8_0))!=(esk8_0)|p88), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax88])])])])).
% 24.36/24.11 thf(c_0_47, plain, ![X1:$i]:((f__6 @ X1)=(X1)|~p83), inference(split_conjunct,[status(thm)],[c_0_41])).
% 24.36/24.11 thf(c_0_48, plain, p83, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 24.36/24.11 thf(c_0_49, plain, ![X41:$i]:(~p78|(f__5 @ X41)=(X41)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax78])])])).
% 24.36/24.11 thf(c_0_50, plain, (p78|~p68), inference(split_conjunct,[status(thm)],[c_0_44])).
% 24.36/24.11 thf(c_0_51, plain, p68, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_45]), c_0_40])).
% 24.36/24.11 thf(c_0_52, plain, (p88|(f__5 @ (f__6 @ esk8_0))!=(esk8_0)), inference(split_conjunct,[status(thm)],[c_0_46])).
% 24.36/24.11 thf(c_0_53, plain, ![X1:$i]:(f__6 @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_48])])).
% 24.36/24.11 thf(c_0_54, plain, ![X1:$i]:((f__5 @ X1)=(X1)|~p78), inference(split_conjunct,[status(thm)],[c_0_49])).
% 24.36/24.11 thf(c_0_55, plain, p78, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 24.36/24.11 thf(c_0_56, plain, (~p67|~p70|~p71), inference(fof_simplification,[status(thm)],[ax134])).
% 24.36/24.11 thf(c_0_57, plain, (p65|p67), inference(split_conjunct,[status(thm)],[ax137])).
% 24.36/24.11 thf(c_0_58, plain, (p70|~p88), inference(fof_simplification,[status(thm)],[ax114])).
% 24.36/24.11 thf(c_0_59, plain, (p88|(f__5 @ esk8_0)!=(esk8_0)), inference(rw,[status(thm)],[c_0_52, c_0_53])).
% 24.36/24.11 thf(c_0_60, plain, ![X1:$i]:(f__5 @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 24.36/24.11 thf(c_0_61, plain, ((f__0 @ f__7|p89)&(~f__0 @ (f__5 @ f__7)|p89)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax89])])])).
% 24.36/24.11 thf(c_0_62, plain, (~p67|~p70|~p71), inference(split_conjunct,[status(thm)],[c_0_56])).
% 24.36/24.11 thf(c_0_63, plain, p67, inference(sr,[status(thm)],[c_0_57, c_0_40])).
% 24.36/24.11 thf(c_0_64, plain, (p70|~p88), inference(split_conjunct,[status(thm)],[c_0_58])).
% 24.36/24.11 thf(c_0_65, plain, p88, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_60])])).
% 24.36/24.11 thf(c_0_66, plain, (p71|~p89), inference(fof_simplification,[status(thm)],[ax113])).
% 24.36/24.11 thf(c_0_67, plain, (p89|~f__0 @ (f__5 @ f__7)), inference(split_conjunct,[status(thm)],[c_0_61])).
% 24.36/24.11 thf(c_0_68, plain, (f__0 @ f__7|p89), inference(split_conjunct,[status(thm)],[c_0_61])).
% 24.36/24.11 thf(c_0_69, plain, (~p70|~p71), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_62, c_0_63])])).
% 24.36/24.11 thf(c_0_70, plain, p70, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65])])).
% 24.36/24.11 thf(c_0_71, plain, (p71|~p89), inference(split_conjunct,[status(thm)],[c_0_66])).
% 24.36/24.11 thf(c_0_72, plain, p89, inference(csr,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_60]), c_0_68])).
% 24.36/24.11 thf(c_0_73, plain, ~p71, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70])])).
% 24.36/24.11 thf(c_0_74, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_72])]), c_0_73]), ['proof']).
% 24.36/24.11 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 24.36/24.11 thf(0,theorem,(![X1:$i>$o]:(~((![X2:($i>$i)>$o]:((X2 @ (^[X3:$i]:X3)) => (~((![X3:$i>$i]:(![X4:$i>$i]:((~(((X2 @ X3) => (~((X2 @ X4)))))) => (~(((X2 @ (^[X5:$i]:(X3 @ (X4 @ X5)))) => (~((![X5:$i]:((X1 @ X5) => (X1 @ (X3 @ X5))))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 24.36/24.11 % SZS output end Proof
%------------------------------------------------------------------------------