%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS121+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.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:39 PM UTC 2025 % Result : Unsatisfiable 4.21s 4.37s % Output : Proof 4.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS121+1 : TPTP v9.2.0. Released v3.1.0. % 0.07/0.14 % Command : duper %s % 0.15/0.35 % Computer : n005.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 10:15:08 EDT 2025 % 0.15/0.35 % CPUTime : % 4.21/4.37 SZS status Theorem for theBenchmark.p % 4.21/4.37 SZS output start Proof for theBenchmark.p % 4.21/4.37 Clause #21 (by assumption #[]): Eq (∀ (X : Iota), Iff (cUnsatisfiable X) (And (Exists fun Y => And (rr X Y) (ca_Vx3 Y)) (cp1 X))) True % 4.21/4.37 Clause #22 (by assumption #[]): Eq (∀ (X : Iota), Iff (cp1 X) (Not (Exists fun Y => ra_Px1 X Y))) True % 4.21/4.37 Clause #23 (by assumption #[]): Eq (∀ (X : Iota), Iff (cp1xcomp X) (Exists fun Y0 => ra_Px1 X Y0)) True % 4.21/4.37 Clause #24 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Ax2 X) (And (cp1 X) (∀ (Y : Iota), rinvR X Y → cp1xcomp Y))) True % 4.21/4.37 Clause #25 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Vx3 X) (Exists fun Y => And (rr X Y) (ca_Ax2 Y))) True % 4.21/4.37 Clause #28 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvR X Y) (rr Y X)) True % 4.21/4.37 Clause #29 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (rr X Y) (rr Y Z) → rr X Z) True % 4.21/4.37 Clause #30 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_21_5199) True % 4.21/4.37 Clause #98 (by clausification #[29]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (rr a Y) (rr Y Z) → rr a Z) True % 4.21/4.37 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (rr a a_1) (rr a_1 Z) → rr a Z) True % 4.21/4.37 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 : Iota), Eq (And (rr a a_1) (rr a_1 a_2) → rr a a_2) True % 4.21/4.37 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (rr a a_1) (rr a_1 a_2)) False) (Eq (rr a a_2) True) % 4.21/4.37 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), Or (Eq (rr a a_1) True) (Or (Eq (rr a a_2) False) (Eq (rr a_2 a_1) False)) % 4.21/4.37 Clause #174 (by clausification #[28]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvR a Y) (rr Y a)) True % 4.21/4.37 Clause #175 (by clausification #[174]): ∀ (a a_1 : Iota), Eq (Iff (rinvR a a_1) (rr a_1 a)) True % 4.21/4.37 Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), Or (Eq (rinvR a a_1) True) (Eq (rr a_1 a) False) % 4.21/4.37 Clause #178 (by clausification #[21]): ∀ (a : Iota), Eq (Iff (cUnsatisfiable a) (And (Exists fun Y => And (rr a Y) (ca_Vx3 Y)) (cp1 a))) True % 4.21/4.37 Clause #180 (by clausification #[178]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (Exists fun Y => And (rr a Y) (ca_Vx3 Y)) (cp1 a)) True) % 4.21/4.37 Clause #184 (by betaEtaReduce #[23]): Eq (∀ (X : Iota), Iff (cp1xcomp X) (Exists (ra_Px1 X))) True % 4.21/4.37 Clause #185 (by clausification #[184]): ∀ (a : Iota), Eq (Iff (cp1xcomp a) (Exists (ra_Px1 a))) True % 4.21/4.37 Clause #187 (by clausification #[185]): ∀ (a : Iota), Or (Eq (cp1xcomp a) False) (Eq (Exists (ra_Px1 a)) True) % 4.21/4.37 Clause #189 (by clausification #[187]): ∀ (a a_1 : Iota), Or (Eq (cp1xcomp a) False) (Eq (ra_Px1 a (skS.0 0 a a_1)) True) % 4.21/4.37 Clause #190 (by betaEtaReduce #[22]): Eq (∀ (X : Iota), Iff (cp1 X) (Not (Exists (ra_Px1 X)))) True % 4.21/4.37 Clause #191 (by clausification #[190]): ∀ (a : Iota), Eq (Iff (cp1 a) (Not (Exists (ra_Px1 a)))) True % 4.21/4.37 Clause #193 (by clausification #[191]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Not (Exists (ra_Px1 a))) True) % 4.21/4.37 Clause #199 (by clausification #[24]): ∀ (a : Iota), Eq (Iff (ca_Ax2 a) (And (cp1 a) (∀ (Y : Iota), rinvR a Y → cp1xcomp Y))) True % 4.21/4.37 Clause #201 (by clausification #[199]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (And (cp1 a) (∀ (Y : Iota), rinvR a Y → cp1xcomp Y)) True) % 4.21/4.37 Clause #207 (by clausification #[193]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Exists (ra_Px1 a)) False) % 4.21/4.37 Clause #208 (by clausification #[207]): ∀ (a a_1 : Iota), Or (Eq (cp1 a) False) (Eq (ra_Px1 a a_1) False) % 4.21/4.37 Clause #209 (by clausification #[201]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (∀ (Y : Iota), rinvR a Y → cp1xcomp Y) True) % 4.21/4.37 Clause #211 (by clausification #[209]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Eq (rinvR a a_1 → cp1xcomp a_1) True) % 4.21/4.37 Clause #212 (by clausification #[211]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Or (Eq (rinvR a a_1) False) (Eq (cp1xcomp a_1) True)) % 4.21/4.37 Clause #213 (by clausification #[25]): ∀ (a : Iota), Eq (Iff (ca_Vx3 a) (Exists fun Y => And (rr a Y) (ca_Ax2 Y))) True % 4.21/4.37 Clause #215 (by clausification #[213]): ∀ (a : Iota), Or (Eq (ca_Vx3 a) False) (Eq (Exists fun Y => And (rr a Y) (ca_Ax2 Y)) True) % 4.21/4.37 Clause #218 (by clausification #[215]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 a) False) (Eq (And (rr a (skS.0 3 a a_1)) (ca_Ax2 (skS.0 3 a a_1))) True) % 4.21/4.39 Clause #219 (by clausification #[218]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 a) False) (Eq (ca_Ax2 (skS.0 3 a a_1)) True) % 4.21/4.39 Clause #220 (by clausification #[218]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 a) False) (Eq (rr a (skS.0 3 a a_1)) True) % 4.21/4.39 Clause #221 (by clausification #[180]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp1 a) True) % 4.21/4.39 Clause #222 (by clausification #[180]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rr a Y) (ca_Vx3 Y)) True) % 4.21/4.39 Clause #223 (by superposition #[221, 30]): Or (Eq (cp1 i2003_11_14_17_21_5199) True) (Eq False True) % 4.21/4.39 Clause #224 (by clausification #[223]): Eq (cp1 i2003_11_14_17_21_5199) True % 4.21/4.39 Clause #227 (by superposition #[224, 208]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px1 i2003_11_14_17_21_5199 a) False) % 4.21/4.39 Clause #228 (by clausification #[227]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_5199 a) False % 4.21/4.39 Clause #231 (by clausification #[222]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rr a (skS.0 4 a a_1)) (ca_Vx3 (skS.0 4 a a_1))) True) % 4.21/4.39 Clause #232 (by clausification #[231]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (ca_Vx3 (skS.0 4 a a_1)) True) % 4.21/4.39 Clause #233 (by clausification #[231]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 4 a a_1)) True) % 4.21/4.39 Clause #234 (by superposition #[232, 30]): ∀ (a : Iota), Or (Eq (ca_Vx3 (skS.0 4 i2003_11_14_17_21_5199 a)) True) (Eq False True) % 4.21/4.39 Clause #235 (by clausification #[234]): ∀ (a : Iota), Eq (ca_Vx3 (skS.0 4 i2003_11_14_17_21_5199 a)) True % 4.21/4.39 Clause #236 (by superposition #[235, 219]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (ca_Ax2 (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1)) True) % 4.21/4.39 Clause #239 (by superposition #[233, 30]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_21_5199 (skS.0 4 i2003_11_14_17_21_5199 a)) True) (Eq False True) % 4.21/4.39 Clause #240 (by clausification #[239]): ∀ (a : Iota), Eq (rr i2003_11_14_17_21_5199 (skS.0 4 i2003_11_14_17_21_5199 a)) True % 4.21/4.39 Clause #241 (by superposition #[240, 102]): ∀ (a a_1 : Iota), % 4.21/4.39 Or (Eq (rr i2003_11_14_17_21_5199 a) True) (Or (Eq True False) (Eq (rr (skS.0 4 i2003_11_14_17_21_5199 a_1) a) False)) % 4.21/4.39 Clause #247 (by superposition #[220, 235]): ∀ (a a_1 : Iota), % 4.21/4.39 Or (Eq True False) (Eq (rr (skS.0 4 i2003_11_14_17_21_5199 a) (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1)) True) % 4.21/4.39 Clause #263 (by clausification #[241]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_21_5199 a) True) (Eq (rr (skS.0 4 i2003_11_14_17_21_5199 a_1) a) False) % 4.21/4.39 Clause #265 (by clausification #[236]): ∀ (a a_1 : Iota), Eq (ca_Ax2 (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1)) True % 4.21/4.39 Clause #266 (by superposition #[265, 212]): ∀ (a a_1 a_2 : Iota), % 4.21/4.39 Or (Eq True False) % 4.21/4.39 (Or (Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1) a_2) False) (Eq (cp1xcomp a_2) True)) % 4.21/4.39 Clause #268 (by clausification #[247]): ∀ (a a_1 : Iota), Eq (rr (skS.0 4 i2003_11_14_17_21_5199 a) (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1)) True % 4.21/4.39 Clause #269 (by superposition #[268, 263]): ∀ (a a_1 : Iota), % 4.21/4.39 Or (Eq (rr i2003_11_14_17_21_5199 (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1)) True) (Eq True False) % 4.21/4.39 Clause #282 (by clausification #[269]): ∀ (a a_1 : Iota), Eq (rr i2003_11_14_17_21_5199 (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1)) True % 4.21/4.39 Clause #285 (by superposition #[282, 176]): ∀ (a a_1 : Iota), % 4.21/4.39 Or (Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1) i2003_11_14_17_21_5199) True) (Eq True False) % 4.21/4.39 Clause #289 (by clausification #[285]): ∀ (a a_1 : Iota), Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1) i2003_11_14_17_21_5199) True % 4.21/4.39 Clause #327 (by clausification #[266]): ∀ (a a_1 a_2 : Iota), % 4.21/4.39 Or (Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_5199 a) a_1) a_2) False) (Eq (cp1xcomp a_2) True) % 4.21/4.39 Clause #328 (by superposition #[327, 289]): Or (Eq (cp1xcomp i2003_11_14_17_21_5199) True) (Eq False True) % 4.21/4.39 Clause #329 (by clausification #[328]): Eq (cp1xcomp i2003_11_14_17_21_5199) True % 4.21/4.40 Clause #330 (by superposition #[329, 189]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px1 i2003_11_14_17_21_5199 (skS.0 0 i2003_11_14_17_21_5199 a)) True) % 4.21/4.40 Clause #331 (by clausification #[330]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_5199 (skS.0 0 i2003_11_14_17_21_5199 a)) True % 4.21/4.40 Clause #332 (by superposition #[331, 228]): Eq True False % 4.21/4.40 Clause #334 (by clausification #[332]): False % 4.21/4.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------