%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS255+1 : TPTP v9.2.0. Bugfixed v5.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:50 PM UTC 2025 % Result : Theorem 134.13s 134.43s % Output : Proof 134.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.19 % Problem : KRS255+1 : TPTP v9.2.0. Bugfixed v5.4.0. % 0.11/0.20 % Command : duper %s % 0.14/0.46 % Computer : n016.cluster.edu % 0.14/0.46 % Model : x86_64 x86_64 % 0.14/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.46 % Memory : 8042.1875MB % 0.14/0.46 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.46 % CPULimit : 300 % 0.14/0.46 % WCLimit : 300 % 0.14/0.46 % DateTime : Thu Oct 2 10:18:08 EDT 2025 % 0.14/0.46 % CPUTime : % 134.13/134.43 SZS status Theorem for theBenchmark.p % 134.13/134.43 SZS output start Proof for theBenchmark.p % 134.13/134.43 Clause #1 (by assumption #[]): Eq (∀ (Ax C : Iota), Iff ((Exists fun I1 => model I1 Ax) → Exists fun I2 => model I2 C) (status Ax C sap)) True % 134.13/134.43 Clause #4 (by assumption #[]): Eq (∀ (Ax C : Iota), Iff (∀ (I1 : Iota), model I1 Ax → model I1 C) (status Ax C thm)) True % 134.13/134.43 Clause #19 (by assumption #[]): Eq (∀ (S1 S2 : Iota), Iff (Exists fun Ax => Exists fun C => And (status Ax C S1) (status Ax C S2)) (mighta S1 S2)) True % 134.13/134.43 Clause #26 (by assumption #[]): Eq (Exists fun F => ∀ (I : Iota), model I F) True % 134.13/134.43 Clause #32 (by assumption #[]): Eq (Not (mighta sap thm)) True % 134.13/134.43 Clause #33 (by clausification #[32]): Eq (mighta sap thm) False % 134.13/134.43 Clause #34 (by clausification #[26]): ∀ (a : Iota), Eq (∀ (I : Iota), model I (skS.0 0 a)) True % 134.13/134.43 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), Eq (model a (skS.0 0 a_1)) True % 134.13/134.43 Clause #63 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff ((Exists fun I1 => model I1 a) → Exists fun I2 => model I2 C) (status a C sap)) True % 134.13/134.43 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), Eq (Iff ((Exists fun I1 => model I1 a) → Exists fun I2 => model I2 a_1) (status a a_1 sap)) True % 134.13/134.43 Clause #66 (by clausification #[64]): ∀ (a a_1 : Iota), % 134.13/134.43 Or (Eq ((Exists fun I1 => model I1 a) → Exists fun I2 => model I2 a_1) False) (Eq (status a a_1 sap) True) % 134.13/134.43 Clause #70 (by clausification #[66]): ∀ (a a_1 : Iota), Or (Eq (status a a_1 sap) True) (Eq (Exists fun I1 => model I1 a) True) % 134.13/134.43 Clause #71 (by clausification #[66]): ∀ (a a_1 : Iota), Or (Eq (status a a_1 sap) True) (Eq (Exists fun I2 => model I2 a_1) False) % 134.13/134.43 Clause #72 (by clausification #[70]): ∀ (a a_1 a_2 : Iota), Or (Eq (status a a_1 sap) True) (Eq (model (skS.0 4 a a_2) a) True) % 134.13/134.43 Clause #80 (by clausification #[71]): ∀ (a a_1 a_2 : Iota), Or (Eq (status a a_1 sap) True) (Eq (model a_2 a_1) False) % 134.13/134.43 Clause #83 (by superposition #[80, 72]): ∀ (a a_1 a_2 : Iota), Or (Eq (status a a_1 sap) True) (Or (Eq (status a_1 a_2 sap) True) (Eq False True)) % 134.13/134.43 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 : Iota), Or (Eq (status a a_1 sap) True) (Eq (status a_1 a_2 sap) True) % 134.13/134.43 Clause #87 (by equality factoring #[84]): ∀ (a : Iota), Or (Ne True True) (Eq (status a a sap) True) % 134.13/134.43 Clause #88 (by clausification #[87]): ∀ (a : Iota), Or (Eq (status a a sap) True) (Or (Eq True False) (Eq True False)) % 134.13/134.43 Clause #90 (by clausification #[88]): ∀ (a : Iota), Or (Eq (status a a sap) True) (Eq True False) % 134.13/134.43 Clause #91 (by clausification #[90]): ∀ (a : Iota), Eq (status a a sap) True % 134.13/134.43 Clause #110 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (∀ (I1 : Iota), model I1 a → model I1 C) (status a C thm)) True % 134.13/134.43 Clause #111 (by clausification #[110]): ∀ (a a_1 : Iota), Eq (Iff (∀ (I1 : Iota), model I1 a → model I1 a_1) (status a a_1 thm)) True % 134.13/134.43 Clause #113 (by clausification #[111]): ∀ (a a_1 : Iota), Or (Eq (∀ (I1 : Iota), model I1 a → model I1 a_1) False) (Eq (status a a_1 thm) True) % 134.13/134.43 Clause #116 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), % 134.13/134.43 Or (Eq (status a a_1 thm) True) (Eq (Not (model (skS.0 6 a a_1 a_2) a → model (skS.0 6 a a_1 a_2) a_1)) True) % 134.13/134.43 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 : Iota), % 134.13/134.43 Or (Eq (status a a_1 thm) True) (Eq (model (skS.0 6 a a_1 a_2) a → model (skS.0 6 a a_1 a_2) a_1) False) % 134.13/134.43 Clause #119 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), Or (Eq (status a a_1 thm) True) (Eq (model (skS.0 6 a a_1 a_2) a_1) False) % 134.13/134.43 Clause #546 (by clausification #[19]): ∀ (a : Iota), % 134.13/134.43 Eq (∀ (S2 : Iota), Iff (Exists fun Ax => Exists fun C => And (status Ax C a) (status Ax C S2)) (mighta a S2)) True % 134.13/134.43 Clause #547 (by clausification #[546]): ∀ (a a_1 : Iota), Eq (Iff (Exists fun Ax => Exists fun C => And (status Ax C a) (status Ax C a_1)) (mighta a a_1)) True % 134.13/134.43 Clause #549 (by clausification #[547]): ∀ (a a_1 : Iota), % 134.13/134.43 Or (Eq (Exists fun Ax => Exists fun C => And (status Ax C a) (status Ax C a_1)) False) (Eq (mighta a a_1) True) % 134.13/134.43 Clause #1410 (by superposition #[119, 35]): ∀ (a a_1 : Iota), Or (Eq (status a (skS.0 0 a_1) thm) True) (Eq False True) % 134.38/134.69 Clause #1428 (by clausification #[1410]): ∀ (a a_1 : Iota), Eq (status a (skS.0 0 a_1) thm) True % 134.38/134.69 Clause #16131 (by clausification #[549]): ∀ (a a_1 a_2 : Iota), Or (Eq (mighta a a_1) True) (Eq (Exists fun C => And (status a_2 C a) (status a_2 C a_1)) False) % 134.38/134.69 Clause #16132 (by clausification #[16131]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (mighta a a_1) True) (Eq (And (status a_2 a_3 a) (status a_2 a_3 a_1)) False) % 134.38/134.69 Clause #16133 (by clausification #[16132]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (mighta a a_1) True) (Or (Eq (status a_2 a_3 a) False) (Eq (status a_2 a_3 a_1) False)) % 134.38/134.69 Clause #16330 (by superposition #[16133, 91]): ∀ (a a_1 : Iota), Or (Eq (mighta sap a) True) (Or (Eq (status a_1 a_1 a) False) (Eq False True)) % 134.38/134.69 Clause #18841 (by clausification #[16330]): ∀ (a a_1 : Iota), Or (Eq (mighta sap a) True) (Eq (status a_1 a_1 a) False) % 134.38/134.69 Clause #18850 (by superposition #[18841, 1428]): Or (Eq (mighta sap thm) True) (Eq False True) % 134.38/134.69 Clause #19227 (by clausification #[18850]): Eq (mighta sap thm) True % 134.38/134.69 Clause #19228 (by superposition #[19227, 33]): Eq True False % 134.38/134.69 Clause #19231 (by clausification #[19228]): False % 134.38/134.69 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------