%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS119+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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.00s 4.19s % Output : Proof 4.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS119+1 : TPTP v9.2.0. Released v3.1.0. % 0.07/0.13 % Command : duper %s % 0.14/0.34 % Computer : n001.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 10:10:08 EDT 2025 % 0.14/0.34 % CPUTime : % 4.00/4.19 SZS status Theorem for theBenchmark.p % 4.00/4.19 SZS output start Proof for theBenchmark.p % 4.00/4.19 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.00/4.19 Clause #22 (by assumption #[]): Eq (∀ (X : Iota), Iff (cp1 X) (Not (Exists fun Y => ra_Px1 X Y))) True % 4.00/4.19 Clause #23 (by assumption #[]): Eq (∀ (X : Iota), Iff (cp1xcomp X) (Exists fun Y0 => ra_Px1 X Y0)) True % 4.00/4.19 Clause #24 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Ax2 X) (And (cp1 X) (∀ (Y : Iota), rinvR X Y → cp1xcomp Y))) True % 4.00/4.19 Clause #25 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Vx3 X) (Exists fun Y => And (rr X Y) (ca_Ax2 Y))) True % 4.00/4.19 Clause #28 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvR X Y) (rr Y X)) True % 4.00/4.19 Clause #29 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (rr X Y) (rr Y Z) → rr X Z) True % 4.00/4.19 Clause #30 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_21_44786) True % 4.00/4.19 Clause #98 (by clausification #[29]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (rr a Y) (rr Y Z) → rr a Z) True % 4.00/4.19 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.00/4.19 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.00/4.19 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.00/4.19 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.00/4.19 Clause #177 (by clausification #[28]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvR a Y) (rr Y a)) True % 4.00/4.19 Clause #178 (by clausification #[177]): ∀ (a a_1 : Iota), Eq (Iff (rinvR a a_1) (rr a_1 a)) True % 4.00/4.19 Clause #179 (by clausification #[178]): ∀ (a a_1 : Iota), Or (Eq (rinvR a a_1) True) (Eq (rr a_1 a) False) % 4.00/4.19 Clause #181 (by clausification #[21]): ∀ (a : Iota), Eq (Iff (cUnsatisfiable a) (And (Exists fun Y => And (rr a Y) (ca_Vx3 Y)) (cp1 a))) True % 4.00/4.19 Clause #183 (by clausification #[181]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (Exists fun Y => And (rr a Y) (ca_Vx3 Y)) (cp1 a)) True) % 4.00/4.19 Clause #187 (by betaEtaReduce #[23]): Eq (∀ (X : Iota), Iff (cp1xcomp X) (Exists (ra_Px1 X))) True % 4.00/4.19 Clause #188 (by clausification #[187]): ∀ (a : Iota), Eq (Iff (cp1xcomp a) (Exists (ra_Px1 a))) True % 4.00/4.19 Clause #190 (by clausification #[188]): ∀ (a : Iota), Or (Eq (cp1xcomp a) False) (Eq (Exists (ra_Px1 a)) True) % 4.00/4.19 Clause #192 (by clausification #[190]): ∀ (a a_1 : Iota), Or (Eq (cp1xcomp a) False) (Eq (ra_Px1 a (skS.0 0 a a_1)) True) % 4.00/4.19 Clause #193 (by betaEtaReduce #[22]): Eq (∀ (X : Iota), Iff (cp1 X) (Not (Exists (ra_Px1 X)))) True % 4.00/4.19 Clause #194 (by clausification #[193]): ∀ (a : Iota), Eq (Iff (cp1 a) (Not (Exists (ra_Px1 a)))) True % 4.00/4.19 Clause #196 (by clausification #[194]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Not (Exists (ra_Px1 a))) True) % 4.00/4.19 Clause #202 (by clausification #[24]): ∀ (a : Iota), Eq (Iff (ca_Ax2 a) (And (cp1 a) (∀ (Y : Iota), rinvR a Y → cp1xcomp Y))) True % 4.00/4.19 Clause #204 (by clausification #[202]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (And (cp1 a) (∀ (Y : Iota), rinvR a Y → cp1xcomp Y)) True) % 4.00/4.19 Clause #210 (by clausification #[196]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Exists (ra_Px1 a)) False) % 4.00/4.19 Clause #211 (by clausification #[210]): ∀ (a a_1 : Iota), Or (Eq (cp1 a) False) (Eq (ra_Px1 a a_1) False) % 4.00/4.19 Clause #212 (by clausification #[204]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (∀ (Y : Iota), rinvR a Y → cp1xcomp Y) True) % 4.00/4.19 Clause #214 (by clausification #[212]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Eq (rinvR a a_1 → cp1xcomp a_1) True) % 4.00/4.19 Clause #215 (by clausification #[214]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Or (Eq (rinvR a a_1) False) (Eq (cp1xcomp a_1) True)) % 4.00/4.19 Clause #216 (by clausification #[25]): ∀ (a : Iota), Eq (Iff (ca_Vx3 a) (Exists fun Y => And (rr a Y) (ca_Ax2 Y))) True % 4.00/4.19 Clause #218 (by clausification #[216]): ∀ (a : Iota), Or (Eq (ca_Vx3 a) False) (Eq (Exists fun Y => And (rr a Y) (ca_Ax2 Y)) True) % 4.00/4.19 Clause #221 (by clausification #[218]): ∀ (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.00/4.21 Clause #222 (by clausification #[221]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 a) False) (Eq (ca_Ax2 (skS.0 3 a a_1)) True) % 4.00/4.21 Clause #223 (by clausification #[221]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 a) False) (Eq (rr a (skS.0 3 a a_1)) True) % 4.00/4.21 Clause #224 (by clausification #[183]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp1 a) True) % 4.00/4.21 Clause #225 (by clausification #[183]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rr a Y) (ca_Vx3 Y)) True) % 4.00/4.21 Clause #226 (by superposition #[224, 30]): Or (Eq (cp1 i2003_11_14_17_21_44786) True) (Eq False True) % 4.00/4.21 Clause #227 (by clausification #[226]): Eq (cp1 i2003_11_14_17_21_44786) True % 4.00/4.21 Clause #230 (by superposition #[227, 211]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px1 i2003_11_14_17_21_44786 a) False) % 4.00/4.21 Clause #231 (by clausification #[230]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_44786 a) False % 4.00/4.21 Clause #234 (by clausification #[225]): ∀ (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.00/4.21 Clause #235 (by clausification #[234]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (ca_Vx3 (skS.0 4 a a_1)) True) % 4.00/4.21 Clause #236 (by clausification #[234]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 4 a a_1)) True) % 4.00/4.21 Clause #237 (by superposition #[235, 30]): ∀ (a : Iota), Or (Eq (ca_Vx3 (skS.0 4 i2003_11_14_17_21_44786 a)) True) (Eq False True) % 4.00/4.21 Clause #238 (by clausification #[237]): ∀ (a : Iota), Eq (ca_Vx3 (skS.0 4 i2003_11_14_17_21_44786 a)) True % 4.00/4.21 Clause #239 (by superposition #[238, 222]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (ca_Ax2 (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1)) True) % 4.00/4.21 Clause #242 (by superposition #[236, 30]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_21_44786 (skS.0 4 i2003_11_14_17_21_44786 a)) True) (Eq False True) % 4.00/4.21 Clause #243 (by clausification #[242]): ∀ (a : Iota), Eq (rr i2003_11_14_17_21_44786 (skS.0 4 i2003_11_14_17_21_44786 a)) True % 4.00/4.21 Clause #244 (by superposition #[243, 102]): ∀ (a a_1 : Iota), % 4.00/4.21 Or (Eq (rr i2003_11_14_17_21_44786 a) True) % 4.00/4.21 (Or (Eq True False) (Eq (rr (skS.0 4 i2003_11_14_17_21_44786 a_1) a) False)) % 4.00/4.21 Clause #250 (by superposition #[223, 238]): ∀ (a a_1 : Iota), % 4.00/4.21 Or (Eq True False) % 4.00/4.21 (Eq (rr (skS.0 4 i2003_11_14_17_21_44786 a) (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1)) True) % 4.00/4.21 Clause #266 (by clausification #[244]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_21_44786 a) True) (Eq (rr (skS.0 4 i2003_11_14_17_21_44786 a_1) a) False) % 4.00/4.21 Clause #268 (by clausification #[239]): ∀ (a a_1 : Iota), Eq (ca_Ax2 (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1)) True % 4.00/4.21 Clause #269 (by superposition #[268, 215]): ∀ (a a_1 a_2 : Iota), % 4.00/4.21 Or (Eq True False) % 4.00/4.21 (Or (Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1) a_2) False) (Eq (cp1xcomp a_2) True)) % 4.00/4.21 Clause #271 (by clausification #[250]): ∀ (a a_1 : Iota), Eq (rr (skS.0 4 i2003_11_14_17_21_44786 a) (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1)) True % 4.00/4.21 Clause #272 (by superposition #[271, 266]): ∀ (a a_1 : Iota), % 4.00/4.21 Or (Eq (rr i2003_11_14_17_21_44786 (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1)) True) (Eq True False) % 4.00/4.21 Clause #285 (by clausification #[272]): ∀ (a a_1 : Iota), Eq (rr i2003_11_14_17_21_44786 (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1)) True % 4.00/4.21 Clause #288 (by superposition #[285, 179]): ∀ (a a_1 : Iota), % 4.00/4.21 Or (Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1) i2003_11_14_17_21_44786) True) (Eq True False) % 4.00/4.21 Clause #292 (by clausification #[288]): ∀ (a a_1 : Iota), Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1) i2003_11_14_17_21_44786) True % 4.00/4.21 Clause #330 (by clausification #[269]): ∀ (a a_1 a_2 : Iota), % 4.00/4.21 Or (Eq (rinvR (skS.0 3 (skS.0 4 i2003_11_14_17_21_44786 a) a_1) a_2) False) (Eq (cp1xcomp a_2) True) % 4.00/4.21 Clause #331 (by superposition #[330, 292]): Or (Eq (cp1xcomp i2003_11_14_17_21_44786) True) (Eq False True) % 4.00/4.21 Clause #332 (by clausification #[331]): Eq (cp1xcomp i2003_11_14_17_21_44786) True % 4.00/4.22 Clause #333 (by superposition #[332, 192]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px1 i2003_11_14_17_21_44786 (skS.0 0 i2003_11_14_17_21_44786 a)) True) % 4.00/4.22 Clause #334 (by clausification #[333]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_44786 (skS.0 0 i2003_11_14_17_21_44786 a)) True % 4.00/4.22 Clause #335 (by superposition #[334, 231]): Eq True False % 4.00/4.22 Clause #337 (by clausification #[335]): False % 4.00/4.22 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------