%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:36:15 AM UTC 2026 % Result : Theorem 16.78s 17.10s % Output : Proof 17.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : duper %s % 0.12/0.37 % Computer : n013.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Sat Sep 5 19:59:20 UTC 2026 % 0.12/0.37 % CPUTime : % 16.78/17.10 SZS status Theorem for theBenchmark.p % 16.78/17.10 SZS output start Proof for theBenchmark.p % 16.78/17.10 Clause #0 (by assumption #[]): Eq % 16.78/17.10 (Not % 16.78/17.10 (Not % 16.78/17.10 (Exists fun X => % 16.78/17.10 Not % 16.78/17.10 (Or % 16.78/17.10 (Or % 16.78/17.10 (Or % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 16.78/17.10 (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) % 16.78/17.10 (Not % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (Not % 16.78/17.10 (Or % 16.78/17.10 (Or % 16.78/17.10 (Not % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.78/17.10 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.78/17.10 (Not % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (Not % 16.78/17.10 (Or % 16.78/17.10 (Or % 16.78/17.10 (Not % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.78/17.10 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.78/17.10 (Not % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (Not % 16.78/17.10 (Not % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (Not % 16.78/17.10 (Or (And (Not (p1 X)) (Not (p2 X))) % 16.78/17.10 (And (p2 X) (p1 X)))))))))))))))))) % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (p4 X) (p3 X)) (p2 X)) (p1 X)))))))))) % 16.78/17.10 True % 16.78/17.10 Clause #1 (by clausification #[0]): Eq % 16.78/17.10 (Not % 16.78/17.10 (Exists fun X => % 16.78/17.10 Not % 16.78/17.10 (Or % 16.78/17.10 (Or % 16.78/17.10 (Or % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 16.78/17.10 (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) % 16.78/17.10 (Not % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (Not % 16.78/17.10 (Or % 16.78/17.10 (Or % 16.78/17.10 (Not % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) % 16.78/17.10 (∀ (Y : Iota), % 16.78/17.10 Or (Not (r1 X Y)) % 16.78/17.10 (∀ (X : Iota), % 16.78/17.10 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.78/17.10 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.88/17.15 (Not % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (Not % 16.88/17.15 (Or % 16.88/17.15 (Or % 16.88/17.15 (Not % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.88/17.15 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.88/17.15 (Not % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (Not % 16.88/17.15 (Not % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (Not % 16.88/17.15 (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))))))) % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (p4 X) (p3 X)) (p2 X)) (p1 X))))))))) % 16.88/17.15 False % 16.88/17.15 Clause #2 (by clausification #[1]): Eq % 16.88/17.15 (Exists fun X => % 16.88/17.15 Not % 16.88/17.15 (Or % 16.88/17.15 (Or % 16.88/17.15 (Or % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 16.88/17.15 (∀ (Y : Iota), Or (Not (r1 X Y)) (p5 Y))) % 16.88/17.15 (Not % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (Not % 16.88/17.15 (Or % 16.88/17.15 (Or % 16.88/17.15 (Not % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.88/17.15 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.88/17.15 (Not % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (Not % 16.88/17.15 (Or % 16.88/17.15 (Or % 16.88/17.15 (Not % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.88/17.15 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.88/17.15 (Not % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (Not % 16.88/17.15 (Not % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))))))) % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) % 16.88/17.15 (∀ (X : Iota), % 16.88/17.15 Or (Not (r1 Y X)) % 16.88/17.15 (∀ (Y : Iota), % 16.88/17.15 Or (Not (r1 X Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (p4 X) (p3 X)) (p2 X)) (p1 X)))))))) % 16.88/17.15 True % 16.88/17.15 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 16.88/17.18 Eq % 16.88/17.18 (Not % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 (skS.0 0 a) Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 16.88/17.18 (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p5 Y))) % 16.88/17.18 (Not % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 (skS.0 0 a) Y)) % 16.88/17.18 (Not % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (Not % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.88/17.18 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.88/17.18 (Not % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (Not % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (Not % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.88/17.18 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.88/17.18 (Not % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) % 16.88/17.18 (Not % 16.88/17.18 (Not % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))))))) % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 (skS.0 0 a) Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (p4 X) (p3 X)) (p2 X)) (p1 X)))))))) % 16.88/17.18 True % 16.88/17.18 Clause #4 (by clausification #[3]): ∀ (a : Iota), % 16.88/17.18 Eq % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 (skS.0 0 a) Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 16.88/17.18 (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p5 Y))) % 16.88/17.18 (Not % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 (skS.0 0 a) Y)) % 16.88/17.18 (Not % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (Not % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.88/17.18 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.88/17.18 (Not % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (Not % 16.88/17.18 (Or % 16.88/17.18 (Or % 16.88/17.18 (Not % 16.88/17.18 (∀ (Y : Iota), % 16.88/17.18 Or (Not (r1 X Y)) % 16.88/17.18 (∀ (X : Iota), % 16.88/17.18 Or (Not (r1 Y X)) % 16.88/17.18 (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.95/17.22 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.95/17.22 (Not % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (Not % 16.95/17.22 (Not % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))))))) % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 (skS.0 0 a) Y)) % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (p4 X) (p3 X)) (p2 X)) (p1 X))))))) % 16.95/17.22 False % 16.95/17.22 Clause #6 (by clausification #[4]): ∀ (a : Iota), % 16.95/17.22 Eq % 16.95/17.22 (Or % 16.95/17.22 (Or % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 (skS.0 0 a) Y)) % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 16.95/17.22 (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p5 Y))) % 16.95/17.22 (Not % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 (skS.0 0 a) Y)) % 16.95/17.22 (Not % 16.95/17.22 (Or % 16.95/17.22 (Or % 16.95/17.22 (Not % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.95/17.22 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.95/17.22 (Not % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (Not % 16.95/17.22 (Or % 16.95/17.22 (Or % 16.95/17.22 (Not % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.95/17.22 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.95/17.22 (Not % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (Not % 16.95/17.22 (Not % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))))))) % 16.95/17.22 False % 16.95/17.22 Clause #30 (by clausification #[6]): ∀ (a : Iota), % 16.95/17.22 Eq % 16.95/17.22 (Not % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 (skS.0 0 a) Y)) % 16.95/17.22 (Not % 16.95/17.22 (Or % 16.95/17.22 (Or % 16.95/17.22 (Not % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.95/17.22 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.95/17.22 (Not % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) % 16.95/17.22 (Not % 16.95/17.22 (Or % 16.95/17.22 (Or % 16.95/17.22 (Not % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (∀ (X : Iota), % 16.95/17.22 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.95/17.22 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.95/17.22 (Not % 16.95/17.22 (∀ (Y : Iota), % 16.95/17.22 Or (Not (r1 X Y)) % 16.95/17.22 (Not % 16.95/17.22 (Not % 16.95/17.22 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) % 16.95/17.27 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))))))))))))) % 16.95/17.27 False % 16.95/17.27 Clause #31 (by clausification #[6]): ∀ (a : Iota), % 16.95/17.27 Eq % 16.95/17.27 (Or % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 (skS.0 0 a) Y)) % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 16.95/17.27 (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p5 Y))) % 16.95/17.27 False % 16.95/17.27 Clause #32 (by clausification #[30]): ∀ (a : Iota), % 16.95/17.27 Eq % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 (skS.0 0 a) Y)) % 16.95/17.27 (Not % 16.95/17.27 (Or % 16.95/17.27 (Or % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.95/17.27 (∀ (X : Iota), Or (Not (r1 Y X)) (p4 X))) % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) % 16.95/17.27 (Not % 16.95/17.27 (Or % 16.95/17.27 (Or % 16.95/17.27 (Not % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.95/17.27 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.95/17.27 (Not % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (Not % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) % 16.95/17.27 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))))) % 16.95/17.27 True % 16.95/17.27 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), % 16.95/17.27 Eq % 16.95/17.27 (Or (Not (r1 (skS.0 0 a) a_1)) % 16.95/17.27 (Not % 16.95/17.27 (Or % 16.95/17.27 (Or % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 a_1 X)) % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.95/17.27 (∀ (X : Iota), Or (Not (r1 a_1 X)) (p4 X))) % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 a_1 X)) % 16.95/17.27 (Not % 16.95/17.27 (Or % 16.95/17.27 (Or % 16.95/17.27 (Not % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 16.95/17.27 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 16.95/17.27 (Not % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (Not % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) % 16.95/17.27 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))))) % 16.95/17.27 True % 16.95/17.27 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), % 16.95/17.27 Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) % 16.95/17.27 (Eq % 16.95/17.27 (Not % 16.95/17.27 (Or % 16.95/17.27 (Or % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 a_1 X)) % 16.95/17.27 (∀ (Y : Iota), % 16.95/17.27 Or (Not (r1 X Y)) % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 16.95/17.27 (∀ (X : Iota), Or (Not (r1 a_1 X)) (p4 X))) % 16.95/17.27 (Not % 16.95/17.27 (∀ (X : Iota), % 16.95/17.27 Or (Not (r1 a_1 X)) % 16.95/17.27 (Not % 16.95/17.27 (Or % 17.05/17.32 (Or % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.32 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (Not % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) % 17.05/17.32 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))))))))))) % 17.05/17.32 True) % 17.05/17.32 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), % 17.05/17.32 Or % 17.05/17.32 (Eq % 17.05/17.32 (Not % 17.05/17.32 (Or % 17.05/17.32 (Or % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 a X)) % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 17.05/17.32 (∀ (X : Iota), Or (Not (r1 a X)) (p4 X))) % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 a X)) % 17.05/17.32 (Not % 17.05/17.32 (Or % 17.05/17.32 (Or % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.32 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (Not % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) % 17.05/17.32 (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))))))))))) % 17.05/17.32 True) % 17.05/17.32 (Eq (r1 (skS.0 0 a_1) a) False) % 17.05/17.32 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 17.05/17.32 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.32 (Eq % 17.05/17.32 (Or % 17.05/17.32 (Or % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 a_1 X)) % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 17.05/17.32 (∀ (X : Iota), Or (Not (r1 a_1 X)) (p4 X))) % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 a_1 X)) % 17.05/17.32 (Not % 17.05/17.32 (Or % 17.05/17.32 (Or % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.32 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (Not % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))))) % 17.05/17.32 False) % 17.05/17.32 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 17.05/17.32 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.32 (Eq % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 a_1 X)) % 17.05/17.32 (Not % 17.05/17.32 (Or % 17.05/17.32 (Or % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (∀ (X : Iota), % 17.05/17.32 Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.32 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 17.05/17.32 (Not % 17.05/17.32 (∀ (Y : Iota), % 17.05/17.32 Or (Not (r1 X Y)) % 17.05/17.32 (Not % 17.05/17.32 (Not % 17.05/17.32 (∀ (X : Iota), % 17.05/17.38 Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))))))))) % 17.05/17.38 False) % 17.05/17.38 Clause #38 (by clausification #[36]): ∀ (a a_1 : Iota), % 17.05/17.38 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.38 (Eq % 17.05/17.38 (Or % 17.05/17.38 (Not % 17.05/17.38 (∀ (X : Iota), % 17.05/17.38 Or (Not (r1 a_1 X)) % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 X Y)) % 17.05/17.38 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 17.05/17.38 (∀ (X : Iota), Or (Not (r1 a_1 X)) (p4 X))) % 17.05/17.38 False) % 17.05/17.38 Clause #39 (by clausification #[37]): ∀ (a a_1 : Iota), % 17.05/17.38 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.38 (Eq % 17.05/17.38 (∀ (X : Iota), % 17.05/17.38 Or (Not (r1 a_1 X)) % 17.05/17.38 (Not % 17.05/17.38 (Or % 17.05/17.38 (Or % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 X Y)) % 17.05/17.38 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.38 (∀ (Y : Iota), Or (Not (r1 X Y)) (p3 Y))) % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 X Y)) % 17.05/17.38 (Not % 17.05/17.38 (Not % 17.05/17.38 (∀ (X : Iota), % 17.05/17.38 Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))) % 17.05/17.38 True) % 17.05/17.38 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 17.05/17.38 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.38 (Eq % 17.05/17.38 (Or (Not (r1 a_1 a_2)) % 17.05/17.38 (Not % 17.05/17.38 (Or % 17.05/17.38 (Or % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 a_2 Y)) % 17.05/17.38 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.38 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 a_2 Y)) % 17.05/17.38 (Not % 17.05/17.38 (Not % 17.05/17.38 (∀ (X : Iota), % 17.05/17.38 Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))))) % 17.05/17.38 True) % 17.05/17.38 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), % 17.05/17.38 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.38 (Or (Eq (Not (r1 a_1 a_2)) True) % 17.05/17.38 (Eq % 17.05/17.38 (Not % 17.05/17.38 (Or % 17.05/17.38 (Or % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 a_2 Y)) % 17.05/17.38 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.38 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 a_2 Y)) % 17.05/17.38 (Not % 17.05/17.38 (Not % 17.05/17.38 (∀ (X : Iota), % 17.05/17.38 Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))))))) % 17.05/17.38 True)) % 17.05/17.38 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 17.05/17.38 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.38 (Or % 17.05/17.38 (Eq % 17.05/17.38 (Not % 17.05/17.38 (Or % 17.05/17.38 (Or % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 a_2 Y)) % 17.05/17.38 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.38 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 a_2 Y)) % 17.05/17.38 (Not % 17.05/17.38 (Not % 17.05/17.38 (∀ (X : Iota), % 17.05/17.38 Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))))))) % 17.05/17.38 True) % 17.05/17.38 (Eq (r1 a_1 a_2) False)) % 17.05/17.38 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), % 17.05/17.38 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.05/17.38 (Or (Eq (r1 a_1 a_2) False) % 17.05/17.38 (Eq % 17.05/17.38 (Or % 17.05/17.38 (Or % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.05/17.38 Or (Not (r1 a_2 Y)) % 17.05/17.38 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.05/17.38 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 17.05/17.38 (Not % 17.05/17.38 (∀ (Y : Iota), % 17.15/17.44 Or (Not (r1 a_2 Y)) % 17.15/17.44 (Not % 17.15/17.44 (Not % 17.15/17.44 (∀ (X : Iota), % 17.15/17.44 Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))))) % 17.15/17.44 False)) % 17.15/17.44 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Eq % 17.15/17.44 (Not % 17.15/17.44 (∀ (Y : Iota), % 17.15/17.44 Or (Not (r1 a_2 Y)) % 17.15/17.44 (Not % 17.15/17.44 (Not % 17.15/17.44 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))))) % 17.15/17.44 False)) % 17.15/17.44 Clause #45 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Eq % 17.15/17.44 (Or % 17.15/17.44 (Not % 17.15/17.44 (∀ (Y : Iota), % 17.15/17.44 Or (Not (r1 a_2 Y)) % 17.15/17.44 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.15/17.44 (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p3 Y))) % 17.15/17.44 False)) % 17.15/17.44 Clause #46 (by clausification #[44]): ∀ (a a_1 a_2 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Eq % 17.15/17.44 (∀ (Y : Iota), % 17.15/17.44 Or (Not (r1 a_2 Y)) % 17.15/17.44 (Not % 17.15/17.44 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))) % 17.15/17.44 True)) % 17.15/17.44 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Eq % 17.15/17.44 (Or (Not (r1 a_2 a_3)) % 17.15/17.44 (Not % 17.15/17.44 (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))))) % 17.15/17.44 True)) % 17.15/17.44 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or (Eq (Not (r1 a_2 a_3)) True) % 17.15/17.44 (Eq % 17.15/17.44 (Not (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))) % 17.15/17.44 True))) % 17.15/17.44 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or % 17.15/17.44 (Eq % 17.15/17.44 (Not (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))))) % 17.15/17.44 True) % 17.15/17.44 (Eq (r1 a_2 a_3) False))) % 17.15/17.44 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or (Eq (r1 a_2 a_3) False) % 17.15/17.44 (Eq (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X)))))) % 17.15/17.44 False))) % 17.15/17.44 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or (Eq (r1 a_2 a_3) False) % 17.15/17.44 (Eq (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p1 X)) (Not (p2 X))) (And (p2 X) (p1 X))))) True))) % 17.15/17.44 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or (Eq (r1 a_2 a_3) False) % 17.15/17.44 (Eq (Or (Not (r1 a_3 a_4)) (Not (Or (And (Not (p1 a_4)) (Not (p2 a_4))) (And (p2 a_4) (p1 a_4))))) True))) % 17.15/17.44 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or (Eq (r1 a_2 a_3) False) % 17.15/17.44 (Or (Eq (Not (r1 a_3 a_4)) True) % 17.15/17.44 (Eq (Not (Or (And (Not (p1 a_4)) (Not (p2 a_4))) (And (p2 a_4) (p1 a_4)))) True)))) % 17.15/17.44 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or (Eq (r1 a_2 a_3) False) % 17.15/17.44 (Or (Eq (Not (Or (And (Not (p1 a_4)) (Not (p2 a_4))) (And (p2 a_4) (p1 a_4)))) True) (Eq (r1 a_3 a_4) False)))) % 17.15/17.44 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.15/17.44 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.15/17.44 (Or (Eq (r1 a_1 a_2) False) % 17.15/17.44 (Or (Eq (r1 a_2 a_3) False) % 17.15/17.44 (Or (Eq (r1 a_3 a_4) False) (Eq (Or (And (Not (p1 a_4)) (Not (p2 a_4))) (And (p2 a_4) (p1 a_4))) False)))) % 17.25/17.51 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Or (Eq (r1 a_1 a_2) False) % 17.25/17.51 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Eq (And (p2 a_4) (p1 a_4)) False)))) % 17.25/17.51 Clause #57 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Or (Eq (r1 a_1 a_2) False) % 17.25/17.51 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Eq (And (Not (p1 a_4)) (Not (p2 a_4))) False)))) % 17.25/17.51 Clause #58 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Or (Eq (r1 a_1 a_2) False) % 17.25/17.51 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) False) (Eq (p1 a_4) False))))) % 17.25/17.51 Clause #66 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Or (Eq (r1 a_1 a_2) False) % 17.25/17.51 (Or (Eq (r1 a_2 a_3) False) % 17.25/17.51 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (Not (p1 a_4)) False) (Eq (Not (p2 a_4)) False))))) % 17.25/17.51 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Or (Eq (r1 a_1 a_2) False) % 17.25/17.51 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (Not (p2 a_4)) False) (Eq (p1 a_4) True))))) % 17.25/17.51 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Or (Eq (r1 a_1 a_2) False) % 17.25/17.51 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) True) (Eq (p2 a_4) True))))) % 17.25/17.51 Clause #73 (by clausification #[31]): ∀ (a : Iota), % 17.25/17.51 Eq % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 (skS.0 0 a) Y)) % 17.25/17.51 (∀ (X : Iota), % 17.25/17.51 Or (Not (r1 Y X)) % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 X Y)) % 17.25/17.51 (∀ (X : Iota), % 17.25/17.51 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 17.25/17.51 False % 17.25/17.51 Clause #88 (by clausification #[38]): ∀ (a a_1 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Eq % 17.25/17.51 (Not % 17.25/17.51 (∀ (X : Iota), % 17.25/17.51 Or (Not (r1 a_1 X)) % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 X Y)) % 17.25/17.51 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))))) % 17.25/17.51 False) % 17.25/17.51 Clause #107 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), % 17.25/17.51 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.25/17.51 (Or (Eq (r1 a_1 a_2) False) % 17.25/17.51 (Eq % 17.25/17.51 (Not % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 a_2 Y)) % 17.25/17.51 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))))) % 17.25/17.51 False)) % 17.25/17.51 Clause #133 (by clausification #[73]): ∀ (a a_1 : Iota), % 17.25/17.51 Eq % 17.25/17.51 (Not % 17.25/17.51 (Or (Not (r1 (skS.0 0 a) (skS.0 8 a a_1))) % 17.25/17.51 (∀ (X : Iota), % 17.25/17.51 Or (Not (r1 (skS.0 8 a a_1) X)) % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 X Y)) % 17.25/17.51 (∀ (X : Iota), % 17.25/17.51 Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X)))))))) % 17.25/17.51 True % 17.25/17.51 Clause #134 (by clausification #[133]): ∀ (a a_1 : Iota), % 17.25/17.51 Eq % 17.25/17.51 (Or (Not (r1 (skS.0 0 a) (skS.0 8 a a_1))) % 17.25/17.51 (∀ (X : Iota), % 17.25/17.51 Or (Not (r1 (skS.0 8 a a_1) X)) % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 X Y)) % 17.25/17.51 (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 17.25/17.51 False % 17.25/17.51 Clause #135 (by clausification #[134]): ∀ (a a_1 : Iota), % 17.25/17.51 Eq % 17.25/17.51 (∀ (X : Iota), % 17.25/17.51 Or (Not (r1 (skS.0 8 a a_1) X)) % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 X Y)) % 17.25/17.51 (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X)))))) % 17.25/17.51 False % 17.25/17.51 Clause #136 (by clausification #[134]): ∀ (a a_1 : Iota), Eq (Not (r1 (skS.0 0 a) (skS.0 8 a a_1))) False % 17.25/17.51 Clause #137 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 17.25/17.51 Eq % 17.25/17.51 (Not % 17.25/17.51 (Or (Not (r1 (skS.0 8 a a_1) (skS.0 9 a a_1 a_2))) % 17.25/17.51 (∀ (Y : Iota), % 17.25/17.51 Or (Not (r1 (skS.0 9 a a_1 a_2) Y)) % 17.25/17.51 (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))))) % 17.25/17.58 True % 17.25/17.58 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 17.25/17.58 Eq % 17.25/17.58 (Or (Not (r1 (skS.0 8 a a_1) (skS.0 9 a a_1 a_2))) % 17.25/17.58 (∀ (Y : Iota), % 17.25/17.58 Or (Not (r1 (skS.0 9 a a_1 a_2) Y)) % 17.25/17.58 (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X)))))) % 17.25/17.58 False % 17.25/17.58 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 17.25/17.58 Eq % 17.25/17.58 (∀ (Y : Iota), % 17.25/17.58 Or (Not (r1 (skS.0 9 a a_1 a_2) Y)) % 17.25/17.58 (∀ (X : Iota), Or (Not (r1 Y X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))) % 17.25/17.58 False % 17.25/17.58 Clause #140 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), Eq (Not (r1 (skS.0 8 a a_1) (skS.0 9 a a_1 a_2))) False % 17.25/17.58 Clause #141 (by clausification #[139]): ∀ (a a_1 a_2 a_3 : Iota), % 17.25/17.58 Eq % 17.25/17.58 (Not % 17.25/17.58 (Or (Not (r1 (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3))) % 17.25/17.58 (∀ (X : Iota), % 17.25/17.58 Or (Not (r1 (skS.0 10 a a_1 a_2 a_3) X)) % 17.25/17.58 (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X)))))) % 17.25/17.58 True % 17.25/17.58 Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 a_3 : Iota), % 17.25/17.58 Eq % 17.25/17.58 (Or (Not (r1 (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3))) % 17.25/17.58 (∀ (X : Iota), % 17.25/17.58 Or (Not (r1 (skS.0 10 a a_1 a_2 a_3) X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X))))) % 17.25/17.58 False % 17.25/17.58 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), % 17.25/17.58 Eq % 17.25/17.58 (∀ (X : Iota), % 17.25/17.58 Or (Not (r1 (skS.0 10 a a_1 a_2 a_3) X)) (And (And (And (Not (p8 X)) (Not (p6 X))) (Not (p4 X))) (Not (p2 X)))) % 17.25/17.58 False % 17.25/17.58 Clause #144 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Not (r1 (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3))) False % 17.25/17.58 Clause #145 (by clausification #[143]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.58 Eq % 17.25/17.58 (Not % 17.25/17.58 (Or (Not (r1 (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4))) % 17.25/17.58 (And % 17.25/17.58 (And (And (Not (p8 (skS.0 11 a a_1 a_2 a_3 a_4))) (Not (p6 (skS.0 11 a a_1 a_2 a_3 a_4)))) % 17.25/17.58 (Not (p4 (skS.0 11 a a_1 a_2 a_3 a_4)))) % 17.25/17.58 (Not (p2 (skS.0 11 a a_1 a_2 a_3 a_4)))))) % 17.25/17.58 True % 17.25/17.58 Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.58 Eq % 17.25/17.58 (Or (Not (r1 (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4))) % 17.25/17.58 (And % 17.25/17.58 (And (And (Not (p8 (skS.0 11 a a_1 a_2 a_3 a_4))) (Not (p6 (skS.0 11 a a_1 a_2 a_3 a_4)))) % 17.25/17.58 (Not (p4 (skS.0 11 a a_1 a_2 a_3 a_4)))) % 17.25/17.58 (Not (p2 (skS.0 11 a a_1 a_2 a_3 a_4))))) % 17.25/17.58 False % 17.25/17.58 Clause #148 (by clausification #[146]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (Not (r1 (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4))) False % 17.25/17.58 Clause #156 (by clausification #[136]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 0 a) (skS.0 8 a a_1)) True % 17.25/17.58 Clause #157 (by superposition #[156, 58]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.58 Or (Eq True False) % 17.25/17.58 (Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.25/17.58 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) False) (Eq (p1 a_4) False))))) % 17.25/17.58 Clause #158 (by superposition #[156, 68]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.58 Or (Eq True False) % 17.25/17.58 (Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.25/17.58 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) True) (Eq (p2 a_4) True))))) % 17.25/17.58 Clause #164 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 8 a a_1) (skS.0 9 a a_1 a_2)) True % 17.25/17.58 Clause #171 (by clausification #[144]): ∀ (a a_1 a_2 a_3 : Iota), Eq (r1 (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3)) True % 17.25/17.58 Clause #172 (by clausification #[158]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.58 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.25/17.58 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) True) (Eq (p2 a_4) True)))) % 17.25/17.58 Clause #173 (by superposition #[172, 164]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.58 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) % 17.25/17.58 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) True) (Or (Eq (p2 a_4) True) (Eq False True)))) % 17.25/17.58 Clause #174 (by clausification #[173]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.25/17.58 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) True) (Eq (p2 a_4) True))) % 17.35/17.65 Clause #175 (by superposition #[174, 171]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p1 a_4) True) (Or (Eq (p2 a_4) True) (Eq False True))) % 17.35/17.65 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p1 a_4) True) (Eq (p2 a_4) True)) % 17.35/17.65 Clause #177 (by clausification #[88]): ∀ (a a_1 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Eq % 17.35/17.65 (∀ (X : Iota), % 17.35/17.65 Or (Not (r1 a_1 X)) % 17.35/17.65 (∀ (Y : Iota), % 17.35/17.65 Or (Not (r1 X Y)) % 17.35/17.65 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X))))))) % 17.35/17.65 True) % 17.35/17.65 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Eq % 17.35/17.65 (Or (Not (r1 a_1 a_2)) % 17.35/17.65 (∀ (Y : Iota), % 17.35/17.65 Or (Not (r1 a_2 Y)) % 17.35/17.65 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X))))))) % 17.35/17.65 True) % 17.35/17.65 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (Not (r1 a_1 a_2)) True) % 17.35/17.65 (Eq % 17.35/17.65 (∀ (Y : Iota), % 17.35/17.65 Or (Not (r1 a_2 Y)) % 17.35/17.65 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))) % 17.35/17.65 True)) % 17.35/17.65 Clause #180 (by clausification #[179]): ∀ (a a_1 a_2 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or % 17.35/17.65 (Eq % 17.35/17.65 (∀ (Y : Iota), % 17.35/17.65 Or (Not (r1 a_2 Y)) % 17.35/17.65 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))) % 17.35/17.65 True) % 17.35/17.65 (Eq (r1 a_1 a_2) False)) % 17.35/17.65 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 a_3 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Eq % 17.35/17.65 (Or (Not (r1 a_2 a_3)) % 17.35/17.65 (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X)))))) % 17.35/17.65 True)) % 17.35/17.65 Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 a_3 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Or (Eq (Not (r1 a_2 a_3)) True) % 17.35/17.65 (Eq (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X))))) True))) % 17.35/17.65 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 a_3 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p3 X)) (Not (p1 X))) (And (p1 X) (p3 X))))) True) % 17.35/17.65 (Eq (r1 a_2 a_3) False))) % 17.35/17.65 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Or (Eq (r1 a_2 a_3) False) % 17.35/17.65 (Eq (Or (Not (r1 a_3 a_4)) (Not (Or (And (Not (p3 a_4)) (Not (p1 a_4))) (And (p1 a_4) (p3 a_4))))) True))) % 17.35/17.65 Clause #185 (by clausification #[184]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Or (Eq (r1 a_2 a_3) False) % 17.35/17.65 (Or (Eq (Not (r1 a_3 a_4)) True) % 17.35/17.65 (Eq (Not (Or (And (Not (p3 a_4)) (Not (p1 a_4))) (And (p1 a_4) (p3 a_4)))) True)))) % 17.35/17.65 Clause #186 (by clausification #[185]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Or (Eq (r1 a_2 a_3) False) % 17.35/17.65 (Or (Eq (Not (Or (And (Not (p3 a_4)) (Not (p1 a_4))) (And (p1 a_4) (p3 a_4)))) True) (Eq (r1 a_3 a_4) False)))) % 17.35/17.65 Clause #187 (by clausification #[186]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Or (Eq (r1 a_2 a_3) False) % 17.35/17.65 (Or (Eq (r1 a_3 a_4) False) (Eq (Or (And (Not (p3 a_4)) (Not (p1 a_4))) (And (p1 a_4) (p3 a_4))) False)))) % 17.35/17.65 Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.35/17.65 (Or (Eq (r1 a_1 a_2) False) % 17.35/17.65 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Eq (And (p1 a_4) (p3 a_4)) False)))) % 17.35/17.65 Clause #189 (by clausification #[187]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.35/17.65 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.72 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Eq (And (Not (p3 a_4)) (Not (p1 a_4))) False)))) % 17.45/17.72 Clause #190 (by clausification #[188]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.72 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) False) (Eq (p3 a_4) False))))) % 17.45/17.72 Clause #193 (by superposition #[190, 156]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.72 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) False) (Or (Eq (p3 a_4) False) (Eq False True))))) % 17.45/17.72 Clause #201 (by clausification #[193]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) False) (Eq (p3 a_4) False)))) % 17.45/17.72 Clause #202 (by superposition #[201, 164]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) % 17.45/17.72 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) False) (Or (Eq (p3 a_4) False) (Eq False True)))) % 17.45/17.72 Clause #204 (by clausification #[202]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p1 a_4) False) (Eq (p3 a_4) False))) % 17.45/17.72 Clause #205 (by superposition #[204, 171]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p1 a_4) False) (Or (Eq (p3 a_4) False) (Eq False True))) % 17.45/17.72 Clause #207 (by clausification #[205]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p1 a_4) False) (Eq (p3 a_4) False)) % 17.45/17.72 Clause #208 (by clausification #[157]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) False) (Eq (p1 a_4) False)))) % 17.45/17.72 Clause #209 (by superposition #[208, 164]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) % 17.45/17.72 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) False) (Or (Eq (p1 a_4) False) (Eq False True)))) % 17.45/17.72 Clause #211 (by clausification #[209]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) False) (Eq (p1 a_4) False))) % 17.45/17.72 Clause #212 (by superposition #[211, 171]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p2 a_4) False) (Or (Eq (p1 a_4) False) (Eq False True))) % 17.45/17.72 Clause #213 (by clausification #[212]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p2 a_4) False) (Eq (p1 a_4) False)) % 17.45/17.72 Clause #222 (by clausification #[148]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (r1 (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4)) True % 17.45/17.72 Clause #223 (by superposition #[222, 176]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq True False) (Or (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True)) % 17.45/17.72 Clause #224 (by superposition #[222, 207]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq True False) (Or (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) False)) % 17.45/17.72 Clause #225 (by superposition #[222, 213]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq True False) (Or (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) False)) % 17.45/17.72 Clause #226 (by clausification #[189]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.72 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.72 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (Not (p3 a_4)) False) (Eq (Not (p1 a_4)) False))))) % 17.45/17.72 Clause #227 (by clausification #[226]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.72 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (Not (p1 a_4)) False) (Eq (p3 a_4) True))))) % 17.45/17.72 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.72 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.72 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.72 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) True) (Eq (p1 a_4) True))))) % 17.45/17.79 Clause #231 (by superposition #[228, 156]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.79 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) True) (Or (Eq (p1 a_4) True) (Eq False True))))) % 17.45/17.79 Clause #232 (by clausification #[231]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) True) (Eq (p1 a_4) True)))) % 17.45/17.79 Clause #233 (by superposition #[232, 164]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) % 17.45/17.79 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) True) (Or (Eq (p1 a_4) True) (Eq False True)))) % 17.45/17.79 Clause #235 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Eq % 17.45/17.79 (∀ (Y : Iota), % 17.45/17.79 Or (Not (r1 a_2 Y)) % 17.45/17.79 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X)))))) % 17.45/17.79 True)) % 17.45/17.79 Clause #236 (by clausification #[235]): ∀ (a a_1 a_2 a_3 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Eq % 17.45/17.79 (Or (Not (r1 a_2 a_3)) % 17.45/17.79 (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X)))))) % 17.45/17.79 True)) % 17.45/17.79 Clause #237 (by clausification #[236]): ∀ (a a_1 a_2 a_3 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (Not (r1 a_2 a_3)) True) % 17.45/17.79 (Eq (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))) True))) % 17.45/17.79 Clause #238 (by clausification #[237]): ∀ (a a_1 a_2 a_3 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_3 X)) (Not (Or (And (Not (p2 X)) (Not (p3 X))) (And (p3 X) (p2 X))))) True) % 17.45/17.79 (Eq (r1 a_2 a_3) False))) % 17.45/17.79 Clause #239 (by clausification #[238]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.79 (Eq (Or (Not (r1 a_3 a_4)) (Not (Or (And (Not (p2 a_4)) (Not (p3 a_4))) (And (p3 a_4) (p2 a_4))))) True))) % 17.45/17.79 Clause #240 (by clausification #[239]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.79 (Or (Eq (Not (r1 a_3 a_4)) True) % 17.45/17.79 (Eq (Not (Or (And (Not (p2 a_4)) (Not (p3 a_4))) (And (p3 a_4) (p2 a_4)))) True)))) % 17.45/17.79 Clause #241 (by clausification #[240]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.79 (Or (Eq (Not (Or (And (Not (p2 a_4)) (Not (p3 a_4))) (And (p3 a_4) (p2 a_4)))) True) (Eq (r1 a_3 a_4) False)))) % 17.45/17.79 Clause #242 (by clausification #[241]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.79 (Or (Eq (r1 a_3 a_4) False) (Eq (Or (And (Not (p2 a_4)) (Not (p3 a_4))) (And (p3 a_4) (p2 a_4))) False)))) % 17.45/17.79 Clause #243 (by clausification #[242]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Eq (And (p3 a_4) (p2 a_4)) False)))) % 17.45/17.79 Clause #244 (by clausification #[242]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Eq (And (Not (p2 a_4)) (Not (p3 a_4))) False)))) % 17.45/17.79 Clause #245 (by clausification #[243]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.45/17.79 (Or (Eq (r1 a_1 a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) False) (Eq (p2 a_4) False))))) % 17.45/17.79 Clause #248 (by superposition #[245, 156]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.45/17.79 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.45/17.79 (Or (Eq (r1 a_2 a_3) False) % 17.45/17.79 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) False) (Or (Eq (p2 a_4) False) (Eq False True))))) % 17.55/17.86 Clause #249 (by clausification #[233]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) True) (Eq (p1 a_4) True))) % 17.55/17.86 Clause #250 (by superposition #[249, 171]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p3 a_4) True) (Or (Eq (p1 a_4) True) (Eq False True))) % 17.55/17.86 Clause #251 (by clausification #[250]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p3 a_4) True) (Eq (p1 a_4) True)) % 17.55/17.86 Clause #252 (by superposition #[251, 222]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Or (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq False True)) % 17.55/17.86 Clause #255 (by clausification #[248]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.55/17.86 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) False) (Eq (p2 a_4) False)))) % 17.55/17.86 Clause #256 (by superposition #[255, 164]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) % 17.55/17.86 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) False) (Or (Eq (p2 a_4) False) (Eq False True)))) % 17.55/17.86 Clause #258 (by clausification #[256]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p3 a_4) False) (Eq (p2 a_4) False))) % 17.55/17.86 Clause #259 (by superposition #[258, 171]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p3 a_4) False) (Or (Eq (p2 a_4) False) (Eq False True))) % 17.55/17.86 Clause #263 (by clausification #[259]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p3 a_4) False) (Eq (p2 a_4) False)) % 17.55/17.86 Clause #264 (by superposition #[263, 222]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Or (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Eq False True)) % 17.55/17.86 Clause #295 (by clausification #[244]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.55/17.86 (Or (Eq (r1 a_1 a_2) False) % 17.55/17.86 (Or (Eq (r1 a_2 a_3) False) % 17.55/17.86 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (Not (p2 a_4)) False) (Eq (Not (p3 a_4)) False))))) % 17.55/17.86 Clause #296 (by clausification #[295]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.55/17.86 (Or (Eq (r1 a_1 a_2) False) % 17.55/17.86 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (Not (p3 a_4)) False) (Eq (p2 a_4) True))))) % 17.55/17.86 Clause #297 (by clausification #[296]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 0 a) a_1) False) % 17.55/17.86 (Or (Eq (r1 a_1 a_2) False) % 17.55/17.86 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) True) (Eq (p3 a_4) True))))) % 17.55/17.86 Clause #300 (by superposition #[297, 156]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.55/17.86 (Or (Eq (r1 a_2 a_3) False) % 17.55/17.86 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) True) (Or (Eq (p3 a_4) True) (Eq False True))))) % 17.55/17.86 Clause #301 (by clausification #[300]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 8 a a_1) a_2) False) % 17.55/17.86 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) True) (Eq (p3 a_4) True)))) % 17.55/17.86 Clause #302 (by superposition #[301, 164]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) % 17.55/17.86 (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) True) (Or (Eq (p3 a_4) True) (Eq False True)))) % 17.55/17.86 Clause #310 (by clausification #[302]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 9 a a_1 a_2) a_3) False) (Or (Eq (r1 a_3 a_4) False) (Or (Eq (p2 a_4) True) (Eq (p3 a_4) True))) % 17.55/17.86 Clause #311 (by superposition #[310, 171]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p2 a_4) True) (Or (Eq (p3 a_4) True) (Eq False True))) % 17.55/17.86 Clause #313 (by clausification #[311]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (r1 (skS.0 10 a a_1 a_2 a_3) a_4) False) (Or (Eq (p2 a_4) True) (Eq (p3 a_4) True)) % 17.55/17.86 Clause #314 (by superposition #[313, 222]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.55/17.86 Or (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq False True)) % 17.65/17.91 Clause #363 (by clausification #[223]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True) % 17.65/17.91 Clause #369 (by clausification #[224]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) False) % 17.65/17.91 Clause #370 (by superposition #[369, 363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Or (Eq False True) (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True)) % 17.65/17.91 Clause #376 (by clausification #[225]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) False) % 17.65/17.91 Clause #382 (by clausification #[252]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) True) % 17.65/17.91 Clause #389 (by clausification #[264]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) False) % 17.65/17.91 Clause #393 (by clausification #[370]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) False) (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True) % 17.65/17.91 Clause #399 (by clausification #[314]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) % 17.65/17.91 Clause #400 (by superposition #[399, 376]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Or (Eq True False) (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) False)) % 17.65/17.91 Clause #401 (by clausification #[400]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq (p1 (skS.0 11 a a_1 a_2 a_3 a_4)) False) % 17.65/17.91 Clause #403 (by superposition #[401, 382]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 17.65/17.91 Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq False True)) % 17.65/17.91 Clause #404 (by clausification #[403]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) (Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True) % 17.65/17.91 Clause #405 (by eliminate duplicate literals #[404]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (p3 (skS.0 11 a a_1 a_2 a_3 a_4)) True % 17.65/17.91 Clause #408 (by backward demodulation #[405, 389]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) False) % 17.65/17.91 Clause #409 (by backward demodulation #[405, 393]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True) % 17.65/17.91 Clause #412 (by clausification #[409]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) True % 17.65/17.91 Clause #418 (by clausification #[408]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (p2 (skS.0 11 a a_1 a_2 a_3 a_4)) False % 17.65/17.91 Clause #419 (by superposition #[418, 412]): Eq False True % 17.65/17.91 Clause #420 (by clausification #[419]): False % 17.65/17.91 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------