%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM931_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.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:38 PM UTC 2025 % Result : Theorem 7.04s 7.30s % Output : Proof 7.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : NUM931_5 : TPTP v9.2.0. Released v6.0.0. % 0.00/0.10 % Command : duper %s % 0.09/0.30 % Computer : n023.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Fri Oct 3 07:09:23 EDT 2025 % 0.09/0.30 % CPUTime : % 7.04/7.30 SZS status Theorem for theBenchmark.p % 7.04/7.30 SZS output start Proof for theBenchmark.p % 7.04/7.30 Clause #0 (by assumption #[]): Eq (Not (ord_less_eq int (one_one int) m)) True % 7.04/7.30 Clause #71 (by assumption #[]): Eq (∀ (A : Type), linorder A → ∀ (X2 Y1 : A), Not (ord_less_eq A Y1 X2) → ord_less A X2 Y1) True % 7.04/7.30 Clause #83 (by assumption #[]): Eq (∀ (Z2 : int), Iff (ord_less_eq int (one_one int) Z2) (ord_less int (zero_zero int) Z2)) True % 7.04/7.30 Clause #100 (by assumption #[]): Eq (linorder int) True % 7.04/7.30 Clause #111 (by assumption #[]): Eq (Not (ord_less_eq int m (zero_zero int))) True % 7.04/7.30 Clause #112 (by clausification #[0]): Eq (ord_less_eq int (one_one int) m) False % 7.04/7.30 Clause #119 (by clausification #[111]): Eq (ord_less_eq int m (zero_zero int)) False % 7.04/7.30 Clause #273 (by clausification #[71]): ∀ (a : Type), Eq (linorder a → ∀ (X2 Y1 : a), Not (ord_less_eq a Y1 X2) → ord_less a X2 Y1) True % 7.04/7.30 Clause #274 (by clausification #[273]): ∀ (a : Type), Or (Eq (linorder a) False) (Eq (∀ (X2 Y1 : a), Not (ord_less_eq a Y1 X2) → ord_less a X2 Y1) True) % 7.04/7.30 Clause #275 (by clausification #[274]): ∀ (a : Type) (a_1 : a), % 7.04/7.30 Or (Eq (linorder a) False) (Eq (∀ (Y1 : a), Not (ord_less_eq a Y1 a_1) → ord_less a a_1 Y1) True) % 7.04/7.30 Clause #276 (by clausification #[275]): ∀ (a : Type) (a_1 a_2 : a), Or (Eq (linorder a) False) (Eq (Not (ord_less_eq a a_1 a_2) → ord_less a a_2 a_1) True) % 7.04/7.30 Clause #277 (by clausification #[276]): ∀ (a : Type) (a_1 a_2 : a), % 7.04/7.30 Or (Eq (linorder a) False) (Or (Eq (Not (ord_less_eq a a_1 a_2)) False) (Eq (ord_less a a_2 a_1) True)) % 7.04/7.30 Clause #278 (by clausification #[277]): ∀ (a : Type) (a_1 a_2 : a), % 7.04/7.30 Or (Eq (linorder a) False) (Or (Eq (ord_less a a_1 a_2) True) (Eq (ord_less_eq a a_2 a_1) True)) % 7.04/7.30 Clause #280 (by superposition #[278, 100]): ∀ (a a_1 : int), Or (Eq (ord_less int a a_1) True) (Or (Eq (ord_less_eq int a_1 a) True) (Eq False True)) % 7.04/7.30 Clause #555 (by clausification #[280]): ∀ (a a_1 : int), Or (Eq (ord_less int a a_1) True) (Eq (ord_less_eq int a_1 a) True) % 7.04/7.30 Clause #667 (by clausification #[83]): ∀ (a : int), Eq (Iff (ord_less_eq int (one_one int) a) (ord_less int (zero_zero int) a)) True % 7.04/7.30 Clause #668 (by clausification #[667]): ∀ (a : int), Or (Eq (ord_less_eq int (one_one int) a) True) (Eq (ord_less int (zero_zero int) a) False) % 7.04/7.30 Clause #671 (by superposition #[668, 555]): ∀ (a : int), % 7.04/7.30 Or (Eq (ord_less_eq int (one_one int) a) True) (Or (Eq False True) (Eq (ord_less_eq int a (zero_zero int)) True)) % 7.04/7.30 Clause #879 (by clausification #[671]): ∀ (a : int), Or (Eq (ord_less_eq int (one_one int) a) True) (Eq (ord_less_eq int a (zero_zero int)) True) % 7.04/7.30 Clause #880 (by superposition #[879, 112]): Or (Eq (ord_less_eq int m (zero_zero int)) True) (Eq True False) % 7.04/7.30 Clause #916 (by clausification #[880]): Eq (ord_less_eq int m (zero_zero int)) True % 7.04/7.30 Clause #917 (by superposition #[916, 119]): Eq True False % 7.04/7.30 Clause #921 (by clausification #[917]): False % 7.04/7.30 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------