%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT052+1 : TPTP v9.3.0. Released v2.4.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:20 AM UTC 2026 % Result : Theorem 32.25s 32.59s % Output : Proof 32.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT052+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.05 % Command : duper %s % 0.11/0.36 % Computer : n015.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % 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 13:23:45 UTC 2026 % 0.11/0.37 % CPUTime : % 32.25/32.59 SZS status Theorem for theBenchmark.p % 32.25/32.59 SZS output start Proof for theBenchmark.p % 32.25/32.59 Clause #6 (by assumption #[]): Eq (∀ (X T0 T : Iota), Iff (dissimilar X T0 T) (And (organization X) (Not (Iff (is_aligned X T0) (is_aligned X T))))) % 32.25/32.59 True % 32.25/32.59 Clause #7 (by assumption #[]): Eq (Not (∀ (X T : Iota), Not (dissimilar X T T))) True % 32.25/32.59 Clause #13 (by clausification #[7]): Eq (∀ (X T : Iota), Not (dissimilar X T T)) False % 32.25/32.59 Clause #14 (by clausification #[13]): ∀ (a : Iota), Eq (Not (∀ (T : Iota), Not (dissimilar (skS.0 0 a) T T))) True % 32.25/32.59 Clause #15 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (T : Iota), Not (dissimilar (skS.0 0 a) T T)) False % 32.25/32.59 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), Eq (Not (Not (dissimilar (skS.0 0 a) (skS.0 1 a a_1) (skS.0 1 a a_1)))) True % 32.25/32.59 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), Eq (Not (dissimilar (skS.0 0 a) (skS.0 1 a a_1) (skS.0 1 a a_1))) False % 32.25/32.59 Clause #18 (by clausification #[17]): ∀ (a a_1 : Iota), Eq (dissimilar (skS.0 0 a) (skS.0 1 a a_1) (skS.0 1 a a_1)) True % 32.25/32.59 Clause #87 (by clausification #[6]): ∀ (a : Iota), % 32.25/32.59 Eq (∀ (T0 T : Iota), Iff (dissimilar a T0 T) (And (organization a) (Not (Iff (is_aligned a T0) (is_aligned a T))))) % 32.25/32.59 True % 32.25/32.59 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), % 32.25/32.59 Eq (∀ (T : Iota), Iff (dissimilar a a_1 T) (And (organization a) (Not (Iff (is_aligned a a_1) (is_aligned a T))))) % 32.25/32.59 True % 32.25/32.59 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 : Iota), % 32.25/32.59 Eq (Iff (dissimilar a a_1 a_2) (And (organization a) (Not (Iff (is_aligned a a_1) (is_aligned a a_2))))) True % 32.25/32.59 Clause #91 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 32.25/32.59 Or (Eq (dissimilar a a_1 a_2) False) % 32.25/32.59 (Eq (And (organization a) (Not (Iff (is_aligned a a_1) (is_aligned a a_2)))) True) % 32.25/32.59 Clause #122 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), Or (Eq (dissimilar a a_1 a_2) False) (Eq (Not (Iff (is_aligned a a_1) (is_aligned a a_2))) True) % 32.25/32.59 Clause #124 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), Or (Eq (dissimilar a a_1 a_2) False) (Eq (Iff (is_aligned a a_1) (is_aligned a a_2)) False) % 32.25/32.59 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 32.25/32.59 Or (Eq (dissimilar a a_1 a_2) False) (Or (Eq (is_aligned a a_1) False) (Eq (is_aligned a a_2) False)) % 32.25/32.59 Clause #126 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 32.25/32.59 Or (Eq (dissimilar a a_1 a_2) False) (Or (Eq (is_aligned a a_1) True) (Eq (is_aligned a a_2) True)) % 32.25/32.59 Clause #127 (by superposition #[125, 18]): ∀ (a a_1 : Iota), % 32.25/32.59 Or (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) False) % 32.25/32.59 (Or (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq False True)) % 32.25/32.59 Clause #142 (by superposition #[126, 18]): ∀ (a a_1 : Iota), % 32.25/32.59 Or (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) True) % 32.25/32.59 (Or (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq False True)) % 32.25/32.59 Clause #2990 (by clausification #[127]): ∀ (a a_1 : Iota), % 32.25/32.59 Or (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) False) % 32.25/32.59 Clause #2991 (by eliminate duplicate literals #[2990]): ∀ (a a_1 : Iota), Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) False % 32.25/32.60 Clause #5408 (by clausification #[142]): ∀ (a a_1 : Iota), % 32.25/32.60 Or (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) True) % 32.25/32.60 Clause #5409 (by eliminate duplicate literals #[5408]): ∀ (a a_1 : Iota), Eq (is_aligned (skS.0 0 a) (skS.0 1 a a_1)) True % 32.25/32.60 Clause #5410 (by superposition #[5409, 2991]): Eq True False % 32.25/32.60 Clause #5598 (by clausification #[5410]): False % 32.25/32.60 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------