%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KLE074+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:52:21 PM UTC 2025 % Result : Theorem 8.58s 8.77s % Output : Proof 8.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KLE074+1 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.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 16:35:08 EDT 2025 % 0.13/0.34 % CPUTime : % 8.58/8.77 SZS status Theorem for theBenchmark.p % 8.58/8.77 SZS output start Proof for theBenchmark.p % 8.58/8.77 Clause #4 (by assumption #[]): Eq (∀ (A B C : Iota), Eq (multiplication A (multiplication B C)) (multiplication (multiplication A B) C)) True % 8.58/8.77 Clause #13 (by assumption #[]): Eq (∀ (X0 X1 : Iota), Eq (domain (multiplication X0 X1)) (domain (multiplication X0 (domain X1)))) True % 8.58/8.77 Clause #17 (by assumption #[]): Eq % 8.58/8.77 (Not % 8.58/8.77 (∀ (X0 X1 X2 : Iota), % 8.58/8.77 Eq (domain (multiplication (multiplication X0 X1) (domain X2))) % 8.58/8.77 (domain (multiplication X0 (domain (multiplication X1 (domain X2))))))) % 8.58/8.77 True % 8.58/8.77 Clause #59 (by clausification #[4]): ∀ (a : Iota), % 8.58/8.77 Eq (∀ (B C : Iota), Eq (multiplication a (multiplication B C)) (multiplication (multiplication a B) C)) True % 8.58/8.77 Clause #60 (by clausification #[59]): ∀ (a a_1 : Iota), % 8.58/8.77 Eq (∀ (C : Iota), Eq (multiplication a (multiplication a_1 C)) (multiplication (multiplication a a_1) C)) True % 8.58/8.77 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 : Iota), % 8.58/8.77 Eq (Eq (multiplication a (multiplication a_1 a_2)) (multiplication (multiplication a a_1) a_2)) True % 8.58/8.77 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 : Iota), Eq (multiplication a (multiplication a_1 a_2)) (multiplication (multiplication a a_1) a_2) % 8.58/8.77 Clause #171 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (X1 : Iota), Eq (domain (multiplication a X1)) (domain (multiplication a (domain X1)))) True % 8.58/8.77 Clause #172 (by clausification #[171]): ∀ (a a_1 : Iota), Eq (Eq (domain (multiplication a a_1)) (domain (multiplication a (domain a_1)))) True % 8.58/8.77 Clause #173 (by clausification #[172]): ∀ (a a_1 : Iota), Eq (domain (multiplication a a_1)) (domain (multiplication a (domain a_1))) % 8.58/8.77 Clause #179 (by superposition #[173, 173]): ∀ (a a_1 a_2 : Iota), % 8.58/8.77 Eq (domain (multiplication a (multiplication a_1 (domain a_2)))) % 8.58/8.77 (domain (multiplication a (domain (multiplication a_1 a_2)))) % 8.58/8.77 Clause #210 (by clausification #[17]): Eq % 8.58/8.77 (∀ (X0 X1 X2 : Iota), % 8.58/8.77 Eq (domain (multiplication (multiplication X0 X1) (domain X2))) % 8.58/8.77 (domain (multiplication X0 (domain (multiplication X1 (domain X2)))))) % 8.58/8.77 False % 8.58/8.77 Clause #211 (by clausification #[210]): ∀ (a : Iota), % 8.58/8.77 Eq % 8.58/8.77 (Not % 8.58/8.77 (∀ (X1 X2 : Iota), % 8.58/8.77 Eq (domain (multiplication (multiplication (skS.0 0 a) X1) (domain X2))) % 8.58/8.77 (domain (multiplication (skS.0 0 a) (domain (multiplication X1 (domain X2))))))) % 8.58/8.77 True % 8.58/8.77 Clause #212 (by clausification #[211]): ∀ (a : Iota), % 8.58/8.77 Eq % 8.58/8.77 (∀ (X1 X2 : Iota), % 8.58/8.77 Eq (domain (multiplication (multiplication (skS.0 0 a) X1) (domain X2))) % 8.58/8.77 (domain (multiplication (skS.0 0 a) (domain (multiplication X1 (domain X2)))))) % 8.58/8.77 False % 8.58/8.77 Clause #213 (by clausification #[212]): ∀ (a a_1 : Iota), % 8.58/8.77 Eq % 8.58/8.77 (Not % 8.58/8.77 (∀ (X2 : Iota), % 8.58/8.77 Eq (domain (multiplication (multiplication (skS.0 0 a) (skS.0 1 a a_1)) (domain X2))) % 8.58/8.77 (domain (multiplication (skS.0 0 a) (domain (multiplication (skS.0 1 a a_1) (domain X2))))))) % 8.58/8.77 True % 8.58/8.77 Clause #214 (by clausification #[213]): ∀ (a a_1 : Iota), % 8.58/8.77 Eq % 8.58/8.77 (∀ (X2 : Iota), % 8.58/8.77 Eq (domain (multiplication (multiplication (skS.0 0 a) (skS.0 1 a a_1)) (domain X2))) % 8.58/8.77 (domain (multiplication (skS.0 0 a) (domain (multiplication (skS.0 1 a a_1) (domain X2)))))) % 8.58/8.77 False % 8.58/8.77 Clause #215 (by clausification #[214]): ∀ (a a_1 a_2 : Iota), % 8.58/8.77 Eq % 8.58/8.77 (Not % 8.58/8.77 (Eq (domain (multiplication (multiplication (skS.0 0 a) (skS.0 1 a a_1)) (domain (skS.0 2 a a_1 a_2)))) % 8.58/8.77 (domain (multiplication (skS.0 0 a) (domain (multiplication (skS.0 1 a a_1) (domain (skS.0 2 a a_1 a_2)))))))) % 8.58/8.77 True % 8.58/8.77 Clause #216 (by clausification #[215]): ∀ (a a_1 a_2 : Iota), % 8.58/8.77 Eq % 8.58/8.77 (Eq (domain (multiplication (multiplication (skS.0 0 a) (skS.0 1 a a_1)) (domain (skS.0 2 a a_1 a_2)))) % 8.58/8.77 (domain (multiplication (skS.0 0 a) (domain (multiplication (skS.0 1 a a_1) (domain (skS.0 2 a a_1 a_2))))))) % 8.58/8.77 False % 8.58/8.77 Clause #217 (by clausification #[216]): ∀ (a a_1 a_2 : Iota), % 8.58/8.77 Ne (domain (multiplication (multiplication (skS.0 0 a) (skS.0 1 a a_1)) (domain (skS.0 2 a a_1 a_2)))) % 8.58/8.77 (domain (multiplication (skS.0 0 a) (domain (multiplication (skS.0 1 a a_1) (domain (skS.0 2 a a_1 a_2)))))) % 8.61/8.79 Clause #218 (by forward demodulation #[217, 173]): ∀ (a a_1 a_2 : Iota), % 8.61/8.79 Ne (domain (multiplication (multiplication (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2))) % 8.61/8.79 (domain (multiplication (skS.0 0 a) (domain (multiplication (skS.0 1 a a_1) (domain (skS.0 2 a a_1 a_2)))))) % 8.61/8.79 Clause #219 (by forward demodulation #[218, 62]): ∀ (a a_1 a_2 : Iota), % 8.61/8.79 Ne (domain (multiplication (skS.0 0 a) (multiplication (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 8.61/8.79 (domain (multiplication (skS.0 0 a) (domain (multiplication (skS.0 1 a a_1) (domain (skS.0 2 a a_1 a_2)))))) % 8.61/8.79 Clause #220 (by forward demodulation #[219, 173]): ∀ (a a_1 a_2 : Iota), % 8.61/8.79 Ne (domain (multiplication (skS.0 0 a) (multiplication (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 8.61/8.79 (domain (multiplication (skS.0 0 a) (multiplication (skS.0 1 a a_1) (domain (skS.0 2 a a_1 a_2))))) % 8.61/8.79 Clause #3090 (by superposition #[179, 173]): ∀ (a a_1 a_2 : Iota), % 8.61/8.79 Eq (domain (multiplication a (multiplication a_1 a_2))) (domain (multiplication a (multiplication a_1 (domain a_2)))) % 8.61/8.79 Clause #3192 (by backward contextual literal cutting #[3090, 220]): False % 8.61/8.79 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------