%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO179^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n004.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:41 PM UTC 2025 % Result : Theorem 9.05s 9.20s % Output : Proof 9.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYO179^5 : TPTP v9.2.0. Released v4.0.0. % 0.13/0.13 % Command : duper %s % 0.14/0.34 % Computer : n004.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 13:48:08 EDT 2025 % 0.14/0.34 % CPUTime : % 9.05/9.20 SZS status Theorem for theBenchmark.p % 9.05/9.20 SZS output start Proof for theBenchmark.p % 9.05/9.20 Clause #0 (by assumption #[]): Eq % 9.05/9.20 (Not % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) % 9.05/9.20 (Or (cR cA cD) (cG cA cD))) % 9.05/9.20 (Or (cR cA cE) (cG cA cE))) % 9.05/9.20 (Or (cR cA cF) (cG cA cF))) % 9.05/9.20 (Or (cR cB cC) (cG cB cC))) % 9.05/9.20 (Or (cR cB cD) (cG cB cD))) % 9.05/9.20 (Or (cR cB cE) (cG cB cE))) % 9.05/9.20 (Or (cR cB cF) (cG cB cF))) % 9.05/9.20 (Or (cR cC cD) (cG cC cD))) % 9.05/9.20 (Or (cR cC cE) (cG cC cE))) % 9.05/9.20 (Or (cR cC cF) (cG cC cF))) % 9.05/9.20 (Or (cR cD cE) (cG cD cE))) % 9.05/9.20 (Or (cR cD cF) (cG cD cF))) % 9.05/9.20 (Or (cR cE cF) (cG cE cF)) → % 9.05/9.20 Or (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cR Xa Xb) (cR Xa Xc)) (cR Xb Xc)) % 9.05/9.20 (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cG Xa Xb) (cG Xa Xc)) (cG Xb Xc)))) % 9.05/9.20 True % 9.05/9.20 Clause #1 (by clausification #[0]): Eq % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.20 (Or (cR cA cE) (cG cA cE))) % 9.05/9.20 (Or (cR cA cF) (cG cA cF))) % 9.05/9.20 (Or (cR cB cC) (cG cB cC))) % 9.05/9.20 (Or (cR cB cD) (cG cB cD))) % 9.05/9.20 (Or (cR cB cE) (cG cB cE))) % 9.05/9.20 (Or (cR cB cF) (cG cB cF))) % 9.05/9.20 (Or (cR cC cD) (cG cC cD))) % 9.05/9.20 (Or (cR cC cE) (cG cC cE))) % 9.05/9.20 (Or (cR cC cF) (cG cC cF))) % 9.05/9.20 (Or (cR cD cE) (cG cD cE))) % 9.05/9.20 (Or (cR cD cF) (cG cD cF))) % 9.05/9.20 (Or (cR cE cF) (cG cE cF)) → % 9.05/9.20 Or (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cR Xa Xb) (cR Xa Xc)) (cR Xb Xc)) % 9.05/9.20 (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cG Xa Xb) (cG Xa Xc)) (cG Xb Xc))) % 9.05/9.20 False % 9.05/9.20 Clause #2 (by clausification #[1]): Eq % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.20 (Or (cR cA cE) (cG cA cE))) % 9.05/9.20 (Or (cR cA cF) (cG cA cF))) % 9.05/9.20 (Or (cR cB cC) (cG cB cC))) % 9.05/9.20 (Or (cR cB cD) (cG cB cD))) % 9.05/9.20 (Or (cR cB cE) (cG cB cE))) % 9.05/9.20 (Or (cR cB cF) (cG cB cF))) % 9.05/9.20 (Or (cR cC cD) (cG cC cD))) % 9.05/9.20 (Or (cR cC cE) (cG cC cE))) % 9.05/9.20 (Or (cR cC cF) (cG cC cF))) % 9.05/9.20 (Or (cR cD cE) (cG cD cE))) % 9.05/9.20 (Or (cR cD cF) (cG cD cF))) % 9.05/9.20 (Or (cR cE cF) (cG cE cF))) % 9.05/9.20 True % 9.05/9.20 Clause #3 (by clausification #[1]): Eq % 9.05/9.20 (Or (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cR Xa Xb) (cR Xa Xc)) (cR Xb Xc)) % 9.05/9.20 (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cG Xa Xb) (cG Xa Xc)) (cG Xb Xc))) % 9.05/9.20 False % 9.05/9.20 Clause #4 (by clausification #[2]): Eq (Or (cR cE cF) (cG cE cF)) True % 9.05/9.20 Clause #5 (by clausification #[2]): Eq % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And % 9.05/9.20 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.20 (Or (cR cA cE) (cG cA cE))) % 9.05/9.20 (Or (cR cA cF) (cG cA cF))) % 9.05/9.22 (Or (cR cB cC) (cG cB cC))) % 9.05/9.22 (Or (cR cB cD) (cG cB cD))) % 9.05/9.22 (Or (cR cB cE) (cG cB cE))) % 9.05/9.22 (Or (cR cB cF) (cG cB cF))) % 9.05/9.22 (Or (cR cC cD) (cG cC cD))) % 9.05/9.22 (Or (cR cC cE) (cG cC cE))) % 9.05/9.22 (Or (cR cC cF) (cG cC cF))) % 9.05/9.22 (Or (cR cD cE) (cG cD cE))) % 9.05/9.22 (Or (cR cD cF) (cG cD cF))) % 9.05/9.22 True % 9.05/9.22 Clause #6 (by clausification #[4]): Or (Eq (cR cE cF) True) (Eq (cG cE cF) True) % 9.05/9.22 Clause #7 (by clausification #[3]): Eq (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cG Xa Xb) (cG Xa Xc)) (cG Xb Xc)) False % 9.05/9.22 Clause #8 (by clausification #[3]): Eq (Exists fun Xa => Exists fun Xb => Exists fun Xc => And (And (cR Xa Xb) (cR Xa Xc)) (cR Xb Xc)) False % 9.05/9.22 Clause #9 (by clausification #[7]): ∀ (a : Iota), Eq (Exists fun Xb => Exists fun Xc => And (And (cG a Xb) (cG a Xc)) (cG Xb Xc)) False % 9.05/9.22 Clause #10 (by clausification #[9]): ∀ (a a_1 : Iota), Eq (Exists fun Xc => And (And (cG a a_1) (cG a Xc)) (cG a_1 Xc)) False % 9.05/9.22 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 : Iota), Eq (And (And (cG a a_1) (cG a a_2)) (cG a_1 a_2)) False % 9.05/9.22 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (cG a a_1) (cG a a_2)) False) (Eq (cG a_1 a_2) False) % 9.05/9.22 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 : Iota), Or (Eq (cG a a_1) False) (Or (Eq (cG a_2 a) False) (Eq (cG a_2 a_1) False)) % 9.05/9.22 Clause #14 (by superposition #[13, 6]): ∀ (a : Iota), Or (Eq (cG a cE) False) (Or (Eq (cG a cF) False) (Or (Eq (cR cE cF) True) (Eq False True))) % 9.05/9.22 Clause #15 (by clausification #[14]): ∀ (a : Iota), Or (Eq (cG a cE) False) (Or (Eq (cG a cF) False) (Eq (cR cE cF) True)) % 9.05/9.22 Clause #16 (by clausification #[8]): ∀ (a : Iota), Eq (Exists fun Xb => Exists fun Xc => And (And (cR a Xb) (cR a Xc)) (cR Xb Xc)) False % 9.05/9.22 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), Eq (Exists fun Xc => And (And (cR a a_1) (cR a Xc)) (cR a_1 Xc)) False % 9.05/9.22 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), Eq (And (And (cR a a_1) (cR a a_2)) (cR a_1 a_2)) False % 9.05/9.22 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (cR a a_1) (cR a a_2)) False) (Eq (cR a_1 a_2) False) % 9.05/9.22 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 : Iota), Or (Eq (cR a a_1) False) (Or (Eq (cR a_2 a) False) (Eq (cR a_2 a_1) False)) % 9.05/9.22 Clause #21 (by clausification #[5]): Eq (Or (cR cD cF) (cG cD cF)) True % 9.05/9.22 Clause #22 (by clausification #[5]): Eq % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.22 (Or (cR cA cE) (cG cA cE))) % 9.05/9.22 (Or (cR cA cF) (cG cA cF))) % 9.05/9.22 (Or (cR cB cC) (cG cB cC))) % 9.05/9.22 (Or (cR cB cD) (cG cB cD))) % 9.05/9.22 (Or (cR cB cE) (cG cB cE))) % 9.05/9.22 (Or (cR cB cF) (cG cB cF))) % 9.05/9.22 (Or (cR cC cD) (cG cC cD))) % 9.05/9.22 (Or (cR cC cE) (cG cC cE))) % 9.05/9.22 (Or (cR cC cF) (cG cC cF))) % 9.05/9.22 (Or (cR cD cE) (cG cD cE))) % 9.05/9.22 True % 9.05/9.22 Clause #23 (by clausification #[21]): Or (Eq (cR cD cF) True) (Eq (cG cD cF) True) % 9.05/9.22 Clause #24 (by superposition #[23, 13]): ∀ (a : Iota), Or (Eq (cR cD cF) True) (Or (Eq True False) (Or (Eq (cG a cD) False) (Eq (cG a cF) False))) % 9.05/9.22 Clause #25 (by clausification #[22]): Eq (Or (cR cD cE) (cG cD cE)) True % 9.05/9.22 Clause #26 (by clausification #[22]): Eq % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And % 9.05/9.22 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.22 (Or (cR cA cE) (cG cA cE))) % 9.05/9.22 (Or (cR cA cF) (cG cA cF))) % 9.05/9.22 (Or (cR cB cC) (cG cB cC))) % 9.05/9.22 (Or (cR cB cD) (cG cB cD))) % 9.05/9.22 (Or (cR cB cE) (cG cB cE))) % 9.05/9.22 (Or (cR cB cF) (cG cB cF))) % 9.05/9.22 (Or (cR cC cD) (cG cC cD))) % 9.05/9.22 (Or (cR cC cE) (cG cC cE))) % 9.05/9.22 (Or (cR cC cF) (cG cC cF))) % 9.05/9.22 True % 9.05/9.22 Clause #27 (by clausification #[25]): Or (Eq (cR cD cE) True) (Eq (cG cD cE) True) % 9.05/9.25 Clause #29 (by superposition #[27, 13]): ∀ (a : Iota), Or (Eq (cR cD cE) True) (Or (Eq True False) (Or (Eq (cG a cD) False) (Eq (cG a cE) False))) % 9.05/9.25 Clause #30 (by clausification #[29]): ∀ (a : Iota), Or (Eq (cR cD cE) True) (Or (Eq (cG a cD) False) (Eq (cG a cE) False)) % 9.05/9.25 Clause #35 (by clausification #[24]): ∀ (a : Iota), Or (Eq (cR cD cF) True) (Or (Eq (cG a cD) False) (Eq (cG a cF) False)) % 9.05/9.25 Clause #37 (by clausification #[26]): Eq (Or (cR cC cF) (cG cC cF)) True % 9.05/9.25 Clause #38 (by clausification #[26]): Eq % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.25 (Or (cR cA cE) (cG cA cE))) % 9.05/9.25 (Or (cR cA cF) (cG cA cF))) % 9.05/9.25 (Or (cR cB cC) (cG cB cC))) % 9.05/9.25 (Or (cR cB cD) (cG cB cD))) % 9.05/9.25 (Or (cR cB cE) (cG cB cE))) % 9.05/9.25 (Or (cR cB cF) (cG cB cF))) % 9.05/9.25 (Or (cR cC cD) (cG cC cD))) % 9.05/9.25 (Or (cR cC cE) (cG cC cE))) % 9.05/9.25 True % 9.05/9.25 Clause #39 (by clausification #[37]): Or (Eq (cR cC cF) True) (Eq (cG cC cF) True) % 9.05/9.25 Clause #40 (by superposition #[39, 13]): ∀ (a : Iota), Or (Eq (cR cC cF) True) (Or (Eq True False) (Or (Eq (cG a cC) False) (Eq (cG a cF) False))) % 9.05/9.25 Clause #41 (by clausification #[40]): ∀ (a : Iota), Or (Eq (cR cC cF) True) (Or (Eq (cG a cC) False) (Eq (cG a cF) False)) % 9.05/9.25 Clause #42 (by clausification #[38]): Eq (Or (cR cC cE) (cG cC cE)) True % 9.05/9.25 Clause #43 (by clausification #[38]): Eq % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.25 (Or (cR cA cE) (cG cA cE))) % 9.05/9.25 (Or (cR cA cF) (cG cA cF))) % 9.05/9.25 (Or (cR cB cC) (cG cB cC))) % 9.05/9.25 (Or (cR cB cD) (cG cB cD))) % 9.05/9.25 (Or (cR cB cE) (cG cB cE))) % 9.05/9.25 (Or (cR cB cF) (cG cB cF))) % 9.05/9.25 (Or (cR cC cD) (cG cC cD))) % 9.05/9.25 True % 9.05/9.25 Clause #44 (by clausification #[42]): Or (Eq (cR cC cE) True) (Eq (cG cC cE) True) % 9.05/9.25 Clause #45 (by superposition #[44, 15]): Or (Eq (cR cC cE) True) (Or (Eq True False) (Or (Eq (cG cC cF) False) (Eq (cR cE cF) True))) % 9.05/9.25 Clause #46 (by superposition #[44, 13]): ∀ (a : Iota), Or (Eq (cR cC cE) True) (Or (Eq True False) (Or (Eq (cG a cC) False) (Eq (cG a cE) False))) % 9.05/9.25 Clause #47 (by clausification #[46]): ∀ (a : Iota), Or (Eq (cR cC cE) True) (Or (Eq (cG a cC) False) (Eq (cG a cE) False)) % 9.05/9.25 Clause #48 (by clausification #[45]): Or (Eq (cR cC cE) True) (Or (Eq (cG cC cF) False) (Eq (cR cE cF) True)) % 9.05/9.25 Clause #49 (by superposition #[48, 39]): Or (Eq (cR cC cE) True) (Or (Eq (cR cE cF) True) (Or (Eq (cR cC cF) True) (Eq False True))) % 9.05/9.25 Clause #50 (by clausification #[49]): Or (Eq (cR cC cE) True) (Or (Eq (cR cE cF) True) (Eq (cR cC cF) True)) % 9.05/9.25 Clause #51 (by superposition #[50, 20]): ∀ (a : Iota), % 9.05/9.25 Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Or (Eq (cR a cE) False) (Eq (cR a cF) False)))) % 9.05/9.25 Clause #52 (by clausification #[43]): Eq (Or (cR cC cD) (cG cC cD)) True % 9.05/9.25 Clause #53 (by clausification #[43]): Eq % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And % 9.05/9.25 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.25 (Or (cR cA cE) (cG cA cE))) % 9.05/9.25 (Or (cR cA cF) (cG cA cF))) % 9.05/9.25 (Or (cR cB cC) (cG cB cC))) % 9.05/9.25 (Or (cR cB cD) (cG cB cD))) % 9.05/9.25 (Or (cR cB cE) (cG cB cE))) % 9.05/9.25 (Or (cR cB cF) (cG cB cF))) % 9.05/9.25 True % 9.05/9.25 Clause #54 (by clausification #[52]): Or (Eq (cR cC cD) True) (Eq (cG cC cD) True) % 9.05/9.25 Clause #55 (by superposition #[54, 30]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cE) True) (Or (Eq True False) (Eq (cG cC cE) False))) % 9.05/9.25 Clause #56 (by superposition #[54, 35]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cF) True) (Or (Eq True False) (Eq (cG cC cF) False))) % 9.05/9.25 Clause #57 (by superposition #[54, 13]): ∀ (a : Iota), Or (Eq (cR cC cD) True) (Or (Eq True False) (Or (Eq (cG a cC) False) (Eq (cG a cD) False))) % 9.05/9.25 Clause #58 (by clausification #[57]): ∀ (a : Iota), Or (Eq (cR cC cD) True) (Or (Eq (cG a cC) False) (Eq (cG a cD) False)) % 9.05/9.27 Clause #59 (by clausification #[56]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cF) True) (Eq (cG cC cF) False)) % 9.05/9.27 Clause #60 (by superposition #[59, 39]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cF) True) (Or (Eq (cR cC cF) True) (Eq False True))) % 9.05/9.27 Clause #61 (by clausification #[60]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cF) True) (Eq (cR cC cF) True)) % 9.05/9.27 Clause #62 (by superposition #[61, 20]): ∀ (a : Iota), % 9.05/9.27 Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Or (Eq (cR a cD) False) (Eq (cR a cF) False)))) % 9.05/9.27 Clause #63 (by clausification #[55]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cE) True) (Eq (cG cC cE) False)) % 9.05/9.27 Clause #64 (by superposition #[63, 44]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cE) True) (Or (Eq (cR cC cE) True) (Eq False True))) % 9.05/9.27 Clause #65 (by clausification #[64]): Or (Eq (cR cC cD) True) (Or (Eq (cR cD cE) True) (Eq (cR cC cE) True)) % 9.05/9.27 Clause #66 (by superposition #[65, 20]): ∀ (a : Iota), % 9.05/9.27 Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Or (Eq True False) (Or (Eq (cR a cD) False) (Eq (cR a cE) False)))) % 9.05/9.27 Clause #67 (by clausification #[51]): ∀ (a : Iota), Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Or (Eq (cR a cE) False) (Eq (cR a cF) False))) % 9.05/9.27 Clause #69 (by clausification #[66]): ∀ (a : Iota), Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR a cD) False) (Eq (cR a cE) False))) % 9.05/9.27 Clause #70 (by clausification #[62]): ∀ (a : Iota), Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Or (Eq (cR a cD) False) (Eq (cR a cF) False))) % 9.05/9.27 Clause #78 (by clausification #[53]): Eq (Or (cR cB cF) (cG cB cF)) True % 9.05/9.27 Clause #79 (by clausification #[53]): Eq % 9.05/9.27 (And % 9.05/9.27 (And % 9.05/9.27 (And % 9.05/9.27 (And % 9.05/9.27 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.27 (Or (cR cA cE) (cG cA cE))) % 9.05/9.27 (Or (cR cA cF) (cG cA cF))) % 9.05/9.27 (Or (cR cB cC) (cG cB cC))) % 9.05/9.27 (Or (cR cB cD) (cG cB cD))) % 9.05/9.27 (Or (cR cB cE) (cG cB cE))) % 9.05/9.27 True % 9.05/9.27 Clause #80 (by clausification #[78]): Or (Eq (cR cB cF) True) (Eq (cG cB cF) True) % 9.05/9.27 Clause #81 (by superposition #[80, 13]): ∀ (a : Iota), Or (Eq (cR cB cF) True) (Or (Eq True False) (Or (Eq (cG a cB) False) (Eq (cG a cF) False))) % 9.05/9.27 Clause #82 (by clausification #[81]): ∀ (a : Iota), Or (Eq (cR cB cF) True) (Or (Eq (cG a cB) False) (Eq (cG a cF) False)) % 9.05/9.27 Clause #83 (by clausification #[79]): Eq (Or (cR cB cE) (cG cB cE)) True % 9.05/9.27 Clause #84 (by clausification #[79]): Eq % 9.05/9.27 (And % 9.05/9.27 (And % 9.05/9.27 (And % 9.05/9.27 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.27 (Or (cR cA cE) (cG cA cE))) % 9.05/9.27 (Or (cR cA cF) (cG cA cF))) % 9.05/9.27 (Or (cR cB cC) (cG cB cC))) % 9.05/9.27 (Or (cR cB cD) (cG cB cD))) % 9.05/9.27 True % 9.05/9.27 Clause #85 (by clausification #[83]): Or (Eq (cR cB cE) True) (Eq (cG cB cE) True) % 9.05/9.27 Clause #86 (by superposition #[85, 15]): Or (Eq (cR cB cE) True) (Or (Eq True False) (Or (Eq (cG cB cF) False) (Eq (cR cE cF) True))) % 9.05/9.27 Clause #87 (by superposition #[85, 13]): ∀ (a : Iota), Or (Eq (cR cB cE) True) (Or (Eq True False) (Or (Eq (cG a cB) False) (Eq (cG a cE) False))) % 9.05/9.27 Clause #88 (by clausification #[87]): ∀ (a : Iota), Or (Eq (cR cB cE) True) (Or (Eq (cG a cB) False) (Eq (cG a cE) False)) % 9.05/9.27 Clause #89 (by clausification #[86]): Or (Eq (cR cB cE) True) (Or (Eq (cG cB cF) False) (Eq (cR cE cF) True)) % 9.05/9.27 Clause #90 (by superposition #[89, 80]): Or (Eq (cR cB cE) True) (Or (Eq (cR cE cF) True) (Or (Eq (cR cB cF) True) (Eq False True))) % 9.05/9.27 Clause #91 (by clausification #[90]): Or (Eq (cR cB cE) True) (Or (Eq (cR cE cF) True) (Eq (cR cB cF) True)) % 9.05/9.27 Clause #92 (by superposition #[91, 20]): ∀ (a : Iota), % 9.05/9.27 Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Or (Eq (cR a cE) False) (Eq (cR a cF) False)))) % 9.05/9.27 Clause #93 (by clausification #[84]): Eq (Or (cR cB cD) (cG cB cD)) True % 9.05/9.27 Clause #94 (by clausification #[84]): Eq % 9.05/9.27 (And % 9.05/9.27 (And % 9.05/9.27 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.05/9.27 (Or (cR cA cE) (cG cA cE))) % 9.05/9.27 (Or (cR cA cF) (cG cA cF))) % 9.05/9.27 (Or (cR cB cC) (cG cB cC))) % 9.15/9.30 True % 9.15/9.30 Clause #95 (by clausification #[93]): Or (Eq (cR cB cD) True) (Eq (cG cB cD) True) % 9.15/9.30 Clause #96 (by superposition #[95, 30]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cE) True) (Or (Eq True False) (Eq (cG cB cE) False))) % 9.15/9.30 Clause #97 (by superposition #[95, 35]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cF) True) (Or (Eq True False) (Eq (cG cB cF) False))) % 9.15/9.30 Clause #98 (by superposition #[95, 13]): ∀ (a : Iota), Or (Eq (cR cB cD) True) (Or (Eq True False) (Or (Eq (cG a cB) False) (Eq (cG a cD) False))) % 9.15/9.30 Clause #99 (by clausification #[98]): ∀ (a : Iota), Or (Eq (cR cB cD) True) (Or (Eq (cG a cB) False) (Eq (cG a cD) False)) % 9.15/9.30 Clause #100 (by clausification #[97]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cF) True) (Eq (cG cB cF) False)) % 9.15/9.30 Clause #101 (by superposition #[100, 80]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cF) True) (Or (Eq (cR cB cF) True) (Eq False True))) % 9.15/9.30 Clause #102 (by clausification #[101]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cF) True) (Eq (cR cB cF) True)) % 9.15/9.30 Clause #103 (by superposition #[102, 20]): ∀ (a : Iota), % 9.15/9.30 Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Or (Eq (cR a cD) False) (Eq (cR a cF) False)))) % 9.15/9.30 Clause #104 (by clausification #[96]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cE) True) (Eq (cG cB cE) False)) % 9.15/9.30 Clause #105 (by superposition #[104, 85]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cE) True) (Or (Eq (cR cB cE) True) (Eq False True))) % 9.15/9.30 Clause #106 (by clausification #[105]): Or (Eq (cR cB cD) True) (Or (Eq (cR cD cE) True) (Eq (cR cB cE) True)) % 9.15/9.30 Clause #108 (by superposition #[106, 20]): ∀ (a : Iota), % 9.15/9.30 Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Or (Eq (cR a cD) False) (Eq (cR a cE) False)))) % 9.15/9.30 Clause #109 (by clausification #[92]): ∀ (a : Iota), Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR a cE) False) (Eq (cR a cF) False))) % 9.15/9.30 Clause #111 (by superposition #[109, 106]): Or (Eq (cR cB cE) True) % 9.15/9.30 (Or (Eq (cR cB cF) True) % 9.15/9.30 (Or (Eq (cR cD cF) False) (Or (Eq (cR cB cD) True) (Or (Eq False True) (Eq (cR cB cE) True))))) % 9.15/9.30 Clause #112 (by clausification #[103]): ∀ (a : Iota), Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR a cD) False) (Eq (cR a cF) False))) % 9.15/9.30 Clause #113 (by clausification #[108]): ∀ (a : Iota), Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR a cD) False) (Eq (cR a cE) False))) % 9.15/9.30 Clause #117 (by clausification #[111]): Or (Eq (cR cB cE) True) % 9.15/9.30 (Or (Eq (cR cB cF) True) (Or (Eq (cR cD cF) False) (Or (Eq (cR cB cD) True) (Eq (cR cB cE) True)))) % 9.15/9.30 Clause #118 (by eliminate duplicate literals #[117]): Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR cD cF) False) (Eq (cR cB cD) True))) % 9.15/9.30 Clause #120 (by superposition #[118, 102]): Or (Eq (cR cB cE) True) % 9.15/9.30 (Or (Eq (cR cB cF) True) % 9.15/9.30 (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cD) True) (Or (Eq False True) (Eq (cR cB cF) True))))) % 9.15/9.30 Clause #121 (by clausification #[120]): Or (Eq (cR cB cE) True) % 9.15/9.30 (Or (Eq (cR cB cF) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cF) True)))) % 9.15/9.30 Clause #122 (by eliminate duplicate literals #[121]): Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Eq (cR cB cD) True)) % 9.15/9.30 Clause #123 (by superposition #[122, 20]): ∀ (a : Iota), % 9.15/9.30 Or (Eq (cR cB cE) True) (Or (Eq (cR cB cD) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cF) False)))) % 9.15/9.30 Clause #124 (by clausification #[94]): Eq (Or (cR cB cC) (cG cB cC)) True % 9.15/9.30 Clause #125 (by clausification #[94]): Eq % 9.15/9.30 (And % 9.15/9.30 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.15/9.30 (Or (cR cA cE) (cG cA cE))) % 9.15/9.30 (Or (cR cA cF) (cG cA cF))) % 9.15/9.30 True % 9.15/9.30 Clause #126 (by clausification #[124]): Or (Eq (cR cB cC) True) (Eq (cG cB cC) True) % 9.15/9.30 Clause #127 (by superposition #[126, 41]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Eq (cG cB cF) False))) % 9.15/9.30 Clause #128 (by superposition #[126, 47]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cE) True) (Or (Eq True False) (Eq (cG cB cE) False))) % 9.15/9.30 Clause #129 (by superposition #[126, 58]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cD) True) (Or (Eq True False) (Eq (cG cB cD) False))) % 9.16/9.33 Clause #130 (by superposition #[126, 13]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq True False) (Or (Eq (cG a cB) False) (Eq (cG a cC) False))) % 9.16/9.33 Clause #131 (by clausification #[130]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq (cG a cB) False) (Eq (cG a cC) False)) % 9.16/9.33 Clause #132 (by clausification #[129]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cD) True) (Eq (cG cB cD) False)) % 9.16/9.33 Clause #133 (by superposition #[132, 95]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cB cD) True) (Eq False True))) % 9.16/9.33 Clause #134 (by clausification #[133]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cD) True) (Eq (cR cB cD) True)) % 9.16/9.33 Clause #137 (by superposition #[134, 20]): ∀ (a : Iota), % 9.16/9.33 Or (Eq (cR cB cC) True) (Or (Eq (cR cB cD) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cD) False)))) % 9.16/9.33 Clause #138 (by clausification #[128]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cE) True) (Eq (cG cB cE) False)) % 9.16/9.33 Clause #139 (by superposition #[138, 85]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR cB cE) True) (Eq False True))) % 9.16/9.33 Clause #140 (by clausification #[139]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cE) True) (Eq (cR cB cE) True)) % 9.16/9.33 Clause #142 (by superposition #[140, 109]): Or (Eq (cR cB cC) True) % 9.16/9.33 (Or (Eq (cR cB cE) True) % 9.16/9.33 (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Eq (cR cC cF) False))))) % 9.16/9.33 Clause #143 (by superposition #[140, 20]): ∀ (a : Iota), % 9.16/9.33 Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cE) False)))) % 9.16/9.33 Clause #147 (by clausification #[127]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cF) True) (Eq (cG cB cF) False)) % 9.16/9.33 Clause #148 (by superposition #[147, 80]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cF) True) (Or (Eq (cR cB cF) True) (Eq False True))) % 9.16/9.33 Clause #149 (by clausification #[148]): Or (Eq (cR cB cC) True) (Or (Eq (cR cC cF) True) (Eq (cR cB cF) True)) % 9.16/9.33 Clause #150 (by superposition #[149, 20]): ∀ (a : Iota), % 9.16/9.33 Or (Eq (cR cB cC) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cF) False)))) % 9.16/9.33 Clause #151 (by clausification #[150]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR a cC) False) (Eq (cR a cF) False))) % 9.16/9.33 Clause #152 (by clausification #[143]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR a cC) False) (Eq (cR a cE) False))) % 9.16/9.33 Clause #153 (by clausification #[137]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR a cC) False) (Eq (cR a cD) False))) % 9.16/9.33 Clause #156 (by clausification #[123]): ∀ (a : Iota), Or (Eq (cR cB cE) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR a cB) False) (Eq (cR a cF) False))) % 9.16/9.33 Clause #183 (by clausification #[125]): Eq (Or (cR cA cF) (cG cA cF)) True % 9.16/9.33 Clause #184 (by clausification #[125]): Eq % 9.16/9.33 (And (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) % 9.16/9.33 (Or (cR cA cE) (cG cA cE))) % 9.16/9.33 True % 9.16/9.33 Clause #185 (by clausification #[183]): Or (Eq (cR cA cF) True) (Eq (cG cA cF) True) % 9.16/9.33 Clause #192 (by clausification #[142]): Or (Eq (cR cB cC) True) % 9.16/9.33 (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Eq (cR cC cF) False)))) % 9.16/9.33 Clause #193 (by eliminate duplicate literals #[192]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Eq (cR cC cF) False))) % 9.16/9.33 Clause #195 (by superposition #[193, 149]): Or (Eq (cR cB cC) True) % 9.16/9.33 (Or (Eq (cR cB cE) True) % 9.16/9.33 (Or (Eq (cR cB cF) True) (Or (Eq (cR cB cC) True) (Or (Eq False True) (Eq (cR cB cF) True))))) % 9.16/9.33 Clause #196 (by clausification #[195]): Or (Eq (cR cB cC) True) % 9.16/9.33 (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR cB cC) True) (Eq (cR cB cF) True)))) % 9.16/9.33 Clause #197 (by eliminate duplicate literals #[196]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Eq (cR cB cF) True)) % 9.16/9.33 Clause #200 (by superposition #[197, 20]): ∀ (a : Iota), % 9.16/9.33 Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cF) False)))) % 9.16/9.33 Clause #203 (by clausification #[200]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR a cB) False) (Eq (cR a cF) False))) % 9.16/9.35 Clause #241 (by clausification #[184]): Eq (Or (cR cA cE) (cG cA cE)) True % 9.16/9.35 Clause #242 (by clausification #[184]): Eq (And (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) (Or (cR cA cD) (cG cA cD))) True % 9.16/9.35 Clause #243 (by clausification #[241]): Or (Eq (cR cA cE) True) (Eq (cG cA cE) True) % 9.16/9.35 Clause #244 (by superposition #[243, 15]): Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cG cA cF) False) (Eq (cR cE cF) True))) % 9.16/9.35 Clause #247 (by clausification #[244]): Or (Eq (cR cA cE) True) (Or (Eq (cG cA cF) False) (Eq (cR cE cF) True)) % 9.16/9.35 Clause #248 (by superposition #[247, 185]): Or (Eq (cR cA cE) True) (Or (Eq (cR cE cF) True) (Or (Eq (cR cA cF) True) (Eq False True))) % 9.16/9.35 Clause #249 (by clausification #[248]): Or (Eq (cR cA cE) True) (Or (Eq (cR cE cF) True) (Eq (cR cA cF) True)) % 9.16/9.35 Clause #250 (by superposition #[249, 20]): ∀ (a : Iota), % 9.16/9.35 Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq True False) (Or (Eq (cR a cE) False) (Eq (cR a cF) False)))) % 9.16/9.35 Clause #251 (by clausification #[250]): ∀ (a : Iota), Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR a cE) False) (Eq (cR a cF) False))) % 9.16/9.35 Clause #275 (by clausification #[242]): Eq (Or (cR cA cD) (cG cA cD)) True % 9.16/9.35 Clause #276 (by clausification #[242]): Eq (And (Or (cR cA cB) (cG cA cB)) (Or (cR cA cC) (cG cA cC))) True % 9.16/9.35 Clause #277 (by clausification #[275]): Or (Eq (cR cA cD) True) (Eq (cG cA cD) True) % 9.16/9.35 Clause #278 (by superposition #[277, 30]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cE) True) (Or (Eq True False) (Eq (cG cA cE) False))) % 9.16/9.35 Clause #279 (by superposition #[277, 35]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cF) True) (Or (Eq True False) (Eq (cG cA cF) False))) % 9.16/9.35 Clause #284 (by clausification #[279]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cF) True) (Eq (cG cA cF) False)) % 9.16/9.35 Clause #285 (by superposition #[284, 185]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cF) True) (Or (Eq (cR cA cF) True) (Eq False True))) % 9.16/9.35 Clause #286 (by clausification #[285]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cF) True) (Eq (cR cA cF) True)) % 9.16/9.35 Clause #291 (by superposition #[286, 20]): ∀ (a : Iota), % 9.16/9.35 Or (Eq (cR cA cD) True) (Or (Eq (cR cA cF) True) (Or (Eq True False) (Or (Eq (cR a cD) False) (Eq (cR a cF) False)))) % 9.16/9.35 Clause #292 (by clausification #[278]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cE) True) (Eq (cG cA cE) False)) % 9.16/9.35 Clause #293 (by superposition #[292, 243]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cE) True) (Or (Eq (cR cA cE) True) (Eq False True))) % 9.16/9.35 Clause #294 (by clausification #[293]): Or (Eq (cR cA cD) True) (Or (Eq (cR cD cE) True) (Eq (cR cA cE) True)) % 9.16/9.35 Clause #297 (by superposition #[294, 251]): Or (Eq (cR cA cD) True) % 9.16/9.35 (Or (Eq (cR cA cE) True) % 9.16/9.35 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq True False) (Eq (cR cD cF) False))))) % 9.16/9.35 Clause #298 (by superposition #[294, 20]): ∀ (a : Iota), % 9.16/9.35 Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cD) False) (Eq (cR a cE) False)))) % 9.16/9.35 Clause #299 (by clausification #[276]): Eq (Or (cR cA cC) (cG cA cC)) True % 9.16/9.35 Clause #300 (by clausification #[276]): Eq (Or (cR cA cB) (cG cA cB)) True % 9.16/9.35 Clause #301 (by clausification #[299]): Or (Eq (cR cA cC) True) (Eq (cG cA cC) True) % 9.16/9.35 Clause #302 (by superposition #[301, 41]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Eq (cG cA cF) False))) % 9.16/9.35 Clause #303 (by superposition #[301, 47]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cE) True) (Or (Eq True False) (Eq (cG cA cE) False))) % 9.16/9.35 Clause #304 (by superposition #[301, 58]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cD) True) (Or (Eq True False) (Eq (cG cA cD) False))) % 9.16/9.35 Clause #308 (by clausification #[300]): Or (Eq (cR cA cB) True) (Eq (cG cA cB) True) % 9.16/9.35 Clause #309 (by superposition #[308, 82]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Eq (cG cA cF) False))) % 9.16/9.35 Clause #310 (by superposition #[308, 88]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Eq (cG cA cE) False))) % 9.16/9.35 Clause #311 (by superposition #[308, 99]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Or (Eq True False) (Eq (cG cA cD) False))) % 9.16/9.38 Clause #312 (by superposition #[308, 131]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cC) True) (Or (Eq True False) (Eq (cG cA cC) False))) % 9.16/9.38 Clause #314 (by clausification #[302]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cF) True) (Eq (cG cA cF) False)) % 9.16/9.38 Clause #315 (by superposition #[314, 185]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cF) True) (Or (Eq (cR cA cF) True) (Eq False True))) % 9.16/9.38 Clause #316 (by clausification #[315]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cF) True) (Eq (cR cA cF) True)) % 9.16/9.38 Clause #320 (by superposition #[316, 20]): ∀ (a : Iota), % 9.16/9.38 Or (Eq (cR cA cC) True) (Or (Eq (cR cA cF) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cF) False)))) % 9.16/9.38 Clause #322 (by clausification #[312]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cC) True) (Eq (cG cA cC) False)) % 9.16/9.38 Clause #323 (by superposition #[322, 301]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cC) True) (Or (Eq (cR cA cC) True) (Eq False True))) % 9.16/9.38 Clause #326 (by clausification #[323]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cC) True) (Eq (cR cA cC) True)) % 9.16/9.38 Clause #329 (by clausification #[309]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cF) True) (Eq (cG cA cF) False)) % 9.16/9.38 Clause #330 (by superposition #[329, 185]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR cA cF) True) (Eq False True))) % 9.16/9.38 Clause #331 (by clausification #[330]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cF) True) (Eq (cR cA cF) True)) % 9.16/9.38 Clause #335 (by clausification #[304]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cD) True) (Eq (cG cA cD) False)) % 9.16/9.38 Clause #336 (by superposition #[335, 277]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cD) True) (Eq False True))) % 9.16/9.38 Clause #338 (by clausification #[336]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cD) True) (Eq (cR cA cD) True)) % 9.16/9.38 Clause #343 (by superposition #[338, 20]): ∀ (a : Iota), % 9.16/9.38 Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cD) False)))) % 9.16/9.38 Clause #344 (by clausification #[303]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cE) True) (Eq (cG cA cE) False)) % 9.16/9.38 Clause #345 (by superposition #[344, 243]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR cA cE) True) (Eq False True))) % 9.16/9.38 Clause #346 (by clausification #[345]): Or (Eq (cR cA cC) True) (Or (Eq (cR cC cE) True) (Eq (cR cA cE) True)) % 9.16/9.38 Clause #349 (by superposition #[346, 251]): Or (Eq (cR cA cC) True) % 9.16/9.38 (Or (Eq (cR cA cE) True) % 9.16/9.38 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq True False) (Eq (cR cC cF) False))))) % 9.16/9.38 Clause #350 (by superposition #[346, 20]): ∀ (a : Iota), % 9.16/9.38 Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cE) False)))) % 9.16/9.38 Clause #351 (by clausification #[311]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq (cG cA cD) False)) % 9.16/9.38 Clause #352 (by superposition #[351, 277]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cD) True) (Eq False True))) % 9.16/9.38 Clause #353 (by clausification #[352]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq (cR cA cD) True)) % 9.16/9.38 Clause #359 (by clausification #[310]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Eq (cG cA cE) False)) % 9.16/9.38 Clause #360 (by superposition #[359, 243]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR cA cE) True) (Eq False True))) % 9.16/9.38 Clause #361 (by clausification #[360]): Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Eq (cR cA cE) True)) % 9.16/9.38 Clause #364 (by superposition #[361, 251]): Or (Eq (cR cA cB) True) % 9.16/9.38 (Or (Eq (cR cA cE) True) % 9.16/9.38 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq True False) (Eq (cR cB cF) False))))) % 9.16/9.38 Clause #366 (by clausification #[291]): ∀ (a : Iota), Or (Eq (cR cA cD) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR a cD) False) (Eq (cR a cF) False))) % 9.16/9.38 Clause #368 (by superposition #[366, 338]): Or (Eq (cR cA cD) True) % 9.16/9.38 (Or (Eq (cR cA cF) True) % 9.16/9.38 (Or (Eq (cR cC cF) False) (Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cD) True))))) % 9.16/9.38 Clause #369 (by superposition #[366, 353]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) % 9.26/9.41 (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cD) True))))) % 9.26/9.41 Clause #370 (by clausification #[298]): ∀ (a : Iota), Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cD) False) (Eq (cR a cE) False))) % 9.26/9.41 Clause #372 (by superposition #[370, 338]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cE) True) % 9.26/9.41 (Or (Eq (cR cC cE) False) (Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cD) True))))) % 9.26/9.41 Clause #373 (by superposition #[370, 353]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cE) True) % 9.26/9.41 (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cD) True))))) % 9.26/9.41 Clause #374 (by clausification #[320]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR a cC) False) (Eq (cR a cF) False))) % 9.26/9.41 Clause #375 (by superposition #[374, 326]): Or (Eq (cR cA cC) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) % 9.26/9.41 (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True))))) % 9.26/9.41 Clause #379 (by clausification #[350]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cC) False) (Eq (cR a cE) False))) % 9.26/9.41 Clause #380 (by superposition #[379, 326]): Or (Eq (cR cA cC) True) % 9.26/9.41 (Or (Eq (cR cA cE) True) % 9.26/9.41 (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True))))) % 9.26/9.41 Clause #383 (by clausification #[343]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR a cC) False) (Eq (cR a cD) False))) % 9.26/9.41 Clause #384 (by superposition #[383, 326]): Or (Eq (cR cA cC) True) % 9.26/9.41 (Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cB cD) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True))))) % 9.26/9.41 Clause #399 (by clausification #[364]): Or (Eq (cR cA cB) True) % 9.26/9.41 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Eq (cR cB cF) False)))) % 9.26/9.41 Clause #400 (by eliminate duplicate literals #[399]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Eq (cR cB cF) False))) % 9.26/9.41 Clause #404 (by superposition #[400, 331]): Or (Eq (cR cA cB) True) % 9.26/9.41 (Or (Eq (cR cA cE) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cF) True))))) % 9.26/9.41 Clause #405 (by clausification #[404]): Or (Eq (cR cA cB) True) % 9.26/9.41 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cF) True)))) % 9.26/9.41 Clause #406 (by eliminate duplicate literals #[405]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cF) True)) % 9.26/9.41 Clause #430 (by clausification #[369]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cD) True)))) % 9.26/9.41 Clause #431 (by eliminate duplicate literals #[430]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR cB cF) False) (Eq (cR cA cB) True))) % 9.26/9.41 Clause #435 (by superposition #[431, 331]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) % 9.26/9.41 (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cF) True))))) % 9.26/9.41 Clause #436 (by clausification #[435]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cF) True)))) % 9.26/9.41 Clause #437 (by eliminate duplicate literals #[436]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cF) True) (Eq (cR cA cB) True)) % 9.26/9.41 Clause #444 (by clausification #[368]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) (Or (Eq (cR cC cF) False) (Or (Eq (cR cA cC) True) (Eq (cR cA cD) True)))) % 9.26/9.41 Clause #445 (by eliminate duplicate literals #[444]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR cC cF) False) (Eq (cR cA cC) True))) % 9.26/9.41 Clause #449 (by superposition #[445, 316]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) % 9.26/9.41 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cF) True))))) % 9.26/9.41 Clause #450 (by clausification #[449]): Or (Eq (cR cA cD) True) % 9.26/9.41 (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cF) True)))) % 9.26/9.41 Clause #451 (by eliminate duplicate literals #[450]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cF) True) (Eq (cR cA cC) True)) % 9.26/9.43 Clause #462 (by clausification #[349]): Or (Eq (cR cA cC) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Eq (cR cC cF) False)))) % 9.26/9.43 Clause #463 (by eliminate duplicate literals #[462]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Eq (cR cC cF) False))) % 9.26/9.43 Clause #467 (by superposition #[463, 316]): Or (Eq (cR cA cC) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) % 9.26/9.43 (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cF) True))))) % 9.26/9.43 Clause #470 (by clausification #[467]): Or (Eq (cR cA cC) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cF) True)))) % 9.26/9.43 Clause #471 (by eliminate duplicate literals #[470]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cF) True)) % 9.26/9.43 Clause #491 (by clausification #[297]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Eq (cR cD cF) False)))) % 9.26/9.43 Clause #492 (by eliminate duplicate literals #[491]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Eq (cR cD cF) False))) % 9.26/9.43 Clause #496 (by superposition #[492, 286]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) % 9.26/9.43 (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cF) True))))) % 9.26/9.43 Clause #497 (by clausification #[496]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cF) True)))) % 9.26/9.43 Clause #498 (by eliminate duplicate literals #[497]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cF) True)) % 9.26/9.43 Clause #511 (by clausification #[373]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cD) True)))) % 9.26/9.43 Clause #512 (by eliminate duplicate literals #[511]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cB cE) False) (Eq (cR cA cB) True))) % 9.26/9.43 Clause #514 (by superposition #[512, 361]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) % 9.26/9.43 (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cE) True))))) % 9.26/9.43 Clause #515 (by clausification #[514]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cE) True)))) % 9.26/9.43 Clause #516 (by eliminate duplicate literals #[515]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cB) True)) % 9.26/9.43 Clause #518 (by superposition #[516, 67]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cB) True) % 9.26/9.43 (Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Eq (cR cA cF) False))))) % 9.26/9.43 Clause #530 (by clausification #[518]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Eq (cR cA cF) False)))) % 9.26/9.43 Clause #532 (by superposition #[530, 437]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cB) True) % 9.26/9.43 (Or (Eq (cR cC cE) True) % 9.26/9.43 (Or (Eq (cR cC cF) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cB) True)))))) % 9.26/9.43 Clause #547 (by clausification #[372]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cC cE) False) (Or (Eq (cR cA cC) True) (Eq (cR cA cD) True)))) % 9.26/9.43 Clause #548 (by eliminate duplicate literals #[547]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cC cE) False) (Eq (cR cA cC) True))) % 9.26/9.43 Clause #550 (by superposition #[548, 346]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) % 9.26/9.43 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cE) True))))) % 9.26/9.43 Clause #553 (by clausification #[550]): Or (Eq (cR cA cD) True) % 9.26/9.43 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cE) True)))) % 9.26/9.43 Clause #554 (by eliminate duplicate literals #[553]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cC) True)) % 9.26/9.43 Clause #566 (by clausification #[384]): Or (Eq (cR cA cC) True) % 9.26/9.43 (Or (Eq (cR cA cD) True) (Or (Eq (cR cB cD) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True)))) % 9.26/9.43 Clause #567 (by eliminate duplicate literals #[566]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cB cD) False) (Eq (cR cA cB) True))) % 9.26/9.46 Clause #568 (by superposition #[567, 353]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cD) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cD) True))))) % 9.26/9.46 Clause #570 (by clausification #[568]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cD) True)))) % 9.26/9.46 Clause #571 (by eliminate duplicate literals #[570]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cB) True)) % 9.26/9.46 Clause #572 (by superposition #[571, 69]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) % 9.26/9.46 (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Or (Eq True False) (Eq (cR cA cE) False))))) % 9.26/9.46 Clause #573 (by superposition #[571, 70]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) % 9.26/9.46 (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Eq (cR cA cF) False))))) % 9.26/9.46 Clause #574 (by superposition #[571, 112]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) % 9.26/9.46 (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Eq (cR cA cF) False))))) % 9.26/9.46 Clause #575 (by superposition #[571, 113]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) % 9.26/9.46 (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Eq (cR cA cE) False))))) % 9.26/9.46 Clause #582 (by clausification #[575]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Eq (cR cA cE) False)))) % 9.26/9.46 Clause #585 (by clausification #[574]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Eq (cR cA cF) False)))) % 9.26/9.46 Clause #591 (by clausification #[573]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Eq (cR cA cF) False)))) % 9.26/9.46 Clause #597 (by clausification #[572]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Eq (cR cA cE) False)))) % 9.26/9.46 Clause #617 (by clausification #[375]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cF) True) (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True)))) % 9.26/9.46 Clause #618 (by eliminate duplicate literals #[617]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cF) True) (Or (Eq (cR cB cF) False) (Eq (cR cA cB) True))) % 9.26/9.46 Clause #622 (by superposition #[618, 331]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cF) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cF) True))))) % 9.26/9.46 Clause #623 (by clausification #[622]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cF) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cF) True)))) % 9.26/9.46 Clause #624 (by eliminate duplicate literals #[623]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cF) True) (Eq (cR cA cB) True)) % 9.26/9.46 Clause #629 (by superposition #[624, 585]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) % 9.26/9.46 (Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Eq True False)))))) % 9.26/9.46 Clause #630 (by superposition #[624, 591]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) % 9.26/9.46 (Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Eq True False)))))) % 9.26/9.46 Clause #643 (by clausification #[380]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cE) True) (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True)))) % 9.26/9.46 Clause #644 (by eliminate duplicate literals #[643]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cB cE) False) (Eq (cR cA cB) True))) % 9.26/9.46 Clause #646 (by superposition #[644, 361]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cE) True) % 9.26/9.46 (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cE) True))))) % 9.26/9.46 Clause #656 (by clausification #[646]): Or (Eq (cR cA cC) True) % 9.26/9.46 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cE) True)))) % 9.26/9.46 Clause #657 (by eliminate duplicate literals #[656]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cB) True)) % 9.26/9.46 Clause #658 (by superposition #[657, 582]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Eq True False)))))) % 9.26/9.49 Clause #659 (by superposition #[657, 597]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Eq True False)))))) % 9.26/9.49 Clause #661 (by superposition #[657, 67]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Eq (cR cA cF) False))))) % 9.26/9.49 Clause #662 (by superposition #[657, 109]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Eq (cR cA cF) False))))) % 9.26/9.49 Clause #665 (by clausification #[662]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Eq (cR cA cF) False)))) % 9.26/9.49 Clause #671 (by superposition #[665, 624]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cB cE) True) % 9.26/9.49 (Or (Eq (cR cB cF) True) (Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cB) True)))))) % 9.26/9.49 Clause #672 (by clausification #[661]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Eq (cR cA cF) False)))) % 9.26/9.49 Clause #678 (by superposition #[672, 624]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cC cE) True) % 9.26/9.49 (Or (Eq (cR cC cF) True) (Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cB) True)))))) % 9.26/9.49 Clause #921 (by clausification #[659]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cC cE) True))))) % 9.26/9.49 Clause #922 (by eliminate duplicate literals #[921]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cC cE) True))) % 9.26/9.49 Clause #928 (by superposition #[922, 20]): ∀ (a : Iota), % 9.26/9.49 Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cC cD) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cE) False))))) % 9.26/9.49 Clause #931 (by clausification #[928]): ∀ (a : Iota), % 9.26/9.49 Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR a cC) False) (Eq (cR a cE) False)))) % 9.26/9.49 Clause #932 (by superposition #[931, 326]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cC cD) True) % 9.26/9.49 (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True)))))) % 9.26/9.49 Clause #933 (by clausification #[630]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cC cF) True))))) % 9.26/9.49 Clause #934 (by eliminate duplicate literals #[933]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cC cF) True))) % 9.26/9.49 Clause #943 (by superposition #[934, 20]): ∀ (a : Iota), % 9.26/9.49 Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cC cD) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cF) False))))) % 9.26/9.49 Clause #944 (by clausification #[943]): ∀ (a : Iota), % 9.26/9.49 Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR a cC) False) (Eq (cR a cF) False)))) % 9.26/9.49 Clause #945 (by superposition #[944, 326]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cC cD) True) % 9.26/9.49 (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True)))))) % 9.26/9.49 Clause #946 (by clausification #[945]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cC cD) True) (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True))))) % 9.26/9.49 Clause #947 (by eliminate duplicate literals #[946]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cB cF) False))) % 9.26/9.49 Clause #977 (by clausification #[629]): Or (Eq (cR cA cC) True) % 9.26/9.49 (Or (Eq (cR cA cB) True) % 9.26/9.49 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cF) True))))) % 9.26/9.49 Clause #978 (by eliminate duplicate literals #[977]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cF) True))) % 9.35/9.51 Clause #1019 (by clausification #[658]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cE) True))))) % 9.35/9.51 Clause #1020 (by eliminate duplicate literals #[1019]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cE) True))) % 9.35/9.51 Clause #1074 (by clausification #[932]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cD) True) (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True))))) % 9.35/9.51 Clause #1075 (by eliminate duplicate literals #[1074]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cB cE) False))) % 9.35/9.51 Clause #1113 (by clausification #[532]): Or (Eq (cR cA cD) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cB) True))))) % 9.35/9.51 Clause #1114 (by eliminate duplicate literals #[1113]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Eq (cR cC cF) True))) % 9.35/9.51 Clause #1125 (by superposition #[1114, 20]): ∀ (a : Iota), % 9.35/9.51 Or (Eq (cR cA cD) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cF) False))))) % 9.35/9.51 Clause #1126 (by clausification #[1125]): ∀ (a : Iota), % 9.35/9.51 Or (Eq (cR cA cD) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR a cC) False) (Eq (cR a cF) False)))) % 9.35/9.51 Clause #1198 (by clausification #[678]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) (Or (Eq (cR cC cF) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cB) True))))) % 9.35/9.51 Clause #1199 (by eliminate duplicate literals #[1198]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Eq (cR cC cF) True))) % 9.35/9.51 Clause #1210 (by superposition #[1199, 20]): ∀ (a : Iota), % 9.35/9.51 Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cF) False))))) % 9.35/9.51 Clause #1213 (by clausification #[1210]): ∀ (a : Iota), % 9.35/9.51 Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR a cC) False) (Eq (cR a cF) False)))) % 9.35/9.51 Clause #1214 (by superposition #[1213, 326]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) % 9.35/9.51 (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True)))))) % 9.35/9.51 Clause #1215 (by clausification #[1214]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) (Or (Eq (cR cB cF) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True))))) % 9.35/9.51 Clause #1216 (by eliminate duplicate literals #[1215]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Eq (cR cB cF) False))) % 9.35/9.51 Clause #1222 (by superposition #[1216, 978]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) % 9.35/9.51 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq False True)))))) % 9.35/9.51 Clause #1233 (by clausification #[1222]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cC cE) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cB cD) True))))) % 9.35/9.51 Clause #1234 (by eliminate duplicate literals #[1233]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Eq (cR cB cD) True))) % 9.35/9.51 Clause #1240 (by superposition #[1234, 20]): ∀ (a : Iota), % 9.35/9.51 Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cB cD) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cE) False))))) % 9.35/9.51 Clause #1241 (by clausification #[1240]): ∀ (a : Iota), % 9.35/9.51 Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR a cC) False) (Eq (cR a cE) False)))) % 9.35/9.51 Clause #1242 (by superposition #[1241, 326]): Or (Eq (cR cA cC) True) % 9.35/9.51 (Or (Eq (cR cA cB) True) % 9.35/9.51 (Or (Eq (cR cB cD) True) % 9.35/9.51 (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True)))))) % 9.35/9.54 Clause #1243 (by clausification #[1242]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True))))) % 9.35/9.54 Clause #1244 (by eliminate duplicate literals #[1243]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cE) False))) % 9.35/9.54 Clause #1247 (by superposition #[1244, 1020]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cD) True) % 9.35/9.54 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) True) (Eq False True)))))) % 9.35/9.54 Clause #1256 (by clausification #[1247]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cB cD) True))))) % 9.35/9.54 Clause #1257 (by eliminate duplicate literals #[1256]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cB cD) True)) % 9.35/9.54 Clause #1296 (by clausification #[671]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cB) True))))) % 9.35/9.54 Clause #1297 (by eliminate duplicate literals #[1296]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Eq (cR cB cF) True))) % 9.35/9.54 Clause #1301 (by superposition #[1297, 947]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cE) True) % 9.35/9.54 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq True False)))))) % 9.35/9.54 Clause #1336 (by clausification #[1301]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cE) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cC cD) True))))) % 9.35/9.54 Clause #1337 (by eliminate duplicate literals #[1336]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Eq (cR cC cD) True))) % 9.35/9.54 Clause #1348 (by superposition #[1337, 20]): ∀ (a : Iota), % 9.35/9.54 Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cE) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cD) False))))) % 9.35/9.54 Clause #1349 (by clausification #[1348]): ∀ (a : Iota), % 9.35/9.54 Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR a cC) False) (Eq (cR a cD) False)))) % 9.35/9.54 Clause #1350 (by superposition #[1349, 326]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cE) True) % 9.35/9.54 (Or (Eq (cR cB cD) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True)))))) % 9.35/9.54 Clause #1351 (by clausification #[1350]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cE) True) (Or (Eq (cR cB cD) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True))))) % 9.35/9.54 Clause #1352 (by eliminate duplicate literals #[1351]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Eq (cR cB cD) False))) % 9.35/9.54 Clause #1355 (by superposition #[1352, 1257]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cB cE) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq False True))))) % 9.35/9.54 Clause #1356 (by clausification #[1355]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cB) True)))) % 9.35/9.54 Clause #1357 (by eliminate duplicate literals #[1356]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cB cE) True)) % 9.35/9.54 Clause #1360 (by superposition #[1357, 1075]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) % 9.35/9.54 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq True False))))) % 9.35/9.54 Clause #1376 (by clausification #[1360]): Or (Eq (cR cA cC) True) % 9.35/9.54 (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cC cD) True)))) % 9.35/9.54 Clause #1377 (by eliminate duplicate literals #[1376]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cC cD) True)) % 9.35/9.54 Clause #1388 (by superposition #[1377, 20]): ∀ (a : Iota), % 9.35/9.54 Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cD) False)))) % 9.35/9.54 Clause #1399 (by clausification #[1388]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR a cC) False) (Eq (cR a cD) False))) % 9.35/9.56 Clause #1400 (by superposition #[1399, 326]): Or (Eq (cR cA cC) True) % 9.35/9.56 (Or (Eq (cR cA cB) True) % 9.35/9.56 (Or (Eq (cR cB cD) False) (Or (Eq (cR cA cB) True) (Or (Eq False True) (Eq (cR cA cC) True))))) % 9.35/9.56 Clause #1404 (by clausification #[1400]): Or (Eq (cR cA cC) True) % 9.35/9.56 (Or (Eq (cR cA cB) True) (Or (Eq (cR cB cD) False) (Or (Eq (cR cA cB) True) (Eq (cR cA cC) True)))) % 9.35/9.56 Clause #1405 (by eliminate duplicate literals #[1404]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq (cR cB cD) False)) % 9.35/9.56 Clause #1408 (by superposition #[1405, 1257]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Eq False True)))) % 9.35/9.56 Clause #1411 (by clausification #[1408]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cB) True))) % 9.35/9.56 Clause #1412 (by eliminate duplicate literals #[1411]): Or (Eq (cR cA cC) True) (Eq (cR cA cB) True) % 9.35/9.56 Clause #1419 (by superposition #[1412, 1126]): Or (Eq (cR cA cB) True) % 9.35/9.56 (Or (Eq (cR cA cD) True) % 9.35/9.56 (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Or (Eq True False) (Eq (cR cA cF) False))))) % 9.35/9.56 Clause #1523 (by clausification #[1419]): Or (Eq (cR cA cB) True) % 9.35/9.56 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cE) True) (Eq (cR cA cF) False)))) % 9.35/9.56 Clause #1524 (by eliminate duplicate literals #[1523]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cC cE) True) (Eq (cR cA cF) False))) % 9.35/9.56 Clause #1526 (by superposition #[1524, 437]): Or (Eq (cR cA cB) True) % 9.35/9.56 (Or (Eq (cR cA cD) True) % 9.35/9.56 (Or (Eq (cR cC cE) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cB) True))))) % 9.35/9.56 Clause #1544 (by clausification #[1526]): Or (Eq (cR cA cB) True) % 9.35/9.56 (Or (Eq (cR cA cD) True) (Or (Eq (cR cC cE) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cB) True)))) % 9.35/9.56 Clause #1545 (by eliminate duplicate literals #[1544]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Eq (cR cC cE) True)) % 9.35/9.56 Clause #1551 (by superposition #[1545, 20]): ∀ (a : Iota), % 9.35/9.56 Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cE) False)))) % 9.35/9.56 Clause #1552 (by clausification #[1551]): ∀ (a : Iota), Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR a cC) False) (Eq (cR a cE) False))) % 9.35/9.56 Clause #1553 (by superposition #[1552, 1412]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) False) (Or (Eq False True) (Eq (cR cA cB) True)))) % 9.35/9.56 Clause #1554 (by clausification #[1553]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) False) (Eq (cR cA cB) True))) % 9.35/9.56 Clause #1555 (by eliminate duplicate literals #[1554]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cE) False)) % 9.35/9.56 Clause #1556 (by superposition #[1555, 516]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cB) True)))) % 9.35/9.56 Clause #1560 (by clausification #[1556]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cB) True))) % 9.35/9.56 Clause #1561 (by eliminate duplicate literals #[1560]): Or (Eq (cR cA cB) True) (Eq (cR cA cD) True) % 9.35/9.56 Clause #1563 (by superposition #[1561, 69]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Or (Eq True False) (Eq (cR cA cE) False)))) % 9.35/9.56 Clause #1564 (by superposition #[1561, 70]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Or (Eq True False) (Eq (cR cA cF) False)))) % 9.35/9.56 Clause #1578 (by clausification #[1564]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Eq (cR cA cF) False))) % 9.35/9.56 Clause #1579 (by superposition #[1578, 406]): Or (Eq (cR cA cB) True) % 9.35/9.56 (Or (Eq (cR cC cD) True) % 9.35/9.56 (Or (Eq (cR cC cF) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Eq False True))))) % 9.35/9.56 Clause #1583 (by clausification #[1563]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Eq (cR cA cE) False))) % 9.35/9.56 Clause #1633 (by clausification #[1579]): Or (Eq (cR cA cB) True) % 9.35/9.56 (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cE) True)))) % 9.44/9.59 Clause #1634 (by eliminate duplicate literals #[1633]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cF) True) (Eq (cR cA cE) True))) % 9.44/9.59 Clause #1644 (by superposition #[1634, 20]): ∀ (a : Iota), % 9.44/9.59 Or (Eq (cR cA cB) True) % 9.44/9.59 (Or (Eq (cR cC cD) True) % 9.44/9.59 (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cF) False))))) % 9.44/9.59 Clause #1645 (by clausification #[1644]): ∀ (a : Iota), % 9.44/9.59 Or (Eq (cR cA cB) True) % 9.44/9.59 (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cC) False) (Eq (cR a cF) False)))) % 9.44/9.59 Clause #1646 (by superposition #[1645, 1412]): Or (Eq (cR cA cB) True) % 9.44/9.59 (Or (Eq (cR cC cD) True) % 9.44/9.59 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) False) (Or (Eq False True) (Eq (cR cA cB) True))))) % 9.44/9.59 Clause #1647 (by clausification #[1646]): Or (Eq (cR cA cB) True) % 9.44/9.59 (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) False) (Eq (cR cA cB) True)))) % 9.44/9.59 Clause #1648 (by eliminate duplicate literals #[1647]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cF) False))) % 9.44/9.59 Clause #1649 (by superposition #[1648, 406]): Or (Eq (cR cA cB) True) % 9.44/9.59 (Or (Eq (cR cC cD) True) % 9.44/9.59 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Eq False True))))) % 9.44/9.59 Clause #1660 (by clausification #[1649]): Or (Eq (cR cA cB) True) % 9.44/9.59 (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cB) True) (Eq (cR cA cE) True)))) % 9.44/9.59 Clause #1661 (by eliminate duplicate literals #[1660]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cA cE) True)) % 9.44/9.59 Clause #1672 (by superposition #[1661, 20]): ∀ (a : Iota), % 9.44/9.59 Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cD) False)))) % 9.44/9.59 Clause #1673 (by clausification #[1672]): ∀ (a : Iota), Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cC) False) (Eq (cR a cD) False))) % 9.44/9.59 Clause #1674 (by superposition #[1673, 1412]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cD) False) (Or (Eq False True) (Eq (cR cA cB) True)))) % 9.44/9.59 Clause #1677 (by clausification #[1674]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cD) False) (Eq (cR cA cB) True))) % 9.44/9.59 Clause #1678 (by eliminate duplicate literals #[1677]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cD) False)) % 9.44/9.59 Clause #1679 (by superposition #[1678, 1561]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cB) True) (Eq False True))) % 9.44/9.59 Clause #1680 (by clausification #[1679]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cB) True)) % 9.44/9.59 Clause #1681 (by eliminate duplicate literals #[1680]): Or (Eq (cR cA cB) True) (Eq (cR cA cE) True) % 9.44/9.59 Clause #1683 (by superposition #[1681, 1583]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cC cE) True) (Eq True False)))) % 9.44/9.59 Clause #1690 (by clausification #[1683]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cC cE) True))) % 9.44/9.59 Clause #1691 (by eliminate duplicate literals #[1690]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cC cE) True)) % 9.44/9.59 Clause #1697 (by superposition #[1691, 20]): ∀ (a : Iota), % 9.44/9.59 Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cE) False)))) % 9.44/9.59 Clause #1698 (by clausification #[1697]): ∀ (a : Iota), Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR a cC) False) (Eq (cR a cE) False))) % 9.44/9.59 Clause #1699 (by superposition #[1698, 1412]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cE) False) (Or (Eq False True) (Eq (cR cA cB) True)))) % 9.44/9.59 Clause #1702 (by clausification #[1699]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cE) False) (Eq (cR cA cB) True))) % 9.44/9.59 Clause #1703 (by eliminate duplicate literals #[1702]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cA cE) False)) % 9.44/9.59 Clause #1705 (by superposition #[1703, 1681]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Or (Eq (cR cA cB) True) (Eq False True))) % 9.44/9.59 Clause #1706 (by clausification #[1705]): Or (Eq (cR cA cB) True) (Or (Eq (cR cC cD) True) (Eq (cR cA cB) True)) % 9.45/9.62 Clause #1707 (by eliminate duplicate literals #[1706]): Or (Eq (cR cA cB) True) (Eq (cR cC cD) True) % 9.45/9.62 Clause #1718 (by superposition #[1707, 20]): ∀ (a : Iota), Or (Eq (cR cA cB) True) (Or (Eq True False) (Or (Eq (cR a cC) False) (Eq (cR a cD) False))) % 9.45/9.62 Clause #1719 (by clausification #[1718]): ∀ (a : Iota), Or (Eq (cR cA cB) True) (Or (Eq (cR a cC) False) (Eq (cR a cD) False)) % 9.45/9.62 Clause #1720 (by superposition #[1719, 1412]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) False) (Or (Eq False True) (Eq (cR cA cB) True))) % 9.45/9.62 Clause #1721 (by clausification #[1720]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cD) False) (Eq (cR cA cB) True)) % 9.45/9.62 Clause #1722 (by eliminate duplicate literals #[1721]): Or (Eq (cR cA cB) True) (Eq (cR cA cD) False) % 9.45/9.62 Clause #1723 (by superposition #[1722, 1561]): Or (Eq (cR cA cB) True) (Or (Eq (cR cA cB) True) (Eq False True)) % 9.45/9.62 Clause #1724 (by clausification #[1723]): Or (Eq (cR cA cB) True) (Eq (cR cA cB) True) % 9.45/9.62 Clause #1725 (by eliminate duplicate literals #[1724]): Eq (cR cA cB) True % 9.45/9.62 Clause #1745 (by superposition #[1725, 156]): Or (Eq (cR cB cE) True) (Or (Eq (cR cB cD) True) (Or (Eq True False) (Eq (cR cA cF) False))) % 9.45/9.62 Clause #1748 (by superposition #[1725, 203]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Eq (cR cA cF) False))) % 9.45/9.62 Clause #1759 (by clausification #[1745]): Or (Eq (cR cB cE) True) (Or (Eq (cR cB cD) True) (Eq (cR cA cF) False)) % 9.45/9.62 Clause #1760 (by superposition #[1759, 451]): Or (Eq (cR cB cE) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cC) True)))) % 9.45/9.62 Clause #1763 (by clausification #[1748]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Eq (cR cA cF) False)) % 9.45/9.62 Clause #1764 (by superposition #[1763, 451]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cC) True)))) % 9.45/9.62 Clause #1791 (by clausification #[1764]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cC) True))) % 9.45/9.62 Clause #1796 (by superposition #[1791, 20]): ∀ (a : Iota), % 9.45/9.62 Or (Eq (cR cB cC) True) % 9.45/9.62 (Or (Eq (cR cA cD) True) % 9.45/9.62 (Or (Eq (cR cA cC) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cE) False))))) % 9.45/9.62 Clause #1844 (by clausification #[1760]): Or (Eq (cR cB cE) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cC) True))) % 9.45/9.62 Clause #1849 (by superposition #[1844, 20]): ∀ (a : Iota), % 9.45/9.62 Or (Eq (cR cB cD) True) % 9.45/9.62 (Or (Eq (cR cA cD) True) % 9.45/9.62 (Or (Eq (cR cA cC) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cE) False))))) % 9.45/9.62 Clause #1879 (by clausification #[1796]): ∀ (a : Iota), % 9.45/9.62 Or (Eq (cR cB cC) True) % 9.45/9.62 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR a cB) False) (Eq (cR a cE) False)))) % 9.45/9.62 Clause #1880 (by superposition #[1879, 1725]): Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) False) (Eq False True)))) % 9.45/9.62 Clause #1881 (by clausification #[1880]): Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cE) False))) % 9.45/9.62 Clause #1882 (by superposition #[1881, 554]): Or (Eq (cR cB cC) True) % 9.45/9.62 (Or (Eq (cR cA cD) True) % 9.45/9.62 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cC) True))))) % 9.45/9.62 Clause #1883 (by clausification #[1882]): Or (Eq (cR cB cC) True) % 9.45/9.62 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cC) True)))) % 9.45/9.62 Clause #1884 (by eliminate duplicate literals #[1883]): Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cC) True)) % 9.45/9.62 Clause #1888 (by superposition #[1884, 383]): Or (Eq (cR cA cD) True) % 9.45/9.62 (Or (Eq (cR cA cC) True) % 9.45/9.62 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Or (Eq True False) (Eq (cR cB cD) False))))) % 9.45/9.62 Clause #1898 (by clausification #[1888]): Or (Eq (cR cA cD) True) % 9.45/9.62 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Eq (cR cB cD) False)))) % 9.45/9.62 Clause #1899 (by eliminate duplicate literals #[1898]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Eq (cR cB cD) False)) % 9.45/9.62 Clause #1921 (by clausification #[1849]): ∀ (a : Iota), % 9.48/9.64 Or (Eq (cR cB cD) True) % 9.48/9.64 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR a cB) False) (Eq (cR a cE) False)))) % 9.48/9.64 Clause #1922 (by superposition #[1921, 1725]): Or (Eq (cR cB cD) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) False) (Eq False True)))) % 9.48/9.64 Clause #1923 (by clausification #[1922]): Or (Eq (cR cB cD) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cE) False))) % 9.48/9.64 Clause #1924 (by superposition #[1923, 554]): Or (Eq (cR cB cD) True) % 9.48/9.64 (Or (Eq (cR cA cD) True) % 9.48/9.64 (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Or (Eq False True) (Eq (cR cA cC) True))))) % 9.48/9.64 Clause #1925 (by clausification #[1924]): Or (Eq (cR cB cD) True) % 9.48/9.64 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cC) True)))) % 9.48/9.64 Clause #1926 (by eliminate duplicate literals #[1925]): Or (Eq (cR cB cD) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cC) True)) % 9.48/9.64 Clause #1927 (by superposition #[1926, 1899]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Eq True False)))) % 9.48/9.64 Clause #1939 (by clausification #[1927]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cC) True))) % 9.48/9.64 Clause #1940 (by eliminate duplicate literals #[1939]): Or (Eq (cR cA cD) True) (Eq (cR cA cC) True) % 9.48/9.64 Clause #1944 (by superposition #[1940, 112]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Eq (cR cA cF) False)))) % 9.48/9.64 Clause #1945 (by superposition #[1940, 113]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Eq (cR cA cE) False)))) % 9.48/9.64 Clause #1951 (by clausification #[1945]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Eq (cR cA cE) False))) % 9.48/9.64 Clause #1952 (by clausification #[1944]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Eq (cR cA cF) False))) % 9.48/9.64 Clause #1953 (by superposition #[1952, 471]): Or (Eq (cR cA cC) True) % 9.48/9.64 (Or (Eq (cR cB cD) True) % 9.48/9.64 (Or (Eq (cR cB cF) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Eq False True))))) % 9.48/9.64 Clause #1971 (by clausification #[1953]): Or (Eq (cR cA cC) True) % 9.48/9.64 (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cE) True)))) % 9.48/9.64 Clause #1972 (by eliminate duplicate literals #[1971]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cF) True) (Eq (cR cA cE) True))) % 9.48/9.64 Clause #1974 (by superposition #[1972, 20]): ∀ (a : Iota), % 9.48/9.64 Or (Eq (cR cA cC) True) % 9.48/9.64 (Or (Eq (cR cB cD) True) % 9.48/9.64 (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cF) False))))) % 9.48/9.64 Clause #1975 (by clausification #[1974]): ∀ (a : Iota), % 9.48/9.64 Or (Eq (cR cA cC) True) % 9.48/9.64 (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cB) False) (Eq (cR a cF) False)))) % 9.48/9.64 Clause #1976 (by superposition #[1975, 1725]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) False) (Eq False True)))) % 9.48/9.64 Clause #1980 (by clausification #[1976]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cF) False))) % 9.48/9.64 Clause #1981 (by superposition #[1980, 471]): Or (Eq (cR cA cC) True) % 9.48/9.64 (Or (Eq (cR cB cD) True) % 9.48/9.64 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Eq False True))))) % 9.48/9.64 Clause #1985 (by clausification #[1981]): Or (Eq (cR cA cC) True) % 9.48/9.64 (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cC) True) (Eq (cR cA cE) True)))) % 9.48/9.64 Clause #1986 (by eliminate duplicate literals #[1985]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Eq (cR cA cE) True)) % 9.48/9.64 Clause #1991 (by superposition #[1986, 20]): ∀ (a : Iota), % 9.48/9.64 Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cD) False)))) % 9.48/9.64 Clause #1992 (by clausification #[1991]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cB) False) (Eq (cR a cD) False))) % 9.48/9.64 Clause #1993 (by superposition #[1992, 1725]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cD) False) (Eq False True))) % 9.48/9.67 Clause #1994 (by clausification #[1993]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cD) False)) % 9.48/9.67 Clause #1995 (by superposition #[1994, 1940]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Or (Eq False True) (Eq (cR cA cC) True))) % 9.48/9.67 Clause #1998 (by clausification #[1995]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cC) True)) % 9.48/9.67 Clause #1999 (by eliminate duplicate literals #[1998]): Or (Eq (cR cA cC) True) (Eq (cR cA cE) True) % 9.48/9.67 Clause #2001 (by superposition #[1999, 1951]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cB cE) True) (Eq True False)))) % 9.48/9.67 Clause #2014 (by clausification #[2001]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cE) True))) % 9.48/9.67 Clause #2015 (by eliminate duplicate literals #[2014]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Eq (cR cB cE) True)) % 9.48/9.67 Clause #2020 (by superposition #[2015, 20]): ∀ (a : Iota), % 9.48/9.67 Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cE) False)))) % 9.48/9.67 Clause #2021 (by clausification #[2020]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR a cB) False) (Eq (cR a cE) False))) % 9.48/9.67 Clause #2022 (by superposition #[2021, 1725]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cE) False) (Eq False True))) % 9.48/9.67 Clause #2025 (by clausification #[2022]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Eq (cR cA cE) False)) % 9.48/9.67 Clause #2026 (by superposition #[2025, 1999]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Or (Eq (cR cA cC) True) (Eq False True))) % 9.48/9.67 Clause #2027 (by clausification #[2026]): Or (Eq (cR cA cC) True) (Or (Eq (cR cB cD) True) (Eq (cR cA cC) True)) % 9.48/9.67 Clause #2028 (by eliminate duplicate literals #[2027]): Or (Eq (cR cA cC) True) (Eq (cR cB cD) True) % 9.48/9.67 Clause #2033 (by superposition #[2028, 20]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cD) False))) % 9.48/9.67 Clause #2034 (by clausification #[2033]): ∀ (a : Iota), Or (Eq (cR cA cC) True) (Or (Eq (cR a cB) False) (Eq (cR a cD) False)) % 9.48/9.67 Clause #2035 (by superposition #[2034, 1725]): Or (Eq (cR cA cC) True) (Or (Eq (cR cA cD) False) (Eq False True)) % 9.48/9.67 Clause #2036 (by clausification #[2035]): Or (Eq (cR cA cC) True) (Eq (cR cA cD) False) % 9.48/9.67 Clause #2037 (by superposition #[2036, 1940]): Or (Eq (cR cA cC) True) (Or (Eq False True) (Eq (cR cA cC) True)) % 9.48/9.67 Clause #2038 (by clausification #[2037]): Or (Eq (cR cA cC) True) (Eq (cR cA cC) True) % 9.48/9.67 Clause #2039 (by eliminate duplicate literals #[2038]): Eq (cR cA cC) True % 9.48/9.67 Clause #2053 (by superposition #[2039, 151]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cF) True) (Or (Eq True False) (Eq (cR cA cF) False))) % 9.48/9.67 Clause #2054 (by superposition #[2039, 152]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Or (Eq True False) (Eq (cR cA cE) False))) % 9.48/9.67 Clause #2055 (by superposition #[2039, 153]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cD) True) (Or (Eq True False) (Eq (cR cA cD) False))) % 9.48/9.67 Clause #2072 (by clausification #[2055]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cD) True) (Eq (cR cA cD) False)) % 9.48/9.67 Clause #2077 (by clausification #[2054]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Eq (cR cA cE) False)) % 9.48/9.67 Clause #2080 (by clausification #[2053]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cF) True) (Eq (cR cA cF) False)) % 9.48/9.67 Clause #2081 (by superposition #[2080, 498]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq False True)))) % 9.48/9.67 Clause #2082 (by clausification #[2081]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cF) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cE) True))) % 9.48/9.67 Clause #2084 (by superposition #[2082, 20]): ∀ (a : Iota), % 9.48/9.67 Or (Eq (cR cB cC) True) % 9.48/9.67 (Or (Eq (cR cA cD) True) % 9.48/9.67 (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cF) False))))) % 9.48/9.67 Clause #2179 (by clausification #[2084]): ∀ (a : Iota), % 9.48/9.67 Or (Eq (cR cB cC) True) % 9.48/9.67 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cB) False) (Eq (cR a cF) False)))) % 9.48/9.69 Clause #2180 (by superposition #[2179, 1725]): Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cF) False) (Eq False True)))) % 9.48/9.69 Clause #2181 (by clausification #[2180]): Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cF) False))) % 9.48/9.69 Clause #2182 (by superposition #[2181, 498]): Or (Eq (cR cB cC) True) % 9.48/9.69 (Or (Eq (cR cA cD) True) % 9.48/9.69 (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq False True))))) % 9.48/9.69 Clause #2183 (by clausification #[2182]): Or (Eq (cR cB cC) True) % 9.48/9.69 (Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cE) True)))) % 9.48/9.69 Clause #2184 (by eliminate duplicate literals #[2183]): Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) True) (Eq (cR cA cE) True)) % 9.48/9.69 Clause #2191 (by superposition #[2184, 20]): ∀ (a : Iota), % 9.48/9.69 Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cC) False)))) % 9.48/9.69 Clause #2192 (by clausification #[2191]): ∀ (a : Iota), Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR a cB) False) (Eq (cR a cC) False))) % 9.48/9.69 Clause #2193 (by superposition #[2192, 1725]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Or (Eq (cR cA cC) False) (Eq False True))) % 9.48/9.69 Clause #2196 (by clausification #[2193]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq (cR cA cC) False)) % 9.48/9.69 Clause #2197 (by forward demodulation #[2196, 2039]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cE) True) (Eq True False)) % 9.48/9.69 Clause #2198 (by clausification #[2197]): Or (Eq (cR cA cD) True) (Eq (cR cA cE) True) % 9.48/9.69 Clause #2200 (by superposition #[2198, 2077]): Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Or (Eq (cR cB cE) True) (Eq True False))) % 9.48/9.69 Clause #2206 (by clausification #[2200]): Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Eq (cR cB cE) True)) % 9.48/9.69 Clause #2211 (by superposition #[2206, 20]): ∀ (a : Iota), % 9.48/9.69 Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cE) False)))) % 9.48/9.69 Clause #2221 (by clausification #[2211]): ∀ (a : Iota), Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Or (Eq (cR a cB) False) (Eq (cR a cE) False))) % 9.48/9.69 Clause #2222 (by superposition #[2221, 1725]): Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Or (Eq (cR cA cE) False) (Eq False True))) % 9.48/9.69 Clause #2223 (by clausification #[2222]): Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Eq (cR cA cE) False)) % 9.48/9.69 Clause #2224 (by superposition #[2223, 2198]): Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) True) (Eq False True))) % 9.48/9.69 Clause #2225 (by clausification #[2224]): Or (Eq (cR cA cD) True) (Or (Eq (cR cB cC) True) (Eq (cR cA cD) True)) % 9.48/9.69 Clause #2226 (by eliminate duplicate literals #[2225]): Or (Eq (cR cA cD) True) (Eq (cR cB cC) True) % 9.48/9.69 Clause #2232 (by superposition #[2226, 20]): ∀ (a : Iota), Or (Eq (cR cA cD) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cC) False))) % 9.48/9.69 Clause #2233 (by clausification #[2232]): ∀ (a : Iota), Or (Eq (cR cA cD) True) (Or (Eq (cR a cB) False) (Eq (cR a cC) False)) % 9.48/9.69 Clause #2234 (by superposition #[2233, 1725]): Or (Eq (cR cA cD) True) (Or (Eq (cR cA cC) False) (Eq False True)) % 9.48/9.69 Clause #2238 (by clausification #[2234]): Or (Eq (cR cA cD) True) (Eq (cR cA cC) False) % 9.48/9.69 Clause #2239 (by forward demodulation #[2238, 2039]): Or (Eq (cR cA cD) True) (Eq True False) % 9.48/9.69 Clause #2240 (by clausification #[2239]): Eq (cR cA cD) True % 9.48/9.69 Clause #2252 (by backward demodulation #[2240, 2072]): Or (Eq (cR cB cC) True) (Or (Eq (cR cB cD) True) (Eq True False)) % 9.48/9.69 Clause #2265 (by clausification #[2252]): Or (Eq (cR cB cC) True) (Eq (cR cB cD) True) % 9.48/9.69 Clause #2268 (by superposition #[2265, 20]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cD) False))) % 9.48/9.69 Clause #2270 (by clausification #[2268]): ∀ (a : Iota), Or (Eq (cR cB cC) True) (Or (Eq (cR a cB) False) (Eq (cR a cD) False)) % 9.48/9.69 Clause #2271 (by superposition #[2270, 1725]): Or (Eq (cR cB cC) True) (Or (Eq (cR cA cD) False) (Eq False True)) % 9.48/9.69 Clause #2275 (by clausification #[2271]): Or (Eq (cR cB cC) True) (Eq (cR cA cD) False) % 9.48/9.70 Clause #2276 (by forward demodulation #[2275, 2240]): Or (Eq (cR cB cC) True) (Eq True False) % 9.48/9.70 Clause #2277 (by clausification #[2276]): Eq (cR cB cC) True % 9.48/9.70 Clause #2299 (by superposition #[2277, 20]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (cR a cB) False) (Eq (cR a cC) False)) % 9.48/9.70 Clause #2300 (by clausification #[2299]): ∀ (a : Iota), Or (Eq (cR a cB) False) (Eq (cR a cC) False) % 9.48/9.70 Clause #2301 (by superposition #[2300, 1725]): Or (Eq (cR cA cC) False) (Eq False True) % 9.48/9.70 Clause #2302 (by clausification #[2301]): Eq (cR cA cC) False % 9.48/9.70 Clause #2303 (by superposition #[2302, 2039]): Eq False True % 9.48/9.70 Clause #2304 (by clausification #[2303]): False % 9.48/9.70 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------