%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRA014+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:48:50 PM UTC 2025 % Result : Theorem 25.93s 26.16s % Output : Proof 26.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : GRA014+1 : TPTP v9.2.0. Released v3.2.0. % 0.12/0.13 % Command : duper %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 16:13:08 EDT 2025 % 0.13/0.34 % CPUTime : % 25.93/26.16 SZS status Theorem for theBenchmark.p % 25.93/26.16 SZS output start Proof for theBenchmark.p % 25.93/26.16 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), And (And (red A B) (red B C)) (red A C) → goal) True % 25.93/26.16 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), And (And (green A B) (green B C)) (green A C) → goal) True % 25.93/26.16 Clause #2 (by assumption #[]): Eq (And (And (And (And (less_than n1 n2) (less_than n2 n3)) (less_than n3 n4)) (less_than n4 n5)) (less_than n5 n6)) % 25.93/26.16 True % 25.93/26.16 Clause #3 (by assumption #[]): Eq (∀ (A B C : Iota), And (less_than A B) (less_than B C) → less_than A C) True % 25.93/26.16 Clause #4 (by assumption #[]): Eq (∀ (A B : Iota), less_than A B → Or (red A B) (green A B)) True % 25.93/26.16 Clause #5 (by assumption #[]): Eq (Not goal) True % 25.93/26.16 Clause #6 (by clausification #[5]): Eq goal False % 25.93/26.16 Clause #7 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), And (And (green a B) (green B C)) (green a C) → goal) True % 25.93/26.16 Clause #8 (by clausification #[7]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), And (And (green a a_1) (green a_1 C)) (green a C) → goal) True % 25.93/26.16 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 : Iota), Eq (And (And (green a a_1) (green a_1 a_2)) (green a a_2) → goal) True % 25.93/26.16 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (And (green a a_1) (green a_1 a_2)) (green a a_2)) False) (Eq goal True) % 25.93/26.16 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 : Iota), Or (Eq goal True) (Or (Eq (And (green a a_1) (green a_1 a_2)) False) (Eq (green a a_2) False)) % 25.93/26.16 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 : Iota), % 25.93/26.16 Or (Eq goal True) (Or (Eq (green a a_1) False) (Or (Eq (green a a_2) False) (Eq (green a_2 a_1) False))) % 25.93/26.16 Clause #13 (by forward demodulation #[12, 6]): ∀ (a a_1 a_2 : Iota), % 25.93/26.16 Or (Eq False True) (Or (Eq (green a a_1) False) (Or (Eq (green a a_2) False) (Eq (green a_2 a_1) False))) % 25.93/26.16 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 : Iota), Or (Eq (green a a_1) False) (Or (Eq (green a a_2) False) (Eq (green a_2 a_1) False)) % 25.93/26.16 Clause #15 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), And (And (red a B) (red B C)) (red a C) → goal) True % 25.93/26.16 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), And (And (red a a_1) (red a_1 C)) (red a C) → goal) True % 25.93/26.16 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), Eq (And (And (red a a_1) (red a_1 a_2)) (red a a_2) → goal) True % 25.93/26.16 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (And (red a a_1) (red a_1 a_2)) (red a a_2)) False) (Eq goal True) % 25.93/26.16 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), Or (Eq goal True) (Or (Eq (And (red a a_1) (red a_1 a_2)) False) (Eq (red a a_2) False)) % 25.93/26.16 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 : Iota), Or (Eq goal True) (Or (Eq (red a a_1) False) (Or (Eq (red a a_2) False) (Eq (red a_2 a_1) False))) % 25.93/26.16 Clause #21 (by forward demodulation #[20, 6]): ∀ (a a_1 a_2 : Iota), % 25.93/26.16 Or (Eq False True) (Or (Eq (red a a_1) False) (Or (Eq (red a a_2) False) (Eq (red a_2 a_1) False))) % 25.93/26.16 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), Or (Eq (red a a_1) False) (Or (Eq (red a a_2) False) (Eq (red a_2 a_1) False)) % 25.93/26.16 Clause #23 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C : Iota), And (less_than a B) (less_than B C) → less_than a C) True % 25.93/26.16 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), And (less_than a a_1) (less_than a_1 C) → less_than a C) True % 25.93/26.16 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), Eq (And (less_than a a_1) (less_than a_1 a_2) → less_than a a_2) True % 25.93/26.16 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (less_than a a_1) (less_than a_1 a_2)) False) (Eq (less_than a a_2) True) % 25.93/26.16 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Or (Eq (less_than a a_1) True) (Or (Eq (less_than a a_2) False) (Eq (less_than a_2 a_1) False)) % 25.93/26.16 Clause #28 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B : Iota), less_than a B → Or (red a B) (green a B)) True % 25.93/26.16 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), Eq (less_than a a_1 → Or (red a a_1) (green a a_1)) True % 26.01/26.18 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), Or (Eq (less_than a a_1) False) (Eq (Or (red a a_1) (green a a_1)) True) % 26.01/26.18 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Or (Eq (less_than a a_1) False) (Or (Eq (red a a_1) True) (Eq (green a a_1) True)) % 26.01/26.18 Clause #32 (by clausification #[2]): Eq (less_than n5 n6) True % 26.01/26.18 Clause #33 (by clausification #[2]): Eq (And (And (And (less_than n1 n2) (less_than n2 n3)) (less_than n3 n4)) (less_than n4 n5)) True % 26.01/26.18 Clause #35 (by superposition #[32, 31]): Or (Eq True False) (Or (Eq (red n5 n6) True) (Eq (green n5 n6) True)) % 26.01/26.18 Clause #36 (by clausification #[35]): Or (Eq (red n5 n6) True) (Eq (green n5 n6) True) % 26.01/26.18 Clause #43 (by clausification #[33]): Eq (less_than n4 n5) True % 26.01/26.18 Clause #44 (by clausification #[33]): Eq (And (And (less_than n1 n2) (less_than n2 n3)) (less_than n3 n4)) True % 26.01/26.18 Clause #45 (by superposition #[43, 27]): ∀ (a : Iota), Or (Eq (less_than n4 a) True) (Or (Eq True False) (Eq (less_than n5 a) False)) % 26.01/26.18 Clause #46 (by superposition #[43, 31]): Or (Eq True False) (Or (Eq (red n4 n5) True) (Eq (green n4 n5) True)) % 26.01/26.18 Clause #47 (by clausification #[44]): Eq (less_than n3 n4) True % 26.01/26.18 Clause #48 (by clausification #[44]): Eq (And (less_than n1 n2) (less_than n2 n3)) True % 26.01/26.18 Clause #49 (by superposition #[47, 27]): ∀ (a : Iota), Or (Eq (less_than n3 a) True) (Or (Eq True False) (Eq (less_than n4 a) False)) % 26.01/26.18 Clause #50 (by superposition #[47, 31]): Or (Eq True False) (Or (Eq (red n3 n4) True) (Eq (green n3 n4) True)) % 26.01/26.18 Clause #51 (by clausification #[48]): Eq (less_than n2 n3) True % 26.01/26.18 Clause #52 (by clausification #[48]): Eq (less_than n1 n2) True % 26.01/26.18 Clause #53 (by superposition #[51, 27]): ∀ (a : Iota), Or (Eq (less_than n2 a) True) (Or (Eq True False) (Eq (less_than n3 a) False)) % 26.01/26.18 Clause #54 (by superposition #[51, 31]): Or (Eq True False) (Or (Eq (red n2 n3) True) (Eq (green n2 n3) True)) % 26.01/26.18 Clause #55 (by superposition #[52, 27]): ∀ (a : Iota), Or (Eq (less_than n1 a) True) (Or (Eq True False) (Eq (less_than n2 a) False)) % 26.01/26.18 Clause #56 (by superposition #[52, 31]): Or (Eq True False) (Or (Eq (red n1 n2) True) (Eq (green n1 n2) True)) % 26.01/26.18 Clause #57 (by clausification #[46]): Or (Eq (red n4 n5) True) (Eq (green n4 n5) True) % 26.01/26.18 Clause #59 (by clausification #[50]): Or (Eq (red n3 n4) True) (Eq (green n3 n4) True) % 26.01/26.18 Clause #61 (by clausification #[49]): ∀ (a : Iota), Or (Eq (less_than n3 a) True) (Eq (less_than n4 a) False) % 26.01/26.18 Clause #62 (by superposition #[61, 43]): Or (Eq (less_than n3 n5) True) (Eq False True) % 26.01/26.18 Clause #63 (by clausification #[45]): ∀ (a : Iota), Or (Eq (less_than n4 a) True) (Eq (less_than n5 a) False) % 26.01/26.18 Clause #64 (by superposition #[63, 32]): Or (Eq (less_than n4 n6) True) (Eq False True) % 26.01/26.18 Clause #65 (by clausification #[64]): Eq (less_than n4 n6) True % 26.01/26.18 Clause #66 (by superposition #[65, 61]): Or (Eq (less_than n3 n6) True) (Eq True False) % 26.01/26.18 Clause #68 (by superposition #[65, 31]): Or (Eq True False) (Or (Eq (red n4 n6) True) (Eq (green n4 n6) True)) % 26.01/26.18 Clause #69 (by clausification #[66]): Eq (less_than n3 n6) True % 26.01/26.18 Clause #71 (by superposition #[69, 31]): Or (Eq True False) (Or (Eq (red n3 n6) True) (Eq (green n3 n6) True)) % 26.01/26.18 Clause #72 (by clausification #[62]): Eq (less_than n3 n5) True % 26.01/26.18 Clause #74 (by superposition #[72, 31]): Or (Eq True False) (Or (Eq (red n3 n5) True) (Eq (green n3 n5) True)) % 26.01/26.18 Clause #75 (by clausification #[55]): ∀ (a : Iota), Or (Eq (less_than n1 a) True) (Eq (less_than n2 a) False) % 26.01/26.18 Clause #76 (by superposition #[75, 51]): Or (Eq (less_than n1 n3) True) (Eq False True) % 26.01/26.18 Clause #77 (by clausification #[76]): Eq (less_than n1 n3) True % 26.01/26.18 Clause #79 (by superposition #[77, 31]): Or (Eq True False) (Or (Eq (red n1 n3) True) (Eq (green n1 n3) True)) % 26.01/26.18 Clause #80 (by clausification #[53]): ∀ (a : Iota), Or (Eq (less_than n2 a) True) (Eq (less_than n3 a) False) % 26.01/26.18 Clause #81 (by superposition #[80, 47]): Or (Eq (less_than n2 n4) True) (Eq False True) % 26.01/26.18 Clause #82 (by superposition #[80, 69]): Or (Eq (less_than n2 n6) True) (Eq False True) % 26.01/26.18 Clause #83 (by superposition #[80, 72]): Or (Eq (less_than n2 n5) True) (Eq False True) % 26.01/26.18 Clause #84 (by clausification #[83]): Eq (less_than n2 n5) True % 26.03/26.21 Clause #85 (by superposition #[84, 75]): Or (Eq (less_than n1 n5) True) (Eq True False) % 26.03/26.21 Clause #87 (by superposition #[84, 31]): Or (Eq True False) (Or (Eq (red n2 n5) True) (Eq (green n2 n5) True)) % 26.03/26.21 Clause #88 (by clausification #[85]): Eq (less_than n1 n5) True % 26.03/26.21 Clause #90 (by superposition #[88, 31]): Or (Eq True False) (Or (Eq (red n1 n5) True) (Eq (green n1 n5) True)) % 26.03/26.21 Clause #91 (by clausification #[82]): Eq (less_than n2 n6) True % 26.03/26.21 Clause #92 (by superposition #[91, 75]): Or (Eq (less_than n1 n6) True) (Eq True False) % 26.03/26.21 Clause #94 (by superposition #[91, 31]): Or (Eq True False) (Or (Eq (red n2 n6) True) (Eq (green n2 n6) True)) % 26.03/26.21 Clause #95 (by clausification #[92]): Eq (less_than n1 n6) True % 26.03/26.21 Clause #97 (by superposition #[95, 31]): Or (Eq True False) (Or (Eq (red n1 n6) True) (Eq (green n1 n6) True)) % 26.03/26.21 Clause #98 (by clausification #[81]): Eq (less_than n2 n4) True % 26.03/26.21 Clause #99 (by superposition #[98, 75]): Or (Eq (less_than n1 n4) True) (Eq True False) % 26.03/26.21 Clause #101 (by superposition #[98, 31]): Or (Eq True False) (Or (Eq (red n2 n4) True) (Eq (green n2 n4) True)) % 26.03/26.21 Clause #102 (by clausification #[54]): Or (Eq (red n2 n3) True) (Eq (green n2 n3) True) % 26.03/26.21 Clause #104 (by clausification #[99]): Eq (less_than n1 n4) True % 26.03/26.21 Clause #106 (by superposition #[104, 31]): Or (Eq True False) (Or (Eq (red n1 n4) True) (Eq (green n1 n4) True)) % 26.03/26.21 Clause #107 (by clausification #[106]): Or (Eq (red n1 n4) True) (Eq (green n1 n4) True) % 26.03/26.21 Clause #108 (by superposition #[107, 14]): ∀ (a : Iota), Or (Eq (red n1 n4) True) (Or (Eq True False) (Or (Eq (green n1 a) False) (Eq (green a n4) False))) % 26.03/26.21 Clause #109 (by clausification #[79]): Or (Eq (red n1 n3) True) (Eq (green n1 n3) True) % 26.03/26.21 Clause #110 (by superposition #[109, 14]): ∀ (a : Iota), Or (Eq (red n1 n3) True) (Or (Eq True False) (Or (Eq (green n1 a) False) (Eq (green a n3) False))) % 26.03/26.21 Clause #115 (by clausification #[56]): Or (Eq (red n1 n2) True) (Eq (green n1 n2) True) % 26.03/26.21 Clause #118 (by clausification #[101]): Or (Eq (red n2 n4) True) (Eq (green n2 n4) True) % 26.03/26.21 Clause #119 (by superposition #[118, 14]): ∀ (a : Iota), Or (Eq (red n2 n4) True) (Or (Eq True False) (Or (Eq (green n2 a) False) (Eq (green a n4) False))) % 26.03/26.21 Clause #123 (by clausification #[87]): Or (Eq (red n2 n5) True) (Eq (green n2 n5) True) % 26.03/26.21 Clause #124 (by superposition #[123, 14]): ∀ (a : Iota), Or (Eq (red n2 n5) True) (Or (Eq True False) (Or (Eq (green n2 a) False) (Eq (green a n5) False))) % 26.03/26.21 Clause #127 (by clausification #[94]): Or (Eq (red n2 n6) True) (Eq (green n2 n6) True) % 26.03/26.21 Clause #128 (by superposition #[127, 14]): ∀ (a : Iota), Or (Eq (red n2 n6) True) (Or (Eq True False) (Or (Eq (green n2 a) False) (Eq (green a n6) False))) % 26.03/26.21 Clause #132 (by clausification #[97]): Or (Eq (red n1 n6) True) (Eq (green n1 n6) True) % 26.03/26.21 Clause #133 (by superposition #[132, 14]): ∀ (a : Iota), Or (Eq (red n1 n6) True) (Or (Eq True False) (Or (Eq (green n1 a) False) (Eq (green a n6) False))) % 26.03/26.21 Clause #134 (by clausification #[90]): Or (Eq (red n1 n5) True) (Eq (green n1 n5) True) % 26.03/26.21 Clause #135 (by superposition #[134, 14]): ∀ (a : Iota), Or (Eq (red n1 n5) True) (Or (Eq True False) (Or (Eq (green n1 a) False) (Eq (green a n5) False))) % 26.03/26.21 Clause #137 (by clausification #[68]): Or (Eq (red n4 n6) True) (Eq (green n4 n6) True) % 26.03/26.21 Clause #139 (by superposition #[137, 14]): ∀ (a : Iota), Or (Eq (red n4 n6) True) (Or (Eq True False) (Or (Eq (green n4 a) False) (Eq (green a n6) False))) % 26.03/26.21 Clause #142 (by clausification #[71]): Or (Eq (red n3 n6) True) (Eq (green n3 n6) True) % 26.03/26.21 Clause #144 (by superposition #[142, 14]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq True False) (Or (Eq (green n3 a) False) (Eq (green a n6) False))) % 26.03/26.21 Clause #145 (by clausification #[74]): Or (Eq (red n3 n5) True) (Eq (green n3 n5) True) % 26.03/26.21 Clause #147 (by superposition #[145, 14]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq True False) (Or (Eq (green n3 a) False) (Eq (green a n5) False))) % 26.03/26.21 Clause #150 (by clausification #[108]): ∀ (a : Iota), Or (Eq (red n1 n4) True) (Or (Eq (green n1 a) False) (Eq (green a n4) False)) % 26.03/26.21 Clause #152 (by superposition #[150, 109]): Or (Eq (red n1 n4) True) (Or (Eq (green n3 n4) False) (Or (Eq (red n1 n3) True) (Eq False True))) % 26.05/26.23 Clause #153 (by superposition #[150, 115]): Or (Eq (red n1 n4) True) (Or (Eq (green n2 n4) False) (Or (Eq (red n1 n2) True) (Eq False True))) % 26.05/26.23 Clause #167 (by clausification #[110]): ∀ (a : Iota), Or (Eq (red n1 n3) True) (Or (Eq (green n1 a) False) (Eq (green a n3) False)) % 26.05/26.23 Clause #170 (by superposition #[167, 115]): Or (Eq (red n1 n3) True) (Or (Eq (green n2 n3) False) (Or (Eq (red n1 n2) True) (Eq False True))) % 26.05/26.23 Clause #175 (by clausification #[170]): Or (Eq (red n1 n3) True) (Or (Eq (green n2 n3) False) (Eq (red n1 n2) True)) % 26.05/26.23 Clause #176 (by superposition #[175, 102]): Or (Eq (red n1 n3) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n3) True) (Eq False True))) % 26.05/26.23 Clause #177 (by clausification #[176]): Or (Eq (red n1 n3) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n3) True)) % 26.05/26.23 Clause #193 (by clausification #[119]): ∀ (a : Iota), Or (Eq (red n2 n4) True) (Or (Eq (green n2 a) False) (Eq (green a n4) False)) % 26.05/26.23 Clause #194 (by superposition #[193, 102]): Or (Eq (red n2 n4) True) (Or (Eq (green n3 n4) False) (Or (Eq (red n2 n3) True) (Eq False True))) % 26.05/26.23 Clause #202 (by clausification #[194]): Or (Eq (red n2 n4) True) (Or (Eq (green n3 n4) False) (Eq (red n2 n3) True)) % 26.05/26.23 Clause #203 (by superposition #[202, 59]): Or (Eq (red n2 n4) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n3 n4) True) (Eq False True))) % 26.05/26.23 Clause #204 (by clausification #[203]): Or (Eq (red n2 n4) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True)) % 26.05/26.23 Clause #208 (by clausification #[139]): ∀ (a : Iota), Or (Eq (red n4 n6) True) (Or (Eq (green n4 a) False) (Eq (green a n6) False)) % 26.05/26.23 Clause #217 (by clausification #[153]): Or (Eq (red n1 n4) True) (Or (Eq (green n2 n4) False) (Eq (red n1 n2) True)) % 26.05/26.23 Clause #218 (by superposition #[217, 118]): Or (Eq (red n1 n4) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n4) True) (Eq False True))) % 26.05/26.23 Clause #219 (by clausification #[124]): ∀ (a : Iota), Or (Eq (red n2 n5) True) (Or (Eq (green n2 a) False) (Eq (green a n5) False)) % 26.05/26.23 Clause #220 (by superposition #[219, 102]): Or (Eq (red n2 n5) True) (Or (Eq (green n3 n5) False) (Or (Eq (red n2 n3) True) (Eq False True))) % 26.05/26.23 Clause #221 (by superposition #[219, 118]): Or (Eq (red n2 n5) True) (Or (Eq (green n4 n5) False) (Or (Eq (red n2 n4) True) (Eq False True))) % 26.05/26.23 Clause #227 (by clausification #[221]): Or (Eq (red n2 n5) True) (Or (Eq (green n4 n5) False) (Eq (red n2 n4) True)) % 26.05/26.23 Clause #228 (by superposition #[227, 57]): Or (Eq (red n2 n5) True) (Or (Eq (red n2 n4) True) (Or (Eq (red n4 n5) True) (Eq False True))) % 26.05/26.23 Clause #229 (by clausification #[228]): Or (Eq (red n2 n5) True) (Or (Eq (red n2 n4) True) (Eq (red n4 n5) True)) % 26.05/26.23 Clause #231 (by clausification #[220]): Or (Eq (red n2 n5) True) (Or (Eq (green n3 n5) False) (Eq (red n2 n3) True)) % 26.05/26.23 Clause #232 (by superposition #[231, 145]): Or (Eq (red n2 n5) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n3 n5) True) (Eq False True))) % 26.05/26.23 Clause #233 (by clausification #[128]): ∀ (a : Iota), Or (Eq (red n2 n6) True) (Or (Eq (green n2 a) False) (Eq (green a n6) False)) % 26.05/26.23 Clause #234 (by superposition #[233, 102]): Or (Eq (red n2 n6) True) (Or (Eq (green n3 n6) False) (Or (Eq (red n2 n3) True) (Eq False True))) % 26.05/26.23 Clause #235 (by superposition #[233, 118]): Or (Eq (red n2 n6) True) (Or (Eq (green n4 n6) False) (Or (Eq (red n2 n4) True) (Eq False True))) % 26.05/26.23 Clause #236 (by superposition #[233, 123]): Or (Eq (red n2 n6) True) (Or (Eq (green n5 n6) False) (Or (Eq (red n2 n5) True) (Eq False True))) % 26.05/26.23 Clause #240 (by clausification #[236]): Or (Eq (red n2 n6) True) (Or (Eq (green n5 n6) False) (Eq (red n2 n5) True)) % 26.05/26.23 Clause #241 (by superposition #[240, 36]): Or (Eq (red n2 n6) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n5 n6) True) (Eq False True))) % 26.05/26.23 Clause #242 (by clausification #[241]): Or (Eq (red n2 n6) True) (Or (Eq (red n2 n5) True) (Eq (red n5 n6) True)) % 26.05/26.23 Clause #244 (by clausification #[218]): Or (Eq (red n1 n4) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n4) True)) % 26.05/26.23 Clause #245 (by superposition #[244, 22]): ∀ (a : Iota), % 26.05/26.23 Or (Eq (red n1 n2) True) % 26.05/26.23 (Or (Eq (red n2 n4) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n4) False)))) % 26.05/26.26 Clause #246 (by clausification #[234]): Or (Eq (red n2 n6) True) (Or (Eq (green n3 n6) False) (Eq (red n2 n3) True)) % 26.05/26.26 Clause #247 (by superposition #[246, 142]): Or (Eq (red n2 n6) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n3 n6) True) (Eq False True))) % 26.05/26.26 Clause #250 (by clausification #[247]): Or (Eq (red n2 n6) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n6) True)) % 26.05/26.26 Clause #251 (by superposition #[250, 22]): ∀ (a : Iota), % 26.05/26.26 Or (Eq (red n2 n3) True) % 26.05/26.26 (Or (Eq (red n3 n6) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n6) False)))) % 26.05/26.26 Clause #252 (by clausification #[232]): Or (Eq (red n2 n5) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n5) True)) % 26.05/26.26 Clause #253 (by superposition #[252, 22]): ∀ (a : Iota), % 26.05/26.26 Or (Eq (red n2 n3) True) % 26.05/26.26 (Or (Eq (red n3 n5) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n5) False)))) % 26.05/26.26 Clause #254 (by clausification #[235]): Or (Eq (red n2 n6) True) (Or (Eq (green n4 n6) False) (Eq (red n2 n4) True)) % 26.05/26.26 Clause #255 (by superposition #[254, 137]): Or (Eq (red n2 n6) True) (Or (Eq (red n2 n4) True) (Or (Eq (red n4 n6) True) (Eq False True))) % 26.05/26.26 Clause #256 (by clausification #[255]): Or (Eq (red n2 n6) True) (Or (Eq (red n2 n4) True) (Eq (red n4 n6) True)) % 26.05/26.26 Clause #258 (by clausification #[152]): Or (Eq (red n1 n4) True) (Or (Eq (green n3 n4) False) (Eq (red n1 n3) True)) % 26.05/26.26 Clause #259 (by superposition #[258, 59]): Or (Eq (red n1 n4) True) (Or (Eq (red n1 n3) True) (Or (Eq (red n3 n4) True) (Eq False True))) % 26.05/26.26 Clause #260 (by clausification #[133]): ∀ (a : Iota), Or (Eq (red n1 n6) True) (Or (Eq (green n1 a) False) (Eq (green a n6) False)) % 26.05/26.26 Clause #261 (by superposition #[260, 107]): Or (Eq (red n1 n6) True) (Or (Eq (green n4 n6) False) (Or (Eq (red n1 n4) True) (Eq False True))) % 26.05/26.26 Clause #262 (by superposition #[260, 109]): Or (Eq (red n1 n6) True) (Or (Eq (green n3 n6) False) (Or (Eq (red n1 n3) True) (Eq False True))) % 26.05/26.26 Clause #263 (by superposition #[260, 115]): Or (Eq (red n1 n6) True) (Or (Eq (green n2 n6) False) (Or (Eq (red n1 n2) True) (Eq False True))) % 26.05/26.26 Clause #265 (by superposition #[260, 134]): Or (Eq (red n1 n6) True) (Or (Eq (green n5 n6) False) (Or (Eq (red n1 n5) True) (Eq False True))) % 26.05/26.26 Clause #266 (by clausification #[265]): Or (Eq (red n1 n6) True) (Or (Eq (green n5 n6) False) (Eq (red n1 n5) True)) % 26.05/26.26 Clause #267 (by superposition #[266, 36]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n5) True) (Or (Eq (red n5 n6) True) (Eq False True))) % 26.05/26.26 Clause #268 (by clausification #[267]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n5) True) (Eq (red n5 n6) True)) % 26.05/26.26 Clause #269 (by superposition #[268, 22]): ∀ (a : Iota), % 26.05/26.26 Or (Eq (red n1 n5) True) % 26.05/26.26 (Or (Eq (red n5 n6) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n6) False)))) % 26.05/26.26 Clause #272 (by clausification #[263]): Or (Eq (red n1 n6) True) (Or (Eq (green n2 n6) False) (Eq (red n1 n2) True)) % 26.05/26.26 Clause #273 (by superposition #[272, 127]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n6) True) (Eq False True))) % 26.05/26.26 Clause #274 (by clausification #[273]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n6) True)) % 26.05/26.26 Clause #275 (by superposition #[274, 22]): ∀ (a : Iota), % 26.05/26.26 Or (Eq (red n1 n2) True) % 26.05/26.26 (Or (Eq (red n2 n6) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n6) False)))) % 26.05/26.26 Clause #276 (by clausification #[135]): ∀ (a : Iota), Or (Eq (red n1 n5) True) (Or (Eq (green n1 a) False) (Eq (green a n5) False)) % 26.05/26.26 Clause #277 (by superposition #[276, 107]): Or (Eq (red n1 n5) True) (Or (Eq (green n4 n5) False) (Or (Eq (red n1 n4) True) (Eq False True))) % 26.05/26.26 Clause #278 (by superposition #[276, 109]): Or (Eq (red n1 n5) True) (Or (Eq (green n3 n5) False) (Or (Eq (red n1 n3) True) (Eq False True))) % 26.05/26.26 Clause #279 (by superposition #[276, 115]): Or (Eq (red n1 n5) True) (Or (Eq (green n2 n5) False) (Or (Eq (red n1 n2) True) (Eq False True))) % 26.05/26.26 Clause #285 (by clausification #[279]): Or (Eq (red n1 n5) True) (Or (Eq (green n2 n5) False) (Eq (red n1 n2) True)) % 26.05/26.26 Clause #286 (by superposition #[285, 123]): Or (Eq (red n1 n5) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n5) True) (Eq False True))) % 26.05/26.28 Clause #287 (by clausification #[286]): Or (Eq (red n1 n5) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n5) True)) % 26.05/26.28 Clause #288 (by superposition #[287, 22]): ∀ (a : Iota), % 26.05/26.28 Or (Eq (red n1 n2) True) % 26.05/26.28 (Or (Eq (red n2 n5) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n5) False)))) % 26.05/26.28 Clause #289 (by clausification #[262]): Or (Eq (red n1 n6) True) (Or (Eq (green n3 n6) False) (Eq (red n1 n3) True)) % 26.05/26.28 Clause #290 (by superposition #[289, 142]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Eq False True))) % 26.05/26.28 Clause #292 (by clausification #[290]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n3) True) (Eq (red n3 n6) True)) % 26.05/26.28 Clause #293 (by superposition #[292, 22]): ∀ (a : Iota), % 26.05/26.28 Or (Eq (red n1 n3) True) % 26.05/26.28 (Or (Eq (red n3 n6) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n6) False)))) % 26.05/26.28 Clause #294 (by clausification #[277]): Or (Eq (red n1 n5) True) (Or (Eq (green n4 n5) False) (Eq (red n1 n4) True)) % 26.05/26.28 Clause #295 (by superposition #[294, 57]): Or (Eq (red n1 n5) True) (Or (Eq (red n1 n4) True) (Or (Eq (red n4 n5) True) (Eq False True))) % 26.05/26.28 Clause #296 (by clausification #[295]): Or (Eq (red n1 n5) True) (Or (Eq (red n1 n4) True) (Eq (red n4 n5) True)) % 26.05/26.28 Clause #297 (by superposition #[296, 22]): ∀ (a : Iota), % 26.05/26.28 Or (Eq (red n1 n5) True) % 26.05/26.28 (Or (Eq (red n4 n5) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n4) False)))) % 26.05/26.28 Clause #298 (by clausification #[278]): Or (Eq (red n1 n5) True) (Or (Eq (green n3 n5) False) (Eq (red n1 n3) True)) % 26.05/26.28 Clause #299 (by superposition #[298, 145]): Or (Eq (red n1 n5) True) (Or (Eq (red n1 n3) True) (Or (Eq (red n3 n5) True) (Eq False True))) % 26.05/26.28 Clause #300 (by clausification #[299]): Or (Eq (red n1 n5) True) (Or (Eq (red n1 n3) True) (Eq (red n3 n5) True)) % 26.05/26.28 Clause #301 (by superposition #[300, 22]): ∀ (a : Iota), % 26.05/26.28 Or (Eq (red n1 n3) True) % 26.05/26.28 (Or (Eq (red n3 n5) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n5) False)))) % 26.05/26.28 Clause #305 (by clausification #[259]): Or (Eq (red n1 n4) True) (Or (Eq (red n1 n3) True) (Eq (red n3 n4) True)) % 26.05/26.28 Clause #306 (by superposition #[305, 22]): ∀ (a : Iota), % 26.05/26.28 Or (Eq (red n1 n3) True) % 26.05/26.28 (Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n4) False)))) % 26.05/26.28 Clause #307 (by clausification #[261]): Or (Eq (red n1 n6) True) (Or (Eq (green n4 n6) False) (Eq (red n1 n4) True)) % 26.05/26.28 Clause #308 (by superposition #[307, 137]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n4) True) (Or (Eq (red n4 n6) True) (Eq False True))) % 26.05/26.28 Clause #309 (by clausification #[308]): Or (Eq (red n1 n6) True) (Or (Eq (red n1 n4) True) (Eq (red n4 n6) True)) % 26.05/26.28 Clause #310 (by superposition #[309, 22]): ∀ (a : Iota), % 26.05/26.28 Or (Eq (red n1 n4) True) % 26.05/26.28 (Or (Eq (red n4 n6) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n6) False)))) % 26.05/26.28 Clause #311 (by clausification #[147]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq (green n3 a) False) (Eq (green a n5) False)) % 26.05/26.28 Clause #312 (by superposition #[311, 59]): Or (Eq (red n3 n5) True) (Or (Eq (green n4 n5) False) (Or (Eq (red n3 n4) True) (Eq False True))) % 26.05/26.28 Clause #315 (by clausification #[144]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq (green n3 a) False) (Eq (green a n6) False)) % 26.05/26.28 Clause #316 (by superposition #[315, 59]): Or (Eq (red n3 n6) True) (Or (Eq (green n4 n6) False) (Or (Eq (red n3 n4) True) (Eq False True))) % 26.05/26.28 Clause #318 (by superposition #[315, 145]): Or (Eq (red n3 n6) True) (Or (Eq (green n5 n6) False) (Or (Eq (red n3 n5) True) (Eq False True))) % 26.05/26.28 Clause #319 (by clausification #[318]): Or (Eq (red n3 n6) True) (Or (Eq (green n5 n6) False) (Eq (red n3 n5) True)) % 26.05/26.28 Clause #320 (by superposition #[319, 36]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n5 n6) True) (Eq False True))) % 26.05/26.28 Clause #321 (by clausification #[320]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Eq (red n5 n6) True)) % 26.05/26.28 Clause #325 (by clausification #[316]): Or (Eq (red n3 n6) True) (Or (Eq (green n4 n6) False) (Eq (red n3 n4) True)) % 26.14/26.31 Clause #326 (by superposition #[325, 137]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n4 n6) True) (Eq False True))) % 26.14/26.31 Clause #327 (by clausification #[326]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq (red n4 n6) True)) % 26.14/26.31 Clause #328 (by superposition #[327, 22]): ∀ (a : Iota), % 26.14/26.31 Or (Eq (red n3 n6) True) % 26.14/26.31 (Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n4 a) False) (Eq (red a n6) False)))) % 26.14/26.31 Clause #333 (by clausification #[312]): Or (Eq (red n3 n5) True) (Or (Eq (green n4 n5) False) (Eq (red n3 n4) True)) % 26.14/26.31 Clause #334 (by superposition #[333, 57]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n4 n5) True) (Eq False True))) % 26.14/26.31 Clause #335 (by clausification #[334]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Eq (red n4 n5) True)) % 26.14/26.31 Clause #354 (by clausification #[269]): ∀ (a : Iota), Or (Eq (red n1 n5) True) (Or (Eq (red n5 n6) True) (Or (Eq (red n1 a) False) (Eq (red a n6) False))) % 26.14/26.31 Clause #365 (by clausification #[297]): ∀ (a : Iota), Or (Eq (red n1 n5) True) (Or (Eq (red n4 n5) True) (Or (Eq (red n1 a) False) (Eq (red a n4) False))) % 26.14/26.31 Clause #376 (by clausification #[306]): ∀ (a : Iota), Or (Eq (red n1 n3) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n1 a) False) (Eq (red a n4) False))) % 26.14/26.31 Clause #377 (by superposition #[376, 177]): Or (Eq (red n1 n3) True) % 26.14/26.31 (Or (Eq (red n3 n4) True) % 26.14/26.31 (Or (Eq (red n2 n4) False) (Or (Eq (red n1 n3) True) (Or (Eq False True) (Eq (red n2 n3) True))))) % 26.14/26.31 Clause #399 (by clausification #[275]): ∀ (a : Iota), Or (Eq (red n1 n2) True) (Or (Eq (red n2 n6) True) (Or (Eq (red n1 a) False) (Eq (red a n6) False))) % 26.14/26.31 Clause #404 (by superposition #[399, 287]): Or (Eq (red n1 n2) True) % 26.14/26.31 (Or (Eq (red n2 n6) True) % 26.14/26.31 (Or (Eq (red n5 n6) False) (Or (Eq False True) (Or (Eq (red n1 n2) True) (Eq (red n2 n5) True))))) % 26.14/26.31 Clause #410 (by clausification #[301]): ∀ (a : Iota), Or (Eq (red n1 n3) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n1 a) False) (Eq (red a n5) False))) % 26.14/26.31 Clause #411 (by superposition #[410, 177]): Or (Eq (red n1 n3) True) % 26.14/26.31 (Or (Eq (red n3 n5) True) % 26.14/26.31 (Or (Eq (red n2 n5) False) (Or (Eq (red n1 n3) True) (Or (Eq False True) (Eq (red n2 n3) True))))) % 26.14/26.31 Clause #419 (by superposition #[410, 305]): Or (Eq (red n1 n3) True) % 26.14/26.31 (Or (Eq (red n3 n5) True) % 26.14/26.31 (Or (Eq (red n4 n5) False) (Or (Eq False True) (Or (Eq (red n1 n3) True) (Eq (red n3 n4) True))))) % 26.14/26.31 Clause #436 (by clausification #[288]): ∀ (a : Iota), Or (Eq (red n1 n2) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n1 a) False) (Eq (red a n5) False))) % 26.14/26.31 Clause #438 (by superposition #[436, 244]): Or (Eq (red n1 n2) True) % 26.14/26.31 (Or (Eq (red n2 n5) True) % 26.14/26.31 (Or (Eq (red n4 n5) False) (Or (Eq False True) (Or (Eq (red n1 n2) True) (Eq (red n2 n4) True))))) % 26.14/26.31 Clause #447 (by clausification #[293]): ∀ (a : Iota), Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n1 a) False) (Eq (red a n6) False))) % 26.14/26.31 Clause #448 (by superposition #[447, 177]): Or (Eq (red n1 n3) True) % 26.14/26.31 (Or (Eq (red n3 n6) True) % 26.14/26.31 (Or (Eq (red n2 n6) False) (Or (Eq (red n1 n3) True) (Or (Eq False True) (Eq (red n2 n3) True))))) % 26.14/26.31 Clause #455 (by superposition #[447, 300]): Or (Eq (red n1 n3) True) % 26.14/26.31 (Or (Eq (red n3 n6) True) % 26.14/26.31 (Or (Eq (red n5 n6) False) (Or (Eq False True) (Or (Eq (red n1 n3) True) (Eq (red n3 n5) True))))) % 26.14/26.31 Clause #456 (by superposition #[447, 305]): Or (Eq (red n1 n3) True) % 26.14/26.31 (Or (Eq (red n3 n6) True) % 26.14/26.31 (Or (Eq (red n4 n6) False) (Or (Eq False True) (Or (Eq (red n1 n3) True) (Eq (red n3 n4) True))))) % 26.14/26.31 Clause #458 (by clausification #[310]): ∀ (a : Iota), Or (Eq (red n1 n4) True) (Or (Eq (red n4 n6) True) (Or (Eq (red n1 a) False) (Eq (red a n6) False))) % 26.14/26.31 Clause #469 (by clausification #[245]): ∀ (a : Iota), Or (Eq (red n1 n2) True) (Or (Eq (red n2 n4) True) (Or (Eq (red n1 a) False) (Eq (red a n4) False))) % 26.14/26.31 Clause #483 (by clausification #[251]): ∀ (a : Iota), Or (Eq (red n2 n3) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n2 a) False) (Eq (red a n6) False))) % 26.14/26.31 Clause #484 (by superposition #[483, 204]): Or (Eq (red n2 n3) True) % 26.14/26.31 (Or (Eq (red n3 n6) True) % 26.14/26.34 (Or (Eq (red n4 n6) False) (Or (Eq False True) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True))))) % 26.14/26.34 Clause #486 (by superposition #[483, 252]): Or (Eq (red n2 n3) True) % 26.14/26.34 (Or (Eq (red n3 n6) True) % 26.14/26.34 (Or (Eq (red n5 n6) False) (Or (Eq False True) (Or (Eq (red n2 n3) True) (Eq (red n3 n5) True))))) % 26.14/26.34 Clause #487 (by clausification #[328]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n4 a) False) (Eq (red a n6) False))) % 26.14/26.34 Clause #492 (by superposition #[487, 335]): Or (Eq (red n3 n6) True) % 26.14/26.34 (Or (Eq (red n3 n4) True) % 26.14/26.34 (Or (Eq (red n5 n6) False) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Eq False True))))) % 26.14/26.34 Clause #493 (by clausification #[253]): ∀ (a : Iota), Or (Eq (red n2 n3) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n2 a) False) (Eq (red a n5) False))) % 26.14/26.34 Clause #494 (by superposition #[493, 204]): Or (Eq (red n2 n3) True) % 26.14/26.34 (Or (Eq (red n3 n5) True) % 26.14/26.34 (Or (Eq (red n4 n5) False) (Or (Eq False True) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True))))) % 26.14/26.34 Clause #499 (by clausification #[494]): Or (Eq (red n2 n3) True) % 26.14/26.34 (Or (Eq (red n3 n5) True) (Or (Eq (red n4 n5) False) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True)))) % 26.14/26.34 Clause #500 (by eliminate duplicate literals #[499]): Or (Eq (red n2 n3) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n4 n5) False) (Eq (red n3 n4) True))) % 26.14/26.34 Clause #502 (by superposition #[500, 335]): Or (Eq (red n2 n3) True) % 26.14/26.34 (Or (Eq (red n3 n5) True) % 26.14/26.34 (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Eq False True))))) % 26.14/26.34 Clause #503 (by clausification #[502]): Or (Eq (red n2 n3) True) % 26.14/26.34 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True)))) % 26.14/26.34 Clause #504 (by eliminate duplicate literals #[503]): Or (Eq (red n2 n3) True) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True)) % 26.14/26.34 Clause #555 (by clausification #[377]): Or (Eq (red n1 n3) True) % 26.14/26.34 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n4) False) (Or (Eq (red n1 n3) True) (Eq (red n2 n3) True)))) % 26.14/26.34 Clause #556 (by eliminate duplicate literals #[555]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n4) False) (Eq (red n2 n3) True))) % 26.14/26.34 Clause #557 (by superposition #[556, 204]): Or (Eq (red n1 n3) True) % 26.14/26.34 (Or (Eq (red n3 n4) True) % 26.14/26.34 (Or (Eq (red n2 n3) True) (Or (Eq False True) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True))))) % 26.14/26.34 Clause #558 (by clausification #[557]): Or (Eq (red n1 n3) True) % 26.14/26.34 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True)))) % 26.14/26.34 Clause #559 (by eliminate duplicate literals #[558]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n4) True) (Eq (red n2 n3) True)) % 26.14/26.34 Clause #560 (by superposition #[559, 354]): Or (Eq (red n3 n4) True) % 26.14/26.34 (Or (Eq (red n2 n3) True) % 26.14/26.34 (Or (Eq (red n1 n5) True) (Or (Eq (red n5 n6) True) (Or (Eq True False) (Eq (red n3 n6) False))))) % 26.14/26.34 Clause #704 (by clausification #[411]): Or (Eq (red n1 n3) True) % 26.14/26.34 (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n5) False) (Or (Eq (red n1 n3) True) (Eq (red n2 n3) True)))) % 26.14/26.34 Clause #705 (by eliminate duplicate literals #[704]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n5) False) (Eq (red n2 n3) True))) % 26.14/26.34 Clause #706 (by superposition #[705, 252]): Or (Eq (red n1 n3) True) % 26.14/26.34 (Or (Eq (red n3 n5) True) % 26.14/26.34 (Or (Eq (red n2 n3) True) (Or (Eq False True) (Or (Eq (red n2 n3) True) (Eq (red n3 n5) True))))) % 26.14/26.34 Clause #707 (by clausification #[706]): Or (Eq (red n1 n3) True) % 26.14/26.34 (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n5) True)))) % 26.14/26.34 Clause #708 (by eliminate duplicate literals #[707]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n5) True) (Eq (red n2 n3) True)) % 26.14/26.34 Clause #713 (by superposition #[708, 458]): Or (Eq (red n3 n5) True) % 26.14/26.34 (Or (Eq (red n2 n3) True) % 26.14/26.34 (Or (Eq (red n1 n4) True) (Or (Eq (red n4 n6) True) (Or (Eq True False) (Eq (red n3 n6) False))))) % 26.14/26.34 Clause #745 (by clausification #[713]): Or (Eq (red n3 n5) True) % 26.14/26.34 (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n4) True) (Or (Eq (red n4 n6) True) (Eq (red n3 n6) False)))) % 26.14/26.34 Clause #784 (by clausification #[419]): Or (Eq (red n1 n3) True) % 26.14/26.36 (Or (Eq (red n3 n5) True) (Or (Eq (red n4 n5) False) (Or (Eq (red n1 n3) True) (Eq (red n3 n4) True)))) % 26.14/26.36 Clause #785 (by eliminate duplicate literals #[784]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n4 n5) False) (Eq (red n3 n4) True))) % 26.14/26.36 Clause #787 (by superposition #[785, 335]): Or (Eq (red n1 n3) True) % 26.14/26.36 (Or (Eq (red n3 n5) True) % 26.14/26.36 (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Eq False True))))) % 26.14/26.36 Clause #788 (by clausification #[787]): Or (Eq (red n1 n3) True) % 26.14/26.36 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True)))) % 26.14/26.36 Clause #789 (by eliminate duplicate literals #[788]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True)) % 26.14/26.36 Clause #792 (by superposition #[789, 399]): Or (Eq (red n3 n5) True) % 26.14/26.36 (Or (Eq (red n3 n4) True) % 26.14/26.36 (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n6) True) (Or (Eq True False) (Eq (red n3 n6) False))))) % 26.14/26.36 Clause #799 (by superposition #[789, 22]): ∀ (a : Iota), % 26.14/26.36 Or (Eq (red n3 n5) True) % 26.14/26.36 (Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n3) False)))) % 26.14/26.36 Clause #802 (by clausification #[799]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n1 a) False) (Eq (red a n3) False))) % 26.14/26.36 Clause #832 (by clausification #[792]): Or (Eq (red n3 n5) True) % 26.14/26.36 (Or (Eq (red n3 n4) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n6) True) (Eq (red n3 n6) False)))) % 26.14/26.36 Clause #847 (by clausification #[455]): Or (Eq (red n1 n3) True) % 26.14/26.36 (Or (Eq (red n3 n6) True) (Or (Eq (red n5 n6) False) (Or (Eq (red n1 n3) True) (Eq (red n3 n5) True)))) % 26.14/26.36 Clause #848 (by eliminate duplicate literals #[847]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n5 n6) False) (Eq (red n3 n5) True))) % 26.14/26.36 Clause #850 (by superposition #[848, 321]): Or (Eq (red n1 n3) True) % 26.14/26.36 (Or (Eq (red n3 n6) True) % 26.14/26.36 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Eq False True))))) % 26.14/26.36 Clause #852 (by clausification #[850]): Or (Eq (red n1 n3) True) % 26.14/26.36 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)))) % 26.14/26.36 Clause #853 (by eliminate duplicate literals #[852]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)) % 26.14/26.36 Clause #859 (by superposition #[853, 469]): Or (Eq (red n3 n6) True) % 26.14/26.36 (Or (Eq (red n3 n5) True) % 26.14/26.36 (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n4) True) (Or (Eq True False) (Eq (red n3 n4) False))))) % 26.14/26.36 Clause #864 (by superposition #[853, 22]): ∀ (a : Iota), % 26.14/26.36 Or (Eq (red n3 n6) True) % 26.14/26.36 (Or (Eq (red n3 n5) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n3) False)))) % 26.14/26.36 Clause #865 (by clausification #[864]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n1 a) False) (Eq (red a n3) False))) % 26.14/26.36 Clause #966 (by clausification #[404]): Or (Eq (red n1 n2) True) % 26.14/26.36 (Or (Eq (red n2 n6) True) (Or (Eq (red n5 n6) False) (Or (Eq (red n1 n2) True) (Eq (red n2 n5) True)))) % 26.14/26.36 Clause #967 (by eliminate duplicate literals #[966]): Or (Eq (red n1 n2) True) (Or (Eq (red n2 n6) True) (Or (Eq (red n5 n6) False) (Eq (red n2 n5) True))) % 26.14/26.36 Clause #968 (by superposition #[967, 242]): Or (Eq (red n1 n2) True) % 26.14/26.36 (Or (Eq (red n2 n6) True) % 26.14/26.36 (Or (Eq (red n2 n5) True) (Or (Eq (red n2 n6) True) (Or (Eq (red n2 n5) True) (Eq False True))))) % 26.14/26.36 Clause #985 (by clausification #[968]): Or (Eq (red n1 n2) True) % 26.14/26.36 (Or (Eq (red n2 n6) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True)))) % 26.14/26.36 Clause #986 (by eliminate duplicate literals #[985]): Or (Eq (red n1 n2) True) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True)) % 26.14/26.36 Clause #1121 (by clausification #[859]): Or (Eq (red n3 n6) True) % 26.14/26.36 (Or (Eq (red n3 n5) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n4) True) (Eq (red n3 n4) False)))) % 26.14/26.36 Clause #1146 (by clausification #[438]): Or (Eq (red n1 n2) True) % 26.14/26.36 (Or (Eq (red n2 n5) True) (Or (Eq (red n4 n5) False) (Or (Eq (red n1 n2) True) (Eq (red n2 n4) True)))) % 26.14/26.36 Clause #1147 (by eliminate duplicate literals #[1146]): Or (Eq (red n1 n2) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n4 n5) False) (Eq (red n2 n4) True))) % 26.22/26.39 Clause #1148 (by superposition #[1147, 229]): Or (Eq (red n1 n2) True) % 26.22/26.39 (Or (Eq (red n2 n5) True) % 26.22/26.39 (Or (Eq (red n2 n4) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n2 n4) True) (Eq False True))))) % 26.22/26.39 Clause #1166 (by clausification #[1148]): Or (Eq (red n1 n2) True) % 26.22/26.39 (Or (Eq (red n2 n5) True) (Or (Eq (red n2 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n2 n4) True)))) % 26.22/26.39 Clause #1167 (by eliminate duplicate literals #[1166]): Or (Eq (red n1 n2) True) (Or (Eq (red n2 n5) True) (Eq (red n2 n4) True)) % 26.22/26.39 Clause #1276 (by clausification #[448]): Or (Eq (red n1 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) (Or (Eq (red n2 n6) False) (Or (Eq (red n1 n3) True) (Eq (red n2 n3) True)))) % 26.22/26.39 Clause #1277 (by eliminate duplicate literals #[1276]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n2 n6) False) (Eq (red n2 n3) True))) % 26.22/26.39 Clause #1278 (by superposition #[1277, 250]): Or (Eq (red n1 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n2 n3) True) (Or (Eq False True) (Or (Eq (red n2 n3) True) (Eq (red n3 n6) True))))) % 26.22/26.39 Clause #1296 (by clausification #[1278]): Or (Eq (red n1 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n6) True)))) % 26.22/26.39 Clause #1297 (by eliminate duplicate literals #[1296]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Eq (red n2 n3) True)) % 26.22/26.39 Clause #1299 (by superposition #[1297, 365]): Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n2 n3) True) % 26.22/26.39 (Or (Eq (red n1 n5) True) (Or (Eq (red n4 n5) True) (Or (Eq True False) (Eq (red n3 n4) False))))) % 26.22/26.39 Clause #1345 (by clausification #[456]): Or (Eq (red n1 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) (Or (Eq (red n4 n6) False) (Or (Eq (red n1 n3) True) (Eq (red n3 n4) True)))) % 26.22/26.39 Clause #1346 (by eliminate duplicate literals #[1345]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n4 n6) False) (Eq (red n3 n4) True))) % 26.22/26.39 Clause #1349 (by superposition #[1346, 327]): Or (Eq (red n1 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq False True))))) % 26.22/26.39 Clause #1350 (by clausification #[1349]): Or (Eq (red n1 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) True)))) % 26.22/26.39 Clause #1351 (by eliminate duplicate literals #[1350]): Or (Eq (red n1 n3) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) True)) % 26.22/26.39 Clause #1367 (by superposition #[1351, 22]): ∀ (a : Iota), % 26.22/26.39 Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n3) False)))) % 26.22/26.39 Clause #1368 (by clausification #[1367]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n1 a) False) (Eq (red a n3) False))) % 26.22/26.39 Clause #1385 (by superposition #[1368, 986]): Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n3 n4) True) % 26.22/26.39 (Or (Eq (red n2 n3) False) (Or (Eq False True) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True))))) % 26.22/26.39 Clause #1386 (by superposition #[1368, 1167]): Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n3 n4) True) % 26.22/26.39 (Or (Eq (red n2 n3) False) (Or (Eq False True) (Or (Eq (red n2 n5) True) (Eq (red n2 n4) True))))) % 26.22/26.39 Clause #1405 (by clausification #[1386]): Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) False) (Or (Eq (red n2 n5) True) (Eq (red n2 n4) True)))) % 26.22/26.39 Clause #1407 (by clausification #[1385]): Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) False) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True)))) % 26.22/26.39 Clause #1452 (by clausification #[484]): Or (Eq (red n2 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) (Or (Eq (red n4 n6) False) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True)))) % 26.22/26.39 Clause #1453 (by eliminate duplicate literals #[1452]): Or (Eq (red n2 n3) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n4 n6) False) (Eq (red n3 n4) True))) % 26.22/26.39 Clause #1456 (by superposition #[1453, 327]): Or (Eq (red n2 n3) True) % 26.22/26.39 (Or (Eq (red n3 n6) True) % 26.22/26.39 (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq False True))))) % 26.22/26.41 Clause #1457 (by clausification #[1456]): Or (Eq (red n2 n3) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) True)))) % 26.22/26.41 Clause #1458 (by eliminate duplicate literals #[1457]): Or (Eq (red n2 n3) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) True)) % 26.22/26.41 Clause #1465 (by superposition #[1458, 1405]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n2 n5) True) (Eq (red n2 n4) True)))))) % 26.22/26.41 Clause #1466 (by superposition #[1458, 1407]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True)))))) % 26.22/26.41 Clause #1488 (by clausification #[560]): Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Or (Eq (red n5 n6) True) (Eq (red n3 n6) False)))) % 26.22/26.41 Clause #1492 (by clausification #[486]): Or (Eq (red n2 n3) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) (Or (Eq (red n5 n6) False) (Or (Eq (red n2 n3) True) (Eq (red n3 n5) True)))) % 26.22/26.41 Clause #1493 (by eliminate duplicate literals #[1492]): Or (Eq (red n2 n3) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n5 n6) False) (Eq (red n3 n5) True))) % 26.22/26.41 Clause #1495 (by superposition #[1493, 321]): Or (Eq (red n2 n3) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Eq False True))))) % 26.22/26.41 Clause #1496 (by clausification #[1495]): Or (Eq (red n2 n3) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)))) % 26.22/26.41 Clause #1497 (by eliminate duplicate literals #[1496]): Or (Eq (red n2 n3) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)) % 26.22/26.41 Clause #1545 (by clausification #[1299]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Or (Eq (red n4 n5) True) (Eq (red n3 n4) False)))) % 26.22/26.41 Clause #1551 (by clausification #[492]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) (Or (Eq (red n5 n6) False) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True)))) % 26.22/26.41 Clause #1552 (by eliminate duplicate literals #[1551]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n5 n6) False) (Eq (red n3 n5) True))) % 26.22/26.41 Clause #1554 (by superposition #[1552, 321]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Eq False True))))) % 26.22/26.41 Clause #1555 (by clausification #[1554]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)))) % 26.22/26.41 Clause #1556 (by eliminate duplicate literals #[1555]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq (red n3 n5) True)) % 26.22/26.41 Clause #1563 (by superposition #[1556, 832]): Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n3 n5) True) % 26.22/26.41 (Or (Eq (red n3 n5) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n6) True) (Eq True False)))))) % 26.22/26.41 Clause #1653 (by clausification #[1466]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True))))) % 26.22/26.41 Clause #1654 (by eliminate duplicate literals #[1653]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True))) % 26.22/26.41 Clause #1668 (by superposition #[1654, 22]): ∀ (a : Iota), % 26.22/26.41 Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n2 n5) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n6) False))))) % 26.22/26.41 Clause #1669 (by clausification #[1668]): ∀ (a : Iota), % 26.22/26.41 Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n2 a) False) (Eq (red a n6) False)))) % 26.22/26.41 Clause #1708 (by clausification #[1465]): Or (Eq (red n3 n6) True) % 26.22/26.41 (Or (Eq (red n3 n4) True) % 26.22/26.41 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n2 n4) True))))) % 26.22/26.41 Clause #1709 (by eliminate duplicate literals #[1708]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n2 n4) True))) % 26.22/26.44 Clause #1719 (by superposition #[1709, 1669]): Or (Eq (red n3 n6) True) % 26.22/26.44 (Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n2 n5) True) % 26.22/26.44 (Or (Eq (red n3 n6) True) % 26.22/26.44 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Or (Eq True False) (Eq (red n4 n6) False))))))) % 26.22/26.44 Clause #2377 (by clausification #[1563]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n6) True))))) % 26.22/26.44 Clause #2378 (by eliminate duplicate literals #[2377]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n6) True))) % 26.22/26.44 Clause #2389 (by superposition #[2378, 802]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n2 n6) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Or (Eq True False) (Eq (red n2 n3) False)))))) % 26.22/26.44 Clause #2471 (by clausification #[2389]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n2 n6) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Eq (red n2 n3) False))))) % 26.22/26.44 Clause #2472 (by eliminate duplicate literals #[2471]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n6) True) (Eq (red n2 n3) False))) % 26.22/26.44 Clause #2473 (by superposition #[2472, 504]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n2 n6) True) (Or (Eq False True) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True))))) % 26.22/26.44 Clause #2479 (by clausification #[2473]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n6) True) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True)))) % 26.22/26.44 Clause #2480 (by eliminate duplicate literals #[2479]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Eq (red n2 n6) True)) % 26.22/26.44 Clause #2500 (by superposition #[2480, 22]): ∀ (a : Iota), % 26.22/26.44 Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n6) False)))) % 26.22/26.44 Clause #2502 (by clausification #[2500]): ∀ (a : Iota), Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n2 a) False) (Eq (red a n6) False))) % 26.22/26.44 Clause #2506 (by superposition #[2502, 504]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n3 n6) False) (Or (Eq False True) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True))))) % 26.22/26.44 Clause #2537 (by clausification #[2506]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) False) (Or (Eq (red n3 n5) True) (Eq (red n3 n4) True)))) % 26.22/26.44 Clause #2538 (by eliminate duplicate literals #[2537]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Eq (red n3 n6) False)) % 26.22/26.44 Clause #2539 (by superposition #[2538, 1556]): Or (Eq (red n3 n4) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) (Or (Eq False True) (Or (Eq (red n3 n4) True) (Eq (red n3 n5) True)))) % 26.22/26.44 Clause #2540 (by clausification #[2539]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) True) (Eq (red n3 n5) True))) % 26.22/26.44 Clause #2541 (by eliminate duplicate literals #[2540]): Or (Eq (red n3 n4) True) (Eq (red n3 n5) True) % 26.22/26.44 Clause #2545 (by superposition #[2541, 1121]): Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n3 n6) True) % 26.22/26.44 (Or (Eq (red n3 n5) True) (Or (Eq (red n1 n2) True) (Or (Eq (red n2 n4) True) (Eq True False))))) % 26.22/26.44 Clause #2715 (by clausification #[2545]): Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n4) True)))) % 26.22/26.44 Clause #2716 (by eliminate duplicate literals #[2715]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n1 n2) True) (Eq (red n2 n4) True))) % 26.22/26.44 Clause #2727 (by superposition #[2716, 865]): Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n3 n6) True) % 26.22/26.44 (Or (Eq (red n2 n4) True) % 26.22/26.44 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Or (Eq True False) (Eq (red n2 n3) False)))))) % 26.22/26.44 Clause #2950 (by clausification #[2727]): Or (Eq (red n3 n5) True) % 26.22/26.44 (Or (Eq (red n3 n6) True) % 26.22/26.44 (Or (Eq (red n2 n4) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) True) (Eq (red n2 n3) False))))) % 26.22/26.44 Clause #2951 (by eliminate duplicate literals #[2950]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n2 n4) True) (Eq (red n2 n3) False))) % 26.22/26.46 Clause #2953 (by superposition #[2951, 1497]): Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n3 n6) True) % 26.22/26.46 (Or (Eq (red n2 n4) True) (Or (Eq False True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True))))) % 26.22/26.46 Clause #2956 (by clausification #[2953]): Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n3 n6) True) (Or (Eq (red n2 n4) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)))) % 26.22/26.46 Clause #2957 (by eliminate duplicate literals #[2956]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Eq (red n2 n4) True)) % 26.22/26.46 Clause #2969 (by superposition #[2957, 22]): ∀ (a : Iota), % 26.22/26.46 Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n3 n6) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n4) False)))) % 26.22/26.46 Clause #2970 (by clausification #[2969]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n2 a) False) (Eq (red a n4) False))) % 26.22/26.46 Clause #2976 (by superposition #[2970, 1497]): Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n3 n6) True) % 26.22/26.46 (Or (Eq (red n3 n4) False) (Or (Eq False True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True))))) % 26.22/26.46 Clause #3006 (by clausification #[2976]): Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) False) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)))) % 26.22/26.46 Clause #3007 (by eliminate duplicate literals #[3006]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) False)) % 26.22/26.46 Clause #3008 (by superposition #[3007, 2541]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq False True) (Eq (red n3 n5) True))) % 26.22/26.46 Clause #3009 (by clausification #[3008]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n5) True)) % 26.22/26.46 Clause #3010 (by eliminate duplicate literals #[3009]): Or (Eq (red n3 n5) True) (Eq (red n3 n6) True) % 26.22/26.46 Clause #3012 (by superposition #[3010, 745]): Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n4) True) (Or (Eq (red n4 n6) True) (Eq True False))))) % 26.22/26.46 Clause #3018 (by superposition #[3010, 22]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq True False) (Or (Eq (red n3 a) False) (Eq (red a n6) False))) % 26.22/26.46 Clause #3039 (by clausification #[3018]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq (red n3 a) False) (Eq (red a n6) False)) % 26.22/26.46 Clause #3040 (by superposition #[3039, 2541]): Or (Eq (red n3 n5) True) (Or (Eq (red n4 n6) False) (Or (Eq False True) (Eq (red n3 n5) True))) % 26.22/26.46 Clause #3044 (by clausification #[3040]): Or (Eq (red n3 n5) True) (Or (Eq (red n4 n6) False) (Eq (red n3 n5) True)) % 26.22/26.46 Clause #3045 (by eliminate duplicate literals #[3044]): Or (Eq (red n3 n5) True) (Eq (red n4 n6) False) % 26.22/26.46 Clause #3047 (by superposition #[3045, 256]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n6) True) (Or (Eq (red n2 n4) True) (Eq False True))) % 26.22/26.46 Clause #3050 (by clausification #[3047]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n6) True) (Eq (red n2 n4) True)) % 26.22/26.46 Clause #3064 (by superposition #[3050, 22]): ∀ (a : Iota), % 26.22/26.46 Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n2 n4) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n6) False)))) % 26.22/26.46 Clause #3101 (by clausification #[3064]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq (red n2 n4) True) (Or (Eq (red n2 a) False) (Eq (red a n6) False))) % 26.22/26.46 Clause #3441 (by clausification #[3012]): Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n4) True) (Eq (red n4 n6) True)))) % 26.22/26.46 Clause #3442 (by eliminate duplicate literals #[3441]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n4) True) (Eq (red n4 n6) True))) % 26.22/26.46 Clause #3467 (by superposition #[3442, 22]): ∀ (a : Iota), % 26.22/26.46 Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n2 n3) True) % 26.22/26.46 (Or (Eq (red n4 n6) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n4) False))))) % 26.22/26.46 Clause #3469 (by clausification #[3467]): ∀ (a : Iota), % 26.22/26.46 Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n2 n3) True) (Or (Eq (red n4 n6) True) (Or (Eq (red n1 a) False) (Eq (red a n4) False)))) % 26.22/26.46 Clause #3482 (by superposition #[3469, 708]): Or (Eq (red n3 n5) True) % 26.22/26.46 (Or (Eq (red n2 n3) True) % 26.31/26.49 (Or (Eq (red n4 n6) True) % 26.31/26.49 (Or (Eq (red n3 n4) False) (Or (Eq False True) (Or (Eq (red n3 n5) True) (Eq (red n2 n3) True)))))) % 26.31/26.49 Clause #3944 (by clausification #[3482]): Or (Eq (red n3 n5) True) % 26.31/26.49 (Or (Eq (red n2 n3) True) % 26.31/26.49 (Or (Eq (red n4 n6) True) (Or (Eq (red n3 n4) False) (Or (Eq (red n3 n5) True) (Eq (red n2 n3) True))))) % 26.31/26.49 Clause #3945 (by eliminate duplicate literals #[3944]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n4 n6) True) (Eq (red n3 n4) False))) % 26.31/26.49 Clause #3946 (by superposition #[3945, 2541]): Or (Eq (red n3 n5) True) % 26.31/26.49 (Or (Eq (red n2 n3) True) (Or (Eq (red n4 n6) True) (Or (Eq False True) (Eq (red n3 n5) True)))) % 26.31/26.49 Clause #3947 (by clausification #[3946]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n4 n6) True) (Eq (red n3 n5) True))) % 26.31/26.49 Clause #3948 (by eliminate duplicate literals #[3947]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Eq (red n4 n6) True)) % 26.31/26.49 Clause #3955 (by superposition #[3948, 3045]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n3 n5) True) (Eq True False))) % 26.31/26.49 Clause #3962 (by clausification #[3955]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n5) True)) % 26.31/26.49 Clause #3963 (by eliminate duplicate literals #[3962]): Or (Eq (red n3 n5) True) (Eq (red n2 n3) True) % 26.31/26.49 Clause #3970 (by superposition #[3963, 3101]): Or (Eq (red n3 n5) True) % 26.31/26.49 (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n4) True) (Or (Eq True False) (Eq (red n3 n6) False)))) % 26.31/26.49 Clause #3986 (by clausification #[3970]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n5) True) (Or (Eq (red n2 n4) True) (Eq (red n3 n6) False))) % 26.31/26.49 Clause #3987 (by eliminate duplicate literals #[3986]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n4) True) (Eq (red n3 n6) False)) % 26.31/26.49 Clause #3988 (by superposition #[3987, 3010]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n4) True) (Or (Eq (red n3 n5) True) (Eq False True))) % 26.31/26.49 Clause #3989 (by clausification #[3988]): Or (Eq (red n3 n5) True) (Or (Eq (red n2 n4) True) (Eq (red n3 n5) True)) % 26.31/26.49 Clause #3990 (by eliminate duplicate literals #[3989]): Or (Eq (red n3 n5) True) (Eq (red n2 n4) True) % 26.31/26.49 Clause #4001 (by superposition #[3990, 22]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n4) False))) % 26.31/26.49 Clause #4002 (by clausification #[4001]): ∀ (a : Iota), Or (Eq (red n3 n5) True) (Or (Eq (red n2 a) False) (Eq (red a n4) False)) % 26.31/26.49 Clause #4010 (by superposition #[4002, 3963]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) False) (Or (Eq (red n3 n5) True) (Eq False True))) % 26.31/26.49 Clause #4013 (by clausification #[4010]): Or (Eq (red n3 n5) True) (Or (Eq (red n3 n4) False) (Eq (red n3 n5) True)) % 26.31/26.49 Clause #4014 (by eliminate duplicate literals #[4013]): Or (Eq (red n3 n5) True) (Eq (red n3 n4) False) % 26.31/26.49 Clause #4015 (by superposition #[4014, 2541]): Or (Eq (red n3 n5) True) (Or (Eq False True) (Eq (red n3 n5) True)) % 26.31/26.49 Clause #4016 (by clausification #[4015]): Or (Eq (red n3 n5) True) (Eq (red n3 n5) True) % 26.31/26.49 Clause #4017 (by eliminate duplicate literals #[4016]): Eq (red n3 n5) True % 26.31/26.49 Clause #4051 (by superposition #[4017, 22]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (red n3 a) False) (Eq (red a n5) False)) % 26.31/26.49 Clause #4057 (by clausification #[4051]): ∀ (a : Iota), Or (Eq (red n3 a) False) (Eq (red a n5) False) % 26.31/26.49 Clause #4201 (by clausification #[1719]): Or (Eq (red n3 n6) True) % 26.31/26.49 (Or (Eq (red n3 n4) True) % 26.31/26.49 (Or (Eq (red n2 n5) True) % 26.31/26.49 (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n4 n6) False)))))) % 26.31/26.49 Clause #4202 (by eliminate duplicate literals #[4201]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n4 n6) False))) % 26.31/26.49 Clause #4205 (by superposition #[4202, 327]): Or (Eq (red n3 n6) True) % 26.31/26.49 (Or (Eq (red n3 n4) True) % 26.31/26.49 (Or (Eq (red n2 n5) True) (Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq False True))))) % 26.31/26.49 Clause #4214 (by clausification #[4205]): Or (Eq (red n3 n6) True) % 26.31/26.49 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) True)))) % 26.31/26.49 Clause #4215 (by eliminate duplicate literals #[4214]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq (red n2 n5) True)) % 26.35/26.51 Clause #4223 (by superposition #[4215, 22]): ∀ (a : Iota), % 26.35/26.51 Or (Eq (red n3 n6) True) % 26.35/26.51 (Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n5) False)))) % 26.35/26.51 Clause #4224 (by clausification #[4223]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 a) False) (Eq (red a n5) False))) % 26.35/26.51 Clause #4228 (by superposition #[4224, 1458]): Or (Eq (red n3 n6) True) % 26.35/26.51 (Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n3 n5) False) (Or (Eq False True) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) True))))) % 26.35/26.51 Clause #4245 (by clausification #[4228]): Or (Eq (red n3 n6) True) % 26.35/26.51 (Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) False) (Or (Eq (red n3 n6) True) (Eq (red n3 n4) True)))) % 26.35/26.51 Clause #4246 (by eliminate duplicate literals #[4245]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq (red n3 n5) False)) % 26.35/26.51 Clause #4247 (by forward demodulation #[4246, 4017]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n4) True) (Eq True False)) % 26.35/26.51 Clause #4248 (by clausification #[4247]): Or (Eq (red n3 n6) True) (Eq (red n3 n4) True) % 26.35/26.51 Clause #4251 (by superposition #[4248, 1488]): Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Or (Eq (red n5 n6) True) (Eq True False))))) % 26.35/26.51 Clause #4253 (by superposition #[4248, 22]): ∀ (a : Iota), Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n3 a) False) (Eq (red a n6) False))) % 26.35/26.51 Clause #4255 (by clausification #[4253]): ∀ (a : Iota), Or (Eq (red n3 n4) True) (Or (Eq (red n3 a) False) (Eq (red a n6) False)) % 26.35/26.51 Clause #4256 (by superposition #[4255, 4017]): Or (Eq (red n3 n4) True) (Or (Eq (red n5 n6) False) (Eq False True)) % 26.35/26.51 Clause #4258 (by clausification #[4256]): Or (Eq (red n3 n4) True) (Eq (red n5 n6) False) % 26.35/26.51 Clause #4259 (by superposition #[4258, 242]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n6) True) (Or (Eq (red n2 n5) True) (Eq False True))) % 26.35/26.51 Clause #4260 (by clausification #[4259]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n6) True) (Eq (red n2 n5) True)) % 26.35/26.51 Clause #4266 (by superposition #[4260, 22]): ∀ (a : Iota), % 26.35/26.51 Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n2 n5) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n6) False)))) % 26.35/26.51 Clause #4271 (by clausification #[4266]): ∀ (a : Iota), Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Or (Eq (red n2 a) False) (Eq (red a n6) False))) % 26.35/26.51 Clause #4278 (by clausification #[4251]): Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Eq (red n5 n6) True)))) % 26.35/26.51 Clause #4279 (by eliminate duplicate literals #[4278]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Eq (red n5 n6) True))) % 26.35/26.51 Clause #4297 (by superposition #[4279, 22]): ∀ (a : Iota), % 26.35/26.51 Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n2 n3) True) % 26.35/26.51 (Or (Eq (red n5 n6) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n5) False))))) % 26.35/26.51 Clause #4298 (by clausification #[4297]): ∀ (a : Iota), % 26.35/26.51 Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n2 n3) True) (Or (Eq (red n5 n6) True) (Or (Eq (red n1 a) False) (Eq (red a n5) False)))) % 26.35/26.51 Clause #4308 (by superposition #[4298, 559]): Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n2 n3) True) % 26.35/26.51 (Or (Eq (red n5 n6) True) % 26.35/26.51 (Or (Eq (red n3 n5) False) (Or (Eq False True) (Or (Eq (red n3 n4) True) (Eq (red n2 n3) True)))))) % 26.35/26.51 Clause #5089 (by clausification #[4308]): Or (Eq (red n3 n4) True) % 26.35/26.51 (Or (Eq (red n2 n3) True) % 26.35/26.51 (Or (Eq (red n5 n6) True) (Or (Eq (red n3 n5) False) (Or (Eq (red n3 n4) True) (Eq (red n2 n3) True))))) % 26.35/26.51 Clause #5090 (by eliminate duplicate literals #[5089]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n5 n6) True) (Eq (red n3 n5) False))) % 26.35/26.51 Clause #5091 (by forward demodulation #[5090, 4017]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n5 n6) True) (Eq True False))) % 26.35/26.51 Clause #5092 (by clausification #[5091]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Eq (red n5 n6) True)) % 26.35/26.51 Clause #5095 (by superposition #[5092, 4258]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n3 n4) True) (Eq True False))) % 26.35/26.54 Clause #5099 (by clausification #[5095]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n4) True)) % 26.35/26.54 Clause #5100 (by eliminate duplicate literals #[5099]): Or (Eq (red n3 n4) True) (Eq (red n2 n3) True) % 26.35/26.54 Clause #5103 (by superposition #[5100, 4271]): Or (Eq (red n3 n4) True) % 26.35/26.54 (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Or (Eq True False) (Eq (red n3 n6) False)))) % 26.35/26.54 Clause #5142 (by clausification #[5103]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n3 n6) False))) % 26.35/26.54 Clause #5143 (by eliminate duplicate literals #[5142]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n3 n6) False)) % 26.35/26.54 Clause #5144 (by superposition #[5143, 4248]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Or (Eq False True) (Eq (red n3 n4) True))) % 26.35/26.54 Clause #5148 (by clausification #[5144]): Or (Eq (red n3 n4) True) (Or (Eq (red n2 n5) True) (Eq (red n3 n4) True)) % 26.35/26.54 Clause #5149 (by eliminate duplicate literals #[5148]): Or (Eq (red n3 n4) True) (Eq (red n2 n5) True) % 26.35/26.54 Clause #5155 (by superposition #[5149, 22]): ∀ (a : Iota), Or (Eq (red n3 n4) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n5) False))) % 26.35/26.54 Clause #5156 (by clausification #[5155]): ∀ (a : Iota), Or (Eq (red n3 n4) True) (Or (Eq (red n2 a) False) (Eq (red a n5) False)) % 26.35/26.54 Clause #5159 (by superposition #[5156, 5100]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) False) (Or (Eq (red n3 n4) True) (Eq False True))) % 26.35/26.54 Clause #5163 (by clausification #[5159]): Or (Eq (red n3 n4) True) (Or (Eq (red n3 n5) False) (Eq (red n3 n4) True)) % 26.35/26.54 Clause #5164 (by eliminate duplicate literals #[5163]): Or (Eq (red n3 n4) True) (Eq (red n3 n5) False) % 26.35/26.54 Clause #5165 (by forward demodulation #[5164, 4017]): Or (Eq (red n3 n4) True) (Eq True False) % 26.35/26.54 Clause #5166 (by clausification #[5165]): Eq (red n3 n4) True % 26.35/26.54 Clause #5180 (by backward demodulation #[5166, 1545]): Or (Eq (red n3 n6) True) % 26.35/26.54 (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Or (Eq (red n4 n5) True) (Eq True False)))) % 26.35/26.54 Clause #5192 (by superposition #[5166, 4057]): Or (Eq True False) (Eq (red n4 n5) False) % 26.35/26.54 Clause #5194 (by clausification #[5192]): Eq (red n4 n5) False % 26.35/26.54 Clause #5195 (by backward demodulation #[5194, 57]): Or (Eq False True) (Eq (green n4 n5) True) % 26.35/26.54 Clause #5226 (by superposition #[5194, 229]): Or (Eq (red n2 n5) True) (Or (Eq (red n2 n4) True) (Eq False True)) % 26.35/26.54 Clause #5232 (by clausification #[5195]): Eq (green n4 n5) True % 26.35/26.54 Clause #5235 (by superposition #[5232, 208]): Or (Eq (red n4 n6) True) (Or (Eq True False) (Eq (green n5 n6) False)) % 26.35/26.54 Clause #5243 (by clausification #[5235]): Or (Eq (red n4 n6) True) (Eq (green n5 n6) False) % 26.35/26.54 Clause #5244 (by superposition #[5243, 36]): Or (Eq (red n4 n6) True) (Or (Eq (red n5 n6) True) (Eq False True)) % 26.35/26.54 Clause #5245 (by clausification #[5244]): Or (Eq (red n4 n6) True) (Eq (red n5 n6) True) % 26.35/26.54 Clause #5308 (by clausification #[5226]): Or (Eq (red n2 n5) True) (Eq (red n2 n4) True) % 26.35/26.54 Clause #5310 (by superposition #[5308, 22]): ∀ (a : Iota), Or (Eq (red n2 n5) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n4) False))) % 26.35/26.54 Clause #5319 (by clausification #[5310]): ∀ (a : Iota), Or (Eq (red n2 n5) True) (Or (Eq (red n2 a) False) (Eq (red a n4) False)) % 26.35/26.54 Clause #5394 (by clausification #[5180]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Eq (red n4 n5) True))) % 26.35/26.54 Clause #5395 (by forward demodulation #[5394, 5194]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n1 n5) True) (Eq False True))) % 26.35/26.54 Clause #5396 (by clausification #[5395]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n3) True) (Eq (red n1 n5) True)) % 26.35/26.54 Clause #5408 (by superposition #[5396, 22]): ∀ (a : Iota), % 26.35/26.54 Or (Eq (red n3 n6) True) % 26.35/26.54 (Or (Eq (red n2 n3) True) (Or (Eq True False) (Or (Eq (red n1 a) False) (Eq (red a n5) False)))) % 26.35/26.54 Clause #5409 (by clausification #[5408]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq (red n2 n3) True) (Or (Eq (red n1 a) False) (Eq (red a n5) False))) % 26.35/26.57 Clause #5418 (by superposition #[5409, 1297]): Or (Eq (red n3 n6) True) % 26.35/26.57 (Or (Eq (red n2 n3) True) % 26.35/26.57 (Or (Eq (red n3 n5) False) (Or (Eq False True) (Or (Eq (red n3 n6) True) (Eq (red n2 n3) True))))) % 26.35/26.57 Clause #5806 (by clausification #[5418]): Or (Eq (red n3 n6) True) % 26.35/26.57 (Or (Eq (red n2 n3) True) (Or (Eq (red n3 n5) False) (Or (Eq (red n3 n6) True) (Eq (red n2 n3) True)))) % 26.35/26.57 Clause #5807 (by eliminate duplicate literals #[5806]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n3) True) (Eq (red n3 n5) False)) % 26.35/26.57 Clause #5808 (by forward demodulation #[5807, 4017]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n3) True) (Eq True False)) % 26.35/26.57 Clause #5809 (by clausification #[5808]): Or (Eq (red n3 n6) True) (Eq (red n2 n3) True) % 26.35/26.57 Clause #5810 (by superposition #[5809, 5319]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n5) True) (Or (Eq True False) (Eq (red n3 n4) False))) % 26.35/26.57 Clause #5819 (by clausification #[5810]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n5) True) (Eq (red n3 n4) False)) % 26.35/26.57 Clause #5820 (by forward demodulation #[5819, 5166]): Or (Eq (red n3 n6) True) (Or (Eq (red n2 n5) True) (Eq True False)) % 26.35/26.57 Clause #5821 (by clausification #[5820]): Or (Eq (red n3 n6) True) (Eq (red n2 n5) True) % 26.35/26.57 Clause #5825 (by superposition #[5821, 22]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq True False) (Or (Eq (red n2 a) False) (Eq (red a n5) False))) % 26.35/26.57 Clause #5826 (by clausification #[5825]): ∀ (a : Iota), Or (Eq (red n3 n6) True) (Or (Eq (red n2 a) False) (Eq (red a n5) False)) % 26.35/26.57 Clause #5828 (by superposition #[5826, 5809]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) False) (Or (Eq (red n3 n6) True) (Eq False True))) % 26.35/26.57 Clause #5834 (by clausification #[5828]): Or (Eq (red n3 n6) True) (Or (Eq (red n3 n5) False) (Eq (red n3 n6) True)) % 26.35/26.57 Clause #5835 (by eliminate duplicate literals #[5834]): Or (Eq (red n3 n6) True) (Eq (red n3 n5) False) % 26.35/26.57 Clause #5836 (by forward demodulation #[5835, 4017]): Or (Eq (red n3 n6) True) (Eq True False) % 26.35/26.57 Clause #5837 (by clausification #[5836]): Eq (red n3 n6) True % 26.35/26.57 Clause #5854 (by superposition #[5837, 22]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (red n3 a) False) (Eq (red a n6) False)) % 26.35/26.57 Clause #5860 (by clausification #[5854]): ∀ (a : Iota), Or (Eq (red n3 a) False) (Eq (red a n6) False) % 26.35/26.57 Clause #5861 (by superposition #[5860, 4017]): Or (Eq (red n5 n6) False) (Eq False True) % 26.35/26.57 Clause #5862 (by superposition #[5860, 5166]): Or (Eq (red n4 n6) False) (Eq False True) % 26.35/26.57 Clause #5867 (by clausification #[5862]): Eq (red n4 n6) False % 26.35/26.57 Clause #5882 (by superposition #[5867, 5245]): Or (Eq False True) (Eq (red n5 n6) True) % 26.35/26.57 Clause #5883 (by clausification #[5882]): Eq (red n5 n6) True % 26.35/26.57 Clause #5896 (by clausification #[5861]): Eq (red n5 n6) False % 26.35/26.57 Clause #5897 (by superposition #[5896, 5883]): Eq False True % 26.35/26.57 Clause #5898 (by clausification #[5897]): False % 26.35/26.57 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------