%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL636+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n003.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:10 AM UTC 2026 % Result : Theorem 8.88s 9.19s % Output : Proof 9.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL636+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : duper %s % 0.09/0.36 % Computer : n003.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % 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 13:23:20 UTC 2026 % 0.09/0.37 % CPUTime : % 8.88/9.19 SZS status Theorem for theBenchmark.p % 8.88/9.19 SZS output start Proof for theBenchmark.p % 8.88/9.19 Clause #0 (by assumption #[]): Eq % 8.88/9.19 (Not % 8.88/9.19 (Not % 8.88/9.19 (Exists fun X => % 8.88/9.19 Not % 8.88/9.19 (Or (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) % 8.88/9.19 (Not % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (∀ (Y : Iota), % 8.88/9.19 Or (Not (r1 X Y)) % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (Or % 8.88/9.19 (And % 8.88/9.19 (Not % 8.88/9.19 (∀ (X : Iota), % 8.88/9.19 Or (Not (r1 Y X)) % 8.88/9.19 (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 8.88/9.19 (Not % 8.88/9.19 (∀ (X : Iota), % 8.88/9.19 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 8.88/9.19 (Not (And (Not (p101 Y)) (p100 Y)))) % 8.88/9.19 (Or % 8.88/9.19 (And % 8.88/9.19 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) % 8.88/9.19 (p2 Y)) % 8.88/9.19 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) % 8.88/9.19 (Not (p2 Y)))) % 8.88/9.19 (Not (p101 Y)))) % 8.88/9.19 (Or % 8.88/9.19 (And % 8.88/9.19 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 8.88/9.19 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) % 8.88/9.19 (Not (p1 Y)))) % 8.88/9.19 (Not (p100 Y)))) % 8.88/9.19 (Or (p101 Y) (Not (p102 Y)))) % 8.88/9.19 (Or (p100 Y) (Not (p101 Y))))) % 8.88/9.19 (Or % 8.88/9.19 (And % 8.88/9.19 (Not % 8.88/9.19 (∀ (Y : Iota), % 8.88/9.19 Or (Not (r1 X Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 8.88/9.19 (Not % 8.88/9.19 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 8.88/9.19 (Not (And (Not (p101 X)) (p100 X))))) % 8.88/9.19 (Or % 8.88/9.19 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 X)) % 8.88/9.19 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 X)))) % 8.88/9.19 (Not (p101 X)))) % 8.88/9.19 (Or % 8.88/9.19 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 X)) % 8.88/9.19 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 X)))) % 8.88/9.19 (Not (p100 X)))) % 8.88/9.19 (Or (p101 X) (Not (p102 X)))) % 8.88/9.19 (Or (p100 X) (Not (p101 X)))) % 8.88/9.19 (Not (p101 X))) % 8.88/9.19 (p100 X))))))) % 8.88/9.19 True % 8.88/9.19 Clause #1 (by clausification #[0]): Eq % 8.88/9.19 (Not % 8.88/9.19 (Exists fun X => % 8.88/9.19 Not % 8.88/9.19 (Or (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) % 8.88/9.19 (Not % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (And % 8.88/9.19 (∀ (Y : Iota), % 8.88/9.19 Or (Not (r1 X Y)) % 8.88/9.19 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (Or % 8.94/9.22 (And % 8.94/9.22 (Not % 8.94/9.22 (∀ (X : Iota), % 8.94/9.22 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 8.94/9.22 (Not % 8.94/9.22 (∀ (X : Iota), % 8.94/9.22 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 8.94/9.22 (Not (And (Not (p101 Y)) (p100 Y)))) % 8.94/9.22 (Or % 8.94/9.22 (And % 8.94/9.22 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 8.94/9.22 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) % 8.94/9.22 (Not (p2 Y)))) % 8.94/9.22 (Not (p101 Y)))) % 8.94/9.22 (Or % 8.94/9.22 (And % 8.94/9.22 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 8.94/9.22 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 8.94/9.22 (Not (p100 Y)))) % 8.94/9.22 (Or (p101 Y) (Not (p102 Y)))) % 8.94/9.22 (Or (p100 Y) (Not (p101 Y))))) % 8.94/9.22 (Or % 8.94/9.22 (And % 8.94/9.22 (Not % 8.94/9.22 (∀ (Y : Iota), % 8.94/9.22 Or (Not (r1 X Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 8.94/9.22 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 8.94/9.22 (Not (And (Not (p101 X)) (p100 X))))) % 8.94/9.22 (Or % 8.94/9.22 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 X)) % 8.94/9.22 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 X)))) % 8.94/9.22 (Not (p101 X)))) % 8.94/9.22 (Or % 8.94/9.22 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 X)) % 8.94/9.22 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 X)))) % 8.94/9.22 (Not (p100 X)))) % 8.94/9.22 (Or (p101 X) (Not (p102 X)))) % 8.94/9.22 (Or (p100 X) (Not (p101 X)))) % 8.94/9.22 (Not (p101 X))) % 8.94/9.22 (p100 X)))))) % 8.94/9.22 False % 8.94/9.22 Clause #2 (by clausification #[1]): Eq % 8.94/9.22 (Exists fun X => % 8.94/9.22 Not % 8.94/9.22 (Or (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p2 Y))) % 8.94/9.22 (Not % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (∀ (Y : Iota), % 8.94/9.22 Or (Not (r1 X Y)) % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (And % 8.94/9.22 (Or % 8.94/9.22 (And % 8.94/9.22 (Not % 8.94/9.22 (∀ (X : Iota), % 8.94/9.22 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 8.94/9.22 (Not % 8.94/9.22 (∀ (X : Iota), % 8.94/9.22 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 8.94/9.22 (Not (And (Not (p101 Y)) (p100 Y)))) % 8.94/9.22 (Or % 8.94/9.22 (And % 8.94/9.22 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 8.94/9.26 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 8.94/9.26 (Not (p101 Y)))) % 8.94/9.26 (Or % 8.94/9.26 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 8.94/9.26 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 8.94/9.26 (Not (p100 Y)))) % 8.94/9.26 (Or (p101 Y) (Not (p102 Y)))) % 8.94/9.26 (Or (p100 Y) (Not (p101 Y))))) % 8.94/9.26 (Or % 8.94/9.26 (And % 8.94/9.26 (Not % 8.94/9.26 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 8.94/9.26 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 8.94/9.26 (Not (And (Not (p101 X)) (p100 X))))) % 8.94/9.26 (Or % 8.94/9.26 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 X)) % 8.94/9.26 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 X)))) % 8.94/9.26 (Not (p101 X)))) % 8.94/9.26 (Or % 8.94/9.26 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 X)) % 8.94/9.26 (Or (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 X)))) % 8.94/9.26 (Not (p100 X)))) % 8.94/9.26 (Or (p101 X) (Not (p102 X)))) % 8.94/9.26 (Or (p100 X) (Not (p101 X)))) % 8.94/9.26 (Not (p101 X))) % 8.94/9.26 (p100 X))))) % 8.94/9.26 True % 8.94/9.26 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 8.94/9.26 Eq % 8.94/9.26 (Not % 8.94/9.26 (Or (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p2 Y))) % 8.94/9.26 (Not % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (∀ (Y : Iota), % 8.94/9.26 Or (Not (r1 (skS.0 0 a) Y)) % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (And % 8.94/9.26 (Or % 8.94/9.26 (And % 8.94/9.26 (Not % 8.94/9.26 (∀ (X : Iota), % 8.94/9.26 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 8.94/9.26 (Not % 8.94/9.26 (∀ (X : Iota), % 8.94/9.26 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 8.94/9.26 (Not (And (Not (p101 Y)) (p100 Y)))) % 8.94/9.26 (Or % 8.94/9.26 (And % 8.94/9.26 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 8.94/9.26 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 8.94/9.26 (Not (p101 Y)))) % 8.94/9.26 (Or % 8.94/9.26 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 8.94/9.26 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 8.94/9.26 (Not (p100 Y)))) % 8.94/9.26 (Or (p101 Y) (Not (p102 Y)))) % 8.94/9.26 (Or (p100 Y) (Not (p101 Y))))) % 8.94/9.26 (Or % 8.94/9.26 (And % 8.94/9.26 (Not % 8.94/9.26 (∀ (Y : Iota), % 8.94/9.26 Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 8.94/9.26 (Not % 9.04/9.30 (∀ (Y : Iota), % 9.04/9.30 Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.04/9.30 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.04/9.30 (Or % 9.04/9.30 (And % 9.04/9.30 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) % 9.04/9.30 (p2 (skS.0 0 a))) % 9.04/9.30 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) % 9.04/9.30 (Not (p2 (skS.0 0 a))))) % 9.04/9.30 (Not (p101 (skS.0 0 a))))) % 9.04/9.30 (Or % 9.04/9.30 (And % 9.04/9.30 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) % 9.04/9.30 (p1 (skS.0 0 a))) % 9.04/9.30 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) % 9.04/9.30 (Not (p1 (skS.0 0 a))))) % 9.04/9.30 (Not (p100 (skS.0 0 a))))) % 9.04/9.30 (Or (p101 (skS.0 0 a)) (Not (p102 (skS.0 0 a))))) % 9.04/9.30 (Or (p100 (skS.0 0 a)) (Not (p101 (skS.0 0 a))))) % 9.04/9.30 (Not (p101 (skS.0 0 a)))) % 9.04/9.30 (p100 (skS.0 0 a)))))) % 9.04/9.30 True % 9.04/9.30 Clause #4 (by clausification #[3]): ∀ (a : Iota), % 9.04/9.30 Eq % 9.04/9.30 (Or (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p2 Y))) % 9.04/9.30 (Not % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (∀ (Y : Iota), % 9.04/9.30 Or (Not (r1 (skS.0 0 a) Y)) % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (And % 9.04/9.30 (Or % 9.04/9.30 (And % 9.04/9.30 (Not % 9.04/9.30 (∀ (X : Iota), % 9.04/9.30 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.04/9.30 (Not % 9.04/9.30 (∀ (X : Iota), % 9.04/9.30 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.04/9.30 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.04/9.30 (Or % 9.04/9.30 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.04/9.30 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.04/9.30 (Not (p101 Y)))) % 9.04/9.30 (Or % 9.04/9.30 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.04/9.30 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.04/9.30 (Not (p100 Y)))) % 9.04/9.30 (Or (p101 Y) (Not (p102 Y)))) % 9.04/9.30 (Or (p100 Y) (Not (p101 Y))))) % 9.04/9.30 (Or % 9.04/9.30 (And % 9.04/9.30 (Not % 9.04/9.30 (∀ (Y : Iota), % 9.04/9.30 Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.04/9.30 (Not % 9.04/9.30 (∀ (Y : Iota), % 9.04/9.30 Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.04/9.30 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.04/9.30 (Or % 9.04/9.30 (And % 9.04/9.30 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) % 9.04/9.30 (p2 (skS.0 0 a))) % 9.04/9.30 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) % 9.04/9.30 (Not (p2 (skS.0 0 a))))) % 9.04/9.30 (Not (p101 (skS.0 0 a))))) % 9.04/9.30 (Or % 9.04/9.30 (And % 9.04/9.37 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 (skS.0 0 a))) % 9.04/9.37 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) % 9.04/9.37 (Not (p1 (skS.0 0 a))))) % 9.04/9.37 (Not (p100 (skS.0 0 a))))) % 9.04/9.37 (Or (p101 (skS.0 0 a)) (Not (p102 (skS.0 0 a))))) % 9.04/9.37 (Or (p100 (skS.0 0 a)) (Not (p101 (skS.0 0 a))))) % 9.04/9.37 (Not (p101 (skS.0 0 a)))) % 9.04/9.37 (p100 (skS.0 0 a))))) % 9.04/9.37 False % 9.04/9.37 Clause #5 (by clausification #[4]): ∀ (a : Iota), % 9.04/9.37 Eq % 9.04/9.37 (Not % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (∀ (Y : Iota), % 9.04/9.37 Or (Not (r1 (skS.0 0 a) Y)) % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (Or % 9.04/9.37 (And % 9.04/9.37 (Not % 9.04/9.37 (∀ (X : Iota), % 9.04/9.37 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.04/9.37 (Not % 9.04/9.37 (∀ (X : Iota), % 9.04/9.37 Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.04/9.37 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.04/9.37 (Or % 9.04/9.37 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.04/9.37 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.04/9.37 (Not (p101 Y)))) % 9.04/9.37 (Or % 9.04/9.37 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.04/9.37 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.04/9.37 (Not (p100 Y)))) % 9.04/9.37 (Or (p101 Y) (Not (p102 Y)))) % 9.04/9.37 (Or (p100 Y) (Not (p101 Y))))) % 9.04/9.37 (Or % 9.04/9.37 (And % 9.04/9.37 (Not % 9.04/9.37 (∀ (Y : Iota), % 9.04/9.37 Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.04/9.37 (Not % 9.04/9.37 (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.04/9.37 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.04/9.37 (Or % 9.04/9.37 (And % 9.04/9.37 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 (skS.0 0 a))) % 9.04/9.37 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) % 9.04/9.37 (Not (p2 (skS.0 0 a))))) % 9.04/9.37 (Not (p101 (skS.0 0 a))))) % 9.04/9.37 (Or % 9.04/9.37 (And % 9.04/9.37 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 (skS.0 0 a))) % 9.04/9.37 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 (skS.0 0 a))))) % 9.04/9.37 (Not (p100 (skS.0 0 a))))) % 9.04/9.37 (Or (p101 (skS.0 0 a)) (Not (p102 (skS.0 0 a))))) % 9.04/9.37 (Or (p100 (skS.0 0 a)) (Not (p101 (skS.0 0 a))))) % 9.04/9.37 (Not (p101 (skS.0 0 a)))) % 9.04/9.37 (p100 (skS.0 0 a)))) % 9.04/9.37 False % 9.04/9.37 Clause #6 (by clausification #[4]): ∀ (a : Iota), Eq (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p2 Y))) False % 9.04/9.37 Clause #7 (by clausification #[5]): ∀ (a : Iota), % 9.04/9.37 Eq % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (∀ (Y : Iota), % 9.04/9.37 Or (Not (r1 (skS.0 0 a) Y)) % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.04/9.37 (And % 9.14/9.41 (Or % 9.14/9.41 (And % 9.14/9.41 (Not % 9.14/9.41 (∀ (X : Iota), % 9.14/9.41 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.14/9.41 (Not % 9.14/9.41 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.14/9.41 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.14/9.41 (Or % 9.14/9.41 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.14/9.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.14/9.41 (Not (p101 Y)))) % 9.14/9.41 (Or % 9.14/9.41 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.14/9.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.14/9.41 (Not (p100 Y)))) % 9.14/9.41 (Or (p101 Y) (Not (p102 Y)))) % 9.14/9.41 (Or (p100 Y) (Not (p101 Y))))) % 9.14/9.41 (Or % 9.14/9.41 (And % 9.14/9.41 (Not % 9.14/9.41 (∀ (Y : Iota), % 9.14/9.41 Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.14/9.41 (Not % 9.14/9.41 (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.14/9.41 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.14/9.41 (Or % 9.14/9.41 (And % 9.14/9.41 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 (skS.0 0 a))) % 9.14/9.41 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 (skS.0 0 a))))) % 9.14/9.41 (Not (p101 (skS.0 0 a))))) % 9.14/9.41 (Or % 9.14/9.41 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 (skS.0 0 a))) % 9.14/9.41 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 (skS.0 0 a))))) % 9.14/9.41 (Not (p100 (skS.0 0 a))))) % 9.14/9.41 (Or (p101 (skS.0 0 a)) (Not (p102 (skS.0 0 a))))) % 9.14/9.41 (Or (p100 (skS.0 0 a)) (Not (p101 (skS.0 0 a))))) % 9.14/9.41 (Not (p101 (skS.0 0 a)))) % 9.14/9.41 (p100 (skS.0 0 a))) % 9.14/9.41 True % 9.14/9.41 Clause #8 (by clausification #[7]): ∀ (a : Iota), Eq (p100 (skS.0 0 a)) True % 9.14/9.41 Clause #9 (by clausification #[7]): ∀ (a : Iota), % 9.14/9.41 Eq % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (∀ (Y : Iota), % 9.14/9.41 Or (Not (r1 (skS.0 0 a) Y)) % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (And % 9.14/9.41 (Or % 9.14/9.41 (And % 9.14/9.41 (Not % 9.14/9.41 (∀ (X : Iota), % 9.14/9.41 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.14/9.41 (Not % 9.14/9.41 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.14/9.41 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.14/9.41 (Or % 9.14/9.41 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.14/9.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.14/9.41 (Not (p101 Y)))) % 9.14/9.41 (Or % 9.14/9.41 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.14/9.41 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.14/9.41 (Not (p100 Y)))) % 9.14/9.41 (Or (p101 Y) (Not (p102 Y)))) % 9.14/9.45 (Or (p100 Y) (Not (p101 Y))))) % 9.14/9.45 (Or % 9.14/9.45 (And % 9.14/9.45 (Not % 9.14/9.45 (∀ (Y : Iota), % 9.14/9.45 Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.14/9.45 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.14/9.45 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.14/9.45 (Or % 9.14/9.45 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 (skS.0 0 a))) % 9.14/9.45 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 (skS.0 0 a))))) % 9.14/9.45 (Not (p101 (skS.0 0 a))))) % 9.14/9.45 (Or % 9.14/9.45 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 (skS.0 0 a))) % 9.14/9.45 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 (skS.0 0 a))))) % 9.14/9.45 (Not (p100 (skS.0 0 a))))) % 9.14/9.45 (Or (p101 (skS.0 0 a)) (Not (p102 (skS.0 0 a))))) % 9.14/9.45 (Or (p100 (skS.0 0 a)) (Not (p101 (skS.0 0 a))))) % 9.14/9.45 (Not (p101 (skS.0 0 a)))) % 9.14/9.45 True % 9.14/9.45 Clause #10 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) True % 9.14/9.45 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Eq (Or (Not (r1 (skS.0 0 a) a_1)) (p2 a_1)) True % 9.14/9.45 Clause #12 (by clausification #[11]): ∀ (a a_1 : Iota), Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) (Eq (p2 a_1) True) % 9.14/9.45 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), Or (Eq (p2 a) True) (Eq (r1 (skS.0 0 a_1) a) False) % 9.14/9.45 Clause #14 (by clausification #[9]): ∀ (a : Iota), Eq (Not (p101 (skS.0 0 a))) True % 9.14/9.45 Clause #15 (by clausification #[9]): ∀ (a : Iota), % 9.14/9.45 Eq % 9.14/9.45 (And % 9.14/9.45 (And % 9.14/9.45 (And % 9.14/9.45 (And % 9.14/9.45 (And % 9.14/9.45 (∀ (Y : Iota), % 9.14/9.45 Or (Not (r1 (skS.0 0 a) Y)) % 9.14/9.45 (And % 9.14/9.45 (And % 9.14/9.45 (And % 9.14/9.45 (And % 9.14/9.45 (Or % 9.14/9.45 (And % 9.14/9.45 (Not % 9.14/9.45 (∀ (X : Iota), % 9.14/9.45 Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.14/9.45 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.14/9.45 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.14/9.45 (Or % 9.14/9.45 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.14/9.45 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.14/9.45 (Not (p101 Y)))) % 9.14/9.45 (Or % 9.14/9.45 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.14/9.45 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.14/9.45 (Not (p100 Y)))) % 9.14/9.45 (Or (p101 Y) (Not (p102 Y)))) % 9.14/9.45 (Or (p100 Y) (Not (p101 Y))))) % 9.14/9.45 (Or % 9.14/9.45 (And % 9.14/9.45 (Not % 9.14/9.45 (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.14/9.45 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.14/9.45 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.14/9.45 (Or % 9.14/9.45 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 (skS.0 0 a))) % 9.14/9.45 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 (skS.0 0 a))))) % 9.14/9.45 (Not (p101 (skS.0 0 a))))) % 9.14/9.45 (Or % 9.14/9.45 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 (skS.0 0 a))) % 9.14/9.45 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 (skS.0 0 a))))) % 9.24/9.52 (Not (p100 (skS.0 0 a))))) % 9.24/9.52 (Or (p101 (skS.0 0 a)) (Not (p102 (skS.0 0 a))))) % 9.24/9.52 (Or (p100 (skS.0 0 a)) (Not (p101 (skS.0 0 a))))) % 9.24/9.52 True % 9.24/9.52 Clause #16 (by clausification #[14]): ∀ (a : Iota), Eq (p101 (skS.0 0 a)) False % 9.24/9.52 Clause #18 (by clausification #[15]): ∀ (a : Iota), % 9.24/9.52 Eq % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (∀ (Y : Iota), % 9.24/9.52 Or (Not (r1 (skS.0 0 a) Y)) % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (Or % 9.24/9.52 (And % 9.24/9.52 (Not % 9.24/9.52 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.24/9.52 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.24/9.52 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.24/9.52 (Or % 9.24/9.52 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.24/9.52 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.24/9.52 (Not (p101 Y)))) % 9.24/9.52 (Or % 9.24/9.52 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.24/9.52 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.24/9.52 (Not (p100 Y)))) % 9.24/9.52 (Or (p101 Y) (Not (p102 Y)))) % 9.24/9.52 (Or (p100 Y) (Not (p101 Y))))) % 9.24/9.52 (Or % 9.24/9.52 (And % 9.24/9.52 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.24/9.52 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.24/9.52 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.24/9.52 (Or % 9.24/9.52 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 (skS.0 0 a))) % 9.24/9.52 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 (skS.0 0 a))))) % 9.24/9.52 (Not (p101 (skS.0 0 a))))) % 9.24/9.52 (Or % 9.24/9.52 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 (skS.0 0 a))) % 9.24/9.52 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 (skS.0 0 a))))) % 9.24/9.52 (Not (p100 (skS.0 0 a))))) % 9.24/9.52 (Or (p101 (skS.0 0 a)) (Not (p102 (skS.0 0 a))))) % 9.24/9.52 True % 9.24/9.52 Clause #23 (by clausification #[18]): ∀ (a : Iota), % 9.24/9.52 Eq % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (∀ (Y : Iota), % 9.24/9.52 Or (Not (r1 (skS.0 0 a) Y)) % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (And % 9.24/9.52 (Or % 9.24/9.52 (And % 9.24/9.52 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.24/9.52 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.24/9.52 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.24/9.52 (Or % 9.24/9.52 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.24/9.52 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.24/9.52 (Not (p101 Y)))) % 9.24/9.52 (Or % 9.24/9.52 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.24/9.52 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.24/9.52 (Not (p100 Y)))) % 9.24/9.52 (Or (p101 Y) (Not (p102 Y)))) % 9.24/9.52 (Or (p100 Y) (Not (p101 Y))))) % 9.24/9.52 (Or % 9.24/9.52 (And % 9.24/9.52 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.24/9.52 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.24/9.57 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.24/9.57 (Or % 9.24/9.57 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 (skS.0 0 a))) % 9.24/9.57 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 (skS.0 0 a))))) % 9.24/9.57 (Not (p101 (skS.0 0 a))))) % 9.24/9.57 (Or % 9.24/9.57 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p1 Y))) (Not (p100 Y))) (p1 (skS.0 0 a))) % 9.24/9.57 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (p100 Y))) (Not (p1 (skS.0 0 a))))) % 9.24/9.57 (Not (p100 (skS.0 0 a))))) % 9.24/9.57 True % 9.24/9.57 Clause #27 (by clausification #[23]): ∀ (a : Iota), % 9.24/9.57 Eq % 9.24/9.57 (And % 9.24/9.57 (And % 9.24/9.57 (∀ (Y : Iota), % 9.24/9.57 Or (Not (r1 (skS.0 0 a) Y)) % 9.24/9.57 (And % 9.24/9.57 (And % 9.24/9.57 (And % 9.24/9.57 (And % 9.24/9.57 (Or % 9.24/9.57 (And % 9.24/9.57 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.24/9.57 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.24/9.57 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.24/9.57 (Or % 9.24/9.57 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.24/9.57 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.24/9.57 (Not (p101 Y)))) % 9.24/9.57 (Or % 9.24/9.57 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.24/9.57 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.24/9.57 (Not (p100 Y)))) % 9.24/9.57 (Or (p101 Y) (Not (p102 Y)))) % 9.24/9.57 (Or (p100 Y) (Not (p101 Y))))) % 9.24/9.57 (Or % 9.24/9.57 (And (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.24/9.57 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.24/9.57 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.24/9.57 (Or % 9.24/9.57 (And (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (Not (p2 Y))) (Not (p101 Y))) (p2 (skS.0 0 a))) % 9.24/9.57 (Or (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p2 Y)) (Not (p101 Y))) (Not (p2 (skS.0 0 a))))) % 9.24/9.57 (Not (p101 (skS.0 0 a))))) % 9.24/9.57 True % 9.24/9.57 Clause #54 (by clausification #[27]): ∀ (a : Iota), % 9.24/9.57 Eq % 9.24/9.57 (And % 9.24/9.57 (∀ (Y : Iota), % 9.24/9.57 Or (Not (r1 (skS.0 0 a) Y)) % 9.24/9.57 (And % 9.24/9.57 (And % 9.24/9.57 (And % 9.24/9.57 (And % 9.24/9.57 (Or % 9.24/9.57 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (Not (p2 X)) (Not (p102 X))) (p101 X))))) % 9.24/9.57 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (And (And (p2 X) (Not (p102 X))) (p101 X)))))) % 9.24/9.57 (Not (And (Not (p101 Y)) (p100 Y)))) % 9.24/9.57 (Or % 9.24/9.57 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p2 X))) (Not (p101 X))) (p2 Y)) % 9.24/9.57 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p2 X)) (Not (p101 X))) (Not (p2 Y)))) % 9.24/9.57 (Not (p101 Y)))) % 9.24/9.57 (Or % 9.24/9.57 (And (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (Not (p1 X))) (Not (p100 X))) (p1 Y)) % 9.24/9.57 (Or (∀ (X : Iota), Or (Or (Not (r1 Y X)) (p1 X)) (Not (p100 X))) (Not (p1 Y)))) % 9.24/9.57 (Not (p100 Y)))) % 9.24/9.57 (Or (p101 Y) (Not (p102 Y)))) % 9.24/9.57 (Or (p100 Y) (Not (p101 Y))))) % 9.24/9.57 (Or % 9.24/9.57 (And (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.24/9.57 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.24/9.57 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))))) % 9.24/9.57 True % 9.24/9.57 Clause #76 (by clausification #[54]): ∀ (a : Iota), % 9.24/9.57 Eq % 9.24/9.57 (Or % 9.24/9.57 (And (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.34/9.64 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.34/9.64 (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a))))) % 9.34/9.64 True % 9.34/9.64 Clause #78 (by clausification #[76]): ∀ (a : Iota), % 9.34/9.64 Or % 9.34/9.64 (Eq % 9.34/9.64 (And (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) % 9.34/9.64 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (p2 Y) (Not (p102 Y))) (p101 Y)))))) % 9.34/9.64 True) % 9.34/9.64 (Eq (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))) True) % 9.34/9.64 Clause #80 (by clausification #[78]): ∀ (a : Iota), % 9.34/9.64 Or (Eq (Not (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a)))) True) % 9.34/9.64 (Eq (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) True) % 9.34/9.64 Clause #118 (by clausification #[80]): ∀ (a : Iota), % 9.34/9.64 Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y))))) True) % 9.34/9.64 (Eq (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a))) False) % 9.34/9.64 Clause #119 (by clausification #[118]): ∀ (a : Iota), % 9.34/9.64 Or (Eq (And (Not (p101 (skS.0 0 a))) (p100 (skS.0 0 a))) False) % 9.34/9.64 (Eq (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y)))) False) % 9.34/9.64 Clause #120 (by clausification #[119]): ∀ (a : Iota), % 9.34/9.64 Or (Eq (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (And (And (Not (p2 Y)) (Not (p102 Y))) (p101 Y)))) False) % 9.34/9.64 (Or (Eq (Not (p101 (skS.0 0 a))) False) (Eq (p100 (skS.0 0 a)) False)) % 9.34/9.64 Clause #121 (by clausification #[120]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (Not (p101 (skS.0 0 a))) False) % 9.34/9.64 (Or (Eq (p100 (skS.0 0 a)) False) % 9.34/9.64 (Eq % 9.34/9.64 (Not % 9.34/9.64 (Or (Not (r1 (skS.0 0 a) (skS.0 2 a a_1))) % 9.34/9.64 (Not (And (And (Not (p2 (skS.0 2 a a_1))) (Not (p102 (skS.0 2 a a_1)))) (p101 (skS.0 2 a a_1)))))) % 9.34/9.64 True)) % 9.34/9.64 Clause #122 (by clausification #[121]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (p100 (skS.0 0 a)) False) % 9.34/9.64 (Or % 9.34/9.64 (Eq % 9.34/9.64 (Not % 9.34/9.64 (Or (Not (r1 (skS.0 0 a) (skS.0 2 a a_1))) % 9.34/9.64 (Not (And (And (Not (p2 (skS.0 2 a a_1))) (Not (p102 (skS.0 2 a a_1)))) (p101 (skS.0 2 a a_1)))))) % 9.34/9.64 True) % 9.34/9.64 (Eq (p101 (skS.0 0 a)) True)) % 9.34/9.64 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (p100 (skS.0 0 a)) False) % 9.34/9.64 (Or (Eq (p101 (skS.0 0 a)) True) % 9.34/9.64 (Eq % 9.34/9.64 (Or (Not (r1 (skS.0 0 a) (skS.0 2 a a_1))) % 9.34/9.64 (Not (And (And (Not (p2 (skS.0 2 a a_1))) (Not (p102 (skS.0 2 a a_1)))) (p101 (skS.0 2 a a_1))))) % 9.34/9.64 False)) % 9.34/9.64 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (p100 (skS.0 0 a)) False) % 9.34/9.64 (Or (Eq (p101 (skS.0 0 a)) True) % 9.34/9.64 (Eq (Not (And (And (Not (p2 (skS.0 2 a a_1))) (Not (p102 (skS.0 2 a a_1)))) (p101 (skS.0 2 a a_1)))) False)) % 9.34/9.64 Clause #125 (by clausification #[123]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (p100 (skS.0 0 a)) False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (Not (r1 (skS.0 0 a) (skS.0 2 a a_1))) False)) % 9.34/9.64 Clause #126 (by clausification #[124]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (p100 (skS.0 0 a)) False) % 9.34/9.64 (Or (Eq (p101 (skS.0 0 a)) True) % 9.34/9.64 (Eq (And (And (Not (p2 (skS.0 2 a a_1))) (Not (p102 (skS.0 2 a a_1)))) (p101 (skS.0 2 a a_1))) True)) % 9.34/9.64 Clause #128 (by clausification #[126]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (p100 (skS.0 0 a)) False) % 9.34/9.64 (Or (Eq (p101 (skS.0 0 a)) True) (Eq (And (Not (p2 (skS.0 2 a a_1))) (Not (p102 (skS.0 2 a a_1)))) True)) % 9.34/9.64 Clause #133 (by clausification #[125]): ∀ (a a_1 : Iota), % 9.34/9.64 Or (Eq (p100 (skS.0 0 a)) False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (r1 (skS.0 0 a) (skS.0 2 a a_1)) True)) % 9.34/9.64 Clause #134 (by forward demodulation #[133, 8]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (r1 (skS.0 0 a) (skS.0 2 a a_1)) True)) % 9.34/9.64 Clause #135 (by clausification #[134]): ∀ (a a_1 : Iota), Or (Eq (p101 (skS.0 0 a)) True) (Eq (r1 (skS.0 0 a) (skS.0 2 a a_1)) True) % 9.34/9.64 Clause #136 (by forward demodulation #[135, 16]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (r1 (skS.0 0 a) (skS.0 2 a a_1)) True) % 9.34/9.64 Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 0 a) (skS.0 2 a a_1)) True % 9.34/9.65 Clause #138 (by superposition #[137, 13]): ∀ (a a_1 : Iota), Or (Eq (p2 (skS.0 2 a a_1)) True) (Eq True False) % 9.34/9.65 Clause #140 (by clausification #[138]): ∀ (a a_1 : Iota), Eq (p2 (skS.0 2 a a_1)) True % 9.34/9.65 Clause #159 (by clausification #[128]): ∀ (a a_1 : Iota), % 9.34/9.65 Or (Eq (p100 (skS.0 0 a)) False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (Not (p2 (skS.0 2 a a_1))) True)) % 9.34/9.65 Clause #165 (by clausification #[159]): ∀ (a a_1 : Iota), Or (Eq (p100 (skS.0 0 a)) False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (p2 (skS.0 2 a a_1)) False)) % 9.34/9.65 Clause #166 (by forward demodulation #[165, 8]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (p101 (skS.0 0 a)) True) (Eq (p2 (skS.0 2 a a_1)) False)) % 9.34/9.65 Clause #167 (by clausification #[166]): ∀ (a a_1 : Iota), Or (Eq (p101 (skS.0 0 a)) True) (Eq (p2 (skS.0 2 a a_1)) False) % 9.34/9.65 Clause #168 (by forward demodulation #[167, 16]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (p2 (skS.0 2 a a_1)) False) % 9.34/9.65 Clause #169 (by clausification #[168]): ∀ (a a_1 : Iota), Eq (p2 (skS.0 2 a a_1)) False % 9.34/9.65 Clause #170 (by superposition #[169, 140]): Eq False True % 9.34/9.65 Clause #171 (by clausification #[170]): False % 9.34/9.65 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------