%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS072+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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 3.75s 3.96s % Output : Proof 3.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.14 % Problem : KRS072+1 : TPTP v9.2.0. Released v3.1.0. % 0.06/0.16 % Command : duper %s % 0.14/0.37 % Computer : n013.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Thu Oct 2 10:20:38 EDT 2025 % 0.14/0.37 % CPUTime : % 3.75/3.96 SZS status Theorem for theBenchmark.p % 3.75/3.96 SZS output start Proof for theBenchmark.p % 3.75/3.96 Clause #16 (by assumption #[]): Eq % 3.75/3.96 (∀ (X : Iota), % 3.75/3.96 Iff (cUnsatisfiable X) % 3.75/3.96 (And % 3.75/3.96 (Exists fun Y => % 3.75/3.96 And (And (rinvR X Y) (∀ (Z0 Z1 : Iota), And (rr Y Z0) (rr Y Z1) → Eq Z0 Z1)) % 3.75/3.96 (Exists fun Z => And (rr Y Z) (cp1 Z))) % 3.75/3.96 (cp2 X))) % 3.75/3.96 True % 3.75/3.96 Clause #17 (by assumption #[]): Eq (∀ (X : Iota), cp1 X → Not (Or (Or (Or (cp3 X) (cp2 X)) (cp4 X)) (cp5 X))) True % 3.75/3.96 Clause #21 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvR X Y) (rr Y X)) True % 3.75/3.96 Clause #22 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_18_50190) True % 3.75/3.96 Clause #128 (by clausification #[16]): ∀ (a : Iota), % 3.75/3.96 Eq % 3.75/3.96 (Iff (cUnsatisfiable a) % 3.75/3.96 (And % 3.75/3.96 (Exists fun Y => % 3.75/3.96 And (And (rinvR a Y) (∀ (Z0 Z1 : Iota), And (rr Y Z0) (rr Y Z1) → Eq Z0 Z1)) % 3.75/3.96 (Exists fun Z => And (rr Y Z) (cp1 Z))) % 3.75/3.96 (cp2 a))) % 3.75/3.96 True % 3.75/3.96 Clause #130 (by clausification #[128]): ∀ (a : Iota), % 3.75/3.96 Or (Eq (cUnsatisfiable a) False) % 3.75/3.96 (Eq % 3.75/3.96 (And % 3.75/3.96 (Exists fun Y => % 3.75/3.96 And (And (rinvR a Y) (∀ (Z0 Z1 : Iota), And (rr Y Z0) (rr Y Z1) → Eq Z0 Z1)) % 3.75/3.96 (Exists fun Z => And (rr Y Z) (cp1 Z))) % 3.75/3.96 (cp2 a)) % 3.75/3.96 True) % 3.75/3.96 Clause #145 (by clausification #[21]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvR a Y) (rr Y a)) True % 3.75/3.96 Clause #146 (by clausification #[145]): ∀ (a a_1 : Iota), Eq (Iff (rinvR a a_1) (rr a_1 a)) True % 3.75/3.96 Clause #148 (by clausification #[146]): ∀ (a a_1 : Iota), Or (Eq (rinvR a a_1) False) (Eq (rr a_1 a) True) % 3.75/3.96 Clause #156 (by clausification #[17]): ∀ (a : Iota), Eq (cp1 a → Not (Or (Or (Or (cp3 a) (cp2 a)) (cp4 a)) (cp5 a))) True % 3.75/3.96 Clause #157 (by clausification #[156]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Not (Or (Or (Or (cp3 a) (cp2 a)) (cp4 a)) (cp5 a))) True) % 3.75/3.96 Clause #158 (by clausification #[157]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Or (Or (Or (cp3 a) (cp2 a)) (cp4 a)) (cp5 a)) False) % 3.75/3.96 Clause #160 (by clausification #[158]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Or (Or (cp3 a) (cp2 a)) (cp4 a)) False) % 3.75/3.96 Clause #162 (by clausification #[160]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (Or (cp3 a) (cp2 a)) False) % 3.75/3.96 Clause #163 (by clausification #[162]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (cp2 a) False) % 3.75/3.96 Clause #165 (by clausification #[130]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp2 a) True) % 3.75/3.96 Clause #166 (by clausification #[130]): ∀ (a : Iota), % 3.75/3.96 Or (Eq (cUnsatisfiable a) False) % 3.75/3.96 (Eq % 3.75/3.96 (Exists fun Y => % 3.75/3.96 And (And (rinvR a Y) (∀ (Z0 Z1 : Iota), And (rr Y Z0) (rr Y Z1) → Eq Z0 Z1)) % 3.75/3.96 (Exists fun Z => And (rr Y Z) (cp1 Z))) % 3.75/3.96 True) % 3.75/3.96 Clause #167 (by superposition #[165, 22]): Or (Eq (cp2 i2003_11_14_17_18_50190) True) (Eq False True) % 3.75/3.96 Clause #169 (by clausification #[167]): Eq (cp2 i2003_11_14_17_18_50190) True % 3.75/3.96 Clause #181 (by clausification #[166]): ∀ (a a_1 : Iota), % 3.75/3.96 Or (Eq (cUnsatisfiable a) False) % 3.75/3.96 (Eq % 3.75/3.96 (And % 3.75/3.96 (And (rinvR a (skS.0 2 a a_1)) % 3.75/3.96 (∀ (Z0 Z1 : Iota), And (rr (skS.0 2 a a_1) Z0) (rr (skS.0 2 a a_1) Z1) → Eq Z0 Z1)) % 3.75/3.96 (Exists fun Z => And (rr (skS.0 2 a a_1) Z) (cp1 Z))) % 3.75/3.96 True) % 3.75/3.96 Clause #182 (by clausification #[181]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Z => And (rr (skS.0 2 a a_1) Z) (cp1 Z)) True) % 3.75/3.96 Clause #183 (by clausification #[181]): ∀ (a a_1 : Iota), % 3.75/3.96 Or (Eq (cUnsatisfiable a) False) % 3.75/3.96 (Eq % 3.75/3.96 (And (rinvR a (skS.0 2 a a_1)) (∀ (Z0 Z1 : Iota), And (rr (skS.0 2 a a_1) Z0) (rr (skS.0 2 a a_1) Z1) → Eq Z0 Z1)) % 3.75/3.96 True) % 3.75/3.96 Clause #184 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), % 3.75/3.96 Or (Eq (cUnsatisfiable a) False) (Eq (And (rr (skS.0 2 a a_1) (skS.0 3 a a_1 a_2)) (cp1 (skS.0 3 a a_1 a_2))) True) % 3.75/3.96 Clause #185 (by clausification #[184]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp1 (skS.0 3 a a_1 a_2)) True) % 3.75/3.96 Clause #186 (by clausification #[184]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr (skS.0 2 a a_1) (skS.0 3 a a_1 a_2)) True) % 3.75/3.96 Clause #187 (by superposition #[185, 22]): ∀ (a a_1 : Iota), Or (Eq (cp1 (skS.0 3 i2003_11_14_17_18_50190 a a_1)) True) (Eq False True) % 3.80/3.98 Clause #188 (by clausification #[187]): ∀ (a a_1 : Iota), Eq (cp1 (skS.0 3 i2003_11_14_17_18_50190 a a_1)) True % 3.80/3.98 Clause #191 (by superposition #[188, 163]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (cp2 (skS.0 3 i2003_11_14_17_18_50190 a a_1)) False) % 3.80/3.98 Clause #194 (by clausification #[191]): ∀ (a a_1 : Iota), Eq (cp2 (skS.0 3 i2003_11_14_17_18_50190 a a_1)) False % 3.80/3.98 Clause #199 (by clausification #[183]): ∀ (a a_1 : Iota), % 3.80/3.98 Or (Eq (cUnsatisfiable a) False) % 3.80/3.98 (Eq (∀ (Z0 Z1 : Iota), And (rr (skS.0 2 a a_1) Z0) (rr (skS.0 2 a a_1) Z1) → Eq Z0 Z1) True) % 3.80/3.98 Clause #200 (by clausification #[183]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rinvR a (skS.0 2 a a_1)) True) % 3.80/3.98 Clause #201 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), % 3.80/3.98 Or (Eq (cUnsatisfiable a) False) % 3.80/3.98 (Eq (∀ (Z1 : Iota), And (rr (skS.0 2 a a_1) a_2) (rr (skS.0 2 a a_1) Z1) → Eq a_2 Z1) True) % 3.80/3.98 Clause #202 (by clausification #[201]): ∀ (a a_1 a_2 a_3 : Iota), % 3.80/3.98 Or (Eq (cUnsatisfiable a) False) (Eq (And (rr (skS.0 2 a a_1) a_2) (rr (skS.0 2 a a_1) a_3) → Eq a_2 a_3) True) % 3.80/3.98 Clause #203 (by clausification #[202]): ∀ (a a_1 a_2 a_3 : Iota), % 3.80/3.98 Or (Eq (cUnsatisfiable a) False) % 3.80/3.98 (Or (Eq (And (rr (skS.0 2 a a_1) a_2) (rr (skS.0 2 a a_1) a_3)) False) (Eq (Eq a_2 a_3) True)) % 3.80/3.98 Clause #204 (by clausification #[203]): ∀ (a a_1 a_2 a_3 : Iota), % 3.80/3.98 Or (Eq (cUnsatisfiable a) False) % 3.80/3.98 (Or (Eq (Eq a_1 a_2) True) (Or (Eq (rr (skS.0 2 a a_3) a_1) False) (Eq (rr (skS.0 2 a a_3) a_2) False))) % 3.80/3.98 Clause #205 (by clausification #[204]): ∀ (a a_1 a_2 a_3 : Iota), % 3.80/3.98 Or (Eq (cUnsatisfiable a) False) % 3.80/3.98 (Or (Eq (rr (skS.0 2 a a_1) a_2) False) (Or (Eq (rr (skS.0 2 a a_1) a_3) False) (Eq a_2 a_3))) % 3.80/3.98 Clause #206 (by superposition #[205, 22]): ∀ (a a_1 a_2 : Iota), % 3.80/3.98 Or (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) a_1) False) % 3.80/3.98 (Or (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) a_2) False) (Or (Eq a_1 a_2) (Eq False True))) % 3.80/3.98 Clause #207 (by superposition #[200, 22]): ∀ (a : Iota), Or (Eq (rinvR i2003_11_14_17_18_50190 (skS.0 2 i2003_11_14_17_18_50190 a)) True) (Eq False True) % 3.80/3.98 Clause #208 (by clausification #[207]): ∀ (a : Iota), Eq (rinvR i2003_11_14_17_18_50190 (skS.0 2 i2003_11_14_17_18_50190 a)) True % 3.80/3.98 Clause #209 (by superposition #[208, 148]): ∀ (a : Iota), Or (Eq True False) (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) i2003_11_14_17_18_50190) True) % 3.80/3.98 Clause #210 (by clausification #[209]): ∀ (a : Iota), Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) i2003_11_14_17_18_50190) True % 3.80/3.98 Clause #214 (by superposition #[186, 22]): ∀ (a a_1 : Iota), % 3.80/3.98 Or (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) (skS.0 3 i2003_11_14_17_18_50190 a a_1)) True) (Eq False True) % 3.80/3.98 Clause #215 (by clausification #[214]): ∀ (a a_1 : Iota), Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) (skS.0 3 i2003_11_14_17_18_50190 a a_1)) True % 3.80/3.98 Clause #219 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 3.80/3.98 Or (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) a_1) False) % 3.80/3.98 (Or (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) a_2) False) (Eq a_1 a_2)) % 3.80/3.98 Clause #220 (by superposition #[219, 210]): ∀ (a a_1 : Iota), % 3.80/3.98 Or (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) a_1) False) (Or (Eq i2003_11_14_17_18_50190 a_1) (Eq False True)) % 3.80/3.98 Clause #222 (by clausification #[220]): ∀ (a a_1 : Iota), Or (Eq (rr (skS.0 2 i2003_11_14_17_18_50190 a) a_1) False) (Eq i2003_11_14_17_18_50190 a_1) % 3.80/3.98 Clause #224 (by superposition #[222, 215]): ∀ (a a_1 : Iota), Or (Eq i2003_11_14_17_18_50190 (skS.0 3 i2003_11_14_17_18_50190 a a_1)) (Eq False True) % 3.80/3.98 Clause #226 (by clausification #[224]): ∀ (a a_1 : Iota), Eq i2003_11_14_17_18_50190 (skS.0 3 i2003_11_14_17_18_50190 a a_1) % 3.80/3.98 Clause #228 (by backward demodulation #[226, 194]): Eq (cp2 i2003_11_14_17_18_50190) False % 3.80/3.98 Clause #229 (by superposition #[228, 169]): Eq False True % 3.80/3.98 Clause #230 (by clausification #[229]): False % 3.80/3.98 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------