%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWV763_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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 : Fri Oct 3 08:05:36 PM UTC 2025 % Result : Theorem 13.33s 13.58s % Output : Proof 13.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV763_5 : TPTP v9.2.0. Released v6.0.0. % 0.11/0.13 % Command : duper %s % 0.12/0.34 % Computer : n031.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 12:23:53 EDT 2025 % 0.12/0.35 % CPUTime : % 13.33/13.58 SZS status Theorem for theBenchmark.p % 13.33/13.58 SZS output start Proof for theBenchmark.p % 13.33/13.58 Clause #77 (by assumption #[]): Eq % 13.33/13.58 (∀ (Evsa : list event) (Ka : nat), % 13.33/13.58 Not (member msg (key Ka) (used Evsa)) → % 13.33/13.58 member nat Ka symKeys → % 13.33/13.58 member (list event) Evsa nS_Sha254967238shared → Not (member nat Ka (keysFor (parts (knows spy Evsa))))) % 13.33/13.58 True % 13.33/13.58 Clause #82 (by assumption #[]): Eq % 13.33/13.58 (∀ (H : fun msg bool) (Xa : msg) (Ka : nat), % 13.33/13.58 member msg (crypt Ka Xa) H → member nat Ka symKeys → member nat Ka (keysFor H)) % 13.33/13.58 True % 13.33/13.58 Clause #101 (by assumption #[]): Eq (member (list event) evs2 nS_Sha254967238shared) True % 13.33/13.58 Clause #102 (by assumption #[]): Eq (Not (member msg (key kab) (used evs2))) True % 13.33/13.58 Clause #103 (by assumption #[]): Eq (member nat kab symKeys) True % 13.33/13.58 Clause #107 (by assumption #[]): Eq % 13.33/13.58 (Not % 13.33/13.58 (Or % 13.33/13.58 (Or % 13.33/13.58 (Or (Or (Or (Or (Ne a aa) (Ne na (nonce nAa))) (Ne b ba)) (Ne k kab)) % 13.33/13.58 (Ne x (crypt (shrK ba) (mPair (key kab) (agent1 aa))))) % 13.33/13.58 (Not (member msg (crypt kab (nonce nb)) (parts (knows spy evs2))))) % 13.33/13.58 (Exists fun A => member event (says A ba (crypt (shrK ba) (mPair (key kab) (agent1 aa)))) (set event evs2)))) % 13.33/13.58 True % 13.33/13.58 Clause #141 (by clausification #[102]): Eq (member msg (key kab) (used evs2)) False % 13.33/13.58 Clause #315 (by clausification #[82]): ∀ (a : fun msg bool), % 13.33/13.58 Eq (∀ (Xa : msg) (Ka : nat), member msg (crypt Ka Xa) a → member nat Ka symKeys → member nat Ka (keysFor a)) True % 13.33/13.58 Clause #316 (by clausification #[315]): ∀ (a : msg) (a_1 : fun msg bool), % 13.33/13.58 Eq (∀ (Ka : nat), member msg (crypt Ka a) a_1 → member nat Ka symKeys → member nat Ka (keysFor a_1)) True % 13.33/13.58 Clause #317 (by clausification #[316]): ∀ (a : nat) (a_1 : msg) (a_2 : fun msg bool), % 13.33/13.58 Eq (member msg (crypt a a_1) a_2 → member nat a symKeys → member nat a (keysFor a_2)) True % 13.33/13.58 Clause #318 (by clausification #[317]): ∀ (a : nat) (a_1 : msg) (a_2 : fun msg bool), % 13.33/13.58 Or (Eq (member msg (crypt a a_1) a_2) False) (Eq (member nat a symKeys → member nat a (keysFor a_2)) True) % 13.33/13.58 Clause #319 (by clausification #[318]): ∀ (a : nat) (a_1 : msg) (a_2 : fun msg bool), % 13.33/13.58 Or (Eq (member msg (crypt a a_1) a_2) False) % 13.33/13.58 (Or (Eq (member nat a symKeys) False) (Eq (member nat a (keysFor a_2)) True)) % 13.33/13.58 Clause #636 (by clausification #[77]): ∀ (a : list event), % 13.33/13.58 Eq % 13.33/13.58 (∀ (Ka : nat), % 13.33/13.58 Not (member msg (key Ka) (used a)) → % 13.33/13.58 member nat Ka symKeys → % 13.33/13.58 member (list event) a nS_Sha254967238shared → Not (member nat Ka (keysFor (parts (knows spy a))))) % 13.33/13.58 True % 13.33/13.58 Clause #637 (by clausification #[636]): ∀ (a : nat) (a_1 : list event), % 13.33/13.58 Eq % 13.33/13.58 (Not (member msg (key a) (used a_1)) → % 13.33/13.58 member nat a symKeys → % 13.33/13.58 member (list event) a_1 nS_Sha254967238shared → Not (member nat a (keysFor (parts (knows spy a_1))))) % 13.33/13.58 True % 13.33/13.58 Clause #638 (by clausification #[637]): ∀ (a : nat) (a_1 : list event), % 13.33/13.58 Or (Eq (Not (member msg (key a) (used a_1))) False) % 13.33/13.58 (Eq % 13.33/13.58 (member nat a symKeys → % 13.33/13.58 member (list event) a_1 nS_Sha254967238shared → Not (member nat a (keysFor (parts (knows spy a_1))))) % 13.33/13.58 True) % 13.33/13.58 Clause #639 (by clausification #[638]): ∀ (a : nat) (a_1 : list event), % 13.33/13.58 Or % 13.33/13.58 (Eq % 13.33/13.58 (member nat a symKeys → % 13.33/13.58 member (list event) a_1 nS_Sha254967238shared → Not (member nat a (keysFor (parts (knows spy a_1))))) % 13.33/13.58 True) % 13.33/13.58 (Eq (member msg (key a) (used a_1)) True) % 13.33/13.58 Clause #640 (by clausification #[639]): ∀ (a : nat) (a_1 : list event), % 13.33/13.58 Or (Eq (member msg (key a) (used a_1)) True) % 13.33/13.58 (Or (Eq (member nat a symKeys) False) % 13.33/13.58 (Eq (member (list event) a_1 nS_Sha254967238shared → Not (member nat a (keysFor (parts (knows spy a_1))))) True)) % 13.33/13.58 Clause #641 (by clausification #[640]): ∀ (a : nat) (a_1 : list event), % 13.33/13.58 Or (Eq (member msg (key a) (used a_1)) True) % 13.33/13.58 (Or (Eq (member nat a symKeys) False) % 13.33/13.58 (Or (Eq (member (list event) a_1 nS_Sha254967238shared) False) % 13.33/13.58 (Eq (Not (member nat a (keysFor (parts (knows spy a_1))))) True))) % 13.33/13.58 Clause #642 (by clausification #[641]): ∀ (a : nat) (a_1 : list event), % 13.33/13.58 Or (Eq (member msg (key a) (used a_1)) True) % 13.33/13.58 (Or (Eq (member nat a symKeys) False) % 13.43/13.60 (Or (Eq (member (list event) a_1 nS_Sha254967238shared) False) % 13.43/13.60 (Eq (member nat a (keysFor (parts (knows spy a_1)))) False))) % 13.43/13.60 Clause #643 (by superposition #[642, 103]): ∀ (a : list event), % 13.43/13.60 Or (Eq (member msg (key kab) (used a)) True) % 13.43/13.60 (Or (Eq (member (list event) a nS_Sha254967238shared) False) % 13.43/13.60 (Or (Eq (member nat kab (keysFor (parts (knows spy a)))) False) (Eq False True))) % 13.43/13.60 Clause #937 (by clausification #[107]): Eq % 13.43/13.60 (Or % 13.43/13.60 (Or % 13.43/13.60 (Or (Or (Or (Or (Ne a aa) (Ne na (nonce nAa))) (Ne b ba)) (Ne k kab)) % 13.43/13.60 (Ne x (crypt (shrK ba) (mPair (key kab) (agent1 aa))))) % 13.43/13.60 (Not (member msg (crypt kab (nonce nb)) (parts (knows spy evs2))))) % 13.43/13.60 (Exists fun A => member event (says A ba (crypt (shrK ba) (mPair (key kab) (agent1 aa)))) (set event evs2))) % 13.43/13.60 False % 13.43/13.60 Clause #939 (by clausification #[937]): Eq % 13.43/13.60 (Or % 13.43/13.60 (Or (Or (Or (Or (Ne a aa) (Ne na (nonce nAa))) (Ne b ba)) (Ne k kab)) % 13.43/13.60 (Ne x (crypt (shrK ba) (mPair (key kab) (agent1 aa))))) % 13.43/13.60 (Not (member msg (crypt kab (nonce nb)) (parts (knows spy evs2))))) % 13.43/13.60 False % 13.43/13.60 Clause #1128 (by clausification #[643]): ∀ (a : list event), % 13.43/13.60 Or (Eq (member msg (key kab) (used a)) True) % 13.43/13.60 (Or (Eq (member (list event) a nS_Sha254967238shared) False) % 13.43/13.60 (Eq (member nat kab (keysFor (parts (knows spy a)))) False)) % 13.43/13.60 Clause #1129 (by superposition #[1128, 101]): Or (Eq (member msg (key kab) (used evs2)) True) % 13.43/13.60 (Or (Eq (member nat kab (keysFor (parts (knows spy evs2)))) False) (Eq False True)) % 13.43/13.60 Clause #1307 (by clausification #[1129]): Or (Eq (member msg (key kab) (used evs2)) True) (Eq (member nat kab (keysFor (parts (knows spy evs2)))) False) % 13.43/13.60 Clause #1308 (by forward demodulation #[1307, 141]): Or (Eq False True) (Eq (member nat kab (keysFor (parts (knows spy evs2)))) False) % 13.43/13.60 Clause #1309 (by clausification #[1308]): Eq (member nat kab (keysFor (parts (knows spy evs2)))) False % 13.43/13.60 Clause #1329 (by clausification #[939]): Eq (Not (member msg (crypt kab (nonce nb)) (parts (knows spy evs2)))) False % 13.43/13.60 Clause #1331 (by clausification #[1329]): Eq (member msg (crypt kab (nonce nb)) (parts (knows spy evs2))) True % 13.43/13.60 Clause #1334 (by superposition #[1331, 319]): Or (Eq True False) % 13.43/13.60 (Or (Eq (member nat kab symKeys) False) (Eq (member nat kab (keysFor (parts (knows spy evs2)))) True)) % 13.43/13.60 Clause #1468 (by clausification #[1334]): Or (Eq (member nat kab symKeys) False) (Eq (member nat kab (keysFor (parts (knows spy evs2)))) True) % 13.43/13.60 Clause #1469 (by forward demodulation #[1468, 103]): Or (Eq True False) (Eq (member nat kab (keysFor (parts (knows spy evs2)))) True) % 13.43/13.60 Clause #1470 (by clausification #[1469]): Eq (member nat kab (keysFor (parts (knows spy evs2)))) True % 13.43/13.60 Clause #1471 (by superposition #[1470, 1309]): Eq True False % 13.43/13.60 Clause #1475 (by clausification #[1471]): False % 13.43/13.60 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------