%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM693^1 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:57:05 PM UTC 2025 % Result : Theorem 5.38s 5.56s % Output : Proof 5.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.10 % Problem : NUM693^1 : TPTP v9.2.0. Released v3.7.0. % 0.09/0.11 % Command : duper %s % 0.10/0.32 % Computer : n028.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Fri Oct 3 06:51:08 EDT 2025 % 0.10/0.32 % CPUTime : % 5.38/5.56 SZS status Theorem for theBenchmark.p % 5.38/5.56 SZS output start Proof for theBenchmark.p % 5.38/5.56 Clause #1 (by assumption #[]): Eq (∀ (Xx : nat), Ne Xx n_1 → Not (∀ (Xx_0 : nat), Ne Xx (suc Xx_0))) True % 5.38/5.56 Clause #2 (by assumption #[]): Eq (∀ (Xx Xy : nat), more (pl Xx Xy) Xx) True % 5.38/5.56 Clause #3 (by assumption #[]): Eq (∀ (Xx : nat), Eq (suc Xx) (pl n_1 Xx)) True % 5.38/5.56 Clause #4 (by assumption #[]): Eq (Not (Not (more x n_1) → Eq x n_1)) True % 5.38/5.56 Clause #9 (by clausification #[4]): Eq (Not (more x n_1) → Eq x n_1) False % 5.38/5.56 Clause #10 (by clausification #[9]): Eq (Not (more x n_1)) True % 5.38/5.56 Clause #11 (by clausification #[9]): Eq (Eq x n_1) False % 5.38/5.56 Clause #12 (by clausification #[10]): Eq (more x n_1) False % 5.38/5.56 Clause #13 (by clausification #[11]): Ne x n_1 % 5.38/5.56 Clause #14 (by clausification #[2]): ∀ (a : nat), Eq (∀ (Xy : nat), more (pl a Xy) a) True % 5.38/5.56 Clause #15 (by clausification #[14]): ∀ (a a_1 : nat), Eq (more (pl a a_1) a) True % 5.38/5.56 Clause #16 (by clausification #[3]): ∀ (a : nat), Eq (Eq (suc a) (pl n_1 a)) True % 5.38/5.56 Clause #17 (by clausification #[16]): ∀ (a : nat), Eq (suc a) (pl n_1 a) % 5.38/5.56 Clause #18 (by superposition #[17, 15]): ∀ (a : nat), Eq (more (suc a) n_1) True % 5.38/5.56 Clause #19 (by clausification #[1]): ∀ (a : nat), Eq (Ne a n_1 → Not (∀ (Xx_0 : nat), Ne a (suc Xx_0))) True % 5.38/5.56 Clause #20 (by clausification #[19]): ∀ (a : nat), Or (Eq (Ne a n_1) False) (Eq (Not (∀ (Xx_0 : nat), Ne a (suc Xx_0))) True) % 5.38/5.56 Clause #21 (by clausification #[20]): ∀ (a : nat), Or (Eq (Not (∀ (Xx_0 : nat), Ne a (suc Xx_0))) True) (Eq a n_1) % 5.38/5.56 Clause #22 (by clausification #[21]): ∀ (a : nat), Or (Eq a n_1) (Eq (∀ (Xx_0 : nat), Ne a (suc Xx_0)) False) % 5.38/5.56 Clause #23 (by clausification #[22]): ∀ (a a_1 : nat), Or (Eq a n_1) (Eq (Not (Ne a (suc (skS.0 0 a a_1)))) True) % 5.38/5.56 Clause #24 (by clausification #[23]): ∀ (a a_1 : nat), Or (Eq a n_1) (Eq (Ne a (suc (skS.0 0 a a_1))) False) % 5.38/5.56 Clause #25 (by clausification #[24]): ∀ (a a_1 : nat), Or (Eq a n_1) (Eq a (suc (skS.0 0 a a_1))) % 5.38/5.56 Clause #31 (by superposition #[18, 25]): ∀ (a : nat), Or (Eq a n_1) (Eq (more a n_1) True) % 5.38/5.56 Clause #37 (by superposition #[31, 12]): Or (Eq x n_1) (Eq True False) % 5.38/5.56 Clause #39 (by clausification #[37]): Eq x n_1 % 5.38/5.56 Clause #40 (by forward contextual literal cutting #[39, 13]): False % 5.38/5.56 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------