%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEV107^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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 08:02:51 PM UTC 2025 % Result : Theorem 165.06s 165.29s % Output : Proof 165.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEV107^5 : TPTP v9.2.0. Released v4.0.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 01:15:42 EDT 2025 % 0.13/0.34 % CPUTime : % 165.06/165.29 SZS status Theorem for theBenchmark.p % 165.06/165.29 SZS output start Proof for theBenchmark.p % 165.06/165.29 Clause #0 (by assumption #[]): Eq % 165.06/165.29 (Not % 165.06/165.29 (And (∀ (Xu Xv Xw : a), And (cR Xu Xv) (cR Xw Xv) → cR Xu Xw) (∀ (Xx : a), cR Xx Xx) → % 165.06/165.29 And % 165.06/165.29 (And (∀ (Xx : a), Exists fun Xy => f Xx Xy) % 165.06/165.29 (∀ (Xx : a) (Xy1 Xy2 : Iota), And (f Xx Xy1) (f Xx Xy2) → cS Xy1 Xy2)) % 165.06/165.29 (∀ (Xx1 Xx2 : a) (Xy : Iota), And (f Xx1 Xy) (f Xx2 Xy) → cR Xx1 Xx2) → % 165.06/165.29 And % 165.06/165.29 (And (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) % 165.06/165.29 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.29 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.29 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.29 cR Xx1 Xx2)) % 165.06/165.29 (∀ (Xy : Iota), Exists fun Xx => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))))) % 165.06/165.29 True % 165.06/165.29 Clause #1 (by betaEtaReduce #[0]): Eq % 165.06/165.29 (Not % 165.06/165.29 (And (∀ (Xu Xv Xw : a), And (cR Xu Xv) (cR Xw Xv) → cR Xu Xw) (∀ (Xx : a), cR Xx Xx) → % 165.06/165.29 And (And (∀ (Xx : a), Exists (f Xx)) (∀ (Xx : a) (Xy1 Xy2 : Iota), And (f Xx Xy1) (f Xx Xy2) → cS Xy1 Xy2)) % 165.06/165.29 (∀ (Xx1 Xx2 : a) (Xy : Iota), And (f Xx1 Xy) (f Xx2 Xy) → cR Xx1 Xx2) → % 165.06/165.29 And % 165.06/165.29 (And (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) % 165.06/165.29 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.29 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.29 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.29 cR Xx1 Xx2)) % 165.06/165.29 (∀ (Xy : Iota), Exists fun Xx => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))))) % 165.06/165.29 True % 165.06/165.29 Clause #2 (by clausification #[1]): Eq % 165.06/165.29 (And (∀ (Xu Xv Xw : a), And (cR Xu Xv) (cR Xw Xv) → cR Xu Xw) (∀ (Xx : a), cR Xx Xx) → % 165.06/165.29 And (And (∀ (Xx : a), Exists (f Xx)) (∀ (Xx : a) (Xy1 Xy2 : Iota), And (f Xx Xy1) (f Xx Xy2) → cS Xy1 Xy2)) % 165.06/165.29 (∀ (Xx1 Xx2 : a) (Xy : Iota), And (f Xx1 Xy) (f Xx2 Xy) → cR Xx1 Xx2) → % 165.06/165.29 And % 165.06/165.29 (And (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) % 165.06/165.29 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.29 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.29 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.29 cR Xx1 Xx2)) % 165.06/165.29 (∀ (Xy : Iota), Exists fun Xx => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z)))) % 165.06/165.29 False % 165.06/165.29 Clause #3 (by clausification #[2]): Eq (And (∀ (Xu Xv Xw : a), And (cR Xu Xv) (cR Xw Xv) → cR Xu Xw) (∀ (Xx : a), cR Xx Xx)) True % 165.06/165.29 Clause #4 (by clausification #[2]): Eq % 165.06/165.29 (And (And (∀ (Xx : a), Exists (f Xx)) (∀ (Xx : a) (Xy1 Xy2 : Iota), And (f Xx Xy1) (f Xx Xy2) → cS Xy1 Xy2)) % 165.06/165.29 (∀ (Xx1 Xx2 : a) (Xy : Iota), And (f Xx1 Xy) (f Xx2 Xy) → cR Xx1 Xx2) → % 165.06/165.29 And % 165.06/165.29 (And (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) % 165.06/165.29 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.29 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.29 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.29 cR Xx1 Xx2)) % 165.06/165.29 (∀ (Xy : Iota), Exists fun Xx => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z)))) % 165.06/165.29 False % 165.06/165.29 Clause #5 (by clausification #[3]): Eq (∀ (Xx : a), cR Xx Xx) True % 165.06/165.29 Clause #6 (by clausification #[3]): Eq (∀ (Xu Xv Xw : a), And (cR Xu Xv) (cR Xw Xv) → cR Xu Xw) True % 165.06/165.29 Clause #7 (by clausification #[5]): ∀ (a : a), Eq (cR a a) True % 165.06/165.29 Clause #8 (by clausification #[6]): ∀ (a_1 : a), Eq (∀ (Xv Xw : a), And (cR a_1 Xv) (cR Xw Xv) → cR a_1 Xw) True % 165.06/165.29 Clause #9 (by clausification #[8]): ∀ (a_1 a_2 : a), Eq (∀ (Xw : a), And (cR a_1 a_2) (cR Xw a_2) → cR a_1 Xw) True % 165.06/165.29 Clause #10 (by clausification #[9]): ∀ (a_1 a_2 a : a), Eq (And (cR a_1 a_2) (cR a a_2) → cR a_1 a) True % 165.06/165.29 Clause #11 (by clausification #[10]): ∀ (a_1 a_2 a : a), Or (Eq (And (cR a_1 a_2) (cR a a_2)) False) (Eq (cR a_1 a) True) % 165.06/165.29 Clause #12 (by clausification #[11]): ∀ (a_1 a_2 a : a), Or (Eq (cR a_1 a_2) True) (Or (Eq (cR a_1 a) False) (Eq (cR a_2 a) False)) % 165.06/165.31 Clause #13 (by superposition #[12, 7]): ∀ (a_1 a : a), Or (Eq (cR a_1 a) True) (Or (Eq (cR a a_1) False) (Eq False True)) % 165.06/165.31 Clause #14 (by clausification #[13]): ∀ (a_1 a : a), Or (Eq (cR a_1 a) True) (Eq (cR a a_1) False) % 165.06/165.31 Clause #16 (by clausification #[4]): Eq % 165.06/165.31 (And (And (∀ (Xx : a), Exists (f Xx)) (∀ (Xx : a) (Xy1 Xy2 : Iota), And (f Xx Xy1) (f Xx Xy2) → cS Xy1 Xy2)) % 165.06/165.31 (∀ (Xx1 Xx2 : a) (Xy : Iota), And (f Xx1 Xy) (f Xx2 Xy) → cR Xx1 Xx2)) % 165.06/165.31 True % 165.06/165.31 Clause #17 (by clausification #[4]): Eq % 165.06/165.31 (And % 165.06/165.31 (And (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) % 165.06/165.31 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.31 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.31 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.31 cR Xx1 Xx2)) % 165.06/165.31 (∀ (Xy : Iota), Exists fun Xx => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z)))) % 165.06/165.32 False % 165.06/165.32 Clause #18 (by clausification #[16]): Eq (∀ (Xx1 Xx2 : a) (Xy : Iota), And (f Xx1 Xy) (f Xx2 Xy) → cR Xx1 Xx2) True % 165.06/165.32 Clause #19 (by clausification #[16]): Eq (And (∀ (Xx : a), Exists (f Xx)) (∀ (Xx : a) (Xy1 Xy2 : Iota), And (f Xx Xy1) (f Xx Xy2) → cS Xy1 Xy2)) True % 165.06/165.32 Clause #20 (by clausification #[18]): ∀ (a_1 : a), Eq (∀ (Xx2 : a) (Xy : Iota), And (f a_1 Xy) (f Xx2 Xy) → cR a_1 Xx2) True % 165.06/165.32 Clause #21 (by clausification #[20]): ∀ (a_1 a : a), Eq (∀ (Xy : Iota), And (f a_1 Xy) (f a Xy) → cR a_1 a) True % 165.06/165.32 Clause #22 (by clausification #[21]): ∀ (a_1 : a) (a_2 : Iota) (a : a), Eq (And (f a_1 a_2) (f a a_2) → cR a_1 a) True % 165.06/165.32 Clause #23 (by clausification #[22]): ∀ (a_1 : a) (a_2 : Iota) (a : a), Or (Eq (And (f a_1 a_2) (f a a_2)) False) (Eq (cR a_1 a) True) % 165.06/165.32 Clause #24 (by clausification #[23]): ∀ (a_1 a : a) (a_2 : Iota), Or (Eq (cR a_1 a) True) (Or (Eq (f a_1 a_2) False) (Eq (f a a_2) False)) % 165.06/165.32 Clause #25 (by clausification #[17]): Or % 165.06/165.32 (Eq % 165.06/165.32 (And (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) % 165.06/165.32 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.32 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.32 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.32 cR Xx1 Xx2)) % 165.06/165.32 False) % 165.06/165.32 (Eq (∀ (Xy : Iota), Exists fun Xx => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) False) % 165.06/165.32 Clause #26 (by clausification #[25]): Or (Eq (∀ (Xy : Iota), Exists fun Xx => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) False) % 165.06/165.32 (Or (Eq (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) False) % 165.06/165.32 (Eq % 165.06/165.32 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.32 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.32 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.32 cR Xx1 Xx2) % 165.06/165.32 False)) % 165.06/165.32 Clause #27 (by clausification #[26]): ∀ (a_1 : Iota), % 165.06/165.32 Or (Eq (∀ (Xx : a), Exists fun Xy => ∀ (Xw : a), Or (f Xx Xy) (And (Not (f Xw Xy)) (cR Xx z))) False) % 165.06/165.32 (Or % 165.06/165.32 (Eq % 165.06/165.32 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.32 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.32 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.32 cR Xx1 Xx2) % 165.06/165.32 False) % 165.06/165.32 (Eq (Not (Exists fun Xx => ∀ (Xw : a), Or (f Xx (skS.0 0 a_1)) (And (Not (f Xw (skS.0 0 a_1))) (cR Xx z)))) True)) % 165.06/165.32 Clause #28 (by clausification #[27]): ∀ (a_1 : Iota) (a_2 : a), % 165.06/165.32 Or % 165.06/165.32 (Eq % 165.06/165.32 (∀ (Xy : Iota) (Xx1 Xx2 : a), % 165.06/165.32 And (∀ (Xw : a), Or (f Xx1 Xy) (And (Not (f Xw Xy)) (cR Xx1 z))) % 165.06/165.32 (∀ (Xw : a), Or (f Xx2 Xy) (And (Not (f Xw Xy)) (cR Xx2 z))) → % 165.06/165.32 cR Xx1 Xx2) % 165.06/165.32 False) % 165.06/165.32 (Or % 165.06/165.32 (Eq (Not (Exists fun Xx => ∀ (Xw : a), Or (f Xx (skS.0 0 a_1)) (And (Not (f Xw (skS.0 0 a_1))) (cR Xx z)))) True) % 165.06/165.32 (Eq (Not (Exists fun Xy => ∀ (Xw : a), Or (f (skS.0 1 a_2) Xy) (And (Not (f Xw Xy)) (cR (skS.0 1 a_2) z)))) True)) % 165.06/165.32 Clause #29 (by clausification #[28]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota), % 165.06/165.34 Or (Eq (Not (Exists fun Xx => ∀ (Xw : a), Or (f Xx (skS.0 0 a_1)) (And (Not (f Xw (skS.0 0 a_1))) (cR Xx z)))) True) % 165.06/165.34 (Or % 165.06/165.34 (Eq (Not (Exists fun Xy => ∀ (Xw : a), Or (f (skS.0 1 a_2) Xy) (And (Not (f Xw Xy)) (cR (skS.0 1 a_2) z)))) True) % 165.06/165.34 (Eq % 165.06/165.34 (Not % 165.06/165.34 (∀ (Xx1 Xx2 : a), % 165.06/165.34 And (∀ (Xw : a), Or (f Xx1 (skS.0 2 a_3)) (And (Not (f Xw (skS.0 2 a_3))) (cR Xx1 z))) % 165.06/165.34 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_3)) (And (Not (f Xw (skS.0 2 a_3))) (cR Xx2 z))) → % 165.06/165.34 cR Xx1 Xx2)) % 165.06/165.34 True)) % 165.06/165.34 Clause #30 (by clausification #[29]): ∀ (a_1 : a) (a_2 a_3 : Iota), % 165.06/165.34 Or (Eq (Not (Exists fun Xy => ∀ (Xw : a), Or (f (skS.0 1 a_1) Xy) (And (Not (f Xw Xy)) (cR (skS.0 1 a_1) z)))) True) % 165.06/165.34 (Or % 165.06/165.34 (Eq % 165.06/165.34 (Not % 165.06/165.34 (∀ (Xx1 Xx2 : a), % 165.06/165.34 And (∀ (Xw : a), Or (f Xx1 (skS.0 2 a_2)) (And (Not (f Xw (skS.0 2 a_2))) (cR Xx1 z))) % 165.06/165.34 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_2)) (And (Not (f Xw (skS.0 2 a_2))) (cR Xx2 z))) → % 165.06/165.34 cR Xx1 Xx2)) % 165.06/165.34 True) % 165.06/165.34 (Eq (Exists fun Xx => ∀ (Xw : a), Or (f Xx (skS.0 0 a_3)) (And (Not (f Xw (skS.0 0 a_3))) (cR Xx z))) False)) % 165.06/165.34 Clause #31 (by clausification #[30]): ∀ (a_1 a_2 : Iota) (a_3 : a), % 165.06/165.34 Or % 165.06/165.34 (Eq % 165.06/165.34 (Not % 165.06/165.34 (∀ (Xx1 Xx2 : a), % 165.06/165.34 And (∀ (Xw : a), Or (f Xx1 (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR Xx1 z))) % 165.06/165.34 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR Xx2 z))) → % 165.06/165.34 cR Xx1 Xx2)) % 165.06/165.34 True) % 165.06/165.34 (Or (Eq (Exists fun Xx => ∀ (Xw : a), Or (f Xx (skS.0 0 a_2)) (And (Not (f Xw (skS.0 0 a_2))) (cR Xx z))) False) % 165.06/165.34 (Eq (Exists fun Xy => ∀ (Xw : a), Or (f (skS.0 1 a_3) Xy) (And (Not (f Xw Xy)) (cR (skS.0 1 a_3) z))) False)) % 165.06/165.34 Clause #32 (by clausification #[31]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota), % 165.06/165.34 Or (Eq (Exists fun Xx => ∀ (Xw : a), Or (f Xx (skS.0 0 a_1)) (And (Not (f Xw (skS.0 0 a_1))) (cR Xx z))) False) % 165.06/165.34 (Or (Eq (Exists fun Xy => ∀ (Xw : a), Or (f (skS.0 1 a_2) Xy) (And (Not (f Xw Xy)) (cR (skS.0 1 a_2) z))) False) % 165.06/165.34 (Eq % 165.06/165.34 (∀ (Xx1 Xx2 : a), % 165.06/165.34 And (∀ (Xw : a), Or (f Xx1 (skS.0 2 a_3)) (And (Not (f Xw (skS.0 2 a_3))) (cR Xx1 z))) % 165.06/165.34 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_3)) (And (Not (f Xw (skS.0 2 a_3))) (cR Xx2 z))) → % 165.06/165.34 cR Xx1 Xx2) % 165.06/165.34 False)) % 165.06/165.34 Clause #33 (by clausification #[32]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota), % 165.06/165.34 Or (Eq (Exists fun Xy => ∀ (Xw : a), Or (f (skS.0 1 a_1) Xy) (And (Not (f Xw Xy)) (cR (skS.0 1 a_1) z))) False) % 165.06/165.34 (Or % 165.06/165.34 (Eq % 165.06/165.34 (∀ (Xx1 Xx2 : a), % 165.06/165.34 And (∀ (Xw : a), Or (f Xx1 (skS.0 2 a_2)) (And (Not (f Xw (skS.0 2 a_2))) (cR Xx1 z))) % 165.06/165.34 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_2)) (And (Not (f Xw (skS.0 2 a_2))) (cR Xx2 z))) → % 165.06/165.34 cR Xx1 Xx2) % 165.06/165.34 False) % 165.06/165.34 (Eq (∀ (Xw : a), Or (f a_3 (skS.0 0 a_4)) (And (Not (f Xw (skS.0 0 a_4))) (cR a_3 z))) False)) % 165.06/165.34 Clause #34 (by clausification #[33]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a) (a_5 : Iota), % 165.06/165.34 Or % 165.06/165.34 (Eq % 165.06/165.34 (∀ (Xx1 Xx2 : a), % 165.06/165.34 And (∀ (Xw : a), Or (f Xx1 (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR Xx1 z))) % 165.06/165.34 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR Xx2 z))) → % 165.06/165.34 cR Xx1 Xx2) % 165.06/165.34 False) % 165.06/165.34 (Or (Eq (∀ (Xw : a), Or (f a_2 (skS.0 0 a_3)) (And (Not (f Xw (skS.0 0 a_3))) (cR a_2 z))) False) % 165.06/165.34 (Eq (∀ (Xw : a), Or (f (skS.0 1 a_4) a_5) (And (Not (f Xw a_5)) (cR (skS.0 1 a_4) z))) False)) % 165.06/165.34 Clause #35 (by clausification #[34]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 : a), % 165.06/165.34 Or (Eq (∀ (Xw : a), Or (f a_1 (skS.0 0 a_2)) (And (Not (f Xw (skS.0 0 a_2))) (cR a_1 z))) False) % 165.06/165.34 (Or (Eq (∀ (Xw : a), Or (f (skS.0 1 a_3) a_4) (And (Not (f Xw a_4)) (cR (skS.0 1 a_3) z))) False) % 165.06/165.34 (Eq % 165.06/165.34 (Not % 165.06/165.34 (∀ (Xx2 : a), % 165.06/165.34 And % 165.06/165.34 (∀ (Xw : a), % 165.06/165.34 Or (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) (And (Not (f Xw (skS.0 2 a_5))) (cR (skS.0 3 a_5 a_6) z))) % 165.17/165.37 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_5)) (And (Not (f Xw (skS.0 2 a_5))) (cR Xx2 z))) → % 165.17/165.37 cR (skS.0 3 a_5 a_6) Xx2)) % 165.17/165.37 True)) % 165.17/165.37 Clause #36 (by clausification #[35]): ∀ (a_1 : a) (a_2 a_3 : Iota) (a_4 a_5 : a) (a_6 : Iota) (a_7 : a), % 165.17/165.37 Or (Eq (∀ (Xw : a), Or (f (skS.0 1 a_1) a_2) (And (Not (f Xw a_2)) (cR (skS.0 1 a_1) z))) False) % 165.17/165.37 (Or % 165.17/165.37 (Eq % 165.17/165.37 (Not % 165.17/165.37 (∀ (Xx2 : a), % 165.17/165.37 And % 165.17/165.37 (∀ (Xw : a), % 165.17/165.37 Or (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) (And (Not (f Xw (skS.0 2 a_3))) (cR (skS.0 3 a_3 a_4) z))) % 165.17/165.37 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_3)) (And (Not (f Xw (skS.0 2 a_3))) (cR Xx2 z))) → % 165.17/165.37 cR (skS.0 3 a_3 a_4) Xx2)) % 165.17/165.37 True) % 165.17/165.37 (Eq (Not (Or (f a_5 (skS.0 0 a_6)) (And (Not (f (skS.0 4 a_5 a_6 a_7) (skS.0 0 a_6))) (cR a_5 z)))) True)) % 165.17/165.37 Clause #37 (by clausification #[36]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 a_6 : a) (a_7 : Iota) (a_8 : a), % 165.17/165.37 Or % 165.17/165.37 (Eq % 165.17/165.37 (Not % 165.17/165.37 (∀ (Xx2 : a), % 165.17/165.37 And % 165.17/165.37 (∀ (Xw : a), % 165.17/165.37 Or (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR (skS.0 3 a_1 a_2) z))) % 165.17/165.37 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR Xx2 z))) → % 165.17/165.37 cR (skS.0 3 a_1 a_2) Xx2)) % 165.17/165.37 True) % 165.17/165.37 (Or (Eq (Not (Or (f a_3 (skS.0 0 a_4)) (And (Not (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4))) (cR a_3 z)))) True) % 165.17/165.37 (Eq (Not (Or (f (skS.0 1 a_6) a_7) (And (Not (f (skS.0 5 a_6 a_7 a_8) a_7)) (cR (skS.0 1 a_6) z)))) True)) % 165.17/165.37 Clause #38 (by clausification #[37]): ∀ (a_1 : a) (a_2 : Iota) (a_3 a_4 : a) (a_5 : Iota) (a_6 : a) (a_7 : Iota) (a_8 : a), % 165.17/165.37 Or (Eq (Not (Or (f a_1 (skS.0 0 a_2)) (And (Not (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2))) (cR a_1 z)))) True) % 165.17/165.37 (Or (Eq (Not (Or (f (skS.0 1 a_4) a_5) (And (Not (f (skS.0 5 a_4 a_5 a_6) a_5)) (cR (skS.0 1 a_4) z)))) True) % 165.17/165.37 (Eq % 165.17/165.37 (∀ (Xx2 : a), % 165.17/165.37 And % 165.17/165.37 (∀ (Xw : a), % 165.17/165.37 Or (f (skS.0 3 a_7 a_8) (skS.0 2 a_7)) (And (Not (f Xw (skS.0 2 a_7))) (cR (skS.0 3 a_7 a_8) z))) % 165.17/165.37 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_7)) (And (Not (f Xw (skS.0 2 a_7))) (cR Xx2 z))) → % 165.17/165.37 cR (skS.0 3 a_7 a_8) Xx2) % 165.17/165.37 False)) % 165.17/165.37 Clause #39 (by clausification #[38]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 : a) (a_7 : Iota) (a_8 : a), % 165.17/165.37 Or (Eq (Not (Or (f (skS.0 1 a_1) a_2) (And (Not (f (skS.0 5 a_1 a_2 a_3) a_2)) (cR (skS.0 1 a_1) z)))) True) % 165.17/165.37 (Or % 165.17/165.37 (Eq % 165.17/165.37 (∀ (Xx2 : a), % 165.17/165.37 And % 165.17/165.37 (∀ (Xw : a), % 165.17/165.37 Or (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) (And (Not (f Xw (skS.0 2 a_4))) (cR (skS.0 3 a_4 a_5) z))) % 165.17/165.37 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_4)) (And (Not (f Xw (skS.0 2 a_4))) (cR Xx2 z))) → % 165.17/165.37 cR (skS.0 3 a_4 a_5) Xx2) % 165.17/165.37 False) % 165.17/165.37 (Eq (Or (f a_6 (skS.0 0 a_7)) (And (Not (f (skS.0 4 a_6 a_7 a_8) (skS.0 0 a_7))) (cR a_6 z))) False)) % 165.17/165.37 Clause #40 (by clausification #[39]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 a_6 : a) (a_7 : Iota) (a_8 : a), % 165.17/165.37 Or % 165.17/165.37 (Eq % 165.17/165.37 (∀ (Xx2 : a), % 165.17/165.37 And % 165.17/165.37 (∀ (Xw : a), % 165.17/165.37 Or (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR (skS.0 3 a_1 a_2) z))) % 165.17/165.37 (∀ (Xw : a), Or (f Xx2 (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR Xx2 z))) → % 165.17/165.37 cR (skS.0 3 a_1 a_2) Xx2) % 165.17/165.37 False) % 165.17/165.37 (Or (Eq (Or (f a_3 (skS.0 0 a_4)) (And (Not (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4))) (cR a_3 z))) False) % 165.17/165.37 (Eq (Or (f (skS.0 1 a_6) a_7) (And (Not (f (skS.0 5 a_6 a_7 a_8) a_7)) (cR (skS.0 1 a_6) z))) False)) % 165.17/165.37 Clause #41 (by clausification #[40]): ∀ (a_1 : a) (a_2 : Iota) (a_3 a_4 : a) (a_5 : Iota) (a_6 : a) (a_7 : Iota) (a_8 a_9 : a), % 165.17/165.37 Or (Eq (Or (f a_1 (skS.0 0 a_2)) (And (Not (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2))) (cR a_1 z))) False) % 165.17/165.37 (Or (Eq (Or (f (skS.0 1 a_4) a_5) (And (Not (f (skS.0 5 a_4 a_5 a_6) a_5)) (cR (skS.0 1 a_4) z))) False) % 165.17/165.37 (Eq % 165.17/165.37 (Not % 165.17/165.37 (And % 165.17/165.37 (∀ (Xw : a), % 165.17/165.37 Or (f (skS.0 3 a_7 a_8) (skS.0 2 a_7)) (And (Not (f Xw (skS.0 2 a_7))) (cR (skS.0 3 a_7 a_8) z))) % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 6 a_7 a_8 a_9) (skS.0 2 a_7)) % 165.17/165.39 (And (Not (f Xw (skS.0 2 a_7))) (cR (skS.0 6 a_7 a_8 a_9) z))) → % 165.17/165.39 cR (skS.0 3 a_7 a_8) (skS.0 6 a_7 a_8 a_9))) % 165.17/165.39 True)) % 165.17/165.39 Clause #42 (by clausification #[41]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 a_7 : a) (a_8 : Iota) (a_9 : a), % 165.17/165.39 Or (Eq (Or (f (skS.0 1 a_1) a_2) (And (Not (f (skS.0 5 a_1 a_2 a_3) a_2)) (cR (skS.0 1 a_1) z))) False) % 165.17/165.39 (Or % 165.17/165.39 (Eq % 165.17/165.39 (Not % 165.17/165.39 (And % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) (And (Not (f Xw (skS.0 2 a_4))) (cR (skS.0 3 a_4 a_5) z))) % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) % 165.17/165.39 (And (Not (f Xw (skS.0 2 a_4))) (cR (skS.0 6 a_4 a_5 a_6) z))) → % 165.17/165.39 cR (skS.0 3 a_4 a_5) (skS.0 6 a_4 a_5 a_6))) % 165.17/165.39 True) % 165.17/165.39 (Eq (And (Not (f (skS.0 4 a_7 a_8 a_9) (skS.0 0 a_8))) (cR a_7 z)) False)) % 165.17/165.39 Clause #43 (by clausification #[41]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 a_7 : a) (a_8 : Iota), % 165.17/165.39 Or (Eq (Or (f (skS.0 1 a_1) a_2) (And (Not (f (skS.0 5 a_1 a_2 a_3) a_2)) (cR (skS.0 1 a_1) z))) False) % 165.17/165.39 (Or % 165.17/165.39 (Eq % 165.17/165.39 (Not % 165.17/165.39 (And % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) (And (Not (f Xw (skS.0 2 a_4))) (cR (skS.0 3 a_4 a_5) z))) % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) % 165.17/165.39 (And (Not (f Xw (skS.0 2 a_4))) (cR (skS.0 6 a_4 a_5 a_6) z))) → % 165.17/165.39 cR (skS.0 3 a_4 a_5) (skS.0 6 a_4 a_5 a_6))) % 165.17/165.39 True) % 165.17/165.39 (Eq (f a_7 (skS.0 0 a_8)) False)) % 165.17/165.39 Clause #45 (by clausification #[42]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a) (a_5 : Iota) (a_6 a_7 : a) (a_8 : Iota), % 165.17/165.39 Or % 165.17/165.39 (Eq % 165.17/165.39 (Not % 165.17/165.39 (And % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR (skS.0 3 a_1 a_2) z))) % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) % 165.17/165.39 (And (Not (f Xw (skS.0 2 a_1))) (cR (skS.0 6 a_1 a_2 a_3) z))) → % 165.17/165.39 cR (skS.0 3 a_1 a_2) (skS.0 6 a_1 a_2 a_3))) % 165.17/165.39 True) % 165.17/165.39 (Or (Eq (And (Not (f (skS.0 4 a_4 a_5 a_6) (skS.0 0 a_5))) (cR a_4 z)) False) (Eq (f (skS.0 1 a_7) a_8) False)) % 165.17/165.39 Clause #61 (by clausification #[19]): Eq (∀ (Xx : a), Exists (f Xx)) True % 165.17/165.39 Clause #67 (by clausification #[61]): ∀ (a : a), Eq (Exists (f a)) True % 165.17/165.39 Clause #68 (by clausification #[67]): ∀ (a_1 : a) (a_2 : Iota), Eq (f a_1 (skS.0 7 a_1 a_2)) True % 165.17/165.39 Clause #76 (by clausification #[43]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a) (a_5 : Iota) (a_6 : a) (a_7 : Iota), % 165.17/165.39 Or % 165.17/165.39 (Eq % 165.17/165.39 (Not % 165.17/165.39 (And % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) (And (Not (f Xw (skS.0 2 a_1))) (cR (skS.0 3 a_1 a_2) z))) % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) % 165.17/165.39 (And (Not (f Xw (skS.0 2 a_1))) (cR (skS.0 6 a_1 a_2 a_3) z))) → % 165.17/165.39 cR (skS.0 3 a_1 a_2) (skS.0 6 a_1 a_2 a_3))) % 165.17/165.39 True) % 165.17/165.39 (Or (Eq (f a_4 (skS.0 0 a_5)) False) (Eq (f (skS.0 1 a_6) a_7) False)) % 165.17/165.39 Clause #88 (by clausification #[76]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.17/165.39 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.17/165.39 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.17/165.39 (Eq % 165.17/165.39 (And % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) (And (Not (f Xw (skS.0 2 a_5))) (cR (skS.0 3 a_5 a_6) z))) % 165.17/165.39 (∀ (Xw : a), % 165.17/165.39 Or (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) % 165.17/165.39 (And (Not (f Xw (skS.0 2 a_5))) (cR (skS.0 6 a_5 a_6 a_7) z))) → % 165.17/165.39 cR (skS.0 3 a_5 a_6) (skS.0 6 a_5 a_6 a_7)) % 165.17/165.39 False)) % 165.17/165.39 Clause #89 (by clausification #[88]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.17/165.39 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.17/165.39 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.17/165.39 (Eq % 165.17/165.39 (And % 165.17/165.39 (∀ (Xw : a), Or (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) (And (Not (f Xw (skS.0 2 a_5))) (cR (skS.0 3 a_5 a_6) z))) % 165.21/165.42 (∀ (Xw : a), % 165.21/165.42 Or (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) (And (Not (f Xw (skS.0 2 a_5))) (cR (skS.0 6 a_5 a_6 a_7) z)))) % 165.21/165.42 True)) % 165.21/165.42 Clause #90 (by clausification #[88]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) (Eq (cR (skS.0 3 a_5 a_6) (skS.0 6 a_5 a_6 a_7)) False)) % 165.21/165.42 Clause #91 (by clausification #[89]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.21/165.42 (Eq % 165.21/165.42 (∀ (Xw : a), % 165.21/165.42 Or (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) (And (Not (f Xw (skS.0 2 a_5))) (cR (skS.0 6 a_5 a_6 a_7) z))) % 165.21/165.42 True)) % 165.21/165.42 Clause #92 (by clausification #[89]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.21/165.42 (Eq (∀ (Xw : a), Or (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) (And (Not (f Xw (skS.0 2 a_5))) (cR (skS.0 3 a_5 a_6) z))) % 165.21/165.42 True)) % 165.21/165.42 Clause #93 (by clausification #[91]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 a_8 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.21/165.42 (Eq (Or (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) (And (Not (f a_8 (skS.0 2 a_5))) (cR (skS.0 6 a_5 a_6 a_7) z))) % 165.21/165.42 True)) % 165.21/165.42 Clause #94 (by clausification #[93]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 a_8 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.21/165.42 (Or (Eq (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) True) % 165.21/165.42 (Eq (And (Not (f a_8 (skS.0 2 a_5))) (cR (skS.0 6 a_5 a_6 a_7) z)) True))) % 165.21/165.42 Clause #95 (by clausification #[94]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.21/165.42 (Or (Eq (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) True) (Eq (cR (skS.0 6 a_5 a_6 a_7) z) True))) % 165.21/165.42 Clause #96 (by clausification #[94]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 a_8 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.21/165.42 (Or (Eq (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) True) (Eq (Not (f a_8 (skS.0 2 a_5))) True))) % 165.21/165.42 Clause #97 (by clausification #[96]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 a_8 : a), % 165.21/165.42 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.21/165.42 (Or (Eq (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) True) (Eq (f a_8 (skS.0 2 a_5)) False))) % 165.21/165.42 Clause #99 (by clausification #[45]): ∀ (a_1 : a) (a_2 : Iota) (a_3 a_4 : a) (a_5 a_6 : Iota) (a_7 a_8 : a), % 165.21/165.42 Or (Eq (And (Not (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2))) (cR a_1 z)) False) % 165.21/165.42 (Or (Eq (f (skS.0 1 a_4) a_5) False) % 165.21/165.42 (Eq % 165.21/165.42 (And % 165.21/165.42 (∀ (Xw : a), % 165.21/165.42 Or (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) (And (Not (f Xw (skS.0 2 a_6))) (cR (skS.0 3 a_6 a_7) z))) % 165.21/165.42 (∀ (Xw : a), % 165.21/165.42 Or (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) % 165.21/165.42 (And (Not (f Xw (skS.0 2 a_6))) (cR (skS.0 6 a_6 a_7 a_8) z))) → % 165.21/165.42 cR (skS.0 3 a_6 a_7) (skS.0 6 a_6 a_7 a_8)) % 165.21/165.42 False)) % 165.21/165.42 Clause #100 (by clausification #[99]): ∀ (a_1 : a) (a_2 a_3 : Iota) (a_4 a_5 a_6 : a) (a_7 : Iota) (a_8 : a), % 165.21/165.42 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.42 (Or % 165.21/165.42 (Eq % 165.21/165.42 (And % 165.21/165.42 (∀ (Xw : a), % 165.21/165.42 Or (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) (And (Not (f Xw (skS.0 2 a_3))) (cR (skS.0 3 a_3 a_4) z))) % 165.21/165.42 (∀ (Xw : a), % 165.21/165.42 Or (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) % 165.21/165.42 (And (Not (f Xw (skS.0 2 a_3))) (cR (skS.0 6 a_3 a_4 a_5) z))) → % 165.21/165.42 cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_4 a_5)) % 165.21/165.42 False) % 165.21/165.42 (Or (Eq (Not (f (skS.0 4 a_6 a_7 a_8) (skS.0 0 a_7))) False) (Eq (cR a_6 z) False))) % 165.21/165.42 Clause #101 (by clausification #[100]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.21/165.42 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (Not (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4))) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Eq % 165.21/165.45 (And % 165.21/165.45 (∀ (Xw : a), % 165.21/165.45 Or (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) (And (Not (f Xw (skS.0 2 a_6))) (cR (skS.0 3 a_6 a_7) z))) % 165.21/165.45 (∀ (Xw : a), % 165.21/165.45 Or (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) (And (Not (f Xw (skS.0 2 a_6))) (cR (skS.0 6 a_6 a_7 a_8) z)))) % 165.21/165.45 True))) % 165.21/165.45 Clause #102 (by clausification #[100]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (Not (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4))) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) (Eq (cR (skS.0 3 a_6 a_7) (skS.0 6 a_6 a_7 a_8)) False))) % 165.21/165.45 Clause #103 (by clausification #[101]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 : a) (a_7 : Iota) (a_8 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Or % 165.21/165.45 (Eq % 165.21/165.45 (And % 165.21/165.45 (∀ (Xw : a), % 165.21/165.45 Or (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) (And (Not (f Xw (skS.0 2 a_4))) (cR (skS.0 3 a_4 a_5) z))) % 165.21/165.45 (∀ (Xw : a), % 165.21/165.45 Or (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) (And (Not (f Xw (skS.0 2 a_4))) (cR (skS.0 6 a_4 a_5 a_6) z)))) % 165.21/165.45 True) % 165.21/165.45 (Eq (f (skS.0 4 a_3 a_7 a_8) (skS.0 0 a_7)) True))) % 165.21/165.45 Clause #104 (by clausification #[103]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.21/165.45 (Eq % 165.21/165.45 (∀ (Xw : a), % 165.21/165.45 Or (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) (And (Not (f Xw (skS.0 2 a_6))) (cR (skS.0 6 a_6 a_7 a_8) z))) % 165.21/165.45 True))) % 165.21/165.45 Clause #105 (by clausification #[103]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.21/165.45 (Eq % 165.21/165.45 (∀ (Xw : a), Or (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) (And (Not (f Xw (skS.0 2 a_6))) (cR (skS.0 3 a_6 a_7) z))) % 165.21/165.45 True))) % 165.21/165.45 Clause #106 (by clausification #[104]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 a_9 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.21/165.45 (Eq (Or (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) (And (Not (f a_9 (skS.0 2 a_6))) (cR (skS.0 6 a_6 a_7 a_8) z))) % 165.21/165.45 True))) % 165.21/165.45 Clause #107 (by clausification #[106]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 a_9 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.21/165.45 (Or (Eq (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) True) % 165.21/165.45 (Eq (And (Not (f a_9 (skS.0 2 a_6))) (cR (skS.0 6 a_6 a_7 a_8) z)) True)))) % 165.21/165.45 Clause #108 (by clausification #[107]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.21/165.45 (Or (Eq (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) True) (Eq (cR (skS.0 6 a_6 a_7 a_8) z) True)))) % 165.21/165.45 Clause #109 (by clausification #[107]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 a_9 : a), % 165.21/165.45 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.21/165.45 (Or (Eq (cR a_3 z) False) % 165.21/165.45 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.21/165.45 (Or (Eq (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) True) (Eq (Not (f a_9 (skS.0 2 a_6))) True)))) % 165.21/165.45 Clause #110 (by superposition #[108, 68]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.21/165.45 Or (Eq (cR a_1 z) False) % 165.21/165.45 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.21/165.45 (Or (Eq (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) True) % 165.21/165.45 (Or (Eq (cR (skS.0 6 a_4 a_5 a_6) z) True) (Eq False True)))) % 165.21/165.45 Clause #114 (by clausification #[102]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 : a) (a_7 : Iota) (a_8 : a), % 165.28/165.48 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.28/165.48 (Or (Eq (cR a_3 z) False) % 165.28/165.48 (Or (Eq (cR (skS.0 3 a_4 a_5) (skS.0 6 a_4 a_5 a_6)) False) (Eq (f (skS.0 4 a_3 a_7 a_8) (skS.0 0 a_7)) True))) % 165.28/165.48 Clause #115 (by superposition #[114, 68]): ∀ (a_1 : a) (a_2 : Iota) (a_3 a_4 : a) (a_5 : Iota) (a_6 : a), % 165.28/165.48 Or (Eq (cR a_1 z) False) % 165.28/165.48 (Or (Eq (cR (skS.0 3 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) False) % 165.28/165.48 (Or (Eq (f (skS.0 4 a_1 a_5 a_6) (skS.0 0 a_5)) True) (Eq False True))) % 165.28/165.48 Clause #116 (by clausification #[115]): ∀ (a_1 : a) (a_2 : Iota) (a_3 a_4 : a) (a_5 : Iota) (a_6 : a), % 165.28/165.48 Or (Eq (cR a_1 z) False) % 165.28/165.48 (Or (Eq (cR (skS.0 3 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) False) (Eq (f (skS.0 4 a_1 a_5 a_6) (skS.0 0 a_5)) True)) % 165.28/165.48 Clause #117 (by superposition #[116, 7]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.28/165.48 Or (Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_1 a_2 a_3)) False) % 165.28/165.48 (Or (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True) (Eq False True)) % 165.28/165.48 Clause #118 (by clausification #[117]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.28/165.48 Or (Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_1 a_2 a_3)) False) (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True) % 165.28/165.48 Clause #119 (by clausification #[110]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.28/165.48 Or (Eq (cR a_1 z) False) % 165.28/165.48 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.28/165.48 (Or (Eq (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) True) (Eq (cR (skS.0 6 a_4 a_5 a_6) z) True))) % 165.28/165.48 Clause #120 (by superposition #[119, 7]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.28/165.48 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.28/165.48 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Or (Eq (cR (skS.0 6 a_3 a_4 a_5) z) True) (Eq False True))) % 165.28/165.48 Clause #121 (by clausification #[120]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.28/165.48 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.28/165.48 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Eq (cR (skS.0 6 a_3 a_4 a_5) z) True)) % 165.28/165.48 Clause #123 (by superposition #[121, 95]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a) (a_5 a_6 : Iota) (a_7 a_8 : a), % 165.28/165.48 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) % 165.28/165.48 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.28/165.48 (Or (Eq True False) % 165.28/165.48 (Or (Eq (f (skS.0 1 a_4) a_5) False) % 165.28/165.48 (Or (Eq (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) True) (Eq (cR (skS.0 6 a_6 a_7 a_8) z) True))))) % 165.28/165.48 Clause #148 (by clausification #[92]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.28/165.48 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.28/165.48 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.28/165.48 (Eq (Or (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) (And (Not (f a_7 (skS.0 2 a_5))) (cR (skS.0 3 a_5 a_6) z))) True)) % 165.28/165.48 Clause #149 (by clausification #[148]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.28/165.48 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.28/165.48 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.28/165.48 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) % 165.28/165.48 (Eq (And (Not (f a_7 (skS.0 2 a_5))) (cR (skS.0 3 a_5 a_6) z)) True))) % 165.28/165.48 Clause #150 (by clausification #[149]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 : a), % 165.28/165.48 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.28/165.48 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.28/165.48 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (cR (skS.0 3 a_5 a_6) z) True))) % 165.28/165.48 Clause #151 (by clausification #[149]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.28/165.48 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.28/165.48 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.28/165.48 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (Not (f a_7 (skS.0 2 a_5))) True))) % 165.28/165.48 Clause #155 (by clausification #[151]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.28/165.48 Or (Eq (f a_1 (skS.0 0 a_2)) False) % 165.28/165.48 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.28/165.48 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (f a_7 (skS.0 2 a_5)) False))) % 165.28/165.48 Clause #200 (by clausification #[109]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 a_9 : a), % 165.28/165.48 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.28/165.48 (Or (Eq (cR a_3 z) False) % 165.28/165.48 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.28/165.50 (Or (Eq (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) True) (Eq (f a_9 (skS.0 2 a_6)) False)))) % 165.28/165.50 Clause #201 (by superposition #[200, 68]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 a_7 : a), % 165.28/165.50 Or (Eq (cR a_1 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.28/165.50 (Or (Eq (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) True) (Or (Eq (f a_7 (skS.0 2 a_4)) False) (Eq False True)))) % 165.28/165.50 Clause #202 (by clausification #[201]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 a_7 : a), % 165.28/165.50 Or (Eq (cR a_1 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.28/165.50 (Or (Eq (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) True) (Eq (f a_7 (skS.0 2 a_4)) False))) % 165.28/165.50 Clause #203 (by superposition #[202, 7]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.28/165.50 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.28/165.50 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Or (Eq (f a_6 (skS.0 2 a_3)) False) (Eq False True))) % 165.28/165.50 Clause #204 (by clausification #[203]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.28/165.50 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.28/165.50 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Eq (f a_6 (skS.0 2 a_3)) False)) % 165.28/165.50 Clause #239 (by clausification #[105]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.28/165.50 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.28/165.50 (Or (Eq (cR a_3 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.28/165.50 (Eq (Or (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) (And (Not (f a_8 (skS.0 2 a_6))) (cR (skS.0 3 a_6 a_7) z))) True))) % 165.28/165.50 Clause #240 (by clausification #[239]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.28/165.50 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.28/165.50 (Or (Eq (cR a_3 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) True) % 165.28/165.50 (Eq (And (Not (f a_8 (skS.0 2 a_6))) (cR (skS.0 3 a_6 a_7) z)) True)))) % 165.28/165.50 Clause #241 (by clausification #[240]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 : a), % 165.28/165.50 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.28/165.50 (Or (Eq (cR a_3 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) True) (Eq (cR (skS.0 3 a_6 a_7) z) True)))) % 165.28/165.50 Clause #242 (by clausification #[240]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.28/165.50 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.28/165.50 (Or (Eq (cR a_3 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) True) (Eq (Not (f a_8 (skS.0 2 a_6))) True)))) % 165.28/165.50 Clause #243 (by superposition #[241, 68]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a), % 165.28/165.50 Or (Eq (cR a_1 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) True) (Or (Eq (cR (skS.0 3 a_4 a_5) z) True) (Eq False True)))) % 165.28/165.50 Clause #244 (by clausification #[243]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a), % 165.28/165.50 Or (Eq (cR a_1 z) False) % 165.28/165.50 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) True) (Eq (cR (skS.0 3 a_4 a_5) z) True))) % 165.28/165.50 Clause #245 (by superposition #[244, 7]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.28/165.50 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) (Eq False True))) % 165.28/165.50 Clause #246 (by clausification #[245]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.28/165.50 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (cR (skS.0 3 a_3 a_4) z) True)) % 165.28/165.50 Clause #253 (by superposition #[246, 150]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 : a), % 165.28/165.50 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.28/165.50 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.28/165.50 (Or (Eq True False) % 165.28/165.50 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.28/165.50 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (cR (skS.0 3 a_5 a_6) z) True))))) % 165.33/165.53 Clause #345 (by clausification #[123]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a) (a_5 a_6 : Iota) (a_7 a_8 : a), % 165.33/165.53 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (f (skS.0 1 a_4) a_5) False) % 165.33/165.53 (Or (Eq (f (skS.0 6 a_6 a_7 a_8) (skS.0 2 a_6)) True) (Eq (cR (skS.0 6 a_6 a_7 a_8) z) True)))) % 165.33/165.53 Clause #346 (by superposition #[345, 68]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.33/165.53 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_4 a_5 a_6) z) True) (Eq False True)))) % 165.33/165.53 Clause #347 (by clausification #[242]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.33/165.53 Or (Eq (f (skS.0 1 a_1) a_2) False) % 165.33/165.53 (Or (Eq (cR a_3 z) False) % 165.33/165.53 (Or (Eq (f (skS.0 4 a_3 a_4 a_5) (skS.0 0 a_4)) True) % 165.33/165.53 (Or (Eq (f (skS.0 3 a_6 a_7) (skS.0 2 a_6)) True) (Eq (f a_8 (skS.0 2 a_6)) False)))) % 165.33/165.53 Clause #348 (by superposition #[347, 68]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.33/165.53 Or (Eq (cR a_1 z) False) % 165.33/165.53 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.33/165.53 (Or (Eq (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) True) (Or (Eq (f a_6 (skS.0 2 a_4)) False) (Eq False True)))) % 165.33/165.53 Clause #349 (by clausification #[348]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.33/165.53 Or (Eq (cR a_1 z) False) % 165.33/165.53 (Or (Eq (f (skS.0 4 a_1 a_2 a_3) (skS.0 0 a_2)) True) % 165.33/165.53 (Or (Eq (f (skS.0 3 a_4 a_5) (skS.0 2 a_4)) True) (Eq (f a_6 (skS.0 2 a_4)) False))) % 165.33/165.53 Clause #350 (by superposition #[349, 7]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.33/165.53 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.33/165.53 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Or (Eq (f a_5 (skS.0 2 a_3)) False) (Eq False True))) % 165.33/165.53 Clause #351 (by clausification #[350]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.33/165.53 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.33/165.53 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (f a_5 (skS.0 2 a_3)) False)) % 165.33/165.53 Clause #476 (by clausification #[346]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.33/165.53 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (f (skS.0 6 a_4 a_5 a_6) (skS.0 2 a_4)) True) (Eq (cR (skS.0 6 a_4 a_5 a_6) z) True))) % 165.33/165.53 Clause #509 (by equality factoring #[476]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.33/165.53 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Or (Ne True True) (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True))) % 165.33/165.53 Clause #570 (by clausification #[509]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.33/165.53 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) (Or (Eq True False) (Eq True False)))) % 165.33/165.53 Clause #572 (by clausification #[570]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.33/165.53 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) (Eq True False))) % 165.33/165.53 Clause #573 (by clausification #[572]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.33/165.53 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True)) % 165.33/165.53 Clause #574 (by eliminate duplicate literals #[573]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.33/165.53 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) % 165.33/165.53 Clause #579 (by superposition #[574, 351]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.33/165.53 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True) % 165.33/165.53 (Or (Eq (f (skS.0 3 a_1 a_6) (skS.0 2 a_1)) True) (Eq True False))) % 165.33/165.53 Clause #587 (by superposition #[574, 24]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.33/165.53 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.33/165.53 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) a_4) True) (Or (Eq True False) (Eq (f a_4 (skS.0 2 a_1)) False))) % 165.37/165.56 Clause #593 (by clausification #[587]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.37/165.56 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.37/165.56 (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) a_4) True) (Eq (f a_4 (skS.0 2 a_1)) False)) % 165.37/165.56 Clause #666 (by clausification #[579]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 a_6 : a), % 165.37/165.56 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.37/165.56 (Or (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True) (Eq (f (skS.0 3 a_1 a_6) (skS.0 2 a_1)) True)) % 165.37/165.56 Clause #4596 (by clausification #[253]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 : a), % 165.37/165.56 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.37/165.56 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.37/165.56 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (cR (skS.0 3 a_5 a_6) z) True)))) % 165.37/165.56 Clause #4597 (by superposition #[4596, 68]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.56 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.37/165.56 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) (Eq False True)))) % 165.37/165.56 Clause #4598 (by clausification #[4597]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.56 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.37/165.56 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (cR (skS.0 3 a_3 a_4) z) True))) % 165.37/165.56 Clause #4685 (by equality factoring #[4598]): ∀ (a_1 : Iota) (a_2 : a), % 165.37/165.56 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Ne True True) (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True))) % 165.37/165.56 Clause #4686 (by clausification #[4685]): ∀ (a_1 : Iota) (a_2 : a), % 165.37/165.56 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Eq True False) (Eq True False)))) % 165.37/165.56 Clause #4688 (by clausification #[4686]): ∀ (a_1 : Iota) (a_2 : a), % 165.37/165.56 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq True False))) % 165.37/165.56 Clause #4689 (by clausification #[4688]): ∀ (a_1 : Iota) (a_2 : a), % 165.37/165.56 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True)) % 165.37/165.56 Clause #4690 (by eliminate duplicate literals #[4689]): ∀ (a_1 : Iota) (a_2 : a), Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.37/165.56 Clause #4691 (by superposition #[4690, 204]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.37/165.56 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (f (skS.0 4 z a_3 a_4) (skS.0 0 a_3)) True) % 165.37/165.56 (Or (Eq (f (skS.0 6 a_1 a_5 a_6) (skS.0 2 a_1)) True) (Eq True False))) % 165.37/165.56 Clause #5057 (by clausification #[4691]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.37/165.56 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.56 (Or (Eq (f (skS.0 4 z a_3 a_4) (skS.0 0 a_3)) True) (Eq (f (skS.0 6 a_1 a_5 a_6) (skS.0 2 a_1)) True)) % 165.37/165.56 Clause #5078 (by superposition #[5057, 14]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.37/165.56 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.56 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Or (Eq (cR z (skS.0 3 a_3 a_6)) True) (Eq True False))) % 165.37/165.56 Clause #5124 (by clausification #[5078]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.37/165.56 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.56 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Eq (cR z (skS.0 3 a_3 a_6)) True)) % 165.37/165.56 Clause #5166 (by superposition #[5124, 24]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.56 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.56 (Or (Eq (cR z (skS.0 3 a_3 a_4)) True) % 165.37/165.56 (Or (Eq (cR (skS.0 6 a_3 a_5 a_6) a_7) True) (Or (Eq True False) (Eq (f a_7 (skS.0 2 a_3)) False)))) % 165.37/165.56 Clause #5918 (by clausification #[5166]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.56 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.56 (Or (Eq (cR z (skS.0 3 a_3 a_4)) True) % 165.37/165.56 (Or (Eq (cR (skS.0 6 a_3 a_5 a_6) a_7) True) (Eq (f a_7 (skS.0 2 a_3)) False))) % 165.37/165.59 Clause #5932 (by superposition #[5918, 4690]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR z (skS.0 3 a_3 a_4)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 6 a_3 a_5 a_6) (skS.0 3 a_3 a_7)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_7) z) True) (Eq False True)))) % 165.37/165.59 Clause #9710 (by clausification #[5932]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR z (skS.0 3 a_3 a_4)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 6 a_3 a_5 a_6) (skS.0 3 a_3 a_7)) True) (Eq (cR (skS.0 3 a_3 a_7) z) True))) % 165.37/165.59 Clause #9782 (by superposition #[9710, 14]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 6 a_3 a_4 a_5) (skS.0 3 a_3 a_6)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_6) z) True) (Or (Eq (cR (skS.0 3 a_3 a_7) z) True) (Eq True False)))) % 165.37/165.59 Clause #9797 (by clausification #[9782]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 6 a_3 a_4 a_5) (skS.0 3 a_3 a_6)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_6) z) True) (Eq (cR (skS.0 3 a_3 a_7) z) True))) % 165.37/165.59 Clause #9869 (by superposition #[9797, 14]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_5) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_6 a_7)) True) (Eq True False)))) % 165.37/165.59 Clause #9896 (by clausification #[9869]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_5) z) True) (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_6 a_7)) True))) % 165.37/165.59 Clause #9979 (by superposition #[9896, 118]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a) (a_6 : Iota) (a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_5) z) True) (Or (Eq True False) (Eq (f (skS.0 4 z a_6 a_7) (skS.0 0 a_6)) True)))) % 165.37/165.59 Clause #10002 (by clausification #[9979]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a) (a_6 : Iota) (a_7 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_5) z) True) (Eq (f (skS.0 4 z a_6 a_7) (skS.0 0 a_6)) True))) % 165.37/165.59 Clause #10142 (by equality factoring #[10002]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.37/165.59 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_1 a_3) z) True) (Or (Ne True True) (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True))) % 165.37/165.59 Clause #10144 (by clausification #[10142]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.37/165.59 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_1 a_3) z) True) % 165.37/165.59 (Or (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True) (Or (Eq True False) (Eq True False)))) % 165.37/165.59 Clause #10146 (by clausification #[10144]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.37/165.59 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_1 a_3) z) True) (Or (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True) (Eq True False))) % 165.37/165.59 Clause #10147 (by clausification #[10146]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.37/165.59 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_1 a_3) z) True) (Eq (f (skS.0 4 z a_4 a_5) (skS.0 0 a_4)) True)) % 165.37/165.59 Clause #10230 (by equality factoring #[10147]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) (Or (Ne True True) (Eq (cR (skS.0 3 a_3 a_4) z) True)) % 165.37/165.59 Clause #10231 (by clausification #[10230]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.59 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.37/165.59 (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) (Or (Eq True False) (Eq True False))) % 165.37/165.59 Clause #10233 (by clausification #[10231]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.62 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) (Or (Eq (cR (skS.0 3 a_3 a_4) z) True) (Eq True False)) % 165.37/165.62 Clause #10234 (by clausification #[10233]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.62 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) (Eq (cR (skS.0 3 a_3 a_4) z) True) % 165.37/165.62 Clause #10238 (by superposition #[10234, 155]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.37/165.62 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.62 (Or (Eq True False) % 165.37/165.62 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.37/165.62 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (f a_7 (skS.0 2 a_5)) False)))) % 165.37/165.62 Clause #10316 (by superposition #[10234, 14]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.62 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) (Or (Eq (cR z (skS.0 3 a_3 a_4)) True) (Eq True False)) % 165.37/165.62 Clause #10317 (by clausification #[10316]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.37/165.62 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) (Eq (cR z (skS.0 3 a_3 a_4)) True) % 165.37/165.62 Clause #10318 (by superposition #[10317, 90]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.37/165.62 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.37/165.62 (Or (Eq True False) (Or (Eq (f (skS.0 1 a_3) a_4) False) (Eq (cR (skS.0 3 a_5 a_6) (skS.0 6 a_5 a_6 a_7)) False))) % 165.37/165.62 Clause #10319 (by superposition #[10317, 97]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 a_8 : a), % 165.37/165.62 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.37/165.62 (Or (Eq True False) % 165.37/165.62 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.37/165.62 (Or (Eq (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) True) (Eq (f a_8 (skS.0 2 a_5)) False)))) % 165.37/165.62 Clause #10726 (by clausification #[10318]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.37/165.62 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.37/165.62 (Or (Eq (f (skS.0 1 a_3) a_4) False) (Eq (cR (skS.0 3 a_5 a_6) (skS.0 6 a_5 a_6 a_7)) False)) % 165.37/165.62 Clause #10727 (by superposition #[10726, 68]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.37/165.62 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) (Or (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_4 a_5)) False) (Eq False True)) % 165.37/165.62 Clause #10728 (by clausification #[10727]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.37/165.62 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_4 a_5)) False) % 165.37/165.62 Clause #10856 (by clausification #[10238]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.37/165.62 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.62 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.37/165.62 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (f a_7 (skS.0 2 a_5)) False))) % 165.37/165.62 Clause #10857 (by superposition #[10856, 68]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.37/165.62 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.62 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Or (Eq (f a_5 (skS.0 2 a_3)) False) (Eq False True))) % 165.37/165.62 Clause #10858 (by clausification #[10857]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.37/165.62 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.62 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (f a_5 (skS.0 2 a_3)) False)) % 165.37/165.62 Clause #10870 (by superposition #[10858, 4690]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.37/165.62 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.62 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Or (Eq (cR (skS.0 3 a_3 a_5) z) True) (Eq False True))) % 165.37/165.62 Clause #10871 (by clausification #[10870]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.37/165.62 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.37/165.62 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (cR (skS.0 3 a_3 a_5) z) True)) % 165.37/165.62 Clause #10939 (by equality factoring #[10871]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.37/165.62 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Ne True True) (Eq (cR (skS.0 3 a_1 a_3) z) True)) % 165.37/165.62 Clause #10941 (by clausification #[10939]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.37/165.62 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.37/165.62 (Or (Eq (cR (skS.0 3 a_1 a_3) z) True) (Or (Eq True False) (Eq True False))) % 165.37/165.62 Clause #10943 (by clausification #[10941]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.37/165.62 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Eq (cR (skS.0 3 a_1 a_3) z) True) (Eq True False)) % 165.37/165.62 Clause #10944 (by clausification #[10943]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq (cR (skS.0 3 a_1 a_3) z) True) % 165.45/165.64 Clause #10985 (by superposition #[10944, 14]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.45/165.64 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Eq (cR z (skS.0 3 a_1 a_3)) True) (Eq True False)) % 165.45/165.64 Clause #10986 (by clausification #[10985]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq (cR z (skS.0 3 a_1 a_3)) True) % 165.45/165.64 Clause #11011 (by superposition #[10986, 24]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.45/165.64 (Or (Eq (cR (skS.0 3 a_1 a_3) a_4) True) (Or (Eq True False) (Eq (f a_4 (skS.0 2 a_1)) False))) % 165.45/165.64 Clause #11087 (by clausification #[11011]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) (Or (Eq (cR (skS.0 3 a_1 a_3) a_4) True) (Eq (f a_4 (skS.0 2 a_1)) False)) % 165.45/165.64 Clause #17317 (by clausification #[10319]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 a_8 : a), % 165.45/165.64 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.45/165.64 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.45/165.64 (Or (Eq (f (skS.0 6 a_5 a_6 a_7) (skS.0 2 a_5)) True) (Eq (f a_8 (skS.0 2 a_5)) False))) % 165.45/165.64 Clause #17318 (by superposition #[17317, 68]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.45/165.64 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.45/165.64 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Or (Eq (f a_6 (skS.0 2 a_3)) False) (Eq False True))) % 165.45/165.64 Clause #17320 (by clausification #[17318]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.45/165.64 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.45/165.64 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Eq (f a_6 (skS.0 2 a_3)) False)) % 165.45/165.64 Clause #17333 (by superposition #[17320, 10986]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.45/165.64 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.45/165.64 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Or (Eq False True) (Eq (cR z (skS.0 3 a_3 a_6)) True))) % 165.45/165.64 Clause #17346 (by clausification #[17333]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.45/165.64 Or (Eq (cR z (skS.0 3 a_1 a_2)) True) % 165.45/165.64 (Or (Eq (f (skS.0 6 a_3 a_4 a_5) (skS.0 2 a_3)) True) (Eq (cR z (skS.0 3 a_3 a_6)) True)) % 165.45/165.64 Clause #17427 (by equality factoring #[17346]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) (Or (Ne True True) (Eq (cR z (skS.0 3 a_1 a_4)) True)) % 165.45/165.64 Clause #17428 (by clausification #[17427]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) % 165.45/165.64 (Or (Eq (cR z (skS.0 3 a_1 a_4)) True) (Or (Eq True False) (Eq True False))) % 165.45/165.64 Clause #17430 (by clausification #[17428]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) (Or (Eq (cR z (skS.0 3 a_1 a_4)) True) (Eq True False)) % 165.45/165.64 Clause #17431 (by clausification #[17430]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) (Eq (cR z (skS.0 3 a_1 a_4)) True) % 165.45/165.64 Clause #17482 (by superposition #[17431, 14]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) (Or (Eq (cR (skS.0 3 a_1 a_4) z) True) (Eq True False)) % 165.45/165.64 Clause #17483 (by clausification #[17482]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.45/165.64 Or (Eq (f (skS.0 6 a_1 a_2 a_3) (skS.0 2 a_1)) True) (Eq (cR (skS.0 3 a_1 a_4) z) True) % 165.45/165.64 Clause #17498 (by superposition #[17483, 11087]): ∀ (a_1 : Iota) (a_2 a_3 a_4 a_5 a_6 : a), % 165.45/165.64 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.45/165.64 (Or (Eq (cR z (skS.0 3 a_1 a_3)) True) (Or (Eq (cR (skS.0 3 a_1 a_4) (skS.0 6 a_1 a_5 a_6)) True) (Eq True False))) % 165.45/165.64 Clause #18544 (by clausification #[17498]): ∀ (a_1 : Iota) (a_2 a_3 a_4 a_5 a_6 : a), % 165.45/165.64 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.45/165.64 (Or (Eq (cR z (skS.0 3 a_1 a_3)) True) (Eq (cR (skS.0 3 a_1 a_4) (skS.0 6 a_1 a_5 a_6)) True)) % 165.45/165.64 Clause #18613 (by superposition #[18544, 10728]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.45/165.64 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.45/165.64 (Or (Eq (cR z (skS.0 3 a_1 a_3)) True) (Or (Eq (cR z (skS.0 3 a_4 a_5)) True) (Eq True False))) % 165.45/165.64 Clause #18637 (by clausification #[18613]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 : Iota) (a_5 : a), % 165.45/165.67 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Eq (cR z (skS.0 3 a_1 a_3)) True) (Eq (cR z (skS.0 3 a_4 a_5)) True)) % 165.45/165.67 Clause #18725 (by equality factoring #[18637]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.45/165.67 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Ne True True) (Eq (cR z (skS.0 3 a_1 a_3)) True)) % 165.45/165.67 Clause #18727 (by clausification #[18725]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.45/165.67 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Eq (cR z (skS.0 3 a_1 a_3)) True) (Or (Eq True False) (Eq True False))) % 165.45/165.67 Clause #18729 (by clausification #[18727]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.45/165.67 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Eq (cR z (skS.0 3 a_1 a_3)) True) (Eq True False)) % 165.45/165.67 Clause #18730 (by clausification #[18729]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Eq (cR z (skS.0 3 a_1 a_3)) True) % 165.45/165.67 Clause #18792 (by superposition #[18730, 14]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.45/165.67 Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Eq (cR (skS.0 3 a_1 a_3) z) True) (Eq True False)) % 165.45/165.67 Clause #18793 (by clausification #[18792]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Eq (cR (skS.0 3 a_1 a_3) z) True) % 165.45/165.67 Clause #18829 (by equality factoring #[18793]): ∀ (a_1 : Iota) (a_2 : a), Or (Ne True True) (Eq (cR (skS.0 3 a_1 a_2) z) True) % 165.45/165.67 Clause #18830 (by clausification #[18829]): ∀ (a_1 : Iota) (a_2 : a), Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Or (Eq True False) (Eq True False)) % 165.45/165.67 Clause #18832 (by clausification #[18830]): ∀ (a_1 : Iota) (a_2 : a), Or (Eq (cR (skS.0 3 a_1 a_2) z) True) (Eq True False) % 165.45/165.67 Clause #18833 (by clausification #[18832]): ∀ (a_1 : Iota) (a_2 : a), Eq (cR (skS.0 3 a_1 a_2) z) True % 165.45/165.67 Clause #18867 (by superposition #[18833, 12]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR (skS.0 3 a_1 a_2) a_3) True) (Or (Eq True False) (Eq (cR a_3 z) False)) % 165.45/165.67 Clause #18868 (by superposition #[18833, 14]): ∀ (a_1 : Iota) (a_2 : a), Or (Eq (cR z (skS.0 3 a_1 a_2)) True) (Eq True False) % 165.45/165.67 Clause #18869 (by clausification #[18868]): ∀ (a_1 : Iota) (a_2 : a), Eq (cR z (skS.0 3 a_1 a_2)) True % 165.45/165.67 Clause #18887 (by superposition #[18869, 12]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a), Or (Eq (cR z a_1) True) (Or (Eq True False) (Eq (cR a_1 (skS.0 3 a_2 a_3)) False)) % 165.45/165.67 Clause #18889 (by clausification #[18867]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR (skS.0 3 a_1 a_2) a_3) True) (Eq (cR a_3 z) False) % 165.45/165.67 Clause #18890 (by superposition #[18889, 666]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.45/165.67 Or (Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_3 a_4 a_5)) True) % 165.45/165.67 (Or (Eq False True) % 165.45/165.67 (Or (Eq (f (skS.0 4 z a_6 a_7) (skS.0 0 a_6)) True) (Eq (f (skS.0 3 a_3 a_8) (skS.0 2 a_3)) True))) % 165.45/165.67 Clause #18909 (by clausification #[18887]): ∀ (a_1 : a) (a_2 : Iota) (a_3 : a), Or (Eq (cR z a_1) True) (Eq (cR a_1 (skS.0 3 a_2 a_3)) False) % 165.45/165.67 Clause #23634 (by clausification #[18890]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a) (a_6 : Iota) (a_7 a_8 : a), % 165.45/165.67 Or (Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_3 a_4 a_5)) True) % 165.45/165.67 (Or (Eq (f (skS.0 4 z a_6 a_7) (skS.0 0 a_6)) True) (Eq (f (skS.0 3 a_3 a_8) (skS.0 2 a_3)) True)) % 165.45/165.67 Clause #23635 (by superposition #[23634, 118]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a) (a_5 : Iota) (a_6 : a), % 165.45/165.67 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.45/165.67 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) % 165.45/165.67 (Or (Eq True False) (Eq (f (skS.0 4 z a_5 a_6) (skS.0 0 a_5)) True))) % 165.45/165.67 Clause #23714 (by clausification #[23635]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a) (a_5 : Iota) (a_6 : a), % 165.45/165.67 Or (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.45/165.67 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (f (skS.0 4 z a_5 a_6) (skS.0 0 a_5)) True)) % 165.45/165.67 Clause #23807 (by equality factoring #[23714]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.45/165.67 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Ne True True) (Eq (f (skS.0 4 z a_3 a_4) (skS.0 0 a_3)) True)) % 165.45/165.67 Clause #23808 (by clausification #[23807]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.45/165.67 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.45/165.67 (Or (Eq (f (skS.0 4 z a_3 a_4) (skS.0 0 a_3)) True) (Or (Eq True False) (Eq True False))) % 165.50/165.70 Clause #23810 (by clausification #[23808]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Eq (f (skS.0 4 z a_3 a_4) (skS.0 0 a_3)) True) (Eq True False)) % 165.50/165.70 Clause #23811 (by clausification #[23810]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq (f (skS.0 4 z a_3 a_4) (skS.0 0 a_3)) True) % 165.50/165.70 Clause #23837 (by superposition #[23811, 90]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq True False) (Or (Eq (f (skS.0 1 a_3) a_4) False) (Eq (cR (skS.0 3 a_5 a_6) (skS.0 6 a_5 a_6 a_7)) False))) % 165.50/165.70 Clause #23840 (by superposition #[23811, 155]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq True False) % 165.50/165.70 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.50/165.70 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (f a_7 (skS.0 2 a_5)) False)))) % 165.50/165.70 Clause #24272 (by clausification #[23837]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (f (skS.0 1 a_3) a_4) False) (Eq (cR (skS.0 3 a_5 a_6) (skS.0 6 a_5 a_6 a_7)) False)) % 165.50/165.70 Clause #24273 (by superposition #[24272, 68]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_4 a_5)) False) (Eq False True)) % 165.50/165.70 Clause #24274 (by clausification #[24273]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_4 a_5)) False) % 165.50/165.70 Clause #25078 (by clausification #[23840]): ∀ (a_1 : Iota) (a_2 a_3 : a) (a_4 a_5 : Iota) (a_6 a_7 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (f (skS.0 1 a_3) a_4) False) % 165.50/165.70 (Or (Eq (f (skS.0 3 a_5 a_6) (skS.0 2 a_5)) True) (Eq (f a_7 (skS.0 2 a_5)) False))) % 165.50/165.70 Clause #25079 (by superposition #[25078, 68]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Or (Eq (f a_5 (skS.0 2 a_3)) False) (Eq False True))) % 165.50/165.70 Clause #25080 (by clausification #[25079]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (f a_5 (skS.0 2 a_3)) False)) % 165.50/165.70 Clause #25081 (by superposition #[25080, 574]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Or (Eq (cR (skS.0 6 a_3 a_5 a_6) z) True) (Eq False True))) % 165.50/165.70 Clause #25107 (by clausification #[25081]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq (cR (skS.0 6 a_3 a_5 a_6) z) True)) % 165.50/165.70 Clause #25158 (by equality factoring #[25107]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.50/165.70 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Or (Ne True True) (Eq (f (skS.0 3 a_1 a_4) (skS.0 2 a_1)) True)) % 165.50/165.70 Clause #25159 (by clausification #[25158]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.50/165.70 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) % 165.50/165.70 (Or (Eq (f (skS.0 3 a_1 a_4) (skS.0 2 a_1)) True) (Or (Eq True False) (Eq True False))) % 165.50/165.70 Clause #25161 (by clausification #[25159]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.50/165.70 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Or (Eq (f (skS.0 3 a_1 a_4) (skS.0 2 a_1)) True) (Eq True False)) % 165.50/165.70 Clause #25162 (by clausification #[25161]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.50/165.70 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Eq (f (skS.0 3 a_1 a_4) (skS.0 2 a_1)) True) % 165.50/165.70 Clause #25170 (by superposition #[25162, 18889]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.50/165.70 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.50/165.70 (Or (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_1 a_5 a_6)) True) (Eq True False)) % 165.75/165.99 Clause #25340 (by clausification #[25170]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 a_6 : a), % 165.75/165.99 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_1 a_5 a_6)) True) % 165.75/165.99 Clause #25369 (by superposition #[25340, 24274]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.75/165.99 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) (Eq True False)) % 165.75/165.99 Clause #25380 (by clausification #[25369]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 : a), % 165.75/165.99 Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq (f (skS.0 3 a_3 a_4) (skS.0 2 a_3)) True) % 165.75/165.99 Clause #25404 (by equality factoring #[25380]): ∀ (a_1 : Iota) (a_2 : a), Or (Ne True True) (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) % 165.75/165.99 Clause #25452 (by clausification #[25404]): ∀ (a_1 : Iota) (a_2 : a), Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Or (Eq True False) (Eq True False)) % 165.75/165.99 Clause #25454 (by clausification #[25452]): ∀ (a_1 : Iota) (a_2 : a), Or (Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True) (Eq True False) % 165.75/165.99 Clause #25455 (by clausification #[25454]): ∀ (a_1 : Iota) (a_2 : a), Eq (f (skS.0 3 a_1 a_2) (skS.0 2 a_1)) True % 165.75/165.99 Clause #25457 (by superposition #[25455, 593]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.75/165.99 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Or (Eq (cR (skS.0 6 a_1 a_2 a_3) (skS.0 3 a_1 a_4)) True) (Eq True False)) % 165.75/165.99 Clause #25632 (by clausification #[25457]): ∀ (a_1 : Iota) (a_2 a_3 a_4 : a), % 165.75/165.99 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Eq (cR (skS.0 6 a_1 a_2 a_3) (skS.0 3 a_1 a_4)) True) % 165.75/165.99 Clause #25634 (by superposition #[25632, 18909]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.75/165.99 Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Or (Eq (cR z (skS.0 6 a_1 a_2 a_3)) True) (Eq True False)) % 165.75/165.99 Clause #25638 (by clausification #[25634]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Eq (cR z (skS.0 6 a_1 a_2 a_3)) True) % 165.75/165.99 Clause #25647 (by superposition #[25638, 14]): ∀ (a_1 : Iota) (a_2 a_3 : a), % 165.75/165.99 Or (Eq (cR z (skS.0 6 a_1 a_2 a_3)) True) (Or (Eq (cR z (skS.0 6 a_1 a_2 a_3)) True) (Eq True False)) % 165.75/165.99 Clause #25648 (by clausification #[25647]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR z (skS.0 6 a_1 a_2 a_3)) True) (Eq (cR z (skS.0 6 a_1 a_2 a_3)) True) % 165.75/165.99 Clause #25649 (by eliminate duplicate literals #[25648]): ∀ (a_1 : Iota) (a_2 a_3 : a), Eq (cR z (skS.0 6 a_1 a_2 a_3)) True % 165.75/165.99 Clause #25656 (by superposition #[25649, 14]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR (skS.0 6 a_1 a_2 a_3) z) True) (Eq True False) % 165.75/165.99 Clause #25657 (by clausification #[25656]): ∀ (a_1 : Iota) (a_2 a_3 : a), Eq (cR (skS.0 6 a_1 a_2 a_3) z) True % 165.75/165.99 Clause #25671 (by superposition #[25657, 18889]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), % 165.75/165.99 Or (Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_3 a_4 a_5)) True) (Eq True False) % 165.75/165.99 Clause #25684 (by clausification #[25671]): ∀ (a_1 : Iota) (a_2 : a) (a_3 : Iota) (a_4 a_5 : a), Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_3 a_4 a_5)) True % 165.75/165.99 Clause #25685 (by superposition #[25684, 118]): ∀ (a_1 : Iota) (a_2 : a), Or (Eq True False) (Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True) % 165.75/165.99 Clause #25689 (by clausification #[25685]): ∀ (a_1 : Iota) (a_2 : a), Eq (f (skS.0 4 z a_1 a_2) (skS.0 0 a_1)) True % 165.75/165.99 Clause #25690 (by superposition #[25689, 90]): ∀ (a_1 : a) (a_2 a_3 : Iota) (a_4 a_5 : a), % 165.75/165.99 Or (Eq True False) (Or (Eq (f (skS.0 1 a_1) a_2) False) (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_4 a_5)) False)) % 165.75/165.99 Clause #25732 (by clausification #[25690]): ∀ (a_1 : a) (a_2 a_3 : Iota) (a_4 a_5 : a), % 165.75/165.99 Or (Eq (f (skS.0 1 a_1) a_2) False) (Eq (cR (skS.0 3 a_3 a_4) (skS.0 6 a_3 a_4 a_5)) False) % 165.75/165.99 Clause #25733 (by superposition #[25732, 68]): ∀ (a_1 : Iota) (a_2 a_3 : a), Or (Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_1 a_2 a_3)) False) (Eq False True) % 165.75/165.99 Clause #25734 (by clausification #[25733]): ∀ (a_1 : Iota) (a_2 a_3 : a), Eq (cR (skS.0 3 a_1 a_2) (skS.0 6 a_1 a_2 a_3)) False % 165.75/165.99 Clause #25735 (by superposition #[25734, 25684]): Eq False True % 165.75/165.99 Clause #25736 (by clausification #[25735]): False % 165.75/165.99 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------