%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:22 AM UTC 2026 % Result : Theorem 14.16s 14.49s % Output : Proof 14.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.07 % Command : duper %s % 0.17/0.43 % Computer : n018.cluster.edu % 0.17/0.43 % Model : x86_64 x86_64 % 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.43 % Memory : 8046.5625MB % 0.17/0.43 % OS : Linux 6.8.0-71-generic % 0.17/0.43 % CPULimit : 300 % 0.17/0.43 % WCLimit : 300 % 0.17/0.43 % DateTime : Mon Sep 7 13:59:07 UTC 2026 % 0.17/0.44 % CPUTime : % 14.16/14.49 SZS status Theorem for theBenchmark.p % 14.16/14.49 SZS output start Proof for theBenchmark.p % 14.16/14.49 Clause #1 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (less X Y) (less Y Z) → less X Z) True % 14.16/14.49 Clause #3 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (leq X Y) (Or (less X Y) (Eq X Y))) True % 14.16/14.49 Clause #5 (by assumption #[]): Eq (∀ (X Y : Iota), less X Y → leq X Y) True % 14.16/14.49 Clause #9 (by assumption #[]): Eq (∀ (X A B : Iota), Iff (in_closed X A B) (And (leq A X) (leq X B))) True % 14.16/14.49 Clause #32 (by assumption #[]): Eq (less n0 n5) True % 14.16/14.49 Clause #33 (by assumption #[]): Eq (less n5 n10) True % 14.16/14.49 Clause #35 (by assumption #[]): Eq (Not (Exists fun X => And (in_closed X n0 n10) (in_closed X n5 n10))) True % 14.16/14.49 Clause #41 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (Y : Iota), less a Y → leq a Y) True % 14.16/14.49 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), Eq (less a a_1 → leq a a_1) True % 14.16/14.49 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), Or (Eq (less a a_1) False) (Eq (leq a a_1) True) % 14.16/14.49 Clause #44 (by superposition #[43, 33]): Or (Eq (leq n5 n10) True) (Eq False True) % 14.16/14.49 Clause #46 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (less a Y) (less Y Z) → less a Z) True % 14.16/14.49 Clause #47 (by clausification #[46]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (less a a_1) (less a_1 Z) → less a Z) True % 14.16/14.49 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 : Iota), Eq (And (less a a_1) (less a_1 a_2) → less a a_2) True % 14.16/14.49 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (less a a_1) (less a_1 a_2)) False) (Eq (less a a_2) True) % 14.16/14.49 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 : Iota), Or (Eq (less a a_1) True) (Or (Eq (less a a_2) False) (Eq (less a_2 a_1) False)) % 14.16/14.49 Clause #52 (by superposition #[50, 32]): ∀ (a : Iota), Or (Eq (less n0 a) True) (Or (Eq (less n5 a) False) (Eq False True)) % 14.16/14.49 Clause #54 (by clausification #[44]): Eq (leq n5 n10) True % 14.16/14.49 Clause #141 (by clausification #[52]): ∀ (a : Iota), Or (Eq (less n0 a) True) (Eq (less n5 a) False) % 14.16/14.49 Clause #142 (by superposition #[141, 33]): Or (Eq (less n0 n10) True) (Eq False True) % 14.16/14.49 Clause #147 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (leq a Y) (Or (less a Y) (Eq a Y))) True % 14.16/14.49 Clause #148 (by clausification #[147]): ∀ (a a_1 : Iota), Eq (Iff (leq a a_1) (Or (less a a_1) (Eq a a_1))) True % 14.16/14.49 Clause #149 (by clausification #[148]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) True) (Eq (Or (less a a_1) (Eq a a_1)) False) % 14.16/14.49 Clause #151 (by clausification #[149]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) True) (Eq (Eq a a_1) False) % 14.16/14.49 Clause #153 (by clausification #[151]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) True) (Ne a a_1) % 14.16/14.49 Clause #154 (by destructive equality resolution #[153]): ∀ (a : Iota), Eq (leq a a) True % 14.16/14.49 Clause #157 (by clausification #[142]): Eq (less n0 n10) True % 14.16/14.49 Clause #158 (by superposition #[157, 43]): Or (Eq True False) (Eq (leq n0 n10) True) % 14.16/14.49 Clause #165 (by clausification #[158]): Eq (leq n0 n10) True % 14.16/14.49 Clause #181 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (A B : Iota), Iff (in_closed a A B) (And (leq A a) (leq a B))) True % 14.16/14.49 Clause #182 (by clausification #[181]): ∀ (a a_1 : Iota), Eq (∀ (B : Iota), Iff (in_closed a a_1 B) (And (leq a_1 a) (leq a B))) True % 14.16/14.49 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), Eq (Iff (in_closed a a_1 a_2) (And (leq a_1 a) (leq a a_2))) True % 14.16/14.49 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 : Iota), Or (Eq (in_closed a a_1 a_2) True) (Eq (And (leq a_1 a) (leq a a_2)) False) % 14.16/14.49 Clause #186 (by clausification #[184]): ∀ (a a_1 a_2 : Iota), Or (Eq (in_closed a a_1 a_2) True) (Or (Eq (leq a_1 a) False) (Eq (leq a a_2) False)) % 14.16/14.49 Clause #188 (by superposition #[186, 54]): ∀ (a : Iota), Or (Eq (in_closed n10 n5 a) True) (Or (Eq (leq n10 a) False) (Eq False True)) % 14.16/14.49 Clause #189 (by superposition #[186, 165]): ∀ (a : Iota), Or (Eq (in_closed n10 n0 a) True) (Or (Eq (leq n10 a) False) (Eq False True)) % 14.16/14.49 Clause #716 (by clausification #[35]): Eq (Exists fun X => And (in_closed X n0 n10) (in_closed X n5 n10)) False % 14.16/14.49 Clause #717 (by clausification #[716]): ∀ (a : Iota), Eq (And (in_closed a n0 n10) (in_closed a n5 n10)) False % 14.26/14.50 Clause #718 (by clausification #[717]): ∀ (a : Iota), Or (Eq (in_closed a n0 n10) False) (Eq (in_closed a n5 n10) False) % 14.26/14.50 Clause #1173 (by clausification #[189]): ∀ (a : Iota), Or (Eq (in_closed n10 n0 a) True) (Eq (leq n10 a) False) % 14.26/14.50 Clause #1177 (by superposition #[1173, 154]): Or (Eq (in_closed n10 n0 n10) True) (Eq False True) % 14.26/14.50 Clause #1183 (by clausification #[1177]): Eq (in_closed n10 n0 n10) True % 14.26/14.50 Clause #1184 (by superposition #[1183, 718]): Or (Eq True False) (Eq (in_closed n10 n5 n10) False) % 14.26/14.50 Clause #1196 (by clausification #[1184]): Eq (in_closed n10 n5 n10) False % 14.26/14.50 Clause #1205 (by clausification #[188]): ∀ (a : Iota), Or (Eq (in_closed n10 n5 a) True) (Eq (leq n10 a) False) % 14.26/14.50 Clause #1209 (by superposition #[1205, 154]): Or (Eq (in_closed n10 n5 n10) True) (Eq False True) % 14.26/14.50 Clause #1240 (by clausification #[1209]): Eq (in_closed n10 n5 n10) True % 14.26/14.50 Clause #1241 (by superposition #[1240, 1196]): Eq True False % 14.26/14.50 Clause #1253 (by clausification #[1241]): False % 14.26/14.50 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------