%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWV811_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:39 PM UTC 2025 % Result : Theorem 4.93s 5.17s % Output : Proof 4.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWV811_5 : TPTP v9.2.0. Released v6.0.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.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 : Thu Oct 2 12:15:23 EDT 2025 % 0.13/0.34 % CPUTime : % 4.93/5.17 SZS status Theorem for theBenchmark.p % 4.93/5.17 SZS output start Proof for theBenchmark.p % 4.93/5.17 Clause #5 (by assumption #[]): Eq (∀ (A : Type) (P1 : fun A bool), Eq (takeWhile A P1 (nil A)) (nil A)) True % 4.93/5.17 Clause #7 (by assumption #[]): Eq (∀ (A : Type), Eq (rev A (nil A)) (nil A)) True % 4.93/5.17 Clause #58 (by assumption #[]): Eq (∀ (Aa : agent), Eq (knows Aa (nil event)) (initState Aa)) True % 4.93/5.17 Clause #88 (by assumption #[]): Eq (∀ (Ba : agent) (X2 : msg) (Ka : nat), Not (member msg (crypt Ka X2) (parts (initState Ba)))) True % 4.93/5.17 Clause #107 (by assumption #[]): Eq % 4.93/5.17 (Not % 4.93/5.17 (Or % 4.93/5.17 (Or (member msg (key k) (analz (knows spy (nil event)))) % 4.93/5.17 (Not (member event (says a b (crypt k (mPair (nonce nb) (nonce nb)))) (set event (nil event))))) % 4.93/5.17 (Not % 4.93/5.17 (member msg (crypt k (mPair (nonce nb) (nonce nb))) % 4.93/5.17 (parts % 4.93/5.17 (knows spy % 4.93/5.17 (takeWhile event % 4.93/5.17 (combb bool bool event fNot % 4.93/5.17 (combc event event bool (fequal event) (says a b (crypt k (mPair (nonce nb) (nonce nb)))))) % 4.93/5.17 (rev event (nil event))))))))) % 4.93/5.17 True % 4.93/5.17 Clause #196 (by clausification #[5]): ∀ (a : Type), Eq (∀ (P1 : fun a bool), Eq (takeWhile a P1 (nil a)) (nil a)) True % 4.93/5.17 Clause #197 (by clausification #[196]): ∀ (a : Type) (a_1 : fun a bool), Eq (Eq (takeWhile a a_1 (nil a)) (nil a)) True % 4.93/5.17 Clause #198 (by clausification #[197]): ∀ (a : Type) (a_1 : fun a bool), Eq (takeWhile a a_1 (nil a)) (nil a) % 4.93/5.17 Clause #253 (by clausification #[7]): ∀ (a : Type), Eq (Eq (rev a (nil a)) (nil a)) True % 4.93/5.17 Clause #254 (by clausification #[253]): ∀ (a : Type), Eq (rev a (nil a)) (nil a) % 4.93/5.17 Clause #414 (by clausification #[58]): ∀ (a : agent), Eq (Eq (knows a (nil event)) (initState a)) True % 4.93/5.17 Clause #415 (by clausification #[414]): ∀ (a : agent), Eq (knows a (nil event)) (initState a) % 4.93/5.17 Clause #568 (by clausification #[88]): ∀ (a : agent), Eq (∀ (X2 : msg) (Ka : nat), Not (member msg (crypt Ka X2) (parts (initState a)))) True % 4.93/5.17 Clause #569 (by clausification #[568]): ∀ (a : msg) (a_1 : agent), Eq (∀ (Ka : nat), Not (member msg (crypt Ka a) (parts (initState a_1)))) True % 4.93/5.17 Clause #570 (by clausification #[569]): ∀ (a : nat) (a_1 : msg) (a_2 : agent), Eq (Not (member msg (crypt a a_1) (parts (initState a_2)))) True % 4.93/5.17 Clause #571 (by clausification #[570]): ∀ (a : nat) (a_1 : msg) (a_2 : agent), Eq (member msg (crypt a a_1) (parts (initState a_2))) False % 4.93/5.17 Clause #931 (by clausification #[107]): Eq % 4.93/5.17 (Or % 4.93/5.17 (Or (member msg (key k) (analz (knows spy (nil event)))) % 4.93/5.17 (Not (member event (says a b (crypt k (mPair (nonce nb) (nonce nb)))) (set event (nil event))))) % 4.93/5.17 (Not % 4.93/5.17 (member msg (crypt k (mPair (nonce nb) (nonce nb))) % 4.93/5.17 (parts % 4.93/5.17 (knows spy % 4.93/5.17 (takeWhile event % 4.93/5.17 (combb bool bool event fNot % 4.93/5.17 (combc event event bool (fequal event) (says a b (crypt k (mPair (nonce nb) (nonce nb)))))) % 4.93/5.17 (rev event (nil event)))))))) % 4.93/5.17 False % 4.93/5.17 Clause #932 (by clausification #[931]): Eq % 4.93/5.17 (Not % 4.93/5.17 (member msg (crypt k (mPair (nonce nb) (nonce nb))) % 4.93/5.17 (parts % 4.93/5.17 (knows spy % 4.93/5.17 (takeWhile event % 4.93/5.17 (combb bool bool event fNot % 4.93/5.17 (combc event event bool (fequal event) (says a b (crypt k (mPair (nonce nb) (nonce nb)))))) % 4.93/5.17 (rev event (nil event))))))) % 4.93/5.17 False % 4.93/5.17 Clause #934 (by clausification #[932]): Eq % 4.93/5.17 (member msg (crypt k (mPair (nonce nb) (nonce nb))) % 4.93/5.17 (parts % 4.93/5.17 (knows spy % 4.93/5.17 (takeWhile event % 4.93/5.17 (combb bool bool event fNot % 4.93/5.17 (combc event event bool (fequal event) (says a b (crypt k (mPair (nonce nb) (nonce nb)))))) % 4.93/5.17 (rev event (nil event)))))) % 4.93/5.17 True % 4.93/5.17 Clause #935 (by forward demodulation #[934, 254]): Eq % 4.93/5.17 (member msg (crypt k (mPair (nonce nb) (nonce nb))) % 4.93/5.17 (parts % 4.93/5.17 (knows spy % 4.93/5.17 (takeWhile event % 4.93/5.17 (combb bool bool event fNot % 4.93/5.17 (combc event event bool (fequal event) (says a b (crypt k (mPair (nonce nb) (nonce nb)))))) % 4.93/5.17 (nil event))))) % 4.93/5.17 True % 4.93/5.17 Clause #936 (by forward demodulation #[935, 198]): Eq (member msg (crypt k (mPair (nonce nb) (nonce nb))) (parts (knows spy (nil event)))) True % 4.93/5.17 Clause #937 (by forward demodulation #[936, 415]): Eq (member msg (crypt k (mPair (nonce nb) (nonce nb))) (parts (initState spy))) True % 4.93/5.17 Clause #939 (by superposition #[937, 571]): Eq True False % 4.93/5.17 Clause #944 (by clausification #[939]): False % 4.93/5.17 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------