%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS087+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 3.64s 3.85s % Output : Proof 3.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS087+1 : TPTP v9.2.0. Released v3.1.0. % 0.11/0.13 % Command : duper %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 10:16:23 EDT 2025 % 0.12/0.34 % CPUTime : % 3.64/3.85 SZS status Theorem for theBenchmark.p % 3.64/3.85 SZS output start Proof for theBenchmark.p % 3.64/3.85 Clause #16 (by assumption #[]): Eq % 3.64/3.85 (∀ (X : Iota), % 3.64/3.85 Iff (cUnsatisfiable X) % 3.64/3.85 (And (cp1 X) % 3.64/3.85 (Exists fun Y => % 3.64/3.85 And (rr X Y) (Exists fun Z => And (And (rr Y Z) (∀ (W : Iota), rinvR Z W → Not (cp1 W))) (cp1 Z))))) % 3.64/3.85 True % 3.64/3.85 Clause #19 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvR X Y) (rr Y X)) True % 3.64/3.85 Clause #20 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (rr X Y) (rr Y Z) → rr X Z) True % 3.64/3.85 Clause #21 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_19_46763) True % 3.64/3.85 Clause #58 (by clausification #[20]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (rr a Y) (rr Y Z) → rr a Z) True % 3.64/3.85 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 % 3.64/3.85 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 % 3.64/3.85 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) % 3.64/3.85 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)) % 3.64/3.85 Clause #130 (by clausification #[19]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvR a Y) (rr Y a)) True % 3.64/3.85 Clause #131 (by clausification #[130]): ∀ (a a_1 : Iota), Eq (Iff (rinvR a a_1) (rr a_1 a)) True % 3.64/3.85 Clause #132 (by clausification #[131]): ∀ (a a_1 : Iota), Or (Eq (rinvR a a_1) True) (Eq (rr a_1 a) False) % 3.64/3.85 Clause #134 (by clausification #[16]): ∀ (a : Iota), % 3.64/3.85 Eq % 3.64/3.85 (Iff (cUnsatisfiable a) % 3.64/3.85 (And (cp1 a) % 3.64/3.85 (Exists fun Y => % 3.64/3.85 And (rr a Y) (Exists fun Z => And (And (rr Y Z) (∀ (W : Iota), rinvR Z W → Not (cp1 W))) (cp1 Z))))) % 3.64/3.85 True % 3.64/3.85 Clause #136 (by clausification #[134]): ∀ (a : Iota), % 3.64/3.85 Or (Eq (cUnsatisfiable a) False) % 3.64/3.85 (Eq % 3.64/3.85 (And (cp1 a) % 3.64/3.85 (Exists fun Y => % 3.64/3.85 And (rr a Y) (Exists fun Z => And (And (rr Y Z) (∀ (W : Iota), rinvR Z W → Not (cp1 W))) (cp1 Z)))) % 3.64/3.85 True) % 3.64/3.85 Clause #152 (by clausification #[136]): ∀ (a : Iota), % 3.64/3.85 Or (Eq (cUnsatisfiable a) False) % 3.64/3.85 (Eq % 3.64/3.85 (Exists fun Y => % 3.64/3.85 And (rr a Y) (Exists fun Z => And (And (rr Y Z) (∀ (W : Iota), rinvR Z W → Not (cp1 W))) (cp1 Z))) % 3.64/3.85 True) % 3.64/3.85 Clause #153 (by clausification #[136]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp1 a) True) % 3.64/3.85 Clause #154 (by clausification #[152]): ∀ (a a_1 : Iota), % 3.64/3.85 Or (Eq (cUnsatisfiable a) False) % 3.64/3.85 (Eq % 3.64/3.85 (And (rr a (skS.0 1 a a_1)) % 3.64/3.85 (Exists fun Z => And (And (rr (skS.0 1 a a_1) Z) (∀ (W : Iota), rinvR Z W → Not (cp1 W))) (cp1 Z))) % 3.64/3.85 True) % 3.64/3.85 Clause #155 (by clausification #[154]): ∀ (a a_1 : Iota), % 3.64/3.85 Or (Eq (cUnsatisfiable a) False) % 3.64/3.85 (Eq (Exists fun Z => And (And (rr (skS.0 1 a a_1) Z) (∀ (W : Iota), rinvR Z W → Not (cp1 W))) (cp1 Z)) True) % 3.64/3.85 Clause #156 (by clausification #[154]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 1 a a_1)) True) % 3.64/3.85 Clause #157 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), % 3.64/3.85 Or (Eq (cUnsatisfiable a) False) % 3.64/3.85 (Eq % 3.64/3.85 (And (And (rr (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) (∀ (W : Iota), rinvR (skS.0 2 a a_1 a_2) W → Not (cp1 W))) % 3.64/3.85 (cp1 (skS.0 2 a a_1 a_2))) % 3.64/3.85 True) % 3.64/3.85 Clause #159 (by clausification #[157]): ∀ (a a_1 a_2 : Iota), % 3.64/3.85 Or (Eq (cUnsatisfiable a) False) % 3.64/3.85 (Eq (And (rr (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) (∀ (W : Iota), rinvR (skS.0 2 a a_1 a_2) W → Not (cp1 W))) True) % 3.64/3.85 Clause #161 (by superposition #[153, 21]): Or (Eq (cp1 i2003_11_14_17_19_46763) True) (Eq False True) % 3.64/3.85 Clause #162 (by superposition #[156, 21]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_19_46763 (skS.0 1 i2003_11_14_17_19_46763 a)) True) (Eq False True) % 3.64/3.85 Clause #163 (by clausification #[161]): Eq (cp1 i2003_11_14_17_19_46763) True % 3.64/3.85 Clause #166 (by clausification #[162]): ∀ (a : Iota), Eq (rr i2003_11_14_17_19_46763 (skS.0 1 i2003_11_14_17_19_46763 a)) True % 3.64/3.85 Clause #167 (by superposition #[166, 62]): ∀ (a a_1 : Iota), % 3.64/3.85 Or (Eq (rr i2003_11_14_17_19_46763 a) True) % 3.64/3.85 (Or (Eq True False) (Eq (rr (skS.0 1 i2003_11_14_17_19_46763 a_1) a) False)) % 3.64/3.86 Clause #174 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), % 3.64/3.86 Or (Eq (cUnsatisfiable a) False) (Eq (∀ (W : Iota), rinvR (skS.0 2 a a_1 a_2) W → Not (cp1 W)) True) % 3.64/3.86 Clause #175 (by clausification #[159]): ∀ (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) % 3.64/3.86 Clause #176 (by clausification #[174]): ∀ (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) % 3.64/3.86 Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 a_3 : Iota), % 3.64/3.86 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)) % 3.64/3.86 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : Iota), % 3.64/3.86 Or (Eq (cUnsatisfiable a) False) (Or (Eq (rinvR (skS.0 2 a a_1 a_2) a_3) False) (Eq (cp1 a_3) False)) % 3.64/3.86 Clause #179 (by superposition #[178, 21]): ∀ (a a_1 a_2 : Iota), % 3.64/3.86 Or (Eq (rinvR (skS.0 2 i2003_11_14_17_19_46763 a a_1) a_2) False) (Or (Eq (cp1 a_2) False) (Eq False True)) % 3.64/3.86 Clause #180 (by clausification #[167]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_19_46763 a) True) (Eq (rr (skS.0 1 i2003_11_14_17_19_46763 a_1) a) False) % 3.64/3.86 Clause #181 (by clausification #[179]): ∀ (a a_1 a_2 : Iota), Or (Eq (rinvR (skS.0 2 i2003_11_14_17_19_46763 a a_1) a_2) False) (Eq (cp1 a_2) False) % 3.64/3.86 Clause #182 (by superposition #[175, 21]): ∀ (a a_1 : Iota), % 3.64/3.86 Or (Eq (rr (skS.0 1 i2003_11_14_17_19_46763 a) (skS.0 2 i2003_11_14_17_19_46763 a a_1)) True) (Eq False True) % 3.64/3.86 Clause #183 (by clausification #[182]): ∀ (a a_1 : Iota), Eq (rr (skS.0 1 i2003_11_14_17_19_46763 a) (skS.0 2 i2003_11_14_17_19_46763 a a_1)) True % 3.64/3.86 Clause #184 (by superposition #[183, 180]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_19_46763 (skS.0 2 i2003_11_14_17_19_46763 a a_1)) True) (Eq True False) % 3.64/3.86 Clause #187 (by clausification #[184]): ∀ (a a_1 : Iota), Eq (rr i2003_11_14_17_19_46763 (skS.0 2 i2003_11_14_17_19_46763 a a_1)) True % 3.64/3.86 Clause #189 (by superposition #[187, 132]): ∀ (a a_1 : Iota), Or (Eq (rinvR (skS.0 2 i2003_11_14_17_19_46763 a a_1) i2003_11_14_17_19_46763) True) (Eq True False) % 3.64/3.86 Clause #192 (by clausification #[189]): ∀ (a a_1 : Iota), Eq (rinvR (skS.0 2 i2003_11_14_17_19_46763 a a_1) i2003_11_14_17_19_46763) True % 3.64/3.86 Clause #193 (by superposition #[192, 181]): Or (Eq True False) (Eq (cp1 i2003_11_14_17_19_46763) False) % 3.64/3.86 Clause #195 (by clausification #[193]): Eq (cp1 i2003_11_14_17_19_46763) False % 3.64/3.86 Clause #196 (by superposition #[195, 163]): Eq False True % 3.64/3.86 Clause #197 (by clausification #[196]): False % 3.64/3.86 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------