%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO105^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:08:36 PM UTC 2025 % Result : Theorem 7.83s 8.08s % Output : Proof 8.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SYO105^5 : TPTP v9.2.0. Released v4.0.0. % 0.12/0.14 % Command : duper %s % 0.14/0.35 % Computer : n017.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 12:51:53 EDT 2025 % 0.14/0.35 % CPUTime : % 7.83/8.08 SZS status Theorem for theBenchmark.p % 7.83/8.08 SZS output start Proof for theBenchmark.p % 7.83/8.08 Clause #0 (by assumption #[]): Eq % 7.83/8.08 (Not % 7.83/8.08 (Iff % 7.83/8.08 (Not % 7.83/8.08 ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists fun Xv => cR Xv)))) % 7.83/8.08 (Exists fun Xx => ∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ Xx y → Not (cP Xu y Xz → Not (cR Xv)))))) % 7.83/8.08 True % 7.83/8.08 Clause #1 (by betaEtaReduce #[0]): Eq % 7.83/8.08 (Not % 7.83/8.08 (Iff (Not ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)))) % 7.83/8.08 (Exists fun Xx => ∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ Xx y → Not (cP Xu y Xz → Not (cR Xv)))))) % 7.83/8.08 True % 7.83/8.08 Clause #2 (by clausification #[1]): Eq % 7.83/8.08 (Iff (Not ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)))) % 7.83/8.08 (Exists fun Xx => ∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ Xx y → Not (cP Xu y Xz → Not (cR Xv))))) % 7.83/8.08 False % 7.83/8.08 Clause #3 (by clausification #[2]): Or (Eq (Not ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)))) False) % 7.83/8.08 (Eq (Exists fun Xx => ∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ Xx y → Not (cP Xu y Xz → Not (cR Xv)))) % 7.83/8.08 False) % 7.83/8.08 Clause #4 (by clausification #[2]): Or (Eq (Not ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)))) True) % 7.83/8.08 (Eq (Exists fun Xx => ∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ Xx y → Not (cP Xu y Xz → Not (cR Xv)))) % 7.83/8.08 True) % 7.83/8.08 Clause #5 (by clausification #[3]): Or % 7.83/8.08 (Eq (Exists fun Xx => ∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ Xx y → Not (cP Xu y Xz → Not (cR Xv)))) % 7.83/8.08 False) % 7.83/8.08 (Eq ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) True) % 7.83/8.08 Clause #6 (by clausification #[5]): ∀ (a : Iota), % 7.83/8.08 Or (Eq ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) True) % 7.83/8.08 (Eq (∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ a y → Not (cP Xu y Xz → Not (cR Xv)))) False) % 7.83/8.08 Clause #7 (by clausification #[6]): ∀ (a : Iota), % 7.83/8.08 Or (Eq (∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ a y → Not (cP Xu y Xz → Not (cR Xv)))) False) % 7.83/8.08 (Or (Eq (Exists fun Xx => cQ Xx y) False) % 7.83/8.08 (Eq (Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) True)) % 7.83/8.08 Clause #8 (by clausification #[7]): ∀ (a a_1 : Iota), % 7.83/8.08 Or (Eq (Exists fun Xx => cQ Xx y) False) % 7.83/8.08 (Or (Eq (Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) True) % 7.83/8.08 (Eq (Not (Exists fun Xu => ∀ (Xv : Iota), Not (cQ a y → Not (cP Xu y (skS.0 0 a a_1) → Not (cR Xv))))) True)) % 7.83/8.08 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 : Iota), % 7.83/8.08 Or (Eq (Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) True) % 7.83/8.08 (Or (Eq (Not (Exists fun Xu => ∀ (Xv : Iota), Not (cQ a y → Not (cP Xu y (skS.0 0 a a_1) → Not (cR Xv))))) True) % 7.83/8.08 (Eq (cQ a_2 y) False)) % 7.83/8.08 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 : Iota), % 7.83/8.08 Or (Eq (Not (Exists fun Xu => ∀ (Xv : Iota), Not (cQ a y → Not (cP Xu y (skS.0 0 a a_1) → Not (cR Xv))))) True) % 7.83/8.08 (Or (Eq (cQ a_2 y) False) (Eq (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)) False)) % 7.83/8.08 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 : Iota), % 7.83/8.08 Or (Eq (cQ a y) False) % 7.83/8.08 (Or (Eq (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)) False) % 7.83/8.08 (Eq (Exists fun Xu => ∀ (Xv : Iota), Not (cQ a_1 y → Not (cP Xu y (skS.0 0 a_1 a_2) → Not (cR Xv)))) False)) % 7.83/8.08 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 a_3 : Iota), % 7.83/8.08 Or (Eq (cQ a y) False) % 7.83/8.08 (Or (Eq (Exists fun Xu => ∀ (Xv : Iota), Not (cQ a_1 y → Not (cP Xu y (skS.0 0 a_1 a_2) → Not (cR Xv)))) False) % 7.83/8.08 (Eq (Not ((∀ (Xu : Iota), cP Xu y (skS.0 1 a_3)) → Not (Exists cR))) True)) % 7.83/8.08 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.83/8.08 Or (Eq (cQ a y) False) % 7.83/8.08 (Or (Eq (Not ((∀ (Xu : Iota), cP Xu y (skS.0 1 a_1)) → Not (Exists cR))) True) % 7.95/8.11 (Eq (∀ (Xv : Iota), Not (cQ a_2 y → Not (cP a_3 y (skS.0 0 a_2 a_4) → Not (cR Xv)))) False)) % 7.95/8.11 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (∀ (Xv : Iota), Not (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR Xv)))) False) % 7.95/8.11 (Eq ((∀ (Xu : Iota), cP Xu y (skS.0 1 a_4)) → Not (Exists cR)) False)) % 7.95/8.11 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq ((∀ (Xu : Iota), cP Xu y (skS.0 1 a_1)) → Not (Exists cR)) False) % 7.95/8.11 (Eq (Not (Not (cQ a_2 y → Not (cP a_3 y (skS.0 0 a_2 a_4) → Not (cR (skS.0 2 a_2 a_3 a_4 a_5)))))) True)) % 7.95/8.11 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (Not (Not (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR (skS.0 2 a_1 a_2 a_3 a_4)))))) True) % 7.95/8.11 (Eq (∀ (Xu : Iota), cP Xu y (skS.0 1 a_5)) True)) % 7.95/8.11 Clause #17 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (Not (Not (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR (skS.0 2 a_1 a_2 a_3 a_4)))))) True) % 7.95/8.11 (Eq (Not (Exists cR)) False)) % 7.95/8.11 Clause #18 (by clausification #[16]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (∀ (Xu : Iota), cP Xu y (skS.0 1 a_1)) True) % 7.95/8.11 (Eq (Not (cQ a_2 y → Not (cP a_3 y (skS.0 0 a_2 a_4) → Not (cR (skS.0 2 a_2 a_3 a_4 a_5))))) False)) % 7.95/8.11 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (Not (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR (skS.0 2 a_1 a_2 a_3 a_4))))) False) % 7.95/8.11 (Eq (cP a_5 y (skS.0 1 a_6)) True)) % 7.95/8.11 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) % 7.95/8.11 (Eq (cQ a_3 y → Not (cP a_4 y (skS.0 0 a_3 a_5) → Not (cR (skS.0 2 a_3 a_4 a_5 a_6)))) True)) % 7.95/8.11 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) % 7.95/8.11 (Or (Eq (cQ a_3 y) False) (Eq (Not (cP a_4 y (skS.0 0 a_3 a_5) → Not (cR (skS.0 2 a_3 a_4 a_5 a_6)))) True))) % 7.95/8.11 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) % 7.95/8.11 (Or (Eq (cQ a_3 y) False) (Eq (cP a_4 y (skS.0 0 a_3 a_5) → Not (cR (skS.0 2 a_3 a_4 a_5 a_6))) False))) % 7.95/8.11 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.95/8.11 Or (Eq (cQ a y) False) % 7.95/8.11 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) (Or (Eq (cQ a_3 y) False) (Eq (cP a_4 y (skS.0 0 a_3 a_5)) True))) % 7.95/8.11 Clause #25 (by clausification #[4]): Or % 7.95/8.11 (Eq (Exists fun Xx => ∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ Xx y → Not (cP Xu y Xz → Not (cR Xv)))) % 7.95/8.11 True) % 7.95/8.11 (Eq ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) False) % 7.95/8.11 Clause #26 (by clausification #[25]): ∀ (a : Iota), % 7.95/8.11 Or (Eq ((Exists fun Xx => cQ Xx y) → Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) False) % 7.95/8.11 (Eq (∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP Xu y Xz → Not (cR Xv)))) True) % 7.95/8.11 Clause #27 (by clausification #[26]): ∀ (a : Iota), % 7.95/8.11 Or (Eq (∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP Xu y Xz → Not (cR Xv)))) True) % 7.95/8.11 (Eq (Exists fun Xx => cQ Xx y) True) % 7.95/8.11 Clause #28 (by clausification #[26]): ∀ (a : Iota), % 7.95/8.11 Or (Eq (∀ (Xz : Iota), Exists fun Xu => ∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP Xu y Xz → Not (cR Xv)))) True) % 7.95/8.11 (Eq (Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) False) % 7.95/8.11 Clause #29 (by clausification #[27]): ∀ (a a_1 : Iota), % 7.95/8.11 Or (Eq (Exists fun Xx => cQ Xx y) True) % 7.95/8.11 (Eq (Exists fun Xu => ∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP Xu y a_1 → Not (cR Xv)))) True) % 7.96/8.14 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 : Iota), % 7.96/8.14 Or (Eq (Exists fun Xu => ∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP Xu y a_1 → Not (cR Xv)))) True) % 7.96/8.14 (Eq (cQ (skS.0 4 a_2) y) True) % 7.96/8.14 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 a_3 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 4 a) y) True) % 7.96/8.14 (Eq (∀ (Xv : Iota), Not (cQ (skS.0 3 a_1) y → Not (cP (skS.0 5 a_1 a_2 a_3) y a_2 → Not (cR Xv)))) True) % 7.96/8.14 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 4 a) y) True) % 7.96/8.14 (Eq (Not (cQ (skS.0 3 a_1) y → Not (cP (skS.0 5 a_1 a_2 a_3) y a_2 → Not (cR a_4)))) True) % 7.96/8.14 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 4 a) y) True) (Eq (cQ (skS.0 3 a_1) y → Not (cP (skS.0 5 a_1 a_2 a_3) y a_2 → Not (cR a_4))) False) % 7.96/8.14 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Eq (cQ (skS.0 3 a_1) y) True) % 7.96/8.14 Clause #35 (by clausification #[33]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 4 a) y) True) (Eq (Not (cP (skS.0 5 a_1 a_2 a_3) y a_2 → Not (cR a_4))) False) % 7.96/8.14 Clause #37 (by superposition #[34, 23]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 4 a) y) True) % 7.96/8.14 (Or (Eq True False) % 7.96/8.14 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) (Or (Eq (cQ a_3 y) False) (Eq (cP a_4 y (skS.0 0 a_3 a_5)) True)))) % 7.96/8.14 Clause #38 (by clausification #[35]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Eq (cP (skS.0 5 a_1 a_2 a_3) y a_2 → Not (cR a_4)) True) % 7.96/8.14 Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cP (skS.0 5 a_1 a_2 a_3) y a_2) False) (Eq (Not (cR a_4)) True)) % 7.96/8.14 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cP (skS.0 5 a_1 a_2 a_3) y a_2) False) (Eq (cR a_4) False)) % 7.96/8.14 Clause #41 (by clausification #[28]): ∀ (a a_1 : Iota), % 7.96/8.14 Or (Eq (Not (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR))) False) % 7.96/8.14 (Eq (Exists fun Xu => ∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP Xu y a_1 → Not (cR Xv)))) True) % 7.96/8.14 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 7.96/8.14 Or (Eq (Exists fun Xu => ∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP Xu y a_1 → Not (cR Xv)))) True) % 7.96/8.14 (Eq (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)) True) % 7.96/8.14 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), % 7.96/8.14 Or (Eq (∀ (Xz : Iota), (∀ (Xu : Iota), cP Xu y Xz) → Not (Exists cR)) True) % 7.96/8.14 (Eq (∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP (skS.0 6 a a_1 a_2) y a_1 → Not (cR Xv)))) True) % 7.96/8.14 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 : Iota), % 7.96/8.14 Or (Eq (∀ (Xv : Iota), Not (cQ (skS.0 3 a) y → Not (cP (skS.0 6 a a_1 a_2) y a_1 → Not (cR Xv)))) True) % 7.96/8.14 (Eq ((∀ (Xu : Iota), cP Xu y a_3) → Not (Exists cR)) True) % 7.96/8.14 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq ((∀ (Xu : Iota), cP Xu y a) → Not (Exists cR)) True) % 7.96/8.14 (Eq (Not (cQ (skS.0 3 a_1) y → Not (cP (skS.0 6 a_1 a_2 a_3) y a_2 → Not (cR a_4)))) True) % 7.96/8.14 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq (Not (cQ (skS.0 3 a) y → Not (cP (skS.0 6 a a_1 a_2) y a_1 → Not (cR a_3)))) True) % 7.96/8.14 (Or (Eq (∀ (Xu : Iota), cP Xu y a_4) False) (Eq (Not (Exists cR)) True)) % 7.96/8.14 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.14 Or (Eq (∀ (Xu : Iota), cP Xu y a) False) % 7.96/8.14 (Or (Eq (Not (Exists cR)) True) % 7.96/8.14 (Eq (cQ (skS.0 3 a_1) y → Not (cP (skS.0 6 a_1 a_2 a_3) y a_2 → Not (cR a_4))) False)) % 7.96/8.14 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.14 Or (Eq (Not (Exists cR)) True) % 7.96/8.14 (Or (Eq (cQ (skS.0 3 a) y → Not (cP (skS.0 6 a a_1 a_2) y a_1 → Not (cR a_3))) False) % 7.96/8.14 (Eq (Not (cP (skS.0 7 a_4 a_5) y a_4)) True)) % 7.96/8.14 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.14 Or (Eq (cQ (skS.0 3 a) y → Not (cP (skS.0 6 a a_1 a_2) y a_1 → Not (cR a_3))) False) % 7.96/8.14 (Or (Eq (Not (cP (skS.0 7 a_4 a_5) y a_4)) True) (Eq (Exists cR) False)) % 7.96/8.17 Clause #51 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (Not (cP (skS.0 7 a a_1) y a)) True) % 7.96/8.17 (Or (Eq (Exists cR) False) (Eq (Not (cP (skS.0 6 a_2 a_3 a_4) y a_3 → Not (cR a_5))) False)) % 7.96/8.17 Clause #54 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (Exists cR) False) % 7.96/8.17 (Or (Eq (Not (cP (skS.0 6 a a_1 a_2) y a_1 → Not (cR a_3))) False) (Eq (cP (skS.0 7 a_4 a_5) y a_4) False)) % 7.96/8.17 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.96/8.17 Or (Eq (Not (cP (skS.0 6 a a_1 a_2) y a_1 → Not (cR a_3))) False) % 7.96/8.17 (Or (Eq (cP (skS.0 7 a_4 a_5) y a_4) False) (Eq (cR a_6) False)) % 7.96/8.17 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.96/8.17 Or (Eq (cP (skS.0 7 a a_1) y a) False) % 7.96/8.17 (Or (Eq (cR a_2) False) (Eq (cP (skS.0 6 a_3 a_4 a_5) y a_4 → Not (cR a_6)) True)) % 7.96/8.17 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.96/8.17 Or (Eq (cP (skS.0 7 a a_1) y a) False) % 7.96/8.17 (Or (Eq (cR a_2) False) (Or (Eq (cP (skS.0 6 a_3 a_4 a_5) y a_4) False) (Eq (Not (cR a_6)) True))) % 7.96/8.17 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.96/8.17 Or (Eq (cP (skS.0 7 a a_1) y a) False) % 7.96/8.17 (Or (Eq (cR a_2) False) (Or (Eq (cP (skS.0 6 a_3 a_4 a_5) y a_4) False) (Eq (cR a_6) False))) % 7.96/8.17 Clause #59 (by clausification #[17]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (Not (Exists cR)) False) % 7.96/8.17 (Eq (Not (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR (skS.0 2 a_1 a_2 a_3 a_4))))) False)) % 7.96/8.17 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (Not (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR (skS.0 2 a_1 a_2 a_3 a_4))))) False) % 7.96/8.17 (Eq (Exists cR) True)) % 7.96/8.17 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (Exists cR) True) % 7.96/8.17 (Eq (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR (skS.0 2 a_1 a_2 a_3 a_4)))) True)) % 7.96/8.17 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (cQ a_1 y → Not (cP a_2 y (skS.0 0 a_1 a_3) → Not (cR (skS.0 2 a_1 a_2 a_3 a_4)))) True) % 7.96/8.17 (Eq (cR (skS.0 8 a_5)) True)) % 7.96/8.17 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (cR (skS.0 8 a_1)) True) % 7.96/8.17 (Or (Eq (cQ a_2 y) False) (Eq (Not (cP a_3 y (skS.0 0 a_2 a_4) → Not (cR (skS.0 2 a_2 a_3 a_4 a_5)))) True))) % 7.96/8.17 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (cR (skS.0 8 a_1)) True) % 7.96/8.17 (Or (Eq (cQ a_2 y) False) (Eq (cP a_3 y (skS.0 0 a_2 a_4) → Not (cR (skS.0 2 a_2 a_3 a_4 a_5))) False))) % 7.96/8.17 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cQ a_2 y) False) (Eq (cP a_3 y (skS.0 0 a_2 a_4)) True))) % 7.96/8.17 Clause #66 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cQ a_2 y) False) (Eq (Not (cR (skS.0 2 a_2 a_3 a_4 a_5))) False))) % 7.96/8.17 Clause #68 (by superposition #[65, 34]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.17 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.17 (Or (Eq (cQ a_1 y) False) % 7.96/8.17 (Or (Eq (cP a_2 y (skS.0 0 a_1 a_3)) True) (Or (Eq (cQ (skS.0 4 a_4) y) True) (Eq False True)))) % 7.96/8.17 Clause #69 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (cQ a y) False) % 7.96/8.17 (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cQ a_2 y) False) (Eq (cR (skS.0 2 a_2 a_3 a_4 a_5)) True))) % 7.96/8.17 Clause #71 (by superposition #[69, 34]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.17 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.17 (Or (Eq (cQ a_1 y) False) % 7.96/8.17 (Or (Eq (cR (skS.0 2 a_1 a_2 a_3 a_4)) True) (Or (Eq (cQ (skS.0 4 a_5) y) True) (Eq False True)))) % 7.96/8.17 Clause #75 (by clausification #[68]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.17 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.17 (Or (Eq (cQ a_1 y) False) (Or (Eq (cP a_2 y (skS.0 0 a_1 a_3)) True) (Eq (cQ (skS.0 4 a_4) y) True))) % 7.96/8.17 Clause #77 (by superposition #[75, 34]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cP a_1 y (skS.0 0 (skS.0 3 a_2) a_3)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_4) y) True) (Or (Eq (cQ (skS.0 4 a_5) y) True) (Eq False True)))) % 7.96/8.20 Clause #81 (by clausification #[71]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cQ a_1 y) False) (Or (Eq (cR (skS.0 2 a_1 a_2 a_3 a_4)) True) (Eq (cQ (skS.0 4 a_5) y) True))) % 7.96/8.20 Clause #83 (by superposition #[81, 34]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cR (skS.0 2 (skS.0 3 a_1) a_2 a_3 a_4)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_5) y) True) (Or (Eq (cQ (skS.0 4 a_6) y) True) (Eq False True)))) % 7.96/8.20 Clause #90 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cQ (skS.0 4 a) y) True) % 7.96/8.20 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) (Or (Eq (cQ a_3 y) False) (Eq (cP a_4 y (skS.0 0 a_3 a_5)) True))) % 7.96/8.20 Clause #92 (by superposition #[90, 34]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.96/8.20 Or (Eq (cQ (skS.0 4 a) y) True) % 7.96/8.20 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) % 7.96/8.20 (Or (Eq (cP a_3 y (skS.0 0 (skS.0 3 a_4) a_5)) True) (Or (Eq (cQ (skS.0 4 a_6) y) True) (Eq False True)))) % 7.96/8.20 Clause #99 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cP a_1 y (skS.0 0 (skS.0 3 a_2) a_3)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_4) y) True) (Eq (cQ (skS.0 4 a_5) y) True))) % 7.96/8.20 Clause #115 (by equality factoring #[99]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cP a_1 y (skS.0 0 (skS.0 3 a_2) a_3)) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_4) y) True))) % 7.96/8.20 Clause #117 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cP a_1 y (skS.0 0 (skS.0 3 a_2) a_3)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_4) y) True) (Or (Eq True False) (Eq True False)))) % 7.96/8.20 Clause #119 (by clausification #[117]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cP a_1 y (skS.0 0 (skS.0 3 a_2) a_3)) True) (Or (Eq (cQ (skS.0 4 a_4) y) True) (Eq True False))) % 7.96/8.20 Clause #120 (by clausification #[119]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cP a_1 y (skS.0 0 (skS.0 3 a_2) a_3)) True) (Eq (cQ (skS.0 4 a_4) y) True)) % 7.96/8.20 Clause #121 (by superposition #[120, 40]): ∀ (a a_1 a_2 a_3 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_1) y) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq True False) (Eq (cR a_3) False)))) % 7.96/8.20 Clause #137 (by clausification #[121]): ∀ (a a_1 a_2 a_3 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_1) y) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Eq (cR a_3) False))) % 7.96/8.20 Clause #193 (by clausification #[83]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cR (skS.0 2 (skS.0 3 a_1) a_2 a_3 a_4)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_5) y) True) (Eq (cQ (skS.0 4 a_6) y) True))) % 7.96/8.20 Clause #214 (by equality factoring #[193]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cR (skS.0 2 (skS.0 3 a_1) a_2 a_3 a_4)) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_5) y) True))) % 7.96/8.20 Clause #216 (by clausification #[214]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cR (skS.0 2 (skS.0 3 a_1) a_2 a_3 a_4)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_5) y) True) (Or (Eq True False) (Eq True False)))) % 7.96/8.20 Clause #218 (by clausification #[216]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cR (skS.0 2 (skS.0 3 a_1) a_2 a_3 a_4)) True) (Or (Eq (cQ (skS.0 4 a_5) y) True) (Eq True False))) % 7.96/8.20 Clause #219 (by clausification #[218]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 2 (skS.0 3 a_1) a_2 a_3 a_4)) True) (Eq (cQ (skS.0 4 a_5) y) True)) % 7.96/8.20 Clause #224 (by superposition #[219, 137]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.96/8.20 Or (Eq (cR (skS.0 8 a)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_1) y) True) % 7.96/8.20 (Or (Eq (cR (skS.0 8 a_2)) True) % 7.96/8.20 (Or (Eq (cQ (skS.0 4 a_3) y) True) (Or (Eq (cQ (skS.0 4 a_4) y) True) (Eq True False))))) % 8.06/8.23 Clause #241 (by clausification #[224]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_1) y) True) % 8.06/8.23 (Or (Eq (cR (skS.0 8 a_2)) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Eq (cQ (skS.0 4 a_4) y) True)))) % 8.06/8.23 Clause #276 (by equality factoring #[241]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_1) y) True) % 8.06/8.23 (Or (Eq (cR (skS.0 8 a_2)) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_3) y) True)))) % 8.06/8.23 Clause #277 (by clausification #[276]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_1) y) True) % 8.06/8.23 (Or (Eq (cR (skS.0 8 a_2)) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Or (Eq True False) (Eq True False))))) % 8.06/8.23 Clause #279 (by clausification #[277]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_1) y) True) % 8.06/8.23 (Or (Eq (cR (skS.0 8 a_2)) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Eq True False)))) % 8.06/8.23 Clause #280 (by clausification #[279]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_1) y) True) (Or (Eq (cR (skS.0 8 a_2)) True) (Eq (cQ (skS.0 4 a_3) y) True))) % 8.06/8.23 Clause #310 (by equality factoring #[280]): ∀ (a a_1 a_2 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_2) y) True))) % 8.06/8.23 Clause #343 (by clausification #[310]): ∀ (a a_1 a_2 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) % 8.06/8.23 (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq True False) (Eq True False)))) % 8.06/8.23 Clause #345 (by clausification #[343]): ∀ (a a_1 a_2 : Iota), % 8.06/8.23 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Eq True False))) % 8.06/8.23 Clause #346 (by clausification #[345]): ∀ (a a_1 a_2 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Eq (cQ (skS.0 4 a_2) y) True)) % 8.06/8.23 Clause #359 (by equality factoring #[346]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Ne True True) (Eq (cR (skS.0 8 a_1)) True)) % 8.06/8.23 Clause #360 (by clausification #[359]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq True False) (Eq True False))) % 8.06/8.23 Clause #362 (by clausification #[360]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Eq True False)) % 8.06/8.23 Clause #363 (by clausification #[362]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Eq (cR (skS.0 8 a_1)) True) % 8.06/8.23 Clause #500 (by clausification #[92]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.06/8.23 Or (Eq (cQ (skS.0 4 a) y) True) % 8.06/8.23 (Or (Eq (cP a_1 y (skS.0 1 a_2)) True) % 8.06/8.23 (Or (Eq (cP a_3 y (skS.0 0 (skS.0 3 a_4) a_5)) True) (Eq (cQ (skS.0 4 a_6) y) True))) % 8.06/8.23 Clause #535 (by equality factoring #[500]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.06/8.23 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.23 (Or (Eq (cP a_2 y (skS.0 0 (skS.0 3 a_3) a_4)) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_5) y) True))) % 8.06/8.23 Clause #536 (by clausification #[535]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.06/8.23 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.23 (Or (Eq (cP a_2 y (skS.0 0 (skS.0 3 a_3) a_4)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_5) y) True) (Or (Eq True False) (Eq True False)))) % 8.06/8.23 Clause #538 (by clausification #[536]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.06/8.23 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.23 (Or (Eq (cP a_2 y (skS.0 0 (skS.0 3 a_3) a_4)) True) (Or (Eq (cQ (skS.0 4 a_5) y) True) (Eq True False))) % 8.06/8.23 Clause #539 (by clausification #[538]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.06/8.23 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.23 (Or (Eq (cP a_2 y (skS.0 0 (skS.0 3 a_3) a_4)) True) (Eq (cQ (skS.0 4 a_5) y) True)) % 8.06/8.23 Clause #543 (by superposition #[539, 40]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.06/8.23 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Or (Eq True False) (Eq (cR a_4) False)))) % 8.06/8.23 Clause #561 (by clausification #[543]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.06/8.23 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.23 (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Eq (cR a_4) False))) % 8.06/8.26 Clause #563 (by superposition #[561, 363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.06/8.26 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.26 (Or (Eq (cQ (skS.0 4 a_2) y) True) % 8.06/8.26 (Or (Eq (cQ (skS.0 4 a_3) y) True) (Or (Eq (cQ (skS.0 4 a_4) y) True) (Eq False True)))) % 8.06/8.26 Clause #566 (by clausification #[563]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.06/8.26 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.26 (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Eq (cQ (skS.0 4 a_4) y) True))) % 8.06/8.26 Clause #584 (by equality factoring #[566]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.26 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.26 (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_3) y) True))) % 8.06/8.26 Clause #585 (by clausification #[584]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.26 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.26 (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Or (Eq True False) (Eq True False)))) % 8.06/8.26 Clause #587 (by clausification #[585]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.26 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.06/8.26 (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq (cQ (skS.0 4 a_3) y) True) (Eq True False))) % 8.06/8.26 Clause #588 (by clausification #[587]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.26 Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Eq (cQ (skS.0 4 a_3) y) True)) % 8.06/8.26 Clause #606 (by equality factoring #[588]): ∀ (a a_1 a_2 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_2) y) True)) % 8.06/8.26 Clause #630 (by clausification #[606]): ∀ (a a_1 a_2 : Iota), % 8.06/8.26 Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Or (Eq True False) (Eq True False))) % 8.06/8.26 Clause #632 (by clausification #[630]): ∀ (a a_1 a_2 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Eq True False)) % 8.06/8.26 Clause #633 (by clausification #[632]): ∀ (a a_1 a_2 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Eq (cQ (skS.0 4 a_2) y) True) % 8.06/8.26 Clause #634 (by superposition #[633, 40]): ∀ (a a_1 a_2 : Iota), % 8.06/8.26 Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cQ (skS.0 4 a_1) y) True) (Or (Eq True False) (Eq (cR a_2) False))) % 8.06/8.26 Clause #650 (by clausification #[634]): ∀ (a a_1 a_2 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cQ (skS.0 4 a_1) y) True) (Eq (cR a_2) False)) % 8.06/8.26 Clause #652 (by superposition #[650, 363]): ∀ (a a_1 a_2 : Iota), % 8.06/8.26 Or (Eq (cQ (skS.0 4 a) y) True) % 8.06/8.26 (Or (Eq (cQ (skS.0 4 a_1) y) True) (Or (Eq (cQ (skS.0 4 a_2) y) True) (Eq False True))) % 8.06/8.26 Clause #656 (by clausification #[652]): ∀ (a a_1 a_2 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cQ (skS.0 4 a_1) y) True) (Eq (cQ (skS.0 4 a_2) y) True)) % 8.06/8.26 Clause #669 (by equality factoring #[656]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Ne True True) (Eq (cQ (skS.0 4 a_1) y) True)) % 8.06/8.26 Clause #671 (by clausification #[669]): ∀ (a a_1 : Iota), % 8.06/8.26 Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cQ (skS.0 4 a_1) y) True) (Or (Eq True False) (Eq True False))) % 8.06/8.26 Clause #673 (by clausification #[671]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq (cQ (skS.0 4 a_1) y) True) (Eq True False)) % 8.06/8.26 Clause #674 (by clausification #[673]): ∀ (a a_1 : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Eq (cQ (skS.0 4 a_1) y) True) % 8.06/8.26 Clause #686 (by equality factoring #[674]): ∀ (a : Iota), Or (Ne True True) (Eq (cQ (skS.0 4 a) y) True) % 8.06/8.26 Clause #687 (by clausification #[686]): ∀ (a : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Or (Eq True False) (Eq True False)) % 8.06/8.26 Clause #689 (by clausification #[687]): ∀ (a : Iota), Or (Eq (cQ (skS.0 4 a) y) True) (Eq True False) % 8.06/8.26 Clause #690 (by clausification #[689]): ∀ (a : Iota), Eq (cQ (skS.0 4 a) y) True % 8.06/8.26 Clause #691 (by superposition #[690, 23]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.06/8.26 Or (Eq True False) % 8.06/8.26 (Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cQ a_2 y) False) (Eq (cP a_3 y (skS.0 0 a_2 a_4)) True))) % 8.06/8.26 Clause #692 (by superposition #[690, 65]): ∀ (a a_1 a_2 a_3 : Iota), % 8.06/8.26 Or (Eq True False) (Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cQ a_1 y) False) (Eq (cP a_2 y (skS.0 0 a_1 a_3)) True))) % 8.06/8.26 Clause #693 (by superposition #[690, 69]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.06/8.26 Or (Eq True False) (Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cQ a_1 y) False) (Eq (cR (skS.0 2 a_1 a_2 a_3 a_4)) True))) % 8.13/8.29 Clause #703 (by clausification #[692]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cQ a_1 y) False) (Eq (cP a_2 y (skS.0 0 a_1 a_3)) True)) % 8.13/8.29 Clause #709 (by superposition #[703, 690]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cP a_1 y (skS.0 0 (skS.0 4 a_2) a_3)) True) (Eq False True)) % 8.13/8.29 Clause #711 (by clausification #[709]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Eq (cP a_1 y (skS.0 0 (skS.0 4 a_2) a_3)) True) % 8.13/8.29 Clause #717 (by superposition #[711, 58]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq True False) (Or (Eq (cR a_1) False) (Or (Eq (cP (skS.0 6 a_2 a_3 a_4) y a_3) False) (Eq (cR a_5) False)))) % 8.13/8.29 Clause #723 (by clausification #[693]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cQ a_1 y) False) (Eq (cR (skS.0 2 a_1 a_2 a_3 a_4)) True)) % 8.13/8.29 Clause #728 (by superposition #[723, 690]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 2 (skS.0 4 a_1) a_2 a_3 a_4)) True) (Eq False True)) % 8.13/8.29 Clause #729 (by clausification #[691]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.29 Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cQ a_2 y) False) (Eq (cP a_3 y (skS.0 0 a_2 a_4)) True)) % 8.13/8.29 Clause #734 (by superposition #[729, 690]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.29 Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cP a_2 y (skS.0 0 (skS.0 4 a_3) a_4)) True) (Eq False True)) % 8.13/8.29 Clause #735 (by clausification #[734]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Eq (cP a_2 y (skS.0 0 (skS.0 4 a_3) a_4)) True) % 8.13/8.29 Clause #739 (by superposition #[735, 58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.13/8.29 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.13/8.29 (Or (Eq True False) (Or (Eq (cR a_2) False) (Or (Eq (cP (skS.0 6 a_3 a_4 a_5) y a_4) False) (Eq (cR a_6) False)))) % 8.13/8.29 Clause #746 (by clausification #[728]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Eq (cR (skS.0 2 (skS.0 4 a_1) a_2 a_3 a_4)) True) % 8.13/8.29 Clause #774 (by clausification #[717]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq (cR a_1) False) (Or (Eq (cP (skS.0 6 a_2 a_3 a_4) y a_3) False) (Eq (cR a_5) False))) % 8.13/8.29 Clause #778 (by superposition #[774, 746]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq (cP (skS.0 6 a_1 a_2 a_3) y a_2) False) % 8.13/8.29 (Or (Eq (cR a_4) False) (Or (Eq (cR (skS.0 8 a_5)) True) (Eq False True)))) % 8.13/8.29 Clause #864 (by clausification #[739]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.13/8.29 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.13/8.29 (Or (Eq (cR a_2) False) (Or (Eq (cP (skS.0 6 a_3 a_4 a_5) y a_4) False) (Eq (cR a_6) False))) % 8.13/8.29 Clause #875 (by clausification #[778]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq (cP (skS.0 6 a_1 a_2 a_3) y a_2) False) (Or (Eq (cR a_4) False) (Eq (cR (skS.0 8 a_5)) True))) % 8.13/8.29 Clause #876 (by superposition #[875, 711]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq (cR a_1) False) (Or (Eq (cR (skS.0 8 a_2)) True) (Or (Eq (cR (skS.0 8 a_3)) True) (Eq False True)))) % 8.13/8.29 Clause #882 (by clausification #[876]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR a_1) False) (Or (Eq (cR (skS.0 8 a_2)) True) (Eq (cR (skS.0 8 a_3)) True))) % 8.13/8.29 Clause #885 (by superposition #[882, 746]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq (cR (skS.0 8 a_1)) True) % 8.13/8.29 (Or (Eq (cR (skS.0 8 a_2)) True) (Or (Eq (cR (skS.0 8 a_3)) True) (Eq False True)))) % 8.13/8.29 Clause #896 (by clausification #[885]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cR (skS.0 8 a_2)) True) (Eq (cR (skS.0 8 a_3)) True))) % 8.13/8.29 Clause #901 (by equality factoring #[896]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Ne True True) (Eq (cR (skS.0 8 a_2)) True))) % 8.13/8.29 Clause #903 (by clausification #[901]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Or (Eq (cR (skS.0 8 a)) True) % 8.13/8.29 (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cR (skS.0 8 a_2)) True) (Or (Eq True False) (Eq True False)))) % 8.13/8.32 Clause #905 (by clausification #[903]): ∀ (a a_1 a_2 : Iota), % 8.13/8.32 Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq (cR (skS.0 8 a_2)) True) (Eq True False))) % 8.13/8.32 Clause #906 (by clausification #[905]): ∀ (a a_1 a_2 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Eq (cR (skS.0 8 a_2)) True)) % 8.13/8.32 Clause #910 (by equality factoring #[906]): ∀ (a a_1 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Or (Ne True True) (Eq (cR (skS.0 8 a_1)) True)) % 8.13/8.32 Clause #911 (by clausification #[910]): ∀ (a a_1 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Or (Eq True False) (Eq True False))) % 8.13/8.32 Clause #913 (by clausification #[911]): ∀ (a a_1 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Or (Eq (cR (skS.0 8 a_1)) True) (Eq True False)) % 8.13/8.32 Clause #914 (by clausification #[913]): ∀ (a a_1 : Iota), Or (Eq (cR (skS.0 8 a)) True) (Eq (cR (skS.0 8 a_1)) True) % 8.13/8.32 Clause #916 (by equality factoring #[914]): ∀ (a : Iota), Or (Ne True True) (Eq (cR (skS.0 8 a)) True) % 8.13/8.32 Clause #917 (by clausification #[916]): ∀ (a : Iota), Or (Eq (cR (skS.0 8 a)) True) (Or (Eq True False) (Eq True False)) % 8.13/8.32 Clause #919 (by clausification #[917]): ∀ (a : Iota), Or (Eq (cR (skS.0 8 a)) True) (Eq True False) % 8.13/8.32 Clause #920 (by clausification #[919]): ∀ (a : Iota), Eq (cR (skS.0 8 a)) True % 8.13/8.32 Clause #921 (by superposition #[920, 864]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.32 Or (Eq (cP a y (skS.0 1 a_1)) True) % 8.13/8.32 (Or (Eq True False) (Or (Eq (cP (skS.0 6 a_2 a_3 a_4) y a_3) False) (Eq (cR a_5) False))) % 8.13/8.32 Clause #923 (by clausification #[921]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.32 Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cP (skS.0 6 a_2 a_3 a_4) y a_3) False) (Eq (cR a_5) False)) % 8.13/8.32 Clause #925 (by superposition #[923, 735]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.32 Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cR a_2) False) (Or (Eq (cP a_3 y (skS.0 1 a_4)) True) (Eq False True))) % 8.13/8.32 Clause #929 (by clausification #[925]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.32 Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cR a_2) False) (Eq (cP a_3 y (skS.0 1 a_4)) True)) % 8.13/8.32 Clause #931 (by superposition #[929, 920]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq (cP a_2 y (skS.0 1 a_3)) True) (Eq False True)) % 8.13/8.32 Clause #932 (by clausification #[931]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Eq (cP a_2 y (skS.0 1 a_3)) True) % 8.13/8.32 Clause #934 (by equality factoring #[932]): ∀ (a a_1 : Iota), Or (Ne True True) (Eq (cP a y (skS.0 1 a_1)) True) % 8.13/8.32 Clause #935 (by clausification #[934]): ∀ (a a_1 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Or (Eq True False) (Eq True False)) % 8.13/8.32 Clause #937 (by clausification #[935]): ∀ (a a_1 : Iota), Or (Eq (cP a y (skS.0 1 a_1)) True) (Eq True False) % 8.13/8.32 Clause #938 (by clausification #[937]): ∀ (a a_1 : Iota), Eq (cP a y (skS.0 1 a_1)) True % 8.13/8.32 Clause #939 (by superposition #[938, 58]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.32 Or (Eq True False) (Or (Eq (cR a) False) (Or (Eq (cP (skS.0 6 a_1 a_2 a_3) y a_2) False) (Eq (cR a_4) False))) % 8.13/8.32 Clause #941 (by clausification #[939]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cR a) False) (Or (Eq (cP (skS.0 6 a_1 a_2 a_3) y a_2) False) (Eq (cR a_4) False)) % 8.13/8.32 Clause #942 (by superposition #[941, 920]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cP (skS.0 6 a a_1 a_2) y a_1) False) (Or (Eq (cR a_3) False) (Eq False True)) % 8.13/8.32 Clause #943 (by clausification #[942]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cP (skS.0 6 a a_1 a_2) y a_1) False) (Eq (cR a_3) False) % 8.13/8.32 Clause #944 (by superposition #[943, 938]): ∀ (a : Iota), Or (Eq (cR a) False) (Eq False True) % 8.13/8.32 Clause #945 (by clausification #[944]): ∀ (a : Iota), Eq (cR a) False % 8.13/8.32 Clause #946 (by superposition #[945, 920]): Eq False True % 8.13/8.32 Clause #947 (by clausification #[946]): False % 8.13/8.32 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------