%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT049+1 : TPTP v9.3.0. Released v2.4.0. % 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:20 AM UTC 2026 % Result : Theorem 26.87s 27.14s % Output : Proof 26.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT049+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : duper %s % 0.09/0.36 % Computer : n001.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 13:21:07 UTC 2026 % 0.09/0.36 % CPUTime : % 26.87/27.14 SZS status Theorem for theBenchmark.p % 26.87/27.14 SZS output start Proof for theBenchmark.p % 26.87/27.14 Clause #6 (by assumption #[]): Eq % 26.87/27.14 (∀ (X T0 T : Iota), % 26.87/27.14 organization X → % 26.87/27.14 And (greater (external_ties X T) (external_ties X T0) → greater (position X T) (position X T0)) % 26.87/27.14 (Eq (external_ties X T) (external_ties X T0) → Eq (position X T) (position X T0))) % 26.87/27.14 True % 26.87/27.14 Clause #7 (by assumption #[]): Eq (∀ (X T0 T : Iota), organization X → Eq (external_ties X T) (external_ties X T0)) True % 26.87/27.14 Clause #8 (by assumption #[]): Eq (Not (∀ (X T0 T : Iota), And (organization X) (greater (age X T) (age X T0)) → Eq (position X T) (position X T0))) % 26.87/27.14 True % 26.87/27.14 Clause #22 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (T0 T : Iota), organization a → Eq (external_ties a T) (external_ties a T0)) True % 26.87/27.14 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Eq (∀ (T : Iota), organization a → Eq (external_ties a T) (external_ties a a_1)) True % 26.87/27.14 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), Eq (organization a → Eq (external_ties a a_1) (external_ties a a_2)) True % 26.87/27.14 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a) False) (Eq (Eq (external_ties a a_1) (external_ties a a_2)) True) % 26.87/27.14 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a) False) (Eq (external_ties a a_1) (external_ties a a_2)) % 26.87/27.14 Clause #39 (by clausification #[8]): Eq (∀ (X T0 T : Iota), And (organization X) (greater (age X T) (age X T0)) → Eq (position X T) (position X T0)) False % 26.87/27.14 Clause #40 (by clausification #[39]): ∀ (a : Iota), % 26.87/27.14 Eq % 26.87/27.14 (Not % 26.87/27.14 (∀ (T0 T : Iota), % 26.87/27.14 And (organization (skS.0 0 a)) (greater (age (skS.0 0 a) T) (age (skS.0 0 a) T0)) → % 26.87/27.14 Eq (position (skS.0 0 a) T) (position (skS.0 0 a) T0))) % 26.87/27.14 True % 26.87/27.14 Clause #41 (by clausification #[40]): ∀ (a : Iota), % 26.87/27.14 Eq % 26.87/27.14 (∀ (T0 T : Iota), % 26.87/27.14 And (organization (skS.0 0 a)) (greater (age (skS.0 0 a) T) (age (skS.0 0 a) T0)) → % 26.87/27.14 Eq (position (skS.0 0 a) T) (position (skS.0 0 a) T0)) % 26.87/27.14 False % 26.87/27.14 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 26.87/27.14 Eq % 26.87/27.14 (Not % 26.87/27.14 (∀ (T : Iota), % 26.87/27.14 And (organization (skS.0 0 a)) (greater (age (skS.0 0 a) T) (age (skS.0 0 a) (skS.0 1 a a_1))) → % 26.87/27.14 Eq (position (skS.0 0 a) T) (position (skS.0 0 a) (skS.0 1 a a_1)))) % 26.87/27.14 True % 26.87/27.14 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), % 26.87/27.14 Eq % 26.87/27.14 (∀ (T : Iota), % 26.87/27.14 And (organization (skS.0 0 a)) (greater (age (skS.0 0 a) T) (age (skS.0 0 a) (skS.0 1 a a_1))) → % 26.87/27.14 Eq (position (skS.0 0 a) T) (position (skS.0 0 a) (skS.0 1 a a_1))) % 26.87/27.14 False % 26.87/27.14 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 26.87/27.14 Eq % 26.87/27.14 (Not % 26.87/27.14 (And (organization (skS.0 0 a)) % 26.87/27.14 (greater (age (skS.0 0 a) (skS.0 2 a a_1 a_2)) (age (skS.0 0 a) (skS.0 1 a a_1))) → % 26.87/27.14 Eq (position (skS.0 0 a) (skS.0 2 a a_1 a_2)) (position (skS.0 0 a) (skS.0 1 a a_1)))) % 26.87/27.14 True % 26.87/27.14 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 : Iota), % 26.87/27.14 Eq % 26.87/27.14 (And (organization (skS.0 0 a)) (greater (age (skS.0 0 a) (skS.0 2 a a_1 a_2)) (age (skS.0 0 a) (skS.0 1 a a_1))) → % 26.87/27.14 Eq (position (skS.0 0 a) (skS.0 2 a a_1 a_2)) (position (skS.0 0 a) (skS.0 1 a a_1))) % 26.87/27.14 False % 26.87/27.14 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), % 26.87/27.14 Eq (And (organization (skS.0 0 a)) (greater (age (skS.0 0 a) (skS.0 2 a a_1 a_2)) (age (skS.0 0 a) (skS.0 1 a a_1)))) % 26.87/27.14 True % 26.87/27.14 Clause #47 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), Eq (Eq (position (skS.0 0 a) (skS.0 2 a a_1 a_2)) (position (skS.0 0 a) (skS.0 1 a a_1))) False % 26.87/27.14 Clause #49 (by clausification #[46]): ∀ (a : Iota), Eq (organization (skS.0 0 a)) True % 26.87/27.14 Clause #100 (by clausification #[6]): ∀ (a : Iota), % 26.87/27.14 Eq % 26.87/27.14 (∀ (T0 T : Iota), % 26.87/27.14 organization a → % 26.87/27.14 And (greater (external_ties a T) (external_ties a T0) → greater (position a T) (position a T0)) % 26.87/27.14 (Eq (external_ties a T) (external_ties a T0) → Eq (position a T) (position a T0))) % 26.87/27.14 True % 26.87/27.14 Clause #101 (by clausification #[100]): ∀ (a a_1 : Iota), % 26.87/27.14 Eq % 26.87/27.14 (∀ (T : Iota), % 26.87/27.14 organization a → % 26.87/27.14 And (greater (external_ties a T) (external_ties a a_1) → greater (position a T) (position a a_1)) % 26.93/27.28 (Eq (external_ties a T) (external_ties a a_1) → Eq (position a T) (position a a_1))) % 26.93/27.28 True % 26.93/27.28 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), % 26.93/27.28 Eq % 26.93/27.28 (organization a → % 26.93/27.28 And (greater (external_ties a a_1) (external_ties a a_2) → greater (position a a_1) (position a a_2)) % 26.93/27.28 (Eq (external_ties a a_1) (external_ties a a_2) → Eq (position a a_1) (position a a_2))) % 26.93/27.28 True % 26.93/27.28 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 : Iota), % 26.93/27.28 Or (Eq (organization a) False) % 26.93/27.28 (Eq % 26.93/27.28 (And (greater (external_ties a a_1) (external_ties a a_2) → greater (position a a_1) (position a a_2)) % 26.93/27.28 (Eq (external_ties a a_1) (external_ties a a_2) → Eq (position a a_1) (position a a_2))) % 26.93/27.28 True) % 26.93/27.28 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 26.93/27.28 Or (Eq (organization a) False) % 26.93/27.28 (Eq (Eq (external_ties a a_1) (external_ties a a_2) → Eq (position a a_1) (position a a_2)) True) % 26.93/27.28 Clause #106 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 26.93/27.28 Or (Eq (organization a) False) % 26.93/27.28 (Or (Eq (Eq (external_ties a a_1) (external_ties a a_2)) False) (Eq (Eq (position a a_1) (position a a_2)) True)) % 26.93/27.28 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 26.93/27.28 Or (Eq (organization a) False) % 26.93/27.28 (Or (Eq (Eq (position a a_1) (position a a_2)) True) (Ne (external_ties a a_1) (external_ties a a_2))) % 26.93/27.28 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 26.93/27.28 Or (Eq (organization a) False) % 26.93/27.28 (Or (Ne (external_ties a a_1) (external_ties a a_2)) (Eq (position a a_1) (position a a_2))) % 26.93/27.28 Clause #109 (by forward contextual literal cutting #[108, 26]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a) False) (Eq (position a a_1) (position a a_2)) % 26.93/27.28 Clause #110 (by superposition #[109, 49]): ∀ (a a_1 a_2 : Iota), Or (Eq (position (skS.0 0 a) a_1) (position (skS.0 0 a) a_2)) (Eq False True) % 26.93/27.28 Clause #153 (by clausification #[47]): ∀ (a a_1 a_2 : Iota), Ne (position (skS.0 0 a) (skS.0 2 a a_1 a_2)) (position (skS.0 0 a) (skS.0 1 a a_1)) % 26.93/27.28 Clause #8253 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), Eq (position (skS.0 0 a) a_1) (position (skS.0 0 a) a_2) % 26.93/27.28 Clause #8254 (by backward contextual literal cutting #[8253, 153]): False % 26.93/27.28 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------