%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW504_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:06:22 PM UTC 2025 % Result : Theorem 12.83s 13.03s % Output : Proof 12.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SWW504_5 : TPTP v9.2.0. Released v6.0.0. % 0.08/0.14 % Command : duper %s % 0.15/0.35 % Computer : n031.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 10:30:53 EDT 2025 % 0.15/0.35 % CPUTime : % 12.83/13.03 SZS status Theorem for theBenchmark.p % 12.83/13.03 SZS output start Proof for theBenchmark.p % 12.83/13.03 Clause #131 (by assumption #[]): Eq (Exists fun S1 => Exists fun T => Ne S1 T) True % 12.83/13.03 Clause #132 (by assumption #[]): Eq (Not (∀ (T : state), Exists fun S => Ne S T)) True % 12.83/13.03 Clause #617 (by clausification #[132]): Eq (∀ (T : state), Exists fun S => Ne S T) False % 12.83/13.03 Clause #618 (by clausification #[617]): ∀ (a : state), Eq (Not (Exists fun S => Ne S (skS.0 7 a))) True % 12.83/13.03 Clause #619 (by clausification #[618]): ∀ (a : state), Eq (Exists fun S => Ne S (skS.0 7 a)) False % 12.83/13.03 Clause #620 (by clausification #[619]): ∀ (a a_1 : state), Eq (Ne a (skS.0 7 a_1)) False % 12.83/13.03 Clause #621 (by clausification #[620]): ∀ (a a_1 : state), Eq a (skS.0 7 a_1) % 12.83/13.03 Clause #624 (by superposition #[621, 621]): ∀ (a a_1 : state), Eq a a_1 % 12.83/13.03 Clause #3133 (by betaEtaReduce #[131]): Eq (Exists fun S1 => Exists (Ne S1)) True % 12.83/13.03 Clause #3134 (by clausification #[3133]): ∀ (a : state), Eq (Exists (Ne (skS.0 16 a))) True % 12.83/13.03 Clause #3135 (by clausification #[3134]): ∀ (a a_1 : state), Eq (Ne (skS.0 16 a) (skS.0 17 a a_1)) True % 12.83/13.04 Clause #3136 (by clausification #[3135]): ∀ (a a_1 : state), Ne (skS.0 16 a) (skS.0 17 a a_1) % 12.83/13.04 Clause #3137 (by forward contextual literal cutting #[3136, 624]): False % 12.83/13.04 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------