%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET994+1 : TPTP v9.2.0. Released v3.2.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:00:47 PM UTC 2025 % Result : Theorem 13.91s 14.09s % Output : Proof 13.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET994+1 : TPTP v9.2.0. Released v3.2.0. % 0.13/0.14 % Command : duper %s % 0.13/0.35 % Computer : n009.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 13:38:23 EDT 2025 % 0.13/0.35 % CPUTime : % 13.91/14.09 SZS status Theorem for theBenchmark.p % 13.91/14.09 SZS output start Proof for theBenchmark.p % 13.91/14.09 Clause #3 (by assumption #[]): Eq (∀ (A : Iota), Exists fun B => element B A) True % 13.91/14.09 Clause #6 (by assumption #[]): Eq (empty empty_set) True % 13.91/14.09 Clause #19 (by assumption #[]): Eq % 13.91/14.09 (∀ (A : Iota), % 13.91/14.09 Exists fun B => % 13.91/14.09 And (And (And (relation B) (function B)) (Eq (relation_dom B) A)) (∀ (C : Iota), in C A → Eq (apply B C) n0)) % 13.91/14.09 True % 13.91/14.09 Clause #20 (by assumption #[]): Eq % 13.91/14.09 (∀ (A : Iota), % 13.91/14.09 Exists fun B => % 13.91/14.09 And (And (And (relation B) (function B)) (Eq (relation_dom B) A)) (∀ (C : Iota), in C A → Eq (apply B C) n1)) % 13.91/14.09 True % 13.91/14.09 Clause #21 (by assumption #[]): Eq (empty n0) True % 13.91/14.09 Clause #22 (by assumption #[]): Eq (Not (empty n1)) True % 13.91/14.09 Clause #23 (by assumption #[]): Eq % 13.91/14.09 (Not % 13.91/14.09 (∀ (A : Iota), % 13.91/14.09 (∀ (B : Iota), % 13.91/14.09 And (relation B) (function B) → % 13.91/14.09 ∀ (C : Iota), % 13.91/14.09 And (relation C) (function C) → And (Eq (relation_dom B) A) (Eq (relation_dom C) A) → Eq B C) → % 13.91/14.09 Eq A empty_set)) % 13.91/14.09 True % 13.91/14.09 Clause #25 (by assumption #[]): Eq (∀ (A B : Iota), element A B → Or (empty B) (in A B)) True % 13.91/14.09 Clause #29 (by assumption #[]): Eq (∀ (A : Iota), empty A → Eq A empty_set) True % 13.91/14.09 Clause #32 (by clausification #[22]): Eq (empty n1) False % 13.91/14.09 Clause #51 (by clausification #[3]): ∀ (a : Iota), Eq (Exists fun B => element B a) True % 13.91/14.09 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), Eq (element (skS.0 0 a a_1) a) True % 13.91/14.09 Clause #66 (by clausification #[29]): ∀ (a : Iota), Eq (empty a → Eq a empty_set) True % 13.91/14.09 Clause #67 (by clausification #[66]): ∀ (a : Iota), Or (Eq (empty a) False) (Eq (Eq a empty_set) True) % 13.91/14.09 Clause #68 (by clausification #[67]): ∀ (a : Iota), Or (Eq (empty a) False) (Eq a empty_set) % 13.91/14.09 Clause #69 (by superposition #[68, 21]): Or (Eq n0 empty_set) (Eq False True) % 13.91/14.09 Clause #74 (by clausification #[69]): Eq n0 empty_set % 13.91/14.09 Clause #80 (by clausification #[23]): Eq % 13.91/14.09 (∀ (A : Iota), % 13.91/14.09 (∀ (B : Iota), % 13.91/14.09 And (relation B) (function B) → % 13.91/14.09 ∀ (C : Iota), And (relation C) (function C) → And (Eq (relation_dom B) A) (Eq (relation_dom C) A) → Eq B C) → % 13.91/14.09 Eq A empty_set) % 13.91/14.09 False % 13.91/14.09 Clause #81 (by clausification #[80]): ∀ (a : Iota), % 13.91/14.09 Eq % 13.91/14.09 (Not % 13.91/14.09 ((∀ (B : Iota), % 13.91/14.09 And (relation B) (function B) → % 13.91/14.09 ∀ (C : Iota), % 13.91/14.09 And (relation C) (function C) → % 13.91/14.09 And (Eq (relation_dom B) (skS.0 3 a)) (Eq (relation_dom C) (skS.0 3 a)) → Eq B C) → % 13.91/14.09 Eq (skS.0 3 a) empty_set)) % 13.91/14.09 True % 13.91/14.09 Clause #82 (by clausification #[81]): ∀ (a : Iota), % 13.91/14.09 Eq % 13.91/14.09 ((∀ (B : Iota), % 13.91/14.09 And (relation B) (function B) → % 13.91/14.09 ∀ (C : Iota), % 13.91/14.09 And (relation C) (function C) → % 13.91/14.09 And (Eq (relation_dom B) (skS.0 3 a)) (Eq (relation_dom C) (skS.0 3 a)) → Eq B C) → % 13.91/14.09 Eq (skS.0 3 a) empty_set) % 13.91/14.09 False % 13.91/14.09 Clause #83 (by clausification #[82]): ∀ (a : Iota), % 13.91/14.09 Eq % 13.91/14.09 (∀ (B : Iota), % 13.91/14.09 And (relation B) (function B) → % 13.91/14.09 ∀ (C : Iota), % 13.91/14.09 And (relation C) (function C) → % 13.91/14.09 And (Eq (relation_dom B) (skS.0 3 a)) (Eq (relation_dom C) (skS.0 3 a)) → Eq B C) % 13.91/14.09 True % 13.91/14.09 Clause #84 (by clausification #[82]): ∀ (a : Iota), Eq (Eq (skS.0 3 a) empty_set) False % 13.91/14.09 Clause #85 (by clausification #[83]): ∀ (a a_1 : Iota), % 13.91/14.09 Eq % 13.91/14.09 (And (relation a) (function a) → % 13.91/14.09 ∀ (C : Iota), % 13.91/14.09 And (relation C) (function C) → % 13.91/14.09 And (Eq (relation_dom a) (skS.0 3 a_1)) (Eq (relation_dom C) (skS.0 3 a_1)) → Eq a C) % 13.91/14.09 True % 13.91/14.09 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), % 13.91/14.09 Or (Eq (And (relation a) (function a)) False) % 13.91/14.09 (Eq % 13.91/14.09 (∀ (C : Iota), % 13.91/14.09 And (relation C) (function C) → % 13.91/14.09 And (Eq (relation_dom a) (skS.0 3 a_1)) (Eq (relation_dom C) (skS.0 3 a_1)) → Eq a C) % 13.91/14.09 True) % 13.91/14.09 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), % 13.91/14.09 Or % 13.91/14.09 (Eq % 13.91/14.09 (∀ (C : Iota), % 13.91/14.09 And (relation C) (function C) → % 13.91/14.09 And (Eq (relation_dom a) (skS.0 3 a_1)) (Eq (relation_dom C) (skS.0 3 a_1)) → Eq a C) % 13.91/14.09 True) % 13.91/14.09 (Or (Eq (relation a) False) (Eq (function a) False)) % 13.91/14.12 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Eq % 13.91/14.12 (And (relation a_1) (function a_1) → % 13.91/14.12 And (Eq (relation_dom a) (skS.0 3 a_2)) (Eq (relation_dom a_1) (skS.0 3 a_2)) → Eq a a_1) % 13.91/14.12 True)) % 13.91/14.12 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Or (Eq (And (relation a_1) (function a_1)) False) % 13.91/14.12 (Eq (And (Eq (relation_dom a) (skS.0 3 a_2)) (Eq (relation_dom a_1) (skS.0 3 a_2)) → Eq a a_1) True))) % 13.91/14.12 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Or (Eq (And (Eq (relation_dom a) (skS.0 3 a_1)) (Eq (relation_dom a_2) (skS.0 3 a_1)) → Eq a a_2) True) % 13.91/14.12 (Or (Eq (relation a_2) False) (Eq (function a_2) False)))) % 13.91/14.12 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Or (Eq (relation a_1) False) % 13.91/14.12 (Or (Eq (function a_1) False) % 13.91/14.12 (Or (Eq (And (Eq (relation_dom a) (skS.0 3 a_2)) (Eq (relation_dom a_1) (skS.0 3 a_2))) False) % 13.91/14.12 (Eq (Eq a a_1) True))))) % 13.91/14.12 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Or (Eq (relation a_1) False) % 13.91/14.12 (Or (Eq (function a_1) False) % 13.91/14.12 (Or (Eq (Eq a a_1) True) % 13.91/14.12 (Or (Eq (Eq (relation_dom a) (skS.0 3 a_2)) False) (Eq (Eq (relation_dom a_1) (skS.0 3 a_2)) False)))))) % 13.91/14.12 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Or (Eq (relation a_1) False) % 13.91/14.12 (Or (Eq (function a_1) False) % 13.91/14.12 (Or (Eq (Eq (relation_dom a) (skS.0 3 a_2)) False) % 13.91/14.12 (Or (Eq (Eq (relation_dom a_1) (skS.0 3 a_2)) False) (Eq a a_1)))))) % 13.91/14.12 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Or (Eq (relation a_1) False) % 13.91/14.12 (Or (Eq (function a_1) False) % 13.91/14.12 (Or (Eq (Eq (relation_dom a_1) (skS.0 3 a_2)) False) (Or (Eq a a_1) (Ne (relation_dom a) (skS.0 3 a_2))))))) % 13.91/14.12 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), % 13.91/14.12 Or (Eq (relation a) False) % 13.91/14.12 (Or (Eq (function a) False) % 13.91/14.12 (Or (Eq (relation a_1) False) % 13.91/14.12 (Or (Eq (function a_1) False) % 13.91/14.12 (Or (Eq a a_1) (Or (Ne (relation_dom a) (skS.0 3 a_2)) (Ne (relation_dom a_1) (skS.0 3 a_2))))))) % 13.91/14.12 Clause #158 (by clausification #[25]): ∀ (a : Iota), Eq (∀ (B : Iota), element a B → Or (empty B) (in a B)) True % 13.91/14.12 Clause #159 (by clausification #[158]): ∀ (a a_1 : Iota), Eq (element a a_1 → Or (empty a_1) (in a a_1)) True % 13.91/14.12 Clause #160 (by clausification #[159]): ∀ (a a_1 : Iota), Or (Eq (element a a_1) False) (Eq (Or (empty a_1) (in a a_1)) True) % 13.91/14.12 Clause #161 (by clausification #[160]): ∀ (a a_1 : Iota), Or (Eq (element a a_1) False) (Or (Eq (empty a_1) True) (Eq (in a a_1) True)) % 13.91/14.12 Clause #162 (by superposition #[161, 52]): ∀ (a a_1 : Iota), Or (Eq (empty a) True) (Or (Eq (in (skS.0 0 a a_1) a) True) (Eq False True)) % 13.91/14.12 Clause #182 (by clausification #[84]): ∀ (a : Iota), Ne (skS.0 3 a) empty_set % 13.91/14.12 Clause #185 (by clausification #[19]): ∀ (a : Iota), % 13.91/14.12 Eq % 13.91/14.12 (Exists fun B => % 13.91/14.12 And (And (And (relation B) (function B)) (Eq (relation_dom B) a)) (∀ (C : Iota), in C a → Eq (apply B C) n0)) % 13.91/14.12 True % 13.91/14.12 Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), % 13.91/14.12 Eq % 13.91/14.12 (And (And (And (relation (skS.0 10 a a_1)) (function (skS.0 10 a a_1))) (Eq (relation_dom (skS.0 10 a a_1)) a)) % 13.91/14.12 (∀ (C : Iota), in C a → Eq (apply (skS.0 10 a a_1) C) n0)) % 13.91/14.12 True % 13.91/14.12 Clause #187 (by clausification #[186]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), in C a → Eq (apply (skS.0 10 a a_1) C) n0) True % 13.91/14.12 Clause #188 (by clausification #[186]): ∀ (a a_1 : Iota), % 13.91/14.12 Eq (And (And (relation (skS.0 10 a a_1)) (function (skS.0 10 a a_1))) (Eq (relation_dom (skS.0 10 a a_1)) a)) True % 13.91/14.12 Clause #189 (by clausification #[187]): ∀ (a a_1 a_2 : Iota), Eq (in a a_1 → Eq (apply (skS.0 10 a_1 a_2) a) n0) True % 13.91/14.14 Clause #190 (by clausification #[189]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Eq (Eq (apply (skS.0 10 a_1 a_2) a) n0) True) % 13.91/14.14 Clause #191 (by clausification #[190]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Eq (apply (skS.0 10 a_1 a_2) a) n0) % 13.91/14.14 Clause #192 (by forward demodulation #[191, 74]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Eq (apply (skS.0 10 a_1 a_2) a) empty_set) % 13.91/14.14 Clause #199 (by clausification #[20]): ∀ (a : Iota), % 13.91/14.14 Eq % 13.91/14.14 (Exists fun B => % 13.91/14.14 And (And (And (relation B) (function B)) (Eq (relation_dom B) a)) (∀ (C : Iota), in C a → Eq (apply B C) n1)) % 13.91/14.14 True % 13.91/14.14 Clause #200 (by clausification #[199]): ∀ (a a_1 : Iota), % 13.91/14.14 Eq % 13.91/14.14 (And (And (And (relation (skS.0 11 a a_1)) (function (skS.0 11 a a_1))) (Eq (relation_dom (skS.0 11 a a_1)) a)) % 13.91/14.14 (∀ (C : Iota), in C a → Eq (apply (skS.0 11 a a_1) C) n1)) % 13.91/14.14 True % 13.91/14.14 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), in C a → Eq (apply (skS.0 11 a a_1) C) n1) True % 13.91/14.14 Clause #202 (by clausification #[200]): ∀ (a a_1 : Iota), % 13.91/14.14 Eq (And (And (relation (skS.0 11 a a_1)) (function (skS.0 11 a a_1))) (Eq (relation_dom (skS.0 11 a a_1)) a)) True % 13.91/14.14 Clause #203 (by clausification #[201]): ∀ (a a_1 a_2 : Iota), Eq (in a a_1 → Eq (apply (skS.0 11 a_1 a_2) a) n1) True % 13.91/14.14 Clause #204 (by clausification #[203]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Eq (Eq (apply (skS.0 11 a_1 a_2) a) n1) True) % 13.91/14.14 Clause #205 (by clausification #[204]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a a_1) False) (Eq (apply (skS.0 11 a_1 a_2) a) n1) % 13.91/14.14 Clause #287 (by clausification #[162]): ∀ (a a_1 : Iota), Or (Eq (empty a) True) (Eq (in (skS.0 0 a a_1) a) True) % 13.91/14.14 Clause #292 (by superposition #[287, 192]): ∀ (a a_1 a_2 : Iota), % 13.91/14.14 Or (Eq (empty a) True) (Or (Eq True False) (Eq (apply (skS.0 10 a a_1) (skS.0 0 a a_2)) empty_set)) % 13.91/14.14 Clause #293 (by superposition #[287, 205]): ∀ (a a_1 a_2 : Iota), Or (Eq (empty a) True) (Or (Eq True False) (Eq (apply (skS.0 11 a a_1) (skS.0 0 a a_2)) n1)) % 13.91/14.14 Clause #362 (by clausification #[188]): ∀ (a a_1 : Iota), Eq (Eq (relation_dom (skS.0 10 a a_1)) a) True % 13.91/14.14 Clause #363 (by clausification #[188]): ∀ (a a_1 : Iota), Eq (And (relation (skS.0 10 a a_1)) (function (skS.0 10 a a_1))) True % 13.91/14.14 Clause #364 (by clausification #[362]): ∀ (a a_1 : Iota), Eq (relation_dom (skS.0 10 a a_1)) a % 13.91/14.14 Clause #367 (by clausification #[363]): ∀ (a a_1 : Iota), Eq (function (skS.0 10 a a_1)) True % 13.91/14.14 Clause #368 (by clausification #[363]): ∀ (a a_1 : Iota), Eq (relation (skS.0 10 a a_1)) True % 13.91/14.14 Clause #370 (by superposition #[368, 95]): ∀ (a a_1 a_2 a_3 : Iota), % 13.91/14.14 Or (Eq True False) % 13.91/14.14 (Or (Eq (function (skS.0 10 a a_1)) False) % 13.91/14.14 (Or (Eq (relation a_2) False) % 13.91/14.14 (Or (Eq (function a_2) False) % 13.91/14.14 (Or (Eq (skS.0 10 a a_1) a_2) % 13.91/14.14 (Or (Ne (relation_dom (skS.0 10 a a_1)) (skS.0 3 a_3)) (Ne (relation_dom a_2) (skS.0 3 a_3))))))) % 13.91/14.14 Clause #371 (by clausification #[202]): ∀ (a a_1 : Iota), Eq (Eq (relation_dom (skS.0 11 a a_1)) a) True % 13.91/14.14 Clause #372 (by clausification #[202]): ∀ (a a_1 : Iota), Eq (And (relation (skS.0 11 a a_1)) (function (skS.0 11 a a_1))) True % 13.91/14.14 Clause #373 (by clausification #[371]): ∀ (a a_1 : Iota), Eq (relation_dom (skS.0 11 a a_1)) a % 13.91/14.14 Clause #374 (by clausification #[372]): ∀ (a a_1 : Iota), Eq (function (skS.0 11 a a_1)) True % 13.91/14.14 Clause #375 (by clausification #[372]): ∀ (a a_1 : Iota), Eq (relation (skS.0 11 a a_1)) True % 13.91/14.14 Clause #403 (by clausification #[292]): ∀ (a a_1 a_2 : Iota), Or (Eq (empty a) True) (Eq (apply (skS.0 10 a a_1) (skS.0 0 a a_2)) empty_set) % 13.91/14.14 Clause #411 (by clausification #[293]): ∀ (a a_1 a_2 : Iota), Or (Eq (empty a) True) (Eq (apply (skS.0 11 a a_1) (skS.0 0 a a_2)) n1) % 13.91/14.14 Clause #476 (by clausification #[370]): ∀ (a a_1 a_2 a_3 : Iota), % 13.91/14.14 Or (Eq (function (skS.0 10 a a_1)) False) % 13.91/14.14 (Or (Eq (relation a_2) False) % 13.91/14.14 (Or (Eq (function a_2) False) % 13.91/14.14 (Or (Eq (skS.0 10 a a_1) a_2) % 13.91/14.14 (Or (Ne (relation_dom (skS.0 10 a a_1)) (skS.0 3 a_3)) (Ne (relation_dom a_2) (skS.0 3 a_3)))))) % 13.99/14.17 Clause #477 (by forward demodulation #[476, 364]): ∀ (a a_1 a_2 a_3 : Iota), % 13.99/14.17 Or (Eq (function (skS.0 10 a a_1)) False) % 13.99/14.17 (Or (Eq (relation a_2) False) % 13.99/14.17 (Or (Eq (function a_2) False) % 13.99/14.17 (Or (Eq (skS.0 10 a a_1) a_2) (Or (Ne a (skS.0 3 a_3)) (Ne (relation_dom a_2) (skS.0 3 a_3)))))) % 13.99/14.17 Clause #478 (by destructive equality resolution #[477]): ∀ (a a_1 a_2 : Iota), % 13.99/14.17 Or (Eq (function (skS.0 10 (skS.0 3 a) a_1)) False) % 13.99/14.17 (Or (Eq (relation a_2) False) % 13.99/14.17 (Or (Eq (function a_2) False) (Or (Eq (skS.0 10 (skS.0 3 a) a_1) a_2) (Ne (relation_dom a_2) (skS.0 3 a))))) % 13.99/14.17 Clause #479 (by superposition #[478, 367]): ∀ (a a_1 a_2 : Iota), % 13.99/14.17 Or (Eq (relation a) False) % 13.99/14.17 (Or (Eq (function a) False) % 13.99/14.17 (Or (Eq (skS.0 10 (skS.0 3 a_1) a_2) a) (Or (Ne (relation_dom a) (skS.0 3 a_1)) (Eq False True)))) % 13.99/14.17 Clause #481 (by clausification #[479]): ∀ (a a_1 a_2 : Iota), % 13.99/14.17 Or (Eq (relation a) False) % 13.99/14.17 (Or (Eq (function a) False) (Or (Eq (skS.0 10 (skS.0 3 a_1) a_2) a) (Ne (relation_dom a) (skS.0 3 a_1)))) % 13.99/14.17 Clause #487 (by superposition #[481, 375]): ∀ (a a_1 a_2 a_3 : Iota), % 13.99/14.17 Or (Eq (function (skS.0 11 a a_1)) False) % 13.99/14.17 (Or (Eq (skS.0 10 (skS.0 3 a_2) a_3) (skS.0 11 a a_1)) % 13.99/14.17 (Or (Ne (relation_dom (skS.0 11 a a_1)) (skS.0 3 a_2)) (Eq False True))) % 13.99/14.17 Clause #895 (by clausification #[487]): ∀ (a a_1 a_2 a_3 : Iota), % 13.99/14.17 Or (Eq (function (skS.0 11 a a_1)) False) % 13.99/14.17 (Or (Eq (skS.0 10 (skS.0 3 a_2) a_3) (skS.0 11 a a_1)) (Ne (relation_dom (skS.0 11 a a_1)) (skS.0 3 a_2))) % 13.99/14.17 Clause #896 (by forward demodulation #[895, 373]): ∀ (a a_1 a_2 a_3 : Iota), % 13.99/14.17 Or (Eq (function (skS.0 11 a a_1)) False) (Or (Eq (skS.0 10 (skS.0 3 a_2) a_3) (skS.0 11 a a_1)) (Ne a (skS.0 3 a_2))) % 13.99/14.17 Clause #897 (by destructive equality resolution #[896]): ∀ (a a_1 a_2 : Iota), % 13.99/14.17 Or (Eq (function (skS.0 11 (skS.0 3 a) a_1)) False) (Eq (skS.0 10 (skS.0 3 a) a_2) (skS.0 11 (skS.0 3 a) a_1)) % 13.99/14.17 Clause #898 (by superposition #[897, 374]): ∀ (a a_1 a_2 : Iota), Or (Eq (skS.0 10 (skS.0 3 a) a_1) (skS.0 11 (skS.0 3 a) a_2)) (Eq False True) % 13.99/14.17 Clause #899 (by clausification #[898]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 10 (skS.0 3 a) a_1) (skS.0 11 (skS.0 3 a) a_2) % 13.99/14.17 Clause #905 (by superposition #[899, 403]): ∀ (a a_1 a_2 : Iota), % 13.99/14.17 Or (Eq (empty (skS.0 3 a)) True) (Eq (apply (skS.0 11 (skS.0 3 a) a_1) (skS.0 0 (skS.0 3 a) a_2)) empty_set) % 13.99/14.17 Clause #1056 (by superposition #[905, 411]): ∀ (a : Iota), Or (Eq (empty (skS.0 3 a)) True) (Or (Eq (empty (skS.0 3 a)) True) (Eq empty_set n1)) % 13.99/14.17 Clause #1057 (by eliminate duplicate literals #[1056]): ∀ (a : Iota), Or (Eq (empty (skS.0 3 a)) True) (Eq empty_set n1) % 13.99/14.17 Clause #1060 (by superposition #[1057, 68]): ∀ (a : Iota), Or (Eq empty_set n1) (Or (Eq True False) (Eq (skS.0 3 a) empty_set)) % 13.99/14.17 Clause #1073 (by clausification #[1060]): ∀ (a : Iota), Or (Eq empty_set n1) (Eq (skS.0 3 a) empty_set) % 13.99/14.17 Clause #1074 (by forward contextual literal cutting #[1073, 182]): Eq empty_set n1 % 13.99/14.17 Clause #1075 (by backward demodulation #[1074, 32]): Eq (empty empty_set) False % 13.99/14.17 Clause #1087 (by superposition #[1075, 6]): Eq False True % 13.99/14.17 Clause #1088 (by clausification #[1087]): False % 13.99/14.17 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------