%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM021+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.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:45:48 PM UTC 2025 % Result : Theorem 249.89s 250.07s % Output : Proof 250.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COM021+1 : TPTP v9.2.0. Released v4.0.0. % 0.14/0.14 % Command : duper %s % 0.14/0.34 % Computer : n025.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 : Thu Oct 2 15:55:08 EDT 2025 % 0.14/0.35 % CPUTime : % 249.89/250.07 SZS status Theorem for theBenchmark.p % 249.89/250.07 SZS output start Proof for theBenchmark.p % 249.89/250.07 Clause #5 (by assumption #[]): Eq % 249.89/250.07 (∀ (W0 W1 W2 : Iota), % 249.89/250.07 And (And (aElement0 W0) (aRewritingSystem0 W1)) (aElement0 W2) → % 249.89/250.07 Iff (sdtmndtplgtdt0 W0 W1 W2) % 249.89/250.07 (Or (aReductOfIn0 W2 W0 W1) % 249.89/250.07 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 W0 W1)) (sdtmndtplgtdt0 W3 W1 W2)))) % 249.89/250.07 True % 249.89/250.07 Clause #7 (by assumption #[]): Eq % 249.89/250.07 (∀ (W0 W1 W2 : Iota), % 249.89/250.07 And (And (aElement0 W0) (aRewritingSystem0 W1)) (aElement0 W2) → % 249.89/250.07 Iff (sdtmndtasgtdt0 W0 W1 W2) (Or (Eq W0 W2) (sdtmndtplgtdt0 W0 W1 W2))) % 249.89/250.07 True % 249.89/250.07 Clause #12 (by assumption #[]): Eq % 249.89/250.07 (∀ (W0 W1 : Iota), % 249.89/250.07 And (aElement0 W0) (aRewritingSystem0 W1) → % 249.89/250.07 ∀ (W2 : Iota), % 249.89/250.07 Iff (aNormalFormOfIn0 W2 W0 W1) % 249.89/250.07 (And (And (aElement0 W2) (sdtmndtasgtdt0 W0 W1 W2)) (Not (Exists fun W3 => aReductOfIn0 W3 W2 W1)))) % 249.89/250.07 True % 249.89/250.07 Clause #14 (by assumption #[]): Eq (aRewritingSystem0 xR) True % 249.89/250.07 Clause #21 (by assumption #[]): Eq (And (And (aElement0 xw) (sdtmndtasgtdt0 xu xR xw)) (sdtmndtasgtdt0 xv xR xw)) True % 249.89/250.07 Clause #22 (by assumption #[]): Eq (aNormalFormOfIn0 xd xw xR) True % 249.89/250.07 Clause #23 (by assumption #[]): Eq (And (And (aElement0 xx) (sdtmndtasgtdt0 xb xR xx)) (sdtmndtasgtdt0 xd xR xx)) True % 249.89/250.07 Clause #24 (by assumption #[]): Eq (Not (sdtmndtasgtdt0 xb xR xd)) True % 249.89/250.07 Clause #42 (by clausification #[24]): Eq (sdtmndtasgtdt0 xb xR xd) False % 249.89/250.07 Clause #53 (by clausification #[5]): ∀ (a : Iota), % 249.89/250.07 Eq % 249.89/250.07 (∀ (W1 W2 : Iota), % 249.89/250.07 And (And (aElement0 a) (aRewritingSystem0 W1)) (aElement0 W2) → % 249.89/250.07 Iff (sdtmndtplgtdt0 a W1 W2) % 249.89/250.07 (Or (aReductOfIn0 W2 a W1) % 249.89/250.07 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a W1)) (sdtmndtplgtdt0 W3 W1 W2)))) % 249.89/250.07 True % 249.89/250.07 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), % 249.89/250.07 Eq % 249.89/250.07 (∀ (W2 : Iota), % 249.89/250.07 And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 W2) → % 249.89/250.07 Iff (sdtmndtplgtdt0 a a_1 W2) % 249.89/250.07 (Or (aReductOfIn0 W2 a a_1) % 249.89/250.07 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a a_1)) (sdtmndtplgtdt0 W3 a_1 W2)))) % 249.89/250.07 True % 249.89/250.07 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 : Iota), % 249.89/250.07 Eq % 249.89/250.07 (And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 a_2) → % 249.89/250.07 Iff (sdtmndtplgtdt0 a a_1 a_2) % 249.89/250.07 (Or (aReductOfIn0 a_2 a a_1) % 249.89/250.07 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a a_1)) (sdtmndtplgtdt0 W3 a_1 a_2)))) % 249.89/250.07 True % 249.89/250.07 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 : Iota), % 249.89/250.07 Or (Eq (And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 a_2)) False) % 249.89/250.07 (Eq % 249.89/250.07 (Iff (sdtmndtplgtdt0 a a_1 a_2) % 249.89/250.07 (Or (aReductOfIn0 a_2 a a_1) % 249.89/250.07 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a a_1)) (sdtmndtplgtdt0 W3 a_1 a_2)))) % 249.89/250.07 True) % 249.89/250.07 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 : Iota), % 249.89/250.07 Or % 249.89/250.07 (Eq % 249.89/250.07 (Iff (sdtmndtplgtdt0 a a_1 a_2) % 249.89/250.07 (Or (aReductOfIn0 a_2 a a_1) % 249.89/250.07 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a a_1)) (sdtmndtplgtdt0 W3 a_1 a_2)))) % 249.89/250.07 True) % 249.89/250.07 (Or (Eq (And (aElement0 a) (aRewritingSystem0 a_1)) False) (Eq (aElement0 a_2) False)) % 249.89/250.07 Clause #59 (by clausification #[57]): ∀ (a a_1 a_2 : Iota), % 249.89/250.07 Or (Eq (And (aElement0 a) (aRewritingSystem0 a_1)) False) % 249.89/250.07 (Or (Eq (aElement0 a_2) False) % 249.89/250.07 (Or (Eq (sdtmndtplgtdt0 a a_1 a_2) False) % 249.89/250.07 (Eq % 249.89/250.07 (Or (aReductOfIn0 a_2 a a_1) % 249.89/250.07 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a a_1)) (sdtmndtplgtdt0 W3 a_1 a_2))) % 249.89/250.07 True))) % 249.89/250.07 Clause #88 (by clausification #[7]): ∀ (a : Iota), % 249.89/250.07 Eq % 249.89/250.07 (∀ (W1 W2 : Iota), % 249.89/250.07 And (And (aElement0 a) (aRewritingSystem0 W1)) (aElement0 W2) → % 249.89/250.07 Iff (sdtmndtasgtdt0 a W1 W2) (Or (Eq a W2) (sdtmndtplgtdt0 a W1 W2))) % 249.89/250.07 True % 249.89/250.07 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), % 249.89/250.07 Eq % 249.89/250.07 (∀ (W2 : Iota), % 249.89/250.07 And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 W2) → % 249.89/250.07 Iff (sdtmndtasgtdt0 a a_1 W2) (Or (Eq a W2) (sdtmndtplgtdt0 a a_1 W2))) % 249.89/250.07 True % 249.89/250.07 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 249.89/250.07 Eq % 249.89/250.07 (And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 a_2) → % 249.89/250.10 Iff (sdtmndtasgtdt0 a a_1 a_2) (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2))) % 249.89/250.10 True % 249.89/250.10 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 249.89/250.10 Or (Eq (And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 a_2)) False) % 249.89/250.10 (Eq (Iff (sdtmndtasgtdt0 a a_1 a_2) (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2))) True) % 249.89/250.10 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 249.89/250.10 Or (Eq (Iff (sdtmndtasgtdt0 a a_1 a_2) (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2))) True) % 249.89/250.10 (Or (Eq (And (aElement0 a) (aRewritingSystem0 a_1)) False) (Eq (aElement0 a_2) False)) % 249.89/250.10 Clause #94 (by clausification #[92]): ∀ (a a_1 a_2 : Iota), % 249.89/250.10 Or (Eq (And (aElement0 a) (aRewritingSystem0 a_1)) False) % 249.89/250.10 (Or (Eq (aElement0 a_2) False) % 249.89/250.10 (Or (Eq (sdtmndtasgtdt0 a a_1 a_2) False) (Eq (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2)) True))) % 249.89/250.10 Clause #162 (by clausification #[21]): Eq (And (aElement0 xw) (sdtmndtasgtdt0 xu xR xw)) True % 249.89/250.10 Clause #164 (by clausification #[162]): Eq (aElement0 xw) True % 249.89/250.10 Clause #196 (by clausification #[12]): ∀ (a : Iota), % 249.89/250.10 Eq % 249.89/250.10 (∀ (W1 : Iota), % 249.89/250.10 And (aElement0 a) (aRewritingSystem0 W1) → % 249.89/250.10 ∀ (W2 : Iota), % 249.89/250.10 Iff (aNormalFormOfIn0 W2 a W1) % 249.89/250.10 (And (And (aElement0 W2) (sdtmndtasgtdt0 a W1 W2)) (Not (Exists fun W3 => aReductOfIn0 W3 W2 W1)))) % 249.89/250.10 True % 249.89/250.10 Clause #197 (by clausification #[196]): ∀ (a a_1 : Iota), % 249.89/250.10 Eq % 249.89/250.10 (And (aElement0 a) (aRewritingSystem0 a_1) → % 249.89/250.10 ∀ (W2 : Iota), % 249.89/250.10 Iff (aNormalFormOfIn0 W2 a a_1) % 249.89/250.10 (And (And (aElement0 W2) (sdtmndtasgtdt0 a a_1 W2)) (Not (Exists fun W3 => aReductOfIn0 W3 W2 a_1)))) % 249.89/250.10 True % 249.89/250.10 Clause #198 (by clausification #[197]): ∀ (a a_1 : Iota), % 249.89/250.10 Or (Eq (And (aElement0 a) (aRewritingSystem0 a_1)) False) % 249.89/250.10 (Eq % 249.89/250.10 (∀ (W2 : Iota), % 249.89/250.10 Iff (aNormalFormOfIn0 W2 a a_1) % 249.89/250.10 (And (And (aElement0 W2) (sdtmndtasgtdt0 a a_1 W2)) (Not (Exists fun W3 => aReductOfIn0 W3 W2 a_1)))) % 249.89/250.10 True) % 249.89/250.10 Clause #199 (by clausification #[198]): ∀ (a a_1 : Iota), % 249.89/250.10 Or % 249.89/250.10 (Eq % 249.89/250.10 (∀ (W2 : Iota), % 249.89/250.10 Iff (aNormalFormOfIn0 W2 a a_1) % 249.89/250.10 (And (And (aElement0 W2) (sdtmndtasgtdt0 a a_1 W2)) (Not (Exists fun W3 => aReductOfIn0 W3 W2 a_1)))) % 249.89/250.10 True) % 249.89/250.10 (Or (Eq (aElement0 a) False) (Eq (aRewritingSystem0 a_1) False)) % 249.89/250.10 Clause #200 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), % 249.89/250.10 Or (Eq (aElement0 a) False) % 249.89/250.10 (Or (Eq (aRewritingSystem0 a_1) False) % 249.89/250.10 (Eq % 249.89/250.10 (Iff (aNormalFormOfIn0 a_2 a a_1) % 249.89/250.10 (And (And (aElement0 a_2) (sdtmndtasgtdt0 a a_1 a_2)) (Not (Exists fun W3 => aReductOfIn0 W3 a_2 a_1)))) % 249.89/250.10 True)) % 249.89/250.10 Clause #202 (by clausification #[200]): ∀ (a a_1 a_2 : Iota), % 249.89/250.10 Or (Eq (aElement0 a) False) % 249.89/250.10 (Or (Eq (aRewritingSystem0 a_1) False) % 249.89/250.10 (Or (Eq (aNormalFormOfIn0 a_2 a a_1) False) % 249.89/250.10 (Eq (And (And (aElement0 a_2) (sdtmndtasgtdt0 a a_1 a_2)) (Not (Exists fun W3 => aReductOfIn0 W3 a_2 a_1))) % 249.89/250.10 True))) % 249.89/250.10 Clause #217 (by clausification #[23]): Eq (sdtmndtasgtdt0 xd xR xx) True % 249.89/250.10 Clause #218 (by clausification #[23]): Eq (And (aElement0 xx) (sdtmndtasgtdt0 xb xR xx)) True % 249.89/250.10 Clause #219 (by clausification #[218]): Eq (sdtmndtasgtdt0 xb xR xx) True % 249.89/250.10 Clause #220 (by clausification #[218]): Eq (aElement0 xx) True % 249.89/250.10 Clause #259 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), % 249.89/250.10 Or (Eq (aElement0 a) False) % 249.89/250.10 (Or (Eq (sdtmndtplgtdt0 a_1 a_2 a) False) % 249.89/250.10 (Or % 249.89/250.10 (Eq % 249.89/250.10 (Or (aReductOfIn0 a a_1 a_2) % 249.89/250.10 (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a_1 a_2)) (sdtmndtplgtdt0 W3 a_2 a))) % 249.89/250.10 True) % 249.89/250.10 (Or (Eq (aElement0 a_1) False) (Eq (aRewritingSystem0 a_2) False)))) % 249.89/250.10 Clause #260 (by clausification #[259]): ∀ (a a_1 a_2 : Iota), % 249.89/250.10 Or (Eq (aElement0 a) False) % 249.89/250.10 (Or (Eq (sdtmndtplgtdt0 a_1 a_2 a) False) % 249.89/250.10 (Or (Eq (aElement0 a_1) False) % 249.89/250.10 (Or (Eq (aRewritingSystem0 a_2) False) % 249.89/250.10 (Or (Eq (aReductOfIn0 a a_1 a_2) True) % 249.89/250.10 (Eq (Exists fun W3 => And (And (aElement0 W3) (aReductOfIn0 W3 a_1 a_2)) (sdtmndtplgtdt0 W3 a_2 a)) % 249.89/250.10 True))))) % 249.89/250.10 Clause #261 (by clausification #[260]): ∀ (a a_1 a_2 a_3 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (sdtmndtplgtdt0 a_1 a_2 a) False) % 249.95/250.12 (Or (Eq (aElement0 a_1) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_2) False) % 249.95/250.12 (Or (Eq (aReductOfIn0 a a_1 a_2) True) % 249.95/250.12 (Eq % 249.95/250.12 (And (And (aElement0 (skS.0 11 a_1 a_2 a a_3)) (aReductOfIn0 (skS.0 11 a_1 a_2 a a_3) a_1 a_2)) % 249.95/250.12 (sdtmndtplgtdt0 (skS.0 11 a_1 a_2 a a_3) a_2 a)) % 249.95/250.12 True))))) % 249.95/250.12 Clause #263 (by clausification #[261]): ∀ (a a_1 a_2 a_3 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (sdtmndtplgtdt0 a_1 a_2 a) False) % 249.95/250.12 (Or (Eq (aElement0 a_1) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_2) False) % 249.95/250.12 (Or (Eq (aReductOfIn0 a a_1 a_2) True) % 249.95/250.12 (Eq (And (aElement0 (skS.0 11 a_1 a_2 a a_3)) (aReductOfIn0 (skS.0 11 a_1 a_2 a a_3) a_1 a_2)) True))))) % 249.95/250.12 Clause #413 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (sdtmndtasgtdt0 a_1 a_2 a) False) % 249.95/250.12 (Or (Eq (Or (Eq a_1 a) (sdtmndtplgtdt0 a_1 a_2 a)) True) % 249.95/250.12 (Or (Eq (aElement0 a_1) False) (Eq (aRewritingSystem0 a_2) False)))) % 249.95/250.12 Clause #414 (by clausification #[413]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (sdtmndtasgtdt0 a_1 a_2 a) False) % 249.95/250.12 (Or (Eq (aElement0 a_1) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_2) False) (Or (Eq (Eq a_1 a) True) (Eq (sdtmndtplgtdt0 a_1 a_2 a) True))))) % 249.95/250.12 Clause #415 (by clausification #[414]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (sdtmndtasgtdt0 a_1 a_2 a) False) % 249.95/250.12 (Or (Eq (aElement0 a_1) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_2) False) (Or (Eq (sdtmndtplgtdt0 a_1 a_2 a) True) (Eq a_1 a))))) % 249.95/250.12 Clause #422 (by superposition #[415, 220]): ∀ (a a_1 : Iota), % 249.95/250.12 Or (Eq (sdtmndtasgtdt0 a a_1 xx) False) % 249.95/250.12 (Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_1) False) (Or (Eq (sdtmndtplgtdt0 a a_1 xx) True) (Or (Eq a xx) (Eq False True))))) % 249.95/250.12 Clause #859 (by clausification #[202]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_1) False) % 249.95/250.12 (Or (Eq (aNormalFormOfIn0 a_2 a a_1) False) (Eq (Not (Exists fun W3 => aReductOfIn0 W3 a_2 a_1)) True))) % 249.95/250.12 Clause #860 (by clausification #[202]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_1) False) % 249.95/250.12 (Or (Eq (aNormalFormOfIn0 a_2 a a_1) False) (Eq (And (aElement0 a_2) (sdtmndtasgtdt0 a a_1 a_2)) True))) % 249.95/250.12 Clause #861 (by clausification #[859]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_1) False) % 249.95/250.12 (Or (Eq (aNormalFormOfIn0 a_2 a a_1) False) (Eq (Exists fun W3 => aReductOfIn0 W3 a_2 a_1) False))) % 249.95/250.12 Clause #862 (by clausification #[861]): ∀ (a a_1 a_2 a_3 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_1) False) % 249.95/250.12 (Or (Eq (aNormalFormOfIn0 a_2 a a_1) False) (Eq (aReductOfIn0 a_3 a_2 a_1) False))) % 249.95/250.12 Clause #867 (by superposition #[862, 164]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aRewritingSystem0 a) False) % 249.95/250.12 (Or (Eq (aNormalFormOfIn0 a_1 xw a) False) (Or (Eq (aReductOfIn0 a_2 a_1 a) False) (Eq False True))) % 249.95/250.12 Clause #875 (by clausification #[867]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aRewritingSystem0 a) False) (Or (Eq (aNormalFormOfIn0 a_1 xw a) False) (Eq (aReductOfIn0 a_2 a_1 a) False)) % 249.95/250.12 Clause #876 (by superposition #[875, 14]): ∀ (a a_1 : Iota), Or (Eq (aNormalFormOfIn0 a xw xR) False) (Or (Eq (aReductOfIn0 a_1 a xR) False) (Eq False True)) % 249.95/250.12 Clause #877 (by clausification #[876]): ∀ (a a_1 : Iota), Or (Eq (aNormalFormOfIn0 a xw xR) False) (Eq (aReductOfIn0 a_1 a xR) False) % 249.95/250.12 Clause #878 (by superposition #[877, 22]): ∀ (a : Iota), Or (Eq (aReductOfIn0 a xd xR) False) (Eq False True) % 249.95/250.12 Clause #882 (by clausification #[878]): ∀ (a : Iota), Eq (aReductOfIn0 a xd xR) False % 249.95/250.12 Clause #1101 (by clausification #[860]): ∀ (a a_1 a_2 : Iota), % 249.95/250.12 Or (Eq (aElement0 a) False) % 249.95/250.12 (Or (Eq (aRewritingSystem0 a_1) False) (Or (Eq (aNormalFormOfIn0 a_2 a a_1) False) (Eq (aElement0 a_2) True))) % 249.95/250.12 Clause #1113 (by superposition #[1101, 164]): ∀ (a a_1 : Iota), % 249.95/250.14 Or (Eq (aRewritingSystem0 a) False) % 249.95/250.14 (Or (Eq (aNormalFormOfIn0 a_1 xw a) False) (Or (Eq (aElement0 a_1) True) (Eq False True))) % 249.95/250.14 Clause #1126 (by clausification #[1113]): ∀ (a a_1 : Iota), % 249.95/250.14 Or (Eq (aRewritingSystem0 a) False) (Or (Eq (aNormalFormOfIn0 a_1 xw a) False) (Eq (aElement0 a_1) True)) % 249.95/250.14 Clause #1127 (by superposition #[1126, 14]): ∀ (a : Iota), Or (Eq (aNormalFormOfIn0 a xw xR) False) (Or (Eq (aElement0 a) True) (Eq False True)) % 249.95/250.14 Clause #1128 (by clausification #[1127]): ∀ (a : Iota), Or (Eq (aNormalFormOfIn0 a xw xR) False) (Eq (aElement0 a) True) % 249.95/250.14 Clause #1129 (by superposition #[1128, 22]): Or (Eq (aElement0 xd) True) (Eq False True) % 249.95/250.14 Clause #1131 (by clausification #[1129]): Eq (aElement0 xd) True % 249.95/250.14 Clause #1184 (by clausification #[263]): ∀ (a a_1 a_2 a_3 : Iota), % 249.95/250.14 Or (Eq (aElement0 a) False) % 249.95/250.14 (Or (Eq (sdtmndtplgtdt0 a_1 a_2 a) False) % 249.95/250.14 (Or (Eq (aElement0 a_1) False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 a_2) False) % 249.95/250.14 (Or (Eq (aReductOfIn0 a a_1 a_2) True) (Eq (aReductOfIn0 (skS.0 11 a_1 a_2 a a_3) a_1 a_2) True))))) % 249.95/250.14 Clause #1192 (by superposition #[1184, 220]): ∀ (a a_1 a_2 : Iota), % 249.95/250.14 Or (Eq (sdtmndtplgtdt0 a a_1 xx) False) % 249.95/250.14 (Or (Eq (aElement0 a) False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 a_1) False) % 249.95/250.14 (Or (Eq (aReductOfIn0 xx a a_1) True) % 249.95/250.14 (Or (Eq (aReductOfIn0 (skS.0 11 a a_1 xx a_2) a a_1) True) (Eq False True))))) % 249.95/250.14 Clause #2133 (by clausification #[422]): ∀ (a a_1 : Iota), % 249.95/250.14 Or (Eq (sdtmndtasgtdt0 a a_1 xx) False) % 249.95/250.14 (Or (Eq (aElement0 a) False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 a_1) False) (Or (Eq (sdtmndtplgtdt0 a a_1 xx) True) (Eq a xx)))) % 249.95/250.14 Clause #2134 (by superposition #[2133, 217]): Or (Eq (aElement0 xd) False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 xR) False) (Or (Eq (sdtmndtplgtdt0 xd xR xx) True) (Or (Eq xd xx) (Eq False True)))) % 249.95/250.14 Clause #2149 (by clausification #[2134]): Or (Eq (aElement0 xd) False) (Or (Eq (aRewritingSystem0 xR) False) (Or (Eq (sdtmndtplgtdt0 xd xR xx) True) (Eq xd xx))) % 249.95/250.14 Clause #2150 (by forward demodulation #[2149, 1131]): Or (Eq True False) (Or (Eq (aRewritingSystem0 xR) False) (Or (Eq (sdtmndtplgtdt0 xd xR xx) True) (Eq xd xx))) % 249.95/250.14 Clause #2151 (by clausification #[2150]): Or (Eq (aRewritingSystem0 xR) False) (Or (Eq (sdtmndtplgtdt0 xd xR xx) True) (Eq xd xx)) % 249.95/250.14 Clause #2152 (by forward demodulation #[2151, 14]): Or (Eq True False) (Or (Eq (sdtmndtplgtdt0 xd xR xx) True) (Eq xd xx)) % 249.95/250.14 Clause #2153 (by clausification #[2152]): Or (Eq (sdtmndtplgtdt0 xd xR xx) True) (Eq xd xx) % 249.95/250.14 Clause #5536 (by clausification #[1192]): ∀ (a a_1 a_2 : Iota), % 249.95/250.14 Or (Eq (sdtmndtplgtdt0 a a_1 xx) False) % 249.95/250.14 (Or (Eq (aElement0 a) False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 a_1) False) % 249.95/250.14 (Or (Eq (aReductOfIn0 xx a a_1) True) (Eq (aReductOfIn0 (skS.0 11 a a_1 xx a_2) a a_1) True)))) % 249.95/250.14 Clause #5538 (by superposition #[5536, 2153]): ∀ (a : Iota), % 249.95/250.14 Or (Eq (aElement0 xd) False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 xR) False) % 249.95/250.14 (Or (Eq (aReductOfIn0 xx xd xR) True) % 249.95/250.14 (Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Or (Eq False True) (Eq xd xx))))) % 249.95/250.14 Clause #14730 (by clausification #[5538]): ∀ (a : Iota), % 249.95/250.14 Or (Eq (aElement0 xd) False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 xR) False) % 249.95/250.14 (Or (Eq (aReductOfIn0 xx xd xR) True) (Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Eq xd xx)))) % 249.95/250.14 Clause #14731 (by forward demodulation #[14730, 1131]): ∀ (a : Iota), % 249.95/250.14 Or (Eq True False) % 249.95/250.14 (Or (Eq (aRewritingSystem0 xR) False) % 249.95/250.14 (Or (Eq (aReductOfIn0 xx xd xR) True) (Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Eq xd xx)))) % 249.95/250.14 Clause #14732 (by clausification #[14731]): ∀ (a : Iota), % 249.95/250.14 Or (Eq (aRewritingSystem0 xR) False) % 249.95/250.14 (Or (Eq (aReductOfIn0 xx xd xR) True) (Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Eq xd xx))) % 249.95/250.14 Clause #14733 (by forward demodulation #[14732, 14]): ∀ (a : Iota), % 249.95/250.14 Or (Eq True False) % 249.95/250.14 (Or (Eq (aReductOfIn0 xx xd xR) True) (Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Eq xd xx))) % 249.95/250.14 Clause #14734 (by clausification #[14733]): ∀ (a : Iota), Or (Eq (aReductOfIn0 xx xd xR) True) (Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Eq xd xx)) % 250.18/250.35 Clause #14735 (by forward demodulation #[14734, 882]): ∀ (a : Iota), Or (Eq False True) (Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Eq xd xx)) % 250.18/250.35 Clause #14736 (by clausification #[14735]): ∀ (a : Iota), Or (Eq (aReductOfIn0 (skS.0 11 xd xR xx a) xd xR) True) (Eq xd xx) % 250.18/250.35 Clause #14737 (by superposition #[14736, 882]): Or (Eq xd xx) (Eq True False) % 250.18/250.35 Clause #14740 (by clausification #[14737]): Eq xd xx % 250.18/250.35 Clause #14742 (by backward demodulation #[14740, 42]): Eq (sdtmndtasgtdt0 xb xR xx) False % 250.18/250.35 Clause #15227 (by superposition #[14742, 219]): Eq False True % 250.18/250.35 Clause #15228 (by clausification #[15227]): False % 250.18/250.35 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------