%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS108+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:38 PM UTC 2025 % Result : Unsatisfiable 4.37s 4.54s % Output : Proof 4.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KRS108+1 : TPTP v9.2.0. Released v3.1.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 10:16:38 EDT 2025 % 0.13/0.34 % CPUTime : % 4.37/4.54 SZS status Theorem for theBenchmark.p % 4.37/4.54 SZS output start Proof for theBenchmark.p % 4.37/4.54 Clause #41 (by assumption #[]): Eq (∀ (X : Iota), Iff (cUnsatisfiable X) (And (Exists fun Y => And (rinvR X Y) (ca_Ax14 Y)) (cp2 X))) True % 4.37/4.54 Clause #42 (by assumption #[]): Eq (∀ (X : Iota), cp1 X → ca_Cx1 X) True % 4.37/4.54 Clause #43 (by assumption #[]): Eq (∀ (X : Iota), Iff (cp2 X) (Exists fun Y0 => ra_Px5 X Y0)) True % 4.37/4.54 Clause #45 (by assumption #[]): Eq (∀ (X : Iota), Iff (cp2xcomp X) (Not (Exists fun Y => ra_Px5 X Y))) True % 4.37/4.54 Clause #54 (by assumption #[]): Eq % 4.37/4.54 (∀ (X : Iota), % 4.37/4.54 Iff (ca_Ax14 X) (And (Exists fun Y => And (rr X Y) (cp1 Y)) (∀ (Y0 Y1 : Iota), And (rr X Y0) (rr X Y1) → Eq Y0 Y1))) % 4.37/4.54 True % 4.37/4.54 Clause #55 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Cx1 X) (And (And (And (cp2xcomp X) (cp5xcomp X)) (cp3xcomp X)) (cp4xcomp X))) True % 4.37/4.54 Clause #64 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvR X Y) (rr Y X)) True % 4.37/4.54 Clause #65 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_21_04740) True % 4.37/4.54 Clause #72 (by clausification #[42]): ∀ (a : Iota), Eq (cp1 a → ca_Cx1 a) True % 4.37/4.54 Clause #73 (by clausification #[72]): ∀ (a : Iota), Or (Eq (cp1 a) False) (Eq (ca_Cx1 a) True) % 4.37/4.54 Clause #334 (by clausification #[64]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvR a Y) (rr Y a)) True % 4.37/4.54 Clause #335 (by clausification #[334]): ∀ (a a_1 : Iota), Eq (Iff (rinvR a a_1) (rr a_1 a)) True % 4.37/4.54 Clause #337 (by clausification #[335]): ∀ (a a_1 : Iota), Or (Eq (rinvR a a_1) False) (Eq (rr a_1 a) True) % 4.37/4.54 Clause #338 (by clausification #[41]): ∀ (a : Iota), Eq (Iff (cUnsatisfiable a) (And (Exists fun Y => And (rinvR a Y) (ca_Ax14 Y)) (cp2 a))) True % 4.37/4.54 Clause #340 (by clausification #[338]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (Exists fun Y => And (rinvR a Y) (ca_Ax14 Y)) (cp2 a)) True) % 4.37/4.54 Clause #356 (by betaEtaReduce #[43]): Eq (∀ (X : Iota), Iff (cp2 X) (Exists (ra_Px5 X))) True % 4.37/4.54 Clause #357 (by clausification #[356]): ∀ (a : Iota), Eq (Iff (cp2 a) (Exists (ra_Px5 a))) True % 4.37/4.54 Clause #359 (by clausification #[357]): ∀ (a : Iota), Or (Eq (cp2 a) False) (Eq (Exists (ra_Px5 a)) True) % 4.37/4.54 Clause #361 (by clausification #[359]): ∀ (a a_1 : Iota), Or (Eq (cp2 a) False) (Eq (ra_Px5 a (skS.0 2 a a_1)) True) % 4.37/4.54 Clause #374 (by betaEtaReduce #[45]): Eq (∀ (X : Iota), Iff (cp2xcomp X) (Not (Exists (ra_Px5 X)))) True % 4.37/4.54 Clause #375 (by clausification #[374]): ∀ (a : Iota), Eq (Iff (cp2xcomp a) (Not (Exists (ra_Px5 a)))) True % 4.37/4.54 Clause #377 (by clausification #[375]): ∀ (a : Iota), Or (Eq (cp2xcomp a) False) (Eq (Not (Exists (ra_Px5 a))) True) % 4.37/4.54 Clause #382 (by clausification #[377]): ∀ (a : Iota), Or (Eq (cp2xcomp a) False) (Eq (Exists (ra_Px5 a)) False) % 4.37/4.54 Clause #383 (by clausification #[382]): ∀ (a a_1 : Iota), Or (Eq (cp2xcomp a) False) (Eq (ra_Px5 a a_1) False) % 4.37/4.54 Clause #443 (by clausification #[54]): ∀ (a : Iota), % 4.37/4.54 Eq % 4.37/4.54 (Iff (ca_Ax14 a) % 4.37/4.54 (And (Exists fun Y => And (rr a Y) (cp1 Y)) (∀ (Y0 Y1 : Iota), And (rr a Y0) (rr a Y1) → Eq Y0 Y1))) % 4.37/4.54 True % 4.37/4.54 Clause #445 (by clausification #[443]): ∀ (a : Iota), % 4.37/4.54 Or (Eq (ca_Ax14 a) False) % 4.37/4.54 (Eq (And (Exists fun Y => And (rr a Y) (cp1 Y)) (∀ (Y0 Y1 : Iota), And (rr a Y0) (rr a Y1) → Eq Y0 Y1)) True) % 4.37/4.54 Clause #473 (by clausification #[55]): ∀ (a : Iota), Eq (Iff (ca_Cx1 a) (And (And (And (cp2xcomp a) (cp5xcomp a)) (cp3xcomp a)) (cp4xcomp a))) True % 4.37/4.54 Clause #475 (by clausification #[473]): ∀ (a : Iota), Or (Eq (ca_Cx1 a) False) (Eq (And (And (And (cp2xcomp a) (cp5xcomp a)) (cp3xcomp a)) (cp4xcomp a)) True) % 4.37/4.54 Clause #514 (by clausification #[340]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cp2 a) True) % 4.37/4.54 Clause #515 (by clausification #[340]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rinvR a Y) (ca_Ax14 Y)) True) % 4.37/4.54 Clause #516 (by superposition #[514, 65]): Or (Eq (cp2 i2003_11_14_17_21_04740) True) (Eq False True) % 4.37/4.54 Clause #517 (by clausification #[516]): Eq (cp2 i2003_11_14_17_21_04740) True % 4.37/4.54 Clause #520 (by superposition #[517, 361]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px5 i2003_11_14_17_21_04740 (skS.0 2 i2003_11_14_17_21_04740 a)) True) % 4.37/4.54 Clause #554 (by clausification #[445]): ∀ (a : Iota), Or (Eq (ca_Ax14 a) False) (Eq (∀ (Y0 Y1 : Iota), And (rr a Y0) (rr a Y1) → Eq Y0 Y1) True) % 4.40/4.56 Clause #555 (by clausification #[445]): ∀ (a : Iota), Or (Eq (ca_Ax14 a) False) (Eq (Exists fun Y => And (rr a Y) (cp1 Y)) True) % 4.40/4.56 Clause #556 (by clausification #[554]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax14 a) False) (Eq (∀ (Y1 : Iota), And (rr a a_1) (rr a Y1) → Eq a_1 Y1) True) % 4.40/4.56 Clause #557 (by clausification #[556]): ∀ (a a_1 a_2 : Iota), Or (Eq (ca_Ax14 a) False) (Eq (And (rr a a_1) (rr a a_2) → Eq a_1 a_2) True) % 4.40/4.56 Clause #558 (by clausification #[557]): ∀ (a a_1 a_2 : Iota), Or (Eq (ca_Ax14 a) False) (Or (Eq (And (rr a a_1) (rr a a_2)) False) (Eq (Eq a_1 a_2) True)) % 4.40/4.56 Clause #559 (by clausification #[558]): ∀ (a a_1 a_2 : Iota), % 4.40/4.56 Or (Eq (ca_Ax14 a) False) (Or (Eq (Eq a_1 a_2) True) (Or (Eq (rr a a_1) False) (Eq (rr a a_2) False))) % 4.40/4.56 Clause #560 (by clausification #[559]): ∀ (a a_1 a_2 : Iota), Or (Eq (ca_Ax14 a) False) (Or (Eq (rr a a_1) False) (Or (Eq (rr a a_2) False) (Eq a_1 a_2))) % 4.40/4.56 Clause #570 (by clausification #[555]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax14 a) False) (Eq (And (rr a (skS.0 16 a a_1)) (cp1 (skS.0 16 a a_1))) True) % 4.40/4.56 Clause #571 (by clausification #[570]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax14 a) False) (Eq (cp1 (skS.0 16 a a_1)) True) % 4.40/4.56 Clause #572 (by clausification #[570]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax14 a) False) (Eq (rr a (skS.0 16 a a_1)) True) % 4.40/4.56 Clause #573 (by clausification #[515]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rinvR a (skS.0 17 a a_1)) (ca_Ax14 (skS.0 17 a a_1))) True) % 4.40/4.56 Clause #574 (by clausification #[573]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (ca_Ax14 (skS.0 17 a a_1)) True) % 4.40/4.56 Clause #575 (by clausification #[573]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rinvR a (skS.0 17 a a_1)) True) % 4.40/4.56 Clause #576 (by superposition #[574, 65]): ∀ (a : Iota), Or (Eq (ca_Ax14 (skS.0 17 i2003_11_14_17_21_04740 a)) True) (Eq False True) % 4.40/4.56 Clause #577 (by clausification #[576]): ∀ (a : Iota), Eq (ca_Ax14 (skS.0 17 i2003_11_14_17_21_04740 a)) True % 4.40/4.56 Clause #578 (by superposition #[577, 560]): ∀ (a a_1 a_2 : Iota), % 4.40/4.56 Or (Eq True False) % 4.40/4.56 (Or (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) a_1) False) % 4.40/4.56 (Or (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) a_2) False) (Eq a_1 a_2))) % 4.40/4.56 Clause #579 (by superposition #[577, 571]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (cp1 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True) % 4.40/4.56 Clause #580 (by clausification #[520]): ∀ (a : Iota), Eq (ra_Px5 i2003_11_14_17_21_04740 (skS.0 2 i2003_11_14_17_21_04740 a)) True % 4.40/4.56 Clause #593 (by superposition #[575, 65]): ∀ (a : Iota), Or (Eq (rinvR i2003_11_14_17_21_04740 (skS.0 17 i2003_11_14_17_21_04740 a)) True) (Eq False True) % 4.40/4.56 Clause #594 (by clausification #[593]): ∀ (a : Iota), Eq (rinvR i2003_11_14_17_21_04740 (skS.0 17 i2003_11_14_17_21_04740 a)) True % 4.40/4.56 Clause #595 (by superposition #[594, 337]): ∀ (a : Iota), Or (Eq True False) (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) i2003_11_14_17_21_04740) True) % 4.40/4.56 Clause #596 (by clausification #[595]): ∀ (a : Iota), Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) i2003_11_14_17_21_04740) True % 4.40/4.56 Clause #603 (by clausification #[475]): ∀ (a : Iota), Or (Eq (ca_Cx1 a) False) (Eq (And (And (cp2xcomp a) (cp5xcomp a)) (cp3xcomp a)) True) % 4.40/4.56 Clause #605 (by clausification #[603]): ∀ (a : Iota), Or (Eq (ca_Cx1 a) False) (Eq (And (cp2xcomp a) (cp5xcomp a)) True) % 4.40/4.56 Clause #607 (by clausification #[605]): ∀ (a : Iota), Or (Eq (ca_Cx1 a) False) (Eq (cp2xcomp a) True) % 4.40/4.56 Clause #608 (by superposition #[572, 577]): ∀ (a a_1 : Iota), % 4.40/4.56 Or (Eq True False) % 4.40/4.56 (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True) % 4.40/4.56 Clause #613 (by clausification #[579]): ∀ (a a_1 : Iota), Eq (cp1 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True % 4.40/4.56 Clause #614 (by superposition #[613, 73]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (ca_Cx1 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True) % 4.40/4.56 Clause #615 (by clausification #[614]): ∀ (a a_1 : Iota), Eq (ca_Cx1 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True % 4.40/4.57 Clause #620 (by superposition #[615, 607]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (cp2xcomp (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True) % 4.40/4.57 Clause #621 (by clausification #[620]): ∀ (a a_1 : Iota), Eq (cp2xcomp (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True % 4.40/4.57 Clause #622 (by superposition #[621, 383]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (ra_Px5 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1) a_2) False) % 4.40/4.57 Clause #625 (by clausification #[578]): ∀ (a a_1 a_2 : Iota), % 4.40/4.57 Or (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) a_1) False) % 4.40/4.57 (Or (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) a_2) False) (Eq a_1 a_2)) % 4.40/4.57 Clause #626 (by superposition #[625, 596]): ∀ (a a_1 : Iota), % 4.40/4.57 Or (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) a_1) False) (Or (Eq i2003_11_14_17_21_04740 a_1) (Eq False True)) % 4.40/4.57 Clause #627 (by clausification #[626]): ∀ (a a_1 : Iota), Or (Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) a_1) False) (Eq i2003_11_14_17_21_04740 a_1) % 4.40/4.57 Clause #637 (by clausification #[622]): ∀ (a a_1 a_2 : Iota), Eq (ra_Px5 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1) a_2) False % 4.40/4.57 Clause #643 (by clausification #[608]): ∀ (a a_1 : Iota), Eq (rr (skS.0 17 i2003_11_14_17_21_04740 a) (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) True % 4.40/4.57 Clause #645 (by superposition #[643, 627]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq i2003_11_14_17_21_04740 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1)) % 4.40/4.57 Clause #650 (by clausification #[645]): ∀ (a a_1 : Iota), Eq i2003_11_14_17_21_04740 (skS.0 16 (skS.0 17 i2003_11_14_17_21_04740 a) a_1) % 4.40/4.57 Clause #654 (by backward demodulation #[650, 637]): ∀ (a : Iota), Eq (ra_Px5 i2003_11_14_17_21_04740 a) False % 4.40/4.57 Clause #664 (by superposition #[654, 580]): Eq False True % 4.40/4.57 Clause #666 (by clausification #[664]): False % 4.40/4.57 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------