%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM018+4 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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 274.76s 275.06s % Output : Proof 275.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.13 % Problem : COM018+4 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.14 % Command : duper %s % 0.14/0.35 % Computer : n016.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 15:56:08 EDT 2025 % 0.14/0.35 % CPUTime : % 274.76/275.06 SZS status Theorem for theBenchmark.p % 274.76/275.06 SZS output start Proof for theBenchmark.p % 274.76/275.06 Clause #13 (by assumption #[]): Eq % 274.76/275.06 (∀ (W0 : Iota), % 274.76/275.06 And (aRewritingSystem0 W0) (isTerminating0 W0) → % 274.76/275.06 ∀ (W1 : Iota), aElement0 W1 → Exists fun W2 => aNormalFormOfIn0 W2 W1 W0) % 274.76/275.06 True % 274.76/275.06 Clause #14 (by assumption #[]): Eq (aRewritingSystem0 xR) True % 274.76/275.06 Clause #15 (by assumption #[]): Eq % 274.76/275.06 (And % 274.76/275.06 (And % 274.76/275.06 (And % 274.76/275.06 (∀ (W0 W1 W2 : Iota), % 274.76/275.06 And (And (And (And (aElement0 W0) (aElement0 W1)) (aElement0 W2)) (aReductOfIn0 W1 W0 xR)) % 274.76/275.06 (aReductOfIn0 W2 W0 xR) → % 274.76/275.06 Exists fun W3 => % 274.76/275.06 And % 274.76/275.06 (And % 274.76/275.06 (And % 274.76/275.06 (And (aElement0 W3) % 274.76/275.06 (Or (Eq W1 W3) % 274.76/275.06 (And % 274.76/275.06 (Or (aReductOfIn0 W3 W1 xR) % 274.76/275.06 (Exists fun W4 => % 274.76/275.06 And (And (aElement0 W4) (aReductOfIn0 W4 W1 xR)) (sdtmndtplgtdt0 W4 xR W3))) % 274.76/275.06 (sdtmndtplgtdt0 W1 xR W3)))) % 274.76/275.06 (sdtmndtasgtdt0 W1 xR W3)) % 274.76/275.06 (Or (Eq W2 W3) % 274.76/275.06 (And % 274.76/275.06 (Or (aReductOfIn0 W3 W2 xR) % 274.76/275.06 (Exists fun W4 => And (And (aElement0 W4) (aReductOfIn0 W4 W2 xR)) (sdtmndtplgtdt0 W4 xR W3))) % 274.76/275.06 (sdtmndtplgtdt0 W2 xR W3)))) % 274.76/275.06 (sdtmndtasgtdt0 W2 xR W3)) % 274.76/275.06 (isLocallyConfluent0 xR)) % 274.76/275.06 (∀ (W0 W1 : Iota), % 274.76/275.06 And (aElement0 W0) (aElement0 W1) → % 274.76/275.06 Or % 274.76/275.06 (Or (aReductOfIn0 W1 W0 xR) % 274.76/275.06 (Exists fun W2 => And (And (aElement0 W2) (aReductOfIn0 W2 W0 xR)) (sdtmndtplgtdt0 W2 xR W1))) % 274.76/275.06 (sdtmndtplgtdt0 W0 xR W1) → % 274.76/275.06 iLess0 W1 W0)) % 274.76/275.06 (isTerminating0 xR)) % 274.76/275.06 True % 274.76/275.06 Clause #21 (by assumption #[]): Eq % 274.76/275.06 (And % 274.76/275.06 (And % 274.76/275.06 (And % 274.76/275.06 (And (aElement0 xw) % 274.76/275.06 (Or (Eq xu xw) % 274.76/275.06 (And % 274.76/275.06 (Or (aReductOfIn0 xw xu xR) % 274.76/275.06 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xu xR)) (sdtmndtplgtdt0 W0 xR xw))) % 274.76/275.06 (sdtmndtplgtdt0 xu xR xw)))) % 274.76/275.06 (sdtmndtasgtdt0 xu xR xw)) % 274.76/275.06 (Or (Eq xv xw) % 274.76/275.06 (And % 274.76/275.06 (Or (aReductOfIn0 xw xv xR) % 274.76/275.06 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xv xR)) (sdtmndtplgtdt0 W0 xR xw))) % 274.76/275.06 (sdtmndtplgtdt0 xv xR xw)))) % 274.76/275.06 (sdtmndtasgtdt0 xv xR xw)) % 274.76/275.06 True % 274.76/275.06 Clause #22 (by assumption #[]): Eq % 274.76/275.06 (Not % 274.76/275.06 (Exists fun W0 => % 274.76/275.06 Or % 274.76/275.06 (And % 274.76/275.06 (And (aElement0 W0) % 274.76/275.06 (Or % 274.76/275.06 (Or % 274.76/275.06 (Or (Or (Eq xw W0) (aReductOfIn0 W0 xw xR)) % 274.76/275.06 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 xw xR)) (sdtmndtplgtdt0 W1 xR W0))) % 274.76/275.06 (sdtmndtplgtdt0 xw xR W0)) % 274.76/275.06 (sdtmndtasgtdt0 xw xR W0))) % 274.76/275.06 (Not (Exists fun W1 => aReductOfIn0 W1 W0 xR))) % 274.76/275.06 (aNormalFormOfIn0 W0 xw xR))) % 274.76/275.06 True % 274.76/275.06 Clause #94 (by clausification #[13]): ∀ (a : Iota), % 274.76/275.06 Eq % 274.76/275.06 (And (aRewritingSystem0 a) (isTerminating0 a) → % 274.76/275.06 ∀ (W1 : Iota), aElement0 W1 → Exists fun W2 => aNormalFormOfIn0 W2 W1 a) % 274.76/275.06 True % 274.76/275.06 Clause #95 (by clausification #[94]): ∀ (a : Iota), % 274.76/275.06 Or (Eq (And (aRewritingSystem0 a) (isTerminating0 a)) False) % 274.76/275.06 (Eq (∀ (W1 : Iota), aElement0 W1 → Exists fun W2 => aNormalFormOfIn0 W2 W1 a) True) % 274.76/275.06 Clause #96 (by clausification #[95]): ∀ (a : Iota), % 274.76/275.06 Or (Eq (∀ (W1 : Iota), aElement0 W1 → Exists fun W2 => aNormalFormOfIn0 W2 W1 a) True) % 274.76/275.06 (Or (Eq (aRewritingSystem0 a) False) (Eq (isTerminating0 a) False)) % 274.76/275.06 Clause #97 (by clausification #[96]): ∀ (a a_1 : Iota), % 274.76/275.06 Or (Eq (aRewritingSystem0 a) False) % 274.76/275.06 (Or (Eq (isTerminating0 a) False) (Eq (aElement0 a_1 → Exists fun W2 => aNormalFormOfIn0 W2 a_1 a) True)) % 274.76/275.06 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), % 274.76/275.06 Or (Eq (aRewritingSystem0 a) False) % 274.76/275.06 (Or (Eq (isTerminating0 a) False) % 274.76/275.06 (Or (Eq (aElement0 a_1) False) (Eq (Exists fun W2 => aNormalFormOfIn0 W2 a_1 a) True))) % 274.76/275.06 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 : Iota), % 274.76/275.06 Or (Eq (aRewritingSystem0 a) False) % 274.76/275.06 (Or (Eq (isTerminating0 a) False) % 275.01/275.29 (Or (Eq (aElement0 a_1) False) (Eq (aNormalFormOfIn0 (skS.0 0 a_1 a a_2) a_1 a) True))) % 275.01/275.29 Clause #100 (by superposition #[99, 14]): ∀ (a a_1 : Iota), % 275.01/275.29 Or (Eq (isTerminating0 xR) False) % 275.01/275.29 (Or (Eq (aElement0 a) False) (Or (Eq (aNormalFormOfIn0 (skS.0 0 a xR a_1) a xR) True) (Eq False True))) % 275.01/275.29 Clause #230 (by clausification #[15]): Eq (isTerminating0 xR) True % 275.01/275.29 Clause #303 (by clausification #[21]): Eq % 275.01/275.29 (And % 275.01/275.29 (And % 275.01/275.29 (And (aElement0 xw) % 275.01/275.29 (Or (Eq xu xw) % 275.01/275.29 (And % 275.01/275.29 (Or (aReductOfIn0 xw xu xR) % 275.01/275.29 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xu xR)) (sdtmndtplgtdt0 W0 xR xw))) % 275.01/275.29 (sdtmndtplgtdt0 xu xR xw)))) % 275.01/275.29 (sdtmndtasgtdt0 xu xR xw)) % 275.01/275.29 (Or (Eq xv xw) % 275.01/275.29 (And % 275.01/275.29 (Or (aReductOfIn0 xw xv xR) % 275.01/275.29 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xv xR)) (sdtmndtplgtdt0 W0 xR xw))) % 275.01/275.29 (sdtmndtplgtdt0 xv xR xw)))) % 275.01/275.29 True % 275.01/275.29 Clause #314 (by clausification #[22]): Eq % 275.01/275.29 (Exists fun W0 => % 275.01/275.29 Or % 275.01/275.29 (And % 275.01/275.29 (And (aElement0 W0) % 275.01/275.29 (Or % 275.01/275.29 (Or % 275.01/275.29 (Or (Or (Eq xw W0) (aReductOfIn0 W0 xw xR)) % 275.01/275.29 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 xw xR)) (sdtmndtplgtdt0 W1 xR W0))) % 275.01/275.29 (sdtmndtplgtdt0 xw xR W0)) % 275.01/275.29 (sdtmndtasgtdt0 xw xR W0))) % 275.01/275.29 (Not (Exists fun W1 => aReductOfIn0 W1 W0 xR))) % 275.01/275.29 (aNormalFormOfIn0 W0 xw xR)) % 275.01/275.29 False % 275.01/275.29 Clause #315 (by clausification #[314]): ∀ (a : Iota), % 275.01/275.29 Eq % 275.01/275.29 (Or % 275.01/275.29 (And % 275.01/275.29 (And (aElement0 a) % 275.01/275.29 (Or % 275.01/275.29 (Or % 275.01/275.29 (Or (Or (Eq xw a) (aReductOfIn0 a xw xR)) % 275.01/275.29 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 xw xR)) (sdtmndtplgtdt0 W1 xR a))) % 275.01/275.29 (sdtmndtplgtdt0 xw xR a)) % 275.01/275.29 (sdtmndtasgtdt0 xw xR a))) % 275.01/275.29 (Not (Exists fun W1 => aReductOfIn0 W1 a xR))) % 275.01/275.29 (aNormalFormOfIn0 a xw xR)) % 275.01/275.29 False % 275.01/275.29 Clause #316 (by clausification #[315]): ∀ (a : Iota), Eq (aNormalFormOfIn0 a xw xR) False % 275.01/275.29 Clause #386 (by clausification #[100]): ∀ (a a_1 : Iota), % 275.01/275.29 Or (Eq (isTerminating0 xR) False) (Or (Eq (aElement0 a) False) (Eq (aNormalFormOfIn0 (skS.0 0 a xR a_1) a xR) True)) % 275.01/275.29 Clause #387 (by forward demodulation #[386, 230]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (aElement0 a) False) (Eq (aNormalFormOfIn0 (skS.0 0 a xR a_1) a xR) True)) % 275.01/275.29 Clause #388 (by clausification #[387]): ∀ (a a_1 : Iota), Or (Eq (aElement0 a) False) (Eq (aNormalFormOfIn0 (skS.0 0 a xR a_1) a xR) True) % 275.01/275.29 Clause #1261 (by clausification #[303]): Eq % 275.01/275.29 (And % 275.01/275.29 (And (aElement0 xw) % 275.01/275.29 (Or (Eq xu xw) % 275.01/275.29 (And % 275.01/275.29 (Or (aReductOfIn0 xw xu xR) % 275.01/275.29 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xu xR)) (sdtmndtplgtdt0 W0 xR xw))) % 275.01/275.29 (sdtmndtplgtdt0 xu xR xw)))) % 275.01/275.29 (sdtmndtasgtdt0 xu xR xw)) % 275.01/275.29 True % 275.01/275.29 Clause #10045 (by clausification #[1261]): Eq % 275.01/275.29 (And (aElement0 xw) % 275.01/275.29 (Or (Eq xu xw) % 275.01/275.29 (And % 275.01/275.29 (Or (aReductOfIn0 xw xu xR) % 275.01/275.29 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xu xR)) (sdtmndtplgtdt0 W0 xR xw))) % 275.01/275.29 (sdtmndtplgtdt0 xu xR xw)))) % 275.01/275.29 True % 275.01/275.29 Clause #11667 (by clausification #[10045]): Eq (aElement0 xw) True % 275.01/275.29 Clause #11695 (by superposition #[11667, 388]): ∀ (a : Iota), Or (Eq True False) (Eq (aNormalFormOfIn0 (skS.0 0 xw xR a) xw xR) True) % 275.01/275.29 Clause #12187 (by clausification #[11695]): ∀ (a : Iota), Eq (aNormalFormOfIn0 (skS.0 0 xw xR a) xw xR) True % 275.01/275.29 Clause #12188 (by superposition #[12187, 316]): Eq True False % 275.01/275.29 Clause #12189 (by clausification #[12188]): False % 275.01/275.29 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------