%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEV045^5 : TPTP v9.2.0. Released v4.0.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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:02:46 PM UTC 2025 % Result : Theorem 4.37s 4.54s % Output : Proof 4.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEV045^5 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.14/0.35 % Computer : n001.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 01:49:08 EDT 2025 % 0.14/0.35 % CPUTime : % 4.37/4.54 SZS status Theorem for theBenchmark.p % 4.37/4.54 SZS output start Proof for theBenchmark.p % 4.37/4.54 Clause #0 (by assumption #[]): Eq % 4.37/4.54 (Not % 4.37/4.54 ((∀ (Xx : a), cP Xx Xx → cQ Xx (f Xx) (g Xx)) → % 4.37/4.54 (∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (f Xy)) → % 4.37/4.54 And (∀ (Xx Xy : a), cP Xx Xy → cP Xy Xx) (∀ (Xx Xy Xz : a), And (cP Xx Xy) (cP Xy Xz) → cP Xx Xz) → % 4.37/4.54 And % 4.37/4.54 (∀ (Xx : a), % 4.37/4.54 cP Xx Xx → % 4.37/4.54 And (∀ (Xx0 Xy : b), cQ Xx Xx0 Xy → cQ Xx Xy Xx0) % 4.37/4.54 (∀ (Xx0 Xy Xz : b), And (cQ Xx Xx0 Xy) (cQ Xx Xy Xz) → cQ Xx Xx0 Xz)) % 4.37/4.54 (∀ (Xx Xy : a), cP Xx Xy → Eq (cQ Xx) (cQ Xy)) → % 4.37/4.54 ∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (g Xy))) % 4.37/4.54 True % 4.37/4.54 Clause #1 (by clausification #[0]): Eq % 4.37/4.54 ((∀ (Xx : a), cP Xx Xx → cQ Xx (f Xx) (g Xx)) → % 4.37/4.54 (∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (f Xy)) → % 4.37/4.54 And (∀ (Xx Xy : a), cP Xx Xy → cP Xy Xx) (∀ (Xx Xy Xz : a), And (cP Xx Xy) (cP Xy Xz) → cP Xx Xz) → % 4.37/4.54 And % 4.37/4.54 (∀ (Xx : a), % 4.37/4.54 cP Xx Xx → % 4.37/4.54 And (∀ (Xx0 Xy : b), cQ Xx Xx0 Xy → cQ Xx Xy Xx0) % 4.37/4.54 (∀ (Xx0 Xy Xz : b), And (cQ Xx Xx0 Xy) (cQ Xx Xy Xz) → cQ Xx Xx0 Xz)) % 4.37/4.54 (∀ (Xx Xy : a), cP Xx Xy → Eq (cQ Xx) (cQ Xy)) → % 4.37/4.54 ∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (g Xy)) % 4.37/4.54 False % 4.37/4.54 Clause #2 (by clausification #[1]): Eq (∀ (Xx : a), cP Xx Xx → cQ Xx (f Xx) (g Xx)) True % 4.37/4.54 Clause #3 (by clausification #[1]): Eq % 4.37/4.54 ((∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (f Xy)) → % 4.37/4.54 And (∀ (Xx Xy : a), cP Xx Xy → cP Xy Xx) (∀ (Xx Xy Xz : a), And (cP Xx Xy) (cP Xy Xz) → cP Xx Xz) → % 4.37/4.54 And % 4.37/4.54 (∀ (Xx : a), % 4.37/4.54 cP Xx Xx → % 4.37/4.54 And (∀ (Xx0 Xy : b), cQ Xx Xx0 Xy → cQ Xx Xy Xx0) % 4.37/4.54 (∀ (Xx0 Xy Xz : b), And (cQ Xx Xx0 Xy) (cQ Xx Xy Xz) → cQ Xx Xx0 Xz)) % 4.37/4.54 (∀ (Xx Xy : a), cP Xx Xy → Eq (cQ Xx) (cQ Xy)) → % 4.37/4.54 ∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (g Xy)) % 4.37/4.54 False % 4.37/4.54 Clause #4 (by clausification #[2]): ∀ (a : a), Eq (cP a a → cQ a (f a) (g a)) True % 4.37/4.54 Clause #5 (by clausification #[4]): ∀ (a : a), Or (Eq (cP a a) False) (Eq (cQ a (f a) (g a)) True) % 4.37/4.54 Clause #6 (by clausification #[3]): Eq (∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (f Xy)) True % 4.37/4.54 Clause #7 (by clausification #[3]): Eq % 4.37/4.54 (And (∀ (Xx Xy : a), cP Xx Xy → cP Xy Xx) (∀ (Xx Xy Xz : a), And (cP Xx Xy) (cP Xy Xz) → cP Xx Xz) → % 4.37/4.54 And % 4.37/4.54 (∀ (Xx : a), % 4.37/4.54 cP Xx Xx → % 4.37/4.54 And (∀ (Xx0 Xy : b), cQ Xx Xx0 Xy → cQ Xx Xy Xx0) % 4.37/4.54 (∀ (Xx0 Xy Xz : b), And (cQ Xx Xx0 Xy) (cQ Xx Xy Xz) → cQ Xx Xx0 Xz)) % 4.37/4.54 (∀ (Xx Xy : a), cP Xx Xy → Eq (cQ Xx) (cQ Xy)) → % 4.37/4.54 ∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (g Xy)) % 4.37/4.54 False % 4.37/4.54 Clause #8 (by clausification #[6]): ∀ (a_1 : a), Eq (∀ (Xy : a), cP a_1 Xy → cQ a_1 (f a_1) (f Xy)) True % 4.37/4.54 Clause #9 (by clausification #[8]): ∀ (a_1 a : a), Eq (cP a_1 a → cQ a_1 (f a_1) (f a)) True % 4.37/4.54 Clause #10 (by clausification #[9]): ∀ (a_1 a : a), Or (Eq (cP a_1 a) False) (Eq (cQ a_1 (f a_1) (f a)) True) % 4.37/4.54 Clause #11 (by clausification #[7]): Eq (And (∀ (Xx Xy : a), cP Xx Xy → cP Xy Xx) (∀ (Xx Xy Xz : a), And (cP Xx Xy) (cP Xy Xz) → cP Xx Xz)) True % 4.37/4.54 Clause #12 (by clausification #[7]): Eq % 4.37/4.54 (And % 4.37/4.54 (∀ (Xx : a), % 4.37/4.54 cP Xx Xx → % 4.37/4.54 And (∀ (Xx0 Xy : b), cQ Xx Xx0 Xy → cQ Xx Xy Xx0) % 4.37/4.54 (∀ (Xx0 Xy Xz : b), And (cQ Xx Xx0 Xy) (cQ Xx Xy Xz) → cQ Xx Xx0 Xz)) % 4.37/4.54 (∀ (Xx Xy : a), cP Xx Xy → Eq (cQ Xx) (cQ Xy)) → % 4.37/4.54 ∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (g Xy)) % 4.37/4.54 False % 4.37/4.54 Clause #13 (by clausification #[11]): Eq (∀ (Xx Xy Xz : a), And (cP Xx Xy) (cP Xy Xz) → cP Xx Xz) True % 4.37/4.54 Clause #14 (by clausification #[11]): Eq (∀ (Xx Xy : a), cP Xx Xy → cP Xy Xx) True % 4.37/4.54 Clause #15 (by clausification #[13]): ∀ (a_1 : a), Eq (∀ (Xy Xz : a), And (cP a_1 Xy) (cP Xy Xz) → cP a_1 Xz) True % 4.37/4.54 Clause #16 (by clausification #[15]): ∀ (a_1 a_2 : a), Eq (∀ (Xz : a), And (cP a_1 a_2) (cP a_2 Xz) → cP a_1 Xz) True % 4.37/4.54 Clause #17 (by clausification #[16]): ∀ (a_1 a_2 a : a), Eq (And (cP a_1 a_2) (cP a_2 a) → cP a_1 a) True % 4.40/4.56 Clause #18 (by clausification #[17]): ∀ (a_1 a_2 a : a), Or (Eq (And (cP a_1 a_2) (cP a_2 a)) False) (Eq (cP a_1 a) True) % 4.40/4.56 Clause #19 (by clausification #[18]): ∀ (a_1 a_2 a : a), Or (Eq (cP a_1 a_2) True) (Or (Eq (cP a_1 a) False) (Eq (cP a a_2) False)) % 4.40/4.56 Clause #20 (by clausification #[14]): ∀ (a_1 : a), Eq (∀ (Xy : a), cP a_1 Xy → cP Xy a_1) True % 4.40/4.56 Clause #21 (by clausification #[20]): ∀ (a_1 a : a), Eq (cP a_1 a → cP a a_1) True % 4.40/4.56 Clause #22 (by clausification #[21]): ∀ (a_1 a : a), Or (Eq (cP a_1 a) False) (Eq (cP a a_1) True) % 4.40/4.56 Clause #23 (by clausification #[12]): Eq % 4.40/4.56 (And % 4.40/4.56 (∀ (Xx : a), % 4.40/4.56 cP Xx Xx → % 4.40/4.56 And (∀ (Xx0 Xy : b), cQ Xx Xx0 Xy → cQ Xx Xy Xx0) % 4.40/4.56 (∀ (Xx0 Xy Xz : b), And (cQ Xx Xx0 Xy) (cQ Xx Xy Xz) → cQ Xx Xx0 Xz)) % 4.40/4.56 (∀ (Xx Xy : a), cP Xx Xy → Eq (cQ Xx) (cQ Xy))) % 4.40/4.56 True % 4.40/4.56 Clause #24 (by clausification #[12]): Eq (∀ (Xx Xy : a), cP Xx Xy → cQ Xx (f Xx) (g Xy)) False % 4.40/4.56 Clause #25 (by clausification #[23]): Eq (∀ (Xx Xy : a), cP Xx Xy → Eq (cQ Xx) (cQ Xy)) True % 4.40/4.56 Clause #26 (by clausification #[23]): Eq % 4.40/4.56 (∀ (Xx : a), % 4.40/4.56 cP Xx Xx → % 4.40/4.56 And (∀ (Xx0 Xy : b), cQ Xx Xx0 Xy → cQ Xx Xy Xx0) % 4.40/4.56 (∀ (Xx0 Xy Xz : b), And (cQ Xx Xx0 Xy) (cQ Xx Xy Xz) → cQ Xx Xx0 Xz)) % 4.40/4.56 True % 4.40/4.56 Clause #27 (by clausification #[25]): ∀ (a_1 : a), Eq (∀ (Xy : a), cP a_1 Xy → Eq (cQ a_1) (cQ Xy)) True % 4.40/4.56 Clause #28 (by clausification #[27]): ∀ (a_1 a : a), Eq (cP a_1 a → Eq (cQ a_1) (cQ a)) True % 4.40/4.56 Clause #29 (by clausification #[28]): ∀ (a_1 a : a), Or (Eq (cP a_1 a) False) (Eq (Eq (cQ a_1) (cQ a)) True) % 4.40/4.56 Clause #30 (by clausification #[29]): ∀ (a_1 a : a), Or (Eq (cP a_1 a) False) (Eq (cQ a_1) (cQ a)) % 4.40/4.56 Clause #31 (by clausification #[24]): ∀ (a_1 : a), Eq (Not (∀ (Xy : a), cP (skS.0 0 a_1) Xy → cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (g Xy))) True % 4.40/4.56 Clause #32 (by clausification #[31]): ∀ (a_1 : a), Eq (∀ (Xy : a), cP (skS.0 0 a_1) Xy → cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (g Xy)) False % 4.40/4.56 Clause #33 (by clausification #[32]): ∀ (a_1 a_2 : a), % 4.40/4.56 Eq (Not (cP (skS.0 0 a_1) (skS.0 1 a_1 a_2) → cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (g (skS.0 1 a_1 a_2)))) True % 4.40/4.56 Clause #34 (by clausification #[33]): ∀ (a_1 a_2 : a), % 4.40/4.56 Eq (cP (skS.0 0 a_1) (skS.0 1 a_1 a_2) → cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (g (skS.0 1 a_1 a_2))) False % 4.40/4.56 Clause #35 (by clausification #[34]): ∀ (a_1 a_2 : a), Eq (cP (skS.0 0 a_1) (skS.0 1 a_1 a_2)) True % 4.40/4.56 Clause #36 (by clausification #[34]): ∀ (a_1 a_2 : a), Eq (cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (g (skS.0 1 a_1 a_2))) False % 4.40/4.56 Clause #37 (by superposition #[35, 10]): ∀ (a_1 a_2 : a), Or (Eq True False) (Eq (cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (f (skS.0 1 a_1 a_2))) True) % 4.40/4.56 Clause #38 (by superposition #[35, 19]): ∀ (a_1 a_2 a_3 : a), Or (Eq (cP (skS.0 0 a_1) a_2) True) (Or (Eq True False) (Eq (cP (skS.0 1 a_1 a_3) a_2) False)) % 4.40/4.56 Clause #39 (by superposition #[35, 22]): ∀ (a_1 a_2 : a), Or (Eq True False) (Eq (cP (skS.0 1 a_1 a_2) (skS.0 0 a_1)) True) % 4.40/4.56 Clause #40 (by superposition #[35, 30]): ∀ (a_1 a_2 : a), Or (Eq True False) (Eq (cQ (skS.0 0 a_1)) (cQ (skS.0 1 a_1 a_2))) % 4.40/4.56 Clause #41 (by clausification #[40]): ∀ (a_1 a_2 : a), Eq (cQ (skS.0 0 a_1)) (cQ (skS.0 1 a_1 a_2)) % 4.40/4.56 Clause #43 (by argument congruence #[41]): ∀ (a_1 : a) (a_2 a_3 : b) (a_4 : a), Eq (cQ (skS.0 0 a_1) a_2 a_3) (cQ (skS.0 1 a_1 a_4) a_2 a_3) % 4.40/4.56 Clause #44 (by clausification #[39]): ∀ (a_1 a_2 : a), Eq (cP (skS.0 1 a_1 a_2) (skS.0 0 a_1)) True % 4.40/4.56 Clause #46 (by superposition #[44, 19]): ∀ (a_1 a_2 a_3 : a), Or (Eq (cP (skS.0 1 a_1 a_2) a_3) True) (Or (Eq True False) (Eq (cP (skS.0 0 a_1) a_3) False)) % 4.40/4.56 Clause #50 (by clausification #[26]): ∀ (a : a), % 4.40/4.56 Eq % 4.40/4.56 (cP a a → % 4.40/4.56 And (∀ (Xx0 Xy : b), cQ a Xx0 Xy → cQ a Xy Xx0) (∀ (Xx0 Xy Xz : b), And (cQ a Xx0 Xy) (cQ a Xy Xz) → cQ a Xx0 Xz)) % 4.40/4.56 True % 4.40/4.56 Clause #51 (by clausification #[50]): ∀ (a : a), % 4.40/4.56 Or (Eq (cP a a) False) % 4.40/4.56 (Eq % 4.40/4.56 (And (∀ (Xx0 Xy : b), cQ a Xx0 Xy → cQ a Xy Xx0) % 4.40/4.56 (∀ (Xx0 Xy Xz : b), And (cQ a Xx0 Xy) (cQ a Xy Xz) → cQ a Xx0 Xz)) % 4.40/4.58 True) % 4.40/4.58 Clause #52 (by clausification #[51]): ∀ (a : a), Or (Eq (cP a a) False) (Eq (∀ (Xx0 Xy Xz : b), And (cQ a Xx0 Xy) (cQ a Xy Xz) → cQ a Xx0 Xz) True) % 4.40/4.58 Clause #54 (by clausification #[52]): ∀ (a : a) (a_1 : b), Or (Eq (cP a a) False) (Eq (∀ (Xy Xz : b), And (cQ a a_1 Xy) (cQ a Xy Xz) → cQ a a_1 Xz) True) % 4.40/4.58 Clause #55 (by clausification #[54]): ∀ (a : a) (a_1 a_2 : b), Or (Eq (cP a a) False) (Eq (∀ (Xz : b), And (cQ a a_1 a_2) (cQ a a_2 Xz) → cQ a a_1 Xz) True) % 4.40/4.58 Clause #56 (by clausification #[55]): ∀ (a : a) (a_1 a_2 a_3 : b), Or (Eq (cP a a) False) (Eq (And (cQ a a_1 a_2) (cQ a a_2 a_3) → cQ a a_1 a_3) True) % 4.40/4.58 Clause #57 (by clausification #[56]): ∀ (a : a) (a_1 a_2 a_3 : b), % 4.40/4.58 Or (Eq (cP a a) False) (Or (Eq (And (cQ a a_1 a_2) (cQ a a_2 a_3)) False) (Eq (cQ a a_1 a_3) True)) % 4.40/4.58 Clause #58 (by clausification #[57]): ∀ (a : a) (a_1 a_2 a_3 : b), % 4.40/4.58 Or (Eq (cP a a) False) (Or (Eq (cQ a a_1 a_2) True) (Or (Eq (cQ a a_1 a_3) False) (Eq (cQ a a_3 a_2) False))) % 4.40/4.58 Clause #64 (by clausification #[38]): ∀ (a_1 a_2 a_3 : a), Or (Eq (cP (skS.0 0 a_1) a_2) True) (Eq (cP (skS.0 1 a_1 a_3) a_2) False) % 4.40/4.58 Clause #65 (by superposition #[64, 44]): ∀ (a_1 : a), Or (Eq (cP (skS.0 0 a_1) (skS.0 0 a_1)) True) (Eq False True) % 4.40/4.58 Clause #66 (by clausification #[65]): ∀ (a_1 : a), Eq (cP (skS.0 0 a_1) (skS.0 0 a_1)) True % 4.40/4.58 Clause #70 (by superposition #[66, 58]): ∀ (a_1 : a) (a_2 a_3 a_4 : b), % 4.40/4.58 Or (Eq True False) % 4.40/4.58 (Or (Eq (cQ (skS.0 0 a_1) a_2 a_3) True) % 4.40/4.58 (Or (Eq (cQ (skS.0 0 a_1) a_2 a_4) False) (Eq (cQ (skS.0 0 a_1) a_4 a_3) False))) % 4.40/4.58 Clause #73 (by clausification #[46]): ∀ (a_1 a_2 a_3 : a), Or (Eq (cP (skS.0 1 a_1 a_2) a_3) True) (Eq (cP (skS.0 0 a_1) a_3) False) % 4.40/4.58 Clause #74 (by superposition #[73, 35]): ∀ (a_1 a_2 a_3 : a), Or (Eq (cP (skS.0 1 a_1 a_2) (skS.0 1 a_1 a_3)) True) (Eq False True) % 4.40/4.58 Clause #76 (by clausification #[74]): ∀ (a_1 a_2 a_3 : a), Eq (cP (skS.0 1 a_1 a_2) (skS.0 1 a_1 a_3)) True % 4.40/4.58 Clause #78 (by superposition #[76, 5]): ∀ (a_1 a_2 : a), Or (Eq True False) (Eq (cQ (skS.0 1 a_1 a_2) (f (skS.0 1 a_1 a_2)) (g (skS.0 1 a_1 a_2))) True) % 4.40/4.58 Clause #86 (by clausification #[37]): ∀ (a_1 a_2 : a), Eq (cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (f (skS.0 1 a_1 a_2))) True % 4.40/4.58 Clause #103 (by clausification #[70]): ∀ (a_1 : a) (a_2 a_3 a_4 : b), % 4.40/4.58 Or (Eq (cQ (skS.0 0 a_1) a_2 a_3) True) % 4.40/4.58 (Or (Eq (cQ (skS.0 0 a_1) a_2 a_4) False) (Eq (cQ (skS.0 0 a_1) a_4 a_3) False)) % 4.40/4.58 Clause #104 (by superposition #[103, 86]): ∀ (a_1 : a) (a_2 : b) (a_3 : a), % 4.40/4.58 Or (Eq (cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) a_2) True) % 4.40/4.58 (Or (Eq (cQ (skS.0 0 a_1) (f (skS.0 1 a_1 a_3)) a_2) False) (Eq False True)) % 4.40/4.58 Clause #115 (by clausification #[78]): ∀ (a_1 a_2 : a), Eq (cQ (skS.0 1 a_1 a_2) (f (skS.0 1 a_1 a_2)) (g (skS.0 1 a_1 a_2))) True % 4.40/4.58 Clause #116 (by superposition #[115, 43]): ∀ (a_1 a_2 : a), Eq (cQ (skS.0 0 a_1) (f (skS.0 1 a_1 a_2)) (g (skS.0 1 a_1 a_2))) True % 4.40/4.58 Clause #158 (by clausification #[104]): ∀ (a_1 : a) (a_2 : b) (a_3 : a), % 4.40/4.58 Or (Eq (cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) a_2) True) (Eq (cQ (skS.0 0 a_1) (f (skS.0 1 a_1 a_3)) a_2) False) % 4.40/4.58 Clause #160 (by superposition #[158, 116]): ∀ (a_1 a_2 : a), Or (Eq (cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (g (skS.0 1 a_1 a_2))) True) (Eq False True) % 4.40/4.58 Clause #162 (by clausification #[160]): ∀ (a_1 a_2 : a), Eq (cQ (skS.0 0 a_1) (f (skS.0 0 a_1)) (g (skS.0 1 a_1 a_2))) True % 4.40/4.58 Clause #163 (by superposition #[162, 36]): Eq True False % 4.40/4.58 Clause #168 (by clausification #[163]): False % 4.40/4.58 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------