%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP087^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 : n004.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:55 PM UTC 2025
% Result : Theorem 1.89s 2.13s
% Output : Proof 1.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : ITP087^1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n004.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 18:19:53 EDT 2025
% 0.12/0.33 % CPUTime :
% 1.89/2.13 % SZS status Theorem
% 1.89/2.13 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 1.89/2.13 % Inferences: 2
% 1.89/2.13 % SZS output start Proof
% 1.89/2.13 thf(conj_0,conjecture,(~(((member_Secrecy_KS @ m) @ (specKeysSecrets @ pq))))).
% 1.89/2.13 thf(h0,negated_conjecture,((member_Secrecy_KS @ m) @ (specKeysSecrets @ pq)),inference(assume_negation,[status(cth)],[conj_0])).
% 1.89/2.13 thf(pax8, axiom, (p8=>![X55:secrecy_specID, X56:secrecy_specID, X57:secrecy_specID, X58:secrecy_KS]:((fsubcomponents @ X55)=(finsert1671894227specID @ X56 @ (finsert1671894227specID @ X57 @ fbot_bo1785112429specID))=>(fcorrectCompositionKS @ X55=>(fmember_Secrecy_KS @ X58 @ (fspecKeysSecrets @ X55)=>(~(fmember_Secrecy_KS @ X58 @ (fspecKeysSecrets @ X56))=>fmember_Secrecy_KS @ X58 @ (fspecKeysSecrets @ X57)))))), file('<stdin>', pax8)).
% 1.89/2.13 thf(pax4, axiom, (p4=>(fsubcomponents @ fpq)=(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))), file('<stdin>', pax4)).
% 1.89/2.13 thf(pax1, axiom, (p1=>fcorrectCompositionKS @ fpq), file('<stdin>', pax1)).
% 1.89/2.13 thf(ax50, axiom, p8, file('<stdin>', ax50)).
% 1.89/2.13 thf(ax54, axiom, p4, file('<stdin>', ax54)).
% 1.89/2.13 thf(ax57, axiom, p1, file('<stdin>', ax57)).
% 1.89/2.13 thf(pax57, axiom, (p57=>fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fpq)), file('<stdin>', pax57)).
% 1.89/2.13 thf(ax1, axiom, p57, file('<stdin>', ax1)).
% 1.89/2.13 thf(nax3, axiom, (p3<=fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fp)), file('<stdin>', nax3)).
% 1.89/2.13 thf(ax55, axiom, ~(p3), file('<stdin>', ax55)).
% 1.89/2.13 thf(nax2, axiom, (p2<=fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fq)), file('<stdin>', nax2)).
% 1.89/2.13 thf(ax56, axiom, ~(p2), file('<stdin>', ax56)).
% 1.89/2.13 thf(c_0_12, plain, ![X371:secrecy_specID, X372:secrecy_specID, X373:secrecy_specID, X374:secrecy_KS]:(~p8|((fsubcomponents @ X371)!=(finsert1671894227specID @ X372 @ (finsert1671894227specID @ X373 @ fbot_bo1785112429specID))|(~fcorrectCompositionKS @ X371|(~fmember_Secrecy_KS @ X374 @ (fspecKeysSecrets @ X371)|(fmember_Secrecy_KS @ X374 @ (fspecKeysSecrets @ X372)|fmember_Secrecy_KS @ X374 @ (fspecKeysSecrets @ X373)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax8])])])])).
% 1.89/2.13 thf(c_0_13, plain, (~p4|(fsubcomponents @ fpq)=(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))), inference(fof_nnf,[status(thm)],[pax4])).
% 1.89/2.13 thf(c_0_14, plain, (~p1|fcorrectCompositionKS @ fpq), inference(fof_nnf,[status(thm)],[pax1])).
% 1.89/2.13 thf(c_0_15, plain, ![X6:secrecy_specID, X9:secrecy_KS, X2:secrecy_specID, X1:secrecy_specID]:(fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X2)|fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X6)|~p8|(fsubcomponents @ X1)!=(finsert1671894227specID @ X2 @ (finsert1671894227specID @ X6 @ fbot_bo1785112429specID))|~fcorrectCompositionKS @ X1|~fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X1)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.89/2.13 thf(c_0_16, plain, p8, inference(split_conjunct,[status(thm)],[ax50])).
% 1.89/2.13 thf(c_0_17, plain, ((fsubcomponents @ fpq)=(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))|~p4), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.89/2.13 thf(c_0_18, plain, p4, inference(split_conjunct,[status(thm)],[ax54])).
% 1.89/2.13 thf(c_0_19, plain, (fcorrectCompositionKS @ fpq|~p1), inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.89/2.13 thf(c_0_20, plain, p1, inference(split_conjunct,[status(thm)],[ax57])).
% 1.89/2.13 thf(c_0_21, plain, (~p57|fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fpq)), inference(fof_nnf,[status(thm)],[pax57])).
% 1.89/2.13 thf(c_0_22, plain, ![X1:secrecy_specID, X2:secrecy_specID, X9:secrecy_KS, X6:secrecy_specID]:(fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X1)|fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X2)|(fsubcomponents @ X6)!=(finsert1671894227specID @ X1 @ (finsert1671894227specID @ X2 @ fbot_bo1785112429specID))|~fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X6)|~fcorrectCompositionKS @ X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_15, c_0_16])])).
% 1.89/2.13 thf(c_0_23, plain, (fsubcomponents @ fpq)=(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 1.89/2.13 thf(c_0_24, plain, fcorrectCompositionKS @ fpq, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 1.89/2.13 thf(c_0_25, plain, (fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fpq)|~p57), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.89/2.13 thf(c_0_26, plain, p57, inference(split_conjunct,[status(thm)],[ax1])).
% 1.89/2.13 thf(c_0_27, plain, (~fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fp)|p3), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax3])])).
% 1.89/2.13 thf(c_0_28, plain, ~p3, inference(fof_simplification,[status(thm)],[ax55])).
% 1.89/2.13 thf(c_0_29, plain, (~fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fq)|p2), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])])).
% 1.89/2.13 thf(c_0_30, plain, ~p2, inference(fof_simplification,[status(thm)],[ax56])).
% 1.89/2.13 thf(c_0_31, plain, ![X1:secrecy_specID, X2:secrecy_specID, X9:secrecy_KS]:(fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X1)|fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ X2)|(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))!=(finsert1671894227specID @ X2 @ (finsert1671894227specID @ X1 @ fbot_bo1785112429specID))|~fmember_Secrecy_KS @ X9 @ (fspecKeysSecrets @ fpq)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_23]), c_0_24])])).
% 1.89/2.13 thf(c_0_32, plain, fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fpq), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 1.89/2.13 thf(c_0_33, plain, (p3|~fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fp)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 1.89/2.13 thf(c_0_34, plain, ~p3, inference(split_conjunct,[status(thm)],[c_0_28])).
% 1.89/2.13 thf(c_0_35, plain, (p2|~fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fq)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 1.89/2.13 thf(c_0_36, plain, ~p2, inference(split_conjunct,[status(thm)],[c_0_30])).
% 1.89/2.13 thf(c_0_37, plain, ![X1:secrecy_specID, X2:secrecy_specID]:(fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ X1)|fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ X2)|(finsert1671894227specID @ fp @ (finsert1671894227specID @ fq @ fbot_bo1785112429specID))!=(finsert1671894227specID @ X1 @ (finsert1671894227specID @ X2 @ fbot_bo1785112429specID))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 1.89/2.13 thf(c_0_38, plain, ~fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fp), inference(sr,[status(thm)],[c_0_33, c_0_34])).
% 1.89/2.13 thf(c_0_39, plain, ~fmember_Secrecy_KS @ fm @ (fspecKeysSecrets @ fq), inference(sr,[status(thm)],[c_0_35, c_0_36])).
% 1.89/2.13 thf(c_0_40, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_37]), c_0_38]), c_0_39]), ['proof']).
% 1.89/2.13 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 1.89/2.13 thf(0,theorem,(~(((member_Secrecy_KS @ m) @ (specKeysSecrets @ pq)))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 1.89/2.13 % SZS output end Proof
%------------------------------------------------------------------------------