%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.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:13 AM UTC 2026 % Result : Theorem 39.39s 39.75s % Output : Proof 40.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : duper %s % 0.12/0.42 % Computer : n006.cluster.edu % 0.12/0.42 % Model : x86_64 x86_64 % 0.12/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.42 % Memory : 8046.5625MB % 0.12/0.42 % OS : Linux 6.8.0-71-generic % 0.12/0.42 % CPULimit : 300 % 0.12/0.42 % WCLimit : 300 % 0.12/0.42 % DateTime : Fri Sep 4 13:07:17 UTC 2026 % 0.12/0.43 % CPUTime : % 39.39/39.75 SZS status Theorem for theBenchmark.p % 39.39/39.75 SZS output start Proof for theBenchmark.p % 39.39/39.75 Clause #0 (by assumption #[]): Eq % 39.39/39.75 (Not % 39.39/39.75 (Not % 39.39/39.75 (Exists fun X => % 39.39/39.75 Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.39/39.75 (p10 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p11 Y)) % 39.39/39.75 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 Y X)) % 39.39/39.75 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 39.39/39.75 (p10 X))) % 39.39/39.75 (p11 Y)) % 39.39/39.75 (Not % 39.39/39.75 (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.39/39.75 (p10 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p11 X)) % 39.39/39.75 (Not % 39.39/39.75 (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) % 39.39/39.75 (p10 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.39/39.75 (p10 Y)) % 39.39/39.75 (p11 Y)) % 39.39/39.75 (Not % 39.39/39.75 (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) % 39.39/39.75 (p10 Y)))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.39/39.75 (p9 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p10 Y)) % 39.39/39.75 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 Y X)) % 39.39/39.75 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 39.39/39.75 (p9 X))) % 39.39/39.75 (p10 Y)) % 39.39/39.75 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.39/39.75 (p9 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p10 X)) % 39.39/39.75 (Not % 39.39/39.75 (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) % 39.39/39.75 (p9 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.39/39.75 (p9 Y)) % 39.39/39.75 (p10 Y)) % 39.39/39.75 (Not % 39.39/39.75 (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.39/39.75 (p8 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p9 Y)) % 39.39/39.75 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 Y X)) % 39.39/39.75 (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 39.39/39.75 (p8 X))) % 39.39/39.75 (p9 Y)) % 39.39/39.75 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.39/39.75 (p8 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p9 X)) % 39.39/39.75 (Not % 39.39/39.75 (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.39/39.75 (p8 Y)) % 39.39/39.75 (p9 Y)) % 39.39/39.75 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.39/39.75 (p7 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p8 Y)) % 39.39/39.75 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 Y X)) % 39.39/39.75 (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 39.39/39.75 (p7 X))) % 39.39/39.75 (p8 Y)) % 39.39/39.75 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.39/39.75 (p7 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p8 X)) % 39.39/39.75 (Not % 39.39/39.75 (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.39/39.75 (p7 Y)) % 39.39/39.75 (p8 Y)) % 39.39/39.75 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.39/39.75 (p6 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p7 Y)) % 39.39/39.75 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 Y X)) % 39.39/39.75 (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 39.39/39.75 (p6 X))) % 39.39/39.75 (p7 Y)) % 39.39/39.75 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.39/39.75 (p6 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p7 X)) % 39.39/39.75 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.39/39.75 (p6 Y)) % 39.39/39.75 (p7 Y)) % 39.39/39.75 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 39.39/39.75 (p5 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p6 Y)) % 39.39/39.75 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 Y X)) % 39.39/39.75 (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 39.39/39.75 (p5 X))) % 39.39/39.75 (p6 Y)) % 39.39/39.75 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 39.39/39.75 (p5 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p6 X)) % 39.39/39.75 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 39.39/39.75 (p5 Y)) % 39.39/39.75 (p6 Y)) % 39.39/39.75 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p5 Y)) % 39.39/39.75 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Not (r1 Y X)) % 39.39/39.75 (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 39.39/39.75 (p4 X))) % 39.39/39.75 (p5 Y)) % 39.39/39.75 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 39.39/39.75 (p4 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p5 X)) % 39.39/39.75 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 39.39/39.75 (p4 Y)) % 39.39/39.75 (p5 Y)) % 39.39/39.75 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p4 Y)) % 39.39/39.75 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 39.39/39.75 (p3 X))) % 39.39/39.75 (p4 Y)) % 39.39/39.75 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 39.39/39.75 (p3 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p4 X)) % 39.39/39.75 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 39.39/39.75 (p3 Y)) % 39.39/39.75 (p4 Y)) % 39.39/39.75 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p3 Y)) % 39.39/39.75 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 39.39/39.75 (p2 X))) % 39.39/39.75 (p3 Y)) % 39.39/39.75 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p3 X)) % 39.39/39.75 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 39.39/39.75 (p3 Y)) % 39.39/39.75 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 39.39/39.75 (Not % 39.39/39.75 (Or % 39.39/39.75 (Or % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Not (r1 X Y)) (p2 Y)) % 39.39/39.75 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 39.39/39.75 (Not % 39.39/39.75 (And % 39.39/39.75 (And % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or % 39.39/39.75 (Or (Not (r1 X Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) % 39.39/39.75 (p1 X))) % 39.39/39.75 (p2 Y)) % 39.39/39.75 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 39.39/39.75 (∀ (X : Iota), % 39.39/39.75 Or (Or (Not (r1 Y X)) (p2 X)) % 39.39/39.75 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 39.39/39.75 (∀ (Y : Iota), % 39.39/39.75 Or % 39.39/39.75 (Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 39.39/39.75 (p2 Y)) % 39.39/39.75 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))))))))))) % 39.59/39.99 True % 39.59/39.99 Clause #1 (by clausification #[0]): Eq % 39.59/39.99 (Not % 39.59/39.99 (Exists fun X => % 39.59/39.99 Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.59/39.99 (p10 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p11 Y)) % 39.59/39.99 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 Y X)) % 39.59/39.99 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 39.59/39.99 (p10 X))) % 39.59/39.99 (p11 Y)) % 39.59/39.99 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.59/39.99 (p10 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p11 X)) % 39.59/39.99 (Not % 39.59/39.99 (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) % 39.59/39.99 (p10 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.59/39.99 (p10 Y)) % 39.59/39.99 (p11 Y)) % 39.59/39.99 (Not % 39.59/39.99 (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.59/39.99 (p9 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p10 Y)) % 39.59/39.99 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 Y X)) % 39.59/39.99 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 39.59/39.99 (p9 X))) % 39.59/39.99 (p10 Y)) % 39.59/39.99 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.59/39.99 (p9 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p10 X)) % 39.59/39.99 (Not % 39.59/39.99 (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) (p9 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.59/39.99 (p9 Y)) % 39.59/39.99 (p10 Y)) % 39.59/39.99 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.59/39.99 (p8 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p9 Y)) % 39.59/39.99 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 Y X)) % 39.59/39.99 (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 39.59/39.99 (p8 X))) % 39.59/39.99 (p9 Y)) % 39.59/39.99 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.59/39.99 (p8 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p9 X)) % 39.59/39.99 (Not % 39.59/39.99 (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.59/39.99 (p8 Y)) % 39.59/39.99 (p9 Y)) % 39.59/39.99 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.59/39.99 (p7 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p8 Y)) % 39.59/39.99 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 Y X)) % 39.59/39.99 (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 39.59/39.99 (p7 X))) % 39.59/39.99 (p8 Y)) % 39.59/39.99 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.59/39.99 (p7 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p8 X)) % 39.59/39.99 (Not (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.59/39.99 (p7 Y)) % 39.59/39.99 (p8 Y)) % 39.59/39.99 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.59/39.99 (p6 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p7 Y)) % 39.59/39.99 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 Y X)) % 39.59/39.99 (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 39.59/39.99 (p6 X))) % 39.59/39.99 (p7 Y)) % 39.59/39.99 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.59/39.99 (p6 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p7 X)) % 39.59/39.99 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.59/39.99 (p6 Y)) % 39.59/39.99 (p7 Y)) % 39.59/39.99 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) (p5 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p6 Y)) % 39.59/39.99 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 Y X)) % 39.59/39.99 (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 39.59/39.99 (p5 X))) % 39.59/39.99 (p6 Y)) % 39.59/39.99 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 39.59/39.99 (p5 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p6 X)) % 39.59/39.99 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 39.59/39.99 (p5 Y)) % 39.59/39.99 (p6 Y)) % 39.59/39.99 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p5 Y)) % 39.59/39.99 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Not (r1 Y X)) % 39.59/39.99 (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 39.59/39.99 (p4 X))) % 39.59/39.99 (p5 Y)) % 39.59/39.99 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 39.59/39.99 (p4 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p5 X)) % 39.59/39.99 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 39.59/39.99 (p4 Y)) % 39.59/39.99 (p5 Y)) % 39.59/39.99 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p4 Y)) % 39.59/39.99 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Not (r1 X Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 39.59/39.99 (p3 X))) % 39.59/39.99 (p4 Y)) % 39.59/39.99 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 39.59/39.99 (∀ (X : Iota), % 39.59/39.99 Or (Or (Not (r1 Y X)) (p4 X)) % 39.59/39.99 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.59/39.99 (Or % 39.59/39.99 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 39.59/39.99 (p4 Y)) % 39.59/39.99 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 39.59/39.99 (Not % 39.59/39.99 (Or % 39.59/39.99 (Or % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or (Or (Not (r1 X Y)) (p3 Y)) % 39.59/39.99 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 39.59/39.99 (Not % 39.59/39.99 (And % 39.59/39.99 (And % 39.59/39.99 (∀ (Y : Iota), % 39.59/39.99 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 39.89/40.23 (p2 X))) % 39.89/40.23 (p3 Y)) % 39.89/40.23 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p3 X)) % 39.89/40.23 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 39.89/40.23 (p3 Y)) % 39.89/40.23 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p2 Y)) % 39.89/40.23 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) % 39.89/40.23 (p1 X))) % 39.89/40.23 (p2 Y)) % 39.89/40.23 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p2 X)) % 39.89/40.23 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 39.89/40.23 (p2 Y)) % 39.89/40.23 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))))))))) % 39.89/40.23 False % 39.89/40.23 Clause #2 (by clausification #[1]): Eq % 39.89/40.23 (Exists fun X => % 39.89/40.23 Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.89/40.23 (p10 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p11 Y)) % 39.89/40.23 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Not (r1 Y X)) % 39.89/40.23 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 39.89/40.23 (p10 X))) % 39.89/40.23 (p11 Y)) % 39.89/40.23 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.89/40.23 (p10 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p11 X)) % 39.89/40.23 (Not % 39.89/40.23 (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) % 39.89/40.23 (p10 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 39.89/40.23 (p10 Y)) % 39.89/40.23 (p11 Y)) % 39.89/40.23 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.89/40.23 (p9 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p10 Y)) % 39.89/40.23 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Not (r1 Y X)) % 39.89/40.23 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 39.89/40.23 (p9 X))) % 39.89/40.23 (p10 Y)) % 39.89/40.23 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.89/40.23 (p9 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p10 X)) % 39.89/40.23 (Not % 39.89/40.23 (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) (p9 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 39.89/40.23 (p9 Y)) % 39.89/40.23 (p10 Y)) % 39.89/40.23 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.89/40.23 (p8 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p9 Y)) % 39.89/40.23 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Not (r1 Y X)) % 39.89/40.23 (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 39.89/40.23 (p8 X))) % 39.89/40.23 (p9 Y)) % 39.89/40.23 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.89/40.23 (p8 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p9 X)) % 39.89/40.23 (Not (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 39.89/40.23 (p8 Y)) % 39.89/40.23 (p9 Y)) % 39.89/40.23 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.89/40.23 (p7 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p8 Y)) % 39.89/40.23 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Not (r1 Y X)) % 39.89/40.23 (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 39.89/40.23 (p7 X))) % 39.89/40.23 (p8 Y)) % 39.89/40.23 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.89/40.23 (p7 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p8 X)) % 39.89/40.23 (Not (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 39.89/40.23 (p7 Y)) % 39.89/40.23 (p8 Y)) % 39.89/40.23 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) (p6 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p7 Y)) % 39.89/40.23 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Not (r1 Y X)) % 39.89/40.23 (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 39.89/40.23 (p6 X))) % 39.89/40.23 (p7 Y)) % 39.89/40.23 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Or (Not (r1 X Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.89/40.23 (p6 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p7 X)) % 39.89/40.23 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Or (Not (r1 X Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 39.89/40.23 (p6 Y)) % 39.89/40.23 (p7 Y)) % 39.89/40.23 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) (p5 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p6 Y)) % 39.89/40.23 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Not (r1 Y X)) % 39.89/40.23 (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 39.89/40.23 (p5 X))) % 39.89/40.23 (p6 Y)) % 39.89/40.23 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 39.89/40.23 (p5 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p6 X)) % 39.89/40.23 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 39.89/40.23 (p5 Y)) % 39.89/40.23 (p6 Y)) % 39.89/40.23 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p5 Y)) % 39.89/40.23 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 39.89/40.23 (p4 X))) % 39.89/40.23 (p5 Y)) % 39.89/40.23 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 39.89/40.23 (p4 Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (p5 X)) % 39.89/40.23 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 39.89/40.23 (p4 Y)) % 39.89/40.23 (p5 Y)) % 39.89/40.23 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (Or % 39.89/40.23 (Or % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or (Or (Not (r1 X Y)) (p4 Y)) % 39.89/40.23 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 39.89/40.23 (Not % 39.89/40.23 (And % 39.89/40.23 (And % 39.89/40.23 (∀ (Y : Iota), % 39.89/40.23 Or % 39.89/40.23 (Or % 39.89/40.23 (Or (Not (r1 X Y)) % 39.89/40.23 (∀ (X : Iota), % 39.89/40.23 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 40.09/40.47 (p3 X))) % 40.09/40.47 (p4 Y)) % 40.09/40.47 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p4 X)) % 40.09/40.47 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 40.09/40.47 (p4 Y)) % 40.09/40.47 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 X Y)) (p3 Y)) % 40.09/40.47 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 X Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 40.09/40.47 (p2 X))) % 40.09/40.47 (p3 Y)) % 40.09/40.47 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p3 X)) % 40.09/40.47 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 40.09/40.47 (p3 Y)) % 40.09/40.47 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 X Y)) (p2 Y)) (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 X Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) (p1 X))) % 40.09/40.47 (p2 Y)) % 40.09/40.47 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p2 X)) % 40.09/40.47 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 40.09/40.47 (p2 Y)) % 40.09/40.47 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))))))))) % 40.09/40.47 True % 40.09/40.47 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 40.09/40.47 Eq % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.09/40.47 (p10 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p11 Y)) % 40.09/40.47 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 Y X)) % 40.09/40.47 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 40.09/40.47 (p10 X))) % 40.09/40.47 (p11 Y)) % 40.09/40.47 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.09/40.47 (p10 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p11 X)) % 40.09/40.47 (Not % 40.09/40.47 (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) % 40.09/40.47 (p10 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.09/40.47 (p10 Y)) % 40.09/40.47 (p11 Y)) % 40.09/40.47 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.09/40.47 (p9 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) % 40.09/40.47 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 Y X)) % 40.09/40.47 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 40.09/40.47 (p9 X))) % 40.09/40.47 (p10 Y)) % 40.09/40.47 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.09/40.47 (p9 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p10 X)) % 40.09/40.47 (Not % 40.09/40.47 (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) (p9 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.09/40.47 (p9 Y)) % 40.09/40.47 (p10 Y)) % 40.09/40.47 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.09/40.47 (p8 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p9 Y)) % 40.09/40.47 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 Y X)) % 40.09/40.47 (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 40.09/40.47 (p8 X))) % 40.09/40.47 (p9 Y)) % 40.09/40.47 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.09/40.47 (p8 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p9 X)) % 40.09/40.47 (Not (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.09/40.47 (p8 Y)) % 40.09/40.47 (p9 Y)) % 40.09/40.47 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.09/40.47 (p7 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p8 Y)) % 40.09/40.47 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 Y X)) % 40.09/40.47 (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 40.09/40.47 (p7 X))) % 40.09/40.47 (p8 Y)) % 40.09/40.47 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.09/40.47 (p7 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p8 X)) % 40.09/40.47 (Not (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.09/40.47 (p7 Y)) % 40.09/40.47 (p8 Y)) % 40.09/40.47 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.09/40.47 (p6 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p7 Y)) % 40.09/40.47 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 Y X)) % 40.09/40.47 (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 40.09/40.47 (p6 X))) % 40.09/40.47 (p7 Y)) % 40.09/40.47 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.09/40.47 (p6 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p7 X)) % 40.09/40.47 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.09/40.47 (p6 Y)) % 40.09/40.47 (p7 Y)) % 40.09/40.47 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.09/40.47 (p5 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 40.09/40.47 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Not (r1 Y X)) % 40.09/40.47 (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 40.09/40.47 (p5 X))) % 40.09/40.47 (p6 Y)) % 40.09/40.47 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.09/40.47 (p5 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p6 X)) % 40.09/40.47 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.09/40.47 (p5 Y)) % 40.09/40.47 (p6 Y)) % 40.09/40.47 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.09/40.47 (p4 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 40.09/40.47 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 40.09/40.47 (p4 X))) % 40.09/40.47 (p5 Y)) % 40.09/40.47 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.09/40.47 (p4 Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (p5 X)) % 40.09/40.47 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.09/40.47 (p4 Y)) % 40.09/40.47 (p5 Y)) % 40.09/40.47 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) % 40.09/40.47 (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (Or % 40.09/40.47 (Or % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p4 Y)) % 40.09/40.47 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 40.09/40.47 (Not % 40.09/40.47 (And % 40.09/40.47 (And % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or % 40.09/40.47 (Or (Not (r1 (skS.0 0 a) Y)) % 40.09/40.47 (∀ (X : Iota), % 40.09/40.47 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 40.09/40.47 (p3 X))) % 40.09/40.47 (p4 Y)) % 40.09/40.47 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 40.09/40.47 (∀ (Y : Iota), % 40.09/40.47 Or % 40.09/40.47 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.09/40.48 (p3 Y)) % 40.09/40.48 (∀ (X : Iota), % 40.09/40.48 Or (Or (Not (r1 Y X)) (p4 X)) % 40.09/40.48 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 40.09/40.48 (∀ (Y : Iota), % 40.09/40.48 Or % 40.09/40.48 (Or % 40.09/40.48 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.09/40.48 (p3 Y)) % 40.09/40.48 (p4 Y)) % 40.09/40.48 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 40.09/40.48 (Not % 40.09/40.48 (Or % 40.09/40.48 (Or % 40.09/40.48 (∀ (Y : Iota), % 40.09/40.48 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 40.09/40.48 (∀ (Y : Iota), % 40.09/40.48 Or (Or (Not (r1 (skS.0 0 a) Y)) (p3 Y)) % 40.09/40.48 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 40.39/40.72 (p2 X))) % 40.39/40.72 (p3 Y)) % 40.39/40.72 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 40.39/40.72 (p2 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p3 X)) % 40.39/40.72 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 40.39/40.72 (p2 Y)) % 40.39/40.72 (p3 Y)) % 40.39/40.72 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) % 40.39/40.72 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) (p1 X))) % 40.39/40.72 (p2 Y)) % 40.39/40.72 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 40.39/40.72 (p1 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p2 X)) % 40.39/40.72 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 40.39/40.72 (p1 Y)) % 40.39/40.72 (p2 Y)) % 40.39/40.72 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))))))))) % 40.39/40.72 True % 40.39/40.72 Clause #4 (by clausification #[3]): ∀ (a : Iota), % 40.39/40.72 Eq % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.39/40.72 (p10 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p11 Y)) % 40.39/40.72 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 Y X)) % 40.39/40.72 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 40.39/40.72 (p10 X))) % 40.39/40.72 (p11 Y)) % 40.39/40.72 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.39/40.72 (p10 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p11 X)) % 40.39/40.72 (Not % 40.39/40.72 (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) (p10 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.39/40.72 (p10 Y)) % 40.39/40.72 (p11 Y)) % 40.39/40.72 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.39/40.72 (p9 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) % 40.39/40.72 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 Y X)) % 40.39/40.72 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 40.39/40.72 (p9 X))) % 40.39/40.72 (p10 Y)) % 40.39/40.72 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.39/40.72 (p9 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p10 X)) % 40.39/40.72 (Not (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) (p9 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.39/40.72 (p9 Y)) % 40.39/40.72 (p10 Y)) % 40.39/40.72 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.39/40.72 (p8 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p9 Y)) % 40.39/40.72 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 Y X)) % 40.39/40.72 (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 40.39/40.72 (p8 X))) % 40.39/40.72 (p9 Y)) % 40.39/40.72 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.39/40.72 (p8 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p9 X)) % 40.39/40.72 (Not (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.39/40.72 (p8 Y)) % 40.39/40.72 (p9 Y)) % 40.39/40.72 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.39/40.72 (p7 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p8 Y)) % 40.39/40.72 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 Y X)) % 40.39/40.72 (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 40.39/40.72 (p7 X))) % 40.39/40.72 (p8 Y)) % 40.39/40.72 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.39/40.72 (p7 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p8 X)) % 40.39/40.72 (Not (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.39/40.72 (p7 Y)) % 40.39/40.72 (p8 Y)) % 40.39/40.72 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.39/40.72 (p6 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p7 Y)) % 40.39/40.72 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Not (r1 Y X)) % 40.39/40.72 (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 40.39/40.72 (p6 X))) % 40.39/40.72 (p7 Y)) % 40.39/40.72 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.39/40.72 (p6 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p7 X)) % 40.39/40.72 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.39/40.72 (p6 Y)) % 40.39/40.72 (p7 Y)) % 40.39/40.72 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.39/40.72 (p5 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 40.39/40.72 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 40.39/40.72 (p5 X))) % 40.39/40.72 (p6 Y)) % 40.39/40.72 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.39/40.72 (p5 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p6 X)) % 40.39/40.72 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.39/40.72 (p5 Y)) % 40.39/40.72 (p6 Y)) % 40.39/40.72 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.39/40.72 (p4 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 40.39/40.72 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 40.39/40.72 (p4 X))) % 40.39/40.72 (p5 Y)) % 40.39/40.72 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.39/40.72 (p4 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p5 X)) % 40.39/40.72 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.39/40.72 (p4 Y)) % 40.39/40.72 (p5 Y)) % 40.39/40.72 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p4 Y)) % 40.39/40.72 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 40.39/40.72 (p3 X))) % 40.39/40.72 (p4 Y)) % 40.39/40.72 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.39/40.72 (p3 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p4 X)) % 40.39/40.72 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.39/40.72 (p3 Y)) % 40.39/40.72 (p4 Y)) % 40.39/40.72 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p3 Y)) % 40.39/40.72 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) (p2 X))) % 40.39/40.72 (p3 Y)) % 40.39/40.72 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 40.39/40.72 (p2 Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (p3 X)) % 40.39/40.72 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 40.39/40.72 (p2 Y)) % 40.39/40.72 (p3 Y)) % 40.39/40.72 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 40.39/40.72 (Not % 40.39/40.72 (Or % 40.39/40.72 (Or % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) % 40.39/40.72 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 40.39/40.72 (Not % 40.39/40.72 (And % 40.39/40.72 (And % 40.39/40.72 (∀ (Y : Iota), % 40.39/40.72 Or % 40.39/40.72 (Or % 40.39/40.72 (Or (Not (r1 (skS.0 0 a) Y)) % 40.39/40.72 (∀ (X : Iota), % 40.39/40.72 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) (p1 X))) % 40.59/40.94 (p2 Y)) % 40.59/40.94 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 40.59/40.94 (p1 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p2 X)) % 40.59/40.94 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 40.59/40.94 (p1 Y)) % 40.59/40.94 (p2 Y)) % 40.59/40.94 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))))))) % 40.59/40.94 False % 40.59/40.94 Clause #6 (by clausification #[4]): ∀ (a : Iota), % 40.59/40.94 Eq % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.59/40.94 (p10 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p11 Y)) % 40.59/40.94 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Not (r1 Y X)) % 40.59/40.94 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 40.59/40.94 (p10 X))) % 40.59/40.94 (p11 Y)) % 40.59/40.94 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.59/40.94 (p10 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p11 X)) % 40.59/40.94 (Not (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) (p10 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.59/40.94 (p10 Y)) % 40.59/40.94 (p11 Y)) % 40.59/40.94 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.59/40.94 (p9 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) % 40.59/40.94 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Not (r1 Y X)) % 40.59/40.94 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 40.59/40.94 (p9 X))) % 40.59/40.94 (p10 Y)) % 40.59/40.94 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.59/40.94 (p9 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p10 X)) % 40.59/40.94 (Not (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) (p9 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.59/40.94 (p9 Y)) % 40.59/40.94 (p10 Y)) % 40.59/40.94 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.59/40.94 (p8 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p9 Y)) % 40.59/40.94 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Not (r1 Y X)) % 40.59/40.94 (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 40.59/40.94 (p8 X))) % 40.59/40.94 (p9 Y)) % 40.59/40.94 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.59/40.94 (p8 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p9 X)) % 40.59/40.94 (Not (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.59/40.94 (p8 Y)) % 40.59/40.94 (p9 Y)) % 40.59/40.94 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.59/40.94 (p7 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p8 Y)) % 40.59/40.94 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Not (r1 Y X)) % 40.59/40.94 (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 40.59/40.94 (p7 X))) % 40.59/40.94 (p8 Y)) % 40.59/40.94 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.59/40.94 (p7 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p8 X)) % 40.59/40.94 (Not (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.59/40.94 (p7 Y)) % 40.59/40.94 (p8 Y)) % 40.59/40.94 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.59/40.94 (p6 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p7 Y)) % 40.59/40.94 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 40.59/40.94 (p6 X))) % 40.59/40.94 (p7 Y)) % 40.59/40.94 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.59/40.94 (p6 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p7 X)) % 40.59/40.94 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.59/40.94 (p6 Y)) % 40.59/40.94 (p7 Y)) % 40.59/40.94 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.59/40.94 (p5 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 40.59/40.94 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 40.59/40.94 (p5 X))) % 40.59/40.94 (p6 Y)) % 40.59/40.94 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.59/40.94 (p5 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p6 X)) % 40.59/40.94 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.59/40.94 (p5 Y)) % 40.59/40.94 (p6 Y)) % 40.59/40.94 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.59/40.94 (p4 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 40.59/40.94 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 40.59/40.94 (p4 X))) % 40.59/40.94 (p5 Y)) % 40.59/40.94 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.59/40.94 (p4 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p5 X)) % 40.59/40.94 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.59/40.94 (p4 Y)) % 40.59/40.94 (p5 Y)) % 40.59/40.94 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p4 Y)) % 40.59/40.94 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) (p3 X))) % 40.59/40.94 (p4 Y)) % 40.59/40.94 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.59/40.94 (p3 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p4 X)) % 40.59/40.94 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.59/40.94 (p3 Y)) % 40.59/40.94 (p4 Y)) % 40.59/40.94 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 40.59/40.94 (Not % 40.59/40.94 (Or % 40.59/40.94 (Or % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or (Or (Not (r1 (skS.0 0 a) Y)) (p3 Y)) % 40.59/40.94 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 40.59/40.94 (Not % 40.59/40.94 (And % 40.59/40.94 (And % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or % 40.59/40.94 (Or (Not (r1 (skS.0 0 a) Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) (p2 X))) % 40.59/40.94 (p3 Y)) % 40.59/40.94 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 40.59/40.94 (∀ (Y : Iota), % 40.59/40.94 Or % 40.59/40.94 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 40.59/40.94 (p2 Y)) % 40.59/40.94 (∀ (X : Iota), % 40.59/40.94 Or (Or (Not (r1 Y X)) (p3 X)) % 40.59/40.94 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 40.82/41.14 (p2 Y)) % 40.82/41.14 (p3 Y)) % 40.82/41.14 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 40.82/41.14 False % 40.82/41.14 Clause #78 (by clausification #[6]): ∀ (a : Iota), % 40.82/41.14 Eq % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.82/41.14 (p10 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p11 Y)) % 40.82/41.14 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (And % 40.82/41.14 (And % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or (Not (r1 Y X)) % 40.82/41.14 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 40.82/41.14 (p10 X))) % 40.82/41.14 (p11 Y)) % 40.82/41.14 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.82/41.14 (p10 Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (p11 X)) % 40.82/41.14 (Not (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) (p10 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.82/41.14 (p10 Y)) % 40.82/41.14 (p11 Y)) % 40.82/41.14 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))))))) % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.82/41.14 (p9 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) % 40.82/41.14 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (And % 40.82/41.14 (And % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or (Not (r1 Y X)) % 40.82/41.14 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 40.82/41.14 (p9 X))) % 40.82/41.14 (p10 Y)) % 40.82/41.14 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.82/41.14 (p9 Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (p10 X)) % 40.82/41.14 (Not (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) (p9 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.82/41.14 (p9 Y)) % 40.82/41.14 (p10 Y)) % 40.82/41.14 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.82/41.14 (p8 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p9 Y)) % 40.82/41.14 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (And % 40.82/41.14 (And % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or (Not (r1 Y X)) % 40.82/41.14 (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 40.82/41.14 (p8 X))) % 40.82/41.14 (p9 Y)) % 40.82/41.14 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.82/41.14 (p8 Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (p9 X)) % 40.82/41.14 (Not (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.82/41.14 (p8 Y)) % 40.82/41.14 (p9 Y)) % 40.82/41.14 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.82/41.14 (p7 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p8 Y)) % 40.82/41.14 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (And % 40.82/41.14 (And % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 40.82/41.14 (p7 X))) % 40.82/41.14 (p8 Y)) % 40.82/41.14 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.82/41.14 (p7 Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (p8 X)) % 40.82/41.14 (Not (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.82/41.14 (p7 Y)) % 40.82/41.14 (p8 Y)) % 40.82/41.14 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.82/41.14 (p6 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p7 Y)) % 40.82/41.14 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (And % 40.82/41.14 (And % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 40.82/41.14 (p6 X))) % 40.82/41.14 (p7 Y)) % 40.82/41.14 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.82/41.14 (p6 Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (p7 X)) % 40.82/41.14 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.82/41.14 (p6 Y)) % 40.82/41.14 (p7 Y)) % 40.82/41.14 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.82/41.14 (p5 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 40.82/41.14 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (And % 40.82/41.14 (And % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 40.82/41.14 (p5 X))) % 40.82/41.14 (p6 Y)) % 40.82/41.14 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.82/41.14 (p5 Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (p6 X)) % 40.82/41.14 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.82/41.14 (p5 Y)) % 40.82/41.14 (p6 Y)) % 40.82/41.14 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 40.82/41.14 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (And % 40.82/41.14 (And % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Not (r1 (skS.0 0 a) Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 40.82/41.14 (p4 X))) % 40.82/41.14 (p5 Y)) % 40.82/41.14 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.82/41.14 (p4 Y)) % 40.82/41.14 (∀ (X : Iota), % 40.82/41.14 Or (Or (Not (r1 Y X)) (p5 X)) % 40.82/41.14 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or % 40.82/41.14 (Or % 40.82/41.14 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.82/41.14 (p4 Y)) % 40.82/41.14 (p5 Y)) % 40.82/41.14 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.82/41.14 (Not % 40.82/41.14 (Or % 40.82/41.14 (Or % 40.82/41.14 (∀ (Y : Iota), % 40.82/41.14 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 40.82/41.14 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p4 Y)) % 40.99/41.31 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) (p3 X))) % 40.99/41.31 (p4 Y)) % 40.99/41.31 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.99/41.31 (p3 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p4 X)) % 40.99/41.31 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 40.99/41.31 (p3 Y)) % 40.99/41.31 (p4 Y)) % 40.99/41.31 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 40.99/41.31 False % 40.99/41.31 Clause #389 (by clausification #[78]): ∀ (a : Iota), % 40.99/41.31 Eq % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Not % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.99/41.31 (p10 Y)) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p11 Y)) % 40.99/41.31 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or (Not (r1 Y X)) % 40.99/41.31 (Not (And (p11 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p11 Y))))) % 40.99/41.31 (p10 X))) % 40.99/41.31 (p11 Y)) % 40.99/41.31 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.99/41.31 (p10 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p11 X)) % 40.99/41.31 (Not (And (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))) (p10 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p11 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p11 X))))) % 40.99/41.31 (p10 Y)) % 40.99/41.31 (p11 Y)) % 40.99/41.31 (Not (And (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))) (p10 Y)))))))) % 40.99/41.31 (Not % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.99/41.31 (p9 Y)) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) % 40.99/41.31 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or (Not (r1 Y X)) % 40.99/41.31 (Not (And (p10 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p10 Y))))) % 40.99/41.31 (p9 X))) % 40.99/41.31 (p10 Y)) % 40.99/41.31 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.99/41.31 (p9 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p10 X)) % 40.99/41.31 (Not (And (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))) (p9 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p10 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X))))) % 40.99/41.31 (p9 Y)) % 40.99/41.31 (p10 Y)) % 40.99/41.31 (Not (And (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))) (p9 Y))))))))) % 40.99/41.31 (Not % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.99/41.31 (p8 Y)) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p9 Y)) % 40.99/41.31 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (Not (And (p9 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p9 Y))))) % 40.99/41.31 (p8 X))) % 40.99/41.31 (p9 Y)) % 40.99/41.31 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.99/41.31 (p8 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p9 X)) % 40.99/41.31 (Not (And (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))) (p8 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p9 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p9 X))))) % 40.99/41.31 (p8 Y)) % 40.99/41.31 (p9 Y)) % 40.99/41.31 (Not (And (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))) (p8 Y))))))))) % 40.99/41.31 (Not % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.99/41.31 (p7 Y)) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p8 Y)) % 40.99/41.31 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (Not (And (p8 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p8 Y))))) % 40.99/41.31 (p7 X))) % 40.99/41.31 (p8 Y)) % 40.99/41.31 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.99/41.31 (p7 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p8 X)) % 40.99/41.31 (Not (And (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))) (p7 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (Not (And (p8 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p8 X))))) % 40.99/41.31 (p7 Y)) % 40.99/41.31 (p8 Y)) % 40.99/41.31 (Not (And (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))) (p7 Y))))))))) % 40.99/41.31 (Not % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.99/41.31 (p6 Y)) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p7 Y)) % 40.99/41.31 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (Not (And (p7 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p7 Y))))) % 40.99/41.31 (p6 X))) % 40.99/41.31 (p7 Y)) % 40.99/41.31 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.99/41.31 (p6 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p7 X)) % 40.99/41.31 (Not (And (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))) (p6 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p7 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p7 X))))) % 40.99/41.31 (p6 Y)) % 40.99/41.31 (p7 Y)) % 40.99/41.31 (Not (And (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))) (p6 Y))))))))) % 40.99/41.31 (Not % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) (p5 Y)) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 40.99/41.31 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 40.99/41.31 (p5 X))) % 40.99/41.31 (p6 Y)) % 40.99/41.31 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.99/41.31 (p5 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p6 X)) % 40.99/41.31 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 40.99/41.31 (p5 Y)) % 40.99/41.31 (p6 Y)) % 40.99/41.31 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))))))) % 40.99/41.31 (Not % 40.99/41.31 (Or % 40.99/41.31 (Or % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 40.99/41.31 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 40.99/41.31 (Not % 40.99/41.31 (And % 40.99/41.31 (And % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Not (r1 (skS.0 0 a) Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 40.99/41.31 (p4 X))) % 40.99/41.31 (p5 Y)) % 40.99/41.31 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.99/41.31 (p4 Y)) % 40.99/41.31 (∀ (X : Iota), % 40.99/41.31 Or (Or (Not (r1 Y X)) (p5 X)) % 40.99/41.31 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or % 40.99/41.31 (Or % 40.99/41.31 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 40.99/41.31 (p4 Y)) % 40.99/41.31 (p5 Y)) % 40.99/41.31 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.99/41.31 (∀ (Y : Iota), % 40.99/41.31 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y))))) % 40.99/41.31 False % 40.99/41.31 Clause #1406 (by clausification #[389]): ∀ (a : Iota), % 40.99/41.39 Eq % 40.99/41.39 (∀ (Y : Iota), % 40.99/41.39 Or (Or (Not (r1 (skS.0 0 a) Y)) (p10 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p10 X)) (p10 Y)))) % 40.99/41.39 False % 40.99/41.39 Clause #1408 (by clausification #[1406]): ∀ (a a_1 : Iota), % 40.99/41.39 Eq % 40.99/41.39 (Not % 40.99/41.39 (Or (Or (Not (r1 (skS.0 0 a) (skS.0 47 a a_1))) (p10 (skS.0 47 a a_1))) % 40.99/41.39 (Not (And (∀ (X : Iota), Or (Not (r1 (skS.0 47 a a_1) X)) (p10 X)) (p10 (skS.0 47 a a_1)))))) % 40.99/41.39 True % 40.99/41.39 Clause #1409 (by clausification #[1408]): ∀ (a a_1 : Iota), % 40.99/41.39 Eq % 40.99/41.39 (Or (Or (Not (r1 (skS.0 0 a) (skS.0 47 a a_1))) (p10 (skS.0 47 a a_1))) % 40.99/41.39 (Not (And (∀ (X : Iota), Or (Not (r1 (skS.0 47 a a_1) X)) (p10 X)) (p10 (skS.0 47 a a_1))))) % 40.99/41.39 False % 40.99/41.39 Clause #1410 (by clausification #[1409]): ∀ (a a_1 : Iota), Eq (Not (And (∀ (X : Iota), Or (Not (r1 (skS.0 47 a a_1) X)) (p10 X)) (p10 (skS.0 47 a a_1)))) False % 40.99/41.39 Clause #1411 (by clausification #[1409]): ∀ (a a_1 : Iota), Eq (Or (Not (r1 (skS.0 0 a) (skS.0 47 a a_1))) (p10 (skS.0 47 a a_1))) False % 40.99/41.39 Clause #1412 (by clausification #[1410]): ∀ (a a_1 : Iota), Eq (And (∀ (X : Iota), Or (Not (r1 (skS.0 47 a a_1) X)) (p10 X)) (p10 (skS.0 47 a a_1))) True % 40.99/41.39 Clause #1413 (by clausification #[1412]): ∀ (a a_1 : Iota), Eq (p10 (skS.0 47 a a_1)) True % 40.99/41.39 Clause #1418 (by clausification #[1411]): ∀ (a a_1 : Iota), Eq (p10 (skS.0 47 a a_1)) False % 40.99/41.39 Clause #1420 (by superposition #[1418, 1413]): Eq False True % 40.99/41.39 Clause #1421 (by clausification #[1420]): False % 40.99/41.39 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------