%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO384^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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:08:58 PM UTC 2025 % Result : Theorem 5.03s 5.26s % Output : Proof 5.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SYO384^5 : TPTP v9.2.0. Released v4.0.0. % 0.00/0.11 % Command : duper %s % 0.10/0.31 % Computer : n009.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Fri Oct 3 13:55:08 EDT 2025 % 0.10/0.31 % CPUTime : % 5.03/5.26 SZS status Theorem for theBenchmark.p % 5.03/5.26 SZS output start Proof for theBenchmark.p % 5.03/5.26 Clause #0 (by assumption #[]): Eq % 5.03/5.26 (Not % 5.03/5.26 ((And % 5.03/5.26 (And (∀ (Xx : Iota), Exists fun Xy => cF Xx Xy) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => % 5.03/5.26 ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) → % 5.03/5.26 Exists fun Xy => % 5.03/5.26 ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe) → % 5.03/5.26 And % 5.03/5.26 (And (∀ (Xx : Iota), Exists fun Xy => cF Xx Xy) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => % 5.03/5.26 ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) → % 5.03/5.26 Exists fun Xy => % 5.03/5.26 ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe)) % 5.03/5.26 True % 5.03/5.26 Clause #1 (by betaEtaReduce #[0]): Eq % 5.03/5.26 (Not % 5.03/5.26 ((And % 5.03/5.26 (And (∀ (Xx : Iota), Exists (cF Xx)) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => % 5.03/5.26 ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) → % 5.03/5.26 Exists fun Xy => % 5.03/5.26 ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe) → % 5.03/5.26 And % 5.03/5.26 (And (∀ (Xx : Iota), Exists (cF Xx)) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => % 5.03/5.26 ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) → % 5.03/5.26 Exists fun Xy => % 5.03/5.26 ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe)) % 5.03/5.26 True % 5.03/5.26 Clause #2 (by clausification #[1]): Eq % 5.03/5.26 ((And % 5.03/5.26 (And (∀ (Xx : Iota), Exists (cF Xx)) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) → % 5.03/5.26 Exists fun Xy => % 5.03/5.26 ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe) → % 5.03/5.26 And % 5.03/5.26 (And (∀ (Xx : Iota), Exists (cF Xx)) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) → % 5.03/5.26 Exists fun Xy => ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe) % 5.03/5.26 False % 5.03/5.26 Clause #4 (by clausification #[2]): Eq % 5.03/5.26 (And % 5.03/5.26 (And (∀ (Xx : Iota), Exists (cF Xx)) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) → % 5.03/5.26 Exists fun Xy => ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe) % 5.03/5.26 False % 5.03/5.26 Clause #35 (by clausification #[4]): Eq % 5.03/5.26 (And % 5.03/5.26 (And (∀ (Xx : Iota), Exists (cF Xx)) % 5.03/5.26 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.03/5.26 (∀ (Xe : Iota), % 5.03/5.26 Exists fun Xd => ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe)) % 5.03/5.26 True % 5.03/5.26 Clause #36 (by clausification #[4]): Eq (Exists fun Xy => ∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz Xy Xe) % 5.03/5.26 False % 5.11/5.31 Clause #37 (by clausification #[35]): Eq % 5.11/5.31 (∀ (Xe : Iota), % 5.11/5.31 Exists fun Xd => ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz Xe) % 5.11/5.31 True % 5.11/5.31 Clause #38 (by clausification #[35]): Eq % 5.11/5.31 (And (∀ (Xx : Iota), Exists (cF Xx)) % 5.11/5.31 (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe)) % 5.11/5.31 True % 5.11/5.31 Clause #39 (by clausification #[37]): ∀ (a : Iota), % 5.11/5.31 Eq (Exists fun Xd => ∀ (Xa Xb : Iota), cD Xa Xb Xd → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz a) True % 5.11/5.31 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 5.11/5.31 Eq (∀ (Xa Xb : Iota), cD Xa Xb (skS.0 8 a a_1) → ∀ (Xy Xz : Iota), And (cF Xa Xy) (cF Xb Xz) → cD Xy Xz a) True % 5.11/5.31 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Eq (∀ (Xb : Iota), cD a Xb (skS.0 8 a_1 a_2) → ∀ (Xy Xz : Iota), And (cF a Xy) (cF Xb Xz) → cD Xy Xz a_1) True % 5.11/5.31 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 : Iota), % 5.11/5.31 Eq (cD a a_1 (skS.0 8 a_2 a_3) → ∀ (Xy Xz : Iota), And (cF a Xy) (cF a_1 Xz) → cD Xy Xz a_2) True % 5.11/5.31 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 : Iota), % 5.11/5.31 Or (Eq (cD a a_1 (skS.0 8 a_2 a_3)) False) (Eq (∀ (Xy Xz : Iota), And (cF a Xy) (cF a_1 Xz) → cD Xy Xz a_2) True) % 5.11/5.31 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.11/5.31 Or (Eq (cD a a_1 (skS.0 8 a_2 a_3)) False) (Eq (∀ (Xz : Iota), And (cF a a_4) (cF a_1 Xz) → cD a_4 Xz a_2) True) % 5.11/5.31 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.11/5.31 Or (Eq (cD a a_1 (skS.0 8 a_2 a_3)) False) (Eq (And (cF a a_4) (cF a_1 a_5) → cD a_4 a_5 a_2) True) % 5.11/5.31 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.11/5.31 Or (Eq (cD a a_1 (skS.0 8 a_2 a_3)) False) (Or (Eq (And (cF a a_4) (cF a_1 a_5)) False) (Eq (cD a_4 a_5 a_2) True)) % 5.11/5.31 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.11/5.31 Or (Eq (cD a a_1 (skS.0 8 a_2 a_3)) False) % 5.11/5.31 (Or (Eq (cD a_4 a_5 a_2) True) (Or (Eq (cF a a_4) False) (Eq (cF a_1 a_5) False))) % 5.11/5.31 Clause #48 (by clausification #[36]): ∀ (a : Iota), Eq (∀ (Xe : Iota), Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz a Xe) False % 5.11/5.31 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), % 5.11/5.31 Eq (Not (Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz a (skS.0 9 a a_1))) True % 5.11/5.31 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), % 5.11/5.31 Eq (Exists fun Xm => ∀ (Xw : Iota), cS Xm Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz a (skS.0 9 a a_1)) False % 5.11/5.31 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Xw : Iota), cS a Xw → ∀ (Xz : Iota), cF Xw Xz → cD Xz a_1 (skS.0 9 a_1 a_2)) False % 5.11/5.31 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 : Iota), % 5.11/5.31 Eq (Not (cS a (skS.0 10 a a_1 a_2 a_3) → ∀ (Xz : Iota), cF (skS.0 10 a a_1 a_2 a_3) Xz → cD Xz a_1 (skS.0 9 a_1 a_2))) % 5.11/5.31 True % 5.11/5.31 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 5.11/5.31 Eq (cS a (skS.0 10 a a_1 a_2 a_3) → ∀ (Xz : Iota), cF (skS.0 10 a a_1 a_2 a_3) Xz → cD Xz a_1 (skS.0 9 a_1 a_2)) False % 5.11/5.31 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cS a (skS.0 10 a a_1 a_2 a_3)) True % 5.11/5.31 Clause #55 (by clausification #[53]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (Xz : Iota), cF (skS.0 10 a a_1 a_2 a_3) Xz → cD Xz a_1 (skS.0 9 a_1 a_2)) False % 5.11/5.31 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.11/5.31 Eq % 5.11/5.31 (Not % 5.11/5.31 (cF (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4) → % 5.11/5.31 cD (skS.0 11 a a_1 a_2 a_3 a_4) a_1 (skS.0 9 a_1 a_2))) % 5.11/5.31 True % 5.11/5.31 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.11/5.31 Eq (cF (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4) → cD (skS.0 11 a a_1 a_2 a_3 a_4) a_1 (skS.0 9 a_1 a_2)) % 5.11/5.31 False % 5.11/5.31 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (cF (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4)) True % 5.11/5.31 Clause #59 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (cD (skS.0 11 a a_1 a_2 a_3 a_4) a_1 (skS.0 9 a_1 a_2)) False % 5.11/5.31 Clause #60 (by clausification #[38]): Eq (Exists fun Xx => ∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw Xx Xe) True % 5.11/5.35 Clause #61 (by clausification #[38]): Eq (∀ (Xx : Iota), Exists (cF Xx)) True % 5.11/5.35 Clause #62 (by clausification #[60]): ∀ (a : Iota), Eq (∀ (Xe : Iota), Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw (skS.0 12 a) Xe) True % 5.11/5.35 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), Eq (Exists fun Xn => ∀ (Xw : Iota), cS Xn Xw → cD Xw (skS.0 12 a) a_1) True % 5.11/5.35 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Xw : Iota), cS (skS.0 13 a a_1 a_2) Xw → cD Xw (skS.0 12 a) a_1) True % 5.11/5.35 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cS (skS.0 13 a a_1 a_2) a_3 → cD a_3 (skS.0 12 a) a_1) True % 5.11/5.35 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cS (skS.0 13 a a_1 a_2) a_3) False) (Eq (cD a_3 (skS.0 12 a) a_1) True) % 5.11/5.35 Clause #67 (by superposition #[66, 54]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.11/5.35 Or (Eq (cD (skS.0 10 (skS.0 13 a a_1 a_2) a_3 a_4 a_5) (skS.0 12 a) a_1) True) (Eq False True) % 5.11/5.35 Clause #70 (by clausification #[61]): ∀ (a : Iota), Eq (Exists (cF a)) True % 5.11/5.35 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), Eq (cF a (skS.0 14 a a_1)) True % 5.11/5.35 Clause #74 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (cD (skS.0 10 (skS.0 13 a a_1 a_2) a_3 a_4 a_5) (skS.0 12 a) a_1) True % 5.11/5.35 Clause #75 (by superposition #[74, 47]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 5.11/5.35 Or (Eq True False) % 5.11/5.35 (Or (Eq (cD a a_1 a_2) True) % 5.11/5.35 (Or (Eq (cF (skS.0 10 (skS.0 13 a_3 (skS.0 8 a_2 a_4) a_5) a_6 a_7 a_8) a) False) % 5.11/5.35 (Eq (cF (skS.0 12 a_3) a_1) False))) % 5.11/5.35 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 5.11/5.35 Or (Eq (cD a a_1 a_2) True) % 5.11/5.35 (Or (Eq (cF (skS.0 10 (skS.0 13 a_3 (skS.0 8 a_2 a_4) a_5) a_6 a_7 a_8) a) False) % 5.11/5.35 (Eq (cF (skS.0 12 a_3) a_1) False)) % 5.11/5.35 Clause #77 (by superposition #[76, 58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 5.11/5.35 Or (Eq (cD (skS.0 11 (skS.0 13 a (skS.0 8 a_1 a_2) a_3) a_4 a_5 a_6 a_7) a_8 a_1) True) % 5.11/5.35 (Or (Eq (cF (skS.0 12 a) a_8) False) (Eq False True)) % 5.11/5.35 Clause #79 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 5.11/5.35 Or (Eq (cD (skS.0 11 (skS.0 13 a (skS.0 8 a_1 a_2) a_3) a_4 a_5 a_6 a_7) a_8 a_1) True) % 5.11/5.35 (Eq (cF (skS.0 12 a) a_8) False) % 5.11/5.35 Clause #80 (by superposition #[79, 71]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 5.11/5.35 Or (Eq (cD (skS.0 11 (skS.0 13 a (skS.0 8 a_1 a_2) a_3) a_4 a_5 a_6 a_7) (skS.0 14 (skS.0 12 a) a_8) a_1) True) % 5.11/5.35 (Eq False True) % 5.11/5.35 Clause #90 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 5.11/5.35 Eq (cD (skS.0 11 (skS.0 13 a (skS.0 8 a_1 a_2) a_3) a_4 a_5 a_6 a_7) (skS.0 14 (skS.0 12 a) a_8) a_1) True % 5.11/5.35 Clause #92 (by superposition #[90, 59]): Eq True False % 5.11/5.35 Clause #93 (by clausification #[92]): False % 5.11/5.35 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------