%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT094+1 : TPTP v9.3.1. Bugfixed v9.3.1. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n004.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:24 AM UTC 2026 % Result : Theorem 12.66s 12.94s % Output : Proof 12.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT094+1 : TPTP v9.3.1. Bugfixed v9.3.1. % 0.00/0.04 % Command : duper %s % 0.11/0.37 % Computer : n004.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Mon Sep 7 14:25:00 UTC 2026 % 0.11/0.37 % CPUTime : % 12.66/12.94 SZS status Theorem for theBenchmark.p % 12.66/12.94 SZS output start Proof for theBenchmark.p % 12.66/12.94 Clause #35 (by assumption #[]): Eq (∀ (L1 H1 L2 H2 : Iota), Not (axis_subsumes L1 H1 L2 H2) → Eq (subs_verdict L1 H1 present L2 H2 present) conflict) % 12.66/12.94 True % 12.66/12.94 Clause #78 (by assumption #[]): Eq (Not (axis_subsumes v0 v800 v0 v600)) True % 12.66/12.94 Clause #79 (by assumption #[]): Eq (Not (Eq (subs_verdict v0 v800 present v0 v600 present) conflict)) True % 12.66/12.94 Clause #745 (by clausification #[78]): Eq (axis_subsumes v0 v800 v0 v600) False % 12.66/12.94 Clause #1104 (by clausification #[35]): ∀ (a : Iota), % 12.66/12.94 Eq (∀ (H1 L2 H2 : Iota), Not (axis_subsumes a H1 L2 H2) → Eq (subs_verdict a H1 present L2 H2 present) conflict) True % 12.66/12.94 Clause #1105 (by clausification #[1104]): ∀ (a a_1 : Iota), % 12.66/12.94 Eq (∀ (L2 H2 : Iota), Not (axis_subsumes a a_1 L2 H2) → Eq (subs_verdict a a_1 present L2 H2 present) conflict) True % 12.66/12.94 Clause #1106 (by clausification #[1105]): ∀ (a a_1 a_2 : Iota), % 12.66/12.94 Eq (∀ (H2 : Iota), Not (axis_subsumes a a_1 a_2 H2) → Eq (subs_verdict a a_1 present a_2 H2 present) conflict) True % 12.66/12.94 Clause #1107 (by clausification #[1106]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.94 Eq (Not (axis_subsumes a a_1 a_2 a_3) → Eq (subs_verdict a a_1 present a_2 a_3 present) conflict) True % 12.66/12.94 Clause #1108 (by clausification #[1107]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.94 Or (Eq (Not (axis_subsumes a a_1 a_2 a_3)) False) (Eq (Eq (subs_verdict a a_1 present a_2 a_3 present) conflict) True) % 12.66/12.94 Clause #1109 (by clausification #[1108]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.94 Or (Eq (Eq (subs_verdict a a_1 present a_2 a_3 present) conflict) True) (Eq (axis_subsumes a a_1 a_2 a_3) True) % 12.66/12.94 Clause #1110 (by clausification #[1109]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.94 Or (Eq (axis_subsumes a a_1 a_2 a_3) True) (Eq (subs_verdict a a_1 present a_2 a_3 present) conflict) % 12.66/12.94 Clause #1287 (by clausification #[79]): Eq (Eq (subs_verdict v0 v800 present v0 v600 present) conflict) False % 12.66/12.94 Clause #1288 (by clausification #[1287]): Ne (subs_verdict v0 v800 present v0 v600 present) conflict % 12.66/12.94 Clause #1289 (by superposition #[1288, 1110]): Or (Eq (axis_subsumes v0 v800 v0 v600) True) (Ne conflict conflict) % 12.66/12.94 Clause #1300 (by eliminate resolved literals #[1289]): Eq (axis_subsumes v0 v800 v0 v600) True % 12.66/12.94 Clause #1301 (by superposition #[1300, 745]): Eq True False % 12.66/12.94 Clause #1309 (by clausification #[1301]): False % 12.66/12.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------