%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM023+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:49 PM UTC 2025 % Result : Theorem 144.29s 144.47s % Output : Proof 144.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : COM023+1 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %s % 0.14/0.34 % Computer : n019.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 16:07:08 EDT 2025 % 0.14/0.34 % CPUTime : % 144.29/144.47 SZS status Theorem for theBenchmark.p % 144.29/144.47 SZS output start Proof for theBenchmark.p % 144.29/144.47 Clause #9 (by assumption #[]): Eq % 144.29/144.47 (∀ (W0 : Iota), % 144.29/144.47 aRewritingSystem0 W0 → % 144.29/144.47 Iff (isConfluent0 W0) % 144.29/144.47 (∀ (W1 W2 W3 : Iota), % 144.29/144.47 And (And (And (And (aElement0 W1) (aElement0 W2)) (aElement0 W3)) (sdtmndtasgtdt0 W1 W0 W2)) % 144.29/144.47 (sdtmndtasgtdt0 W1 W0 W3) → % 144.29/144.47 Exists fun W4 => And (And (aElement0 W4) (sdtmndtasgtdt0 W2 W0 W4)) (sdtmndtasgtdt0 W3 W0 W4))) % 144.29/144.47 True % 144.29/144.47 Clause #14 (by assumption #[]): Eq (aRewritingSystem0 xR) True % 144.29/144.47 Clause #16 (by assumption #[]): Eq % 144.29/144.47 (∀ (W0 W1 W2 : Iota), % 144.29/144.47 And (And (And (And (aElement0 W0) (aElement0 W1)) (aElement0 W2)) (sdtmndtasgtdt0 W0 xR W1)) % 144.29/144.47 (sdtmndtasgtdt0 W0 xR W2) → % 144.29/144.47 Exists fun W3 => And (And (aElement0 W3) (sdtmndtasgtdt0 W1 xR W3)) (sdtmndtasgtdt0 W2 xR W3)) % 144.29/144.47 True % 144.29/144.47 Clause #17 (by assumption #[]): Eq (Not (isConfluent0 xR)) True % 144.29/144.47 Clause #20 (by clausification #[17]): Eq (isConfluent0 xR) False % 144.29/144.47 Clause #123 (by clausification #[16]): ∀ (a : Iota), % 144.29/144.47 Eq % 144.29/144.47 (∀ (W1 W2 : Iota), % 144.29/144.47 And (And (And (And (aElement0 a) (aElement0 W1)) (aElement0 W2)) (sdtmndtasgtdt0 a xR W1)) % 144.29/144.47 (sdtmndtasgtdt0 a xR W2) → % 144.29/144.47 Exists fun W3 => And (And (aElement0 W3) (sdtmndtasgtdt0 W1 xR W3)) (sdtmndtasgtdt0 W2 xR W3)) % 144.29/144.47 True % 144.29/144.47 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 144.29/144.47 Eq % 144.29/144.47 (∀ (W2 : Iota), % 144.29/144.47 And (And (And (And (aElement0 a) (aElement0 a_1)) (aElement0 W2)) (sdtmndtasgtdt0 a xR a_1)) % 144.29/144.47 (sdtmndtasgtdt0 a xR W2) → % 144.29/144.47 Exists fun W3 => And (And (aElement0 W3) (sdtmndtasgtdt0 a_1 xR W3)) (sdtmndtasgtdt0 W2 xR W3)) % 144.29/144.47 True % 144.29/144.47 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 144.29/144.47 Eq % 144.29/144.47 (And (And (And (And (aElement0 a) (aElement0 a_1)) (aElement0 a_2)) (sdtmndtasgtdt0 a xR a_1)) % 144.29/144.47 (sdtmndtasgtdt0 a xR a_2) → % 144.29/144.47 Exists fun W3 => And (And (aElement0 W3) (sdtmndtasgtdt0 a_1 xR W3)) (sdtmndtasgtdt0 a_2 xR W3)) % 144.29/144.47 True % 144.29/144.47 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), % 144.29/144.47 Or % 144.29/144.47 (Eq % 144.29/144.47 (And (And (And (And (aElement0 a) (aElement0 a_1)) (aElement0 a_2)) (sdtmndtasgtdt0 a xR a_1)) % 144.29/144.47 (sdtmndtasgtdt0 a xR a_2)) % 144.29/144.47 False) % 144.29/144.47 (Eq (Exists fun W3 => And (And (aElement0 W3) (sdtmndtasgtdt0 a_1 xR W3)) (sdtmndtasgtdt0 a_2 xR W3)) True) % 144.29/144.47 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 144.29/144.47 Or (Eq (Exists fun W3 => And (And (aElement0 W3) (sdtmndtasgtdt0 a xR W3)) (sdtmndtasgtdt0 a_1 xR W3)) True) % 144.29/144.47 (Or (Eq (And (And (And (aElement0 a_2) (aElement0 a)) (aElement0 a_1)) (sdtmndtasgtdt0 a_2 xR a)) False) % 144.29/144.47 (Eq (sdtmndtasgtdt0 a_2 xR a_1) False)) % 144.29/144.47 Clause #128 (by clausification #[127]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.47 Or (Eq (And (And (And (aElement0 a) (aElement0 a_1)) (aElement0 a_2)) (sdtmndtasgtdt0 a xR a_1)) False) % 144.29/144.47 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.47 (Eq % 144.29/144.47 (And (And (aElement0 (skS.0 3 a_1 a_2 a_3)) (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_1 a_2 a_3))) % 144.29/144.47 (sdtmndtasgtdt0 a_2 xR (skS.0 3 a_1 a_2 a_3))) % 144.29/144.47 True)) % 144.29/144.47 Clause #129 (by clausification #[128]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.47 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.47 (Or % 144.29/144.47 (Eq % 144.29/144.47 (And (And (aElement0 (skS.0 3 a_2 a_1 a_3)) (sdtmndtasgtdt0 a_2 xR (skS.0 3 a_2 a_1 a_3))) % 144.29/144.47 (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_2 a_1 a_3))) % 144.29/144.47 True) % 144.29/144.47 (Or (Eq (And (And (aElement0 a) (aElement0 a_2)) (aElement0 a_1)) False) (Eq (sdtmndtasgtdt0 a xR a_2) False))) % 144.29/144.47 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.47 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.47 (Or (Eq (And (And (aElement0 a) (aElement0 a_2)) (aElement0 a_1)) False) % 144.29/144.47 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_2 a_1 a_3)) True))) % 144.29/144.47 Clause #131 (by clausification #[129]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.47 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.47 (Or (Eq (And (And (aElement0 a) (aElement0 a_2)) (aElement0 a_1)) False) % 144.29/144.47 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.47 (Eq (And (aElement0 (skS.0 3 a_2 a_1 a_3)) (sdtmndtasgtdt0 a_2 xR (skS.0 3 a_2 a_1 a_3))) True))) % 144.29/144.47 Clause #132 (by clausification #[130]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.49 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.49 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.49 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_2 a_1 a_3)) True) % 144.29/144.49 (Or (Eq (And (aElement0 a) (aElement0 a_2)) False) (Eq (aElement0 a_1) False)))) % 144.29/144.49 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.49 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.49 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.49 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_2 a_1 a_3)) True) % 144.29/144.49 (Or (Eq (aElement0 a_1) False) (Or (Eq (aElement0 a) False) (Eq (aElement0 a_2) False))))) % 144.29/144.49 Clause #134 (by clausification #[9]): ∀ (a : Iota), % 144.29/144.49 Eq % 144.29/144.49 (aRewritingSystem0 a → % 144.29/144.49 Iff (isConfluent0 a) % 144.29/144.49 (∀ (W1 W2 W3 : Iota), % 144.29/144.49 And (And (And (And (aElement0 W1) (aElement0 W2)) (aElement0 W3)) (sdtmndtasgtdt0 W1 a W2)) % 144.29/144.49 (sdtmndtasgtdt0 W1 a W3) → % 144.29/144.49 Exists fun W4 => And (And (aElement0 W4) (sdtmndtasgtdt0 W2 a W4)) (sdtmndtasgtdt0 W3 a W4))) % 144.29/144.49 True % 144.29/144.49 Clause #135 (by clausification #[134]): ∀ (a : Iota), % 144.29/144.49 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.49 (Eq % 144.29/144.49 (Iff (isConfluent0 a) % 144.29/144.49 (∀ (W1 W2 W3 : Iota), % 144.29/144.49 And (And (And (And (aElement0 W1) (aElement0 W2)) (aElement0 W3)) (sdtmndtasgtdt0 W1 a W2)) % 144.29/144.49 (sdtmndtasgtdt0 W1 a W3) → % 144.29/144.49 Exists fun W4 => And (And (aElement0 W4) (sdtmndtasgtdt0 W2 a W4)) (sdtmndtasgtdt0 W3 a W4))) % 144.29/144.49 True) % 144.29/144.49 Clause #136 (by clausification #[135]): ∀ (a : Iota), % 144.29/144.49 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.49 (Or (Eq (isConfluent0 a) True) % 144.29/144.49 (Eq % 144.29/144.49 (∀ (W1 W2 W3 : Iota), % 144.29/144.49 And (And (And (And (aElement0 W1) (aElement0 W2)) (aElement0 W3)) (sdtmndtasgtdt0 W1 a W2)) % 144.29/144.49 (sdtmndtasgtdt0 W1 a W3) → % 144.29/144.49 Exists fun W4 => And (And (aElement0 W4) (sdtmndtasgtdt0 W2 a W4)) (sdtmndtasgtdt0 W3 a W4)) % 144.29/144.49 False)) % 144.29/144.49 Clause #138 (by clausification #[136]): ∀ (a a_1 : Iota), % 144.29/144.49 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.49 (Or (Eq (isConfluent0 a) True) % 144.29/144.49 (Eq % 144.29/144.49 (Not % 144.29/144.49 (∀ (W2 W3 : Iota), % 144.29/144.49 And % 144.29/144.49 (And (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 W2)) (aElement0 W3)) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a W2)) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a W3) → % 144.29/144.49 Exists fun W4 => And (And (aElement0 W4) (sdtmndtasgtdt0 W2 a W4)) (sdtmndtasgtdt0 W3 a W4))) % 144.29/144.49 True)) % 144.29/144.49 Clause #139 (by clausification #[138]): ∀ (a a_1 : Iota), % 144.29/144.49 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.49 (Or (Eq (isConfluent0 a) True) % 144.29/144.49 (Eq % 144.29/144.49 (∀ (W2 W3 : Iota), % 144.29/144.49 And % 144.29/144.49 (And (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 W2)) (aElement0 W3)) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a W2)) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a W3) → % 144.29/144.49 Exists fun W4 => And (And (aElement0 W4) (sdtmndtasgtdt0 W2 a W4)) (sdtmndtasgtdt0 W3 a W4)) % 144.29/144.49 False)) % 144.29/144.49 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : Iota), % 144.29/144.49 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.49 (Or (Eq (isConfluent0 a) True) % 144.29/144.49 (Eq % 144.29/144.49 (Not % 144.29/144.49 (∀ (W3 : Iota), % 144.29/144.49 And % 144.29/144.49 (And (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) (aElement0 W3)) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 5 a a_1 a_2))) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a W3) → % 144.29/144.49 Exists fun W4 => % 144.29/144.49 And (And (aElement0 W4) (sdtmndtasgtdt0 (skS.0 5 a a_1 a_2) a W4)) (sdtmndtasgtdt0 W3 a W4))) % 144.29/144.49 True)) % 144.29/144.49 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), % 144.29/144.49 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.49 (Or (Eq (isConfluent0 a) True) % 144.29/144.49 (Eq % 144.29/144.49 (∀ (W3 : Iota), % 144.29/144.49 And % 144.29/144.49 (And (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) (aElement0 W3)) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 5 a a_1 a_2))) % 144.29/144.49 (sdtmndtasgtdt0 (skS.0 4 a a_1) a W3) → % 144.29/144.49 Exists fun W4 => % 144.29/144.49 And (And (aElement0 W4) (sdtmndtasgtdt0 (skS.0 5 a a_1 a_2) a W4)) (sdtmndtasgtdt0 W3 a W4)) % 144.29/144.49 False)) % 144.29/144.51 Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.51 (Or (Eq (isConfluent0 a) True) % 144.29/144.51 (Eq % 144.29/144.51 (Not % 144.29/144.51 (And % 144.29/144.51 (And % 144.29/144.51 (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) % 144.29/144.51 (aElement0 (skS.0 6 a a_1 a_2 a_3))) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 5 a a_1 a_2))) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 6 a a_1 a_2 a_3)) → % 144.29/144.51 Exists fun W4 => % 144.29/144.51 And (And (aElement0 W4) (sdtmndtasgtdt0 (skS.0 5 a a_1 a_2) a W4)) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 6 a a_1 a_2 a_3) a W4))) % 144.29/144.51 True)) % 144.29/144.51 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.51 (Or (Eq (isConfluent0 a) True) % 144.29/144.51 (Eq % 144.29/144.51 (And % 144.29/144.51 (And % 144.29/144.51 (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) % 144.29/144.51 (aElement0 (skS.0 6 a a_1 a_2 a_3))) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 5 a a_1 a_2))) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 6 a a_1 a_2 a_3)) → % 144.29/144.51 Exists fun W4 => % 144.29/144.51 And (And (aElement0 W4) (sdtmndtasgtdt0 (skS.0 5 a a_1 a_2) a W4)) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 6 a a_1 a_2 a_3) a W4)) % 144.29/144.51 False)) % 144.29/144.51 Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.51 (Or (Eq (isConfluent0 a) True) % 144.29/144.51 (Eq % 144.29/144.51 (And % 144.29/144.51 (And % 144.29/144.51 (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) (aElement0 (skS.0 6 a a_1 a_2 a_3))) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 5 a a_1 a_2))) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 6 a a_1 a_2 a_3))) % 144.29/144.51 True)) % 144.29/144.51 Clause #145 (by clausification #[143]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.51 (Or (Eq (isConfluent0 a) True) % 144.29/144.51 (Eq % 144.29/144.51 (Exists fun W4 => % 144.29/144.51 And (And (aElement0 W4) (sdtmndtasgtdt0 (skS.0 5 a a_1 a_2) a W4)) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 6 a a_1 a_2 a_3) a W4)) % 144.29/144.51 False)) % 144.29/144.51 Clause #146 (by clausification #[144]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.51 (Or (Eq (isConfluent0 a) True) (Eq (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 6 a a_1 a_2 a_3)) True)) % 144.29/144.51 Clause #147 (by clausification #[144]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (aRewritingSystem0 a) False) % 144.29/144.51 (Or (Eq (isConfluent0 a) True) % 144.29/144.51 (Eq % 144.29/144.51 (And (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) (aElement0 (skS.0 6 a a_1 a_2 a_3))) % 144.29/144.51 (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 5 a a_1 a_2))) % 144.29/144.51 True)) % 144.29/144.51 Clause #148 (by superposition #[146, 14]): ∀ (a a_1 a_2 : Iota), % 144.29/144.51 Or (Eq (isConfluent0 xR) True) % 144.29/144.51 (Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 6 xR a a_1 a_2)) True) (Eq False True)) % 144.29/144.51 Clause #218 (by clausification #[131]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.51 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.51 (Or (Eq (And (aElement0 (skS.0 3 a_2 a_1 a_3)) (sdtmndtasgtdt0 a_2 xR (skS.0 3 a_2 a_1 a_3))) True) % 144.29/144.51 (Or (Eq (And (aElement0 a) (aElement0 a_2)) False) (Eq (aElement0 a_1) False)))) % 144.29/144.51 Clause #219 (by clausification #[218]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.51 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.51 (Or (Eq (And (aElement0 a) (aElement0 a_2)) False) % 144.29/144.51 (Or (Eq (aElement0 a_1) False) (Eq (sdtmndtasgtdt0 a_2 xR (skS.0 3 a_2 a_1 a_3)) True)))) % 144.29/144.51 Clause #220 (by clausification #[218]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.51 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.51 (Or (Eq (And (aElement0 a) (aElement0 a_2)) False) % 144.29/144.51 (Or (Eq (aElement0 a_1) False) (Eq (aElement0 (skS.0 3 a_2 a_1 a_3)) True)))) % 144.29/144.51 Clause #221 (by clausification #[219]): ∀ (a a_1 a_2 a_3 : Iota), % 144.29/144.51 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.29/144.51 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.29/144.51 (Or (Eq (aElement0 a_1) False) % 144.29/144.51 (Or (Eq (sdtmndtasgtdt0 a_2 xR (skS.0 3 a_2 a_1 a_3)) True) % 144.29/144.51 (Or (Eq (aElement0 a) False) (Eq (aElement0 a_2) False))))) % 144.39/144.54 Clause #230 (by clausification #[148]): ∀ (a a_1 a_2 : Iota), Or (Eq (isConfluent0 xR) True) (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 6 xR a a_1 a_2)) True) % 144.39/144.54 Clause #231 (by forward demodulation #[230, 20]): ∀ (a a_1 a_2 : Iota), Or (Eq False True) (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 6 xR a a_1 a_2)) True) % 144.39/144.54 Clause #232 (by clausification #[231]): ∀ (a a_1 a_2 : Iota), Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 6 xR a a_1 a_2)) True % 144.39/144.54 Clause #233 (by superposition #[232, 133]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.54 Or (Eq True False) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_2 a_3) xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 6 xR a a_2 a_3)) False) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False))))) % 144.39/144.54 Clause #234 (by superposition #[232, 221]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.54 Or (Eq True False) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 6 xR a a_2 a_3)) False) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False))))) % 144.39/144.54 Clause #235 (by clausification #[145]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.54 Or (Eq (aRewritingSystem0 a) False) % 144.39/144.54 (Or (Eq (isConfluent0 a) True) % 144.39/144.54 (Eq % 144.39/144.54 (And (And (aElement0 a_1) (sdtmndtasgtdt0 (skS.0 5 a a_2 a_3) a a_1)) % 144.39/144.54 (sdtmndtasgtdt0 (skS.0 6 a a_2 a_3 a_4) a a_1)) % 144.39/144.54 False)) % 144.39/144.54 Clause #236 (by clausification #[235]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.54 Or (Eq (aRewritingSystem0 a) False) % 144.39/144.54 (Or (Eq (isConfluent0 a) True) % 144.39/144.54 (Or (Eq (And (aElement0 a_1) (sdtmndtasgtdt0 (skS.0 5 a a_2 a_3) a a_1)) False) % 144.39/144.54 (Eq (sdtmndtasgtdt0 (skS.0 6 a a_2 a_3 a_4) a a_1) False))) % 144.39/144.54 Clause #237 (by clausification #[236]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.54 Or (Eq (aRewritingSystem0 a) False) % 144.39/144.54 (Or (Eq (isConfluent0 a) True) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 a a_1 a_2 a_3) a a_4) False) % 144.39/144.54 (Or (Eq (aElement0 a_4) False) (Eq (sdtmndtasgtdt0 (skS.0 5 a a_1 a_2) a a_4) False)))) % 144.39/144.54 Clause #238 (by superposition #[237, 14]): ∀ (a a_1 a_2 a_3 : Iota), % 144.39/144.54 Or (Eq (isConfluent0 xR) True) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR a_3) False) % 144.39/144.54 (Or (Eq (aElement0 a_3) False) (Or (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR a_3) False) (Eq False True)))) % 144.39/144.54 Clause #239 (by clausification #[220]): ∀ (a a_1 a_2 a_3 : Iota), % 144.39/144.54 Or (Eq (sdtmndtasgtdt0 a xR a_1) False) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 a xR a_2) False) % 144.39/144.54 (Or (Eq (aElement0 a_1) False) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 3 a_2 a_1 a_3)) True) (Or (Eq (aElement0 a) False) (Eq (aElement0 a_2) False))))) % 144.39/144.54 Clause #240 (by superposition #[239, 232]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.54 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 6 xR a a_2 a_3)) False) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.54 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Or (Eq (aElement0 a_1) False) (Eq False True))))) % 144.39/144.54 Clause #241 (by clausification #[238]): ∀ (a a_1 a_2 a_3 : Iota), % 144.39/144.54 Or (Eq (isConfluent0 xR) True) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR a_3) False) % 144.39/144.54 (Or (Eq (aElement0 a_3) False) (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR a_3) False))) % 144.39/144.54 Clause #242 (by forward demodulation #[241, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 144.39/144.54 Or (Eq False True) % 144.39/144.54 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR a_3) False) % 144.39/144.54 (Or (Eq (aElement0 a_3) False) (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR a_3) False))) % 144.39/144.54 Clause #243 (by clausification #[242]): ∀ (a a_1 a_2 a_3 : Iota), % 144.39/144.54 Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR a_3) False) % 144.39/144.54 (Or (Eq (aElement0 a_3) False) (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR a_3) False)) % 144.39/144.54 Clause #253 (by clausification #[147]): ∀ (a a_1 a_2 : Iota), % 144.39/144.54 Or (Eq (aRewritingSystem0 a) False) % 144.39/144.54 (Or (Eq (isConfluent0 a) True) (Eq (sdtmndtasgtdt0 (skS.0 4 a a_1) a (skS.0 5 a a_1 a_2)) True)) % 144.39/144.57 Clause #254 (by clausification #[147]): ∀ (a a_1 a_2 a_3 : Iota), % 144.39/144.57 Or (Eq (aRewritingSystem0 a) False) % 144.39/144.57 (Or (Eq (isConfluent0 a) True) % 144.39/144.57 (Eq (And (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) (aElement0 (skS.0 6 a a_1 a_2 a_3))) % 144.39/144.57 True)) % 144.39/144.57 Clause #255 (by superposition #[253, 14]): ∀ (a a_1 : Iota), % 144.39/144.57 Or (Eq (isConfluent0 xR) True) (Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 5 xR a a_1)) True) (Eq False True)) % 144.39/144.57 Clause #256 (by clausification #[255]): ∀ (a a_1 : Iota), Or (Eq (isConfluent0 xR) True) (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 5 xR a a_1)) True) % 144.39/144.57 Clause #257 (by forward demodulation #[256, 20]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 5 xR a a_1)) True) % 144.39/144.57 Clause #258 (by clausification #[257]): ∀ (a a_1 : Iota), Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR (skS.0 5 xR a a_1)) True % 144.39/144.57 Clause #264 (by clausification #[254]): ∀ (a a_1 a_2 a_3 : Iota), % 144.39/144.57 Or (Eq (aRewritingSystem0 a) False) (Or (Eq (isConfluent0 a) True) (Eq (aElement0 (skS.0 6 a a_1 a_2 a_3)) True)) % 144.39/144.57 Clause #265 (by clausification #[254]): ∀ (a a_1 a_2 : Iota), % 144.39/144.57 Or (Eq (aRewritingSystem0 a) False) % 144.39/144.57 (Or (Eq (isConfluent0 a) True) (Eq (And (aElement0 (skS.0 4 a a_1)) (aElement0 (skS.0 5 a a_1 a_2))) True)) % 144.39/144.57 Clause #266 (by superposition #[264, 14]): ∀ (a a_1 a_2 : Iota), Or (Eq (isConfluent0 xR) True) (Or (Eq (aElement0 (skS.0 6 xR a a_1 a_2)) True) (Eq False True)) % 144.39/144.57 Clause #267 (by clausification #[266]): ∀ (a a_1 a_2 : Iota), Or (Eq (isConfluent0 xR) True) (Eq (aElement0 (skS.0 6 xR a a_1 a_2)) True) % 144.39/144.57 Clause #268 (by forward demodulation #[267, 20]): ∀ (a a_1 a_2 : Iota), Or (Eq False True) (Eq (aElement0 (skS.0 6 xR a a_1 a_2)) True) % 144.39/144.57 Clause #269 (by clausification #[268]): ∀ (a a_1 a_2 : Iota), Eq (aElement0 (skS.0 6 xR a a_1 a_2)) True % 144.39/144.57 Clause #304 (by clausification #[265]): ∀ (a a_1 a_2 : Iota), % 144.39/144.57 Or (Eq (aRewritingSystem0 a) False) (Or (Eq (isConfluent0 a) True) (Eq (aElement0 (skS.0 5 a a_1 a_2)) True)) % 144.39/144.57 Clause #305 (by clausification #[265]): ∀ (a a_1 : Iota), % 144.39/144.57 Or (Eq (aRewritingSystem0 a) False) (Or (Eq (isConfluent0 a) True) (Eq (aElement0 (skS.0 4 a a_1)) True)) % 144.39/144.57 Clause #306 (by superposition #[304, 14]): ∀ (a a_1 : Iota), Or (Eq (isConfluent0 xR) True) (Or (Eq (aElement0 (skS.0 5 xR a a_1)) True) (Eq False True)) % 144.39/144.57 Clause #307 (by superposition #[305, 14]): ∀ (a : Iota), Or (Eq (isConfluent0 xR) True) (Or (Eq (aElement0 (skS.0 4 xR a)) True) (Eq False True)) % 144.39/144.57 Clause #308 (by clausification #[307]): ∀ (a : Iota), Or (Eq (isConfluent0 xR) True) (Eq (aElement0 (skS.0 4 xR a)) True) % 144.39/144.57 Clause #309 (by forward demodulation #[308, 20]): ∀ (a : Iota), Or (Eq False True) (Eq (aElement0 (skS.0 4 xR a)) True) % 144.39/144.57 Clause #310 (by clausification #[309]): ∀ (a : Iota), Eq (aElement0 (skS.0 4 xR a)) True % 144.39/144.57 Clause #326 (by clausification #[306]): ∀ (a a_1 : Iota), Or (Eq (isConfluent0 xR) True) (Eq (aElement0 (skS.0 5 xR a a_1)) True) % 144.39/144.57 Clause #327 (by forward demodulation #[326, 20]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (aElement0 (skS.0 5 xR a a_1)) True) % 144.39/144.57 Clause #328 (by clausification #[327]): ∀ (a a_1 : Iota), Eq (aElement0 (skS.0 5 xR a a_1)) True % 144.39/144.57 Clause #369 (by clausification #[233]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.57 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.57 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_2 a_3) xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.57 (Or (Eq (aElement0 (skS.0 6 xR a a_2 a_3)) False) % 144.39/144.57 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False)))) % 144.39/144.57 Clause #370 (by forward demodulation #[369, 269]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.57 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.57 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_2 a_3) xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.57 (Or (Eq True False) (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False)))) % 144.39/144.57 Clause #371 (by clausification #[370]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.57 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.57 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_2 a_3) xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False))) % 144.39/144.59 Clause #372 (by forward demodulation #[371, 310]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_2 a_3) xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq True False) (Eq (aElement0 a_1) False))) % 144.39/144.59 Clause #373 (by clausification #[372]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_2 a_3) xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Eq (aElement0 a_1) False)) % 144.39/144.59 Clause #375 (by superposition #[373, 258]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR (skS.0 3 (skS.0 5 xR a a_3) (skS.0 6 xR a a_1 a_2) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 5 xR a a_3)) False) (Eq False True)) % 144.39/144.59 Clause #390 (by clausification #[234]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 6 xR a a_2 a_3)) False) % 144.39/144.59 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False)))) % 144.39/144.59 Clause #391 (by forward demodulation #[390, 269]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq True False) % 144.39/144.59 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False)))) % 144.39/144.59 Clause #392 (by clausification #[391]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False))) % 144.39/144.59 Clause #393 (by forward demodulation #[392, 310]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq True False) (Eq (aElement0 a_1) False))) % 144.39/144.59 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (sdtmndtasgtdt0 a_1 xR (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) (Eq (aElement0 a_1) False)) % 144.39/144.59 Clause #396 (by superposition #[394, 258]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 5 xR a a_1)) False) (Eq False True)) % 144.39/144.59 Clause #411 (by clausification #[240]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 6 xR a a_2 a_3)) False) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False)))) % 144.39/144.59 Clause #412 (by forward demodulation #[411, 269]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq True False) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False)))) % 144.39/144.59 Clause #413 (by clausification #[412]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 4 xR a)) False) (Eq (aElement0 a_1) False))) % 144.39/144.59 Clause #414 (by forward demodulation #[413, 310]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) (Or (Eq True False) (Eq (aElement0 a_1) False))) % 144.39/144.59 Clause #415 (by clausification #[414]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.39/144.59 Or (Eq (sdtmndtasgtdt0 (skS.0 4 xR a) xR a_1) False) % 144.39/144.59 (Or (Eq (aElement0 (skS.0 3 a_1 (skS.0 6 xR a a_2 a_3) a_4)) True) (Eq (aElement0 a_1) False)) % 144.39/144.59 Clause #417 (by superposition #[415, 258]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (aElement0 (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.63/144.79 (Or (Eq (aElement0 (skS.0 5 xR a a_1)) False) (Eq False True)) % 144.63/144.79 Clause #920 (by clausification #[417]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (aElement0 (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.63/144.79 (Eq (aElement0 (skS.0 5 xR a a_1)) False) % 144.63/144.79 Clause #921 (by forward demodulation #[920, 328]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (aElement0 (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True) (Eq True False) % 144.63/144.79 Clause #922 (by clausification #[921]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (aElement0 (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True % 144.63/144.79 Clause #1058 (by clausification #[375]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR (skS.0 3 (skS.0 5 xR a a_3) (skS.0 6 xR a a_1 a_2) a_4)) True) % 144.63/144.79 (Eq (aElement0 (skS.0 5 xR a a_3)) False) % 144.63/144.79 Clause #1059 (by forward demodulation #[1058, 328]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR (skS.0 3 (skS.0 5 xR a a_3) (skS.0 6 xR a a_1 a_2) a_4)) True) % 144.63/144.79 (Eq True False) % 144.63/144.79 Clause #1060 (by clausification #[1059]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Eq (sdtmndtasgtdt0 (skS.0 6 xR a a_1 a_2) xR (skS.0 3 (skS.0 5 xR a a_3) (skS.0 6 xR a a_1 a_2) a_4)) True % 144.63/144.79 Clause #1064 (by superposition #[1060, 243]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq True False) % 144.63/144.79 (Or (Eq (aElement0 (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) False) % 144.63/144.79 (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_2) xR (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) False)) % 144.63/144.79 Clause #1334 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.63/144.79 (Eq (aElement0 (skS.0 5 xR a a_1)) False) % 144.63/144.79 Clause #1335 (by forward demodulation #[1334, 328]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True) % 144.63/144.79 (Eq True False) % 144.63/144.79 Clause #1336 (by clausification #[1335]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) True % 144.63/144.79 Clause #9123 (by clausification #[1064]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq (aElement0 (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) False) % 144.63/144.79 (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_2) xR (skS.0 3 (skS.0 5 xR a a_1) (skS.0 6 xR a a_2 a_3) a_4)) False) % 144.63/144.79 Clause #9124 (by forward demodulation #[9123, 922]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Or (Eq True False) % 144.63/144.79 (Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR (skS.0 3 (skS.0 5 xR a a_2) (skS.0 6 xR a a_1 a_3) a_4)) False) % 144.63/144.79 Clause #9125 (by clausification #[9124]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 144.63/144.79 Eq (sdtmndtasgtdt0 (skS.0 5 xR a a_1) xR (skS.0 3 (skS.0 5 xR a a_2) (skS.0 6 xR a a_1 a_3) a_4)) False % 144.63/144.79 Clause #9126 (by superposition #[9125, 1336]): Eq False True % 144.63/144.79 Clause #9128 (by clausification #[9126]): False % 144.63/144.79 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------