%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM412+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:56:26 PM UTC 2025 % Result : Theorem 135.83s 136.00s % Output : Proof 135.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM412+1 : TPTP v9.2.0. Released v3.2.0. % 0.11/0.13 % Command : duper %s % 0.14/0.34 % Computer : n020.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 07:39:53 EDT 2025 % 0.14/0.34 % CPUTime : % 135.83/136.00 SZS status Theorem for theBenchmark.p % 135.83/136.00 SZS output start Proof for theBenchmark.p % 135.83/136.00 Clause #7 (by assumption #[]): Eq % 135.83/136.00 (∀ (A B : Iota), % 135.83/136.00 And (And (relation B) (function B)) (transfinite_sequence B) → % 135.83/136.00 Iff (transfinite_sequence_of B A) (subset (relation_rng B) A)) % 135.83/136.00 True % 135.83/136.00 Clause #8 (by assumption #[]): Eq % 135.83/136.00 (∀ (A B : Iota), % 135.83/136.00 And (And (And (relation A) (function A)) (transfinite_sequence A)) (ordinal B) → % 135.83/136.00 transfinite_sequence_of (tseq_dom_restriction A B) (relation_rng A)) % 135.83/136.00 True % 135.83/136.00 Clause #10 (by assumption #[]): Eq (∀ (A B : Iota), transfinite_sequence_of B A → And (And (relation B) (function B)) (transfinite_sequence B)) True % 135.83/136.00 Clause #41 (by assumption #[]): Eq (∀ (A B : Iota), subset A B → ∀ (C : Iota), transfinite_sequence_of C A → transfinite_sequence_of C B) True % 135.83/136.00 Clause #42 (by assumption #[]): Eq % 135.83/136.00 (Not % 135.83/136.00 (∀ (A B : Iota), % 135.83/136.00 transfinite_sequence_of B A → ∀ (C : Iota), ordinal C → transfinite_sequence_of (tseq_dom_restriction B C) A)) % 135.83/136.00 True % 135.83/136.00 Clause #132 (by clausification #[7]): ∀ (a : Iota), % 135.83/136.00 Eq % 135.83/136.00 (∀ (B : Iota), % 135.83/136.00 And (And (relation B) (function B)) (transfinite_sequence B) → % 135.83/136.00 Iff (transfinite_sequence_of B a) (subset (relation_rng B) a)) % 135.83/136.00 True % 135.83/136.00 Clause #133 (by clausification #[132]): ∀ (a a_1 : Iota), % 135.83/136.00 Eq % 135.83/136.00 (And (And (relation a) (function a)) (transfinite_sequence a) → % 135.83/136.00 Iff (transfinite_sequence_of a a_1) (subset (relation_rng a) a_1)) % 135.83/136.00 True % 135.83/136.00 Clause #134 (by clausification #[133]): ∀ (a a_1 : Iota), % 135.83/136.00 Or (Eq (And (And (relation a) (function a)) (transfinite_sequence a)) False) % 135.83/136.00 (Eq (Iff (transfinite_sequence_of a a_1) (subset (relation_rng a) a_1)) True) % 135.83/136.00 Clause #135 (by clausification #[134]): ∀ (a a_1 : Iota), % 135.83/136.00 Or (Eq (Iff (transfinite_sequence_of a a_1) (subset (relation_rng a) a_1)) True) % 135.83/136.00 (Or (Eq (And (relation a) (function a)) False) (Eq (transfinite_sequence a) False)) % 135.83/136.00 Clause #137 (by clausification #[135]): ∀ (a a_1 : Iota), % 135.83/136.00 Or (Eq (And (relation a) (function a)) False) % 135.83/136.00 (Or (Eq (transfinite_sequence a) False) % 135.83/136.00 (Or (Eq (transfinite_sequence_of a a_1) False) (Eq (subset (relation_rng a) a_1) True))) % 135.83/136.00 Clause #139 (by clausification #[41]): ∀ (a : Iota), % 135.83/136.00 Eq (∀ (B : Iota), subset a B → ∀ (C : Iota), transfinite_sequence_of C a → transfinite_sequence_of C B) True % 135.83/136.00 Clause #140 (by clausification #[139]): ∀ (a a_1 : Iota), Eq (subset a a_1 → ∀ (C : Iota), transfinite_sequence_of C a → transfinite_sequence_of C a_1) True % 135.83/136.00 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), % 135.83/136.00 Or (Eq (subset a a_1) False) (Eq (∀ (C : Iota), transfinite_sequence_of C a → transfinite_sequence_of C a_1) True) % 135.83/136.00 Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 : Iota), % 135.83/136.00 Or (Eq (subset a a_1) False) (Eq (transfinite_sequence_of a_2 a → transfinite_sequence_of a_2 a_1) True) % 135.83/136.00 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 : Iota), % 135.83/136.00 Or (Eq (subset a a_1) False) % 135.83/136.00 (Or (Eq (transfinite_sequence_of a_2 a) False) (Eq (transfinite_sequence_of a_2 a_1) True)) % 135.83/136.00 Clause #157 (by clausification #[8]): ∀ (a : Iota), % 135.83/136.00 Eq % 135.83/136.00 (∀ (B : Iota), % 135.83/136.00 And (And (And (relation a) (function a)) (transfinite_sequence a)) (ordinal B) → % 135.83/136.00 transfinite_sequence_of (tseq_dom_restriction a B) (relation_rng a)) % 135.83/136.00 True % 135.83/136.00 Clause #158 (by clausification #[157]): ∀ (a a_1 : Iota), % 135.83/136.00 Eq % 135.83/136.00 (And (And (And (relation a) (function a)) (transfinite_sequence a)) (ordinal a_1) → % 135.83/136.00 transfinite_sequence_of (tseq_dom_restriction a a_1) (relation_rng a)) % 135.83/136.00 True % 135.83/136.00 Clause #159 (by clausification #[158]): ∀ (a a_1 : Iota), % 135.83/136.00 Or (Eq (And (And (And (relation a) (function a)) (transfinite_sequence a)) (ordinal a_1)) False) % 135.83/136.00 (Eq (transfinite_sequence_of (tseq_dom_restriction a a_1) (relation_rng a)) True) % 135.83/136.00 Clause #160 (by clausification #[159]): ∀ (a a_1 : Iota), % 135.83/136.00 Or (Eq (transfinite_sequence_of (tseq_dom_restriction a a_1) (relation_rng a)) True) % 135.83/136.00 (Or (Eq (And (And (relation a) (function a)) (transfinite_sequence a)) False) (Eq (ordinal a_1) False)) % 135.83/136.00 Clause #161 (by clausification #[160]): ∀ (a a_1 : Iota), % 135.83/136.00 Or (Eq (transfinite_sequence_of (tseq_dom_restriction a a_1) (relation_rng a)) True) % 135.85/136.02 (Or (Eq (ordinal a_1) False) (Or (Eq (And (relation a) (function a)) False) (Eq (transfinite_sequence a) False))) % 135.85/136.02 Clause #162 (by clausification #[161]): ∀ (a a_1 : Iota), % 135.85/136.02 Or (Eq (transfinite_sequence_of (tseq_dom_restriction a a_1) (relation_rng a)) True) % 135.85/136.02 (Or (Eq (ordinal a_1) False) % 135.85/136.02 (Or (Eq (transfinite_sequence a) False) (Or (Eq (relation a) False) (Eq (function a) False)))) % 135.85/136.02 Clause #177 (by clausification #[10]): ∀ (a : Iota), % 135.85/136.02 Eq (∀ (B : Iota), transfinite_sequence_of B a → And (And (relation B) (function B)) (transfinite_sequence B)) True % 135.85/136.02 Clause #178 (by clausification #[177]): ∀ (a a_1 : Iota), Eq (transfinite_sequence_of a a_1 → And (And (relation a) (function a)) (transfinite_sequence a)) True % 135.85/136.02 Clause #179 (by clausification #[178]): ∀ (a a_1 : Iota), % 135.85/136.02 Or (Eq (transfinite_sequence_of a a_1) False) (Eq (And (And (relation a) (function a)) (transfinite_sequence a)) True) % 135.85/136.02 Clause #180 (by clausification #[179]): ∀ (a a_1 : Iota), Or (Eq (transfinite_sequence_of a a_1) False) (Eq (transfinite_sequence a) True) % 135.85/136.02 Clause #181 (by clausification #[179]): ∀ (a a_1 : Iota), Or (Eq (transfinite_sequence_of a a_1) False) (Eq (And (relation a) (function a)) True) % 135.85/136.02 Clause #291 (by clausification #[181]): ∀ (a a_1 : Iota), Or (Eq (transfinite_sequence_of a a_1) False) (Eq (function a) True) % 135.85/136.02 Clause #292 (by clausification #[181]): ∀ (a a_1 : Iota), Or (Eq (transfinite_sequence_of a a_1) False) (Eq (relation a) True) % 135.85/136.02 Clause #379 (by clausification #[42]): Eq % 135.85/136.02 (∀ (A B : Iota), % 135.85/136.02 transfinite_sequence_of B A → ∀ (C : Iota), ordinal C → transfinite_sequence_of (tseq_dom_restriction B C) A) % 135.85/136.02 False % 135.85/136.02 Clause #380 (by clausification #[379]): ∀ (a : Iota), % 135.85/136.02 Eq % 135.85/136.02 (Not % 135.85/136.02 (∀ (B : Iota), % 135.85/136.02 transfinite_sequence_of B (skS.0 16 a) → % 135.85/136.02 ∀ (C : Iota), ordinal C → transfinite_sequence_of (tseq_dom_restriction B C) (skS.0 16 a))) % 135.85/136.02 True % 135.85/136.02 Clause #381 (by clausification #[380]): ∀ (a : Iota), % 135.85/136.02 Eq % 135.85/136.02 (∀ (B : Iota), % 135.85/136.02 transfinite_sequence_of B (skS.0 16 a) → % 135.85/136.02 ∀ (C : Iota), ordinal C → transfinite_sequence_of (tseq_dom_restriction B C) (skS.0 16 a)) % 135.85/136.02 False % 135.85/136.02 Clause #382 (by clausification #[381]): ∀ (a a_1 : Iota), % 135.85/136.02 Eq % 135.85/136.02 (Not % 135.85/136.02 (transfinite_sequence_of (skS.0 17 a a_1) (skS.0 16 a) → % 135.85/136.02 ∀ (C : Iota), ordinal C → transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) C) (skS.0 16 a))) % 135.85/136.02 True % 135.85/136.02 Clause #383 (by clausification #[382]): ∀ (a a_1 : Iota), % 135.85/136.02 Eq % 135.85/136.02 (transfinite_sequence_of (skS.0 17 a a_1) (skS.0 16 a) → % 135.85/136.02 ∀ (C : Iota), ordinal C → transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) C) (skS.0 16 a)) % 135.85/136.02 False % 135.85/136.02 Clause #384 (by clausification #[383]): ∀ (a a_1 : Iota), Eq (transfinite_sequence_of (skS.0 17 a a_1) (skS.0 16 a)) True % 135.85/136.02 Clause #385 (by clausification #[383]): ∀ (a a_1 : Iota), % 135.85/136.02 Eq (∀ (C : Iota), ordinal C → transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) C) (skS.0 16 a)) False % 135.85/136.02 Clause #386 (by superposition #[384, 180]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (transfinite_sequence (skS.0 17 a a_1)) True) % 135.85/136.02 Clause #387 (by superposition #[384, 291]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (function (skS.0 17 a a_1)) True) % 135.85/136.02 Clause #388 (by superposition #[384, 292]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (relation (skS.0 17 a a_1)) True) % 135.85/136.02 Clause #389 (by clausification #[388]): ∀ (a a_1 : Iota), Eq (relation (skS.0 17 a a_1)) True % 135.85/136.02 Clause #394 (by clausification #[387]): ∀ (a a_1 : Iota), Eq (function (skS.0 17 a a_1)) True % 135.85/136.02 Clause #407 (by clausification #[386]): ∀ (a a_1 : Iota), Eq (transfinite_sequence (skS.0 17 a a_1)) True % 135.85/136.02 Clause #456 (by clausification #[137]): ∀ (a a_1 : Iota), % 135.85/136.02 Or (Eq (transfinite_sequence a) False) % 135.85/136.02 (Or (Eq (transfinite_sequence_of a a_1) False) % 135.85/136.02 (Or (Eq (subset (relation_rng a) a_1) True) (Or (Eq (relation a) False) (Eq (function a) False)))) % 135.85/136.02 Clause #458 (by superposition #[456, 407]): ∀ (a a_1 a_2 : Iota), % 135.85/136.02 Or (Eq (transfinite_sequence_of (skS.0 17 a a_1) a_2) False) % 135.85/136.04 (Or (Eq (subset (relation_rng (skS.0 17 a a_1)) a_2) True) % 135.85/136.04 (Or (Eq (relation (skS.0 17 a a_1)) False) (Or (Eq (function (skS.0 17 a a_1)) False) (Eq False True)))) % 135.85/136.04 Clause #851 (by clausification #[385]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Eq % 135.85/136.04 (Not % 135.85/136.04 (ordinal (skS.0 18 a a_1 a_2) → % 135.85/136.04 transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a a_1 a_2)) (skS.0 16 a))) % 135.85/136.04 True % 135.85/136.04 Clause #852 (by clausification #[851]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Eq % 135.85/136.04 (ordinal (skS.0 18 a a_1 a_2) → % 135.85/136.04 transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a a_1 a_2)) (skS.0 16 a)) % 135.85/136.04 False % 135.85/136.04 Clause #853 (by clausification #[852]): ∀ (a a_1 a_2 : Iota), Eq (ordinal (skS.0 18 a a_1 a_2)) True % 135.85/136.04 Clause #854 (by clausification #[852]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Eq (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a a_1 a_2)) (skS.0 16 a)) False % 135.85/136.04 Clause #857 (by superposition #[853, 162]): ∀ (a a_1 a_2 a_3 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of (tseq_dom_restriction a (skS.0 18 a_1 a_2 a_3)) (relation_rng a)) True) % 135.85/136.04 (Or (Eq True False) (Or (Eq (transfinite_sequence a) False) (Or (Eq (relation a) False) (Eq (function a) False)))) % 135.85/136.04 Clause #1239 (by clausification #[857]): ∀ (a a_1 a_2 a_3 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of (tseq_dom_restriction a (skS.0 18 a_1 a_2 a_3)) (relation_rng a)) True) % 135.85/136.04 (Or (Eq (transfinite_sequence a) False) (Or (Eq (relation a) False) (Eq (function a) False))) % 135.85/136.04 Clause #1241 (by superposition #[1239, 407]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.04 Or % 135.85/136.04 (Eq % 135.85/136.04 (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) % 135.85/136.04 (relation_rng (skS.0 17 a a_1))) % 135.85/136.04 True) % 135.85/136.04 (Or (Eq (relation (skS.0 17 a a_1)) False) (Or (Eq (function (skS.0 17 a a_1)) False) (Eq False True))) % 135.85/136.04 Clause #1312 (by clausification #[458]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of (skS.0 17 a a_1) a_2) False) % 135.85/136.04 (Or (Eq (subset (relation_rng (skS.0 17 a a_1)) a_2) True) % 135.85/136.04 (Or (Eq (relation (skS.0 17 a a_1)) False) (Eq (function (skS.0 17 a a_1)) False))) % 135.85/136.04 Clause #1313 (by forward demodulation #[1312, 389]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of (skS.0 17 a a_1) a_2) False) % 135.85/136.04 (Or (Eq (subset (relation_rng (skS.0 17 a a_1)) a_2) True) % 135.85/136.04 (Or (Eq True False) (Eq (function (skS.0 17 a a_1)) False))) % 135.85/136.04 Clause #1314 (by clausification #[1313]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of (skS.0 17 a a_1) a_2) False) % 135.85/136.04 (Or (Eq (subset (relation_rng (skS.0 17 a a_1)) a_2) True) (Eq (function (skS.0 17 a a_1)) False)) % 135.85/136.04 Clause #1315 (by forward demodulation #[1314, 394]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of (skS.0 17 a a_1) a_2) False) % 135.85/136.04 (Or (Eq (subset (relation_rng (skS.0 17 a a_1)) a_2) True) (Eq True False)) % 135.85/136.04 Clause #1316 (by clausification #[1315]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of (skS.0 17 a a_1) a_2) False) (Eq (subset (relation_rng (skS.0 17 a a_1)) a_2) True) % 135.85/136.04 Clause #1317 (by superposition #[1316, 384]): ∀ (a a_1 : Iota), Or (Eq (subset (relation_rng (skS.0 17 a a_1)) (skS.0 16 a)) True) (Eq False True) % 135.85/136.04 Clause #1319 (by clausification #[1317]): ∀ (a a_1 : Iota), Eq (subset (relation_rng (skS.0 17 a a_1)) (skS.0 16 a)) True % 135.85/136.04 Clause #1321 (by superposition #[1319, 143]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Or (Eq True False) % 135.85/136.04 (Or (Eq (transfinite_sequence_of a (relation_rng (skS.0 17 a_1 a_2))) False) % 135.85/136.04 (Eq (transfinite_sequence_of a (skS.0 16 a_1)) True)) % 135.85/136.04 Clause #1948 (by clausification #[1321]): ∀ (a a_1 a_2 : Iota), % 135.85/136.04 Or (Eq (transfinite_sequence_of a (relation_rng (skS.0 17 a_1 a_2))) False) % 135.85/136.04 (Eq (transfinite_sequence_of a (skS.0 16 a_1)) True) % 135.85/136.04 Clause #5922 (by clausification #[1241]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.04 Or % 135.85/136.04 (Eq % 135.85/136.04 (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) % 135.85/136.04 (relation_rng (skS.0 17 a a_1))) % 135.85/136.04 True) % 135.85/136.04 (Or (Eq (relation (skS.0 17 a a_1)) False) (Eq (function (skS.0 17 a a_1)) False)) % 135.85/136.04 Clause #5923 (by forward demodulation #[5922, 389]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.07 Or % 135.85/136.07 (Eq % 135.85/136.07 (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) % 135.85/136.07 (relation_rng (skS.0 17 a a_1))) % 135.85/136.07 True) % 135.85/136.07 (Or (Eq True False) (Eq (function (skS.0 17 a a_1)) False)) % 135.85/136.07 Clause #5924 (by clausification #[5923]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.07 Or % 135.85/136.07 (Eq % 135.85/136.07 (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) % 135.85/136.07 (relation_rng (skS.0 17 a a_1))) % 135.85/136.07 True) % 135.85/136.07 (Eq (function (skS.0 17 a a_1)) False) % 135.85/136.07 Clause #5925 (by forward demodulation #[5924, 394]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.07 Or % 135.85/136.07 (Eq % 135.85/136.07 (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) % 135.85/136.07 (relation_rng (skS.0 17 a a_1))) % 135.85/136.07 True) % 135.85/136.07 (Eq True False) % 135.85/136.07 Clause #5926 (by clausification #[5925]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.07 Eq % 135.85/136.07 (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) % 135.85/136.07 (relation_rng (skS.0 17 a a_1))) % 135.85/136.07 True % 135.85/136.07 Clause #5927 (by superposition #[5926, 1948]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.07 Or (Eq True False) % 135.85/136.07 (Eq (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) (skS.0 16 a)) True) % 135.85/136.07 Clause #6036 (by clausification #[5927]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 135.85/136.07 Eq (transfinite_sequence_of (tseq_dom_restriction (skS.0 17 a a_1) (skS.0 18 a_2 a_3 a_4)) (skS.0 16 a)) True % 135.85/136.07 Clause #6037 (by superposition #[6036, 854]): Eq True False % 135.85/136.07 Clause #6038 (by clausification #[6037]): False % 135.85/136.07 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------