%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL654+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:16 AM UTC 2026 % Result : Theorem 183.34s 183.63s % Output : Proof 184.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL654+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : duper %s % 0.08/0.36 % Computer : n007.cluster.edu % 0.08/0.36 % Model : x86_64 x86_64 % 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.36 % Memory : 8046.5625MB % 0.08/0.36 % OS : Linux 6.8.0-71-generic % 0.08/0.36 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Sat Sep 5 00:35:54 UTC 2026 % 0.08/0.36 % CPUTime : % 183.34/183.63 SZS status Theorem for theBenchmark.p % 183.34/183.63 SZS output start Proof for theBenchmark.p % 183.34/183.63 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), r1 X X) True % 183.34/183.63 Clause #1 (by assumption #[]): Eq % 183.34/183.63 (Not % 183.34/183.63 (Not % 183.34/183.63 (Exists fun X => % 183.34/183.63 Not % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Not (r1 X Y)) % 183.34/183.63 (Not % 183.34/183.63 (And % 183.34/183.63 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.34/183.63 (p1 Y))))) % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Not (r1 X Y)) % 183.34/183.63 (∀ (X : Iota), % 183.34/183.63 Or (Not (r1 Y X)) % 183.34/183.63 (Not % 183.34/183.63 (And % 183.34/183.63 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.34/183.63 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Not (r1 X Y)) % 183.34/183.63 (Not % 183.34/183.63 (And % 183.34/183.63 (Not % 183.34/183.63 (∀ (X : Iota), % 183.34/183.63 Or (Not (r1 Y X)) % 183.34/183.63 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.34/183.63 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))))) % 183.34/183.63 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Or (Not (r1 X Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.34/183.63 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))))) % 183.34/183.63 True % 183.34/183.63 Clause #2 (by clausification #[0]): ∀ (a : Iota), Eq (r1 a a) True % 183.34/183.63 Clause #3 (by clausification #[1]): Eq % 183.34/183.63 (Not % 183.34/183.63 (Exists fun X => % 183.34/183.63 Not % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Not (r1 X Y)) % 183.34/183.63 (Not % 183.34/183.63 (And % 183.34/183.63 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.34/183.63 (p1 Y))))) % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Not (r1 X Y)) % 183.34/183.63 (∀ (X : Iota), % 183.34/183.63 Or (Not (r1 Y X)) % 183.34/183.63 (Not % 183.34/183.63 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.34/183.63 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Not (r1 X Y)) % 183.34/183.63 (Not % 183.34/183.63 (And % 183.34/183.63 (Not % 183.34/183.63 (∀ (X : Iota), % 183.34/183.63 Or (Not (r1 Y X)) % 183.34/183.63 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.34/183.63 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))))) % 183.34/183.63 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Or (Not (r1 X Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.34/183.63 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.34/183.63 False % 183.34/183.63 Clause #4 (by clausification #[3]): Eq % 183.34/183.63 (Exists fun X => % 183.34/183.63 Not % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Or % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.63 Or (Not (r1 X Y)) % 183.34/183.63 (Not % 183.34/183.63 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.34/183.63 (p1 Y))))) % 183.34/183.63 (Not % 183.34/183.63 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 X Y)) % 183.34/183.68 (∀ (X : Iota), % 183.34/183.68 Or (Not (r1 Y X)) % 183.34/183.68 (Not % 183.34/183.68 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.34/183.68 (Not % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 X Y)) % 183.34/183.68 (Not % 183.34/183.68 (And % 183.34/183.68 (Not % 183.34/183.68 (∀ (X : Iota), % 183.34/183.68 Or (Not (r1 Y X)) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.34/183.68 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))))) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Or (Not (r1 X Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.34/183.68 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 183.34/183.68 True % 183.34/183.68 Clause #5 (by clausification #[4]): ∀ (a : Iota), % 183.34/183.68 Eq % 183.34/183.68 (Not % 183.34/183.68 (Or % 183.34/183.68 (Or % 183.34/183.68 (Or % 183.34/183.68 (Or % 183.34/183.68 (Not % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 (skS.0 0 a) Y)) % 183.34/183.68 (Not % 183.34/183.68 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.34/183.68 (p1 Y))))) % 183.34/183.68 (Not % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 (skS.0 0 a) Y)) % 183.34/183.68 (∀ (X : Iota), % 183.34/183.68 Or (Not (r1 Y X)) % 183.34/183.68 (Not % 183.34/183.68 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.34/183.68 (Not % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 (skS.0 0 a) Y)) % 183.34/183.68 (Not % 183.34/183.68 (And % 183.34/183.68 (Not % 183.34/183.68 (∀ (X : Iota), % 183.34/183.68 Or (Not (r1 Y X)) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.34/183.68 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))))) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Or (Not (r1 (skS.0 0 a) Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.34/183.68 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 183.34/183.68 True % 183.34/183.68 Clause #6 (by clausification #[5]): ∀ (a : Iota), % 183.34/183.68 Eq % 183.34/183.68 (Or % 183.34/183.68 (Or % 183.34/183.68 (Or % 183.34/183.68 (Or % 183.34/183.68 (Not % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 (skS.0 0 a) Y)) % 183.34/183.68 (Not % 183.34/183.68 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.34/183.68 (p1 Y))))) % 183.34/183.68 (Not % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 (skS.0 0 a) Y)) % 183.34/183.68 (∀ (X : Iota), % 183.34/183.68 Or (Not (r1 Y X)) % 183.34/183.68 (Not % 183.34/183.68 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.34/183.68 (Not % 183.34/183.68 (∀ (Y : Iota), % 183.34/183.68 Or (Not (r1 (skS.0 0 a) Y)) % 183.34/183.68 (Not % 183.34/183.68 (And % 183.34/183.68 (Not % 183.34/183.68 (∀ (X : Iota), % 183.34/183.68 Or (Not (r1 Y X)) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.34/183.68 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))))) % 183.34/183.68 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 183.44/183.74 (∀ (Y : Iota), % 183.44/183.74 Or (Or (Not (r1 (skS.0 0 a) Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.44/183.74 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.44/183.74 False % 183.44/183.74 Clause #7 (by clausification #[6]): ∀ (a : Iota), % 183.44/183.74 Eq % 183.44/183.74 (∀ (Y : Iota), % 183.44/183.74 Or (Or (Not (r1 (skS.0 0 a) Y)) (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.44/183.74 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))) % 183.44/183.74 False % 183.44/183.74 Clause #8 (by clausification #[6]): ∀ (a : Iota), % 183.44/183.74 Eq % 183.44/183.74 (Or % 183.44/183.74 (Or % 183.44/183.74 (Or % 183.44/183.74 (Not % 183.44/183.74 (∀ (Y : Iota), % 183.44/183.74 Or (Not (r1 (skS.0 0 a) Y)) % 183.44/183.74 (Not % 183.44/183.74 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.44/183.74 (p1 Y))))) % 183.44/183.74 (Not % 183.44/183.74 (∀ (Y : Iota), % 183.44/183.74 Or (Not (r1 (skS.0 0 a) Y)) % 183.44/183.74 (∀ (X : Iota), % 183.44/183.74 Or (Not (r1 Y X)) % 183.44/183.74 (Not % 183.44/183.74 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.44/183.74 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.44/183.74 (Not % 183.44/183.74 (∀ (Y : Iota), % 183.44/183.74 Or (Not (r1 (skS.0 0 a) Y)) % 183.44/183.74 (Not % 183.44/183.74 (And % 183.44/183.74 (Not % 183.44/183.74 (∀ (X : Iota), % 183.44/183.74 Or (Not (r1 Y X)) % 183.44/183.74 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.44/183.74 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))))) % 183.44/183.74 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 183.44/183.74 False % 183.44/183.74 Clause #9 (by clausification #[7]): ∀ (a a_1 : Iota), % 183.44/183.74 Eq % 183.44/183.74 (Not % 183.44/183.74 (Or % 183.44/183.74 (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) % 183.44/183.74 (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.44/183.74 (Not (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X))))) % 183.44/183.74 True % 183.44/183.74 Clause #10 (by clausification #[9]): ∀ (a a_1 : Iota), % 183.44/183.74 Eq % 183.44/183.74 (Or % 183.44/183.74 (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) % 183.44/183.74 (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.44/183.74 (Not (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X)))) % 183.44/183.74 False % 183.44/183.74 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Eq (Not (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X))) False % 183.44/183.74 Clause #12 (by clausification #[10]): ∀ (a a_1 : Iota), % 183.44/183.74 Eq % 183.44/183.74 (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) % 183.44/183.74 (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 183.44/183.74 False % 183.44/183.74 Clause #13 (by clausification #[11]): ∀ (a a_1 : Iota), Eq (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X)) True % 183.44/183.74 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 : Iota), Eq (Or (Not (r1 (skS.0 1 a a_1) a_2)) (p1 a_2)) True % 183.44/183.74 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 : Iota), Or (Eq (Not (r1 (skS.0 1 a a_1) a_2)) True) (Eq (p1 a_2) True) % 183.44/183.74 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), Or (Eq (p1 a) True) (Eq (r1 (skS.0 1 a_1 a_2) a) False) % 183.44/183.74 Clause #19 (by clausification #[12]): ∀ (a a_1 : Iota), Eq (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) False % 183.44/183.74 Clause #20 (by clausification #[12]): ∀ (a a_1 : Iota), Eq (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) False % 183.44/183.74 Clause #21 (by clausification #[19]): ∀ (a a_1 a_2 : Iota), % 183.44/183.74 Eq % 183.44/183.74 (Not (Or (Not (r1 (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) (∀ (Y : Iota), Or (Not (r1 (skS.0 2 a a_1 a_2) Y)) (p1 Y)))) % 183.44/183.74 True % 183.44/183.74 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), % 183.44/183.74 Eq (Or (Not (r1 (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) (∀ (Y : Iota), Or (Not (r1 (skS.0 2 a a_1 a_2) Y)) (p1 Y))) % 183.44/183.74 False % 183.44/183.74 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Y : Iota), Or (Not (r1 (skS.0 2 a a_1 a_2) Y)) (p1 Y)) False % 183.44/183.74 Clause #24 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), Eq (Not (r1 (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) False % 183.54/183.80 Clause #25 (by clausification #[23]): ∀ (a a_1 a_2 a_3 : Iota), % 183.54/183.80 Eq (Not (Or (Not (r1 (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) (p1 (skS.0 3 a a_1 a_2 a_3)))) True % 183.54/183.80 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 a_3 : Iota), % 183.54/183.80 Eq (Or (Not (r1 (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) (p1 (skS.0 3 a a_1 a_2 a_3))) False % 183.54/183.80 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), Eq (p1 (skS.0 3 a a_1 a_2 a_3)) False % 183.54/183.80 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Not (r1 (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) False % 183.54/183.80 Clause #29 (by clausification #[20]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 0 a) (skS.0 1 a a_1)) True % 183.54/183.80 Clause #31 (by clausification #[8]): ∀ (a : Iota), % 183.54/183.80 Eq % 183.54/183.80 (Or % 183.54/183.80 (Or % 183.54/183.80 (Not % 183.54/183.80 (∀ (Y : Iota), % 183.54/183.80 Or (Not (r1 (skS.0 0 a) Y)) % 183.54/183.80 (Not % 183.54/183.80 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.54/183.80 (p1 Y))))) % 183.54/183.80 (Not % 183.54/183.80 (∀ (Y : Iota), % 183.54/183.80 Or (Not (r1 (skS.0 0 a) Y)) % 183.54/183.80 (∀ (X : Iota), % 183.54/183.80 Or (Not (r1 Y X)) % 183.54/183.80 (Not % 183.54/183.80 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.54/183.80 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.54/183.80 (Not % 183.54/183.80 (∀ (Y : Iota), % 183.54/183.80 Or (Not (r1 (skS.0 0 a) Y)) % 183.54/183.80 (Not % 183.54/183.80 (And % 183.54/183.80 (Not % 183.54/183.80 (∀ (X : Iota), % 183.54/183.80 Or (Not (r1 Y X)) % 183.54/183.80 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.80 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))))) % 183.54/183.80 False % 183.54/183.80 Clause #44 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True % 183.54/183.80 Clause #49 (by clausification #[28]): ∀ (a a_1 a_2 a_3 : Iota), Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) True % 183.54/183.80 Clause #50 (by clausification #[31]): ∀ (a : Iota), % 183.54/183.80 Eq % 183.54/183.80 (Not % 183.54/183.80 (∀ (Y : Iota), % 183.54/183.80 Or (Not (r1 (skS.0 0 a) Y)) % 183.54/183.80 (Not % 183.54/183.80 (And % 183.54/183.80 (Not % 183.54/183.80 (∀ (X : Iota), % 183.54/183.80 Or (Not (r1 Y X)) % 183.54/183.80 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.80 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.54/183.80 False % 183.54/183.80 Clause #51 (by clausification #[31]): ∀ (a : Iota), % 183.54/183.80 Eq % 183.54/183.80 (Or % 183.54/183.80 (Not % 183.54/183.80 (∀ (Y : Iota), % 183.54/183.80 Or (Not (r1 (skS.0 0 a) Y)) % 183.54/183.80 (Not % 183.54/183.80 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 183.54/183.80 (p1 Y))))) % 183.54/183.80 (Not % 183.54/183.80 (∀ (Y : Iota), % 183.54/183.80 Or (Not (r1 (skS.0 0 a) Y)) % 183.54/183.80 (∀ (X : Iota), % 183.54/183.80 Or (Not (r1 Y X)) % 183.54/183.80 (Not % 183.54/183.80 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.54/183.80 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))))) % 183.54/183.80 False % 183.54/183.80 Clause #52 (by clausification #[50]): ∀ (a : Iota), % 183.54/183.80 Eq % 183.54/183.80 (∀ (Y : Iota), % 183.54/183.80 Or (Not (r1 (skS.0 0 a) Y)) % 183.54/183.80 (Not % 183.54/183.80 (And % 183.54/183.80 (Not % 183.54/183.80 (∀ (X : Iota), % 183.54/183.80 Or (Not (r1 Y X)) % 183.54/183.80 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.80 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))) % 183.54/183.80 True % 183.54/183.80 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), % 183.54/183.80 Eq % 183.54/183.80 (Or (Not (r1 (skS.0 0 a) a_1)) % 183.54/183.80 (Not % 183.54/183.80 (And % 183.54/183.80 (Not % 183.54/183.80 (∀ (X : Iota), % 183.54/183.80 Or (Not (r1 a_1 X)) % 183.54/183.80 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.80 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))) % 183.54/183.87 True % 183.54/183.87 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), % 183.54/183.87 Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) % 183.54/183.87 (Eq % 183.54/183.87 (Not % 183.54/183.87 (And % 183.54/183.87 (Not % 183.54/183.87 (∀ (X : Iota), % 183.54/183.87 Or (Not (r1 a_1 X)) % 183.54/183.87 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.87 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))) % 183.54/183.87 True) % 183.54/183.87 Clause #55 (by clausification #[54]): ∀ (a a_1 : Iota), % 183.54/183.87 Or % 183.54/183.87 (Eq % 183.54/183.87 (Not % 183.54/183.87 (And % 183.54/183.87 (Not % 183.54/183.87 (∀ (X : Iota), % 183.54/183.87 Or (Not (r1 a X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.87 (Not (∀ (X : Iota), Or (Not (r1 a X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))) % 183.54/183.87 True) % 183.54/183.87 (Eq (r1 (skS.0 0 a_1) a) False) % 183.54/183.87 Clause #56 (by clausification #[55]): ∀ (a a_1 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Eq % 183.54/183.87 (And % 183.54/183.87 (Not % 183.54/183.87 (∀ (X : Iota), % 183.54/183.87 Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.87 (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))) % 183.54/183.87 False) % 183.54/183.87 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or % 183.54/183.87 (Eq % 183.54/183.87 (Not % 183.54/183.87 (∀ (X : Iota), % 183.54/183.87 Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 183.54/183.87 False) % 183.54/183.87 (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) False)) % 183.54/183.87 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) False) % 183.54/183.87 (Eq % 183.54/183.87 (∀ (X : Iota), % 183.54/183.87 Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 183.54/183.87 True)) % 183.54/183.87 Clause #59 (by clausification #[58]): ∀ (a a_1 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or % 183.54/183.87 (Eq % 183.54/183.87 (∀ (X : Iota), % 183.54/183.87 Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 183.54/183.87 True) % 183.54/183.87 (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) True)) % 183.54/183.87 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) True) % 183.54/183.87 (Eq % 183.54/183.87 (Or (Not (r1 a_1 a_2)) (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 183.54/183.87 True)) % 183.54/183.87 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or % 183.54/183.87 (Eq % 183.54/183.87 (Or (Not (r1 a_1 a_2)) (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 183.54/183.87 True) % 183.54/183.87 (Eq (Or (Not (r1 a_1 a_3)) (Not (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (p1 Y)))) True)) % 183.54/183.87 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or (Eq (Or (Not (r1 a_1 a_2)) (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)))) True) % 183.54/183.87 (Or (Eq (Not (r1 a_1 a_3)) True) % 183.54/183.87 (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) True))) % 183.54/183.87 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or (Eq (Not (r1 a_1 a_2)) True) % 183.54/183.87 (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) True) % 183.54/183.87 (Or (Eq (Not (r1 a_1 a_3)) True) (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (p1 Y))) True)))) % 183.54/183.87 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 : Iota), % 183.54/183.87 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.54/183.87 (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) True) % 183.54/183.87 (Or (Eq (Not (r1 a_1 a_3)) True) % 183.54/183.87 (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (p1 Y))) True) (Eq (r1 a_1 a_2) False)))) % 183.64/183.94 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (Not (r1 a_1 a_2)) True) % 183.64/183.94 (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))) True) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.94 (Eq (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))) False)))) % 183.64/183.94 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))) True) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.94 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))) False) % 183.64/183.94 (Eq (r1 a_1 a_2) False)))) % 183.64/183.94 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.94 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) (Eq (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (p1 Y)) False)))) % 183.64/183.94 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.94 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (p1 Y)) False) % 183.64/183.94 (Eq (Not (Or (Not (r1 a_2 (skS.0 5 a_2 a_4))) (Not (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_4) X)) (p1 X))))) % 183.64/183.94 True)))) % 183.64/183.94 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.94 (Or % 183.64/183.94 (Eq (Not (Or (Not (r1 a_2 (skS.0 5 a_2 a_4))) (Not (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_4) X)) (p1 X))))) % 183.64/183.94 True) % 183.64/183.94 (Eq (Not (Or (Not (r1 a_3 (skS.0 6 a_3 a_5))) (p1 (skS.0 6 a_3 a_5)))) True)))) % 183.64/183.94 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.94 (Or (Eq (Not (Or (Not (r1 a_3 (skS.0 6 a_3 a_4))) (p1 (skS.0 6 a_3 a_4)))) True) % 183.64/183.94 (Eq (Or (Not (r1 a_2 (skS.0 5 a_2 a_5))) (Not (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_5) X)) (p1 X)))) % 183.64/183.94 False)))) % 183.64/183.94 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.94 (Or % 183.64/183.94 (Eq (Or (Not (r1 a_2 (skS.0 5 a_2 a_4))) (Not (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_4) X)) (p1 X)))) % 183.64/183.94 False) % 183.64/183.94 (Eq (Or (Not (r1 a_3 (skS.0 6 a_3 a_5))) (p1 (skS.0 6 a_3 a_5))) False)))) % 183.64/183.94 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/183.94 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.94 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.94 (Or (Eq (Or (Not (r1 a_3 (skS.0 6 a_3 a_4))) (p1 (skS.0 6 a_3 a_4))) False) % 183.64/183.94 (Eq (Not (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_5) X)) (p1 X))) False)))) % 183.64/183.95 Clause #73 (by clausification #[71]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/183.95 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.95 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.95 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.95 (Or (Eq (Or (Not (r1 a_3 (skS.0 6 a_3 a_4))) (p1 (skS.0 6 a_3 a_4))) False) % 183.64/183.95 (Eq (Not (r1 a_2 (skS.0 5 a_2 a_5))) False)))) % 183.64/183.95 Clause #74 (by clausification #[72]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/183.95 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.95 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.95 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.95 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_4) X)) (p1 X))) False) % 183.64/183.95 (Eq (p1 (skS.0 6 a_3 a_5)) False)))) % 183.64/183.95 Clause #75 (by clausification #[72]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/183.95 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/183.95 (Or (Eq (r1 a_1 a_2) False) % 183.64/183.95 (Or (Eq (r1 a_1 a_3) False) % 183.64/183.95 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_4) X)) (p1 X))) False) % 183.64/183.95 (Eq (Not (r1 a_3 (skS.0 6 a_3 a_5))) False)))) % 183.64/183.95 Clause #76 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_2) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_3) False) % 183.64/184.01 (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Eq (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_5) X)) (p1 X)) True)))) % 183.64/184.01 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_2) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_3) False) % 183.64/184.01 (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Eq (Or (Not (r1 (skS.0 5 a_2 a_5) a_6)) (p1 a_6)) True)))) % 183.64/184.01 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_2) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_3) False) % 183.64/184.01 (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Or (Eq (Not (r1 (skS.0 5 a_2 a_5) a_6)) True) (Eq (p1 a_6) True))))) % 183.64/184.01 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_2) False) % 183.64/184.01 (Or (Eq (r1 a_1 a_3) False) % 183.64/184.01 (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Or (Eq (p1 a_5) True) (Eq (r1 (skS.0 5 a_2 a_6) a_5) False))))) % 183.64/184.01 Clause #80 (by superposition #[79, 29]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.64/184.01 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) % 183.64/184.01 (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) % 183.64/184.01 (Or (Eq (p1 a_5) True) (Or (Eq (r1 (skS.0 5 a_2 a_6) a_5) False) (Eq False True))))) % 183.64/184.01 Clause #95 (by clausification #[51]): ∀ (a : Iota), % 183.64/184.01 Eq % 183.64/184.01 (Not % 183.64/184.01 (∀ (Y : Iota), % 183.64/184.01 Or (Not (r1 (skS.0 0 a) Y)) % 183.64/184.01 (∀ (X : Iota), % 183.64/184.01 Or (Not (r1 Y X)) % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.64/184.01 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))))) % 183.64/184.01 False % 183.64/184.01 Clause #97 (by clausification #[95]): ∀ (a : Iota), % 183.64/184.01 Eq % 183.64/184.01 (∀ (Y : Iota), % 183.64/184.01 Or (Not (r1 (skS.0 0 a) Y)) % 183.64/184.01 (∀ (X : Iota), % 183.64/184.01 Or (Not (r1 Y X)) % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.64/184.01 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))) % 183.64/184.01 True % 183.64/184.01 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), % 183.64/184.01 Eq % 183.64/184.01 (Or (Not (r1 (skS.0 0 a) a_1)) % 183.64/184.01 (∀ (X : Iota), % 183.64/184.01 Or (Not (r1 a_1 X)) % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.64/184.01 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))))) % 183.64/184.01 True % 183.64/184.01 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), % 183.64/184.01 Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) % 183.64/184.01 (Eq % 183.64/184.01 (∀ (X : Iota), % 183.64/184.01 Or (Not (r1 a_1 X)) % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.64/184.01 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))) % 183.64/184.01 True) % 183.64/184.01 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), % 183.64/184.01 Or % 183.64/184.01 (Eq % 183.64/184.01 (∀ (X : Iota), % 183.64/184.01 Or (Not (r1 a X)) % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.64/184.01 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))))) % 183.64/184.01 True) % 183.64/184.01 (Eq (r1 (skS.0 0 a_1) a) False) % 183.64/184.01 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/184.01 (Eq % 183.64/184.01 (Or (Not (r1 a_1 a_2)) % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.64/184.01 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)))))) % 183.64/184.01 True) % 183.64/184.01 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/184.01 (Or (Eq (Not (r1 a_1 a_2)) True) % 183.64/184.01 (Eq % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.64/184.01 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))))) % 183.64/184.01 True)) % 183.64/184.01 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 : Iota), % 183.64/184.01 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.64/184.01 (Or % 183.64/184.01 (Eq % 183.64/184.01 (Not % 183.64/184.01 (And (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.76/184.08 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))))) % 183.76/184.08 True) % 183.76/184.08 (Eq (r1 a_1 a_2) False)) % 183.76/184.08 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Eq % 183.76/184.08 (And (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 183.76/184.08 (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)))) % 183.76/184.08 False)) % 183.76/184.08 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) False) % 183.76/184.08 (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))) False))) % 183.76/184.08 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))) False) % 183.76/184.08 (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))) True))) % 183.76/184.08 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))) True) % 183.76/184.08 (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)) True))) % 183.76/184.08 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)) True) % 183.76/184.08 (Eq (Or (Not (r1 a_2 a_3)) (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (p1 X)))) True))) % 183.76/184.08 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (Or (Not (r1 a_2 a_3)) (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (p1 X)))) True) % 183.76/184.08 (Eq (Or (Not (r1 a_2 a_4)) (p1 a_4)) True))) % 183.76/184.08 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (Or (Not (r1 a_2 a_3)) (p1 a_3)) True) % 183.76/184.08 (Or (Eq (Not (r1 a_2 a_4)) True) (Eq (Not (∀ (X : Iota), Or (Not (r1 a_4 X)) (p1 X))) True)))) % 183.76/184.08 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (Not (r1 a_2 a_3)) True) % 183.76/184.08 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (p1 X))) True) % 183.76/184.08 (Or (Eq (Not (r1 a_2 a_4)) True) (Eq (p1 a_4) True))))) % 183.76/184.08 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a_3 X)) (p1 X))) True) % 183.76/184.08 (Or (Eq (Not (r1 a_2 a_4)) True) (Or (Eq (p1 a_4) True) (Eq (r1 a_2 a_3) False))))) % 183.76/184.08 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (Not (r1 a_2 a_3)) True) % 183.76/184.08 (Or (Eq (p1 a_3) True) (Or (Eq (r1 a_2 a_4) False) (Eq (∀ (X : Iota), Or (Not (r1 a_4 X)) (p1 X)) False))))) % 183.76/184.08 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (p1 a_3) True) % 183.76/184.08 (Or (Eq (r1 a_2 a_4) False) % 183.76/184.08 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_4 X)) (p1 X)) False) (Eq (r1 a_2 a_3) False))))) % 183.76/184.08 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (p1 a_3) True) % 183.76/184.08 (Or (Eq (r1 a_2 a_4) False) % 183.76/184.08 (Or (Eq (r1 a_2 a_3) False) (Eq (Not (Or (Not (r1 a_4 (skS.0 7 a_4 a_5))) (p1 (skS.0 7 a_4 a_5)))) True))))) % 183.76/184.08 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.76/184.08 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.76/184.08 (Or (Eq (r1 a_1 a_2) False) % 183.76/184.08 (Or (Eq (p1 a_3) True) % 183.76/184.08 (Or (Eq (r1 a_2 a_4) False) % 183.87/184.15 (Or (Eq (r1 a_2 a_3) False) (Eq (Or (Not (r1 a_4 (skS.0 7 a_4 a_5))) (p1 (skS.0 7 a_4 a_5))) False))))) % 183.87/184.15 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (p1 a_3) True) % 183.87/184.15 (Or (Eq (r1 a_2 a_4) False) (Or (Eq (r1 a_2 a_3) False) (Eq (p1 (skS.0 7 a_4 a_5)) False))))) % 183.87/184.15 Clause #118 (by clausification #[116]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (p1 a_3) True) % 183.87/184.15 (Or (Eq (r1 a_2 a_4) False) (Or (Eq (r1 a_2 a_3) False) (Eq (Not (r1 a_4 (skS.0 7 a_4 a_5))) False))))) % 183.87/184.15 Clause #119 (by superposition #[117, 29]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.87/184.15 (Or (Eq (p1 a_3) True) % 183.87/184.15 (Or (Eq (r1 a_2 a_4) False) (Or (Eq (r1 a_2 a_3) False) (Or (Eq (p1 (skS.0 7 a_4 a_5)) False) (Eq False True))))) % 183.87/184.15 Clause #136 (by clausification #[73]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) (Or (Eq (Not (r1 a_2 (skS.0 5 a_2 a_4))) False) (Eq (p1 (skS.0 6 a_3 a_5)) False)))) % 183.87/184.15 Clause #137 (by clausification #[73]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) % 183.87/184.15 (Or (Eq (Not (r1 a_2 (skS.0 5 a_2 a_4))) False) (Eq (Not (r1 a_3 (skS.0 6 a_3 a_5))) False)))) % 183.87/184.15 Clause #138 (by clausification #[136]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Eq (r1 a_2 (skS.0 5 a_2 a_5)) True)))) % 183.87/184.15 Clause #139 (by superposition #[138, 29]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.87/184.15 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) % 183.87/184.15 (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Or (Eq (r1 a_2 (skS.0 5 a_2 a_5)) True) (Eq False True)))) % 183.87/184.15 Clause #150 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) % 183.87/184.15 (Or (Eq (Not (r1 a_3 (skS.0 6 a_3 a_4))) False) % 183.87/184.15 (Eq (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_5) X)) (p1 X)) True)))) % 183.87/184.15 Clause #151 (by clausification #[150]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) % 183.87/184.15 (Or (Eq (∀ (X : Iota), Or (Not (r1 (skS.0 5 a_2 a_4) X)) (p1 X)) True) (Eq (r1 a_3 (skS.0 6 a_3 a_5)) True)))) % 183.87/184.15 Clause #152 (by clausification #[151]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) % 183.87/184.15 (Or (Eq (r1 a_3 (skS.0 6 a_3 a_4)) True) (Eq (Or (Not (r1 (skS.0 5 a_2 a_5) a_6)) (p1 a_6)) True)))) % 183.87/184.15 Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) % 183.87/184.15 (Or (Eq (r1 a_3 (skS.0 6 a_3 a_4)) True) (Or (Eq (Not (r1 (skS.0 5 a_2 a_5) a_6)) True) (Eq (p1 a_6) True))))) % 183.87/184.15 Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_2) False) % 183.87/184.15 (Or (Eq (r1 a_1 a_3) False) % 183.87/184.15 (Or (Eq (r1 a_3 (skS.0 6 a_3 a_4)) True) (Or (Eq (p1 a_5) True) (Eq (r1 (skS.0 5 a_2 a_6) a_5) False))))) % 183.87/184.15 Clause #155 (by superposition #[154, 29]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.87/184.15 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) % 183.87/184.15 (Or (Eq (r1 a_3 (skS.0 6 a_3 a_4)) True) % 183.87/184.15 (Or (Eq (p1 a_5) True) (Or (Eq (r1 (skS.0 5 a_2 a_6) a_5) False) (Eq False True))))) % 183.87/184.15 Clause #158 (by clausification #[119]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.87/184.15 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.87/184.15 (Or (Eq (p1 a_3) True) (Or (Eq (r1 a_2 a_4) False) (Or (Eq (r1 a_2 a_3) False) (Eq (p1 (skS.0 7 a_4 a_5)) False)))) % 183.87/184.15 Clause #159 (by superposition #[158, 44]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (p1 a) True) % 183.94/184.22 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a_4) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) (Or (Eq (p1 (skS.0 7 a_4 a_5)) False) (Eq False True)))) % 183.94/184.22 Clause #186 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) % 183.94/184.22 (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Or (Eq (p1 a_5) True) (Eq (r1 (skS.0 5 a_2 a_6) a_5) False)))) % 183.94/184.22 Clause #187 (by superposition #[186, 44]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (p1 (skS.0 6 a_2 a_3)) False) % 183.94/184.22 (Or (Eq (p1 a_4) True) (Or (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_5) a_6) a_4) False) (Eq False True)))) % 183.94/184.22 Clause #221 (by clausification #[118]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.94/184.22 (Or (Eq (r1 a_1 a_2) False) % 183.94/184.22 (Or (Eq (p1 a_3) True) % 183.94/184.22 (Or (Eq (r1 a_2 a_4) False) (Or (Eq (r1 a_2 a_3) False) (Eq (r1 a_4 (skS.0 7 a_4 a_5)) True))))) % 183.94/184.22 Clause #222 (by superposition #[221, 29]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (p1 a_3) True) % 183.94/184.22 (Or (Eq (r1 a_2 a_4) False) % 183.94/184.22 (Or (Eq (r1 a_2 a_3) False) (Or (Eq (r1 a_4 (skS.0 7 a_4 a_5)) True) (Eq False True))))) % 183.94/184.22 Clause #233 (by clausification #[222]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (p1 a_3) True) % 183.94/184.22 (Or (Eq (r1 a_2 a_4) False) (Or (Eq (r1 a_2 a_3) False) (Eq (r1 a_4 (skS.0 7 a_4 a_5)) True)))) % 183.94/184.22 Clause #234 (by superposition #[233, 44]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (p1 a) True) % 183.94/184.22 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a_4) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) (Or (Eq (r1 a_4 (skS.0 7 a_4 a_5)) True) (Eq False True)))) % 183.94/184.22 Clause #336 (by clausification #[137]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.94/184.22 (Or (Eq (r1 a_1 a_2) False) % 183.94/184.22 (Or (Eq (r1 a_1 a_3) False) % 183.94/184.22 (Or (Eq (Not (r1 a_3 (skS.0 6 a_3 a_4))) False) (Eq (r1 a_2 (skS.0 5 a_2 a_5)) True)))) % 183.94/184.22 Clause #337 (by clausification #[336]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 0 a) a_1) False) % 183.94/184.22 (Or (Eq (r1 a_1 a_2) False) % 183.94/184.22 (Or (Eq (r1 a_1 a_3) False) (Or (Eq (r1 a_2 (skS.0 5 a_2 a_4)) True) (Eq (r1 a_3 (skS.0 6 a_3 a_5)) True)))) % 183.94/184.22 Clause #338 (by superposition #[337, 29]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) % 183.94/184.22 (Or (Eq (r1 a_2 (skS.0 5 a_2 a_4)) True) (Or (Eq (r1 a_3 (skS.0 6 a_3 a_5)) True) (Eq False True)))) % 183.94/184.22 Clause #372 (by clausification #[139]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) (Or (Eq (p1 (skS.0 6 a_3 a_4)) False) (Eq (r1 a_2 (skS.0 5 a_2 a_5)) True))) % 183.94/184.22 Clause #373 (by superposition #[372, 44]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (p1 (skS.0 6 a_2 a_3)) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 2 a a_1 a_4) (skS.0 5 (skS.0 2 a a_1 a_4) a_5)) True) (Eq False True))) % 183.94/184.22 Clause #412 (by clausification #[155]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) % 183.94/184.22 (Or (Eq (r1 a_3 (skS.0 6 a_3 a_4)) True) (Or (Eq (p1 a_5) True) (Eq (r1 (skS.0 5 a_2 a_6) a_5) False)))) % 183.94/184.22 Clause #413 (by superposition #[412, 44]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (r1 a_2 (skS.0 6 a_2 a_3)) True) % 183.94/184.22 (Or (Eq (p1 a_4) True) (Or (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_5) a_6) a_4) False) (Eq False True)))) % 183.94/184.22 Clause #452 (by clausification #[159]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.22 Or (Eq (p1 a) True) % 183.94/184.22 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a_4) False) % 183.94/184.22 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) (Eq (p1 (skS.0 7 a_4 a_5)) False))) % 183.94/184.22 Clause #520 (by clausification #[187]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.94/184.22 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.22 (Or (Eq (p1 (skS.0 6 a_2 a_3)) False) (Or (Eq (p1 a_4) True) (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_5) a_6) a_4) False))) % 183.94/184.29 Clause #524 (by superposition #[520, 2]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_2)) False) % 183.94/184.29 (Or (Eq (p1 a_3) True) (Or (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_4) a_5) a_3) False) (Eq False True))) % 183.94/184.29 Clause #528 (by clausification #[524]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_2)) False) % 183.94/184.29 (Or (Eq (p1 a_3) True) (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_4) a_5) a_3) False)) % 183.94/184.29 Clause #575 (by clausification #[234]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (p1 a) True) % 183.94/184.29 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a_4) False) % 183.94/184.29 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) (Eq (r1 a_4 (skS.0 7 a_4 a_5)) True))) % 183.94/184.29 Clause #908 (by clausification #[338]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.29 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) % 183.94/184.29 (Or (Eq (r1 a_2 (skS.0 5 a_2 a_4)) True) (Eq (r1 a_3 (skS.0 6 a_3 a_5)) True))) % 183.94/184.29 Clause #909 (by superposition #[908, 44]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.29 (Or (Eq (r1 (skS.0 2 a a_1 a_3) (skS.0 5 (skS.0 2 a a_1 a_3) a_4)) True) % 183.94/184.29 (Or (Eq (r1 a_2 (skS.0 6 a_2 a_5)) True) (Eq False True))) % 183.94/184.29 Clause #1002 (by clausification #[413]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.29 (Or (Eq (r1 a_2 (skS.0 6 a_2 a_3)) True) % 183.94/184.29 (Or (Eq (p1 a_4) True) (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_5) a_6) a_4) False))) % 183.94/184.29 Clause #1006 (by superposition #[1002, 2]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True) % 183.94/184.29 (Or (Eq (p1 a_3) True) (Or (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_4) a_5) a_3) False) (Eq False True))) % 183.94/184.29 Clause #1807 (by clausification #[1006]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True) % 183.94/184.29 (Or (Eq (p1 a_3) True) (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_4) a_5) a_3) False)) % 183.94/184.29 Clause #1950 (by clausification #[373]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.29 (Or (Eq (p1 (skS.0 6 a_2 a_3)) False) (Eq (r1 (skS.0 2 a a_1 a_4) (skS.0 5 (skS.0 2 a a_1 a_4) a_5)) True)) % 183.94/184.29 Clause #1956 (by superposition #[1950, 2]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.94/184.29 Or (Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_2)) False) % 183.94/184.29 (Or (Eq (r1 (skS.0 2 a a_1 a_3) (skS.0 5 (skS.0 2 a a_1 a_3) a_4)) True) (Eq False True)) % 183.94/184.29 Clause #1959 (by clausification #[1956]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.94/184.29 Or (Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_2)) False) (Eq (r1 (skS.0 2 a a_1 a_3) (skS.0 5 (skS.0 2 a a_1 a_3) a_4)) True) % 183.94/184.29 Clause #2454 (by clausification #[909]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 183.94/184.29 (Or (Eq (r1 (skS.0 2 a a_1 a_3) (skS.0 5 (skS.0 2 a a_1 a_3) a_4)) True) (Eq (r1 a_2 (skS.0 6 a_2 a_5)) True)) % 183.94/184.29 Clause #2459 (by superposition #[2454, 2]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) % 183.94/184.29 (Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_4)) True) (Eq False True)) % 183.94/184.29 Clause #3054 (by clausification #[2459]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) % 183.94/184.29 (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_4)) True) % 183.94/184.29 Clause #3062 (by superposition #[3054, 16]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) % 183.94/184.29 (Or (Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_4)) True) (Eq True False)) % 183.94/184.29 Clause #3085 (by clausification #[3062]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) (Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_4)) True) % 183.94/184.29 Clause #3101 (by superposition #[3085, 1959]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) % 183.94/184.29 (Or (Eq True False) (Eq (r1 (skS.0 2 a a_1 a_4) (skS.0 5 (skS.0 2 a a_1 a_4) a_5)) True)) % 183.94/184.29 Clause #3826 (by clausification #[3101]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 183.94/184.29 Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) % 184.04/184.35 (Eq (r1 (skS.0 2 a a_1 a_4) (skS.0 5 (skS.0 2 a a_1 a_4) a_5)) True) % 184.04/184.35 Clause #3833 (by equality factoring #[3826]): ∀ (a a_1 a_2 a_3 : Iota), Or (Ne True True) (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) % 184.04/184.35 Clause #3834 (by clausification #[3833]): ∀ (a a_1 a_2 a_3 : Iota), % 184.04/184.35 Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) (Or (Eq True False) (Eq True False)) % 184.04/184.35 Clause #3836 (by clausification #[3834]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True) (Eq True False) % 184.04/184.35 Clause #3837 (by clausification #[3836]): ∀ (a a_1 a_2 a_3 : Iota), Eq (r1 (skS.0 2 a a_1 a_2) (skS.0 5 (skS.0 2 a a_1 a_2) a_3)) True % 184.04/184.35 Clause #3838 (by superposition #[3837, 452]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 a) True) % 184.04/184.35 (Or (Eq True False) % 184.04/184.35 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) (Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) a_5)) False))) % 184.04/184.35 Clause #3841 (by superposition #[3837, 575]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 a) True) % 184.04/184.35 (Or (Eq True False) % 184.04/184.35 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) % 184.04/184.35 (Eq (r1 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) (skS.0 7 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) a_5)) True))) % 184.04/184.35 Clause #3847 (by clausification #[3838]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 a) True) % 184.04/184.35 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) (Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) a_5)) False)) % 184.04/184.35 Clause #3848 (by superposition #[3847, 49]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 (skS.0 3 a a_1 a_2 a_3)) True) % 184.04/184.35 (Or (Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_4) a_5)) False) (Eq False True)) % 184.04/184.35 Clause #3855 (by clausification #[3848]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 (skS.0 3 a a_1 a_2 a_3)) True) (Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_4) a_5)) False) % 184.04/184.35 Clause #3976 (by clausification #[3841]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 a) True) % 184.04/184.35 (Or (Eq (r1 (skS.0 2 a_1 a_2 a_3) a) False) % 184.04/184.35 (Eq (r1 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) (skS.0 7 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) a_5)) True)) % 184.04/184.35 Clause #3977 (by superposition #[3976, 49]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 (skS.0 3 a a_1 a_2 a_3)) True) % 184.04/184.35 (Or (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_2) a_4) (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_4) a_5)) True) % 184.04/184.35 (Eq False True)) % 184.04/184.35 Clause #3985 (by clausification #[3977]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (p1 (skS.0 3 a a_1 a_2 a_3)) True) % 184.04/184.35 (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_2) a_4) (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_4) a_5)) True) % 184.04/184.35 Clause #3986 (by superposition #[3985, 27]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 184.04/184.35 Or (Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_2) a_3) (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_3) a_4)) True) (Eq True False) % 184.04/184.35 Clause #3989 (by clausification #[3986]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 184.04/184.35 Eq (r1 (skS.0 5 (skS.0 2 a a_1 a_2) a_3) (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_3) a_4)) True % 184.04/184.35 Clause #3990 (by superposition #[3989, 1807]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True) % 184.04/184.35 (Or (Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_3) a_4) a_5)) True) (Eq True False)) % 184.04/184.35 Clause #3992 (by clausification #[3990]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 184.04/184.35 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True) % 184.04/184.35 (Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_3) a_4) a_5)) True) % 184.04/184.35 Clause #4014 (by superposition #[3992, 3855]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 184.04/184.35 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True) % 184.04/184.35 (Or (Eq (p1 (skS.0 3 a a_1 a_3 a_4)) True) (Eq True False)) % 184.04/184.35 Clause #4016 (by clausification #[4014]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 184.04/184.35 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True) (Eq (p1 (skS.0 3 a a_1 a_3 a_4)) True) % 184.04/184.35 Clause #4038 (by superposition #[4016, 27]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True) (Eq True False) % 184.04/184.35 Clause #4039 (by clausification #[4038]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 1 a a_1) (skS.0 6 (skS.0 1 a a_1) a_2)) True % 184.14/184.42 Clause #4040 (by superposition #[4039, 16]): ∀ (a a_1 a_2 : Iota), Or (Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_2)) True) (Eq True False) % 184.14/184.42 Clause #4062 (by clausification #[4040]): ∀ (a a_1 a_2 : Iota), Eq (p1 (skS.0 6 (skS.0 1 a a_1) a_2)) True % 184.14/184.42 Clause #4065 (by superposition #[4062, 528]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 184.14/184.42 Or (Eq True False) (Or (Eq (p1 a) True) (Eq (r1 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) a) False)) % 184.14/184.42 Clause #4086 (by clausification #[4065]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (p1 a) True) (Eq (r1 (skS.0 5 (skS.0 2 a_1 a_2 a_3) a_4) a) False) % 184.14/184.42 Clause #4087 (by superposition #[4086, 3989]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_3) a_4)) True) (Eq False True) % 184.14/184.42 Clause #4098 (by clausification #[4087]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (p1 (skS.0 7 (skS.0 5 (skS.0 2 a a_1 a_2) a_3) a_4)) True % 184.14/184.42 Clause #4099 (by superposition #[4098, 3855]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (p1 (skS.0 3 a a_1 a_2 a_3)) True) (Eq True False) % 184.14/184.42 Clause #4101 (by clausification #[4099]): ∀ (a a_1 a_2 a_3 : Iota), Eq (p1 (skS.0 3 a a_1 a_2 a_3)) True % 184.14/184.42 Clause #4102 (by superposition #[4101, 27]): Eq True False % 184.14/184.42 Clause #4103 (by clausification #[4102]): False % 184.14/184.42 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------