%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT086+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:23 AM UTC 2026 % Result : Theorem 81.60s 81.99s % Output : Proof 81.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT086+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.05 % Command : duper %s % 0.09/0.37 % Computer : n001.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Mon Sep 7 14:24:52 UTC 2026 % 0.09/0.38 % CPUTime : % 81.60/81.99 SZS status Theorem for theBenchmark.p % 81.60/81.99 SZS output start Proof for theBenchmark.p % 81.60/81.99 Clause #3 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (leq X Y) (Or (less X Y) (Eq X Y))) True % 81.60/81.99 Clause #4 (by assumption #[]): Eq (∀ (X Y : Iota), And (leq X Y) (leq Y X) → Eq X Y) True % 81.60/81.99 Clause #5 (by assumption #[]): Eq (∀ (X Y : Iota), less X Y → leq X Y) True % 81.60/81.99 Clause #10 (by assumption #[]): Eq (∀ (X A B : Iota), Iff (in_lopen X A B) (And (less A X) (leq X B))) True % 81.60/81.99 Clause #32 (by assumption #[]): Eq (less v0 v200) True % 81.60/81.99 Clause #36 (by assumption #[]): Eq (less v200 v400) True % 81.60/81.99 Clause #41 (by assumption #[]): Eq (less v600 v800) True % 81.60/81.99 Clause #42 (by assumption #[]): Eq % 81.60/81.99 (And % 81.60/81.99 (And % 81.60/81.99 (And % 81.60/81.99 (And % 81.60/81.99 (And (And (And (And (And (Ne v0 v200) (Ne v0 v400)) (Ne v0 v600)) (Ne v0 v800)) (Ne v200 v400)) % 81.60/81.99 (Ne v200 v600)) % 81.60/81.99 (Ne v200 v800)) % 81.60/81.99 (Ne v400 v600)) % 81.60/81.99 (Ne v400 v800)) % 81.60/81.99 (Ne v600 v800)) % 81.60/81.99 True % 81.60/81.99 Clause #43 (by assumption #[]): Eq % 81.60/81.99 (Not % 81.60/81.99 (Exists fun X => % 81.60/81.99 Exists fun Y => % 81.60/81.99 And (And (leq v800 X) (in_lopen Y v0 v200)) % 81.60/81.99 (Or (And (in_lopen X v0 v600) (Not (in_lopen Y v0 v400))) % 81.60/81.99 (And (Not (in_lopen X v0 v600)) (in_lopen Y v0 v400))))) % 81.60/81.99 True % 81.60/81.99 Clause #131 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (leq a Y) (Or (less a Y) (Eq a Y))) True % 81.60/81.99 Clause #132 (by clausification #[131]): ∀ (a a_1 : Iota), Eq (Iff (leq a a_1) (Or (less a a_1) (Eq a a_1))) True % 81.60/81.99 Clause #133 (by clausification #[132]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) True) (Eq (Or (less a a_1) (Eq a a_1)) False) % 81.60/81.99 Clause #135 (by clausification #[133]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) True) (Eq (Eq a a_1) False) % 81.60/81.99 Clause #137 (by clausification #[135]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) True) (Ne a a_1) % 81.60/81.99 Clause #138 (by destructive equality resolution #[137]): ∀ (a : Iota), Eq (leq a a) True % 81.60/81.99 Clause #142 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (Y : Iota), less a Y → leq a Y) True % 81.60/81.99 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), Eq (less a a_1 → leq a a_1) True % 81.60/81.99 Clause #144 (by clausification #[143]): ∀ (a a_1 : Iota), Or (Eq (less a a_1) False) (Eq (leq a a_1) True) % 81.60/81.99 Clause #148 (by superposition #[144, 36]): Or (Eq (leq v200 v400) True) (Eq False True) % 81.60/81.99 Clause #149 (by superposition #[144, 41]): Or (Eq (leq v600 v800) True) (Eq False True) % 81.60/81.99 Clause #162 (by clausification #[149]): Eq (leq v600 v800) True % 81.60/81.99 Clause #167 (by clausification #[148]): Eq (leq v200 v400) True % 81.60/81.99 Clause #172 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (leq a Y) (leq Y a) → Eq a Y) True % 81.60/81.99 Clause #173 (by clausification #[172]): ∀ (a a_1 : Iota), Eq (And (leq a a_1) (leq a_1 a) → Eq a a_1) True % 81.60/81.99 Clause #174 (by clausification #[173]): ∀ (a a_1 : Iota), Or (Eq (And (leq a a_1) (leq a_1 a)) False) (Eq (Eq a a_1) True) % 81.60/81.99 Clause #175 (by clausification #[174]): ∀ (a a_1 : Iota), Or (Eq (Eq a a_1) True) (Or (Eq (leq a a_1) False) (Eq (leq a_1 a) False)) % 81.60/81.99 Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) False) (Or (Eq (leq a_1 a) False) (Eq a a_1)) % 81.60/81.99 Clause #178 (by superposition #[176, 162]): Or (Eq (leq v800 v600) False) (Or (Eq v600 v800) (Eq False True)) % 81.60/81.99 Clause #305 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (A B : Iota), Iff (in_lopen a A B) (And (less A a) (leq a B))) True % 81.60/81.99 Clause #306 (by clausification #[305]): ∀ (a a_1 : Iota), Eq (∀ (B : Iota), Iff (in_lopen a a_1 B) (And (less a_1 a) (leq a B))) True % 81.60/81.99 Clause #307 (by clausification #[306]): ∀ (a a_1 a_2 : Iota), Eq (Iff (in_lopen a a_1 a_2) (And (less a_1 a) (leq a a_2))) True % 81.60/81.99 Clause #308 (by clausification #[307]): ∀ (a a_1 a_2 : Iota), Or (Eq (in_lopen a a_1 a_2) True) (Eq (And (less a_1 a) (leq a a_2)) False) % 81.60/81.99 Clause #309 (by clausification #[307]): ∀ (a a_1 a_2 : Iota), Or (Eq (in_lopen a a_1 a_2) False) (Eq (And (less a_1 a) (leq a a_2)) True) % 81.60/81.99 Clause #310 (by clausification #[308]): ∀ (a a_1 a_2 : Iota), Or (Eq (in_lopen a a_1 a_2) True) (Or (Eq (less a_1 a) False) (Eq (leq a a_2) False)) % 81.60/81.99 Clause #320 (by superposition #[310, 32]): ∀ (a : Iota), Or (Eq (in_lopen v200 v0 a) True) (Or (Eq (leq v200 a) False) (Eq False True)) % 81.76/82.10 Clause #328 (by clausification #[178]): Or (Eq (leq v800 v600) False) (Eq v600 v800) % 81.76/82.10 Clause #668 (by clausification #[42]): Eq (Ne v600 v800) True % 81.76/82.10 Clause #670 (by clausification #[668]): Ne v600 v800 % 81.76/82.10 Clause #671 (by backward contextual literal cutting #[670, 328]): Eq (leq v800 v600) False % 81.76/82.10 Clause #688 (by clausification #[43]): Eq % 81.76/82.10 (Exists fun X => % 81.76/82.10 Exists fun Y => % 81.76/82.10 And (And (leq v800 X) (in_lopen Y v0 v200)) % 81.76/82.10 (Or (And (in_lopen X v0 v600) (Not (in_lopen Y v0 v400))) % 81.76/82.10 (And (Not (in_lopen X v0 v600)) (in_lopen Y v0 v400)))) % 81.76/82.10 False % 81.76/82.10 Clause #689 (by clausification #[688]): ∀ (a : Iota), % 81.76/82.10 Eq % 81.76/82.10 (Exists fun Y => % 81.76/82.10 And (And (leq v800 a) (in_lopen Y v0 v200)) % 81.76/82.10 (Or (And (in_lopen a v0 v600) (Not (in_lopen Y v0 v400))) % 81.76/82.10 (And (Not (in_lopen a v0 v600)) (in_lopen Y v0 v400)))) % 81.76/82.10 False % 81.76/82.10 Clause #690 (by clausification #[689]): ∀ (a a_1 : Iota), % 81.76/82.10 Eq % 81.76/82.10 (And (And (leq v800 a) (in_lopen a_1 v0 v200)) % 81.76/82.10 (Or (And (in_lopen a v0 v600) (Not (in_lopen a_1 v0 v400))) % 81.76/82.10 (And (Not (in_lopen a v0 v600)) (in_lopen a_1 v0 v400)))) % 81.76/82.10 False % 81.76/82.10 Clause #691 (by clausification #[690]): ∀ (a a_1 : Iota), % 81.76/82.10 Or (Eq (And (leq v800 a) (in_lopen a_1 v0 v200)) False) % 81.76/82.10 (Eq % 81.76/82.10 (Or (And (in_lopen a v0 v600) (Not (in_lopen a_1 v0 v400))) % 81.76/82.10 (And (Not (in_lopen a v0 v600)) (in_lopen a_1 v0 v400))) % 81.76/82.10 False) % 81.76/82.10 Clause #692 (by clausification #[691]): ∀ (a a_1 : Iota), % 81.76/82.10 Or % 81.76/82.10 (Eq % 81.76/82.10 (Or (And (in_lopen a v0 v600) (Not (in_lopen a_1 v0 v400))) % 81.76/82.10 (And (Not (in_lopen a v0 v600)) (in_lopen a_1 v0 v400))) % 81.76/82.10 False) % 81.76/82.10 (Or (Eq (leq v800 a) False) (Eq (in_lopen a_1 v0 v200) False)) % 81.76/82.10 Clause #693 (by clausification #[692]): ∀ (a a_1 : Iota), % 81.76/82.10 Or (Eq (leq v800 a) False) % 81.76/82.10 (Or (Eq (in_lopen a_1 v0 v200) False) (Eq (And (Not (in_lopen a v0 v600)) (in_lopen a_1 v0 v400)) False)) % 81.76/82.10 Clause #695 (by clausification #[693]): ∀ (a a_1 : Iota), % 81.76/82.10 Or (Eq (leq v800 a) False) % 81.76/82.10 (Or (Eq (in_lopen a_1 v0 v200) False) (Or (Eq (Not (in_lopen a v0 v600)) False) (Eq (in_lopen a_1 v0 v400) False))) % 81.76/82.10 Clause #696 (by clausification #[695]): ∀ (a a_1 : Iota), % 81.76/82.10 Or (Eq (leq v800 a) False) % 81.76/82.10 (Or (Eq (in_lopen a_1 v0 v200) False) (Or (Eq (in_lopen a_1 v0 v400) False) (Eq (in_lopen a v0 v600) True))) % 81.76/82.10 Clause #697 (by superposition #[696, 138]): ∀ (a : Iota), % 81.76/82.10 Or (Eq (in_lopen a v0 v200) False) % 81.76/82.10 (Or (Eq (in_lopen a v0 v400) False) (Or (Eq (in_lopen v800 v0 v600) True) (Eq False True))) % 81.76/82.10 Clause #1366 (by clausification #[320]): ∀ (a : Iota), Or (Eq (in_lopen v200 v0 a) True) (Eq (leq v200 a) False) % 81.76/82.10 Clause #1367 (by superposition #[1366, 167]): Or (Eq (in_lopen v200 v0 v400) True) (Eq False True) % 81.76/82.10 Clause #1370 (by superposition #[1366, 138]): Or (Eq (in_lopen v200 v0 v200) True) (Eq False True) % 81.76/82.10 Clause #1392 (by clausification #[1370]): Eq (in_lopen v200 v0 v200) True % 81.76/82.10 Clause #1404 (by clausification #[1367]): Eq (in_lopen v200 v0 v400) True % 81.76/82.10 Clause #7145 (by clausification #[309]): ∀ (a a_1 a_2 : Iota), Or (Eq (in_lopen a a_1 a_2) False) (Eq (leq a a_2) True) % 81.76/82.10 Clause #15510 (by clausification #[697]): ∀ (a : Iota), Or (Eq (in_lopen a v0 v200) False) (Or (Eq (in_lopen a v0 v400) False) (Eq (in_lopen v800 v0 v600) True)) % 81.76/82.10 Clause #15511 (by superposition #[15510, 1392]): Or (Eq (in_lopen v200 v0 v400) False) (Or (Eq (in_lopen v800 v0 v600) True) (Eq False True)) % 81.76/82.10 Clause #15610 (by clausification #[15511]): Or (Eq (in_lopen v200 v0 v400) False) (Eq (in_lopen v800 v0 v600) True) % 81.76/82.10 Clause #15611 (by superposition #[15610, 1404]): Or (Eq (in_lopen v800 v0 v600) True) (Eq False True) % 81.76/82.10 Clause #15627 (by clausification #[15611]): Eq (in_lopen v800 v0 v600) True % 81.76/82.10 Clause #15629 (by superposition #[15627, 7145]): Or (Eq True False) (Eq (leq v800 v600) True) % 81.76/82.10 Clause #15643 (by clausification #[15629]): Eq (leq v800 v600) True % 81.76/82.10 Clause #15644 (by superposition #[15643, 671]): Eq True False % 81.76/82.10 Clause #15696 (by clausification #[15644]): False % 81.76/82.10 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------