%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW469_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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:06:13 PM UTC 2025 % Result : Theorem 11.85s 12.02s % Output : Proof 11.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWW469_5 : TPTP v9.2.0. Released v6.0.0. % 0.11/0.14 % Command : duper %s % 0.13/0.35 % Computer : n026.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 10:57:38 EDT 2025 % 0.13/0.35 % CPUTime : % 11.85/12.02 SZS status Theorem for theBenchmark.p % 11.85/12.02 SZS output start Proof for theBenchmark.p % 11.85/12.02 Clause #0 (by assumption #[]): Eq (Iff hoare_531836380gleton (Exists fun S2 => Exists fun T2 => Ne S2 T2)) True % 11.85/12.02 Clause #131 (by assumption #[]): Eq hoare_531836380gleton True % 11.85/12.02 Clause #132 (by assumption #[]): Eq (Not (∀ (T : state), Exists fun S => Ne S T)) True % 11.85/12.02 Clause #134 (by betaEtaReduce #[0]): Eq (Iff hoare_531836380gleton (Exists fun S2 => Exists (Ne S2))) True % 11.85/12.02 Clause #136 (by clausification #[134]): Or (Eq hoare_531836380gleton False) (Eq (Exists fun S2 => Exists (Ne S2)) True) % 11.85/12.02 Clause #648 (by clausification #[132]): Eq (∀ (T : state), Exists fun S => Ne S T) False % 11.85/12.02 Clause #649 (by clausification #[648]): ∀ (a : state), Eq (Not (Exists fun S => Ne S (skS.0 7 a))) True % 11.85/12.02 Clause #650 (by clausification #[649]): ∀ (a : state), Eq (Exists fun S => Ne S (skS.0 7 a)) False % 11.85/12.02 Clause #651 (by clausification #[650]): ∀ (a a_1 : state), Eq (Ne a (skS.0 7 a_1)) False % 11.85/12.02 Clause #652 (by clausification #[651]): ∀ (a a_1 : state), Eq a (skS.0 7 a_1) % 11.85/12.02 Clause #655 (by superposition #[652, 652]): ∀ (a a_1 : state), Eq a a_1 % 11.85/12.02 Clause #3111 (by clausification #[136]): ∀ (a : state), Or (Eq hoare_531836380gleton False) (Eq (Exists (Ne (skS.0 16 a))) True) % 11.85/12.02 Clause #3112 (by clausification #[3111]): ∀ (a a_1 : state), Or (Eq hoare_531836380gleton False) (Eq (Ne (skS.0 16 a) (skS.0 17 a a_1)) True) % 11.85/12.02 Clause #3113 (by clausification #[3112]): ∀ (a a_1 : state), Or (Eq hoare_531836380gleton False) (Ne (skS.0 16 a) (skS.0 17 a a_1)) % 11.85/12.02 Clause #3114 (by forward demodulation #[3113, 131]): ∀ (a a_1 : state), Or (Eq True False) (Ne (skS.0 16 a) (skS.0 17 a a_1)) % 11.85/12.02 Clause #3115 (by clausification #[3114]): ∀ (a a_1 : state), Ne (skS.0 16 a) (skS.0 17 a a_1) % 11.85/12.02 Clause #3116 (by forward contextual literal cutting #[3115, 655]): False % 11.85/12.02 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------