%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS071+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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:52:34 PM UTC 2025 % Result : Unsatisfiable 8.18s 8.41s % Output : Proof 8.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.10 % Problem : KRS071+1 : TPTP v9.2.0. Released v3.1.0. % 0.02/0.11 % Command : duper %s % 0.10/0.31 % Computer : n021.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Thu Oct 2 10:13:08 EDT 2025 % 0.15/0.31 % CPUTime : % 8.18/8.41 SZS status Theorem for theBenchmark.p % 8.18/8.41 SZS output start Proof for theBenchmark.p % 8.18/8.41 Clause #16 (by assumption #[]): Eq % 8.18/8.41 (∀ (X : Iota), % 8.18/8.41 Iff (cUnsatisfiable X) % 8.18/8.41 (And % 8.18/8.41 (And (And (Exists fun Y => And (rr X Y) (cp1 Y)) (Exists fun Y => And (rr X Y) (cp2 Y))) % 8.18/8.41 (Exists fun Y => And (rr X Y) (cp3 Y))) % 8.18/8.41 (∀ (Y0 Y1 Y2 : Iota), And (And (rr X Y0) (rr X Y1)) (rr X Y2) → Or (Or (Eq Y0 Y1) (Eq Y0 Y2)) (Eq Y1 Y2)))) % 8.18/8.41 True % 8.18/8.41 Clause #17 (by assumption #[]): Eq (∀ (X : Iota), cp1 X → Not (Or (Or (Or (cp4 X) (cp2 X)) (cp3 X)) (cp5 X))) True % 8.18/8.41 Clause #18 (by assumption #[]): Eq (∀ (X : Iota), cp2 X → Not (Or (Or (cp4 X) (cp3 X)) (cp5 X))) True % 8.18/8.41 Clause #22 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_18_39380) True % 8.18/8.41 Clause #128 (by clausification #[16]): ∀ (a : Iota), % 8.18/8.41 Eq % 8.18/8.41 (Iff (cUnsatisfiable a) % 8.18/8.41 (And % 8.18/8.41 (And (And (Exists fun Y => And (rr a Y) (cp1 Y)) (Exists fun Y => And (rr a Y) (cp2 Y))) % 8.18/8.41 (Exists fun Y => And (rr a Y) (cp3 Y))) % 8.18/8.41 (∀ (Y0 Y1 Y2 : Iota), And (And (rr a Y0) (rr a Y1)) (rr a Y2) → Or (Or (Eq Y0 Y1) (Eq Y0 Y2)) (Eq Y1 Y2)))) % 8.18/8.41 True % 8.18/8.41 Clause #130 (by clausification #[128]): ∀ (a : Iota), % 8.18/8.41 Or (Eq (cUnsatisfiable a) False) % 8.18/8.41 (Eq % 8.18/8.41 (And % 8.18/8.41 (And (And (Exists fun Y => And (rr a Y) (cp1 Y)) (Exists fun Y => And (rr a Y) (cp2 Y))) % 8.18/8.41 (Exists fun Y => And (rr a Y) (cp3 Y))) % 8.18/8.41 (∀ (Y0 Y1 Y2 : Iota), And (And (rr a Y0) (rr a Y1)) (rr a Y2) → Or (Or (Eq Y0 Y1) (Eq Y0 Y2)) (Eq Y1 Y2))) % 8.18/8.41 True) % 8.18/8.41 Clause #154 (by clausification #[18]): ∀ (a : Iota), Eq (cp2 a → Not (Or (Or (cp4 a) (cp3 a)) (cp5 a))) True % 8.18/8.41 Clause #155 (by clausification #[154]): ∀ (a : Iota), Or (Eq (cp2 a) False) (Eq (Not (Or (Or (cp4 a) (cp3 a)) (cp5 a))) True) % 8.18/8.41 Clause #156 (by clausification #[155]): ∀ (a : Iota), Or (Eq (cp2 a) False) (Eq (Or (Or (cp4 a) (cp3 a)) (cp5 a)) False) % 8.18/8.41 Clause #158 (by clausification #[156]): ∀ (a : Iota), Or (Eq (cp2 a) False) (Eq (Or (cp4 a) (cp3 a)) False) % 8.18/8.41 Clause #159 (by clausification #[158]): ∀ (a : Iota), Or (Eq (cp2 a) False) (Eq (cp3 a) False) % 8.18/8.41 Clause #161 (by clausification #[17]): ∀ (a : Iota), Eq (cp1 a → Not (Or (Or (Or (cp4 a) (cp2 a)) (cp3 a)) (cp5 a))) True % 8.18/8.41 Clause #162 (by clausification #[161]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Not (Or (Or (Or (cp4 a) (cp2 a)) (cp3 a)) (cp5 a))) True) % 8.18/8.41 Clause #163 (by clausification #[162]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Or (Or (Or (cp4 a) (cp2 a)) (cp3 a)) (cp5 a)) False) % 8.18/8.41 Clause #165 (by clausification #[163]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Or (Or (cp4 a) (cp2 a)) (cp3 a)) False) % 8.18/8.41 Clause #166 (by clausification #[165]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (cp3 a) False) % 8.18/8.41 Clause #167 (by clausification #[165]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Or (cp4 a) (cp2 a)) False) % 8.18/8.41 Clause #168 (by clausification #[167]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (cp2 a) False) % 8.18/8.41 Clause #172 (by clausification #[130]): ∀ (a : Iota), % 8.18/8.41 Or (Eq (cUnsatisfiable a) False) % 8.18/8.41 (Eq (∀ (Y0 Y1 Y2 : Iota), And (And (rr a Y0) (rr a Y1)) (rr a Y2) → Or (Or (Eq Y0 Y1) (Eq Y0 Y2)) (Eq Y1 Y2)) True) % 8.18/8.41 Clause #173 (by clausification #[130]): ∀ (a : Iota), % 8.18/8.41 Or (Eq (cUnsatisfiable a) False) % 8.18/8.41 (Eq % 8.18/8.41 (And (And (Exists fun Y => And (rr a Y) (cp1 Y)) (Exists fun Y => And (rr a Y) (cp2 Y))) % 8.18/8.41 (Exists fun Y => And (rr a Y) (cp3 Y))) % 8.18/8.41 True) % 8.18/8.41 Clause #174 (by clausification #[172]): ∀ (a a_1 : Iota), % 8.18/8.41 Or (Eq (cUnsatisfiable a) False) % 8.18/8.41 (Eq (∀ (Y1 Y2 : Iota), And (And (rr a a_1) (rr a Y1)) (rr a Y2) → Or (Or (Eq a_1 Y1) (Eq a_1 Y2)) (Eq Y1 Y2)) True) % 8.18/8.41 Clause #175 (by clausification #[174]): ∀ (a a_1 a_2 : Iota), % 8.18/8.41 Or (Eq (cUnsatisfiable a) False) % 8.18/8.41 (Eq (∀ (Y2 : Iota), And (And (rr a a_1) (rr a a_2)) (rr a Y2) → Or (Or (Eq a_1 a_2) (Eq a_1 Y2)) (Eq a_2 Y2)) True) % 8.18/8.41 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 a_3 : Iota), % 8.18/8.41 Or (Eq (cUnsatisfiable a) False) % 8.18/8.41 (Eq (And (And (rr a a_1) (rr a a_2)) (rr a a_3) → Or (Or (Eq a_1 a_2) (Eq a_1 a_3)) (Eq a_2 a_3)) True) % 8.18/8.41 Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (And (And (rr a a_1) (rr a a_2)) (rr a a_3)) False) % 8.27/8.46 (Eq (Or (Or (Eq a_1 a_2) (Eq a_1 a_3)) (Eq a_2 a_3)) True)) % 8.27/8.46 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (Or (Or (Eq a_1 a_2) (Eq a_1 a_3)) (Eq a_2 a_3)) True) % 8.27/8.46 (Or (Eq (And (rr a a_1) (rr a a_2)) False) (Eq (rr a a_3) False))) % 8.27/8.46 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (And (rr a a_1) (rr a a_2)) False) % 8.27/8.46 (Or (Eq (rr a a_3) False) (Or (Eq (Or (Eq a_1 a_2) (Eq a_1 a_3)) True) (Eq (Eq a_2 a_3) True)))) % 8.27/8.46 Clause #180 (by clausification #[179]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (rr a a_1) False) % 8.27/8.46 (Or (Eq (Or (Eq a_2 a_3) (Eq a_2 a_1)) True) % 8.27/8.46 (Or (Eq (Eq a_3 a_1) True) (Or (Eq (rr a a_2) False) (Eq (rr a a_3) False))))) % 8.27/8.46 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (rr a a_1) False) % 8.27/8.46 (Or (Eq (Eq a_2 a_1) True) % 8.27/8.46 (Or (Eq (rr a a_3) False) (Or (Eq (rr a a_2) False) (Or (Eq (Eq a_3 a_2) True) (Eq (Eq a_3 a_1) True)))))) % 8.27/8.46 Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (rr a a_1) False) % 8.27/8.46 (Or (Eq (rr a a_2) False) % 8.27/8.46 (Or (Eq (rr a a_3) False) (Or (Eq (Eq a_2 a_3) True) (Or (Eq (Eq a_2 a_1) True) (Eq a_3 a_1)))))) % 8.27/8.46 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (rr a a_1) False) % 8.27/8.46 (Or (Eq (rr a a_2) False) (Or (Eq (rr a a_3) False) (Or (Eq (Eq a_2 a_1) True) (Or (Eq a_3 a_1) (Eq a_2 a_3)))))) % 8.27/8.46 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 a_3 : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Or (Eq (rr a a_1) False) % 8.27/8.46 (Or (Eq (rr a a_2) False) (Or (Eq (rr a a_3) False) (Or (Eq a_3 a_1) (Or (Eq a_2 a_3) (Eq a_2 a_1)))))) % 8.27/8.46 Clause #185 (by superposition #[184, 22]): ∀ (a a_1 a_2 : Iota), % 8.27/8.46 Or (Eq (rr i2003_11_14_17_18_39380 a) False) % 8.27/8.46 (Or (Eq (rr i2003_11_14_17_18_39380 a_1) False) % 8.27/8.46 (Or (Eq (rr i2003_11_14_17_18_39380 a_2) False) % 8.27/8.46 (Or (Eq a_2 a) (Or (Eq a_1 a_2) (Or (Eq a_1 a) (Eq False True)))))) % 8.27/8.46 Clause #186 (by clausification #[185]): ∀ (a a_1 a_2 : Iota), % 8.27/8.46 Or (Eq (rr i2003_11_14_17_18_39380 a) False) % 8.27/8.46 (Or (Eq (rr i2003_11_14_17_18_39380 a_1) False) % 8.27/8.46 (Or (Eq (rr i2003_11_14_17_18_39380 a_2) False) (Or (Eq a_2 a) (Or (Eq a_1 a_2) (Eq a_1 a))))) % 8.27/8.46 Clause #187 (by clausification #[173]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rr a Y) (cp3 Y)) True) % 8.27/8.46 Clause #188 (by clausification #[173]): ∀ (a : Iota), % 8.27/8.46 Or (Eq (cUnsatisfiable a) False) % 8.27/8.46 (Eq (And (Exists fun Y => And (rr a Y) (cp1 Y)) (Exists fun Y => And (rr a Y) (cp2 Y))) True) % 8.27/8.46 Clause #189 (by clausification #[187]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rr a (skS.0 3 a a_1)) (cp3 (skS.0 3 a a_1))) True) % 8.27/8.46 Clause #190 (by clausification #[189]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp3 (skS.0 3 a a_1)) True) % 8.27/8.46 Clause #191 (by clausification #[189]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 3 a a_1)) True) % 8.27/8.46 Clause #192 (by superposition #[190, 22]): ∀ (a : Iota), Or (Eq (cp3 (skS.0 3 i2003_11_14_17_18_39380 a)) True) (Eq False True) % 8.27/8.46 Clause #193 (by clausification #[192]): ∀ (a : Iota), Eq (cp3 (skS.0 3 i2003_11_14_17_18_39380 a)) True % 8.27/8.46 Clause #201 (by superposition #[191, 22]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_18_39380 (skS.0 3 i2003_11_14_17_18_39380 a)) True) (Eq False True) % 8.27/8.46 Clause #202 (by clausification #[201]): ∀ (a : Iota), Eq (rr i2003_11_14_17_18_39380 (skS.0 3 i2003_11_14_17_18_39380 a)) True % 8.27/8.46 Clause #211 (by clausification #[188]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rr a Y) (cp2 Y)) True) % 8.27/8.46 Clause #212 (by clausification #[188]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rr a Y) (cp1 Y)) True) % 8.27/8.46 Clause #213 (by clausification #[211]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rr a (skS.0 4 a a_1)) (cp2 (skS.0 4 a a_1))) True) % 8.30/8.51 Clause #214 (by clausification #[213]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp2 (skS.0 4 a a_1)) True) % 8.30/8.51 Clause #215 (by clausification #[213]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 4 a a_1)) True) % 8.30/8.51 Clause #216 (by superposition #[214, 22]): ∀ (a : Iota), Or (Eq (cp2 (skS.0 4 i2003_11_14_17_18_39380 a)) True) (Eq False True) % 8.30/8.51 Clause #221 (by clausification #[216]): ∀ (a : Iota), Eq (cp2 (skS.0 4 i2003_11_14_17_18_39380 a)) True % 8.30/8.51 Clause #228 (by clausification #[212]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rr a (skS.0 5 a a_1)) (cp1 (skS.0 5 a a_1))) True) % 8.30/8.51 Clause #229 (by clausification #[228]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp1 (skS.0 5 a a_1)) True) % 8.30/8.51 Clause #230 (by clausification #[228]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 5 a a_1)) True) % 8.30/8.51 Clause #231 (by superposition #[229, 22]): ∀ (a : Iota), Or (Eq (cp1 (skS.0 5 i2003_11_14_17_18_39380 a)) True) (Eq False True) % 8.30/8.51 Clause #234 (by clausification #[231]): ∀ (a : Iota), Eq (cp1 (skS.0 5 i2003_11_14_17_18_39380 a)) True % 8.30/8.51 Clause #236 (by superposition #[234, 166]): ∀ (a : Iota), Or (Eq True False) (Eq (cp3 (skS.0 5 i2003_11_14_17_18_39380 a)) False) % 8.30/8.51 Clause #237 (by superposition #[234, 168]): ∀ (a : Iota), Or (Eq True False) (Eq (cp2 (skS.0 5 i2003_11_14_17_18_39380 a)) False) % 8.30/8.51 Clause #240 (by clausification #[237]): ∀ (a : Iota), Eq (cp2 (skS.0 5 i2003_11_14_17_18_39380 a)) False % 8.30/8.51 Clause #241 (by clausification #[236]): ∀ (a : Iota), Eq (cp3 (skS.0 5 i2003_11_14_17_18_39380 a)) False % 8.30/8.51 Clause #245 (by superposition #[230, 22]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_18_39380 (skS.0 5 i2003_11_14_17_18_39380 a)) True) (Eq False True) % 8.30/8.51 Clause #246 (by clausification #[245]): ∀ (a : Iota), Eq (rr i2003_11_14_17_18_39380 (skS.0 5 i2003_11_14_17_18_39380 a)) True % 8.30/8.51 Clause #257 (by superposition #[215, 22]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_18_39380 (skS.0 4 i2003_11_14_17_18_39380 a)) True) (Eq False True) % 8.30/8.51 Clause #260 (by clausification #[257]): ∀ (a : Iota), Eq (rr i2003_11_14_17_18_39380 (skS.0 4 i2003_11_14_17_18_39380 a)) True % 8.30/8.51 Clause #261 (by superposition #[260, 186]): ∀ (a a_1 a_2 : Iota), % 8.30/8.51 Or (Eq True False) % 8.30/8.51 (Or (Eq (rr i2003_11_14_17_18_39380 a) False) % 8.30/8.51 (Or (Eq (rr i2003_11_14_17_18_39380 a_1) False) % 8.30/8.51 (Or (Eq a_1 (skS.0 4 i2003_11_14_17_18_39380 a_2)) % 8.30/8.51 (Or (Eq a a_1) (Eq a (skS.0 4 i2003_11_14_17_18_39380 a_2)))))) % 8.30/8.51 Clause #275 (by clausification #[261]): ∀ (a a_1 a_2 : Iota), % 8.30/8.51 Or (Eq (rr i2003_11_14_17_18_39380 a) False) % 8.30/8.51 (Or (Eq (rr i2003_11_14_17_18_39380 a_1) False) % 8.30/8.51 (Or (Eq a_1 (skS.0 4 i2003_11_14_17_18_39380 a_2)) (Or (Eq a a_1) (Eq a (skS.0 4 i2003_11_14_17_18_39380 a_2))))) % 8.30/8.51 Clause #276 (by superposition #[275, 202]): ∀ (a a_1 a_2 : Iota), % 8.30/8.51 Or (Eq (rr i2003_11_14_17_18_39380 a) False) % 8.30/8.51 (Or (Eq a (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.30/8.51 (Or (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) a) % 8.30/8.51 (Or (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) (skS.0 4 i2003_11_14_17_18_39380 a_1)) (Eq False True)))) % 8.30/8.51 Clause #283 (by clausification #[276]): ∀ (a a_1 a_2 : Iota), % 8.30/8.51 Or (Eq (rr i2003_11_14_17_18_39380 a) False) % 8.30/8.51 (Or (Eq a (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.30/8.51 (Or (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) a) % 8.30/8.51 (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) (skS.0 4 i2003_11_14_17_18_39380 a_1)))) % 8.30/8.51 Clause #285 (by superposition #[283, 246]): ∀ (a a_1 a_2 : Iota), % 8.30/8.51 Or (Eq (skS.0 5 i2003_11_14_17_18_39380 a) (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.30/8.51 (Or (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) (skS.0 5 i2003_11_14_17_18_39380 a)) % 8.30/8.51 (Or (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) (skS.0 4 i2003_11_14_17_18_39380 a_1)) (Eq False True))) % 8.30/8.51 Clause #340 (by clausification #[285]): ∀ (a a_1 a_2 : Iota), % 8.30/8.51 Or (Eq (skS.0 5 i2003_11_14_17_18_39380 a) (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.30/8.51 (Or (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) (skS.0 5 i2003_11_14_17_18_39380 a)) % 8.34/8.53 (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) (skS.0 4 i2003_11_14_17_18_39380 a_1))) % 8.34/8.53 Clause #376 (by superposition #[340, 221]): ∀ (a a_1 a_2 : Iota), % 8.34/8.53 Or (Eq (skS.0 5 i2003_11_14_17_18_39380 a) (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.34/8.53 (Or (Eq (skS.0 3 i2003_11_14_17_18_39380 a_2) (skS.0 5 i2003_11_14_17_18_39380 a)) % 8.34/8.53 (Eq (cp2 (skS.0 3 i2003_11_14_17_18_39380 a_2)) True)) % 8.34/8.53 Clause #416 (by superposition #[376, 241]): ∀ (a a_1 a_2 : Iota), % 8.34/8.53 Or (Eq (skS.0 5 i2003_11_14_17_18_39380 a) (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.34/8.53 (Or (Eq (cp2 (skS.0 3 i2003_11_14_17_18_39380 a_2)) True) (Eq (cp3 (skS.0 3 i2003_11_14_17_18_39380 a_2)) False)) % 8.34/8.53 Clause #432 (by forward demodulation #[416, 193]): ∀ (a a_1 a_2 : Iota), % 8.34/8.53 Or (Eq (skS.0 5 i2003_11_14_17_18_39380 a) (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.34/8.53 (Or (Eq (cp2 (skS.0 3 i2003_11_14_17_18_39380 a_2)) True) (Eq True False)) % 8.34/8.53 Clause #433 (by clausification #[432]): ∀ (a a_1 a_2 : Iota), % 8.34/8.53 Or (Eq (skS.0 5 i2003_11_14_17_18_39380 a) (skS.0 4 i2003_11_14_17_18_39380 a_1)) % 8.34/8.53 (Eq (cp2 (skS.0 3 i2003_11_14_17_18_39380 a_2)) True) % 8.34/8.53 Clause #436 (by superposition #[433, 240]): ∀ (a a_1 : Iota), % 8.34/8.53 Or (Eq (cp2 (skS.0 3 i2003_11_14_17_18_39380 a)) True) (Eq (cp2 (skS.0 4 i2003_11_14_17_18_39380 a_1)) False) % 8.34/8.53 Clause #456 (by superposition #[436, 221]): ∀ (a : Iota), Or (Eq (cp2 (skS.0 3 i2003_11_14_17_18_39380 a)) True) (Eq False True) % 8.34/8.53 Clause #525 (by clausification #[456]): ∀ (a : Iota), Eq (cp2 (skS.0 3 i2003_11_14_17_18_39380 a)) True % 8.34/8.53 Clause #526 (by superposition #[525, 159]): ∀ (a : Iota), Or (Eq True False) (Eq (cp3 (skS.0 3 i2003_11_14_17_18_39380 a)) False) % 8.34/8.53 Clause #533 (by clausification #[526]): ∀ (a : Iota), Eq (cp3 (skS.0 3 i2003_11_14_17_18_39380 a)) False % 8.34/8.53 Clause #534 (by superposition #[533, 193]): Eq False True % 8.34/8.53 Clause #541 (by clausification #[534]): False % 8.34/8.53 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------