%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM016+4 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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 8.88s 9.08s % Output : Proof 8.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COM016+4 : TPTP v9.2.0. Released v4.0.0. % 0.03/0.13 % Command : duper %s % 0.12/0.34 % Computer : n007.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 15:54:23 EDT 2025 % 0.12/0.34 % CPUTime : % 8.88/9.08 SZS status Theorem for theBenchmark.p % 8.88/9.08 SZS output start Proof for theBenchmark.p % 8.88/9.08 Clause #7 (by assumption #[]): Eq % 8.88/9.08 (∀ (W0 W1 W2 : Iota), % 8.88/9.08 And (And (aElement0 W0) (aRewritingSystem0 W1)) (aElement0 W2) → % 8.88/9.08 Iff (sdtmndtasgtdt0 W0 W1 W2) (Or (Eq W0 W2) (sdtmndtplgtdt0 W0 W1 W2))) % 8.88/9.08 True % 8.88/9.08 Clause #14 (by assumption #[]): Eq (aRewritingSystem0 xR) True % 8.88/9.08 Clause #16 (by assumption #[]): Eq (And (And (aElement0 xa) (aElement0 xb)) (aElement0 xc)) True % 8.88/9.08 Clause #18 (by assumption #[]): Eq % 8.88/9.08 (And % 8.88/9.08 (And % 8.88/9.08 (And % 8.88/9.08 (Or (aReductOfIn0 xb xa xR) % 8.88/9.08 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) (sdtmndtplgtdt0 W0 xR xb))) % 8.88/9.08 (sdtmndtplgtdt0 xa xR xb)) % 8.88/9.08 (Or (aReductOfIn0 xc xa xR) % 8.88/9.08 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) (sdtmndtplgtdt0 W0 xR xc)))) % 8.88/9.08 (sdtmndtplgtdt0 xa xR xc)) % 8.88/9.08 True % 8.88/9.08 Clause #19 (by assumption #[]): Eq % 8.88/9.08 (Not % 8.88/9.08 (Exists fun W0 => % 8.88/9.08 And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) % 8.88/9.08 (Or % 8.88/9.08 (Or % 8.88/9.08 (Or (Or (Eq W0 xb) (aReductOfIn0 xb W0 xR)) % 8.88/9.08 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 W0 xR)) (sdtmndtplgtdt0 W1 xR xb))) % 8.88/9.08 (sdtmndtplgtdt0 W0 xR xb)) % 8.88/9.08 (sdtmndtasgtdt0 W0 xR xb)))) % 8.88/9.08 True % 8.88/9.08 Clause #43 (by clausification #[16]): Eq (And (aElement0 xa) (aElement0 xb)) True % 8.88/9.08 Clause #45 (by clausification #[43]): Eq (aElement0 xb) True % 8.88/9.08 Clause #104 (by clausification #[7]): ∀ (a : Iota), % 8.88/9.08 Eq % 8.88/9.08 (∀ (W1 W2 : Iota), % 8.88/9.08 And (And (aElement0 a) (aRewritingSystem0 W1)) (aElement0 W2) → % 8.88/9.08 Iff (sdtmndtasgtdt0 a W1 W2) (Or (Eq a W2) (sdtmndtplgtdt0 a W1 W2))) % 8.88/9.08 True % 8.88/9.08 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), % 8.88/9.08 Eq % 8.88/9.08 (∀ (W2 : Iota), % 8.88/9.08 And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 W2) → % 8.88/9.08 Iff (sdtmndtasgtdt0 a a_1 W2) (Or (Eq a W2) (sdtmndtplgtdt0 a a_1 W2))) % 8.88/9.08 True % 8.88/9.08 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 8.88/9.08 Eq % 8.88/9.08 (And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 a_2) → % 8.88/9.08 Iff (sdtmndtasgtdt0 a a_1 a_2) (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2))) % 8.88/9.08 True % 8.88/9.08 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 8.88/9.08 Or (Eq (And (And (aElement0 a) (aRewritingSystem0 a_1)) (aElement0 a_2)) False) % 8.88/9.08 (Eq (Iff (sdtmndtasgtdt0 a a_1 a_2) (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2))) True) % 8.88/9.08 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 8.88/9.08 Or (Eq (Iff (sdtmndtasgtdt0 a a_1 a_2) (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2))) True) % 8.88/9.08 (Or (Eq (And (aElement0 a) (aRewritingSystem0 a_1)) False) (Eq (aElement0 a_2) False)) % 8.88/9.08 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 : Iota), % 8.88/9.08 Or (Eq (And (aElement0 a) (aRewritingSystem0 a_1)) False) % 8.88/9.08 (Or (Eq (aElement0 a_2) False) % 8.88/9.08 (Or (Eq (sdtmndtasgtdt0 a a_1 a_2) True) (Eq (Or (Eq a a_2) (sdtmndtplgtdt0 a a_1 a_2)) False))) % 8.88/9.08 Clause #111 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), % 8.88/9.08 Or (Eq (aElement0 a) False) % 8.88/9.08 (Or (Eq (sdtmndtasgtdt0 a_1 a_2 a) True) % 8.88/9.08 (Or (Eq (Or (Eq a_1 a) (sdtmndtplgtdt0 a_1 a_2 a)) False) % 8.88/9.08 (Or (Eq (aElement0 a_1) False) (Eq (aRewritingSystem0 a_2) False)))) % 8.88/9.08 Clause #113 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 8.88/9.08 Or (Eq (aElement0 a) False) % 8.88/9.08 (Or (Eq (sdtmndtasgtdt0 a_1 a_2 a) True) % 8.88/9.08 (Or (Eq (aElement0 a_1) False) (Or (Eq (aRewritingSystem0 a_2) False) (Eq (Eq a_1 a) False)))) % 8.88/9.08 Clause #262 (by clausification #[18]): Eq % 8.88/9.08 (And % 8.88/9.08 (And % 8.88/9.08 (Or (aReductOfIn0 xb xa xR) % 8.88/9.08 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) (sdtmndtplgtdt0 W0 xR xb))) % 8.88/9.08 (sdtmndtplgtdt0 xa xR xb)) % 8.88/9.08 (Or (aReductOfIn0 xc xa xR) % 8.88/9.08 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) (sdtmndtplgtdt0 W0 xR xc)))) % 8.88/9.08 True % 8.88/9.08 Clause #265 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), % 8.88/9.08 Or (Eq (aElement0 a) False) % 8.88/9.08 (Or (Eq (sdtmndtasgtdt0 a_1 a_2 a) True) % 8.88/9.08 (Or (Eq (aElement0 a_1) False) (Or (Eq (aRewritingSystem0 a_2) False) (Ne a_1 a)))) % 8.88/9.08 Clause #266 (by destructive equality resolution #[265]): ∀ (a a_1 : Iota), % 8.88/9.08 Or (Eq (aElement0 a) False) % 8.88/9.10 (Or (Eq (sdtmndtasgtdt0 a a_1 a) True) (Or (Eq (aElement0 a) False) (Eq (aRewritingSystem0 a_1) False))) % 8.88/9.10 Clause #267 (by eliminate duplicate literals #[266]): ∀ (a a_1 : Iota), Or (Eq (aElement0 a) False) (Or (Eq (sdtmndtasgtdt0 a a_1 a) True) (Eq (aRewritingSystem0 a_1) False)) % 8.88/9.10 Clause #269 (by superposition #[267, 45]): ∀ (a : Iota), Or (Eq (sdtmndtasgtdt0 xb a xb) True) (Or (Eq (aRewritingSystem0 a) False) (Eq False True)) % 8.88/9.10 Clause #274 (by clausification #[269]): ∀ (a : Iota), Or (Eq (sdtmndtasgtdt0 xb a xb) True) (Eq (aRewritingSystem0 a) False) % 8.88/9.10 Clause #275 (by superposition #[274, 14]): Or (Eq (sdtmndtasgtdt0 xb xR xb) True) (Eq False True) % 8.88/9.10 Clause #276 (by clausification #[19]): Eq % 8.88/9.10 (Exists fun W0 => % 8.88/9.10 And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) % 8.88/9.10 (Or % 8.88/9.10 (Or % 8.88/9.10 (Or (Or (Eq W0 xb) (aReductOfIn0 xb W0 xR)) % 8.88/9.10 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 W0 xR)) (sdtmndtplgtdt0 W1 xR xb))) % 8.88/9.10 (sdtmndtplgtdt0 W0 xR xb)) % 8.88/9.10 (sdtmndtasgtdt0 W0 xR xb))) % 8.88/9.10 False % 8.88/9.10 Clause #277 (by clausification #[276]): ∀ (a : Iota), % 8.88/9.10 Eq % 8.88/9.10 (And (And (aElement0 a) (aReductOfIn0 a xa xR)) % 8.88/9.10 (Or % 8.88/9.10 (Or % 8.88/9.10 (Or (Or (Eq a xb) (aReductOfIn0 xb a xR)) % 8.88/9.10 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 a xR)) (sdtmndtplgtdt0 W1 xR xb))) % 8.88/9.10 (sdtmndtplgtdt0 a xR xb)) % 8.88/9.10 (sdtmndtasgtdt0 a xR xb))) % 8.88/9.10 False % 8.88/9.10 Clause #278 (by clausification #[277]): ∀ (a : Iota), % 8.88/9.10 Or (Eq (And (aElement0 a) (aReductOfIn0 a xa xR)) False) % 8.88/9.10 (Eq % 8.88/9.10 (Or % 8.88/9.10 (Or % 8.88/9.10 (Or (Or (Eq a xb) (aReductOfIn0 xb a xR)) % 8.88/9.10 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 a xR)) (sdtmndtplgtdt0 W1 xR xb))) % 8.88/9.10 (sdtmndtplgtdt0 a xR xb)) % 8.88/9.10 (sdtmndtasgtdt0 a xR xb)) % 8.88/9.10 False) % 8.88/9.10 Clause #279 (by clausification #[278]): ∀ (a : Iota), % 8.88/9.10 Or % 8.88/9.10 (Eq % 8.88/9.10 (Or % 8.88/9.10 (Or % 8.88/9.10 (Or (Or (Eq a xb) (aReductOfIn0 xb a xR)) % 8.88/9.10 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 a xR)) (sdtmndtplgtdt0 W1 xR xb))) % 8.88/9.10 (sdtmndtplgtdt0 a xR xb)) % 8.88/9.10 (sdtmndtasgtdt0 a xR xb)) % 8.88/9.10 False) % 8.88/9.10 (Or (Eq (aElement0 a) False) (Eq (aReductOfIn0 a xa xR) False)) % 8.88/9.10 Clause #280 (by clausification #[279]): ∀ (a : Iota), Or (Eq (aElement0 a) False) (Or (Eq (aReductOfIn0 a xa xR) False) (Eq (sdtmndtasgtdt0 a xR xb) False)) % 8.88/9.10 Clause #281 (by clausification #[279]): ∀ (a : Iota), % 8.88/9.10 Or (Eq (aElement0 a) False) % 8.88/9.10 (Or (Eq (aReductOfIn0 a xa xR) False) % 8.88/9.10 (Eq % 8.88/9.10 (Or % 8.88/9.10 (Or (Or (Eq a xb) (aReductOfIn0 xb a xR)) % 8.88/9.10 (Exists fun W1 => And (And (aElement0 W1) (aReductOfIn0 W1 a xR)) (sdtmndtplgtdt0 W1 xR xb))) % 8.88/9.10 (sdtmndtplgtdt0 a xR xb)) % 8.88/9.10 False)) % 8.88/9.10 Clause #283 (by superposition #[280, 45]): Or (Eq (aReductOfIn0 xb xa xR) False) (Or (Eq (sdtmndtasgtdt0 xb xR xb) False) (Eq False True)) % 8.88/9.10 Clause #285 (by clausification #[275]): Eq (sdtmndtasgtdt0 xb xR xb) True % 8.88/9.10 Clause #289 (by clausification #[283]): Or (Eq (aReductOfIn0 xb xa xR) False) (Eq (sdtmndtasgtdt0 xb xR xb) False) % 8.88/9.10 Clause #1082 (by clausification #[262]): Eq % 8.88/9.10 (And % 8.88/9.10 (Or (aReductOfIn0 xb xa xR) % 8.88/9.10 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) (sdtmndtplgtdt0 W0 xR xb))) % 8.88/9.10 (sdtmndtplgtdt0 xa xR xb)) % 8.88/9.10 True % 8.88/9.10 Clause #1134 (by clausification #[281]): ∀ (a : Iota), Or (Eq (aElement0 a) False) (Or (Eq (aReductOfIn0 a xa xR) False) (Eq (sdtmndtplgtdt0 a xR xb) False)) % 8.88/9.10 Clause #1179 (by clausification #[1082]): Eq % 8.88/9.10 (Or (aReductOfIn0 xb xa xR) % 8.88/9.10 (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) (sdtmndtplgtdt0 W0 xR xb))) % 8.88/9.10 True % 8.88/9.10 Clause #1269 (by clausification #[1179]): Or (Eq (aReductOfIn0 xb xa xR) True) % 8.88/9.10 (Eq (Exists fun W0 => And (And (aElement0 W0) (aReductOfIn0 W0 xa xR)) (sdtmndtplgtdt0 W0 xR xb)) True) % 8.88/9.10 Clause #1270 (by clausification #[1269]): ∀ (a : Iota), % 8.88/9.10 Or (Eq (aReductOfIn0 xb xa xR) True) % 8.88/9.10 (Eq (And (And (aElement0 (skS.0 16 a)) (aReductOfIn0 (skS.0 16 a) xa xR)) (sdtmndtplgtdt0 (skS.0 16 a) xR xb)) True) % 8.88/9.10 Clause #1271 (by clausification #[1270]): ∀ (a : Iota), Or (Eq (aReductOfIn0 xb xa xR) True) (Eq (sdtmndtplgtdt0 (skS.0 16 a) xR xb) True) % 8.88/9.12 Clause #1272 (by clausification #[1270]): ∀ (a : Iota), % 8.88/9.12 Or (Eq (aReductOfIn0 xb xa xR) True) (Eq (And (aElement0 (skS.0 16 a)) (aReductOfIn0 (skS.0 16 a) xa xR)) True) % 8.88/9.12 Clause #1278 (by clausification #[1272]): ∀ (a : Iota), Or (Eq (aReductOfIn0 xb xa xR) True) (Eq (aReductOfIn0 (skS.0 16 a) xa xR) True) % 8.88/9.12 Clause #1279 (by clausification #[1272]): ∀ (a : Iota), Or (Eq (aReductOfIn0 xb xa xR) True) (Eq (aElement0 (skS.0 16 a)) True) % 8.88/9.12 Clause #1318 (by superposition #[1279, 1134]): ∀ (a : Iota), % 8.88/9.12 Or (Eq (aReductOfIn0 xb xa xR) True) % 8.88/9.12 (Or (Eq True False) % 8.88/9.12 (Or (Eq (aReductOfIn0 (skS.0 16 a) xa xR) False) (Eq (sdtmndtplgtdt0 (skS.0 16 a) xR xb) False))) % 8.88/9.12 Clause #1420 (by clausification #[1318]): ∀ (a : Iota), % 8.88/9.12 Or (Eq (aReductOfIn0 xb xa xR) True) % 8.88/9.12 (Or (Eq (aReductOfIn0 (skS.0 16 a) xa xR) False) (Eq (sdtmndtplgtdt0 (skS.0 16 a) xR xb) False)) % 8.88/9.12 Clause #1421 (by superposition #[1420, 1278]): ∀ (a : Iota), % 8.88/9.12 Or (Eq (aReductOfIn0 xb xa xR) True) % 8.88/9.12 (Or (Eq (sdtmndtplgtdt0 (skS.0 16 a) xR xb) False) (Or (Eq (aReductOfIn0 xb xa xR) True) (Eq False True))) % 8.88/9.12 Clause #1422 (by clausification #[1421]): ∀ (a : Iota), % 8.88/9.12 Or (Eq (aReductOfIn0 xb xa xR) True) % 8.88/9.12 (Or (Eq (sdtmndtplgtdt0 (skS.0 16 a) xR xb) False) (Eq (aReductOfIn0 xb xa xR) True)) % 8.88/9.12 Clause #1423 (by eliminate duplicate literals #[1422]): ∀ (a : Iota), Or (Eq (aReductOfIn0 xb xa xR) True) (Eq (sdtmndtplgtdt0 (skS.0 16 a) xR xb) False) % 8.88/9.12 Clause #1424 (by superposition #[1423, 1271]): Or (Eq (aReductOfIn0 xb xa xR) True) (Or (Eq (aReductOfIn0 xb xa xR) True) (Eq False True)) % 8.88/9.12 Clause #1425 (by clausification #[1424]): Or (Eq (aReductOfIn0 xb xa xR) True) (Eq (aReductOfIn0 xb xa xR) True) % 8.88/9.12 Clause #1426 (by eliminate duplicate literals #[1425]): Eq (aReductOfIn0 xb xa xR) True % 8.88/9.12 Clause #1427 (by backward demodulation #[1426, 289]): Or (Eq True False) (Eq (sdtmndtasgtdt0 xb xR xb) False) % 8.88/9.12 Clause #1460 (by clausification #[1427]): Eq (sdtmndtasgtdt0 xb xR xb) False % 8.88/9.12 Clause #1461 (by superposition #[1460, 285]): Eq False True % 8.88/9.12 Clause #1462 (by clausification #[1461]): False % 8.88/9.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------