%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : REL049+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:58:43 PM UTC 2025 % Result : Theorem 17.05s 17.19s % Output : Proof 17.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : REL049+1 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n005.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 12:03:08 EDT 2025 % 0.13/0.34 % CPUTime : % 17.05/17.19 SZS status Theorem for theBenchmark.p % 17.05/17.19 SZS output start Proof for theBenchmark.p % 17.05/17.19 Clause #1 (by assumption #[]): Eq (∀ (X0 X1 X2 : Iota), Eq (join X0 (join X1 X2)) (join (join X0 X1) X2)) True % 17.05/17.19 Clause #13 (by assumption #[]): Eq (Not (∀ (X0 X1 X2 : Iota), And (Eq (join X0 X1) X1) (Eq (join X2 X1) X1) → Eq (join (join X0 X2) X1) X1)) True % 17.05/17.19 Clause #25 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (X1 X2 : Iota), Eq (join a (join X1 X2)) (join (join a X1) X2)) True % 17.05/17.19 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), Eq (∀ (X2 : Iota), Eq (join a (join a_1 X2)) (join (join a a_1) X2)) True % 17.05/17.19 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Eq (Eq (join a (join a_1 a_2)) (join (join a a_1) a_2)) True % 17.05/17.19 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), Eq (join a (join a_1 a_2)) (join (join a a_1) a_2) % 17.05/17.19 Clause #240 (by clausification #[13]): Eq (∀ (X0 X1 X2 : Iota), And (Eq (join X0 X1) X1) (Eq (join X2 X1) X1) → Eq (join (join X0 X2) X1) X1) False % 17.05/17.19 Clause #241 (by clausification #[240]): ∀ (a : Iota), % 17.05/17.19 Eq % 17.05/17.19 (Not % 17.05/17.19 (∀ (X1 X2 : Iota), % 17.05/17.19 And (Eq (join (skS.0 0 a) X1) X1) (Eq (join X2 X1) X1) → Eq (join (join (skS.0 0 a) X2) X1) X1)) % 17.05/17.19 True % 17.05/17.19 Clause #242 (by clausification #[241]): ∀ (a : Iota), % 17.05/17.19 Eq (∀ (X1 X2 : Iota), And (Eq (join (skS.0 0 a) X1) X1) (Eq (join X2 X1) X1) → Eq (join (join (skS.0 0 a) X2) X1) X1) % 17.05/17.19 False % 17.05/17.19 Clause #243 (by clausification #[242]): ∀ (a a_1 : Iota), % 17.05/17.19 Eq % 17.05/17.19 (Not % 17.05/17.19 (∀ (X2 : Iota), % 17.05/17.19 And (Eq (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (Eq (join X2 (skS.0 1 a a_1)) (skS.0 1 a a_1)) → % 17.05/17.19 Eq (join (join (skS.0 0 a) X2) (skS.0 1 a a_1)) (skS.0 1 a a_1))) % 17.05/17.19 True % 17.05/17.19 Clause #244 (by clausification #[243]): ∀ (a a_1 : Iota), % 17.05/17.19 Eq % 17.05/17.19 (∀ (X2 : Iota), % 17.05/17.19 And (Eq (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (Eq (join X2 (skS.0 1 a a_1)) (skS.0 1 a a_1)) → % 17.05/17.19 Eq (join (join (skS.0 0 a) X2) (skS.0 1 a a_1)) (skS.0 1 a a_1)) % 17.05/17.19 False % 17.05/17.19 Clause #245 (by clausification #[244]): ∀ (a a_1 a_2 : Iota), % 17.05/17.19 Eq % 17.05/17.19 (Not % 17.05/17.19 (And (Eq (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) % 17.05/17.19 (Eq (join (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) (skS.0 1 a a_1)) → % 17.05/17.19 Eq (join (join (skS.0 0 a) (skS.0 2 a a_1 a_2)) (skS.0 1 a a_1)) (skS.0 1 a a_1))) % 17.05/17.19 True % 17.05/17.19 Clause #246 (by clausification #[245]): ∀ (a a_1 a_2 : Iota), % 17.05/17.19 Eq % 17.05/17.19 (And (Eq (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) % 17.05/17.19 (Eq (join (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) (skS.0 1 a a_1)) → % 17.05/17.19 Eq (join (join (skS.0 0 a) (skS.0 2 a a_1 a_2)) (skS.0 1 a a_1)) (skS.0 1 a a_1)) % 17.05/17.19 False % 17.05/17.19 Clause #247 (by clausification #[246]): ∀ (a a_1 a_2 : Iota), % 17.05/17.19 Eq % 17.05/17.19 (And (Eq (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) % 17.05/17.19 (Eq (join (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) (skS.0 1 a a_1))) % 17.05/17.19 True % 17.05/17.19 Clause #248 (by clausification #[246]): ∀ (a a_1 a_2 : Iota), Eq (Eq (join (join (skS.0 0 a) (skS.0 2 a a_1 a_2)) (skS.0 1 a a_1)) (skS.0 1 a a_1)) False % 17.05/17.19 Clause #249 (by clausification #[247]): ∀ (a a_1 a_2 : Iota), Eq (Eq (join (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) (skS.0 1 a a_1)) True % 17.05/17.19 Clause #250 (by clausification #[247]): ∀ (a a_1 : Iota), Eq (Eq (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) True % 17.05/17.19 Clause #251 (by clausification #[249]): ∀ (a a_1 a_2 : Iota), Eq (join (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) (skS.0 1 a a_1) % 17.05/17.19 Clause #6758 (by clausification #[248]): ∀ (a a_1 a_2 : Iota), Ne (join (join (skS.0 0 a) (skS.0 2 a a_1 a_2)) (skS.0 1 a a_1)) (skS.0 1 a a_1) % 17.05/17.19 Clause #6759 (by forward demodulation #[6758, 28]): ∀ (a a_1 a_2 : Iota), Ne (join (skS.0 0 a) (join (skS.0 2 a a_1 a_2) (skS.0 1 a a_1))) (skS.0 1 a a_1) % 17.05/17.19 Clause #6760 (by forward demodulation #[6759, 251]): ∀ (a a_1 : Iota), Ne (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1) % 17.05/17.19 Clause #6818 (by clausification #[250]): ∀ (a a_1 : Iota), Eq (join (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1) % 17.05/17.19 Clause #6819 (by forward contextual literal cutting #[6818, 6760]): False % 17.05/17.19 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------