%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT071+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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 63.14s 63.42s % Output : Proof 63.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT071+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.05 % Command : duper %s % 0.12/0.37 % Computer : n015.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Mon Sep 7 13:57:45 UTC 2026 % 0.12/0.37 % CPUTime : % 63.14/63.42 SZS status Theorem for theBenchmark.p % 63.14/63.42 SZS output start Proof for theBenchmark.p % 63.14/63.42 Clause #13 (by assumption #[]): Eq % 63.14/63.42 (∀ (I1lo I1hi I2lo I2hi : Iota), % 63.14/63.42 Iff (axis_conflict I1lo I1hi I2lo I2hi) (Not (Exists fun X => And (in_closed X I1lo I1hi) (in_closed X I2lo I2hi)))) % 63.14/63.42 True % 63.14/63.42 Clause #35 (by assumption #[]): Eq (axis_conflict n0 n5 n10 n15) True % 63.14/63.42 Clause #36 (by assumption #[]): Eq (Not (Not (Exists fun X => And (in_closed X n0 n5) (in_closed X n10 n15)))) True % 63.14/63.42 Clause #385 (by clausification #[13]): ∀ (a : Iota), % 63.14/63.42 Eq % 63.14/63.42 (∀ (I1hi I2lo I2hi : Iota), % 63.14/63.42 Iff (axis_conflict a I1hi I2lo I2hi) (Not (Exists fun X => And (in_closed X a I1hi) (in_closed X I2lo I2hi)))) % 63.14/63.42 True % 63.14/63.42 Clause #386 (by clausification #[385]): ∀ (a a_1 : Iota), % 63.14/63.42 Eq % 63.14/63.42 (∀ (I2lo I2hi : Iota), % 63.14/63.42 Iff (axis_conflict a a_1 I2lo I2hi) (Not (Exists fun X => And (in_closed X a a_1) (in_closed X I2lo I2hi)))) % 63.14/63.42 True % 63.14/63.42 Clause #387 (by clausification #[386]): ∀ (a a_1 a_2 : Iota), % 63.14/63.42 Eq % 63.14/63.42 (∀ (I2hi : Iota), % 63.14/63.42 Iff (axis_conflict a a_1 a_2 I2hi) (Not (Exists fun X => And (in_closed X a a_1) (in_closed X a_2 I2hi)))) % 63.14/63.42 True % 63.14/63.42 Clause #388 (by clausification #[387]): ∀ (a a_1 a_2 a_3 : Iota), % 63.14/63.42 Eq (Iff (axis_conflict a a_1 a_2 a_3) (Not (Exists fun X => And (in_closed X a a_1) (in_closed X a_2 a_3)))) True % 63.14/63.42 Clause #390 (by clausification #[388]): ∀ (a a_1 a_2 a_3 : Iota), % 63.14/63.42 Or (Eq (axis_conflict a a_1 a_2 a_3) False) % 63.14/63.42 (Eq (Not (Exists fun X => And (in_closed X a a_1) (in_closed X a_2 a_3))) True) % 63.14/63.42 Clause #721 (by clausification #[36]): Eq (Not (Exists fun X => And (in_closed X n0 n5) (in_closed X n10 n15))) False % 63.14/63.42 Clause #722 (by clausification #[721]): Eq (Exists fun X => And (in_closed X n0 n5) (in_closed X n10 n15)) True % 63.14/63.42 Clause #723 (by clausification #[722]): ∀ (a : Iota), Eq (And (in_closed (skS.0 2 a) n0 n5) (in_closed (skS.0 2 a) n10 n15)) True % 63.14/63.42 Clause #724 (by clausification #[723]): ∀ (a : Iota), Eq (in_closed (skS.0 2 a) n10 n15) True % 63.14/63.42 Clause #725 (by clausification #[723]): ∀ (a : Iota), Eq (in_closed (skS.0 2 a) n0 n5) True % 63.14/63.42 Clause #8184 (by clausification #[390]): ∀ (a a_1 a_2 a_3 : Iota), % 63.14/63.42 Or (Eq (axis_conflict a a_1 a_2 a_3) False) (Eq (Exists fun X => And (in_closed X a a_1) (in_closed X a_2 a_3)) False) % 63.14/63.42 Clause #8185 (by clausification #[8184]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 63.14/63.42 Or (Eq (axis_conflict a a_1 a_2 a_3) False) (Eq (And (in_closed a_4 a a_1) (in_closed a_4 a_2 a_3)) False) % 63.14/63.42 Clause #8186 (by clausification #[8185]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 63.14/63.42 Or (Eq (axis_conflict a a_1 a_2 a_3) False) (Or (Eq (in_closed a_4 a a_1) False) (Eq (in_closed a_4 a_2 a_3) False)) % 63.14/63.42 Clause #8187 (by superposition #[8186, 35]): ∀ (a : Iota), Or (Eq (in_closed a n0 n5) False) (Or (Eq (in_closed a n10 n15) False) (Eq False True)) % 63.14/63.42 Clause #8868 (by clausification #[8187]): ∀ (a : Iota), Or (Eq (in_closed a n0 n5) False) (Eq (in_closed a n10 n15) False) % 63.14/63.42 Clause #8870 (by superposition #[8868, 725]): ∀ (a : Iota), Or (Eq (in_closed (skS.0 2 a) n10 n15) False) (Eq False True) % 63.14/63.42 Clause #8927 (by clausification #[8870]): ∀ (a : Iota), Eq (in_closed (skS.0 2 a) n10 n15) False % 63.14/63.42 Clause #8928 (by superposition #[8927, 724]): Eq False True % 63.14/63.42 Clause #8943 (by clausification #[8928]): False % 63.14/63.42 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------