%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL638+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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:11 AM UTC 2026 % Result : Theorem 9.97s 10.26s % Output : Proof 10.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL638+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : duper %s % 0.10/0.36 % Computer : n031.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Fri Sep 4 19:40:54 UTC 2026 % 0.13/0.36 % CPUTime : % 9.97/10.26 SZS status Theorem for theBenchmark.p % 9.97/10.26 SZS output start Proof for theBenchmark.p % 9.97/10.26 Clause #0 (by assumption #[]): Eq % 9.97/10.26 (Not % 9.97/10.26 (Not % 9.97/10.26 (Exists fun X => % 9.97/10.26 Not % 9.97/10.26 (Or % 9.97/10.26 (Or % 9.97/10.26 (Or % 9.97/10.26 (Or % 9.97/10.26 (Or % 9.97/10.26 (Not % 9.97/10.26 (∀ (Y : Iota), % 9.97/10.26 Or (Not (r1 X Y)) % 9.97/10.26 (Not % 9.97/10.26 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 9.97/10.26 (Not (p1 Y)))))) % 9.97/10.26 (Not % 9.97/10.26 (∀ (Y : Iota), % 9.97/10.26 Or (Not (r1 X Y)) % 9.97/10.26 (Not % 9.97/10.26 (And % 9.97/10.26 (Not % 9.97/10.26 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 9.97/10.26 (p1 Y)))))) % 9.97/10.26 (Not % 9.97/10.26 (∀ (Y : Iota), % 9.97/10.26 Or (Not (r1 X Y)) % 9.97/10.27 (Not % 9.97/10.27 (And % 9.97/10.27 (Not % 9.97/10.27 (∀ (X : Iota), % 9.97/10.27 Or (Not (r1 Y X)) % 9.97/10.27 (∀ (Y : Iota), % 9.97/10.27 Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 9.97/10.27 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 9.97/10.27 (Not % 9.97/10.27 (∀ (Y : Iota), % 9.97/10.27 Or (Not (r1 X Y)) % 9.97/10.27 (Not % 9.97/10.27 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 9.97/10.27 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 9.97/10.27 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 9.97/10.27 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p1 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))))) % 9.97/10.27 True % 9.97/10.27 Clause #1 (by clausification #[0]): Eq % 9.97/10.27 (Not % 9.97/10.27 (Exists fun X => % 9.97/10.27 Not % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Not % 9.97/10.27 (∀ (Y : Iota), % 9.97/10.27 Or (Not (r1 X Y)) % 9.97/10.27 (Not % 9.97/10.27 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 9.97/10.27 (Not (p1 Y)))))) % 9.97/10.27 (Not % 9.97/10.27 (∀ (Y : Iota), % 9.97/10.27 Or (Not (r1 X Y)) % 9.97/10.27 (Not % 9.97/10.27 (And % 9.97/10.27 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 9.97/10.27 (p1 Y)))))) % 9.97/10.27 (Not % 9.97/10.27 (∀ (Y : Iota), % 9.97/10.27 Or (Not (r1 X Y)) % 9.97/10.27 (Not % 9.97/10.27 (And % 9.97/10.27 (Not % 9.97/10.27 (∀ (X : Iota), % 9.97/10.27 Or (Not (r1 Y X)) % 9.97/10.27 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 9.97/10.27 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 9.97/10.27 (Not % 9.97/10.27 (∀ (Y : Iota), % 9.97/10.27 Or (Not (r1 X Y)) % 9.97/10.27 (Not % 9.97/10.27 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 9.97/10.27 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 9.97/10.27 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 9.97/10.27 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p1 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 9.97/10.27 False % 9.97/10.27 Clause #2 (by clausification #[1]): Eq % 9.97/10.27 (Exists fun X => % 9.97/10.27 Not % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Or % 9.97/10.27 (Not % 9.97/10.27 (∀ (Y : Iota), % 9.97/10.27 Or (Not (r1 X Y)) % 9.97/10.27 (Not % 10.07/10.31 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 10.07/10.31 (Not (p1 Y)))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 X Y)) % 10.07/10.31 (Not % 10.07/10.31 (And % 10.07/10.31 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 10.07/10.31 (p1 Y)))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 X Y)) % 10.07/10.31 (Not % 10.07/10.31 (And % 10.07/10.31 (Not % 10.07/10.31 (∀ (X : Iota), % 10.07/10.31 Or (Not (r1 Y X)) % 10.07/10.31 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 10.07/10.31 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 X Y)) % 10.07/10.31 (Not % 10.07/10.31 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.07/10.31 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 10.07/10.31 (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 10.07/10.31 (∀ (Y : Iota), Or (Or (Not (r1 X Y)) (p1 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 10.07/10.31 True % 10.07/10.31 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 10.07/10.31 Eq % 10.07/10.31 (Not % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.31 (Not % 10.07/10.31 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 10.07/10.31 (Not (p1 Y)))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.31 (Not % 10.07/10.31 (And % 10.07/10.31 (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 10.07/10.31 (p1 Y)))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.31 (Not % 10.07/10.31 (And % 10.07/10.31 (Not % 10.07/10.31 (∀ (X : Iota), % 10.07/10.31 Or (Not (r1 Y X)) % 10.07/10.31 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 10.07/10.31 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.31 (Not % 10.07/10.31 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.07/10.31 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 10.07/10.31 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 10.07/10.31 (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 10.07/10.31 True % 10.07/10.31 Clause #4 (by clausification #[3]): ∀ (a : Iota), % 10.07/10.31 Eq % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Or % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.31 (Not % 10.07/10.31 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 10.07/10.31 (Not (p1 Y)))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.31 (Not % 10.07/10.31 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 10.07/10.31 (p1 Y)))))) % 10.07/10.31 (Not % 10.07/10.31 (∀ (Y : Iota), % 10.07/10.31 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.31 (Not % 10.07/10.31 (And % 10.07/10.36 (Not % 10.07/10.36 (∀ (X : Iota), % 10.07/10.36 Or (Not (r1 Y X)) % 10.07/10.36 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 10.07/10.36 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 10.07/10.36 (Not % 10.07/10.36 (∀ (Y : Iota), % 10.07/10.36 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.36 (Not % 10.07/10.36 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.07/10.36 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 10.07/10.36 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 10.07/10.36 (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 10.07/10.36 False % 10.07/10.36 Clause #5 (by clausification #[4]): ∀ (a : Iota), % 10.07/10.36 Eq (∀ (Y : Iota), Or (Or (Not (r1 (skS.0 0 a) Y)) (p1 Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))) False % 10.07/10.36 Clause #6 (by clausification #[4]): ∀ (a : Iota), % 10.07/10.36 Eq % 10.07/10.36 (Or % 10.07/10.36 (Or % 10.07/10.36 (Or % 10.07/10.36 (Or % 10.07/10.36 (Not % 10.07/10.36 (∀ (Y : Iota), % 10.07/10.36 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.36 (Not % 10.07/10.36 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 10.07/10.36 (Not (p1 Y)))))) % 10.07/10.36 (Not % 10.07/10.36 (∀ (Y : Iota), % 10.07/10.36 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.36 (Not % 10.07/10.36 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 10.07/10.36 (p1 Y)))))) % 10.07/10.36 (Not % 10.07/10.36 (∀ (Y : Iota), % 10.07/10.36 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.36 (Not % 10.07/10.36 (And % 10.07/10.36 (Not % 10.07/10.36 (∀ (X : Iota), % 10.07/10.36 Or (Not (r1 Y X)) % 10.07/10.36 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 10.07/10.36 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 10.07/10.36 (Not % 10.07/10.36 (∀ (Y : Iota), % 10.07/10.36 Or (Not (r1 (skS.0 0 a) Y)) % 10.07/10.36 (Not % 10.07/10.36 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.07/10.36 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 10.07/10.36 (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))))) % 10.07/10.36 False % 10.07/10.36 Clause #7 (by clausification #[5]): ∀ (a a_1 : Iota), % 10.07/10.36 Eq % 10.07/10.36 (Not % 10.07/10.36 (Or (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) (p1 (skS.0 1 a a_1))) % 10.07/10.36 (Not (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X))))) % 10.07/10.36 True % 10.07/10.36 Clause #8 (by clausification #[7]): ∀ (a a_1 : Iota), % 10.07/10.36 Eq % 10.07/10.36 (Or (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) (p1 (skS.0 1 a a_1))) % 10.07/10.36 (Not (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X)))) % 10.07/10.36 False % 10.07/10.36 Clause #9 (by clausification #[8]): ∀ (a a_1 : Iota), Eq (Not (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X))) False % 10.07/10.36 Clause #10 (by clausification #[8]): ∀ (a a_1 : Iota), Eq (Or (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) (p1 (skS.0 1 a a_1))) False % 10.07/10.36 Clause #11 (by clausification #[9]): ∀ (a a_1 : Iota), Eq (∀ (X : Iota), Or (Not (r1 (skS.0 1 a a_1) X)) (p1 X)) True % 10.07/10.36 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 : Iota), Eq (Or (Not (r1 (skS.0 1 a a_1) a_2)) (p1 a_2)) True % 10.07/10.36 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 : Iota), Or (Eq (Not (r1 (skS.0 1 a a_1) a_2)) True) (Eq (p1 a_2) True) % 10.07/10.36 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 : Iota), Or (Eq (p1 a) True) (Eq (r1 (skS.0 1 a_1 a_2) a) False) % 10.07/10.36 Clause #15 (by clausification #[10]): ∀ (a a_1 : Iota), Eq (p1 (skS.0 1 a a_1)) False % 10.07/10.36 Clause #16 (by clausification #[10]): ∀ (a a_1 : Iota), Eq (Not (r1 (skS.0 0 a) (skS.0 1 a a_1))) False % 10.07/10.36 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 0 a) (skS.0 1 a a_1)) True % 10.07/10.36 Clause #18 (by clausification #[6]): ∀ (a : Iota), Eq (Not (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False)))) False % 10.17/10.42 Clause #19 (by clausification #[6]): ∀ (a : Iota), % 10.17/10.42 Eq % 10.17/10.42 (Or % 10.17/10.42 (Or % 10.17/10.42 (Or % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 10.17/10.42 (Not (p1 Y)))))) % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 10.17/10.42 (p1 Y)))))) % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And % 10.17/10.42 (Not % 10.17/10.42 (∀ (X : Iota), % 10.17/10.42 Or (Not (r1 Y X)) % 10.17/10.42 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 10.17/10.42 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.17/10.42 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))))) % 10.17/10.42 False % 10.17/10.42 Clause #20 (by clausification #[18]): ∀ (a : Iota), Eq (∀ (Y : Iota), Or (Not (r1 (skS.0 0 a) Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) False))) True % 10.17/10.42 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), Eq (Or (Not (r1 (skS.0 0 a) a_1)) (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) False))) True % 10.17/10.42 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) False)) True) % 10.17/10.42 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a X)) False)) True) (Eq (r1 (skS.0 0 a_1) a) False) % 10.17/10.42 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Or (Eq (r1 (skS.0 0 a) a_1) False) (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) False) False) % 10.17/10.42 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 0 a) a_1) False) (Eq (Not (Or (Not (r1 a_1 (skS.0 2 a_1 a_2))) False)) True) % 10.17/10.42 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 0 a) a_1) False) (Eq (Or (Not (r1 a_1 (skS.0 2 a_1 a_2))) False) False) % 10.17/10.42 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 0 a) a_1) False) (Eq (Not (r1 a_1 (skS.0 2 a_1 a_2))) False) % 10.17/10.42 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 0 a) a_1) False) (Eq (r1 a_1 (skS.0 2 a_1 a_2)) True) % 10.17/10.42 Clause #30 (by superposition #[29, 17]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 1 a a_1) (skS.0 2 (skS.0 1 a a_1) a_2)) True) (Eq False True) % 10.17/10.42 Clause #31 (by clausification #[19]): ∀ (a : Iota), % 10.17/10.42 Eq % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.17/10.42 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X)))))) % 10.17/10.42 False % 10.17/10.42 Clause #32 (by clausification #[19]): ∀ (a : Iota), % 10.17/10.42 Eq % 10.17/10.42 (Or % 10.17/10.42 (Or % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 10.17/10.42 (Not (p1 Y)))))) % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 10.17/10.42 (p1 Y)))))) % 10.17/10.42 (Not % 10.17/10.42 (∀ (Y : Iota), % 10.17/10.42 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.42 (Not % 10.17/10.42 (And % 10.17/10.42 (Not % 10.17/10.42 (∀ (X : Iota), % 10.17/10.42 Or (Not (r1 Y X)) % 10.17/10.42 (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (p1 X))))))) % 10.17/10.49 (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))))))) % 10.17/10.49 False % 10.17/10.49 Clause #33 (by clausification #[31]): ∀ (a : Iota), % 10.17/10.49 Eq % 10.17/10.49 (∀ (Y : Iota), % 10.17/10.49 Or (Not (r1 (skS.0 0 a) Y)) % 10.17/10.49 (Not % 10.17/10.49 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.17/10.49 (∀ (X : Iota), Or (Not (r1 Y X)) (p1 X))))) % 10.17/10.49 True % 10.17/10.49 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), % 10.17/10.49 Eq % 10.17/10.49 (Or (Not (r1 (skS.0 0 a) a_1)) % 10.17/10.49 (Not % 10.17/10.49 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.17/10.49 (∀ (X : Iota), Or (Not (r1 a_1 X)) (p1 X))))) % 10.17/10.49 True % 10.17/10.49 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), % 10.17/10.49 Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) % 10.17/10.49 (Eq % 10.17/10.49 (Not % 10.17/10.49 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.17/10.49 (∀ (X : Iota), Or (Not (r1 a_1 X)) (p1 X)))) % 10.17/10.49 True) % 10.17/10.49 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 10.17/10.49 Or % 10.17/10.49 (Eq % 10.17/10.49 (Not % 10.17/10.49 (And (Not (∀ (X : Iota), Or (Not (r1 a X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.17/10.49 (∀ (X : Iota), Or (Not (r1 a X)) (p1 X)))) % 10.17/10.49 True) % 10.17/10.49 (Eq (r1 (skS.0 0 a_1) a) False) % 10.17/10.49 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Eq % 10.17/10.49 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) % 10.17/10.49 (∀ (X : Iota), Or (Not (r1 a_1 X)) (p1 X))) % 10.17/10.49 False) % 10.17/10.49 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) False) % 10.17/10.49 (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (p1 X)) False)) % 10.17/10.49 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (p1 X)) False) % 10.17/10.49 (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) True)) % 10.17/10.49 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))) True) % 10.17/10.49 (Eq (Not (Or (Not (r1 a_1 (skS.0 3 a_1 a_2))) (p1 (skS.0 3 a_1 a_2)))) True)) % 10.17/10.49 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 a_3 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (Not (Or (Not (r1 a_1 (skS.0 3 a_1 a_2))) (p1 (skS.0 3 a_1 a_2)))) True) % 10.17/10.49 (Eq (Or (Not (r1 a_1 a_3)) (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (p1 Y))) True)) % 10.17/10.49 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (Or (Not (r1 a_1 a_2)) (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))) True) % 10.17/10.49 (Eq (Or (Not (r1 a_1 (skS.0 3 a_1 a_3))) (p1 (skS.0 3 a_1 a_3))) False)) % 10.17/10.49 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (Or (Not (r1 a_1 (skS.0 3 a_1 a_2))) (p1 (skS.0 3 a_1 a_2))) False) % 10.17/10.49 (Or (Eq (Not (r1 a_1 a_3)) True) (Eq (∀ (Y : Iota), Or (Not (r1 a_3 Y)) (p1 Y)) True))) % 10.17/10.49 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (Not (r1 a_1 a_2)) True) % 10.17/10.49 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)) True) (Eq (p1 (skS.0 3 a_1 a_3)) False))) % 10.17/10.49 Clause #45 (by clausification #[43]): ∀ (a a_1 a_2 a_3 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (Not (r1 a_1 a_2)) True) % 10.17/10.49 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)) True) (Eq (Not (r1 a_1 (skS.0 3 a_1 a_3))) False))) % 10.17/10.49 Clause #46 (by clausification #[44]): ∀ (a a_1 a_2 a_3 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)) True) % 10.17/10.49 (Or (Eq (p1 (skS.0 3 a_1 a_3)) False) (Eq (r1 a_1 a_2) False))) % 10.17/10.49 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.17/10.49 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.17/10.49 (Or (Eq (p1 (skS.0 3 a_1 a_2)) False) (Or (Eq (r1 a_1 a_3) False) (Eq (Or (Not (r1 a_3 a_4)) (p1 a_4)) True))) % 10.27/10.56 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.27/10.56 (Or (Eq (p1 (skS.0 3 a_1 a_2)) False) % 10.27/10.56 (Or (Eq (r1 a_1 a_3) False) (Or (Eq (Not (r1 a_3 a_4)) True) (Eq (p1 a_4) True)))) % 10.27/10.56 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.27/10.56 (Or (Eq (p1 (skS.0 3 a_1 a_2)) False) (Or (Eq (r1 a_1 a_3) False) (Or (Eq (p1 a_4) True) (Eq (r1 a_3 a_4) False)))) % 10.27/10.56 Clause #50 (by superposition #[49, 17]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (p1 (skS.0 3 (skS.0 1 a a_1) a_2)) False) % 10.27/10.56 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) (Or (Eq (p1 a_4) True) (Or (Eq (r1 a_3 a_4) False) (Eq False True)))) % 10.27/10.56 Clause #51 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 1 a a_1) (skS.0 2 (skS.0 1 a a_1) a_2)) True % 10.27/10.56 Clause #54 (by clausification #[45]): ∀ (a a_1 a_2 a_3 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.27/10.56 (Or (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)) True) % 10.27/10.56 (Or (Eq (Not (r1 a_1 (skS.0 3 a_1 a_3))) False) (Eq (r1 a_1 a_2) False))) % 10.27/10.56 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.27/10.56 (Or (Eq (Not (r1 a_1 (skS.0 3 a_1 a_2))) False) % 10.27/10.56 (Or (Eq (r1 a_1 a_3) False) (Eq (Or (Not (r1 a_3 a_4)) (p1 a_4)) True))) % 10.27/10.56 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.27/10.56 (Or (Eq (r1 a_1 a_2) False) (Or (Eq (Or (Not (r1 a_2 a_3)) (p1 a_3)) True) (Eq (r1 a_1 (skS.0 3 a_1 a_4)) True))) % 10.27/10.56 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.27/10.56 (Or (Eq (r1 a_1 a_2) False) % 10.27/10.56 (Or (Eq (r1 a_1 (skS.0 3 a_1 a_3)) True) (Or (Eq (Not (r1 a_2 a_4)) True) (Eq (p1 a_4) True)))) % 10.27/10.56 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.27/10.56 (Or (Eq (r1 a_1 a_2) False) % 10.27/10.56 (Or (Eq (r1 a_1 (skS.0 3 a_1 a_3)) True) (Or (Eq (p1 a_4) True) (Eq (r1 a_2 a_4) False)))) % 10.27/10.56 Clause #59 (by superposition #[58, 17]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 10.27/10.56 (Or (Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_3)) True) % 10.27/10.56 (Or (Eq (p1 a_4) True) (Or (Eq (r1 a_2 a_4) False) (Eq False True)))) % 10.27/10.56 Clause #60 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (p1 (skS.0 3 (skS.0 1 a a_1) a_2)) False) % 10.27/10.56 (Or (Eq (r1 (skS.0 1 a a_1) a_3) False) (Or (Eq (p1 a_4) True) (Eq (r1 a_3 a_4) False))) % 10.27/10.56 Clause #61 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 1 a a_1) a_2) False) % 10.27/10.56 (Or (Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_3)) True) (Or (Eq (p1 a_4) True) (Eq (r1 a_2 a_4) False))) % 10.27/10.56 Clause #62 (by superposition #[61, 51]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_2)) True) % 10.27/10.56 (Or (Eq (p1 a_3) True) (Or (Eq (r1 (skS.0 2 (skS.0 1 a a_1) a_4) a_3) False) (Eq False True))) % 10.27/10.56 Clause #64 (by clausification #[32]): ∀ (a : Iota), % 10.27/10.56 Eq % 10.27/10.56 (Or % 10.27/10.56 (Not % 10.27/10.56 (∀ (Y : Iota), % 10.27/10.56 Or (Not (r1 (skS.0 0 a) Y)) % 10.27/10.56 (Not % 10.27/10.56 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) % 10.27/10.56 (Not (p1 Y)))))) % 10.27/10.56 (Not % 10.27/10.56 (∀ (Y : Iota), % 10.27/10.56 Or (Not (r1 (skS.0 0 a) Y)) % 10.27/10.56 (Not % 10.27/10.56 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (Not (p1 Y)))))) % 10.27/10.56 (p1 Y)))))) % 10.27/10.56 False % 10.27/10.56 Clause #110 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.27/10.56 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_2)) True) % 10.27/10.56 (Or (Eq (p1 a_3) True) (Eq (r1 (skS.0 2 (skS.0 1 a a_1) a_4) a_3) False)) % 10.27/10.56 Clause #114 (by clausification #[64]): ∀ (a : Iota), % 10.27/10.56 Eq % 10.27/10.56 (Not % 10.27/10.56 (∀ (Y : Iota), % 10.27/10.56 Or (Not (r1 (skS.0 0 a) Y)) % 10.27/10.56 (Not % 10.27/10.56 (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) (Not (p1 Y)))))) % 10.27/10.56 False % 10.27/10.56 Clause #138 (by clausification #[114]): ∀ (a : Iota), % 10.27/10.56 Eq % 10.27/10.56 (∀ (Y : Iota), % 10.37/10.63 Or (Not (r1 (skS.0 0 a) Y)) % 10.37/10.63 (Not (And (Not (∀ (X : Iota), Or (Not (r1 Y X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) (Not (p1 Y))))) % 10.37/10.63 True % 10.37/10.63 Clause #139 (by clausification #[138]): ∀ (a a_1 : Iota), % 10.37/10.63 Eq % 10.37/10.63 (Or (Not (r1 (skS.0 0 a) a_1)) % 10.37/10.63 (Not % 10.37/10.63 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) (Not (p1 a_1))))) % 10.37/10.63 True % 10.37/10.63 Clause #140 (by clausification #[139]): ∀ (a a_1 : Iota), % 10.37/10.63 Or (Eq (Not (r1 (skS.0 0 a) a_1)) True) % 10.37/10.63 (Eq % 10.37/10.63 (Not % 10.37/10.63 (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) (Not (p1 a_1)))) % 10.37/10.63 True) % 10.37/10.63 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), % 10.37/10.63 Or % 10.37/10.63 (Eq (Not (And (Not (∀ (X : Iota), Or (Not (r1 a X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) (Not (p1 a)))) % 10.37/10.63 True) % 10.37/10.63 (Eq (r1 (skS.0 0 a_1) a) False) % 10.37/10.63 Clause #142 (by clausification #[141]): ∀ (a a_1 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Eq (And (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) (Not (p1 a_1))) % 10.37/10.63 False) % 10.37/10.63 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (Not (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y))))) False) % 10.37/10.63 (Eq (Not (p1 a_1)) False)) % 10.37/10.63 Clause #144 (by clausification #[143]): ∀ (a a_1 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (Not (p1 a_1)) False) % 10.37/10.63 (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) True)) % 10.37/10.63 Clause #145 (by clausification #[144]): ∀ (a a_1 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (∀ (X : Iota), Or (Not (r1 a_1 X)) (Not (∀ (Y : Iota), Or (Not (r1 X Y)) (p1 Y)))) True) (Eq (p1 a_1) True)) % 10.37/10.63 Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) (Eq (Or (Not (r1 a_1 a_2)) (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)))) True)) % 10.37/10.63 Clause #147 (by clausification #[146]): ∀ (a a_1 a_2 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) (Or (Eq (Not (r1 a_1 a_2)) True) (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))) True))) % 10.37/10.63 Clause #148 (by clausification #[147]): ∀ (a a_1 a_2 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) (Or (Eq (Not (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y))) True) (Eq (r1 a_1 a_2) False))) % 10.37/10.63 Clause #149 (by clausification #[148]): ∀ (a a_1 a_2 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) (Or (Eq (r1 a_1 a_2) False) (Eq (∀ (Y : Iota), Or (Not (r1 a_2 Y)) (p1 Y)) False))) % 10.37/10.63 Clause #150 (by clausification #[149]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) % 10.37/10.63 (Or (Eq (r1 a_1 a_2) False) (Eq (Not (Or (Not (r1 a_2 (skS.0 8 a_2 a_3))) (p1 (skS.0 8 a_2 a_3)))) True))) % 10.37/10.63 Clause #151 (by clausification #[150]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) % 10.37/10.63 (Or (Eq (r1 a_1 a_2) False) (Eq (Or (Not (r1 a_2 (skS.0 8 a_2 a_3))) (p1 (skS.0 8 a_2 a_3))) False))) % 10.37/10.63 Clause #152 (by clausification #[151]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) (Or (Eq (r1 a_1 a_2) False) (Eq (p1 (skS.0 8 a_2 a_3)) False))) % 10.37/10.63 Clause #153 (by clausification #[151]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) (Or (Eq (r1 a_1 a_2) False) (Eq (Not (r1 a_2 (skS.0 8 a_2 a_3))) False))) % 10.37/10.63 Clause #154 (by superposition #[152, 17]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.63 Or (Eq (p1 (skS.0 1 a a_1)) True) % 10.37/10.63 (Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p1 (skS.0 8 a_2 a_3)) False) (Eq False True))) % 10.37/10.63 Clause #155 (by clausification #[153]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.63 Or (Eq (r1 (skS.0 0 a) a_1) False) % 10.37/10.63 (Or (Eq (p1 a_1) True) (Or (Eq (r1 a_1 a_2) False) (Eq (r1 a_2 (skS.0 8 a_2 a_3)) True))) % 10.37/10.63 Clause #156 (by superposition #[155, 17]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.63 Or (Eq (p1 (skS.0 1 a a_1)) True) % 10.37/10.68 (Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (r1 a_2 (skS.0 8 a_2 a_3)) True) (Eq False True))) % 10.37/10.68 Clause #159 (by clausification #[154]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.68 Or (Eq (p1 (skS.0 1 a a_1)) True) (Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (p1 (skS.0 8 a_2 a_3)) False)) % 10.37/10.68 Clause #160 (by forward demodulation #[159, 15]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq False True) (Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (p1 (skS.0 8 a_2 a_3)) False)) % 10.37/10.68 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (p1 (skS.0 8 a_2 a_3)) False) % 10.37/10.68 Clause #162 (by superposition #[161, 51]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (p1 (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_2) a_3)) False) (Eq False True) % 10.37/10.68 Clause #163 (by clausification #[162]): ∀ (a a_1 a_2 a_3 : Iota), Eq (p1 (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_2) a_3)) False % 10.37/10.68 Clause #164 (by clausification #[156]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.68 Or (Eq (p1 (skS.0 1 a a_1)) True) (Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (r1 a_2 (skS.0 8 a_2 a_3)) True)) % 10.37/10.68 Clause #165 (by forward demodulation #[164, 15]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.68 Or (Eq False True) (Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (r1 a_2 (skS.0 8 a_2 a_3)) True)) % 10.37/10.68 Clause #166 (by clausification #[165]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Eq (r1 a_2 (skS.0 8 a_2 a_3)) True) % 10.37/10.68 Clause #167 (by superposition #[166, 51]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.68 Or (Eq (r1 (skS.0 2 (skS.0 1 a a_1) a_2) (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_2) a_3)) True) (Eq False True) % 10.37/10.68 Clause #168 (by clausification #[167]): ∀ (a a_1 a_2 a_3 : Iota), Eq (r1 (skS.0 2 (skS.0 1 a a_1) a_2) (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_2) a_3)) True % 10.37/10.68 Clause #169 (by superposition #[168, 110]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.37/10.68 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_2)) True) % 10.37/10.68 (Or (Eq (p1 (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_3) a_4)) True) (Eq True False)) % 10.37/10.68 Clause #174 (by clausification #[169]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.37/10.68 Or (Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_2)) True) % 10.37/10.68 (Eq (p1 (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_3) a_4)) True) % 10.37/10.68 Clause #182 (by superposition #[174, 163]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_2)) True) (Eq True False) % 10.37/10.68 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 1 a a_1) (skS.0 3 (skS.0 1 a a_1) a_2)) True % 10.37/10.68 Clause #184 (by superposition #[183, 14]): ∀ (a a_1 a_2 : Iota), Or (Eq (p1 (skS.0 3 (skS.0 1 a a_1) a_2)) True) (Eq True False) % 10.37/10.68 Clause #190 (by clausification #[184]): ∀ (a a_1 a_2 : Iota), Eq (p1 (skS.0 3 (skS.0 1 a a_1) a_2)) True % 10.37/10.68 Clause #191 (by superposition #[190, 60]): ∀ (a a_1 a_2 a_3 : Iota), % 10.37/10.68 Or (Eq True False) (Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p1 a_3) True) (Eq (r1 a_2 a_3) False))) % 10.37/10.68 Clause #192 (by clausification #[191]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r1 (skS.0 1 a a_1) a_2) False) (Or (Eq (p1 a_3) True) (Eq (r1 a_2 a_3) False)) % 10.37/10.68 Clause #193 (by superposition #[192, 51]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (p1 a) True) (Or (Eq (r1 (skS.0 2 (skS.0 1 a_1 a_2) a_3) a) False) (Eq False True)) % 10.37/10.68 Clause #199 (by clausification #[193]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (p1 a) True) (Eq (r1 (skS.0 2 (skS.0 1 a_1 a_2) a_3) a) False) % 10.37/10.68 Clause #200 (by superposition #[199, 168]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (p1 (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_2) a_3)) True) (Eq False True) % 10.37/10.68 Clause #202 (by clausification #[200]): ∀ (a a_1 a_2 a_3 : Iota), Eq (p1 (skS.0 8 (skS.0 2 (skS.0 1 a a_1) a_2) a_3)) True % 10.37/10.68 Clause #203 (by superposition #[202, 163]): Eq True False % 10.37/10.68 Clause #204 (by clausification #[203]): False % 10.37/10.68 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------