%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM021+4 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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 189.40s 189.68s % Output : Proof 189.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.10 % Problem : COM021+4 : TPTP v9.2.0. Released v4.0.0. % 0.09/0.11 % Command : duper %s % 0.11/0.32 % Computer : n008.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Thu Oct 2 16:07:08 EDT 2025 % 0.11/0.32 % CPUTime : % 189.40/189.68 SZS status Theorem for theBenchmark.p % 189.40/189.68 SZS output start Proof for theBenchmark.p % 189.40/189.68 Clause #22 (by assumption #[]): Eq % 189.40/189.68 (And % 189.40/189.68 (And % 189.40/189.68 (And % 189.40/189.68 (And (aElement0 xd) % 189.40/189.68 (Or (Eq xw xd) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xd xw xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xw xR)) (sdtmndtplgtdt0 W0 xR xd))) % 189.40/189.68 (sdtmndtplgtdt0 xw xR xd)))) % 189.40/189.68 (sdtmndtasgtdt0 xw xR xd)) % 189.40/189.68 (Not (Exists fun W0 => aReductOfIn0 W0 xd xR))) % 189.40/189.68 (aNormalFormOfIn0 xd xw xR)) % 189.40/189.68 True % 189.40/189.68 Clause #23 (by assumption #[]): Eq % 189.40/189.68 (And % 189.40/189.68 (And % 189.40/189.68 (And % 189.40/189.68 (And (aElement0 xx) % 189.40/189.68 (Or (Eq xb xx) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xb xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xb xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xb xR xx)))) % 189.40/189.68 (sdtmndtasgtdt0 xb xR xx)) % 189.40/189.68 (Or (Eq xd xx) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xd xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xd xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xd xR xx)))) % 189.40/189.68 (sdtmndtasgtdt0 xd xR xx)) % 189.40/189.68 True % 189.40/189.68 Clause #24 (by assumption #[]): Eq % 189.40/189.68 (Not % 189.40/189.68 (Or % 189.40/189.68 (Or % 189.40/189.68 (Or (Or (Eq xb xd) (aReductOfIn0 xd xb xR)) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xb xR)) (sdtmndtplgtdt0 W0 xR xd))) % 189.40/189.68 (sdtmndtplgtdt0 xb xR xd)) % 189.40/189.68 (sdtmndtasgtdt0 xb xR xd))) % 189.40/189.68 True % 189.40/189.68 Clause #317 (by clausification #[22]): Eq % 189.40/189.68 (And % 189.40/189.68 (And % 189.40/189.68 (And (aElement0 xd) % 189.40/189.68 (Or (Eq xw xd) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xd xw xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xw xR)) (sdtmndtplgtdt0 W0 xR xd))) % 189.40/189.68 (sdtmndtplgtdt0 xw xR xd)))) % 189.40/189.68 (sdtmndtasgtdt0 xw xR xd)) % 189.40/189.68 (Not (Exists fun W0 => aReductOfIn0 W0 xd xR))) % 189.40/189.68 True % 189.40/189.68 Clause #329 (by clausification #[23]): Eq % 189.40/189.68 (And % 189.40/189.68 (And % 189.40/189.68 (And (aElement0 xx) % 189.40/189.68 (Or (Eq xb xx) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xb xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xb xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xb xR xx)))) % 189.40/189.68 (sdtmndtasgtdt0 xb xR xx)) % 189.40/189.68 (Or (Eq xd xx) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xd xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xd xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xd xR xx)))) % 189.40/189.68 True % 189.40/189.68 Clause #337 (by clausification #[24]): Eq % 189.40/189.68 (Or % 189.40/189.68 (Or % 189.40/189.68 (Or (Or (Eq xb xd) (aReductOfIn0 xd xb xR)) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xb xR)) (sdtmndtplgtdt0 W0 xR xd))) % 189.40/189.68 (sdtmndtplgtdt0 xb xR xd)) % 189.40/189.68 (sdtmndtasgtdt0 xb xR xd)) % 189.40/189.68 False % 189.40/189.68 Clause #338 (by clausification #[337]): Eq (sdtmndtasgtdt0 xb xR xd) False % 189.40/189.68 Clause #1307 (by clausification #[317]): Eq (Not (Exists fun W0 => aReductOfIn0 W0 xd xR)) True % 189.40/189.68 Clause #1309 (by clausification #[1307]): Eq (Exists fun W0 => aReductOfIn0 W0 xd xR) False % 189.40/189.68 Clause #1310 (by clausification #[1309]): ∀ (a : Iota), Eq (aReductOfIn0 a xd xR) False % 189.40/189.68 Clause #1328 (by clausification #[329]): Eq % 189.40/189.68 (Or (Eq xd xx) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xd xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xd xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xd xR xx))) % 189.40/189.68 True % 189.40/189.68 Clause #1329 (by clausification #[329]): Eq % 189.40/189.68 (And % 189.40/189.68 (And (aElement0 xx) % 189.40/189.68 (Or (Eq xb xx) % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xb xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xb xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xb xR xx)))) % 189.40/189.68 (sdtmndtasgtdt0 xb xR xx)) % 189.40/189.68 True % 189.40/189.68 Clause #1330 (by clausification #[1328]): Or (Eq (Eq xd xx) True) % 189.40/189.68 (Eq % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xd xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xd xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xd xR xx)) % 189.40/189.68 True) % 189.40/189.68 Clause #1331 (by clausification #[1330]): Or % 189.40/189.68 (Eq % 189.40/189.68 (And % 189.40/189.68 (Or (aReductOfIn0 xx xd xR) % 189.40/189.68 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xd xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.40/189.68 (sdtmndtplgtdt0 xd xR xx)) % 189.60/189.86 True) % 189.60/189.86 (Eq xd xx) % 189.60/189.86 Clause #1333 (by clausification #[1331]): Or (Eq xd xx) % 189.60/189.86 (Eq % 189.60/189.86 (Or (aReductOfIn0 xx xd xR) % 189.60/189.86 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xd xR)) (sdtmndtplgtdt0 W0 xR xx))) % 189.60/189.86 True) % 189.60/189.86 Clause #2583 (by clausification #[1333]): Or (Eq xd xx) % 189.60/189.86 (Or (Eq (aReductOfIn0 xx xd xR) True) % 189.60/189.86 (Eq (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xd xR)) (sdtmndtplgtdt0 W0 xR xx)) True)) % 189.60/189.86 Clause #2584 (by clausification #[2583]): ∀ (a : Iota), % 189.60/189.86 Or (Eq xd xx) % 189.60/189.86 (Or (Eq (aReductOfIn0 xx xd xR) True) % 189.60/189.86 (Eq (And (And (aElement0 (skS.0 18 a)) (aReductOfIn0 (skS.0 18 a) xd xR)) (sdtmndtplgtdt0 (skS.0 18 a) xR xx)) % 189.60/189.86 True)) % 189.60/189.86 Clause #2586 (by clausification #[2584]): ∀ (a : Iota), % 189.60/189.86 Or (Eq xd xx) % 189.60/189.86 (Or (Eq (aReductOfIn0 xx xd xR) True) (Eq (And (aElement0 (skS.0 18 a)) (aReductOfIn0 (skS.0 18 a) xd xR)) True)) % 189.60/189.86 Clause #2984 (by clausification #[2586]): ∀ (a : Iota), Or (Eq xd xx) (Or (Eq (aReductOfIn0 xx xd xR) True) (Eq (aReductOfIn0 (skS.0 18 a) xd xR) True)) % 189.60/189.86 Clause #2986 (by forward demodulation #[2984, 1310]): ∀ (a : Iota), Or (Eq xd xx) (Or (Eq False True) (Eq (aReductOfIn0 (skS.0 18 a) xd xR) True)) % 189.60/189.86 Clause #2987 (by clausification #[2986]): ∀ (a : Iota), Or (Eq xd xx) (Eq (aReductOfIn0 (skS.0 18 a) xd xR) True) % 189.60/189.86 Clause #2988 (by superposition #[2987, 1310]): Or (Eq xd xx) (Eq True False) % 189.60/189.86 Clause #2989 (by clausification #[2988]): Eq xd xx % 189.60/189.86 Clause #10469 (by clausification #[1329]): Eq (sdtmndtasgtdt0 xb xR xx) True % 189.60/189.86 Clause #10471 (by forward demodulation #[10469, 2989]): Eq (sdtmndtasgtdt0 xb xR xd) True % 189.60/189.86 Clause #10472 (by superposition #[10471, 338]): Eq True False % 189.60/189.86 Clause #10473 (by clausification #[10472]): False % 189.60/189.86 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------