%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP085^1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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 07:51:11 PM UTC 2025 % Result : Theorem 17.44s 17.64s % Output : Proof 17.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.11 % Problem : ITP085^1 : TPTP v9.2.0. Released v7.5.0. % 0.05/0.12 % Command : duper %s % 0.10/0.31 % Computer : n013.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Thu Oct 2 23:25:08 EDT 2025 % 0.10/0.31 % CPUTime : % 17.44/17.64 SZS status Theorem for theBenchmark.p % 17.44/17.64 SZS output start Proof for theBenchmark.p % 17.44/17.64 Clause #0 (by assumption #[]): Eq (knowle731562421_knows a (cons_S112077679ession (secrecy_sE m) nil_Se901661471ession)) True % 17.44/17.64 Clause #3 (by assumption #[]): Eq % 17.44/17.64 (∀ (C : secrecy_specID) (M2 : secrecy_Secrets), % 17.44/17.64 Eq (knowle731562421_knows C (cons_S112077679ession (secrec1016742679ession (secrecy_sKS M2)) nil_Se901661471ession)) % 17.44/17.64 (knowle945212990e_know C (secrecy_sKS M2))) % 17.44/17.64 True % 17.44/17.64 Clause #7 (by assumption #[]): Eq (∀ (M : secrecy_Secrets), Eq (secrec1016742679ession (secrecy_sKS M)) (secrecy_sE M)) True % 17.44/17.64 Clause #343 (by assumption #[]): Eq (Not (knowle945212990e_know a (secrecy_sKS m))) True % 17.44/17.64 Clause #380 (by clausification #[3]): ∀ (a : secrecy_specID), % 17.44/17.64 Eq % 17.44/17.64 (∀ (M2 : secrecy_Secrets), % 17.44/17.64 Eq % 17.44/17.64 (knowle731562421_knows a % 17.44/17.64 (cons_S112077679ession (secrec1016742679ession (secrecy_sKS M2)) nil_Se901661471ession)) % 17.44/17.64 (knowle945212990e_know a (secrecy_sKS M2))) % 17.44/17.64 True % 17.44/17.64 Clause #381 (by clausification #[380]): ∀ (a : secrecy_specID) (a_1 : secrecy_Secrets), % 17.44/17.64 Eq % 17.44/17.64 (Eq % 17.44/17.64 (knowle731562421_knows a (cons_S112077679ession (secrec1016742679ession (secrecy_sKS a_1)) nil_Se901661471ession)) % 17.44/17.64 (knowle945212990e_know a (secrecy_sKS a_1))) % 17.44/17.64 True % 17.44/17.64 Clause #382 (by clausification #[381]): ∀ (a : secrecy_specID) (a_1 : secrecy_Secrets), % 17.44/17.64 Eq (knowle731562421_knows a (cons_S112077679ession (secrec1016742679ession (secrecy_sKS a_1)) nil_Se901661471ession)) % 17.44/17.64 (knowle945212990e_know a (secrecy_sKS a_1)) % 17.44/17.64 Clause #412 (by clausification #[343]): Eq (knowle945212990e_know a (secrecy_sKS m)) False % 17.44/17.64 Clause #651 (by clausification #[7]): ∀ (a : secrecy_Secrets), Eq (Eq (secrec1016742679ession (secrecy_sKS a)) (secrecy_sE a)) True % 17.44/17.64 Clause #652 (by clausification #[651]): ∀ (a : secrecy_Secrets), Eq (secrec1016742679ession (secrecy_sKS a)) (secrecy_sE a) % 17.44/17.64 Clause #653 (by backward demodulation #[652, 382]): ∀ (a : secrecy_specID) (a_1 : secrecy_Secrets), % 17.44/17.64 Eq (knowle731562421_knows a (cons_S112077679ession (secrecy_sE a_1) nil_Se901661471ession)) % 17.44/17.64 (knowle945212990e_know a (secrecy_sKS a_1)) % 17.44/17.64 Clause #3822 (by superposition #[653, 0]): Eq (knowle945212990e_know a (secrecy_sKS m)) True % 17.44/17.64 Clause #3934 (by superposition #[3822, 412]): Eq True False % 17.44/17.64 Clause #3953 (by clausification #[3934]): False % 17.44/17.64 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------