%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP088^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n009.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 01:46:56 PM UTC 2025
% Result : Theorem 0.48s 0.68s
% Output : Proof 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ITP088^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.35 % Computer : n009.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 8 18:31:23 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.48/0.68 % SZS status Theorem
% 0.48/0.68 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 0.48/0.68 % Inferences: 6
% 0.48/0.68 % SZS output start Proof
% 0.48/0.68 thf(conj_0,conjecture,(~(((ine @ pq) @ (secrecy_kE @ key))))).
% 0.48/0.68 thf(h0,negated_conjecture,((ine @ pq) @ (secrecy_kE @ key)),inference(assume_negation,[status(cth)],[conj_0])).
% 0.48/0.68 thf(pax20, axiom, (p20=>![X53:secrecy_specID, X55:secrecy_Expression, X26:secrecy_specID, X56:secrecy_specID]:(fine @ X53 @ X55=>((fsubcomponents @ X53)=(finsert1671894227specID @ X26 @ (finsert1671894227specID @ X56 @ fbot_bo1785112429specID))=>(fcorrectCompositionIn @ X53=>(~(fine @ X26 @ X55)=>fine @ X56 @ X55))))), file('<stdin>', pax20)).
% 0.48/0.68 thf(pax4, axiom, (p4=>(fsubcomponents @ fpq)=(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))), file('<stdin>', pax4)).
% 0.48/0.68 thf(nax2, axiom, (p2<=fknowle945212990e_know @ fq @ (fsecrecy_kKS @ fkey)), file('<stdin>', nax2)).
% 0.48/0.68 thf(ax52, axiom, ~(p2), file('<stdin>', ax52)).
% 0.48/0.68 thf(pax6, axiom, (p6=>![X84:secrecy_specID, X85:secrecy_Keys]:(~(fknowle945212990e_know @ X84 @ (fsecrecy_kKS @ X85))=>~(fine @ X84 @ (fsecrecy_kE @ X85)))), file('<stdin>', pax6)).
% 0.48/0.68 thf(nax3, axiom, (p3<=fknowle945212990e_know @ fp @ (fsecrecy_kKS @ fkey)), file('<stdin>', nax3)).
% 0.48/0.68 thf(ax51, axiom, ~(p3), file('<stdin>', ax51)).
% 0.48/0.68 thf(ax34, axiom, p20, file('<stdin>', ax34)).
% 0.48/0.68 thf(ax50, axiom, p4, file('<stdin>', ax50)).
% 0.48/0.68 thf(pax46, axiom, (p46=>fine @ fpq @ (fsecrecy_kE @ fkey)), file('<stdin>', pax46)).
% 0.48/0.68 thf(pax1, axiom, (p1=>fcorrectCompositionIn @ fpq), file('<stdin>', pax1)).
% 0.48/0.68 thf(ax48, axiom, p6, file('<stdin>', ax48)).
% 0.48/0.68 thf(ax8, axiom, p46, file('<stdin>', ax8)).
% 0.48/0.68 thf(ax53, axiom, p1, file('<stdin>', ax53)).
% 0.48/0.68 thf(c_0_14, plain, ![X352:secrecy_specID, X353:secrecy_Expression, X354:secrecy_specID, X355:secrecy_specID]:(~p20|(~fine @ X352 @ X353|((fsubcomponents @ X352)!=(finsert1671894227specID @ X354 @ (finsert1671894227specID @ X355 @ fbot_bo1785112429specID))|(~fcorrectCompositionIn @ X352|(fine @ X354 @ X353|fine @ X355 @ X353))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax20])])])])).
% 0.48/0.68 thf(c_0_15, plain, (~p4|(fsubcomponents @ fpq)=(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))), inference(fof_nnf,[status(thm)],[pax4])).
% 0.48/0.68 thf(c_0_16, plain, (~fknowle945212990e_know @ fq @ (fsecrecy_kKS @ fkey)|p2), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])])).
% 0.48/0.68 thf(c_0_17, plain, ~p2, inference(fof_simplification,[status(thm)],[ax52])).
% 0.48/0.68 thf(c_0_18, plain, ![X424:secrecy_specID, X425:secrecy_Keys]:(~p6|(fknowle945212990e_know @ X424 @ (fsecrecy_kKS @ X425)|~fine @ X424 @ (fsecrecy_kE @ X425))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax6])])])])).
% 0.48/0.68 thf(c_0_19, plain, (~fknowle945212990e_know @ fp @ (fsecrecy_kKS @ fkey)|p3), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax3])])).
% 0.48/0.68 thf(c_0_20, plain, ~p3, inference(fof_simplification,[status(thm)],[ax51])).
% 0.48/0.68 thf(c_0_21, plain, ![X40:secrecy_Expression, X11:secrecy_specID, X2:secrecy_specID, X1:secrecy_specID]:(fine @ X2 @ X40|fine @ X11 @ X40|~p20|~fine @ X1 @ X40|(fsubcomponents @ X1)!=(finsert1671894227specID @ X2 @ (finsert1671894227specID @ X11 @ fbot_bo1785112429specID))|~fcorrectCompositionIn @ X1), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.48/0.68 thf(c_0_22, plain, p20, inference(split_conjunct,[status(thm)],[ax34])).
% 0.48/0.68 thf(c_0_23, plain, ((fsubcomponents @ fpq)=(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))|~p4), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.48/0.68 thf(c_0_24, plain, p4, inference(split_conjunct,[status(thm)],[ax50])).
% 0.48/0.68 thf(c_0_25, plain, (~p46|fine @ fpq @ (fsecrecy_kE @ fkey)), inference(fof_nnf,[status(thm)],[pax46])).
% 0.48/0.68 thf(c_0_26, plain, (~p1|fcorrectCompositionIn @ fpq), inference(fof_nnf,[status(thm)],[pax1])).
% 0.48/0.68 thf(c_0_27, plain, (p2|~fknowle945212990e_know @ fq @ (fsecrecy_kKS @ fkey)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.48/0.68 thf(c_0_28, plain, ~p2, inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.48/0.68 thf(c_0_29, plain, ![X1:secrecy_specID, X4:secrecy_Keys]:(fknowle945212990e_know @ X1 @ (fsecrecy_kKS @ X4)|~p6|~fine @ X1 @ (fsecrecy_kE @ X4)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.48/0.68 thf(c_0_30, plain, p6, inference(split_conjunct,[status(thm)],[ax48])).
% 0.48/0.68 thf(c_0_31, plain, (p3|~fknowle945212990e_know @ fp @ (fsecrecy_kKS @ fkey)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.48/0.68 thf(c_0_32, plain, ~p3, inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.48/0.68 thf(c_0_33, plain, ![X1:secrecy_specID, X2:secrecy_specID, X40:secrecy_Expression, X11:secrecy_specID]:(fine @ X1 @ X40|fine @ X2 @ X40|(fsubcomponents @ X11)!=(finsert1671894227specID @ X1 @ (finsert1671894227specID @ X2 @ fbot_bo1785112429specID))|~fine @ X11 @ X40|~fcorrectCompositionIn @ X11), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 0.48/0.68 thf(c_0_34, plain, (finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))=(fsubcomponents @ fpq), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 0.48/0.68 thf(c_0_35, plain, (fine @ fpq @ (fsecrecy_kE @ fkey)|~p46), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.48/0.68 thf(c_0_36, plain, p46, inference(split_conjunct,[status(thm)],[ax8])).
% 0.48/0.68 thf(c_0_37, plain, (fcorrectCompositionIn @ fpq|~p1), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.48/0.68 thf(c_0_38, plain, p1, inference(split_conjunct,[status(thm)],[ax53])).
% 0.48/0.68 thf(c_0_39, plain, ~fknowle945212990e_know @ fq @ (fsecrecy_kKS @ fkey), inference(sr,[status(thm)],[c_0_27, c_0_28])).
% 0.48/0.68 thf(c_0_40, plain, ![X1:secrecy_specID, X4:secrecy_Keys]:(fknowle945212990e_know @ X1 @ (fsecrecy_kKS @ X4)|~fine @ X1 @ (fsecrecy_kE @ X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 0.48/0.68 thf(c_0_41, plain, ~fknowle945212990e_know @ fp @ (fsecrecy_kKS @ fkey), inference(sr,[status(thm)],[c_0_31, c_0_32])).
% 0.48/0.68 thf(c_0_42, plain, ![X40:secrecy_Expression, X1:secrecy_specID]:(fine @ fq @ X40|fine @ fp @ X40|(fsubcomponents @ X1)!=(fsubcomponents @ fpq)|~fine @ X1 @ X40|~fcorrectCompositionIn @ X1), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.48/0.68 thf(c_0_43, plain, fine @ fpq @ (fsecrecy_kE @ fkey), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 0.48/0.68 thf(c_0_44, plain, fcorrectCompositionIn @ fpq, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 0.48/0.68 thf(c_0_45, plain, ~fine @ fq @ (fsecrecy_kE @ fkey), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 0.48/0.68 thf(c_0_46, plain, ~fine @ fp @ (fsecrecy_kE @ fkey), inference(spm,[status(thm)],[c_0_41, c_0_40])).
% 0.48/0.68 thf(c_0_47, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_44])]), c_0_45]), c_0_46]), ['proof']).
% 0.48/0.68 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 0.48/0.68 thf(0,theorem,(~(((ine @ pq) @ (secrecy_kE @ key)))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 0.48/0.68 % SZS output end Proof
%------------------------------------------------------------------------------