%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET968+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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 08:00:45 PM UTC 2025 % Result : Theorem 16.17s 16.43s % Output : Proof 16.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.14 % Problem : SET968+1 : TPTP v9.2.0. Released v3.2.0. % 0.03/0.15 % Command : duper %s % 0.13/0.37 % Computer : n016.cluster.edu % 0.13/0.37 % Model : x86_64 x86_64 % 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.37 % Memory : 8042.1875MB % 0.13/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.37 % CPULimit : 300 % 0.13/0.37 % WCLimit : 300 % 0.13/0.37 % DateTime : Thu Oct 2 14:39:23 EDT 2025 % 0.13/0.37 % CPUTime : % 16.17/16.43 SZS status Theorem for theBenchmark.p % 16.17/16.43 SZS output start Proof for theBenchmark.p % 16.17/16.43 Clause #0 (by assumption #[]): Eq (∀ (A B : Iota), Eq (set_union2 A B) (set_union2 B A)) True % 16.17/16.43 Clause #6 (by assumption #[]): Eq % 16.17/16.43 (∀ (A B C : Iota), % 16.17/16.43 And (Eq (cartesian_product2 (set_union2 A B) C) (set_union2 (cartesian_product2 A C) (cartesian_product2 B C))) % 16.17/16.43 (Eq (cartesian_product2 C (set_union2 A B)) (set_union2 (cartesian_product2 C A) (cartesian_product2 C B)))) % 16.17/16.43 True % 16.17/16.43 Clause #7 (by assumption #[]): Eq % 16.17/16.43 (Not % 16.17/16.43 (∀ (A B C D : Iota), % 16.17/16.43 Eq (cartesian_product2 (set_union2 A B) (set_union2 C D)) % 16.17/16.43 (set_union2 (set_union2 (set_union2 (cartesian_product2 A C) (cartesian_product2 A D)) (cartesian_product2 B C)) % 16.17/16.43 (cartesian_product2 B D)))) % 16.17/16.43 True % 16.17/16.43 Clause #8 (by assumption #[]): Eq (∀ (A B C : Iota), Eq (set_union2 (set_union2 A B) C) (set_union2 A (set_union2 B C))) True % 16.17/16.43 Clause #22 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B : Iota), Eq (set_union2 a B) (set_union2 B a)) True % 16.17/16.43 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Eq (Eq (set_union2 a a_1) (set_union2 a_1 a)) True % 16.17/16.43 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Eq (set_union2 a a_1) (set_union2 a_1 a) % 16.17/16.43 Clause #30 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (B C : Iota), Eq (set_union2 (set_union2 a B) C) (set_union2 a (set_union2 B C))) True % 16.17/16.43 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), Eq (set_union2 (set_union2 a a_1) C) (set_union2 a (set_union2 a_1 C))) True % 16.17/16.43 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), Eq (Eq (set_union2 (set_union2 a a_1) a_2) (set_union2 a (set_union2 a_1 a_2))) True % 16.17/16.43 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), Eq (set_union2 (set_union2 a a_1) a_2) (set_union2 a (set_union2 a_1 a_2)) % 16.17/16.43 Clause #41 (by superposition #[33, 24]): ∀ (a a_1 a_2 : Iota), Eq (set_union2 (set_union2 a a_1) a_2) (set_union2 a_1 (set_union2 a a_2)) % 16.17/16.43 Clause #48 (by clausification #[6]): ∀ (a : Iota), % 16.17/16.43 Eq % 16.17/16.43 (∀ (B C : Iota), % 16.17/16.43 And (Eq (cartesian_product2 (set_union2 a B) C) (set_union2 (cartesian_product2 a C) (cartesian_product2 B C))) % 16.17/16.43 (Eq (cartesian_product2 C (set_union2 a B)) (set_union2 (cartesian_product2 C a) (cartesian_product2 C B)))) % 16.17/16.43 True % 16.17/16.43 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), % 16.17/16.43 Eq % 16.17/16.43 (∀ (C : Iota), % 16.17/16.43 And % 16.17/16.43 (Eq (cartesian_product2 (set_union2 a a_1) C) (set_union2 (cartesian_product2 a C) (cartesian_product2 a_1 C))) % 16.17/16.43 (Eq (cartesian_product2 C (set_union2 a a_1)) (set_union2 (cartesian_product2 C a) (cartesian_product2 C a_1)))) % 16.17/16.43 True % 16.17/16.43 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 : Iota), % 16.17/16.43 Eq % 16.17/16.43 (And % 16.17/16.43 (Eq (cartesian_product2 (set_union2 a a_1) a_2) % 16.17/16.43 (set_union2 (cartesian_product2 a a_2) (cartesian_product2 a_1 a_2))) % 16.17/16.43 (Eq (cartesian_product2 a_2 (set_union2 a a_1)) % 16.17/16.43 (set_union2 (cartesian_product2 a_2 a) (cartesian_product2 a_2 a_1)))) % 16.17/16.43 True % 16.17/16.43 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), % 16.17/16.43 Eq (Eq (cartesian_product2 a (set_union2 a_1 a_2)) (set_union2 (cartesian_product2 a a_1) (cartesian_product2 a a_2))) % 16.17/16.43 True % 16.17/16.43 Clause #52 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), % 16.17/16.43 Eq % 16.17/16.43 (Eq (cartesian_product2 (set_union2 a a_1) a_2) % 16.17/16.43 (set_union2 (cartesian_product2 a a_2) (cartesian_product2 a_1 a_2))) % 16.17/16.43 True % 16.17/16.43 Clause #53 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 16.17/16.43 Eq (cartesian_product2 a (set_union2 a_1 a_2)) (set_union2 (cartesian_product2 a a_1) (cartesian_product2 a a_2)) % 16.17/16.43 Clause #59 (by superposition #[53, 33]): ∀ (a a_1 a_2 a_3 : Iota), % 16.17/16.43 Eq (set_union2 (cartesian_product2 a (set_union2 a_1 a_2)) a_3) % 16.17/16.43 (set_union2 (cartesian_product2 a a_1) (set_union2 (cartesian_product2 a a_2) a_3)) % 16.17/16.43 Clause #68 (by superposition #[41, 33]): ∀ (a a_1 a_2 : Iota), Eq (set_union2 a (set_union2 a_1 a_2)) (set_union2 a_1 (set_union2 a a_2)) % 16.17/16.43 Clause #70 (by superposition #[41, 24]): ∀ (a a_1 a_2 : Iota), Eq (set_union2 a (set_union2 a_1 a_2)) (set_union2 a_2 (set_union2 a_1 a)) % 16.17/16.43 Clause #116 (by clausification #[7]): Eq % 16.17/16.43 (∀ (A B C D : Iota), % 16.27/16.45 Eq (cartesian_product2 (set_union2 A B) (set_union2 C D)) % 16.27/16.45 (set_union2 (set_union2 (set_union2 (cartesian_product2 A C) (cartesian_product2 A D)) (cartesian_product2 B C)) % 16.27/16.45 (cartesian_product2 B D))) % 16.27/16.45 False % 16.27/16.45 Clause #117 (by clausification #[116]): ∀ (a : Iota), % 16.27/16.45 Eq % 16.27/16.45 (Not % 16.27/16.45 (∀ (B C D : Iota), % 16.27/16.45 Eq (cartesian_product2 (set_union2 (skS.0 2 a) B) (set_union2 C D)) % 16.27/16.45 (set_union2 % 16.27/16.45 (set_union2 (set_union2 (cartesian_product2 (skS.0 2 a) C) (cartesian_product2 (skS.0 2 a) D)) % 16.27/16.45 (cartesian_product2 B C)) % 16.27/16.45 (cartesian_product2 B D)))) % 16.27/16.45 True % 16.27/16.45 Clause #118 (by clausification #[117]): ∀ (a : Iota), % 16.27/16.45 Eq % 16.27/16.45 (∀ (B C D : Iota), % 16.27/16.45 Eq (cartesian_product2 (set_union2 (skS.0 2 a) B) (set_union2 C D)) % 16.27/16.45 (set_union2 % 16.27/16.45 (set_union2 (set_union2 (cartesian_product2 (skS.0 2 a) C) (cartesian_product2 (skS.0 2 a) D)) % 16.27/16.45 (cartesian_product2 B C)) % 16.27/16.45 (cartesian_product2 B D))) % 16.27/16.45 False % 16.27/16.45 Clause #119 (by clausification #[118]): ∀ (a a_1 : Iota), % 16.27/16.46 Eq % 16.27/16.46 (Not % 16.27/16.46 (∀ (C D : Iota), % 16.27/16.46 Eq (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) (set_union2 C D)) % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 (set_union2 (cartesian_product2 (skS.0 2 a) C) (cartesian_product2 (skS.0 2 a) D)) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) C)) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) D)))) % 16.27/16.46 True % 16.27/16.46 Clause #120 (by clausification #[119]): ∀ (a a_1 : Iota), % 16.27/16.46 Eq % 16.27/16.46 (∀ (C D : Iota), % 16.27/16.46 Eq (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) (set_union2 C D)) % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 (set_union2 (cartesian_product2 (skS.0 2 a) C) (cartesian_product2 (skS.0 2 a) D)) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) C)) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) D))) % 16.27/16.46 False % 16.27/16.46 Clause #121 (by clausification #[120]): ∀ (a a_1 a_2 : Iota), % 16.27/16.46 Eq % 16.27/16.46 (Not % 16.27/16.46 (∀ (D : Iota), % 16.27/16.46 Eq (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) (set_union2 (skS.0 4 a a_1 a_2) D)) % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 (cartesian_product2 (skS.0 2 a) (skS.0 4 a a_1 a_2)) (cartesian_product2 (skS.0 2 a) D)) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) D)))) % 16.27/16.46 True % 16.27/16.46 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), % 16.27/16.46 Eq % 16.27/16.46 (∀ (D : Iota), % 16.27/16.46 Eq (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) (set_union2 (skS.0 4 a a_1 a_2) D)) % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 (cartesian_product2 (skS.0 2 a) (skS.0 4 a a_1 a_2)) (cartesian_product2 (skS.0 2 a) D)) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) D))) % 16.27/16.46 False % 16.27/16.46 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 a_3 : Iota), % 16.27/16.46 Eq % 16.27/16.46 (Not % 16.27/16.46 (Eq % 16.27/16.46 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.27/16.46 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 (cartesian_product2 (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 16.27/16.46 (cartesian_product2 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3))))) % 16.27/16.46 True % 16.27/16.46 Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 a_3 : Iota), % 16.27/16.46 Eq % 16.27/16.46 (Eq % 16.27/16.46 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.27/16.46 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 % 16.27/16.46 (set_union2 (cartesian_product2 (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 16.27/16.46 (cartesian_product2 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 16.27/16.46 (cartesian_product2 (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))) % 16.27/16.46 False % 16.27/16.46 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 a_3 : Iota), % 16.27/16.46 Ne % 16.27/16.46 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.27/16.46 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (set_union2 % 16.31/16.51 (set_union2 % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 16.31/16.51 (cartesian_product2 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 16.31/16.51 (cartesian_product2 (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 Clause #126 (by forward demodulation #[125, 33]): ∀ (a a_1 a_2 a_3 : Iota), % 16.31/16.51 Ne % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (set_union2 % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 16.31/16.51 (cartesian_product2 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 16.31/16.51 (cartesian_product2 (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))) % 16.31/16.51 Clause #127 (by forward demodulation #[126, 70]): ∀ (a a_1 a_2 a_3 : Iota), % 16.31/16.51 Ne % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 16.31/16.51 (cartesian_product2 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))))) % 16.31/16.51 Clause #128 (by forward demodulation #[127, 53]): ∀ (a a_1 a_2 a_3 : Iota), % 16.31/16.51 Ne % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 16.31/16.51 (cartesian_product2 (skS.0 2 a) (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))))) % 16.31/16.51 Clause #375 (by superposition #[68, 128]): ∀ (a a_1 a_2 a_3 : Iota), % 16.31/16.51 Ne % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)) % 16.31/16.51 (cartesian_product2 (skS.0 2 a) (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))))) % 16.31/16.51 Clause #617 (by clausification #[52]): ∀ (a a_1 a_2 : Iota), % 16.31/16.51 Eq (cartesian_product2 (set_union2 a a_1) a_2) (set_union2 (cartesian_product2 a a_2) (cartesian_product2 a_1 a_2)) % 16.31/16.51 Clause #8295 (by forward demodulation #[375, 59]): ∀ (a a_1 a_2 a_3 : Iota), % 16.31/16.51 Ne % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (set_union2 (cartesian_product2 (skS.0 3 a a_1) (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (cartesian_product2 (skS.0 2 a) (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3)))) % 16.31/16.51 Clause #8296 (by forward demodulation #[8295, 617]): ∀ (a a_1 a_2 a_3 : Iota), % 16.31/16.51 Ne % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 3 a a_1) (skS.0 2 a)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 Clause #8297 (by forward demodulation #[8296, 24]): ∀ (a a_1 a_2 a_3 : Iota), % 16.31/16.51 Ne % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 (cartesian_product2 (set_union2 (skS.0 2 a) (skS.0 3 a a_1)) % 16.31/16.51 (set_union2 (skS.0 4 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3))) % 16.31/16.51 Clause #8298 (by eliminate resolved literals #[8297]): False % 16.31/16.51 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------