%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS110+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:38 PM UTC 2025 % Result : Unsatisfiable 3.88s 4.04s % Output : Proof 3.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : KRS110+1 : TPTP v9.2.0. Released v3.1.0. % 0.12/0.13 % Command : duper %s % 0.14/0.35 % Computer : n013.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 10:14:53 EDT 2025 % 0.14/0.35 % CPUTime : % 3.88/4.04 SZS status Theorem for theBenchmark.p % 3.88/4.04 SZS output start Proof for theBenchmark.p % 3.88/4.04 Clause #24 (by assumption #[]): Eq % 3.88/4.04 (∀ (X : Iota), % 3.88/4.04 Iff (cUnsatisfiable X) (And (Exists fun Y => And (rs X Y) (ca_Ax2 Y)) (∀ (Y : Iota), rs X Y → cpxcomp Y))) % 3.88/4.04 True % 3.88/4.04 Clause #25 (by assumption #[]): Eq (∀ (X : Iota), Iff (cp X) (Not (Exists fun Y => ra_Px1 X Y))) True % 3.88/4.04 Clause #26 (by assumption #[]): Eq (∀ (X : Iota), Iff (cpxcomp X) (Exists fun Y0 => ra_Px1 X Y0)) True % 3.88/4.04 Clause #27 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Ax2 X) (And (cp X) (Exists fun Y => And (rinvS X Y) (cp Y)))) True % 3.88/4.04 Clause #34 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_21_12565) True % 3.88/4.04 Clause #191 (by clausification #[24]): ∀ (a : Iota), % 3.88/4.04 Eq (Iff (cUnsatisfiable a) (And (Exists fun Y => And (rs a Y) (ca_Ax2 Y)) (∀ (Y : Iota), rs a Y → cpxcomp Y))) True % 3.88/4.04 Clause #193 (by clausification #[191]): ∀ (a : Iota), % 3.88/4.04 Or (Eq (cUnsatisfiable a) False) % 3.88/4.04 (Eq (And (Exists fun Y => And (rs a Y) (ca_Ax2 Y)) (∀ (Y : Iota), rs a Y → cpxcomp Y)) True) % 3.88/4.04 Clause #223 (by betaEtaReduce #[25]): Eq (∀ (X : Iota), Iff (cp X) (Not (Exists (ra_Px1 X)))) True % 3.88/4.04 Clause #224 (by clausification #[223]): ∀ (a : Iota), Eq (Iff (cp a) (Not (Exists (ra_Px1 a)))) True % 3.88/4.04 Clause #226 (by clausification #[224]): ∀ (a : Iota), Or (Eq (cp a) False) (Eq (Not (Exists (ra_Px1 a))) True) % 3.88/4.04 Clause #229 (by clausification #[226]): ∀ (a : Iota), Or (Eq (cp a) False) (Eq (Exists (ra_Px1 a)) False) % 3.88/4.04 Clause #230 (by clausification #[229]): ∀ (a a_1 : Iota), Or (Eq (cp a) False) (Eq (ra_Px1 a a_1) False) % 3.88/4.04 Clause #239 (by betaEtaReduce #[26]): Eq (∀ (X : Iota), Iff (cpxcomp X) (Exists (ra_Px1 X))) True % 3.88/4.04 Clause #240 (by clausification #[239]): ∀ (a : Iota), Eq (Iff (cpxcomp a) (Exists (ra_Px1 a))) True % 3.88/4.04 Clause #242 (by clausification #[240]): ∀ (a : Iota), Or (Eq (cpxcomp a) False) (Eq (Exists (ra_Px1 a)) True) % 3.88/4.04 Clause #246 (by clausification #[242]): ∀ (a a_1 : Iota), Or (Eq (cpxcomp a) False) (Eq (ra_Px1 a (skS.0 2 a a_1)) True) % 3.88/4.04 Clause #251 (by clausification #[27]): ∀ (a : Iota), Eq (Iff (ca_Ax2 a) (And (cp a) (Exists fun Y => And (rinvS a Y) (cp Y)))) True % 3.88/4.04 Clause #253 (by clausification #[251]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (And (cp a) (Exists fun Y => And (rinvS a Y) (cp Y))) True) % 3.88/4.04 Clause #257 (by clausification #[193]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (∀ (Y : Iota), rs a Y → cpxcomp Y) True) % 3.88/4.04 Clause #258 (by clausification #[193]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rs a Y) (ca_Ax2 Y)) True) % 3.88/4.04 Clause #259 (by clausification #[257]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rs a a_1 → cpxcomp a_1) True) % 3.88/4.04 Clause #260 (by clausification #[259]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Or (Eq (rs a a_1) False) (Eq (cpxcomp a_1) True)) % 3.88/4.04 Clause #261 (by superposition #[260, 34]): ∀ (a : Iota), Or (Eq (rs i2003_11_14_17_21_12565 a) False) (Or (Eq (cpxcomp a) True) (Eq False True)) % 3.88/4.04 Clause #262 (by clausification #[261]): ∀ (a : Iota), Or (Eq (rs i2003_11_14_17_21_12565 a) False) (Eq (cpxcomp a) True) % 3.88/4.04 Clause #263 (by clausification #[258]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rs a (skS.0 3 a a_1)) (ca_Ax2 (skS.0 3 a a_1))) True) % 3.88/4.04 Clause #264 (by clausification #[263]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (ca_Ax2 (skS.0 3 a a_1)) True) % 3.88/4.04 Clause #265 (by clausification #[263]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rs a (skS.0 3 a a_1)) True) % 3.88/4.04 Clause #266 (by superposition #[264, 34]): ∀ (a : Iota), Or (Eq (ca_Ax2 (skS.0 3 i2003_11_14_17_21_12565 a)) True) (Eq False True) % 3.88/4.04 Clause #267 (by clausification #[266]): ∀ (a : Iota), Eq (ca_Ax2 (skS.0 3 i2003_11_14_17_21_12565 a)) True % 3.88/4.04 Clause #268 (by superposition #[265, 34]): ∀ (a : Iota), Or (Eq (rs i2003_11_14_17_21_12565 (skS.0 3 i2003_11_14_17_21_12565 a)) True) (Eq False True) % 3.88/4.04 Clause #269 (by clausification #[268]): ∀ (a : Iota), Eq (rs i2003_11_14_17_21_12565 (skS.0 3 i2003_11_14_17_21_12565 a)) True % 3.88/4.04 Clause #270 (by superposition #[269, 262]): ∀ (a : Iota), Or (Eq True False) (Eq (cpxcomp (skS.0 3 i2003_11_14_17_21_12565 a)) True) % 3.88/4.05 Clause #277 (by clausification #[270]): ∀ (a : Iota), Eq (cpxcomp (skS.0 3 i2003_11_14_17_21_12565 a)) True % 3.88/4.05 Clause #278 (by superposition #[277, 246]): ∀ (a a_1 : Iota), % 3.88/4.05 Or (Eq True False) % 3.88/4.05 (Eq (ra_Px1 (skS.0 3 i2003_11_14_17_21_12565 a) (skS.0 2 (skS.0 3 i2003_11_14_17_21_12565 a) a_1)) True) % 3.88/4.05 Clause #286 (by clausification #[253]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (cp a) True) % 3.88/4.05 Clause #291 (by superposition #[286, 267]): ∀ (a : Iota), Or (Eq (cp (skS.0 3 i2003_11_14_17_21_12565 a)) True) (Eq False True) % 3.88/4.05 Clause #292 (by clausification #[291]): ∀ (a : Iota), Eq (cp (skS.0 3 i2003_11_14_17_21_12565 a)) True % 3.88/4.05 Clause #293 (by superposition #[292, 230]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (ra_Px1 (skS.0 3 i2003_11_14_17_21_12565 a) a_1) False) % 3.88/4.05 Clause #299 (by clausification #[293]): ∀ (a a_1 : Iota), Eq (ra_Px1 (skS.0 3 i2003_11_14_17_21_12565 a) a_1) False % 3.88/4.05 Clause #318 (by clausification #[278]): ∀ (a a_1 : Iota), Eq (ra_Px1 (skS.0 3 i2003_11_14_17_21_12565 a) (skS.0 2 (skS.0 3 i2003_11_14_17_21_12565 a) a_1)) True % 3.88/4.05 Clause #319 (by superposition #[318, 299]): Eq True False % 3.88/4.05 Clause #321 (by clausification #[319]): False % 3.88/4.05 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------