%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU019+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.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:48 PM UTC 2025 % Result : Theorem 12.51s 12.74s % Output : Proof 12.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SEU019+1 : TPTP v9.2.0. Released v3.2.0. % 0.00/0.12 % Command : duper %s % 0.10/0.32 % Computer : n002.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Fri Oct 3 06:47:08 EDT 2025 % 0.10/0.32 % CPUTime : % 12.51/12.74 SZS status Theorem for theBenchmark.p % 12.51/12.74 SZS output start Proof for theBenchmark.p % 12.51/12.74 Clause #3 (by assumption #[]): Eq % 12.51/12.74 (∀ (A : Iota), % 12.51/12.74 And (relation A) (function A) → % 12.51/12.74 Iff (one_to_one A) % 12.51/12.74 (∀ (B C : Iota), % 12.51/12.74 And (And (in B (relation_dom A)) (in C (relation_dom A))) (Eq (apply A B) (apply A C)) → Eq B C)) % 12.51/12.74 True % 12.51/12.74 Clause #4 (by assumption #[]): Eq (∀ (A : Iota), relation (identity_relation A)) True % 12.51/12.74 Clause #9 (by assumption #[]): Eq (∀ (A : Iota), And (relation (identity_relation A)) (function (identity_relation A))) True % 12.51/12.74 Clause #24 (by assumption #[]): Eq % 12.51/12.74 (∀ (A B : Iota), % 12.51/12.74 And (relation B) (function B) → % 12.51/12.74 Iff (Eq B (identity_relation A)) (And (Eq (relation_dom B) A) (∀ (C : Iota), in C A → Eq (apply B C) C))) % 12.51/12.74 True % 12.51/12.74 Clause #27 (by assumption #[]): Eq (Not (∀ (A : Iota), one_to_one (identity_relation A))) True % 12.51/12.74 Clause #32 (by clausification #[4]): ∀ (a : Iota), Eq (relation (identity_relation a)) True % 12.51/12.74 Clause #47 (by clausification #[27]): Eq (∀ (A : Iota), one_to_one (identity_relation A)) False % 12.51/12.74 Clause #48 (by clausification #[47]): ∀ (a : Iota), Eq (Not (one_to_one (identity_relation (skS.0 0 a)))) True % 12.51/12.74 Clause #49 (by clausification #[48]): ∀ (a : Iota), Eq (one_to_one (identity_relation (skS.0 0 a))) False % 12.51/12.74 Clause #52 (by clausification #[3]): ∀ (a : Iota), % 12.51/12.74 Eq % 12.51/12.74 (And (relation a) (function a) → % 12.51/12.74 Iff (one_to_one a) % 12.51/12.74 (∀ (B C : Iota), % 12.51/12.74 And (And (in B (relation_dom a)) (in C (relation_dom a))) (Eq (apply a B) (apply a C)) → Eq B C)) % 12.51/12.74 True % 12.51/12.74 Clause #53 (by clausification #[52]): ∀ (a : Iota), % 12.51/12.74 Or (Eq (And (relation a) (function a)) False) % 12.51/12.74 (Eq % 12.51/12.74 (Iff (one_to_one a) % 12.51/12.74 (∀ (B C : Iota), % 12.51/12.74 And (And (in B (relation_dom a)) (in C (relation_dom a))) (Eq (apply a B) (apply a C)) → Eq B C)) % 12.51/12.74 True) % 12.51/12.74 Clause #54 (by clausification #[53]): ∀ (a : Iota), % 12.51/12.74 Or % 12.51/12.74 (Eq % 12.51/12.74 (Iff (one_to_one a) % 12.51/12.74 (∀ (B C : Iota), % 12.51/12.74 And (And (in B (relation_dom a)) (in C (relation_dom a))) (Eq (apply a B) (apply a C)) → Eq B C)) % 12.51/12.74 True) % 12.51/12.74 (Or (Eq (relation a) False) (Eq (function a) False)) % 12.51/12.74 Clause #55 (by clausification #[54]): ∀ (a : Iota), % 12.51/12.74 Or (Eq (relation a) False) % 12.51/12.74 (Or (Eq (function a) False) % 12.51/12.74 (Or (Eq (one_to_one a) True) % 12.51/12.74 (Eq % 12.51/12.74 (∀ (B C : Iota), % 12.51/12.74 And (And (in B (relation_dom a)) (in C (relation_dom a))) (Eq (apply a B) (apply a C)) → Eq B C) % 12.51/12.74 False))) % 12.51/12.74 Clause #57 (by clausification #[55]): ∀ (a a_1 : Iota), % 12.51/12.74 Or (Eq (relation a) False) % 12.51/12.74 (Or (Eq (function a) False) % 12.51/12.74 (Or (Eq (one_to_one a) True) % 12.51/12.74 (Eq % 12.51/12.74 (Not % 12.51/12.74 (∀ (C : Iota), % 12.51/12.74 And (And (in (skS.0 1 a a_1) (relation_dom a)) (in C (relation_dom a))) % 12.51/12.74 (Eq (apply a (skS.0 1 a a_1)) (apply a C)) → % 12.51/12.74 Eq (skS.0 1 a a_1) C)) % 12.51/12.74 True))) % 12.51/12.74 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), % 12.51/12.74 Or (Eq (relation a) False) % 12.51/12.74 (Or (Eq (function a) False) % 12.51/12.74 (Or (Eq (one_to_one a) True) % 12.51/12.74 (Eq % 12.51/12.74 (∀ (C : Iota), % 12.51/12.74 And (And (in (skS.0 1 a a_1) (relation_dom a)) (in C (relation_dom a))) % 12.51/12.74 (Eq (apply a (skS.0 1 a a_1)) (apply a C)) → % 12.51/12.74 Eq (skS.0 1 a a_1) C) % 12.51/12.74 False))) % 12.51/12.74 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), % 12.51/12.74 Or (Eq (relation a) False) % 12.51/12.74 (Or (Eq (function a) False) % 12.51/12.74 (Or (Eq (one_to_one a) True) % 12.51/12.74 (Eq % 12.51/12.74 (Not % 12.51/12.74 (And (And (in (skS.0 1 a a_1) (relation_dom a)) (in (skS.0 2 a a_1 a_2) (relation_dom a))) % 12.51/12.74 (Eq (apply a (skS.0 1 a a_1)) (apply a (skS.0 2 a a_1 a_2))) → % 12.51/12.74 Eq (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 12.51/12.74 True))) % 12.51/12.74 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), % 12.51/12.74 Or (Eq (relation a) False) % 12.51/12.74 (Or (Eq (function a) False) % 12.51/12.74 (Or (Eq (one_to_one a) True) % 12.51/12.74 (Eq % 12.51/12.74 (And (And (in (skS.0 1 a a_1) (relation_dom a)) (in (skS.0 2 a a_1 a_2) (relation_dom a))) % 12.51/12.74 (Eq (apply a (skS.0 1 a a_1)) (apply a (skS.0 2 a a_1 a_2))) → % 12.51/12.74 Eq (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) % 12.51/12.78 False))) % 12.51/12.78 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) % 12.51/12.78 (Or (Eq (one_to_one a) True) % 12.51/12.78 (Eq % 12.51/12.78 (And (And (in (skS.0 1 a a_1) (relation_dom a)) (in (skS.0 2 a a_1 a_2) (relation_dom a))) % 12.51/12.78 (Eq (apply a (skS.0 1 a a_1)) (apply a (skS.0 2 a a_1 a_2)))) % 12.51/12.78 True))) % 12.51/12.78 Clause #62 (by clausification #[60]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) (Or (Eq (one_to_one a) True) (Eq (Eq (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) False))) % 12.51/12.78 Clause #63 (by clausification #[61]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) % 12.51/12.78 (Or (Eq (one_to_one a) True) (Eq (Eq (apply a (skS.0 1 a a_1)) (apply a (skS.0 2 a a_1 a_2))) True))) % 12.51/12.78 Clause #64 (by clausification #[61]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) % 12.51/12.78 (Or (Eq (one_to_one a) True) % 12.51/12.78 (Eq (And (in (skS.0 1 a a_1) (relation_dom a)) (in (skS.0 2 a a_1 a_2) (relation_dom a))) True))) % 12.51/12.78 Clause #65 (by clausification #[63]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) % 12.51/12.78 (Or (Eq (one_to_one a) True) (Eq (apply a (skS.0 1 a a_1)) (apply a (skS.0 2 a a_1 a_2))))) % 12.51/12.78 Clause #66 (by superposition #[65, 32]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (function (identity_relation a)) False) % 12.51/12.78 (Or (Eq (one_to_one (identity_relation a)) True) % 12.51/12.78 (Or % 12.51/12.78 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) % 12.51/12.78 (apply (identity_relation a) (skS.0 2 (identity_relation a) a_1 a_2))) % 12.51/12.78 (Eq False True))) % 12.51/12.78 Clause #102 (by clausification #[9]): ∀ (a : Iota), Eq (And (relation (identity_relation a)) (function (identity_relation a))) True % 12.51/12.78 Clause #103 (by clausification #[102]): ∀ (a : Iota), Eq (function (identity_relation a)) True % 12.51/12.78 Clause #184 (by clausification #[24]): ∀ (a : Iota), % 12.51/12.78 Eq % 12.51/12.78 (∀ (B : Iota), % 12.51/12.78 And (relation B) (function B) → % 12.51/12.78 Iff (Eq B (identity_relation a)) (And (Eq (relation_dom B) a) (∀ (C : Iota), in C a → Eq (apply B C) C))) % 12.51/12.78 True % 12.51/12.78 Clause #185 (by clausification #[184]): ∀ (a a_1 : Iota), % 12.51/12.78 Eq % 12.51/12.78 (And (relation a) (function a) → % 12.51/12.78 Iff (Eq a (identity_relation a_1)) (And (Eq (relation_dom a) a_1) (∀ (C : Iota), in C a_1 → Eq (apply a C) C))) % 12.51/12.78 True % 12.51/12.78 Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), % 12.51/12.78 Or (Eq (And (relation a) (function a)) False) % 12.51/12.78 (Eq (Iff (Eq a (identity_relation a_1)) (And (Eq (relation_dom a) a_1) (∀ (C : Iota), in C a_1 → Eq (apply a C) C))) % 12.51/12.78 True) % 12.51/12.78 Clause #187 (by clausification #[186]): ∀ (a a_1 : Iota), % 12.51/12.78 Or % 12.51/12.78 (Eq (Iff (Eq a (identity_relation a_1)) (And (Eq (relation_dom a) a_1) (∀ (C : Iota), in C a_1 → Eq (apply a C) C))) % 12.51/12.78 True) % 12.51/12.78 (Or (Eq (relation a) False) (Eq (function a) False)) % 12.51/12.78 Clause #189 (by clausification #[187]): ∀ (a a_1 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) % 12.51/12.78 (Or (Eq (Eq a (identity_relation a_1)) False) % 12.51/12.78 (Eq (And (Eq (relation_dom a) a_1) (∀ (C : Iota), in C a_1 → Eq (apply a C) C)) True))) % 12.51/12.78 Clause #260 (by clausification #[62]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) (Or (Eq (one_to_one a) True) (Ne (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 12.51/12.78 Clause #261 (by superposition #[260, 32]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (function (identity_relation a)) False) % 12.51/12.78 (Or (Eq (one_to_one (identity_relation a)) True) % 12.51/12.78 (Or (Ne (skS.0 1 (identity_relation a) a_1) (skS.0 2 (identity_relation a) a_1 a_2)) (Eq False True))) % 12.51/12.78 Clause #271 (by clausification #[64]): ∀ (a a_1 a_2 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) (Or (Eq (one_to_one a) True) (Eq (in (skS.0 2 a a_1 a_2) (relation_dom a)) True))) % 12.51/12.78 Clause #272 (by clausification #[64]): ∀ (a a_1 : Iota), % 12.51/12.78 Or (Eq (relation a) False) % 12.51/12.78 (Or (Eq (function a) False) (Or (Eq (one_to_one a) True) (Eq (in (skS.0 1 a a_1) (relation_dom a)) True))) % 12.51/12.78 Clause #273 (by superposition #[271, 32]): ∀ (a a_1 a_2 : Iota), % 12.62/12.81 Or (Eq (function (identity_relation a)) False) % 12.62/12.81 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.81 (Or (Eq (in (skS.0 2 (identity_relation a) a_1 a_2) (relation_dom (identity_relation a))) True) (Eq False True))) % 12.62/12.81 Clause #291 (by clausification #[66]): ∀ (a a_1 a_2 : Iota), % 12.62/12.81 Or (Eq (function (identity_relation a)) False) % 12.62/12.81 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.81 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) % 12.62/12.81 (apply (identity_relation a) (skS.0 2 (identity_relation a) a_1 a_2)))) % 12.62/12.81 Clause #292 (by forward demodulation #[291, 103]): ∀ (a a_1 a_2 : Iota), % 12.62/12.81 Or (Eq True False) % 12.62/12.81 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.81 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) % 12.62/12.81 (apply (identity_relation a) (skS.0 2 (identity_relation a) a_1 a_2)))) % 12.62/12.81 Clause #293 (by clausification #[292]): ∀ (a a_1 a_2 : Iota), % 12.62/12.81 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.81 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) % 12.62/12.81 (apply (identity_relation a) (skS.0 2 (identity_relation a) a_1 a_2))) % 12.62/12.81 Clause #362 (by superposition #[272, 32]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq (function (identity_relation a)) False) % 12.62/12.81 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.81 (Or (Eq (in (skS.0 1 (identity_relation a) a_1) (relation_dom (identity_relation a))) True) (Eq False True))) % 12.62/12.81 Clause #406 (by clausification #[189]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq (relation a) False) % 12.62/12.81 (Or (Eq (function a) False) % 12.62/12.81 (Or (Eq (And (Eq (relation_dom a) a_1) (∀ (C : Iota), in C a_1 → Eq (apply a C) C)) True) % 12.62/12.81 (Ne a (identity_relation a_1)))) % 12.62/12.81 Clause #407 (by clausification #[406]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq (relation a) False) % 12.62/12.81 (Or (Eq (function a) False) % 12.62/12.81 (Or (Ne a (identity_relation a_1)) (Eq (∀ (C : Iota), in C a_1 → Eq (apply a C) C) True))) % 12.62/12.81 Clause #408 (by clausification #[406]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq (relation a) False) % 12.62/12.81 (Or (Eq (function a) False) (Or (Ne a (identity_relation a_1)) (Eq (Eq (relation_dom a) a_1) True))) % 12.62/12.81 Clause #409 (by clausification #[407]): ∀ (a a_1 a_2 : Iota), % 12.62/12.81 Or (Eq (relation a) False) % 12.62/12.81 (Or (Eq (function a) False) (Or (Ne a (identity_relation a_1)) (Eq (in a_2 a_1 → Eq (apply a a_2) a_2) True))) % 12.62/12.81 Clause #410 (by clausification #[409]): ∀ (a a_1 a_2 : Iota), % 12.62/12.81 Or (Eq (relation a) False) % 12.62/12.81 (Or (Eq (function a) False) % 12.62/12.81 (Or (Ne a (identity_relation a_1)) (Or (Eq (in a_2 a_1) False) (Eq (Eq (apply a a_2) a_2) True)))) % 12.62/12.81 Clause #411 (by clausification #[410]): ∀ (a a_1 a_2 : Iota), % 12.62/12.81 Or (Eq (relation a) False) % 12.62/12.81 (Or (Eq (function a) False) (Or (Ne a (identity_relation a_1)) (Or (Eq (in a_2 a_1) False) (Eq (apply a a_2) a_2)))) % 12.62/12.81 Clause #412 (by destructive equality resolution #[411]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq (relation (identity_relation a)) False) % 12.62/12.81 (Or (Eq (function (identity_relation a)) False) % 12.62/12.81 (Or (Eq (in a_1 a) False) (Eq (apply (identity_relation a) a_1) a_1))) % 12.62/12.81 Clause #413 (by forward demodulation #[412, 32]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq True False) % 12.62/12.81 (Or (Eq (function (identity_relation a)) False) % 12.62/12.81 (Or (Eq (in a_1 a) False) (Eq (apply (identity_relation a) a_1) a_1))) % 12.62/12.81 Clause #414 (by clausification #[413]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq (function (identity_relation a)) False) (Or (Eq (in a_1 a) False) (Eq (apply (identity_relation a) a_1) a_1)) % 12.62/12.81 Clause #415 (by superposition #[414, 103]): ∀ (a a_1 : Iota), Or (Eq (in a a_1) False) (Or (Eq (apply (identity_relation a_1) a) a) (Eq False True)) % 12.62/12.81 Clause #416 (by clausification #[415]): ∀ (a a_1 : Iota), Or (Eq (in a a_1) False) (Eq (apply (identity_relation a_1) a) a) % 12.62/12.81 Clause #423 (by clausification #[408]): ∀ (a a_1 : Iota), % 12.62/12.81 Or (Eq (relation a) False) (Or (Eq (function a) False) (Or (Ne a (identity_relation a_1)) (Eq (relation_dom a) a_1))) % 12.62/12.81 Clause #424 (by destructive equality resolution #[423]): ∀ (a : Iota), % 12.62/12.81 Or (Eq (relation (identity_relation a)) False) % 12.62/12.81 (Or (Eq (function (identity_relation a)) False) (Eq (relation_dom (identity_relation a)) a)) % 12.62/12.81 Clause #425 (by forward demodulation #[424, 32]): ∀ (a : Iota), % 12.62/12.84 Or (Eq True False) (Or (Eq (function (identity_relation a)) False) (Eq (relation_dom (identity_relation a)) a)) % 12.62/12.84 Clause #426 (by clausification #[425]): ∀ (a : Iota), Or (Eq (function (identity_relation a)) False) (Eq (relation_dom (identity_relation a)) a) % 12.62/12.84 Clause #427 (by superposition #[426, 103]): ∀ (a : Iota), Or (Eq (relation_dom (identity_relation a)) a) (Eq False True) % 12.62/12.84 Clause #428 (by clausification #[427]): ∀ (a : Iota), Eq (relation_dom (identity_relation a)) a % 12.62/12.84 Clause #475 (by clausification #[362]): ∀ (a a_1 : Iota), % 12.62/12.84 Or (Eq (function (identity_relation a)) False) % 12.62/12.84 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (in (skS.0 1 (identity_relation a) a_1) (relation_dom (identity_relation a))) True)) % 12.62/12.84 Clause #476 (by forward demodulation #[475, 103]): ∀ (a a_1 : Iota), % 12.62/12.84 Or (Eq True False) % 12.62/12.84 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (in (skS.0 1 (identity_relation a) a_1) (relation_dom (identity_relation a))) True)) % 12.62/12.84 Clause #477 (by clausification #[476]): ∀ (a a_1 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (in (skS.0 1 (identity_relation a) a_1) (relation_dom (identity_relation a))) True) % 12.62/12.84 Clause #478 (by forward demodulation #[477, 428]): ∀ (a a_1 : Iota), Or (Eq (one_to_one (identity_relation a)) True) (Eq (in (skS.0 1 (identity_relation a) a_1) a) True) % 12.62/12.84 Clause #484 (by superposition #[478, 416]): ∀ (a a_1 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Or (Eq True False) % 12.62/12.84 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) (skS.0 1 (identity_relation a) a_1))) % 12.62/12.84 Clause #635 (by clausification #[261]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (function (identity_relation a)) False) % 12.62/12.84 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Ne (skS.0 1 (identity_relation a) a_1) (skS.0 2 (identity_relation a) a_1 a_2))) % 12.62/12.84 Clause #636 (by forward demodulation #[635, 103]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq True False) % 12.62/12.84 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Ne (skS.0 1 (identity_relation a) a_1) (skS.0 2 (identity_relation a) a_1 a_2))) % 12.62/12.84 Clause #637 (by clausification #[636]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Ne (skS.0 1 (identity_relation a) a_1) (skS.0 2 (identity_relation a) a_1 a_2)) % 12.62/12.84 Clause #726 (by clausification #[273]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (function (identity_relation a)) False) % 12.62/12.84 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (in (skS.0 2 (identity_relation a) a_1 a_2) (relation_dom (identity_relation a))) True)) % 12.62/12.84 Clause #727 (by forward demodulation #[726, 103]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq True False) % 12.62/12.84 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (in (skS.0 2 (identity_relation a) a_1 a_2) (relation_dom (identity_relation a))) True)) % 12.62/12.84 Clause #728 (by clausification #[727]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (in (skS.0 2 (identity_relation a) a_1 a_2) (relation_dom (identity_relation a))) True) % 12.62/12.84 Clause #729 (by forward demodulation #[728, 428]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) (Eq (in (skS.0 2 (identity_relation a) a_1 a_2) a) True) % 12.62/12.84 Clause #734 (by superposition #[729, 416]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Or (Eq True False) % 12.62/12.84 (Eq (apply (identity_relation a) (skS.0 2 (identity_relation a) a_1 a_2)) % 12.62/12.84 (skS.0 2 (identity_relation a) a_1 a_2))) % 12.62/12.84 Clause #940 (by clausification #[484]): ∀ (a a_1 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) (skS.0 1 (identity_relation a) a_1)) % 12.62/12.84 Clause #1007 (by clausification #[734]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.84 (Eq (apply (identity_relation a) (skS.0 2 (identity_relation a) a_1 a_2)) (skS.0 2 (identity_relation a) a_1 a_2)) % 12.62/12.84 Clause #1008 (by superposition #[1007, 293]): ∀ (a a_1 a_2 : Iota), % 12.62/12.84 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.85 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.85 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) (skS.0 2 (identity_relation a) a_1 a_2))) % 12.62/12.85 Clause #1011 (by eliminate duplicate literals #[1008]): ∀ (a a_1 a_2 : Iota), % 12.62/12.85 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.85 (Eq (apply (identity_relation a) (skS.0 1 (identity_relation a) a_1)) (skS.0 2 (identity_relation a) a_1 a_2)) % 12.62/12.85 Clause #1012 (by superposition #[1011, 940]): ∀ (a a_1 a_2 : Iota), % 12.62/12.85 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.85 (Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.85 (Eq (skS.0 2 (identity_relation a) a_1 a_2) (skS.0 1 (identity_relation a) a_1))) % 12.62/12.85 Clause #1089 (by eliminate duplicate literals #[1012]): ∀ (a a_1 a_2 : Iota), % 12.62/12.85 Or (Eq (one_to_one (identity_relation a)) True) % 12.62/12.85 (Eq (skS.0 2 (identity_relation a) a_1 a_2) (skS.0 1 (identity_relation a) a_1)) % 12.62/12.85 Clause #1090 (by forward contextual literal cutting #[1089, 637]): ∀ (a : Iota), Eq (one_to_one (identity_relation a)) True % 12.62/12.85 Clause #1114 (by superposition #[1090, 49]): Eq True False % 12.62/12.85 Clause #1117 (by clausification #[1114]): False % 12.62/12.85 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------