%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ092^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n017.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:58:21 PM UTC 2025 % Result : Theorem 4.32s 4.49s % Output : Proof 4.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : PUZ092^5 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n017.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 20:57:23 EDT 2025 % 0.14/0.35 % CPUTime : % 4.32/4.49 SZS status Theorem for theBenchmark.p % 4.32/4.49 SZS output start Proof for theBenchmark.p % 4.32/4.49 Clause #0 (by assumption #[]): Eq % 4.32/4.49 (Not % 4.32/4.49 (∀ (ACRES MRSACRES BARRY MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.49 And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And (And (And (Eq ACRES MRSACRES) (Eq BARRY MRSBARRY)) (Eq EDEN MRSHALL) → Eq COLE MRSDIX) % 4.32/4.49 (And (And (Eq ACRES MRSACRES) (Eq HALL MRSHALL)) (Eq BARRY MRSCOLE) → Ne DIX MRSEDEN)) % 4.32/4.49 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne ACRES MRSBARRY) → Ne EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq ACRES MRSACRES) (Eq DIX MRSDIX)) (Ne BARRY MRSCOLE) → Eq EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne ACRES MRSBARRY)) % 4.32/4.49 (And (And (And (Eq BARRY MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE BARRY)) (Ne EDEN MRSHALL) → Eq DIX MRSEDEN) → % 4.32/4.49 Or % 4.32/4.49 (Or (Or (Or (Or (Ne ACRES MRSACRES) (Ne BARRY MRSBARRY)) (Ne COLE MRSCOLE)) (Ne DIX MRSDIX)) % 4.32/4.49 (Ne EDEN MRSEDEN)) % 4.32/4.49 (Ne HALL MRSHALL))) % 4.32/4.49 True % 4.32/4.49 Clause #1 (by clausification #[0]): Eq % 4.32/4.49 (∀ (ACRES MRSACRES BARRY MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.49 And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And (And (And (Eq ACRES MRSACRES) (Eq BARRY MRSBARRY)) (Eq EDEN MRSHALL) → Eq COLE MRSDIX) % 4.32/4.49 (And (And (Eq ACRES MRSACRES) (Eq HALL MRSHALL)) (Eq BARRY MRSCOLE) → Ne DIX MRSEDEN)) % 4.32/4.49 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne ACRES MRSBARRY) → Ne EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq ACRES MRSACRES) (Eq DIX MRSDIX)) (Ne BARRY MRSCOLE) → Eq EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne ACRES MRSBARRY)) % 4.32/4.49 (And (And (And (Eq BARRY MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE BARRY)) (Ne EDEN MRSHALL) → Eq DIX MRSEDEN) → % 4.32/4.49 Or (Or (Or (Or (Or (Ne ACRES MRSACRES) (Ne BARRY MRSBARRY)) (Ne COLE MRSCOLE)) (Ne DIX MRSDIX)) (Ne EDEN MRSEDEN)) % 4.32/4.49 (Ne HALL MRSHALL)) % 4.32/4.49 False % 4.32/4.49 Clause #2 (by clausification #[1]): ∀ (a : Iota), % 4.32/4.49 Eq % 4.32/4.49 (Not % 4.32/4.49 (∀ (MRSACRES BARRY MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.49 And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And (And (And (Eq (skS.0 0 a) MRSACRES) (Eq BARRY MRSBARRY)) (Eq EDEN MRSHALL) → Eq COLE MRSDIX) % 4.32/4.49 (And (And (Eq (skS.0 0 a) MRSACRES) (Eq HALL MRSHALL)) (Eq BARRY MRSCOLE) → Ne DIX MRSEDEN)) % 4.32/4.49 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne (skS.0 0 a) MRSBARRY) → % 4.32/4.49 Ne EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq (skS.0 0 a) MRSACRES) (Eq DIX MRSDIX)) (Ne BARRY MRSCOLE) → Eq EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) MRSBARRY)) % 4.32/4.49 (And (And (And (Eq BARRY MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE BARRY)) (Ne EDEN MRSHALL) → Eq DIX MRSEDEN) → % 4.32/4.49 Or % 4.32/4.49 (Or (Or (Or (Or (Ne (skS.0 0 a) MRSACRES) (Ne BARRY MRSBARRY)) (Ne COLE MRSCOLE)) (Ne DIX MRSDIX)) % 4.32/4.49 (Ne EDEN MRSEDEN)) % 4.32/4.49 (Ne HALL MRSHALL))) % 4.32/4.49 True % 4.32/4.49 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 4.32/4.49 Eq % 4.32/4.49 (∀ (MRSACRES BARRY MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.49 And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And % 4.32/4.49 (And (And (And (Eq (skS.0 0 a) MRSACRES) (Eq BARRY MRSBARRY)) (Eq EDEN MRSHALL) → Eq COLE MRSDIX) % 4.32/4.49 (And (And (Eq (skS.0 0 a) MRSACRES) (Eq HALL MRSHALL)) (Eq BARRY MRSCOLE) → Ne DIX MRSEDEN)) % 4.32/4.49 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne (skS.0 0 a) MRSBARRY) → % 4.32/4.49 Ne EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq (skS.0 0 a) MRSACRES) (Eq DIX MRSDIX)) (Ne BARRY MRSCOLE) → Eq EDEN MRSHALL)) % 4.32/4.49 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) MRSBARRY)) % 4.32/4.49 (And (And (And (Eq BARRY MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE BARRY)) (Ne EDEN MRSHALL) → Eq DIX MRSEDEN) → % 4.32/4.51 Or % 4.32/4.51 (Or (Or (Or (Or (Ne (skS.0 0 a) MRSACRES) (Ne BARRY MRSBARRY)) (Ne COLE MRSCOLE)) (Ne DIX MRSDIX)) % 4.32/4.51 (Ne EDEN MRSEDEN)) % 4.32/4.51 (Ne HALL MRSHALL)) % 4.32/4.51 False % 4.32/4.51 Clause #4 (by clausification #[3]): ∀ (a a_1 : Iota), % 4.32/4.51 Eq % 4.32/4.51 (Not % 4.32/4.51 (∀ (BARRY MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.51 And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq BARRY MRSBARRY)) (Eq EDEN MRSHALL) → Eq COLE MRSDIX) % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq BARRY MRSCOLE) → Ne DIX MRSEDEN)) % 4.32/4.51 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne (skS.0 0 a) MRSBARRY) → % 4.32/4.51 Ne EDEN MRSHALL)) % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne BARRY MRSCOLE) → Eq EDEN MRSHALL)) % 4.32/4.51 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) MRSBARRY)) % 4.32/4.51 (And (And (And (Eq BARRY MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE BARRY)) (Ne EDEN MRSHALL) → Eq DIX MRSEDEN) → % 4.32/4.51 Or % 4.32/4.51 (Or (Or (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne BARRY MRSBARRY)) (Ne COLE MRSCOLE)) (Ne DIX MRSDIX)) % 4.32/4.51 (Ne EDEN MRSEDEN)) % 4.32/4.51 (Ne HALL MRSHALL))) % 4.32/4.51 True % 4.32/4.51 Clause #5 (by clausification #[4]): ∀ (a a_1 : Iota), % 4.32/4.51 Eq % 4.32/4.51 (∀ (BARRY MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.51 And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq BARRY MRSBARRY)) (Eq EDEN MRSHALL) → Eq COLE MRSDIX) % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq BARRY MRSCOLE) → Ne DIX MRSEDEN)) % 4.32/4.51 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne (skS.0 0 a) MRSBARRY) → % 4.32/4.51 Ne EDEN MRSHALL)) % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne BARRY MRSCOLE) → Eq EDEN MRSHALL)) % 4.32/4.51 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) MRSBARRY)) % 4.32/4.51 (And (And (And (Eq BARRY MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE BARRY)) (Ne EDEN MRSHALL) → Eq DIX MRSEDEN) → % 4.32/4.51 Or % 4.32/4.51 (Or (Or (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne BARRY MRSBARRY)) (Ne COLE MRSCOLE)) (Ne DIX MRSDIX)) % 4.32/4.51 (Ne EDEN MRSEDEN)) % 4.32/4.51 (Ne HALL MRSHALL)) % 4.32/4.51 False % 4.32/4.51 Clause #6 (by clausification #[5]): ∀ (a a_1 a_2 : Iota), % 4.32/4.51 Eq % 4.32/4.51 (Not % 4.32/4.51 (∀ (MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.51 And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) MRSBARRY)) (Eq EDEN MRSHALL) → % 4.32/4.51 Eq COLE MRSDIX) % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.51 Ne DIX MRSEDEN)) % 4.32/4.51 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne (skS.0 0 a) MRSBARRY) → % 4.32/4.51 Ne EDEN MRSHALL)) % 4.32/4.51 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.51 Eq EDEN MRSHALL)) % 4.32/4.51 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) MRSBARRY)) % 4.32/4.51 (And (And (And (Eq (skS.0 2 a a_1 a_2) MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE (skS.0 2 a a_1 a_2))) % 4.32/4.51 (Ne EDEN MRSHALL) → % 4.32/4.51 Eq DIX MRSEDEN) → % 4.32/4.51 Or % 4.32/4.51 (Or % 4.32/4.51 (Or (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) MRSBARRY)) (Ne COLE MRSCOLE)) % 4.32/4.51 (Ne DIX MRSDIX)) % 4.32/4.51 (Ne EDEN MRSEDEN)) % 4.32/4.51 (Ne HALL MRSHALL))) % 4.32/4.51 True % 4.32/4.51 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Iota), % 4.32/4.53 Eq % 4.32/4.53 (∀ (MRSBARRY COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.53 And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) MRSBARRY)) (Eq EDEN MRSHALL) → % 4.32/4.53 Eq COLE MRSDIX) % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.53 Ne DIX MRSEDEN)) % 4.32/4.53 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) (Ne (skS.0 0 a) MRSBARRY) → % 4.32/4.53 Ne EDEN MRSHALL)) % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.53 Eq EDEN MRSHALL)) % 4.32/4.53 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) MRSBARRY)) % 4.32/4.53 (And (And (And (Eq (skS.0 2 a a_1 a_2) MRSBARRY) (Eq COLE MRSCOLE)) (Eq COLE (skS.0 2 a a_1 a_2))) % 4.32/4.53 (Ne EDEN MRSHALL) → % 4.32/4.53 Eq DIX MRSEDEN) → % 4.32/4.53 Or % 4.32/4.53 (Or % 4.32/4.53 (Or (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) MRSBARRY)) (Ne COLE MRSCOLE)) % 4.32/4.53 (Ne DIX MRSDIX)) % 4.32/4.53 (Ne EDEN MRSEDEN)) % 4.32/4.53 (Ne HALL MRSHALL)) % 4.32/4.53 False % 4.32/4.53 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 a_3 : Iota), % 4.32/4.53 Eq % 4.32/4.53 (Not % 4.32/4.53 (∀ (COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.53 And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.53 (Eq EDEN MRSHALL) → % 4.32/4.53 Eq COLE MRSDIX) % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.53 Ne DIX MRSEDEN)) % 4.32/4.53 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) % 4.32/4.53 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.32/4.53 Ne EDEN MRSHALL)) % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.53 Eq EDEN MRSHALL)) % 4.32/4.53 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.53 (And % 4.32/4.53 (And (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) (Eq COLE MRSCOLE)) % 4.32/4.53 (Eq COLE (skS.0 2 a a_1 a_2))) % 4.32/4.53 (Ne EDEN MRSHALL) → % 4.32/4.53 Eq DIX MRSEDEN) → % 4.32/4.53 Or % 4.32/4.53 (Or % 4.32/4.53 (Or % 4.32/4.53 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.53 (Ne COLE MRSCOLE)) % 4.32/4.53 (Ne DIX MRSDIX)) % 4.32/4.53 (Ne EDEN MRSEDEN)) % 4.32/4.53 (Ne HALL MRSHALL))) % 4.32/4.53 True % 4.32/4.53 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 a_3 : Iota), % 4.32/4.53 Eq % 4.32/4.53 (∀ (COLE MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.53 And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.53 (Eq EDEN MRSHALL) → % 4.32/4.53 Eq COLE MRSDIX) % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.53 Ne DIX MRSEDEN)) % 4.32/4.53 (And (And (And (Eq COLE MRSCOLE) (Eq DIX MRSDIX)) (Eq DIX COLE)) % 4.32/4.53 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.32/4.53 Ne EDEN MRSHALL)) % 4.32/4.53 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.53 Eq EDEN MRSHALL)) % 4.32/4.53 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq COLE MRSDIX) → Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.53 (And % 4.32/4.53 (And (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) (Eq COLE MRSCOLE)) % 4.32/4.53 (Eq COLE (skS.0 2 a a_1 a_2))) % 4.32/4.53 (Ne EDEN MRSHALL) → % 4.32/4.53 Eq DIX MRSEDEN) → % 4.32/4.56 Or % 4.32/4.56 (Or % 4.32/4.56 (Or % 4.32/4.56 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.56 (Ne COLE MRSCOLE)) % 4.32/4.56 (Ne DIX MRSDIX)) % 4.32/4.56 (Ne EDEN MRSEDEN)) % 4.32/4.56 (Ne HALL MRSHALL)) % 4.32/4.56 False % 4.32/4.56 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 4.32/4.56 Eq % 4.32/4.56 (Not % 4.32/4.56 (∀ (MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.56 And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.56 (Eq EDEN MRSHALL) → % 4.32/4.56 Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) % 4.32/4.56 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.56 Ne DIX MRSEDEN)) % 4.32/4.56 (And % 4.32/4.56 (And (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSCOLE) (Eq DIX MRSDIX)) % 4.32/4.56 (Eq DIX (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.32/4.56 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.32/4.56 Ne EDEN MRSHALL)) % 4.32/4.56 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.56 Eq EDEN MRSHALL)) % 4.32/4.56 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) → % 4.32/4.56 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.56 (And % 4.32/4.56 (And (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSCOLE)) % 4.32/4.56 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.32/4.56 (Ne EDEN MRSHALL) → % 4.32/4.56 Eq DIX MRSEDEN) → % 4.32/4.56 Or % 4.32/4.56 (Or % 4.32/4.56 (Or % 4.32/4.56 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.56 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) MRSCOLE)) % 4.32/4.56 (Ne DIX MRSDIX)) % 4.32/4.56 (Ne EDEN MRSEDEN)) % 4.32/4.56 (Ne HALL MRSHALL))) % 4.32/4.56 True % 4.32/4.56 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 4.32/4.56 Eq % 4.32/4.56 (∀ (MRSCOLE DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.56 And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.56 (Eq EDEN MRSHALL) → % 4.32/4.56 Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) % 4.32/4.56 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) (Eq (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.56 Ne DIX MRSEDEN)) % 4.32/4.56 (And % 4.32/4.56 (And (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSCOLE) (Eq DIX MRSDIX)) % 4.32/4.56 (Eq DIX (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.32/4.56 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.32/4.56 Ne EDEN MRSHALL)) % 4.32/4.56 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) (Ne (skS.0 2 a a_1 a_2) MRSCOLE) → % 4.32/4.56 Eq EDEN MRSHALL)) % 4.32/4.56 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) → % 4.32/4.56 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.56 (And % 4.32/4.56 (And (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSCOLE)) % 4.32/4.56 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.32/4.56 (Ne EDEN MRSHALL) → % 4.32/4.56 Eq DIX MRSEDEN) → % 4.32/4.56 Or % 4.32/4.56 (Or % 4.32/4.56 (Or % 4.32/4.56 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.32/4.56 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) MRSCOLE)) % 4.32/4.56 (Ne DIX MRSDIX)) % 4.32/4.56 (Ne EDEN MRSEDEN)) % 4.32/4.56 (Ne HALL MRSHALL)) % 4.32/4.56 False % 4.32/4.56 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 4.32/4.56 Eq % 4.32/4.56 (Not % 4.32/4.56 (∀ (DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.32/4.56 And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And % 4.32/4.56 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.42/4.58 (Eq EDEN MRSHALL) → % 4.42/4.58 Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) % 4.42/4.58 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.42/4.58 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.42/4.58 Ne DIX MRSEDEN)) % 4.42/4.58 (And % 4.42/4.58 (And (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) (Eq DIX MRSDIX)) % 4.42/4.58 (Eq DIX (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.42/4.58 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.42/4.58 Ne EDEN MRSHALL)) % 4.42/4.58 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) % 4.42/4.58 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.42/4.58 Eq EDEN MRSHALL)) % 4.42/4.58 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) → % 4.42/4.58 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.42/4.58 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.42/4.58 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.42/4.58 (Ne EDEN MRSHALL) → % 4.42/4.58 Eq DIX MRSEDEN) → % 4.42/4.58 Or % 4.42/4.58 (Or % 4.42/4.58 (Or % 4.42/4.58 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.42/4.58 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.42/4.58 (Ne DIX MRSDIX)) % 4.42/4.58 (Ne EDEN MRSEDEN)) % 4.42/4.58 (Ne HALL MRSHALL))) % 4.42/4.58 True % 4.42/4.58 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 4.42/4.58 Eq % 4.42/4.58 (∀ (DIX MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.42/4.58 And % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.42/4.58 (Eq EDEN MRSHALL) → % 4.42/4.58 Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) % 4.42/4.58 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.42/4.58 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.42/4.58 Ne DIX MRSEDEN)) % 4.42/4.58 (And % 4.42/4.58 (And (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) (Eq DIX MRSDIX)) % 4.42/4.58 (Eq DIX (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.42/4.58 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.42/4.58 Ne EDEN MRSHALL)) % 4.42/4.58 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq DIX MRSDIX)) % 4.42/4.58 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.42/4.58 Eq EDEN MRSHALL)) % 4.42/4.58 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) → % 4.42/4.58 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.42/4.58 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.42/4.58 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.42/4.58 (Ne EDEN MRSHALL) → % 4.42/4.58 Eq DIX MRSEDEN) → % 4.42/4.58 Or % 4.42/4.58 (Or % 4.42/4.58 (Or % 4.42/4.58 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.42/4.58 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.42/4.58 (Ne DIX MRSDIX)) % 4.42/4.58 (Ne EDEN MRSEDEN)) % 4.42/4.58 (Ne HALL MRSHALL)) % 4.42/4.58 False % 4.42/4.58 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 4.42/4.58 Eq % 4.42/4.58 (Not % 4.42/4.58 (∀ (MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.42/4.58 And % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And % 4.42/4.58 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.42/4.58 (Eq EDEN MRSHALL) → % 4.42/4.58 Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) % 4.45/4.61 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.45/4.61 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.61 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN)) % 4.45/4.61 (And % 4.45/4.61 (And % 4.45/4.61 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.45/4.61 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSDIX)) % 4.45/4.61 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.45/4.61 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.45/4.61 Ne EDEN MRSHALL)) % 4.45/4.61 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSDIX)) % 4.45/4.61 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.61 Eq EDEN MRSHALL)) % 4.45/4.61 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) → % 4.45/4.61 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.61 (And % 4.45/4.61 (And % 4.45/4.61 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.45/4.61 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.45/4.61 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.45/4.61 (Ne EDEN MRSHALL) → % 4.45/4.61 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN) → % 4.45/4.61 Or % 4.45/4.61 (Or % 4.45/4.61 (Or % 4.45/4.61 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.61 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.45/4.61 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSDIX)) % 4.45/4.61 (Ne EDEN MRSEDEN)) % 4.45/4.61 (Ne HALL MRSHALL))) % 4.45/4.61 True % 4.45/4.61 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 4.45/4.61 Eq % 4.45/4.61 (∀ (MRSDIX EDEN MRSEDEN HALL MRSHALL : Iota), % 4.45/4.61 And % 4.45/4.61 (And % 4.45/4.61 (And % 4.45/4.61 (And % 4.45/4.61 (And % 4.45/4.61 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.61 (Eq EDEN MRSHALL) → % 4.45/4.61 Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) % 4.45/4.61 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.45/4.61 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.61 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN)) % 4.45/4.61 (And % 4.45/4.61 (And % 4.45/4.61 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.45/4.61 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSDIX)) % 4.45/4.61 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.45/4.61 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.45/4.61 Ne EDEN MRSHALL)) % 4.45/4.61 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSDIX)) % 4.45/4.61 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.61 Eq EDEN MRSHALL)) % 4.45/4.61 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) (Eq (skS.0 4 a a_1 a_2 a_3 a_4) MRSDIX) → % 4.45/4.61 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.61 (And % 4.45/4.61 (And % 4.45/4.61 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.45/4.61 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.45/4.61 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.45/4.61 (Ne EDEN MRSHALL) → % 4.45/4.61 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN) → % 4.45/4.61 Or % 4.45/4.61 (Or % 4.45/4.61 (Or % 4.45/4.61 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.61 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.45/4.61 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSDIX)) % 4.45/4.61 (Ne EDEN MRSEDEN)) % 4.45/4.61 (Ne HALL MRSHALL)) % 4.45/4.61 False % 4.45/4.61 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 4.45/4.61 Eq % 4.45/4.61 (Not % 4.45/4.61 (∀ (EDEN MRSEDEN HALL MRSHALL : Iota), % 4.45/4.62 And % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.62 (Eq EDEN MRSHALL) → % 4.45/4.62 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.45/4.62 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.45/4.62 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.62 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN)) % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.45/4.62 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.45/4.62 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.45/4.62 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.45/4.62 Ne EDEN MRSHALL)) % 4.45/4.62 (And % 4.45/4.62 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.45/4.62 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.45/4.62 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.62 Eq EDEN MRSHALL)) % 4.45/4.62 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) % 4.45/4.62 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.45/4.62 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.45/4.62 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.45/4.62 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.45/4.62 (Ne EDEN MRSHALL) → % 4.45/4.62 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN) → % 4.45/4.62 Or % 4.45/4.62 (Or % 4.45/4.62 (Or % 4.45/4.62 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.62 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.45/4.62 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.45/4.62 (Ne EDEN MRSEDEN)) % 4.45/4.62 (Ne HALL MRSHALL))) % 4.45/4.62 True % 4.45/4.62 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 4.45/4.62 Eq % 4.45/4.62 (∀ (EDEN MRSEDEN HALL MRSHALL : Iota), % 4.45/4.62 And % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.62 (Eq EDEN MRSHALL) → % 4.45/4.62 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.45/4.62 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.45/4.62 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.62 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN)) % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.45/4.62 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.45/4.62 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.45/4.62 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.45/4.62 Ne EDEN MRSHALL)) % 4.45/4.62 (And % 4.45/4.62 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.45/4.62 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.45/4.62 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.45/4.62 Eq EDEN MRSHALL)) % 4.45/4.62 (And (And (Eq EDEN MRSEDEN) (Eq HALL MRSHALL)) % 4.45/4.62 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.45/4.62 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.45/4.62 (And % 4.45/4.62 (And % 4.45/4.62 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.49/4.65 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.65 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.49/4.65 (Ne EDEN MRSHALL) → % 4.49/4.65 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN) → % 4.49/4.65 Or % 4.49/4.65 (Or % 4.49/4.65 (Or % 4.49/4.65 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.65 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.65 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.65 (Ne EDEN MRSEDEN)) % 4.49/4.65 (Ne HALL MRSHALL)) % 4.49/4.65 False % 4.49/4.65 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 4.49/4.65 Eq % 4.49/4.65 (Not % 4.49/4.65 (∀ (MRSEDEN HALL MRSHALL : Iota), % 4.49/4.65 And % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.65 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.65 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.49/4.65 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.49/4.65 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.65 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN)) % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.49/4.65 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.65 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.49/4.65 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.49/4.65 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.65 (And % 4.49/4.65 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.49/4.65 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.65 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.65 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.65 (And (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSEDEN) (Eq HALL MRSHALL)) % 4.49/4.65 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.49/4.65 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.49/4.65 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.65 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.49/4.65 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.65 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN) → % 4.49/4.65 Or % 4.49/4.65 (Or % 4.49/4.65 (Or % 4.49/4.65 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.65 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.65 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.65 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSEDEN)) % 4.49/4.65 (Ne HALL MRSHALL))) % 4.49/4.65 True % 4.49/4.65 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 4.49/4.65 Eq % 4.49/4.65 (∀ (MRSEDEN HALL MRSHALL : Iota), % 4.49/4.65 And % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And % 4.49/4.65 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.65 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.65 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.49/4.65 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.49/4.65 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.65 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN)) % 4.49/4.65 (And % 4.49/4.66 (And % 4.49/4.66 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.49/4.66 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.66 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.49/4.66 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.49/4.66 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.66 (And % 4.49/4.66 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.49/4.66 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.66 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.66 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.66 (And (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSEDEN) (Eq HALL MRSHALL)) % 4.49/4.66 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.49/4.66 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.66 (And % 4.49/4.66 (And % 4.49/4.66 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.49/4.66 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.66 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.49/4.66 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.66 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) MRSEDEN) → % 4.49/4.66 Or % 4.49/4.66 (Or % 4.49/4.66 (Or % 4.49/4.66 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.66 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.66 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.66 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSEDEN)) % 4.49/4.66 (Ne HALL MRSHALL)) % 4.49/4.66 False % 4.49/4.66 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 4.49/4.66 Eq % 4.49/4.66 (Not % 4.49/4.66 (∀ (HALL MRSHALL : Iota), % 4.49/4.66 And % 4.49/4.66 (And % 4.49/4.66 (And % 4.49/4.66 (And % 4.49/4.66 (And % 4.49/4.66 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.66 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.66 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.49/4.66 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.49/4.66 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.66 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.49/4.66 (And % 4.49/4.66 (And % 4.49/4.66 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.49/4.66 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.66 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.49/4.66 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.49/4.66 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.66 (And % 4.49/4.66 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.49/4.66 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.66 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.66 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.66 (And % 4.49/4.66 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.49/4.66 (Eq HALL MRSHALL)) % 4.49/4.66 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.49/4.66 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.66 (And % 4.49/4.66 (And % 4.49/4.66 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.49/4.66 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.66 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.49/4.70 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.70 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) → % 4.49/4.70 Or % 4.49/4.70 (Or % 4.49/4.70 (Or % 4.49/4.70 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.70 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.70 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.70 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.49/4.70 (Ne HALL MRSHALL))) % 4.49/4.70 True % 4.49/4.70 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 4.49/4.70 Eq % 4.49/4.70 (∀ (HALL MRSHALL : Iota), % 4.49/4.70 And % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.70 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.70 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.49/4.70 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq HALL MRSHALL)) % 4.49/4.70 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.70 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.49/4.70 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.70 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.49/4.70 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.49/4.70 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.70 (And % 4.49/4.70 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.49/4.70 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.70 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.49/4.70 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.49/4.70 (And % 4.49/4.70 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.49/4.70 (Eq HALL MRSHALL)) % 4.49/4.70 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.49/4.70 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.49/4.70 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.70 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.49/4.70 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.70 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) → % 4.49/4.70 Or % 4.49/4.70 (Or % 4.49/4.70 (Or % 4.49/4.70 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.70 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.49/4.70 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.49/4.70 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.49/4.70 (Ne HALL MRSHALL)) % 4.49/4.70 False % 4.49/4.70 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.49/4.70 Eq % 4.49/4.70 (Not % 4.49/4.70 (∀ (MRSHALL : Iota), % 4.49/4.70 And % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And % 4.49/4.70 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.49/4.70 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.49/4.70 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.49/4.70 (And % 4.49/4.70 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.49/4.70 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) MRSHALL)) % 4.55/4.71 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.71 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.71 (And % 4.55/4.71 (And % 4.55/4.71 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.55/4.71 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.71 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.55/4.71 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.55/4.71 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.55/4.71 (And % 4.55/4.71 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.55/4.71 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.71 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.71 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.55/4.71 (And % 4.55/4.71 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.55/4.71 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) MRSHALL)) % 4.55/4.71 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.55/4.71 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.71 (And % 4.55/4.71 (And % 4.55/4.71 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.55/4.71 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.71 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.55/4.71 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.55/4.71 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) → % 4.55/4.71 Or % 4.55/4.71 (Or % 4.55/4.71 (Or % 4.55/4.71 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.71 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.71 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.71 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.71 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) MRSHALL))) % 4.55/4.71 True % 4.55/4.71 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.55/4.71 Eq % 4.55/4.71 (∀ (MRSHALL : Iota), % 4.55/4.71 And % 4.55/4.71 (And % 4.55/4.71 (And % 4.55/4.71 (And % 4.55/4.71 (And % 4.55/4.71 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.71 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.55/4.71 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.55/4.71 (And % 4.55/4.71 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.55/4.71 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) MRSHALL)) % 4.55/4.71 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.71 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.71 (And % 4.55/4.71 (And % 4.55/4.71 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.55/4.71 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.71 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.55/4.71 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.55/4.71 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.55/4.71 (And % 4.55/4.71 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.55/4.71 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.71 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.71 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL)) % 4.55/4.73 (And % 4.55/4.73 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.55/4.73 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) MRSHALL)) % 4.55/4.73 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.55/4.73 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.73 (And % 4.55/4.73 (And % 4.55/4.73 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.55/4.73 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.73 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.55/4.73 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) MRSHALL) → % 4.55/4.73 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) → % 4.55/4.73 Or % 4.55/4.73 (Or % 4.55/4.73 (Or % 4.55/4.73 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.73 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.73 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.73 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.73 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) MRSHALL)) % 4.55/4.73 False % 4.55/4.73 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.55/4.73 Eq % 4.55/4.73 (Not % 4.55/4.73 (And % 4.55/4.73 (And % 4.55/4.73 (And % 4.55/4.73 (And % 4.55/4.73 (And % 4.55/4.73 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.73 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.73 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.55/4.73 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.55/4.73 (And % 4.55/4.73 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.55/4.73 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.55/4.73 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.73 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.73 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.73 (And % 4.55/4.73 (And % 4.55/4.73 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.55/4.73 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.73 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.55/4.73 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.55/4.73 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.73 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.73 (And % 4.55/4.73 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.55/4.73 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.73 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.73 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.73 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.73 (And % 4.55/4.73 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.55/4.73 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.55/4.73 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.73 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.55/4.73 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.73 (And % 4.55/4.73 (And % 4.55/4.73 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.55/4.73 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.73 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.55/4.73 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.73 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.55/4.75 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) → % 4.55/4.75 Or % 4.55/4.75 (Or % 4.55/4.75 (Or % 4.55/4.75 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.75 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.75 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.75 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.75 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)))) % 4.55/4.75 True % 4.55/4.75 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.55/4.75 Eq % 4.55/4.75 (And % 4.55/4.75 (And % 4.55/4.75 (And % 4.55/4.75 (And % 4.55/4.75 (And % 4.55/4.75 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.75 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.55/4.75 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.55/4.75 (And % 4.55/4.75 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.55/4.75 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.75 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.75 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.75 (And % 4.55/4.75 (And % 4.55/4.75 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.55/4.75 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.75 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.55/4.75 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.55/4.75 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.75 (And % 4.55/4.75 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.55/4.75 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.75 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.55/4.75 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.75 (And % 4.55/4.75 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.55/4.75 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.55/4.75 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.55/4.75 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.75 (And % 4.55/4.75 (And % 4.55/4.75 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.55/4.75 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.75 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.55/4.75 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.55/4.75 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) → % 4.55/4.75 Or % 4.55/4.75 (Or % 4.55/4.75 (Or % 4.55/4.75 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.55/4.75 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.55/4.75 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.55/4.75 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.55/4.75 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.55/4.75 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.78 False % 4.61/4.78 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.78 Eq % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.61/4.78 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.61/4.78 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.61/4.78 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.61/4.78 (And % 4.61/4.78 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.61/4.78 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.61/4.78 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.78 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.61/4.78 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.61/4.78 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.61/4.78 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.61/4.78 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.61/4.78 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.61/4.78 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.78 (And % 4.61/4.78 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.61/4.78 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.61/4.78 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.61/4.78 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.78 (And % 4.61/4.78 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.78 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.61/4.78 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.78 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.61/4.78 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.78 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.78 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.61/4.78 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.61/4.78 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.61/4.78 True % 4.61/4.78 Clause #27 (by clausification #[25]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.78 Eq % 4.61/4.78 (Or % 4.61/4.78 (Or % 4.61/4.78 (Or % 4.61/4.78 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.61/4.78 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.78 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.61/4.78 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.61/4.78 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.61/4.78 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.78 False % 4.61/4.78 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.78 Eq % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.78 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.78 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.61/4.78 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.61/4.78 Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.78 True % 4.61/4.78 Clause #29 (by clausification #[26]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.78 Eq % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And % 4.61/4.78 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.61/4.80 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.61/4.80 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.61/4.80 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.61/4.80 (And % 4.61/4.80 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.61/4.80 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.61/4.80 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.80 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.61/4.80 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.61/4.80 (And % 4.61/4.80 (And % 4.61/4.80 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.61/4.80 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.61/4.80 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.61/4.80 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.61/4.80 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.80 (And % 4.61/4.80 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.61/4.80 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.61/4.80 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.61/4.80 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.80 (And % 4.61/4.80 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.80 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.61/4.80 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.80 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.61/4.80 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.61/4.80 True % 4.61/4.80 Clause #30 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.80 Or % 4.61/4.80 (Eq % 4.61/4.80 (And % 4.61/4.80 (And % 4.61/4.80 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.80 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.80 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.61/4.80 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.80 False) % 4.61/4.80 (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True) % 4.61/4.80 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.80 Or (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True) % 4.61/4.80 (Or % 4.61/4.80 (Eq % 4.61/4.80 (And % 4.61/4.80 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.80 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.80 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.61/4.80 False) % 4.61/4.80 (Eq (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.61/4.80 False)) % 4.61/4.80 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.80 Or % 4.61/4.80 (Eq % 4.61/4.80 (And % 4.61/4.80 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.80 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.80 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.61/4.80 False) % 4.61/4.80 (Or % 4.61/4.80 (Eq (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.61/4.80 False) % 4.61/4.80 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.61/4.80 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.80 Or % 4.61/4.80 (Eq (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.61/4.80 False) % 4.61/4.80 (Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.80 (Or % 4.61/4.80 (Eq % 4.61/4.80 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.83 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.83 False) % 4.61/4.83 (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) False))) % 4.61/4.83 Clause #34 (by clausification #[33]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.83 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.83 (Or % 4.61/4.83 (Eq % 4.61/4.83 (And (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.83 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.61/4.83 False) % 4.61/4.83 (Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) False) % 4.61/4.83 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)))) % 4.61/4.83 Clause #35 (by clausification #[34]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.83 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.83 (Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) False) % 4.61/4.83 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.61/4.83 (Or (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) False) % 4.61/4.83 (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False)))) % 4.61/4.83 Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.83 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.83 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.61/4.83 (Or (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) False) % 4.61/4.83 (Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.61/4.83 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))))) % 4.61/4.83 Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.83 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.83 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.61/4.83 (Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.61/4.83 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))))) % 4.61/4.83 Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.83 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.83 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.61/4.83 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) % 4.61/4.83 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.83 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))))) % 4.61/4.83 Clause #39 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.83 Eq % 4.61/4.83 (And % 4.61/4.83 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.61/4.83 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.61/4.83 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.83 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 4.61/4.83 Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.61/4.83 True % 4.61/4.83 Clause #40 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.61/4.83 Eq % 4.61/4.83 (And % 4.61/4.83 (And % 4.61/4.83 (And % 4.61/4.83 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.61/4.83 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.61/4.83 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.61/4.83 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.61/4.83 (And % 4.61/4.83 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.61/4.83 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.61/4.83 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.61/4.83 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.70/4.85 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.70/4.85 (And % 4.70/4.85 (And % 4.70/4.85 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.70/4.85 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.85 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.70/4.85 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.70/4.85 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.85 (And % 4.70/4.85 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.70/4.85 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.85 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.70/4.85 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.85 True % 4.70/4.85 Clause #41 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.85 Or % 4.70/4.85 (Eq % 4.70/4.85 (And % 4.70/4.85 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.70/4.85 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.85 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.85 False) % 4.70/4.85 (Eq (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) True) % 4.70/4.85 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.85 Or (Eq (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) True) % 4.70/4.85 (Or % 4.70/4.85 (Eq % 4.70/4.85 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.70/4.85 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.85 False) % 4.70/4.85 (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False)) % 4.70/4.85 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.85 Or % 4.70/4.85 (Eq % 4.70/4.85 (And (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.70/4.85 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.85 False) % 4.70/4.85 (Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False) % 4.70/4.85 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.70/4.85 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.85 Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False) % 4.70/4.85 (Or (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.70/4.85 (Or (Eq (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) False) % 4.70/4.85 (Eq % 4.70/4.85 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.70/4.85 False))) % 4.70/4.85 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.85 Or (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.70/4.85 (Or (Eq (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) False) % 4.70/4.85 (Or % 4.70/4.85 (Eq % 4.70/4.85 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.70/4.85 False) % 4.70/4.85 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))) % 4.70/4.85 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.85 Or (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.70/4.85 (Or % 4.70/4.85 (Eq % 4.70/4.85 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.70/4.85 False) % 4.70/4.85 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.70/4.85 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)))) % 4.70/4.85 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.88 Or (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.70/4.88 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.70/4.88 (Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.70/4.88 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.88 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)))) % 4.70/4.88 Clause #48 (by clausification #[40]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.88 Eq % 4.70/4.88 (And % 4.70/4.88 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.70/4.88 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.88 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.70/4.88 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.70/4.88 True % 4.70/4.88 Clause #49 (by clausification #[40]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.88 Eq % 4.70/4.88 (And % 4.70/4.88 (And % 4.70/4.88 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.70/4.88 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.70/4.88 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.70/4.88 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.70/4.88 (And % 4.70/4.88 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.70/4.88 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.70/4.88 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.88 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.70/4.88 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.70/4.88 (And % 4.70/4.88 (And % 4.70/4.88 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.70/4.88 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.88 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.70/4.88 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.70/4.88 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.88 True % 4.70/4.88 Clause #50 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.88 Or % 4.70/4.88 (Eq % 4.70/4.88 (And % 4.70/4.88 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.70/4.88 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.88 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.70/4.88 False) % 4.70/4.88 (Eq (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.70/4.88 True) % 4.70/4.88 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.88 Or % 4.70/4.88 (Eq (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.70/4.88 True) % 4.70/4.88 (Or % 4.70/4.88 (Eq % 4.70/4.88 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.70/4.88 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.88 False) % 4.70/4.88 (Eq (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False)) % 4.70/4.88 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.88 Or % 4.70/4.88 (Eq % 4.70/4.88 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.70/4.88 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.70/4.88 False) % 4.70/4.88 (Or (Eq (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.70/4.88 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.70/4.88 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.70/4.88 Or (Eq (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.70/4.88 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.70/4.88 (Or (Eq (Eq (skS.0 0 a) (skS.0 1 a a_1)) False) % 4.70/4.88 (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False))) % 4.70/4.88 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.90 (Or (Eq (Eq (skS.0 0 a) (skS.0 1 a a_1)) False) % 4.75/4.90 (Or (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False) % 4.75/4.90 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)))) % 4.75/4.90 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.90 (Or (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False) % 4.75/4.90 (Or (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) (Ne (skS.0 0 a) (skS.0 1 a a_1)))) % 4.75/4.90 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.90 (Or (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.90 (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) % 4.75/4.90 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))) % 4.75/4.90 Clause #57 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Eq % 4.75/4.90 (And % 4.75/4.90 (And % 4.75/4.90 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.75/4.90 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) → % 4.75/4.90 Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.90 True % 4.75/4.90 Clause #58 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Eq % 4.75/4.90 (And % 4.75/4.90 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.75/4.90 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.75/4.90 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.75/4.90 (And % 4.75/4.90 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.75/4.90 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.75/4.90 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.75/4.90 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.75/4.90 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.75/4.90 True % 4.75/4.90 Clause #59 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Or % 4.75/4.90 (Eq % 4.75/4.90 (And % 4.75/4.90 (And % 4.75/4.90 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.75/4.90 (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3))) % 4.75/4.90 False) % 4.75/4.90 (Eq (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.90 True) % 4.75/4.90 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Or % 4.75/4.90 (Eq (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.90 True) % 4.75/4.90 (Or % 4.75/4.90 (Eq % 4.75/4.90 (And % 4.75/4.90 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.75/4.90 False) % 4.75/4.90 (Eq (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) False)) % 4.75/4.90 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.90 Or % 4.75/4.90 (Eq % 4.75/4.90 (And % 4.75/4.90 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.75/4.90 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))) % 4.75/4.93 False) % 4.75/4.93 (Or (Eq (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) False) % 4.75/4.93 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.75/4.93 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Or (Eq (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) False) % 4.75/4.93 (Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.93 (Or % 4.75/4.93 (Eq % 4.75/4.93 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.93 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.75/4.93 False) % 4.75/4.93 (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) False))) % 4.75/4.93 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.93 (Or % 4.75/4.93 (Eq % 4.75/4.93 (And (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.93 (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.75/4.93 False) % 4.75/4.93 (Or (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) False) % 4.75/4.93 (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)))) % 4.75/4.93 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.93 (Or (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) False) % 4.75/4.93 (Or (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.75/4.93 (Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.75/4.93 (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False)))) % 4.75/4.93 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.93 (Or (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.75/4.93 (Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.75/4.93 (Or (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False) % 4.75/4.93 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4))))) % 4.75/4.93 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.93 (Or (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.75/4.93 (Or (Eq (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False) % 4.75/4.93 (Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.75/4.93 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))))) % 4.75/4.93 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.75/4.93 (Or (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.75/4.93 (Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.75/4.93 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.75/4.93 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))))) % 4.75/4.93 Clause #68 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Eq % 4.75/4.93 (And % 4.75/4.93 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.75/4.93 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.75/4.93 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.75/4.93 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) → % 4.75/4.93 Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.75/4.93 True % 4.75/4.93 Clause #69 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.75/4.93 Eq % 4.75/4.93 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.79/4.96 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) → % 4.79/4.96 Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.79/4.96 True % 4.79/4.96 Clause #70 (by clausification #[68]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Or % 4.79/4.96 (Eq % 4.79/4.96 (And % 4.79/4.96 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.79/4.96 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.79/4.96 (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.79/4.96 False) % 4.79/4.96 (Eq (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True) % 4.79/4.96 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Or (Eq (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True) % 4.79/4.96 (Or % 4.79/4.96 (Eq % 4.79/4.96 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.79/4.96 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.79/4.96 False) % 4.79/4.96 (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False)) % 4.79/4.96 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Or % 4.79/4.96 (Eq % 4.79/4.96 (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) % 4.79/4.96 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.79/4.96 False) % 4.79/4.96 (Or (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.79/4.96 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.79/4.96 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Or (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False) % 4.79/4.96 (Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.79/4.96 (Or (Eq (Eq (skS.0 0 a) (skS.0 1 a a_1)) False) % 4.79/4.96 (Eq % 4.79/4.96 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.79/4.96 False))) % 4.79/4.96 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.79/4.96 (Or (Eq (Eq (skS.0 0 a) (skS.0 1 a a_1)) False) % 4.79/4.96 (Or % 4.79/4.96 (Eq % 4.79/4.96 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.79/4.96 False) % 4.79/4.96 (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)))) % 4.79/4.96 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.79/4.96 (Or % 4.79/4.96 (Eq % 4.79/4.96 (Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.79/4.96 False) % 4.79/4.96 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) (Ne (skS.0 0 a) (skS.0 1 a a_1)))) % 4.79/4.96 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.79/4.96 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.79/4.96 (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) % 4.79/4.96 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)))) % 4.79/4.96 Clause #77 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.96 Eq % 4.79/4.96 (Ne (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 4.79/4.96 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.79/4.96 False % 4.79/4.96 Clause #78 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 4.79/4.96 Eq % 4.79/4.96 (Or % 4.79/4.96 (Or % 4.79/4.96 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.79/4.96 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.79/4.98 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.79/4.98 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.79/4.98 False % 4.79/4.98 Clause #79 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.98 Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11) % 4.79/4.98 Clause #81 (by backward demodulation #[79, 67]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.79/4.98 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 4.79/4.98 (Or (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.79/4.98 (Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.79/4.98 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.79/4.98 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))))) % 4.79/4.98 Clause #83 (by backward contextual literal cutting #[79, 47]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 4.79/4.98 Or (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.79/4.98 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.79/4.98 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 4.79/4.98 Clause #84 (by backward contextual literal cutting #[79, 76]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 4.79/4.98 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 4.79/4.98 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) (Ne (skS.0 0 a) (skS.0 1 a a_1))) % 4.79/4.98 Clause #85 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.98 Or % 4.79/4.98 (Eq % 4.79/4.98 (And (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.79/4.98 (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11))) % 4.79/4.98 False) % 4.79/4.98 (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True) % 4.79/4.98 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.98 Or (Eq (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True) % 4.79/4.98 (Or (Eq (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) False) % 4.79/4.98 (Eq (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.79/4.98 False)) % 4.79/4.98 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.98 Or (Eq (And (Eq (skS.0 0 a) (skS.0 1 a a_1)) (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) False) % 4.79/4.98 (Or % 4.79/4.98 (Eq (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.79/4.98 False) % 4.79/4.98 (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.79/4.98 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.98 Or % 4.79/4.98 (Eq (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.79/4.98 False) % 4.79/4.98 (Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.79/4.98 (Or (Eq (Eq (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) False))) % 4.79/4.98 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.98 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.79/4.98 (Or (Eq (Eq (skS.0 0 a) (skS.0 1 a a_1)) False) % 4.79/4.98 (Or (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) False) % 4.79/4.98 (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)))) % 4.79/4.98 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.79/4.98 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.79/4.98 (Or (Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) False) % 4.79/4.98 (Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.01 (Ne (skS.0 0 a) (skS.0 1 a a_1)))) % 4.85/5.01 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.01 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.85/5.01 (Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.01 (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)))) % 4.85/5.01 Clause #92 (by forward demodulation #[91, 79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.85/5.01 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.85/5.01 (Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 4.85/5.01 (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)))) % 4.85/5.01 Clause #93 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 4.85/5.01 Eq (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) False % 4.85/5.01 Clause #94 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 4.85/5.01 Eq % 4.85/5.01 (Or % 4.85/5.01 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.85/5.01 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.85/5.01 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 4.85/5.01 False % 4.85/5.01 Clause #95 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 4.85/5.01 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 4.85/5.01 Clause #96 (by backward demodulation #[95, 38]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.01 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.01 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.01 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) % 4.85/5.01 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.85/5.01 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))))) % 4.85/5.01 Clause #97 (by backward demodulation #[95, 84]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 4.85/5.01 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.01 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) (Ne (skS.0 0 a) (skS.0 1 a a_1))) % 4.85/5.01 Clause #99 (by backward contextual literal cutting #[95, 83]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 4.85/5.01 Or (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 4.85/5.01 Clause #100 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 4.85/5.01 Eq (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) False % 4.85/5.01 Clause #101 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 4.85/5.01 Eq % 4.85/5.01 (Or (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.85/5.01 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.85/5.01 False % 4.85/5.01 Clause #102 (by clausification #[100]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 4.85/5.01 Clause #104 (by backward demodulation #[102, 92]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.85/5.01 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6)) % 4.85/5.01 (Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 4.85/5.01 (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)))) % 4.85/5.01 Clause #105 (by backward demodulation #[102, 99]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 4.85/5.01 Or (Ne (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6)) % 4.85/5.01 Clause #106 (by backward contextual literal cutting #[102, 56]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.01 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.01 (Or (Eq (skS.0 2 a a_1 a_2) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) (Ne (skS.0 0 a) (skS.0 1 a a_1))) % 4.85/5.04 Clause #107 (by forward demodulation #[81, 102]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.85/5.04 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 4.85/5.04 (Or (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.85/5.04 (Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.85/5.04 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) % 4.85/5.04 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6))))) % 4.85/5.04 Clause #108 (by eliminate resolved literals #[107]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.85/5.04 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 4.85/5.04 (Or (Eq (skS.0 0 a) (skS.0 3 a a_1 a_2 a_3)) % 4.85/5.04 (Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.85/5.04 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)))) % 4.85/5.04 Clause #109 (by forward contextual literal cutting #[108, 105]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.85/5.04 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 4.85/5.04 (Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.85/5.04 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))) % 4.85/5.04 Clause #110 (by clausification #[101]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)) False % 4.85/5.04 Clause #111 (by clausification #[101]): ∀ (a a_1 a_2 a_3 : Iota), % 4.85/5.04 Eq (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) False % 4.85/5.04 Clause #112 (by clausification #[110]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5) % 4.85/5.04 Clause #113 (by backward demodulation #[112, 97]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 4.85/5.04 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.04 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 4 a a_1 a_2 a_3 a_4)) (Ne (skS.0 0 a) (skS.0 1 a a_1))) % 4.85/5.04 Clause #115 (by backward contextual literal cutting #[112, 109]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.85/5.04 Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 4.85/5.04 (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.85/5.04 Clause #116 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) False % 4.85/5.04 Clause #117 (by clausification #[111]): ∀ (a a_1 : Iota), Eq (Ne (skS.0 0 a) (skS.0 1 a a_1)) False % 4.85/5.04 Clause #118 (by clausification #[116]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3) % 4.85/5.04 Clause #120 (by clausification #[117]): ∀ (a a_1 : Iota), Eq (skS.0 0 a) (skS.0 1 a a_1) % 4.85/5.04 Clause #121 (by forward demodulation #[113, 120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 4.85/5.04 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.04 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 4 a a_1 a_2 a_3 a_4)) (Ne (skS.0 0 a) (skS.0 0 a))) % 4.85/5.04 Clause #122 (by eliminate resolved literals #[121]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 4.85/5.04 Or (Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.04 (Ne (skS.0 2 a a_1 a_2) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.85/5.04 Clause #123 (by forward demodulation #[96, 118]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.04 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.04 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.04 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) % 4.85/5.04 (Or (Ne (skS.0 2 a a_1 a_2) (skS.0 2 a a_1 a_2)) % 4.85/5.04 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5))))) % 4.85/5.04 Clause #124 (by eliminate resolved literals #[123]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.04 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.04 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.06 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) % 4.85/5.06 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3 a_4 a_5)))) % 4.85/5.06 Clause #125 (by forward demodulation #[124, 112]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.06 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.06 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.06 (Or (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) % 4.85/5.06 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3 a_4)))) % 4.85/5.06 Clause #126 (by eliminate resolved literals #[125]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.06 Or (Eq (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.06 (Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.06 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2))) % 4.85/5.06 Clause #127 (by forward contextual literal cutting #[126, 122]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.06 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.06 (Ne (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 2 a a_1 a_2)) % 4.85/5.06 Clause #128 (by forward demodulation #[106, 112]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.06 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.06 (Or (Eq (skS.0 2 a a_1 a_2) (skS.0 4 a a_1 a_2 a_3 a_4)) (Ne (skS.0 0 a) (skS.0 1 a a_1))) % 4.85/5.06 Clause #129 (by forward demodulation #[128, 120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.06 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.06 (Or (Eq (skS.0 2 a a_1 a_2) (skS.0 4 a a_1 a_2 a_3 a_4)) (Ne (skS.0 0 a) (skS.0 0 a))) % 4.85/5.06 Clause #130 (by eliminate resolved literals #[129]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.06 Or (Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) % 4.85/5.06 (Eq (skS.0 2 a a_1 a_2) (skS.0 4 a a_1 a_2 a_3 a_4)) % 4.85/5.06 Clause #131 (by forward contextual literal cutting #[130, 127]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 4.85/5.06 Eq (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11) % 4.85/5.06 Clause #132 (by superposition #[131, 79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 4.85/5.06 Eq (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 4.85/5.06 Clause #134 (by backward contextual literal cutting #[132, 115]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Ne (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a a_1 a_2 a_3 a_4) % 4.85/5.06 Clause #135 (by forward demodulation #[104, 132]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 4.85/5.06 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6)) % 4.85/5.06 (Or (Ne (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 4.85/5.06 (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)))) % 4.85/5.06 Clause #136 (by eliminate resolved literals #[135]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 4.85/5.06 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6)) % 4.85/5.06 (Or (Ne (skS.0 0 a) (skS.0 1 a a_1)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.85/5.06 Clause #137 (by forward demodulation #[136, 120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 4.85/5.06 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6)) % 4.85/5.06 (Or (Ne (skS.0 0 a) (skS.0 0 a)) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 4.85/5.06 Clause #138 (by eliminate resolved literals #[137]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 4.85/5.06 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6)) % 4.85/5.06 (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 4.85/5.06 Clause #139 (by forward demodulation #[138, 118]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 4.85/5.06 Or (Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6)) (Ne (skS.0 2 a a_1 a_2) (skS.0 2 a a_1 a_2)) % 4.85/5.06 Clause #140 (by eliminate resolved literals #[139]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (skS.0 4 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2 a_3 a_4 a_5 a_6) % 4.85/5.06 Clause #141 (by forward contextual literal cutting #[140, 134]): False % 4.85/5.06 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------