%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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 8.89s 9.14s % Output : Proof 9.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : duper %s % 0.09/0.35 % Computer : n029.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 5 07:09:55 UTC 2026 % 0.09/0.36 % CPUTime : % 8.89/9.14 SZS status Theorem for theBenchmark.p % 8.89/9.14 SZS output start Proof for theBenchmark.p % 8.89/9.14 Clause #0 (by assumption #[]): Eq % 8.89/9.14 (Not % 8.89/9.14 (Not % 8.89/9.14 (Exists fun X => % 8.89/9.14 Not % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (Not % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) (p5 Y)) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (p6 Y)) % 8.89/9.14 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 8.89/9.14 (Not % 8.89/9.14 (And % 8.89/9.14 (And % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or % 8.89/9.14 (Or (Not (r1 X Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or (Not (r1 Y X)) % 8.89/9.14 (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 8.89/9.14 (p5 X))) % 8.89/9.14 (p6 Y)) % 8.89/9.14 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 8.89/9.14 (p5 Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or (Or (Not (r1 Y X)) (p6 X)) % 8.89/9.14 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or % 8.89/9.14 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 8.89/9.14 (p5 Y)) % 8.89/9.14 (p6 Y)) % 8.89/9.14 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))))))) % 8.89/9.14 (Not % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (p5 Y)) % 8.89/9.14 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 8.89/9.14 (Not % 8.89/9.14 (And % 8.89/9.14 (And % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or % 8.89/9.14 (Or (Not (r1 X Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or (Not (r1 Y X)) % 8.89/9.14 (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 8.89/9.14 (p4 X))) % 8.89/9.14 (p5 Y)) % 8.89/9.14 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 8.89/9.14 (p4 Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or (Or (Not (r1 Y X)) (p5 X)) % 8.89/9.14 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or % 8.89/9.14 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 8.89/9.14 (p4 Y)) % 8.89/9.14 (p5 Y)) % 8.89/9.14 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 8.89/9.14 (Not % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (p4 Y)) % 8.89/9.14 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 8.89/9.14 (Not % 8.89/9.14 (And % 8.89/9.14 (And % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or % 8.89/9.14 (Or (Not (r1 X Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or (Not (r1 Y X)) % 8.89/9.14 (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 8.89/9.14 (p3 X))) % 8.89/9.14 (p4 Y)) % 8.89/9.14 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 8.89/9.14 (p3 Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or (Or (Not (r1 Y X)) (p4 X)) % 8.89/9.14 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or % 8.89/9.14 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 8.89/9.14 (p3 Y)) % 8.89/9.14 (p4 Y)) % 8.89/9.14 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 8.89/9.14 (Not % 8.89/9.14 (Or % 8.89/9.14 (Or % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or (Or (Not (r1 X Y)) (p3 Y)) % 8.89/9.14 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 8.89/9.14 (Not % 8.89/9.14 (And % 8.89/9.14 (And % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or % 8.89/9.14 (Or (Not (r1 X Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 8.89/9.14 (p2 X))) % 8.89/9.14 (p3 Y)) % 8.89/9.14 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 8.89/9.14 (∀ (Y : Iota), % 8.89/9.14 Or % 8.89/9.14 (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 8.89/9.14 (p2 Y)) % 8.89/9.14 (∀ (X : Iota), % 8.89/9.14 Or (Or (Not (r1 Y X)) (p3 X)) % 8.89/9.14 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 8.96/9.25 (p2 Y)) % 8.96/9.25 (p3 Y)) % 8.96/9.25 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 8.96/9.25 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (p2 Y)) % 8.96/9.25 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (And % 8.96/9.25 (And % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Not (r1 X Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) % 8.96/9.25 (p1 X))) % 8.96/9.25 (p2 Y)) % 8.96/9.25 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (p2 X)) % 8.96/9.25 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 8.96/9.25 (p2 Y)) % 8.96/9.25 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))))))))))) % 8.96/9.25 True % 8.96/9.25 Clause #1 (by clausification #[0]): Eq % 8.96/9.25 (Not % 8.96/9.25 (Exists fun X => % 8.96/9.25 Not % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (Not % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) (p5 Y)) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (p6 Y)) % 8.96/9.25 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (And % 8.96/9.25 (And % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Not (r1 X Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Not (r1 Y X)) % 8.96/9.25 (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 8.96/9.25 (p5 X))) % 8.96/9.25 (p6 Y)) % 8.96/9.25 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 8.96/9.25 (p5 Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (p6 X)) % 8.96/9.25 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 8.96/9.25 (p5 Y)) % 8.96/9.25 (p6 Y)) % 8.96/9.25 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))))))) % 8.96/9.25 (Not % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (p5 Y)) % 8.96/9.25 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (And % 8.96/9.25 (And % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Not (r1 X Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Not (r1 Y X)) % 8.96/9.25 (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 8.96/9.25 (p4 X))) % 8.96/9.25 (p5 Y)) % 8.96/9.25 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 8.96/9.25 (p4 Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (p5 X)) % 8.96/9.25 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 8.96/9.25 (p4 Y)) % 8.96/9.25 (p5 Y)) % 8.96/9.25 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 8.96/9.25 (Not % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (p4 Y)) % 8.96/9.25 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (And % 8.96/9.25 (And % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Not (r1 X Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 8.96/9.25 (p3 X))) % 8.96/9.25 (p4 Y)) % 8.96/9.25 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 8.96/9.25 (p3 Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (p4 X)) % 8.96/9.25 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 8.96/9.25 (p3 Y)) % 8.96/9.25 (p4 Y)) % 8.96/9.25 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 8.96/9.25 (Not % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (p3 Y)) % 8.96/9.25 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (And % 8.96/9.25 (And % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Not (r1 X Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 8.96/9.25 (p2 X))) % 8.96/9.25 (p3 Y)) % 8.96/9.25 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 8.96/9.25 (p2 Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (p3 X)) % 8.96/9.25 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 8.96/9.25 (p2 Y)) % 8.96/9.25 (p3 Y)) % 8.96/9.25 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 8.96/9.25 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 8.96/9.25 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (Or % 8.96/9.25 (Or % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Not (r1 X Y)) (p2 Y)) % 8.96/9.25 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 8.96/9.25 (Not % 8.96/9.25 (And % 8.96/9.25 (And % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or % 8.96/9.25 (Or (Not (r1 X Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) % 8.96/9.25 (p1 X))) % 8.96/9.25 (p2 Y)) % 8.96/9.25 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 8.96/9.25 (∀ (X : Iota), % 8.96/9.25 Or (Or (Not (r1 Y X)) (p2 X)) % 8.96/9.25 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 8.96/9.25 (∀ (Y : Iota), % 8.96/9.25 Or % 8.96/9.25 (Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 9.06/9.36 (p2 Y)) % 9.06/9.36 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))))))))) % 9.06/9.36 False % 9.06/9.36 Clause #2 (by clausification #[1]): Eq % 9.06/9.36 (Exists fun X => % 9.06/9.36 Not % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (Not % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) (p5 Y)) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (p6 Y)) % 9.06/9.36 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 9.06/9.36 (Not % 9.06/9.36 (And % 9.06/9.36 (And % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Not (r1 X Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 9.06/9.36 (p5 X))) % 9.06/9.36 (p6 Y)) % 9.06/9.36 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.06/9.36 (p5 Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (p6 X)) % 9.06/9.36 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Or (Not (r1 X Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.06/9.36 (p5 Y)) % 9.06/9.36 (p6 Y)) % 9.06/9.36 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))))))) % 9.06/9.36 (Not % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) (p4 Y)) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (p5 Y)) % 9.06/9.36 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 9.06/9.36 (Not % 9.06/9.36 (And % 9.06/9.36 (And % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Not (r1 X Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 9.06/9.36 (p4 X))) % 9.06/9.36 (p5 Y)) % 9.06/9.36 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.06/9.36 (p4 Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (p5 X)) % 9.06/9.36 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Or (Not (r1 X Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.06/9.36 (p4 Y)) % 9.06/9.36 (p5 Y)) % 9.06/9.36 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 9.06/9.36 (Not % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (p4 Y)) % 9.06/9.36 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 9.06/9.36 (Not % 9.06/9.36 (And % 9.06/9.36 (And % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Not (r1 X Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 9.06/9.36 (p3 X))) % 9.06/9.36 (p4 Y)) % 9.06/9.36 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.06/9.36 (p3 Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (p4 X)) % 9.06/9.36 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Or (Not (r1 X Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.06/9.36 (p3 Y)) % 9.06/9.36 (p4 Y)) % 9.06/9.36 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 9.06/9.36 (Not % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Not (r1 X Y)) (p3 Y)) % 9.06/9.36 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 9.06/9.36 (Not % 9.06/9.36 (And % 9.06/9.36 (And % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Not (r1 X Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 9.06/9.36 (p2 X))) % 9.06/9.36 (p3 Y)) % 9.06/9.36 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 9.06/9.36 (∀ (X : Iota), % 9.06/9.36 Or (Or (Not (r1 Y X)) (p3 X)) % 9.06/9.36 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 9.06/9.36 (∀ (Y : Iota), % 9.06/9.36 Or % 9.06/9.36 (Or % 9.06/9.36 (Or (Or (Not (r1 X Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 9.06/9.36 (p3 Y)) % 9.06/9.36 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 9.06/9.36 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.06/9.36 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.06/9.36 (Not % 9.06/9.36 (Or % 9.06/9.36 (Or % 9.06/9.36 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.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))))) % 9.16/9.47 (Not % 9.16/9.47 (And % 9.16/9.47 (And % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or % 9.16/9.47 (Or (Not (r1 X Y)) % 9.16/9.47 (∀ (X : Iota), % 9.16/9.47 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) (p1 X))) % 9.16/9.47 (p2 Y)) % 9.16/9.47 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 9.16/9.47 (∀ (X : Iota), % 9.16/9.47 Or (Or (Not (r1 Y X)) (p2 X)) % 9.16/9.47 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or (Or (Or (Not (r1 X Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 9.16/9.47 (p2 Y)) % 9.16/9.47 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))))))))) % 9.16/9.47 True % 9.16/9.47 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 9.16/9.47 Eq % 9.16/9.47 (Not % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (Not % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.16/9.47 (p5 Y)) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 9.16/9.47 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 9.16/9.47 (Not % 9.16/9.47 (And % 9.16/9.47 (And % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or % 9.16/9.47 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.47 (∀ (X : Iota), % 9.16/9.47 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 9.16/9.47 (p5 X))) % 9.16/9.47 (p6 Y)) % 9.16/9.47 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or % 9.16/9.47 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.47 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.16/9.47 (p5 Y)) % 9.16/9.47 (∀ (X : Iota), % 9.16/9.47 Or (Or (Not (r1 Y X)) (p6 X)) % 9.16/9.47 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.47 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.16/9.47 (p5 Y)) % 9.16/9.47 (p6 Y)) % 9.16/9.47 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))))))) % 9.16/9.47 (Not % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.16/9.47 (p4 Y)) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 9.16/9.47 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 9.16/9.47 (Not % 9.16/9.47 (And % 9.16/9.47 (And % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or % 9.16/9.47 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.47 (∀ (X : Iota), % 9.16/9.47 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 9.16/9.47 (p4 X))) % 9.16/9.47 (p5 Y)) % 9.16/9.47 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or % 9.16/9.47 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.47 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.16/9.47 (p4 Y)) % 9.16/9.47 (∀ (X : Iota), % 9.16/9.47 Or (Or (Not (r1 Y X)) (p5 X)) % 9.16/9.47 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.47 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.16/9.47 (p4 Y)) % 9.16/9.47 (p5 Y)) % 9.16/9.47 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 9.16/9.47 (Not % 9.16/9.47 (Or % 9.16/9.47 (Or % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.16/9.47 (p3 Y)) % 9.16/9.47 (∀ (Y : Iota), % 9.16/9.47 Or (Or (Not (r1 (skS.0 0 a) Y)) (p4 Y)) % 9.16/9.48 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 9.16/9.48 (Not % 9.16/9.48 (And % 9.16/9.48 (And % 9.16/9.48 (∀ (Y : Iota), % 9.16/9.48 Or % 9.16/9.48 (Or % 9.16/9.48 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.48 (∀ (X : Iota), % 9.16/9.48 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 9.16/9.48 (p3 X))) % 9.16/9.48 (p4 Y)) % 9.16/9.48 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 9.16/9.48 (∀ (Y : Iota), % 9.16/9.48 Or % 9.16/9.48 (Or % 9.16/9.48 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.48 (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.16/9.48 (p3 Y)) % 9.16/9.48 (∀ (X : Iota), % 9.16/9.48 Or (Or (Not (r1 Y X)) (p4 X)) % 9.16/9.48 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 9.16/9.48 (∀ (Y : Iota), % 9.16/9.48 Or % 9.16/9.48 (Or % 9.16/9.48 (Or % 9.16/9.48 (Or (Not (r1 (skS.0 0 a) Y)) % 9.16/9.48 (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.16/9.48 (p3 Y)) % 9.16/9.48 (p4 Y)) % 9.16/9.48 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 9.16/9.48 (Not % 9.16/9.48 (Or % 9.16/9.48 (Or % 9.16/9.48 (∀ (Y : Iota), % 9.16/9.48 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 9.16/9.48 (p2 Y)) % 9.16/9.48 (∀ (Y : Iota), % 9.16/9.48 Or (Or (Not (r1 (skS.0 0 a) Y)) (p3 Y)) % 9.26/9.59 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (And % 9.26/9.59 (And % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 9.26/9.59 (p2 X))) % 9.26/9.59 (p3 Y)) % 9.26/9.59 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 9.26/9.59 (p2 Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (p3 X)) % 9.26/9.59 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 9.26/9.59 (p2 Y)) % 9.26/9.59 (p3 Y)) % 9.26/9.59 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) % 9.26/9.59 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (And % 9.26/9.59 (And % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) (p1 X))) % 9.26/9.59 (p2 Y)) % 9.26/9.59 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 9.26/9.59 (p1 Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (p2 X)) % 9.26/9.59 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 9.26/9.59 (p1 Y)) % 9.26/9.59 (p2 Y)) % 9.26/9.59 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))))))))) % 9.26/9.59 True % 9.26/9.59 Clause #4 (by clausification #[3]): ∀ (a : Iota), % 9.26/9.59 Eq % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Not % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.26/9.59 (p5 Y)) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 9.26/9.59 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (And % 9.26/9.59 (And % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 9.26/9.59 (p5 X))) % 9.26/9.59 (p6 Y)) % 9.26/9.59 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.26/9.59 (p5 Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (p6 X)) % 9.26/9.59 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.26/9.59 (p5 Y)) % 9.26/9.59 (p6 Y)) % 9.26/9.59 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))))))) % 9.26/9.59 (Not % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.26/9.59 (p4 Y)) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 9.26/9.59 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (And % 9.26/9.59 (And % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 9.26/9.59 (p4 X))) % 9.26/9.59 (p5 Y)) % 9.26/9.59 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.26/9.59 (p4 Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (p5 X)) % 9.26/9.59 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.26/9.59 (p4 Y)) % 9.26/9.59 (p5 Y)) % 9.26/9.59 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 9.26/9.59 (Not % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.26/9.59 (p3 Y)) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p4 Y)) % 9.26/9.59 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (And % 9.26/9.59 (And % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 9.26/9.59 (p3 X))) % 9.26/9.59 (p4 Y)) % 9.26/9.59 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.26/9.59 (p3 Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (p4 X)) % 9.26/9.59 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.26/9.59 (p3 Y)) % 9.26/9.59 (p4 Y)) % 9.26/9.59 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 9.26/9.59 (Not % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p3 Y)) % 9.26/9.59 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (And % 9.26/9.59 (And % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Not (r1 (skS.0 0 a) Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 9.26/9.59 (p2 X))) % 9.26/9.59 (p3 Y)) % 9.26/9.59 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 9.26/9.59 (p2 Y)) % 9.26/9.59 (∀ (X : Iota), % 9.26/9.59 Or (Or (Not (r1 Y X)) (p3 X)) % 9.26/9.59 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or % 9.26/9.59 (Or % 9.26/9.59 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 9.26/9.59 (p2 Y)) % 9.26/9.59 (p3 Y)) % 9.26/9.59 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (Or % 9.26/9.59 (Or % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) (p1 Y)) % 9.26/9.59 (∀ (Y : Iota), % 9.26/9.59 Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) % 9.26/9.59 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))) % 9.26/9.59 (Not % 9.26/9.59 (And % 9.36/9.68 (And % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (Not (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))))) (p1 X))) % 9.36/9.68 (p2 Y)) % 9.36/9.68 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y)))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 9.36/9.68 (p1 Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (p2 X)) % 9.36/9.68 (Not (And (And (p1 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) (p1 X)))))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))))) % 9.36/9.68 (p1 Y)) % 9.36/9.68 (p2 Y)) % 9.36/9.68 (Not (And (And (p1 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))) (p1 Y))))))))) % 9.36/9.68 False % 9.36/9.68 Clause #6 (by clausification #[4]): ∀ (a : Iota), % 9.36/9.68 Eq % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (Not % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.36/9.68 (p5 Y)) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (p6 Y)) % 9.36/9.68 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y))))) % 9.36/9.68 (Not % 9.36/9.68 (And % 9.36/9.68 (And % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (Not (And (p6 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p6 Y))))) % 9.36/9.68 (p5 X))) % 9.36/9.68 (p6 Y)) % 9.36/9.68 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.36/9.68 (p5 Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (p6 X)) % 9.36/9.68 (Not (And (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) (p5 X)))))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p6 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p6 X))))) % 9.36/9.68 (p5 Y)) % 9.36/9.68 (p6 Y)) % 9.36/9.68 (Not (And (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))) (p5 Y)))))))) % 9.36/9.68 (Not % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.36/9.68 (p4 Y)) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) % 9.36/9.68 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))) % 9.36/9.68 (Not % 9.36/9.68 (And % 9.36/9.68 (And % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (Not (And (p5 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))))) % 9.36/9.68 (p4 X))) % 9.36/9.68 (p5 Y)) % 9.36/9.68 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y)))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.36/9.68 (p4 Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (p5 X)) % 9.36/9.68 (Not (And (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))) (p4 X)))))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p5 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X))))) % 9.36/9.68 (p4 Y)) % 9.36/9.68 (p5 Y)) % 9.36/9.68 (Not (And (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) (p4 Y))))))))) % 9.36/9.68 (Not % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) (p3 Y)) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (p4 Y)) % 9.36/9.68 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))) % 9.36/9.68 (Not % 9.36/9.68 (And % 9.36/9.68 (And % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (Not (And (p4 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p4 Y))))) % 9.36/9.68 (p3 X))) % 9.36/9.68 (p4 Y)) % 9.36/9.68 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y)))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.36/9.68 (p3 Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (p4 X)) % 9.36/9.68 (Not (And (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) (p3 X)))))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p4 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))))) % 9.36/9.68 (p3 Y)) % 9.36/9.68 (p4 Y)) % 9.36/9.68 (Not (And (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))) (p3 Y))))))))) % 9.36/9.68 (Not % 9.36/9.68 (Or % 9.36/9.68 (Or % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) (p2 Y)) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (p3 Y)) % 9.36/9.68 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))) % 9.36/9.68 (Not % 9.36/9.68 (And % 9.36/9.68 (And % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or % 9.36/9.68 (Or (Not (r1 (skS.0 0 a) Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (Not (And (p3 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))))) % 9.36/9.68 (p2 X))) % 9.36/9.68 (p3 Y)) % 9.36/9.68 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y)))) % 9.36/9.68 (∀ (Y : Iota), % 9.36/9.68 Or % 9.36/9.68 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 9.36/9.68 (p2 Y)) % 9.36/9.68 (∀ (X : Iota), % 9.36/9.68 Or (Or (Not (r1 Y X)) (p3 X)) % 9.46/9.71 (Not (And (And (p2 X) (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) (p2 X)))))) % 9.46/9.71 (∀ (Y : Iota), % 9.46/9.71 Or % 9.46/9.71 (Or % 9.46/9.71 (Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (And (p3 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p3 X))))) % 9.46/9.71 (p2 Y)) % 9.46/9.71 (p3 Y)) % 9.46/9.71 (Not (And (And (p2 Y) (∀ (X : Iota), Or (Not (r1 Y X)) (p2 X))) (p2 Y))))))))) % 9.46/9.71 (∀ (Y : Iota), % 9.46/9.71 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.46/9.71 (∀ (Y : Iota), % 9.46/9.71 Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y))))) % 9.46/9.71 False % 9.46/9.71 Clause #77 (by clausification #[6]): ∀ (a : Iota), % 9.46/9.71 Eq (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p5 Y)) (Not (And (∀ (X : Iota), Or (Not (r1 Y X)) (p5 X)) (p5 Y)))) % 9.46/9.71 False % 9.46/9.71 Clause #79 (by clausification #[77]): ∀ (a a_1 : Iota), % 9.46/9.71 Eq % 9.46/9.71 (Not % 9.46/9.71 (Or (Or (Not (r1 (skS.0 0 a) (skS.0 7 a a_1))) (p5 (skS.0 7 a a_1))) % 9.46/9.71 (Not (And (∀ (X : Iota), Or (Not (r1 (skS.0 7 a a_1) X)) (p5 X)) (p5 (skS.0 7 a a_1)))))) % 9.46/9.71 True % 9.46/9.71 Clause #80 (by clausification #[79]): ∀ (a a_1 : Iota), % 9.46/9.71 Eq % 9.46/9.71 (Or (Or (Not (r1 (skS.0 0 a) (skS.0 7 a a_1))) (p5 (skS.0 7 a a_1))) % 9.46/9.71 (Not (And (∀ (X : Iota), Or (Not (r1 (skS.0 7 a a_1) X)) (p5 X)) (p5 (skS.0 7 a a_1))))) % 9.46/9.71 False % 9.46/9.71 Clause #81 (by clausification #[80]): ∀ (a a_1 : Iota), Eq (Not (And (∀ (X : Iota), Or (Not (r1 (skS.0 7 a a_1) X)) (p5 X)) (p5 (skS.0 7 a a_1)))) False % 9.46/9.71 Clause #82 (by clausification #[80]): ∀ (a a_1 : Iota), Eq (Or (Not (r1 (skS.0 0 a) (skS.0 7 a a_1))) (p5 (skS.0 7 a a_1))) False % 9.46/9.71 Clause #83 (by clausification #[81]): ∀ (a a_1 : Iota), Eq (And (∀ (X : Iota), Or (Not (r1 (skS.0 7 a a_1) X)) (p5 X)) (p5 (skS.0 7 a a_1))) True % 9.46/9.71 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), Eq (p5 (skS.0 7 a a_1)) True % 9.46/9.71 Clause #89 (by clausification #[82]): ∀ (a a_1 : Iota), Eq (p5 (skS.0 7 a a_1)) False % 9.46/9.71 Clause #91 (by superposition #[89, 84]): Eq False True % 9.46/9.71 Clause #92 (by clausification #[91]): False % 9.46/9.71 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------