%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT106+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:25 AM UTC 2026 % Result : Unsatisfiable 22.47s 22.79s % Output : Proof 22.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT106+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.05 % Command : duper %s % 0.10/0.38 % Computer : n027.cluster.edu % 0.10/0.38 % Model : x86_64 x86_64 % 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.38 % Memory : 8046.5625MB % 0.10/0.38 % OS : Linux 6.8.0-71-generic % 0.10/0.38 % CPULimit : 300 % 0.10/0.38 % WCLimit : 300 % 0.10/0.38 % DateTime : Mon Sep 7 14:44:45 UTC 2026 % 0.10/0.38 % CPUTime : % 22.47/22.79 SZS status Theorem for theBenchmark.p % 22.47/22.79 SZS output start Proof for theBenchmark.p % 22.47/22.79 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), Not (less X X)) True % 22.47/22.79 Clause #4 (by assumption #[]): Eq (∀ (X Y : Iota), And (leq X Y) (leq Y X) → Eq X Y) True % 22.47/22.79 Clause #5 (by assumption #[]): Eq (∀ (X Y : Iota), less X Y → leq X Y) True % 22.47/22.79 Clause #7 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (less X Y) (leq Y Z) → less X Z) True % 22.47/22.79 Clause #8 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (leq X Y) (leq Y Z) → leq X Z) True % 22.47/22.79 Clause #10 (by assumption #[]): Eq (∀ (X A B : Iota), Iff (in_lopen X A B) (And (less A X) (leq X B))) True % 22.47/22.79 Clause #31 (by assumption #[]): Eq (less v600 v800) True % 22.47/22.79 Clause #34 (by assumption #[]): Eq (in_lopen w v0 v600) True % 22.47/22.79 Clause #35 (by assumption #[]): Eq (leq v800 w) True % 22.47/22.79 Clause #36 (by clausification #[0]): ∀ (a : Iota), Eq (Not (less a a)) True % 22.47/22.79 Clause #37 (by clausification #[36]): ∀ (a : Iota), Eq (less a a) False % 22.47/22.79 Clause #48 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (Y : Iota), less a Y → leq a Y) True % 22.47/22.79 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), Eq (less a a_1 → leq a a_1) True % 22.47/22.79 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), Or (Eq (less a a_1) False) (Eq (leq a a_1) True) % 22.47/22.79 Clause #51 (by superposition #[50, 31]): Or (Eq (leq v600 v800) True) (Eq False True) % 22.47/22.79 Clause #106 (by clausification #[51]): Eq (leq v600 v800) True % 22.47/22.79 Clause #111 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (leq a Y) (leq Y a) → Eq a Y) True % 22.47/22.79 Clause #112 (by clausification #[111]): ∀ (a a_1 : Iota), Eq (And (leq a a_1) (leq a_1 a) → Eq a a_1) True % 22.47/22.79 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Or (Eq (And (leq a a_1) (leq a_1 a)) False) (Eq (Eq a a_1) True) % 22.47/22.79 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), Or (Eq (Eq a a_1) True) (Or (Eq (leq a a_1) False) (Eq (leq a_1 a) False)) % 22.47/22.79 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), Or (Eq (leq a a_1) False) (Or (Eq (leq a_1 a) False) (Eq a a_1)) % 22.47/22.79 Clause #142 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (less a Y) (leq Y Z) → less a Z) True % 22.47/22.79 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (less a a_1) (leq a_1 Z) → less a Z) True % 22.47/22.79 Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 : Iota), Eq (And (less a a_1) (leq a_1 a_2) → less a a_2) True % 22.47/22.79 Clause #145 (by clausification #[144]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (less a a_1) (leq a_1 a_2)) False) (Eq (less a a_2) True) % 22.47/22.79 Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 : Iota), Or (Eq (less a a_1) True) (Or (Eq (less a a_2) False) (Eq (leq a_2 a_1) False)) % 22.47/22.79 Clause #147 (by superposition #[146, 31]): ∀ (a : Iota), Or (Eq (less v600 a) True) (Or (Eq (leq v800 a) False) (Eq False True)) % 22.47/22.79 Clause #158 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (leq a Y) (leq Y Z) → leq a Z) True % 22.47/22.79 Clause #159 (by clausification #[158]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (leq a a_1) (leq a_1 Z) → leq a Z) True % 22.47/22.79 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), Eq (And (leq a a_1) (leq a_1 a_2) → leq a a_2) True % 22.47/22.79 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (leq a a_1) (leq a_1 a_2)) False) (Eq (leq a a_2) True) % 22.47/22.79 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 : Iota), Or (Eq (leq a a_1) True) (Or (Eq (leq a a_2) False) (Eq (leq a_2 a_1) False)) % 22.47/22.79 Clause #165 (by superposition #[162, 106]): ∀ (a : Iota), Or (Eq (leq v600 a) True) (Or (Eq (leq v800 a) False) (Eq False True)) % 22.47/22.79 Clause #209 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (A B : Iota), Iff (in_lopen a A B) (And (less A a) (leq a B))) True % 22.47/22.79 Clause #210 (by clausification #[209]): ∀ (a a_1 : Iota), Eq (∀ (B : Iota), Iff (in_lopen a a_1 B) (And (less a_1 a) (leq a B))) True % 22.47/22.79 Clause #211 (by clausification #[210]): ∀ (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 % 22.47/22.79 Clause #213 (by clausification #[211]): ∀ (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) % 22.57/22.83 Clause #497 (by clausification #[165]): ∀ (a : Iota), Or (Eq (leq v600 a) True) (Eq (leq v800 a) False) % 22.57/22.83 Clause #498 (by superposition #[497, 35]): Or (Eq (leq v600 w) True) (Eq False True) % 22.57/22.83 Clause #501 (by clausification #[498]): Eq (leq v600 w) True % 22.57/22.83 Clause #503 (by superposition #[501, 115]): Or (Eq True False) (Or (Eq (leq w v600) False) (Eq v600 w)) % 22.57/22.83 Clause #522 (by clausification #[503]): Or (Eq (leq w v600) False) (Eq v600 w) % 22.57/22.83 Clause #546 (by clausification #[147]): ∀ (a : Iota), Or (Eq (less v600 a) True) (Eq (leq v800 a) False) % 22.57/22.83 Clause #547 (by superposition #[546, 35]): Or (Eq (less v600 w) True) (Eq False True) % 22.57/22.83 Clause #551 (by clausification #[547]): Eq (less v600 w) True % 22.57/22.83 Clause #3798 (by clausification #[213]): ∀ (a a_1 a_2 : Iota), Or (Eq (in_lopen a a_1 a_2) False) (Eq (leq a a_2) True) % 22.57/22.83 Clause #3800 (by superposition #[3798, 34]): Or (Eq (leq w v600) True) (Eq False True) % 22.57/22.83 Clause #3805 (by clausification #[3800]): Eq (leq w v600) True % 22.57/22.83 Clause #3806 (by superposition #[3805, 522]): Or (Eq True False) (Eq v600 w) % 22.57/22.83 Clause #3837 (by clausification #[3806]): Eq v600 w % 22.57/22.83 Clause #3844 (by backward demodulation #[3837, 551]): Eq (less v600 v600) True % 22.57/22.83 Clause #3902 (by superposition #[3844, 37]): Eq True False % 22.57/22.83 Clause #3914 (by clausification #[3902]): False % 22.57/22.83 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------