%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS085+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:36 PM UTC 2025 % Result : Unsatisfiable 5.86s 6.03s % Output : Proof 5.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : KRS085+1 : TPTP v9.2.0. Released v3.1.0. % 0.00/0.11 % Command : duper %s % 0.10/0.31 % Computer : n029.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.16/0.31 % CPULimit : 300 % 0.16/0.31 % WCLimit : 300 % 0.16/0.31 % DateTime : Thu Oct 2 10:22:08 EDT 2025 % 0.16/0.31 % CPUTime : % 5.86/6.03 SZS status Theorem for theBenchmark.p % 5.86/6.03 SZS output start Proof for theBenchmark.p % 5.86/6.03 Clause #16 (by assumption #[]): Eq % 5.86/6.03 (∀ (X : Iota), % 5.86/6.03 Iff (cUnsatisfiable X) % 5.86/6.03 (And % 5.86/6.03 (Exists fun Y => % 5.86/6.03 And (rr X Y) (Exists fun Z => And (And (rr Y Z) (cp1 Z)) (∀ (W : Iota), rinvR Z W → Not (cp1 W)))) % 5.86/6.03 (cp1 X))) % 5.86/6.03 True % 5.86/6.03 Clause #19 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvR X Y) (rr Y X)) True % 5.86/6.03 Clause #20 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (rr X Y) (rr Y Z) → rr X Z) True % 5.86/6.03 Clause #21 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_19_39537) True % 5.86/6.03 Clause #58 (by clausification #[20]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (rr a Y) (rr Y Z) → rr a Z) True % 5.86/6.03 Clause #59 (by clausification #[58]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (rr a a_1) (rr a_1 Z) → rr a Z) True % 5.86/6.03 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), Eq (And (rr a a_1) (rr a_1 a_2) → rr a a_2) True % 5.86/6.03 Clause #61 (by clausification #[60]): ∀ (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) % 5.86/6.03 Clause #62 (by clausification #[61]): ∀ (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)) % 5.86/6.03 Clause #124 (by clausification #[19]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvR a Y) (rr Y a)) True % 5.86/6.03 Clause #125 (by clausification #[124]): ∀ (a a_1 : Iota), Eq (Iff (rinvR a a_1) (rr a_1 a)) True % 5.86/6.03 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), Or (Eq (rinvR a a_1) True) (Eq (rr a_1 a) False) % 5.86/6.03 Clause #132 (by clausification #[16]): ∀ (a : Iota), % 5.86/6.03 Eq % 5.86/6.03 (Iff (cUnsatisfiable a) % 5.86/6.03 (And % 5.86/6.03 (Exists fun Y => % 5.86/6.03 And (rr a Y) (Exists fun Z => And (And (rr Y Z) (cp1 Z)) (∀ (W : Iota), rinvR Z W → Not (cp1 W)))) % 5.86/6.03 (cp1 a))) % 5.86/6.03 True % 5.86/6.03 Clause #134 (by clausification #[132]): ∀ (a : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) % 5.86/6.03 (Eq % 5.86/6.03 (And % 5.86/6.03 (Exists fun Y => % 5.86/6.03 And (rr a Y) (Exists fun Z => And (And (rr Y Z) (cp1 Z)) (∀ (W : Iota), rinvR Z W → Not (cp1 W)))) % 5.86/6.03 (cp1 a)) % 5.86/6.03 True) % 5.86/6.03 Clause #155 (by clausification #[134]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp1 a) True) % 5.86/6.03 Clause #156 (by clausification #[134]): ∀ (a : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) % 5.86/6.03 (Eq % 5.86/6.03 (Exists fun Y => % 5.86/6.03 And (rr a Y) (Exists fun Z => And (And (rr Y Z) (cp1 Z)) (∀ (W : Iota), rinvR Z W → Not (cp1 W)))) % 5.86/6.03 True) % 5.86/6.03 Clause #157 (by superposition #[155, 21]): Or (Eq (cp1 i2003_11_14_17_19_39537) True) (Eq False True) % 5.86/6.03 Clause #158 (by clausification #[157]): Eq (cp1 i2003_11_14_17_19_39537) True % 5.86/6.03 Clause #161 (by clausification #[156]): ∀ (a a_1 : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) % 5.86/6.03 (Eq % 5.86/6.03 (And (rr a (skS.0 1 a a_1)) % 5.86/6.03 (Exists fun Z => And (And (rr (skS.0 1 a a_1) Z) (cp1 Z)) (∀ (W : Iota), rinvR Z W → Not (cp1 W)))) % 5.86/6.03 True) % 5.86/6.03 Clause #162 (by clausification #[161]): ∀ (a a_1 : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) % 5.86/6.03 (Eq (Exists fun Z => And (And (rr (skS.0 1 a a_1) Z) (cp1 Z)) (∀ (W : Iota), rinvR Z W → Not (cp1 W))) True) % 5.86/6.03 Clause #163 (by clausification #[161]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 1 a a_1)) True) % 5.86/6.03 Clause #164 (by clausification #[162]): ∀ (a a_1 a_2 : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) % 5.86/6.03 (Eq % 5.86/6.03 (And (And (rr (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) (cp1 (skS.0 2 a a_1 a_2))) % 5.86/6.03 (∀ (W : Iota), rinvR (skS.0 2 a a_1 a_2) W → Not (cp1 W))) % 5.86/6.03 True) % 5.86/6.03 Clause #165 (by clausification #[164]): ∀ (a a_1 a_2 : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) (Eq (∀ (W : Iota), rinvR (skS.0 2 a a_1 a_2) W → Not (cp1 W)) True) % 5.86/6.03 Clause #166 (by clausification #[164]): ∀ (a a_1 a_2 : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) (Eq (And (rr (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) (cp1 (skS.0 2 a a_1 a_2))) True) % 5.86/6.03 Clause #167 (by clausification #[165]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rinvR (skS.0 2 a a_1 a_2) a_3 → Not (cp1 a_3)) True) % 5.86/6.03 Clause #168 (by clausification #[167]): ∀ (a a_1 a_2 a_3 : Iota), % 5.86/6.03 Or (Eq (cUnsatisfiable a) False) (Or (Eq (rinvR (skS.0 2 a a_1 a_2) a_3) False) (Eq (Not (cp1 a_3)) True)) % 5.86/6.06 Clause #169 (by clausification #[168]): ∀ (a a_1 a_2 a_3 : Iota), % 5.86/6.06 Or (Eq (cUnsatisfiable a) False) (Or (Eq (rinvR (skS.0 2 a a_1 a_2) a_3) False) (Eq (cp1 a_3) False)) % 5.86/6.06 Clause #170 (by superposition #[169, 21]): ∀ (a a_1 a_2 : Iota), % 5.86/6.06 Or (Eq (rinvR (skS.0 2 i2003_11_14_17_19_39537 a a_1) a_2) False) (Or (Eq (cp1 a_2) False) (Eq False True)) % 5.86/6.06 Clause #171 (by superposition #[163, 21]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_19_39537 (skS.0 1 i2003_11_14_17_19_39537 a)) True) (Eq False True) % 5.86/6.06 Clause #172 (by clausification #[171]): ∀ (a : Iota), Eq (rr i2003_11_14_17_19_39537 (skS.0 1 i2003_11_14_17_19_39537 a)) True % 5.86/6.06 Clause #173 (by superposition #[172, 62]): ∀ (a a_1 : Iota), % 5.86/6.06 Or (Eq (rr i2003_11_14_17_19_39537 a) True) % 5.86/6.06 (Or (Eq True False) (Eq (rr (skS.0 1 i2003_11_14_17_19_39537 a_1) a) False)) % 5.86/6.06 Clause #177 (by clausification #[173]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_19_39537 a) True) (Eq (rr (skS.0 1 i2003_11_14_17_19_39537 a_1) a) False) % 5.86/6.06 Clause #180 (by clausification #[170]): ∀ (a a_1 a_2 : Iota), Or (Eq (rinvR (skS.0 2 i2003_11_14_17_19_39537 a a_1) a_2) False) (Eq (cp1 a_2) False) % 5.86/6.06 Clause #184 (by clausification #[166]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True) % 5.86/6.06 Clause #189 (by superposition #[184, 21]): ∀ (a a_1 : Iota), % 5.86/6.06 Or (Eq (rr (skS.0 1 i2003_11_14_17_19_39537 a) (skS.0 2 i2003_11_14_17_19_39537 a a_1)) True) (Eq False True) % 5.86/6.06 Clause #191 (by clausification #[189]): ∀ (a a_1 : Iota), Eq (rr (skS.0 1 i2003_11_14_17_19_39537 a) (skS.0 2 i2003_11_14_17_19_39537 a a_1)) True % 5.86/6.06 Clause #192 (by superposition #[191, 177]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_19_39537 (skS.0 2 i2003_11_14_17_19_39537 a a_1)) True) (Eq True False) % 5.86/6.06 Clause #195 (by clausification #[192]): ∀ (a a_1 : Iota), Eq (rr i2003_11_14_17_19_39537 (skS.0 2 i2003_11_14_17_19_39537 a a_1)) True % 5.86/6.06 Clause #197 (by superposition #[195, 126]): ∀ (a a_1 : Iota), Or (Eq (rinvR (skS.0 2 i2003_11_14_17_19_39537 a a_1) i2003_11_14_17_19_39537) True) (Eq True False) % 5.86/6.06 Clause #198 (by clausification #[197]): ∀ (a a_1 : Iota), Eq (rinvR (skS.0 2 i2003_11_14_17_19_39537 a a_1) i2003_11_14_17_19_39537) True % 5.86/6.06 Clause #199 (by superposition #[198, 180]): Or (Eq True False) (Eq (cp1 i2003_11_14_17_19_39537) False) % 5.86/6.06 Clause #201 (by clausification #[199]): Eq (cp1 i2003_11_14_17_19_39537) False % 5.86/6.06 Clause #202 (by superposition #[201, 158]): Eq False True % 5.86/6.06 Clause #203 (by clausification #[202]): False % 5.86/6.06 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------