%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:36:23 AM UTC 2026 % Result : Theorem 15.06s 15.34s % Output : Proof 16.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : duper %s % 0.09/0.35 % Computer : n013.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 5 02:05:35 UTC 2026 % 0.09/0.35 % CPUTime : % 15.06/15.34 SZS status Theorem for theBenchmark.p % 15.06/15.34 SZS output start Proof for theBenchmark.p % 15.06/15.34 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), r1 X X) True % 15.06/15.34 Clause #1 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (r1 X Y) (r1 Y Z) → r1 X Z) True % 15.06/15.34 Clause #2 (by assumption #[]): Eq % 15.06/15.34 (Not % 15.06/15.34 (Not % 15.06/15.34 (Exists fun X => % 15.06/15.34 Not % 15.06/15.34 (Or (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 15.06/15.34 (Not % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (∀ (Y : Iota), % 15.06/15.34 Or (Not (r1 X Y)) % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (And % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.06/15.34 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.06/15.34 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.06/15.34 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.06/15.34 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.06/15.34 (Not % 15.06/15.34 (∀ (X : Iota), % 15.06/15.34 Or (Not (r1 Y X)) % 15.06/15.34 (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.06/15.34 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) % 15.06/15.34 (p6 Y)) % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) % 15.06/15.34 (Not (p6 Y)))) % 15.06/15.34 (Not (p105 Y)))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) % 15.06/15.34 (p5 Y)) % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) % 15.06/15.34 (Not (p5 Y)))) % 15.06/15.34 (Not (p104 Y)))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) % 15.06/15.34 (p4 Y)) % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) % 15.06/15.34 (Not (p4 Y)))) % 15.06/15.34 (Not (p103 Y)))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) % 15.06/15.34 (p3 Y)) % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) % 15.06/15.34 (Not (p3 Y)))) % 15.06/15.34 (Not (p102 Y)))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) % 15.06/15.34 (Not (p2 Y)))) % 15.06/15.34 (Not (p101 Y)))) % 15.06/15.34 (Or % 15.06/15.34 (And % 15.06/15.34 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.16/15.41 (Not (p100 Y)))) % 15.16/15.41 (Or (p105 Y) (Not (p106 Y)))) % 15.16/15.41 (Or (p104 Y) (Not (p105 Y)))) % 15.16/15.41 (Or (p103 Y) (Not (p104 Y)))) % 15.16/15.41 (Or (p102 Y) (Not (p103 Y)))) % 15.16/15.41 (Or (p101 Y) (Not (p102 Y)))) % 15.16/15.41 (Or (p100 Y) (Not (p101 Y))))) % 15.16/15.41 (Not (p101 X))) % 15.16/15.41 (p100 X))))))) % 15.16/15.41 True % 15.16/15.41 Clause #3 (by clausification #[0]): ∀ (a : Iota), Eq (r1 a a) True % 15.16/15.41 Clause #4 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (r1 a Y) (r1 Y Z) → r1 a Z) True % 15.16/15.41 Clause #5 (by clausification #[4]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (r1 a a_1) (r1 a_1 Z) → r1 a Z) True % 15.16/15.41 Clause #6 (by clausification #[5]): ∀ (a a_1 a_2 : Iota), Eq (And (r1 a a_1) (r1 a_1 a_2) → r1 a a_2) True % 15.16/15.41 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (r1 a a_1) (r1 a_1 a_2)) False) (Eq (r1 a a_2) True) % 15.16/15.41 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 a a_1) True) (Or (Eq (r1 a a_2) False) (Eq (r1 a_2 a_1) False)) % 15.16/15.41 Clause #11 (by clausification #[2]): Eq % 15.16/15.41 (Not % 15.16/15.41 (Exists fun X => % 15.16/15.41 Not % 15.16/15.41 (Or (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 15.16/15.41 (Not % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (∀ (Y : Iota), % 15.16/15.41 Or (Not (r1 X Y)) % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (And % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.16/15.41 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.16/15.41 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.16/15.41 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.16/15.41 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.16/15.41 (Not % 15.16/15.41 (∀ (X : Iota), % 15.16/15.41 Or (Not (r1 Y X)) % 15.16/15.41 (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.16/15.41 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) % 15.16/15.41 (p6 Y)) % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) % 15.16/15.41 (Not (p6 Y)))) % 15.16/15.41 (Not (p105 Y)))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) % 15.16/15.41 (p5 Y)) % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) % 15.16/15.41 (Not (p5 Y)))) % 15.16/15.41 (Not (p104 Y)))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) % 15.16/15.41 (p4 Y)) % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) % 15.16/15.41 (Not (p4 Y)))) % 15.16/15.41 (Not (p103 Y)))) % 15.16/15.41 (Or % 15.16/15.41 (And % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.16/15.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) % 15.16/15.48 (Not (p3 Y)))) % 15.16/15.48 (Not (p102 Y)))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.16/15.48 (Not (p101 Y)))) % 15.16/15.48 (Or % 15.16/15.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.16/15.48 (Not (p100 Y)))) % 15.16/15.48 (Or (p105 Y) (Not (p106 Y)))) % 15.16/15.48 (Or (p104 Y) (Not (p105 Y)))) % 15.16/15.48 (Or (p103 Y) (Not (p104 Y)))) % 15.16/15.48 (Or (p102 Y) (Not (p103 Y)))) % 15.16/15.48 (Or (p101 Y) (Not (p102 Y)))) % 15.16/15.48 (Or (p100 Y) (Not (p101 Y))))) % 15.16/15.48 (Not (p101 X))) % 15.16/15.48 (p100 X)))))) % 15.16/15.48 False % 15.16/15.48 Clause #12 (by clausification #[11]): Eq % 15.16/15.48 (Exists fun X => % 15.16/15.48 Not % 15.16/15.48 (Or (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 15.16/15.48 (Not % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (∀ (Y : Iota), % 15.16/15.48 Or (Not (r1 X Y)) % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (And % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.16/15.48 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.16/15.48 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.16/15.48 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.16/15.48 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.16/15.48 (Not % 15.16/15.48 (∀ (X : Iota), % 15.16/15.48 Or (Not (r1 Y X)) % 15.16/15.48 (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.16/15.48 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) % 15.16/15.48 (p6 Y)) % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) % 15.16/15.48 (Not (p6 Y)))) % 15.16/15.48 (Not (p105 Y)))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) % 15.16/15.48 (p5 Y)) % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) % 15.16/15.48 (Not (p5 Y)))) % 15.16/15.48 (Not (p104 Y)))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) (p4 Y)) % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) % 15.16/15.48 (Not (p4 Y)))) % 15.16/15.48 (Not (p103 Y)))) % 15.16/15.48 (Or % 15.16/15.48 (And % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.16/15.48 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) (Not (p3 Y)))) % 15.16/15.48 (Not (p102 Y)))) % 15.16/15.48 (Or % 15.16/15.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.26/15.54 (Not (p101 Y)))) % 15.26/15.54 (Or % 15.26/15.54 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.26/15.54 (Not (p100 Y)))) % 15.26/15.54 (Or (p105 Y) (Not (p106 Y)))) % 15.26/15.54 (Or (p104 Y) (Not (p105 Y)))) % 15.26/15.54 (Or (p103 Y) (Not (p104 Y)))) % 15.26/15.54 (Or (p102 Y) (Not (p103 Y)))) % 15.26/15.54 (Or (p101 Y) (Not (p102 Y)))) % 15.26/15.54 (Or (p100 Y) (Not (p101 Y))))) % 15.26/15.54 (Not (p101 X))) % 15.26/15.54 (p100 X))))) % 15.26/15.54 True % 15.26/15.54 Clause #13 (by clausification #[12]): ∀ (a : Iota), % 15.26/15.54 Eq % 15.26/15.54 (Not % 15.26/15.54 (Or (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p3 Y))) % 15.26/15.54 (Not % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (∀ (Y : Iota), % 15.26/15.54 Or (Not (r1 (skS.0 0 a) Y)) % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (And % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.26/15.54 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.26/15.54 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.26/15.54 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.26/15.54 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.26/15.54 (Not % 15.26/15.54 (∀ (X : Iota), % 15.26/15.54 Or (Not (r1 Y X)) % 15.26/15.54 (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.26/15.54 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) % 15.26/15.54 (p6 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) % 15.26/15.54 (Not (p6 Y)))) % 15.26/15.54 (Not (p105 Y)))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) % 15.26/15.54 (p5 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) % 15.26/15.54 (Not (p5 Y)))) % 15.26/15.54 (Not (p104 Y)))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) (p4 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) % 15.26/15.54 (Not (p4 Y)))) % 15.26/15.54 (Not (p103 Y)))) % 15.26/15.54 (Or % 15.26/15.54 (And % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) (Not (p3 Y)))) % 15.26/15.54 (Not (p102 Y)))) % 15.26/15.54 (Or % 15.26/15.54 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.26/15.54 (Not (p101 Y)))) % 15.26/15.54 (Or % 15.26/15.54 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.26/15.54 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.36/15.61 (Not (p100 Y)))) % 15.36/15.61 (Or (p105 Y) (Not (p106 Y)))) % 15.36/15.61 (Or (p104 Y) (Not (p105 Y)))) % 15.36/15.61 (Or (p103 Y) (Not (p104 Y)))) % 15.36/15.61 (Or (p102 Y) (Not (p103 Y)))) % 15.36/15.61 (Or (p101 Y) (Not (p102 Y)))) % 15.36/15.61 (Or (p100 Y) (Not (p101 Y))))) % 15.36/15.61 (Not (p101 (skS.0 0 a)))) % 15.36/15.61 (p100 (skS.0 0 a)))))) % 15.36/15.61 True % 15.36/15.61 Clause #14 (by clausification #[13]): ∀ (a : Iota), % 15.36/15.61 Eq % 15.36/15.61 (Or (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p3 Y))) % 15.36/15.61 (Not % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (∀ (Y : Iota), % 15.36/15.61 Or (Not (r1 (skS.0 0 a) Y)) % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (And % 15.36/15.61 (Or % 15.36/15.61 (And % 15.36/15.61 (Not % 15.36/15.61 (∀ (X : Iota), % 15.36/15.61 Or (Not (r1 Y X)) % 15.36/15.61 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.36/15.61 (Not % 15.36/15.61 (∀ (X : Iota), % 15.36/15.61 Or (Not (r1 Y X)) % 15.36/15.61 (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.36/15.61 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.36/15.61 (Or % 15.36/15.61 (And % 15.36/15.61 (Not % 15.36/15.61 (∀ (X : Iota), % 15.36/15.61 Or (Not (r1 Y X)) % 15.36/15.61 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.36/15.61 (Not % 15.36/15.61 (∀ (X : Iota), % 15.36/15.61 Or (Not (r1 Y X)) % 15.36/15.61 (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.36/15.61 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.36/15.61 (Or % 15.36/15.61 (And % 15.36/15.61 (Not % 15.36/15.61 (∀ (X : Iota), % 15.36/15.61 Or (Not (r1 Y X)) % 15.36/15.61 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.36/15.61 (Not % 15.36/15.61 (∀ (X : Iota), % 15.36/15.61 Or (Not (r1 Y X)) % 15.36/15.61 (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.36/15.61 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.36/15.61 (Or % 15.36/15.61 (And % 15.36/15.61 (Not % 15.36/15.61 (∀ (X : Iota), % 15.36/15.61 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.36/15.67 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.36/15.67 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) % 15.36/15.67 (p6 Y)) % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) % 15.36/15.67 (Not (p6 Y)))) % 15.36/15.67 (Not (p105 Y)))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) (p5 Y)) % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) % 15.36/15.67 (Not (p5 Y)))) % 15.36/15.67 (Not (p104 Y)))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) (p4 Y)) % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) (Not (p4 Y)))) % 15.36/15.67 (Not (p103 Y)))) % 15.36/15.67 (Or % 15.36/15.67 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) (Not (p3 Y)))) % 15.36/15.67 (Not (p102 Y)))) % 15.36/15.67 (Or % 15.36/15.67 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.36/15.67 (Not (p101 Y)))) % 15.36/15.67 (Or % 15.36/15.67 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.36/15.67 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.36/15.67 (Not (p100 Y)))) % 15.36/15.67 (Or (p105 Y) (Not (p106 Y)))) % 15.36/15.67 (Or (p104 Y) (Not (p105 Y)))) % 15.36/15.67 (Or (p103 Y) (Not (p104 Y)))) % 15.36/15.67 (Or (p102 Y) (Not (p103 Y)))) % 15.36/15.67 (Or (p101 Y) (Not (p102 Y)))) % 15.36/15.67 (Or (p100 Y) (Not (p101 Y))))) % 15.36/15.67 (Not (p101 (skS.0 0 a)))) % 15.36/15.67 (p100 (skS.0 0 a))))) % 15.36/15.67 False % 15.36/15.67 Clause #15 (by clausification #[14]): ∀ (a : Iota), % 15.36/15.67 Eq % 15.36/15.67 (Not % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (∀ (Y : Iota), % 15.36/15.67 Or (Not (r1 (skS.0 0 a) Y)) % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (And % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.36/15.67 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.36/15.67 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.36/15.67 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.36/15.67 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.36/15.67 (Or % 15.36/15.67 (And % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) % 15.36/15.67 (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.36/15.67 (Not % 15.36/15.67 (∀ (X : Iota), % 15.36/15.67 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.46/15.74 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) (p6 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) % 15.46/15.74 (Not (p6 Y)))) % 15.46/15.74 (Not (p105 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) (p5 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) (Not (p5 Y)))) % 15.46/15.74 (Not (p104 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) (p4 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) (Not (p4 Y)))) % 15.46/15.74 (Not (p103 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) (Not (p3 Y)))) % 15.46/15.74 (Not (p102 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.46/15.74 (Not (p101 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.46/15.74 (Not (p100 Y)))) % 15.46/15.74 (Or (p105 Y) (Not (p106 Y)))) % 15.46/15.74 (Or (p104 Y) (Not (p105 Y)))) % 15.46/15.74 (Or (p103 Y) (Not (p104 Y)))) % 15.46/15.74 (Or (p102 Y) (Not (p103 Y)))) % 15.46/15.74 (Or (p101 Y) (Not (p102 Y)))) % 15.46/15.74 (Or (p100 Y) (Not (p101 Y))))) % 15.46/15.74 (Not (p101 (skS.0 0 a)))) % 15.46/15.74 (p100 (skS.0 0 a)))) % 15.46/15.74 False % 15.46/15.74 Clause #16 (by clausification #[14]): ∀ (a : Iota), Eq (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p3 Y))) False % 15.46/15.74 Clause #17 (by clausification #[15]): ∀ (a : Iota), % 15.46/15.74 Eq % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (∀ (Y : Iota), % 15.46/15.74 Or (Not (r1 (skS.0 0 a) Y)) % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (And % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) % 15.46/15.74 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) % 15.46/15.74 (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.46/15.74 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) % 15.46/15.74 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) % 15.46/15.74 (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.46/15.74 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) % 15.46/15.74 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.46/15.74 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) % 15.46/15.74 (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.46/15.74 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.46/15.74 (Not % 15.46/15.74 (∀ (X : Iota), % 15.46/15.74 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.46/15.74 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.46/15.74 (Or % 15.46/15.74 (And % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) (p6 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) (Not (p6 Y)))) % 15.46/15.74 (Not (p105 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) (p5 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) (Not (p5 Y)))) % 15.46/15.74 (Not (p104 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) (p4 Y)) % 15.46/15.74 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) (Not (p4 Y)))) % 15.46/15.74 (Not (p103 Y)))) % 15.46/15.74 (Or % 15.46/15.74 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.56/15.80 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) (Not (p3 Y)))) % 15.56/15.80 (Not (p102 Y)))) % 15.56/15.80 (Or % 15.56/15.80 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.56/15.80 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.56/15.80 (Not (p101 Y)))) % 15.56/15.80 (Or % 15.56/15.80 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.56/15.80 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.56/15.80 (Not (p100 Y)))) % 15.56/15.80 (Or (p105 Y) (Not (p106 Y)))) % 15.56/15.80 (Or (p104 Y) (Not (p105 Y)))) % 15.56/15.80 (Or (p103 Y) (Not (p104 Y)))) % 15.56/15.80 (Or (p102 Y) (Not (p103 Y)))) % 15.56/15.80 (Or (p101 Y) (Not (p102 Y)))) % 15.56/15.80 (Or (p100 Y) (Not (p101 Y))))) % 15.56/15.80 (Not (p101 (skS.0 0 a)))) % 15.56/15.80 (p100 (skS.0 0 a))) % 15.56/15.80 True % 15.56/15.80 Clause #18 (by clausification #[17]): ∀ (a : Iota), Eq (p100 (skS.0 0 a)) True % 15.56/15.80 Clause #19 (by clausification #[17]): ∀ (a : Iota), % 15.56/15.80 Eq % 15.56/15.80 (And % 15.56/15.80 (∀ (Y : Iota), % 15.56/15.80 Or (Not (r1 (skS.0 0 a) Y)) % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (And % 15.56/15.80 (Or % 15.56/15.80 (And % 15.56/15.80 (Not % 15.56/15.80 (∀ (X : Iota), % 15.56/15.80 Or (Not (r1 Y X)) % 15.56/15.80 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.56/15.80 (Not % 15.56/15.80 (∀ (X : Iota), % 15.56/15.80 Or (Not (r1 Y X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.56/15.80 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.56/15.80 (Or % 15.56/15.80 (And % 15.56/15.80 (Not % 15.56/15.80 (∀ (X : Iota), % 15.56/15.80 Or (Not (r1 Y X)) % 15.56/15.80 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.56/15.80 (Not % 15.56/15.80 (∀ (X : Iota), % 15.56/15.80 Or (Not (r1 Y X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.56/15.80 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.56/15.80 (Or % 15.56/15.80 (And % 15.56/15.80 (Not % 15.56/15.80 (∀ (X : Iota), % 15.56/15.80 Or (Not (r1 Y X)) % 15.56/15.80 (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.56/15.80 (Not % 15.56/15.80 (∀ (X : Iota), % 15.56/15.80 Or (Not (r1 Y X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.56/15.80 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.56/15.80 (Or % 15.56/15.80 (And % 15.56/15.80 (Not % 15.56/15.80 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.56/15.87 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.56/15.87 (Or % 15.56/15.87 (And % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.56/15.87 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) (p6 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) (Not (p6 Y)))) % 15.56/15.87 (Not (p105 Y)))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) (p5 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) (Not (p5 Y)))) % 15.56/15.87 (Not (p104 Y)))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) (p4 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) (Not (p4 Y)))) % 15.56/15.87 (Not (p103 Y)))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) (Not (p3 Y)))) % 15.56/15.87 (Not (p102 Y)))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.56/15.87 (Not (p101 Y)))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.56/15.87 (Not (p100 Y)))) % 15.56/15.87 (Or (p105 Y) (Not (p106 Y)))) % 15.56/15.87 (Or (p104 Y) (Not (p105 Y)))) % 15.56/15.87 (Or (p103 Y) (Not (p104 Y)))) % 15.56/15.87 (Or (p102 Y) (Not (p103 Y)))) % 15.56/15.87 (Or (p101 Y) (Not (p102 Y)))) % 15.56/15.87 (Or (p100 Y) (Not (p101 Y))))) % 15.56/15.87 (Not (p101 (skS.0 0 a)))) % 15.56/15.87 True % 15.56/15.87 Clause #20 (by clausification #[16]): ∀ (a : Iota), Eq (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p3 Y)) True % 15.56/15.87 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), Eq (Or (Not (r1 (skS.0 0 a) a_1)) (p3 a_1)) True % 15.56/15.87 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) (Eq (p3 a_1) True) % 15.56/15.87 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Or (Eq (p3 a) True) (Eq (r1 (skS.0 0 a_1) a) False) % 15.56/15.87 Clause #25 (by clausification #[19]): ∀ (a : Iota), Eq (Not (p101 (skS.0 0 a))) True % 15.56/15.87 Clause #26 (by clausification #[19]): ∀ (a : Iota), % 15.56/15.87 Eq % 15.56/15.87 (∀ (Y : Iota), % 15.56/15.87 Or (Not (r1 (skS.0 0 a) Y)) % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (And % 15.56/15.87 (Or % 15.56/15.87 (And % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) % 15.56/15.87 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.56/15.87 (Not (And (Not (p105 Y)) (p104 Y)))) % 15.56/15.87 (Or % 15.56/15.87 (And % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) % 15.56/15.87 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.56/15.87 (Not (And (Not (p104 Y)) (p103 Y))))) % 15.56/15.87 (Or % 15.56/15.87 (And % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.56/15.87 (Not (And (Not (p103 Y)) (p102 Y))))) % 15.56/15.87 (Or % 15.56/15.87 (And % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.56/15.87 (Not (And (Not (p102 Y)) (p101 Y))))) % 15.56/15.87 (Or % 15.56/15.87 (And % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.56/15.87 (Not % 15.56/15.87 (∀ (X : Iota), % 15.56/15.87 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.56/15.87 (Not (And (Not (p101 Y)) (p100 Y))))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p6 X))) (Not (p105 X))) (p6 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p6 X)) (Not (p105 X))) (Not (p6 Y)))) % 15.56/15.87 (Not (p105 Y)))) % 15.56/15.87 (Or % 15.56/15.87 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p5 X))) (Not (p104 X))) (p5 Y)) % 15.56/15.87 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p5 X)) (Not (p104 X))) (Not (p5 Y)))) % 15.56/15.87 (Not (p104 Y)))) % 15.56/15.87 (Or % 15.66/15.93 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p4 X))) (Not (p103 X))) (p4 Y)) % 15.66/15.93 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p4 X)) (Not (p103 X))) (Not (p4 Y)))) % 15.66/15.93 (Not (p103 Y)))) % 15.66/15.93 (Or % 15.66/15.93 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p3 X))) (Not (p102 X))) (p3 Y)) % 15.66/15.93 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p3 X)) (Not (p102 X))) (Not (p3 Y)))) % 15.66/15.93 (Not (p102 Y)))) % 15.66/15.93 (Or % 15.66/15.93 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 15.66/15.93 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 15.66/15.93 (Not (p101 Y)))) % 15.66/15.93 (Or % 15.66/15.93 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 15.66/15.93 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 15.66/15.93 (Not (p100 Y)))) % 15.66/15.93 (Or (p105 Y) (Not (p106 Y)))) % 15.66/15.93 (Or (p104 Y) (Not (p105 Y)))) % 15.66/15.93 (Or (p103 Y) (Not (p104 Y)))) % 15.66/15.93 (Or (p102 Y) (Not (p103 Y)))) % 15.66/15.93 (Or (p101 Y) (Not (p102 Y)))) % 15.66/15.93 (Or (p100 Y) (Not (p101 Y))))) % 15.66/15.93 True % 15.66/15.93 Clause #27 (by clausification #[25]): ∀ (a : Iota), Eq (p101 (skS.0 0 a)) False % 15.66/15.93 Clause #29 (by clausification #[26]): ∀ (a a_1 : Iota), % 15.66/15.93 Eq % 15.66/15.93 (Or (Not (r1 (skS.0 0 a) a_1)) % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (And % 15.66/15.93 (Or % 15.66/15.93 (And % 15.66/15.93 (Not % 15.66/15.93 (∀ (X : Iota), % 15.66/15.93 Or (Not (r1 a_1 X)) % 15.66/15.93 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.66/15.93 (Not % 15.66/15.93 (∀ (X : Iota), % 15.66/15.93 Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.66/15.93 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 15.66/15.93 (Or % 15.66/15.93 (And % 15.66/15.93 (Not % 15.66/15.93 (∀ (X : Iota), % 15.66/15.93 Or (Not (r1 a_1 X)) % 15.66/15.93 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.66/15.93 (Not % 15.66/15.93 (∀ (X : Iota), % 15.66/15.93 Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.66/15.93 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 15.66/15.93 (Or % 15.66/15.93 (And % 15.66/15.93 (Not % 15.66/15.93 (∀ (X : Iota), % 15.66/15.93 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.66/15.93 (Not % 15.66/15.93 (∀ (X : Iota), % 15.66/15.93 Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.66/15.93 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 15.66/15.93 (Or % 15.66/15.93 (And % 15.66/15.93 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.66/15.99 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 15.66/15.99 (Or % 15.66/15.99 (And % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.66/15.99 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 15.66/15.99 (Not (p105 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 15.66/15.99 (Not (p104 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 15.66/15.99 (Not (p103 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 15.66/15.99 (Not (p102 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 15.66/15.99 (Not (p101 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 15.66/15.99 (Not (p100 a_1)))) % 15.66/15.99 (Or (p105 a_1) (Not (p106 a_1)))) % 15.66/15.99 (Or (p104 a_1) (Not (p105 a_1)))) % 15.66/15.99 (Or (p103 a_1) (Not (p104 a_1)))) % 15.66/15.99 (Or (p102 a_1) (Not (p103 a_1)))) % 15.66/15.99 (Or (p101 a_1) (Not (p102 a_1)))) % 15.66/15.99 (Or (p100 a_1) (Not (p101 a_1))))) % 15.66/15.99 True % 15.66/15.99 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), % 15.66/15.99 Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) % 15.66/15.99 (Eq % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (And % 15.66/15.99 (Or % 15.66/15.99 (And % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) % 15.66/15.99 (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.66/15.99 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) % 15.66/15.99 (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.66/15.99 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 15.66/15.99 (Or % 15.66/15.99 (And % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.66/15.99 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 15.66/15.99 (Or % 15.66/15.99 (And % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.66/15.99 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 15.66/15.99 (Or % 15.66/15.99 (And % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.66/15.99 (Not % 15.66/15.99 (∀ (X : Iota), % 15.66/15.99 Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.66/15.99 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 15.66/15.99 (Not (p105 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 15.66/15.99 (Not (p104 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 15.66/15.99 (Not (p103 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 15.66/15.99 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 15.66/15.99 (Not (p102 a_1)))) % 15.66/15.99 (Or % 15.66/15.99 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 15.78/16.05 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 15.78/16.05 (Not (p101 a_1)))) % 15.78/16.05 (Or % 15.78/16.05 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 15.78/16.05 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 15.78/16.05 (Not (p100 a_1)))) % 15.78/16.05 (Or (p105 a_1) (Not (p106 a_1)))) % 15.78/16.05 (Or (p104 a_1) (Not (p105 a_1)))) % 15.78/16.05 (Or (p103 a_1) (Not (p104 a_1)))) % 15.78/16.05 (Or (p102 a_1) (Not (p103 a_1)))) % 15.78/16.05 (Or (p101 a_1) (Not (p102 a_1)))) % 15.78/16.05 (Or (p100 a_1) (Not (p101 a_1)))) % 15.78/16.05 True) % 15.78/16.05 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), % 15.78/16.05 Or % 15.78/16.05 (Eq % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (And % 15.78/16.05 (Or % 15.78/16.05 (And % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.78/16.05 (Not (And (Not (p105 a)) (p104 a)))) % 15.78/16.05 (Or % 15.78/16.05 (And % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.78/16.05 (Not (And (Not (p104 a)) (p103 a))))) % 15.78/16.05 (Or % 15.78/16.05 (And % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.78/16.05 (Not (And (Not (p103 a)) (p102 a))))) % 15.78/16.05 (Or % 15.78/16.05 (And % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.78/16.05 (Not (And (Not (p102 a)) (p101 a))))) % 15.78/16.05 (Or % 15.78/16.05 (And % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.78/16.05 (Not % 15.78/16.05 (∀ (X : Iota), % 15.78/16.05 Or (Not (r1 a X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.78/16.11 (Not (And (Not (p101 a)) (p100 a))))) % 15.78/16.11 (Or % 15.78/16.11 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (Not (p6 X))) (Not (p105 X))) (p6 a)) % 15.78/16.11 (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (p6 X)) (Not (p105 X))) (Not (p6 a)))) % 15.78/16.11 (Not (p105 a)))) % 15.78/16.11 (Or % 15.78/16.11 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (Not (p5 X))) (Not (p104 X))) (p5 a)) % 15.78/16.11 (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (p5 X)) (Not (p104 X))) (Not (p5 a)))) % 15.78/16.11 (Not (p104 a)))) % 15.78/16.11 (Or % 15.78/16.11 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (Not (p4 X))) (Not (p103 X))) (p4 a)) % 15.78/16.11 (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (p4 X)) (Not (p103 X))) (Not (p4 a)))) % 15.78/16.11 (Not (p103 a)))) % 15.78/16.11 (Or % 15.78/16.11 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (Not (p3 X))) (Not (p102 X))) (p3 a)) % 15.78/16.11 (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (p3 X)) (Not (p102 X))) (Not (p3 a)))) % 15.78/16.11 (Not (p102 a)))) % 15.78/16.11 (Or % 15.78/16.11 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (Not (p2 X))) (Not (p101 X))) (p2 a)) % 15.78/16.11 (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (p2 X)) (Not (p101 X))) (Not (p2 a)))) % 15.78/16.11 (Not (p101 a)))) % 15.78/16.11 (Or % 15.78/16.11 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (Not (p1 X))) (Not (p100 X))) (p1 a)) % 15.78/16.11 (Or (∀ (X : Iota), Or (Or (Not (r1 a X)) (p1 X)) (Not (p100 X))) (Not (p1 a)))) % 15.78/16.11 (Not (p100 a)))) % 15.78/16.11 (Or (p105 a) (Not (p106 a)))) % 15.78/16.11 (Or (p104 a) (Not (p105 a)))) % 15.78/16.11 (Or (p103 a) (Not (p104 a)))) % 15.78/16.11 (Or (p102 a) (Not (p103 a)))) % 15.78/16.11 (Or (p101 a) (Not (p102 a)))) % 15.78/16.11 (Or (p100 a) (Not (p101 a)))) % 15.78/16.11 True) % 15.78/16.11 (Eq (r1 (skS.0 0 a_1) a) False) % 15.78/16.11 Clause #33 (by clausification #[31]): ∀ (a a_1 : Iota), % 15.78/16.11 Or (Eq (r1 (skS.0 0 a) a_1) False) % 15.78/16.11 (Eq % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (And % 15.78/16.11 (Or % 15.78/16.11 (And % 15.78/16.11 (Not % 15.78/16.11 (∀ (X : Iota), % 15.78/16.11 Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.78/16.11 (Not % 15.78/16.11 (∀ (X : Iota), % 15.78/16.11 Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.78/16.11 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 15.78/16.11 (Or % 15.78/16.11 (And % 15.78/16.11 (Not % 15.78/16.11 (∀ (X : Iota), % 15.78/16.11 Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.78/16.11 (Not % 15.78/16.11 (∀ (X : Iota), % 15.78/16.11 Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.78/16.11 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 15.78/16.11 (Or % 15.78/16.11 (And % 15.78/16.11 (Not % 15.78/16.11 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.89/16.17 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 15.89/16.17 (Or % 15.89/16.17 (And % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.89/16.17 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 15.89/16.17 (Or % 15.89/16.17 (And % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.89/16.17 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 15.89/16.17 (Not (p105 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 15.89/16.17 (Not (p104 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 15.89/16.17 (Not (p103 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 15.89/16.17 (Not (p102 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 15.89/16.17 (Not (p101 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 15.89/16.17 (Not (p100 a_1)))) % 15.89/16.17 (Or (p105 a_1) (Not (p106 a_1)))) % 15.89/16.17 (Or (p104 a_1) (Not (p105 a_1)))) % 15.89/16.17 (Or (p103 a_1) (Not (p104 a_1)))) % 15.89/16.17 (Or (p102 a_1) (Not (p103 a_1)))) % 15.89/16.17 (Or (p101 a_1) (Not (p102 a_1)))) % 15.89/16.17 True) % 15.89/16.17 Clause #40 (by clausification #[33]): ∀ (a a_1 : Iota), % 15.89/16.17 Or (Eq (r1 (skS.0 0 a) a_1) False) % 15.89/16.17 (Eq % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (And % 15.89/16.17 (Or % 15.89/16.17 (And % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.89/16.17 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.89/16.17 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 15.89/16.17 (Or % 15.89/16.17 (And % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.89/16.17 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 15.89/16.17 (Or % 15.89/16.17 (And % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.89/16.17 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 15.89/16.17 (Or % 15.89/16.17 (And % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), % 15.89/16.17 Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.89/16.17 (Not % 15.89/16.17 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.89/16.17 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 15.89/16.17 (Not (p105 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 15.89/16.17 (Not (p104 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 15.89/16.17 (Not (p103 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 15.89/16.17 (Not (p102 a_1)))) % 15.89/16.17 (Or % 15.89/16.17 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 15.89/16.17 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 15.96/16.23 (Not (p101 a_1)))) % 15.96/16.23 (Or % 15.96/16.23 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 15.96/16.23 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 15.96/16.23 (Not (p100 a_1)))) % 15.96/16.23 (Or (p105 a_1) (Not (p106 a_1)))) % 15.96/16.23 (Or (p104 a_1) (Not (p105 a_1)))) % 15.96/16.23 (Or (p103 a_1) (Not (p104 a_1)))) % 15.96/16.23 (Or (p102 a_1) (Not (p103 a_1)))) % 15.96/16.23 True) % 15.96/16.23 Clause #46 (by clausification #[40]): ∀ (a a_1 : Iota), % 15.96/16.23 Or (Eq (r1 (skS.0 0 a) a_1) False) % 15.96/16.23 (Eq % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (And % 15.96/16.23 (Or % 15.96/16.23 (And % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.96/16.23 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 15.96/16.23 (Or % 15.96/16.23 (And % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.96/16.23 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 15.96/16.23 (Or % 15.96/16.23 (And % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.96/16.23 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 15.96/16.23 (Or % 15.96/16.23 (And % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.96/16.23 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 15.96/16.23 (Or % 15.96/16.23 (And % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), % 15.96/16.23 Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 15.96/16.23 (Not % 15.96/16.23 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 15.96/16.23 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 15.96/16.23 (Or % 15.96/16.23 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 15.96/16.23 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 15.96/16.23 (Not (p105 a_1)))) % 15.96/16.23 (Or % 15.96/16.23 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 15.96/16.29 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 15.96/16.29 (Not (p104 a_1)))) % 15.96/16.29 (Or % 15.96/16.29 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 15.96/16.29 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 15.96/16.29 (Not (p103 a_1)))) % 15.96/16.29 (Or % 15.96/16.29 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 15.96/16.29 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 15.96/16.29 (Not (p102 a_1)))) % 15.96/16.29 (Or % 15.96/16.29 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 15.96/16.29 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 15.96/16.29 (Not (p101 a_1)))) % 15.96/16.29 (Or % 15.96/16.29 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 15.96/16.29 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 15.96/16.29 (Not (p100 a_1)))) % 15.96/16.29 (Or (p105 a_1) (Not (p106 a_1)))) % 15.96/16.29 (Or (p104 a_1) (Not (p105 a_1)))) % 15.96/16.29 (Or (p103 a_1) (Not (p104 a_1)))) % 15.96/16.29 True) % 15.96/16.29 Clause #52 (by clausification #[46]): ∀ (a a_1 : Iota), % 15.96/16.29 Or (Eq (r1 (skS.0 0 a) a_1) False) % 15.96/16.29 (Eq % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (And % 15.96/16.29 (Or % 15.96/16.29 (And % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), % 15.96/16.29 Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), % 15.96/16.29 Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 15.96/16.29 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 15.96/16.29 (Or % 15.96/16.29 (And % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), % 15.96/16.29 Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), % 15.96/16.29 Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 15.96/16.29 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 15.96/16.29 (Or % 15.96/16.29 (And % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), % 15.96/16.29 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 15.96/16.29 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 15.96/16.29 (Or % 15.96/16.29 (And % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), % 15.96/16.29 Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 15.96/16.29 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 15.96/16.29 (Or % 15.96/16.29 (And % 15.96/16.29 (Not % 15.96/16.29 (∀ (X : Iota), % 15.96/16.29 Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.06/16.34 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.06/16.34 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.06/16.34 (Or % 16.06/16.34 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.06/16.34 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.06/16.34 (Not (p105 a_1)))) % 16.06/16.34 (Or % 16.06/16.34 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 16.06/16.34 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 16.06/16.34 (Not (p104 a_1)))) % 16.06/16.34 (Or % 16.06/16.34 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 16.06/16.34 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 16.06/16.34 (Not (p103 a_1)))) % 16.06/16.34 (Or % 16.06/16.34 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 16.06/16.34 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 16.06/16.34 (Not (p102 a_1)))) % 16.06/16.34 (Or % 16.06/16.34 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 16.06/16.34 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 16.06/16.34 (Not (p101 a_1)))) % 16.06/16.34 (Or % 16.06/16.34 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 16.06/16.34 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 16.06/16.34 (Not (p100 a_1)))) % 16.06/16.34 (Or (p105 a_1) (Not (p106 a_1)))) % 16.06/16.34 (Or (p104 a_1) (Not (p105 a_1)))) % 16.06/16.34 True) % 16.06/16.34 Clause #58 (by clausification #[52]): ∀ (a a_1 : Iota), % 16.06/16.34 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.06/16.34 (Eq % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (And % 16.06/16.34 (Or % 16.06/16.34 (And % 16.06/16.34 (Not % 16.06/16.34 (∀ (X : Iota), % 16.06/16.34 Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.06/16.34 (Not % 16.06/16.34 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.06/16.34 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.06/16.34 (Or % 16.06/16.34 (And % 16.06/16.34 (Not % 16.06/16.34 (∀ (X : Iota), % 16.06/16.34 Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.06/16.34 (Not % 16.06/16.34 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.06/16.34 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.06/16.34 (Or % 16.06/16.34 (And % 16.06/16.34 (Not % 16.06/16.34 (∀ (X : Iota), % 16.06/16.34 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.06/16.34 (Not % 16.06/16.34 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.06/16.34 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.06/16.34 (Or % 16.06/16.34 (And % 16.06/16.34 (Not % 16.06/16.34 (∀ (X : Iota), % 16.06/16.34 Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.06/16.34 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.06/16.39 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.06/16.39 (Or % 16.06/16.39 (And % 16.06/16.39 (Not % 16.06/16.39 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.06/16.39 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.06/16.39 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.06/16.39 (Or % 16.06/16.39 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.06/16.39 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.06/16.39 (Not (p105 a_1)))) % 16.06/16.39 (Or % 16.06/16.39 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 16.06/16.39 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 16.06/16.39 (Not (p104 a_1)))) % 16.06/16.39 (Or % 16.06/16.39 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 16.06/16.39 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 16.06/16.39 (Not (p103 a_1)))) % 16.06/16.39 (Or % 16.06/16.39 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 16.06/16.39 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 16.06/16.39 (Not (p102 a_1)))) % 16.06/16.39 (Or % 16.06/16.39 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 16.06/16.39 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 16.06/16.39 (Not (p101 a_1)))) % 16.06/16.39 (Or % 16.06/16.39 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 16.06/16.39 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 16.06/16.39 (Not (p100 a_1)))) % 16.06/16.39 (Or (p105 a_1) (Not (p106 a_1)))) % 16.06/16.39 True) % 16.06/16.39 Clause #64 (by clausification #[58]): ∀ (a a_1 : Iota), % 16.06/16.39 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.06/16.39 (Eq % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (And % 16.06/16.39 (Or % 16.06/16.39 (And % 16.06/16.39 (Not % 16.06/16.39 (∀ (X : Iota), % 16.06/16.39 Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.06/16.39 (Not % 16.06/16.39 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.06/16.39 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.06/16.39 (Or % 16.06/16.39 (And % 16.06/16.39 (Not % 16.06/16.39 (∀ (X : Iota), % 16.06/16.39 Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.06/16.39 (Not % 16.06/16.39 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.06/16.39 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.06/16.39 (Or % 16.06/16.39 (And % 16.06/16.39 (Not % 16.06/16.39 (∀ (X : Iota), % 16.06/16.39 Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.06/16.39 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.06/16.39 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.06/16.39 (Or % 16.06/16.39 (And % 16.06/16.39 (Not % 16.06/16.39 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.06/16.39 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.16/16.44 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.16/16.44 (Or % 16.16/16.44 (And % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.16/16.44 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.16/16.44 (Or % 16.16/16.44 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.16/16.44 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.16/16.44 (Not (p105 a_1)))) % 16.16/16.44 (Or % 16.16/16.44 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 16.16/16.44 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 16.16/16.44 (Not (p104 a_1)))) % 16.16/16.44 (Or % 16.16/16.44 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 16.16/16.44 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 16.16/16.44 (Not (p103 a_1)))) % 16.16/16.44 (Or % 16.16/16.44 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 16.16/16.44 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 16.16/16.44 (Not (p102 a_1)))) % 16.16/16.44 (Or % 16.16/16.44 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 16.16/16.44 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 16.16/16.44 (Not (p101 a_1)))) % 16.16/16.44 (Or % 16.16/16.44 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p1 X))) (Not (p100 X))) (p1 a_1)) % 16.16/16.44 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p1 X)) (Not (p100 X))) (Not (p1 a_1)))) % 16.16/16.44 (Not (p100 a_1)))) % 16.16/16.44 True) % 16.16/16.44 Clause #70 (by clausification #[64]): ∀ (a a_1 : Iota), % 16.16/16.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.16/16.44 (Eq % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (And % 16.16/16.44 (Or % 16.16/16.44 (And % 16.16/16.44 (Not % 16.16/16.44 (∀ (X : Iota), % 16.16/16.44 Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.16/16.44 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.16/16.44 (Or % 16.16/16.44 (And % 16.16/16.44 (Not % 16.16/16.44 (∀ (X : Iota), % 16.16/16.44 Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.16/16.44 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.16/16.44 (Or % 16.16/16.44 (And % 16.16/16.44 (Not % 16.16/16.44 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.16/16.44 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.16/16.44 (Or % 16.16/16.44 (And % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.16/16.44 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.16/16.44 (Or % 16.16/16.44 (And % 16.16/16.44 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.16/16.48 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.16/16.48 (Or % 16.16/16.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.16/16.48 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.16/16.48 (Not (p105 a_1)))) % 16.16/16.48 (Or % 16.16/16.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 16.16/16.48 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 16.16/16.48 (Not (p104 a_1)))) % 16.16/16.48 (Or % 16.16/16.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 16.16/16.48 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 16.16/16.48 (Not (p103 a_1)))) % 16.16/16.48 (Or % 16.16/16.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 16.16/16.48 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 16.16/16.48 (Not (p102 a_1)))) % 16.16/16.48 (Or % 16.16/16.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p2 X))) (Not (p101 X))) (p2 a_1)) % 16.16/16.48 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p2 X)) (Not (p101 X))) (Not (p2 a_1)))) % 16.16/16.48 (Not (p101 a_1)))) % 16.16/16.48 True) % 16.16/16.48 Clause #100 (by clausification #[70]): ∀ (a a_1 : Iota), % 16.16/16.48 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.16/16.48 (Eq % 16.16/16.48 (And % 16.16/16.48 (And % 16.16/16.48 (And % 16.16/16.48 (And % 16.16/16.48 (And % 16.16/16.48 (And % 16.16/16.48 (And % 16.16/16.48 (And % 16.16/16.48 (Or % 16.16/16.48 (And % 16.16/16.48 (Not % 16.16/16.48 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.16/16.48 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.16/16.48 (Or % 16.16/16.48 (And % 16.16/16.48 (Not % 16.16/16.48 (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.16/16.48 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.16/16.48 (Or % 16.16/16.48 (And % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.16/16.48 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.16/16.48 (Or % 16.16/16.48 (And % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.16/16.48 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.16/16.48 (Or % 16.16/16.48 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.16/16.48 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.16/16.48 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.16/16.48 (Or % 16.16/16.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.16/16.48 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.16/16.48 (Not (p105 a_1)))) % 16.16/16.48 (Or % 16.16/16.48 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 16.16/16.48 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 16.16/16.48 (Not (p104 a_1)))) % 16.16/16.48 (Or % 16.26/16.56 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 16.26/16.56 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 16.26/16.56 (Not (p103 a_1)))) % 16.26/16.56 (Or % 16.26/16.56 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p3 X))) (Not (p102 X))) (p3 a_1)) % 16.26/16.56 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p3 X)) (Not (p102 X))) (Not (p3 a_1)))) % 16.26/16.56 (Not (p102 a_1)))) % 16.26/16.56 True) % 16.26/16.56 Clause #130 (by clausification #[100]): ∀ (a a_1 : Iota), % 16.26/16.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.26/16.56 (Eq % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (Or % 16.26/16.56 (And % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.26/16.56 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.26/16.56 (Or % 16.26/16.56 (And % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.26/16.56 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.26/16.56 (Or % 16.26/16.56 (And % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.26/16.56 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.26/16.56 (Or % 16.26/16.56 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.26/16.56 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.26/16.56 (Or % 16.26/16.56 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.26/16.56 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.26/16.56 (Or % 16.26/16.56 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.26/16.56 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.26/16.56 (Not (p105 a_1)))) % 16.26/16.56 (Or % 16.26/16.56 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 16.26/16.56 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 16.26/16.56 (Not (p104 a_1)))) % 16.26/16.56 (Or % 16.26/16.56 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p4 X))) (Not (p103 X))) (p4 a_1)) % 16.26/16.56 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p4 X)) (Not (p103 X))) (Not (p4 a_1)))) % 16.26/16.56 (Not (p103 a_1)))) % 16.26/16.56 True) % 16.26/16.56 Clause #155 (by clausification #[130]): ∀ (a a_1 : Iota), % 16.26/16.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.26/16.56 (Eq % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (And % 16.26/16.56 (Or % 16.26/16.56 (And % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.26/16.56 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.26/16.56 (Or % 16.26/16.56 (And % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.26/16.56 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.26/16.56 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.26/16.56 (Or % 16.26/16.56 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.36/16.62 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.36/16.62 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.36/16.62 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.36/16.62 (Or % 16.36/16.62 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.36/16.62 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.36/16.62 (Not (p105 a_1)))) % 16.36/16.62 (Or % 16.36/16.62 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p5 X))) (Not (p104 X))) (p5 a_1)) % 16.36/16.62 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p5 X)) (Not (p104 X))) (Not (p5 a_1)))) % 16.36/16.62 (Not (p104 a_1)))) % 16.36/16.62 True) % 16.36/16.62 Clause #179 (by clausification #[155]): ∀ (a a_1 : Iota), % 16.36/16.62 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.62 (Eq % 16.36/16.62 (And % 16.36/16.62 (And % 16.36/16.62 (And % 16.36/16.62 (And % 16.36/16.62 (And % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.36/16.62 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.36/16.62 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.36/16.62 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.36/16.62 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.36/16.62 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.36/16.62 (Or % 16.36/16.62 (And (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (Not (p6 X))) (Not (p105 X))) (p6 a_1)) % 16.36/16.62 (Or (∀ (X : Iota), Or (Or (Not (r1 a_1 X)) (p6 X)) (Not (p105 X))) (Not (p6 a_1)))) % 16.36/16.62 (Not (p105 a_1)))) % 16.36/16.62 True) % 16.36/16.62 Clause #205 (by clausification #[179]): ∀ (a a_1 : Iota), % 16.36/16.62 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.62 (Eq % 16.36/16.62 (And % 16.36/16.62 (And % 16.36/16.62 (And % 16.36/16.62 (And % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.36/16.62 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.36/16.62 (Or % 16.36/16.62 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.36/16.62 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.36/16.62 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.36/16.67 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.36/16.67 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.36/16.67 (Not (And (Not (p101 a_1)) (p100 a_1))))) % 16.36/16.67 True) % 16.36/16.67 Clause #218 (by clausification #[205]): ∀ (a a_1 : Iota), % 16.36/16.67 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.67 (Eq % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.36/16.67 (Not (And (Not (p101 a_1)) (p100 a_1)))) % 16.36/16.67 True) % 16.36/16.67 Clause #219 (by clausification #[205]): ∀ (a a_1 : Iota), % 16.36/16.67 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.67 (Eq % 16.36/16.67 (And % 16.36/16.67 (And % 16.36/16.67 (And % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p6 X)) (Not (p106 X))) (p105 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p6 X) (Not (p106 X))) (p105 X)))))) % 16.36/16.67 (Not (And (Not (p105 a_1)) (p104 a_1)))) % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p5 X)) (Not (p105 X))) (p104 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p5 X) (Not (p105 X))) (p104 X)))))) % 16.36/16.67 (Not (And (Not (p104 a_1)) (p103 a_1))))) % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p4 X)) (Not (p104 X))) (p103 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p4 X) (Not (p104 X))) (p103 X)))))) % 16.36/16.67 (Not (And (Not (p103 a_1)) (p102 a_1))))) % 16.36/16.67 (Or % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.36/16.67 (Not (And (Not (p102 a_1)) (p101 a_1))))) % 16.36/16.67 True) % 16.36/16.67 Clause #220 (by clausification #[218]): ∀ (a a_1 : Iota), % 16.36/16.67 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.67 (Or % 16.36/16.67 (Eq % 16.36/16.67 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 16.36/16.67 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 16.36/16.67 True) % 16.36/16.67 (Eq (Not (And (Not (p101 a_1)) (p100 a_1))) True)) % 16.36/16.67 Clause #221 (by clausification #[220]): ∀ (a a_1 : Iota), % 16.36/16.67 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.67 (Or (Eq (Not (And (Not (p101 a_1)) (p100 a_1))) True) % 16.36/16.67 (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X))))) True)) % 16.36/16.67 Clause #223 (by clausification #[221]): ∀ (a a_1 : Iota), % 16.36/16.67 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.67 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X))))) True) % 16.36/16.67 (Eq (And (Not (p101 a_1)) (p100 a_1)) False)) % 16.36/16.67 Clause #224 (by clausification #[223]): ∀ (a a_1 : Iota), % 16.36/16.67 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.67 (Or (Eq (And (Not (p101 a_1)) (p100 a_1)) False) % 16.36/16.67 (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))) False)) % 16.36/16.67 Clause #225 (by clausification #[224]): ∀ (a a_1 : Iota), % 16.36/16.67 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.36/16.67 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))) False) % 16.36/16.67 (Or (Eq (Not (p101 a_1)) False) (Eq (p100 a_1) False))) % 16.36/16.67 Clause #226 (by clausification #[225]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (Not (p101 a_1)) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) % 16.46/16.74 (Eq % 16.46/16.74 (Not % 16.46/16.74 (Or (Not (r1 a_1 (skS.0 1 a_1 a_2))) % 16.46/16.74 (Not (And (And (p2 (skS.0 1 a_1 a_2)) (Not (p102 (skS.0 1 a_1 a_2)))) (p101 (skS.0 1 a_1 a_2)))))) % 16.46/16.74 True))) % 16.46/16.74 Clause #227 (by clausification #[226]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) % 16.46/16.74 (Or % 16.46/16.74 (Eq % 16.46/16.74 (Not % 16.46/16.74 (Or (Not (r1 a_1 (skS.0 1 a_1 a_2))) % 16.46/16.74 (Not (And (And (p2 (skS.0 1 a_1 a_2)) (Not (p102 (skS.0 1 a_1 a_2)))) (p101 (skS.0 1 a_1 a_2)))))) % 16.46/16.74 True) % 16.46/16.74 (Eq (p101 a_1) True))) % 16.46/16.74 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) % 16.46/16.74 (Or (Eq (p101 a_1) True) % 16.46/16.74 (Eq % 16.46/16.74 (Or (Not (r1 a_1 (skS.0 1 a_1 a_2))) % 16.46/16.74 (Not (And (And (p2 (skS.0 1 a_1 a_2)) (Not (p102 (skS.0 1 a_1 a_2)))) (p101 (skS.0 1 a_1 a_2))))) % 16.46/16.74 False))) % 16.46/16.74 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) % 16.46/16.74 (Or (Eq (p101 a_1) True) % 16.46/16.74 (Eq (Not (And (And (p2 (skS.0 1 a_1 a_2)) (Not (p102 (skS.0 1 a_1 a_2)))) (p101 (skS.0 1 a_1 a_2)))) False))) % 16.46/16.74 Clause #230 (by clausification #[228]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) (Or (Eq (p101 a_1) True) (Eq (Not (r1 a_1 (skS.0 1 a_1 a_2))) False))) % 16.46/16.74 Clause #231 (by clausification #[229]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) % 16.46/16.74 (Or (Eq (p101 a_1) True) % 16.46/16.74 (Eq (And (And (p2 (skS.0 1 a_1 a_2)) (Not (p102 (skS.0 1 a_1 a_2)))) (p101 (skS.0 1 a_1 a_2))) True))) % 16.46/16.74 Clause #232 (by clausification #[231]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) (Or (Eq (p101 a_1) True) (Eq (p101 (skS.0 1 a_1 a_2)) True))) % 16.46/16.74 Clause #233 (by clausification #[231]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) % 16.46/16.74 (Or (Eq (p101 a_1) True) (Eq (And (p2 (skS.0 1 a_1 a_2)) (Not (p102 (skS.0 1 a_1 a_2)))) True))) % 16.46/16.74 Clause #234 (by superposition #[232, 3]): ∀ (a a_1 : Iota), % 16.46/16.74 Or (Eq (p100 (skS.0 0 a)) False) % 16.46/16.74 (Or (Eq (p101 (skS.0 0 a)) True) (Or (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) True) (Eq False True))) % 16.46/16.74 Clause #235 (by clausification #[230]): ∀ (a a_1 a_2 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or (Eq (p100 a_1) False) (Or (Eq (p101 a_1) True) (Eq (r1 a_1 (skS.0 1 a_1 a_2)) True))) % 16.46/16.74 Clause #236 (by superposition #[235, 3]): ∀ (a a_1 : Iota), % 16.46/16.74 Or (Eq (p100 (skS.0 0 a)) False) % 16.46/16.74 (Or (Eq (p101 (skS.0 0 a)) True) (Or (Eq (r1 (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True) (Eq False True))) % 16.46/16.74 Clause #248 (by clausification #[234]): ∀ (a a_1 : Iota), % 16.46/16.74 Or (Eq (p100 (skS.0 0 a)) False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) True)) % 16.46/16.74 Clause #249 (by forward demodulation #[248, 18]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) True)) % 16.46/16.74 Clause #250 (by clausification #[249]): ∀ (a a_1 : Iota), Or (Eq (p101 (skS.0 0 a)) True) (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) True) % 16.46/16.74 Clause #251 (by forward demodulation #[250, 27]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) True) % 16.46/16.74 Clause #252 (by clausification #[251]): ∀ (a a_1 : Iota), Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) True % 16.46/16.74 Clause #253 (by clausification #[219]): ∀ (a a_1 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Eq % 16.46/16.74 (Or % 16.46/16.74 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.46/16.74 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.46/16.74 (Not (And (Not (p102 a_1)) (p101 a_1)))) % 16.46/16.74 True) % 16.46/16.74 Clause #255 (by clausification #[253]): ∀ (a a_1 : Iota), % 16.46/16.74 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.46/16.74 (Or % 16.46/16.74 (Eq % 16.46/16.74 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) % 16.56/16.81 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (p3 X) (Not (p103 X))) (p102 X)))))) % 16.56/16.81 True) % 16.56/16.81 (Eq (Not (And (Not (p102 a_1)) (p101 a_1))) True)) % 16.56/16.81 Clause #257 (by clausification #[255]): ∀ (a a_1 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (Not (And (Not (p102 a_1)) (p101 a_1))) True) % 16.56/16.81 (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) True)) % 16.56/16.81 Clause #274 (by clausification #[257]): ∀ (a a_1 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X))))) True) % 16.56/16.81 (Eq (And (Not (p102 a_1)) (p101 a_1)) False)) % 16.56/16.81 Clause #275 (by clausification #[274]): ∀ (a a_1 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (And (Not (p102 a_1)) (p101 a_1)) False) % 16.56/16.81 (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X)))) False)) % 16.56/16.81 Clause #276 (by clausification #[275]): ∀ (a a_1 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (And (And (Not (p3 X)) (Not (p103 X))) (p102 X)))) False) % 16.56/16.81 (Or (Eq (Not (p102 a_1)) False) (Eq (p101 a_1) False))) % 16.56/16.81 Clause #277 (by clausification #[276]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (Not (p102 a_1)) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) % 16.56/16.81 (Eq % 16.56/16.81 (Not % 16.56/16.81 (Or (Not (r1 a_1 (skS.0 3 a_1 a_2))) % 16.56/16.81 (Not (And (And (Not (p3 (skS.0 3 a_1 a_2))) (Not (p103 (skS.0 3 a_1 a_2)))) (p102 (skS.0 3 a_1 a_2)))))) % 16.56/16.81 True))) % 16.56/16.81 Clause #278 (by clausification #[277]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) % 16.56/16.81 (Or % 16.56/16.81 (Eq % 16.56/16.81 (Not % 16.56/16.81 (Or (Not (r1 a_1 (skS.0 3 a_1 a_2))) % 16.56/16.81 (Not (And (And (Not (p3 (skS.0 3 a_1 a_2))) (Not (p103 (skS.0 3 a_1 a_2)))) (p102 (skS.0 3 a_1 a_2)))))) % 16.56/16.81 True) % 16.56/16.81 (Eq (p102 a_1) True))) % 16.56/16.81 Clause #279 (by clausification #[278]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) % 16.56/16.81 (Or (Eq (p102 a_1) True) % 16.56/16.81 (Eq % 16.56/16.81 (Or (Not (r1 a_1 (skS.0 3 a_1 a_2))) % 16.56/16.81 (Not (And (And (Not (p3 (skS.0 3 a_1 a_2))) (Not (p103 (skS.0 3 a_1 a_2)))) (p102 (skS.0 3 a_1 a_2))))) % 16.56/16.81 False))) % 16.56/16.81 Clause #280 (by clausification #[279]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) % 16.56/16.81 (Or (Eq (p102 a_1) True) % 16.56/16.81 (Eq (Not (And (And (Not (p3 (skS.0 3 a_1 a_2))) (Not (p103 (skS.0 3 a_1 a_2)))) (p102 (skS.0 3 a_1 a_2)))) % 16.56/16.81 False))) % 16.56/16.81 Clause #281 (by clausification #[279]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) (Or (Eq (p102 a_1) True) (Eq (Not (r1 a_1 (skS.0 3 a_1 a_2))) False))) % 16.56/16.81 Clause #282 (by clausification #[280]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) % 16.56/16.81 (Or (Eq (p102 a_1) True) % 16.56/16.81 (Eq (And (And (Not (p3 (skS.0 3 a_1 a_2))) (Not (p103 (skS.0 3 a_1 a_2)))) (p102 (skS.0 3 a_1 a_2))) True))) % 16.56/16.81 Clause #284 (by clausification #[282]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) % 16.56/16.81 (Or (Eq (p102 a_1) True) (Eq (And (Not (p3 (skS.0 3 a_1 a_2))) (Not (p103 (skS.0 3 a_1 a_2)))) True))) % 16.56/16.81 Clause #286 (by clausification #[281]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p101 a_1) False) (Or (Eq (p102 a_1) True) (Eq (r1 a_1 (skS.0 3 a_1 a_2)) True))) % 16.56/16.81 Clause #309 (by clausification #[233]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p100 a_1) False) (Or (Eq (p101 a_1) True) (Eq (Not (p102 (skS.0 1 a_1 a_2))) True))) % 16.56/16.81 Clause #311 (by clausification #[309]): ∀ (a a_1 a_2 : Iota), % 16.56/16.81 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.81 (Or (Eq (p100 a_1) False) (Or (Eq (p101 a_1) True) (Eq (p102 (skS.0 1 a_1 a_2)) False))) % 16.56/16.81 Clause #312 (by superposition #[311, 3]): ∀ (a a_1 : Iota), % 16.56/16.87 Or (Eq (p100 (skS.0 0 a)) False) % 16.56/16.87 (Or (Eq (p101 (skS.0 0 a)) True) (Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) False) (Eq False True))) % 16.56/16.87 Clause #314 (by clausification #[312]): ∀ (a a_1 : Iota), % 16.56/16.87 Or (Eq (p100 (skS.0 0 a)) False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) False)) % 16.56/16.87 Clause #315 (by forward demodulation #[314, 18]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) False)) % 16.56/16.87 Clause #316 (by clausification #[315]): ∀ (a a_1 : Iota), Or (Eq (p101 (skS.0 0 a)) True) (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) False) % 16.56/16.87 Clause #317 (by forward demodulation #[316, 27]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) False) % 16.56/16.87 Clause #318 (by clausification #[317]): ∀ (a a_1 : Iota), Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) False % 16.56/16.87 Clause #319 (by clausification #[236]): ∀ (a a_1 : Iota), % 16.56/16.87 Or (Eq (p100 (skS.0 0 a)) False) % 16.56/16.87 (Or (Eq (p101 (skS.0 0 a)) True) (Eq (r1 (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True)) % 16.56/16.87 Clause #320 (by forward demodulation #[319, 18]): ∀ (a a_1 : Iota), % 16.56/16.87 Or (Eq True False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (r1 (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True)) % 16.56/16.87 Clause #321 (by clausification #[320]): ∀ (a a_1 : Iota), Or (Eq (p101 (skS.0 0 a)) True) (Eq (r1 (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True) % 16.56/16.87 Clause #322 (by forward demodulation #[321, 27]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (r1 (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True) % 16.56/16.87 Clause #323 (by clausification #[322]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True % 16.56/16.87 Clause #347 (by superposition #[323, 286]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq True False) % 16.56/16.87 (Or (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) False) % 16.56/16.87 (Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) % 16.56/16.87 (Eq (r1 (skS.0 1 (skS.0 0 a) a_1) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True))) % 16.56/16.87 Clause #352 (by superposition #[323, 8]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq (r1 (skS.0 0 a) a_1) True) (Or (Eq True False) (Eq (r1 (skS.0 1 (skS.0 0 a) a_2) a_1) False)) % 16.56/16.87 Clause #354 (by clausification #[352]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 0 a) a_1) True) (Eq (r1 (skS.0 1 (skS.0 0 a) a_2) a_1) False) % 16.56/16.87 Clause #429 (by clausification #[284]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.87 (Or (Eq (p101 a_1) False) (Or (Eq (p102 a_1) True) (Eq (Not (p3 (skS.0 3 a_1 a_2))) True))) % 16.56/16.87 Clause #433 (by clausification #[429]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 16.56/16.87 (Or (Eq (p101 a_1) False) (Or (Eq (p102 a_1) True) (Eq (p3 (skS.0 3 a_1 a_2)) False))) % 16.56/16.87 Clause #434 (by superposition #[433, 323]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) False) % 16.56/16.87 (Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) % 16.56/16.87 (Or (Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) False) (Eq False True))) % 16.56/16.87 Clause #616 (by clausification #[434]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) False) % 16.56/16.87 (Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) (Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) False)) % 16.56/16.87 Clause #617 (by forward demodulation #[616, 252]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq True False) % 16.56/16.87 (Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) (Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) False)) % 16.56/16.87 Clause #618 (by clausification #[617]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) (Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) False) % 16.56/16.87 Clause #619 (by forward demodulation #[618, 318]): ∀ (a a_1 a_2 : Iota), Or (Eq False True) (Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) False) % 16.56/16.87 Clause #620 (by clausification #[619]): ∀ (a a_1 a_2 : Iota), Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) False % 16.56/16.87 Clause #802 (by clausification #[347]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq (p101 (skS.0 1 (skS.0 0 a) a_1)) False) % 16.56/16.87 (Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) % 16.56/16.87 (Eq (r1 (skS.0 1 (skS.0 0 a) a_1) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True)) % 16.56/16.87 Clause #803 (by forward demodulation #[802, 252]): ∀ (a a_1 a_2 : Iota), % 16.56/16.87 Or (Eq True False) % 16.56/16.87 (Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) % 16.66/16.90 (Eq (r1 (skS.0 1 (skS.0 0 a) a_1) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True)) % 16.66/16.90 Clause #804 (by clausification #[803]): ∀ (a a_1 a_2 : Iota), % 16.66/16.90 Or (Eq (p102 (skS.0 1 (skS.0 0 a) a_1)) True) % 16.66/16.90 (Eq (r1 (skS.0 1 (skS.0 0 a) a_1) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True) % 16.66/16.90 Clause #805 (by forward demodulation #[804, 318]): ∀ (a a_1 a_2 : Iota), % 16.66/16.90 Or (Eq False True) (Eq (r1 (skS.0 1 (skS.0 0 a) a_1) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True) % 16.66/16.90 Clause #806 (by clausification #[805]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 1 (skS.0 0 a) a_1) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True % 16.66/16.90 Clause #807 (by superposition #[806, 354]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 0 a) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True) (Eq True False) % 16.66/16.90 Clause #809 (by clausification #[807]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 0 a) (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True % 16.66/16.90 Clause #810 (by superposition #[809, 23]): ∀ (a a_1 a_2 : Iota), Or (Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True) (Eq True False) % 16.66/16.90 Clause #853 (by clausification #[810]): ∀ (a a_1 a_2 : Iota), Eq (p3 (skS.0 3 (skS.0 1 (skS.0 0 a) a_1) a_2)) True % 16.66/16.90 Clause #854 (by superposition #[853, 620]): Eq True False % 16.66/16.90 Clause #855 (by clausification #[854]): False % 16.66/16.90 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------