%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS097+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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:37 PM UTC 2025 % Result : Unsatisfiable 5.19s 5.44s % Output : Proof 5.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS097+1 : TPTP v9.2.0. Released v3.1.0. % 0.11/0.13 % Command : duper %s % 0.12/0.34 % Computer : n015.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:11:23 EDT 2025 % 0.12/0.34 % CPUTime : % 5.19/5.44 SZS status Theorem for theBenchmark.p % 5.19/5.44 SZS output start Proof for theBenchmark.p % 5.19/5.44 Clause #27 (by assumption #[]): Eq % 5.19/5.44 (∀ (X : Iota), % 5.19/5.44 Iff (cUnsatisfiable X) % 5.19/5.44 (And % 5.19/5.44 (And (And (Exists fun Y0 => rr X Y0) (Exists fun Y => And (rr X Y) (cd Y))) % 5.19/5.44 (Not (Exists fun Y0 => Exists fun Y1 => And (And (rr X Y0) (rr X Y1)) (Ne Y0 Y1)))) % 5.19/5.44 (Exists fun Y => And (rr X Y) (cc Y)))) % 5.19/5.44 True % 5.19/5.44 Clause #29 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_20_21603) True % 5.19/5.44 Clause #31 (by assumption #[]): Eq (∀ (X : Iota), Not (And (cd X) (cc X))) True % 5.19/5.44 Clause #194 (by clausification #[31]): ∀ (a : Iota), Eq (Not (And (cd a) (cc a))) True % 5.19/5.44 Clause #195 (by clausification #[194]): ∀ (a : Iota), Eq (And (cd a) (cc a)) False % 5.19/5.44 Clause #196 (by clausification #[195]): ∀ (a : Iota), Or (Eq (cd a) False) (Eq (cc a) False) % 5.19/5.44 Clause #238 (by betaEtaReduce #[27]): Eq % 5.19/5.44 (∀ (X : Iota), % 5.19/5.44 Iff (cUnsatisfiable X) % 5.19/5.44 (And % 5.19/5.44 (And (And (Exists (rr X)) (Exists fun Y => And (rr X Y) (cd Y))) % 5.19/5.44 (Not (Exists fun Y0 => Exists fun Y1 => And (And (rr X Y0) (rr X Y1)) (Ne Y0 Y1)))) % 5.19/5.44 (Exists fun Y => And (rr X Y) (cc Y)))) % 5.19/5.44 True % 5.19/5.44 Clause #239 (by clausification #[238]): ∀ (a : Iota), % 5.19/5.44 Eq % 5.19/5.44 (Iff (cUnsatisfiable a) % 5.19/5.44 (And % 5.19/5.44 (And (And (Exists (rr a)) (Exists fun Y => And (rr a Y) (cd Y))) % 5.19/5.44 (Not (Exists fun Y0 => Exists fun Y1 => And (And (rr a Y0) (rr a Y1)) (Ne Y0 Y1)))) % 5.19/5.44 (Exists fun Y => And (rr a Y) (cc Y)))) % 5.19/5.44 True % 5.19/5.44 Clause #241 (by clausification #[239]): ∀ (a : Iota), % 5.19/5.44 Or (Eq (cUnsatisfiable a) False) % 5.19/5.44 (Eq % 5.19/5.44 (And % 5.19/5.44 (And (And (Exists (rr a)) (Exists fun Y => And (rr a Y) (cd Y))) % 5.19/5.44 (Not (Exists fun Y0 => Exists fun Y1 => And (And (rr a Y0) (rr a Y1)) (Ne Y0 Y1)))) % 5.19/5.44 (Exists fun Y => And (rr a Y) (cc Y))) % 5.19/5.44 True) % 5.19/5.44 Clause #259 (by clausification #[241]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rr a Y) (cc Y)) True) % 5.19/5.44 Clause #260 (by clausification #[241]): ∀ (a : Iota), % 5.19/5.44 Or (Eq (cUnsatisfiable a) False) % 5.19/5.44 (Eq % 5.19/5.44 (And (And (Exists (rr a)) (Exists fun Y => And (rr a Y) (cd Y))) % 5.19/5.44 (Not (Exists fun Y0 => Exists fun Y1 => And (And (rr a Y0) (rr a Y1)) (Ne Y0 Y1)))) % 5.19/5.44 True) % 5.19/5.44 Clause #261 (by clausification #[259]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rr a (skS.0 2 a a_1)) (cc (skS.0 2 a a_1))) True) % 5.19/5.44 Clause #262 (by clausification #[261]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cc (skS.0 2 a a_1)) True) % 5.19/5.44 Clause #263 (by clausification #[261]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 2 a a_1)) True) % 5.19/5.44 Clause #264 (by superposition #[262, 29]): ∀ (a : Iota), Or (Eq (cc (skS.0 2 i2003_11_14_17_20_21603 a)) True) (Eq False True) % 5.19/5.44 Clause #265 (by clausification #[264]): ∀ (a : Iota), Eq (cc (skS.0 2 i2003_11_14_17_20_21603 a)) True % 5.19/5.44 Clause #267 (by clausification #[260]): ∀ (a : Iota), % 5.19/5.44 Or (Eq (cUnsatisfiable a) False) % 5.19/5.44 (Eq (Not (Exists fun Y0 => Exists fun Y1 => And (And (rr a Y0) (rr a Y1)) (Ne Y0 Y1))) True) % 5.19/5.44 Clause #268 (by clausification #[260]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (Exists (rr a)) (Exists fun Y => And (rr a Y) (cd Y))) True) % 5.19/5.44 Clause #269 (by clausification #[267]): ∀ (a : Iota), % 5.19/5.44 Or (Eq (cUnsatisfiable a) False) % 5.19/5.44 (Eq (Exists fun Y0 => Exists fun Y1 => And (And (rr a Y0) (rr a Y1)) (Ne Y0 Y1)) False) % 5.19/5.44 Clause #270 (by clausification #[269]): ∀ (a a_1 : Iota), % 5.19/5.44 Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y1 => And (And (rr a a_1) (rr a Y1)) (Ne a_1 Y1)) False) % 5.19/5.44 Clause #271 (by clausification #[270]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (And (rr a a_1) (rr a a_2)) (Ne a_1 a_2)) False) % 5.19/5.44 Clause #272 (by clausification #[271]): ∀ (a a_1 a_2 : Iota), % 5.19/5.44 Or (Eq (cUnsatisfiable a) False) (Or (Eq (And (rr a a_1) (rr a a_2)) False) (Eq (Ne a_1 a_2) False)) % 5.19/5.44 Clause #273 (by clausification #[272]): ∀ (a a_1 a_2 : Iota), % 5.19/5.44 Or (Eq (cUnsatisfiable a) False) (Or (Eq (Ne a_1 a_2) False) (Or (Eq (rr a a_1) False) (Eq (rr a a_2) False))) % 5.19/5.44 Clause #274 (by clausification #[273]): ∀ (a a_1 a_2 : Iota), % 5.29/5.47 Or (Eq (cUnsatisfiable a) False) (Or (Eq (rr a a_1) False) (Or (Eq (rr a a_2) False) (Eq a_1 a_2))) % 5.29/5.47 Clause #275 (by superposition #[274, 29]): ∀ (a a_1 : Iota), % 5.29/5.47 Or (Eq (rr i2003_11_14_17_20_21603 a) False) % 5.29/5.47 (Or (Eq (rr i2003_11_14_17_20_21603 a_1) False) (Or (Eq a a_1) (Eq False True))) % 5.29/5.47 Clause #276 (by clausification #[275]): ∀ (a a_1 : Iota), % 5.29/5.47 Or (Eq (rr i2003_11_14_17_20_21603 a) False) (Or (Eq (rr i2003_11_14_17_20_21603 a_1) False) (Eq a a_1)) % 5.29/5.47 Clause #279 (by superposition #[263, 29]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_20_21603 (skS.0 2 i2003_11_14_17_20_21603 a)) True) (Eq False True) % 5.29/5.47 Clause #280 (by clausification #[279]): ∀ (a : Iota), Eq (rr i2003_11_14_17_20_21603 (skS.0 2 i2003_11_14_17_20_21603 a)) True % 5.29/5.47 Clause #281 (by superposition #[280, 276]): ∀ (a a_1 : Iota), % 5.29/5.47 Or (Eq True False) (Or (Eq (rr i2003_11_14_17_20_21603 a) False) (Eq (skS.0 2 i2003_11_14_17_20_21603 a_1) a)) % 5.29/5.47 Clause #285 (by clausification #[281]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_20_21603 a) False) (Eq (skS.0 2 i2003_11_14_17_20_21603 a_1) a) % 5.29/5.47 Clause #287 (by clausification #[268]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rr a Y) (cd Y)) True) % 5.29/5.47 Clause #288 (by clausification #[268]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists (rr a)) True) % 5.29/5.47 Clause #289 (by clausification #[287]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rr a (skS.0 3 a a_1)) (cd (skS.0 3 a a_1))) True) % 5.29/5.47 Clause #290 (by clausification #[289]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (cd (skS.0 3 a a_1)) True) % 5.29/5.47 Clause #291 (by clausification #[289]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 3 a a_1)) True) % 5.29/5.47 Clause #292 (by superposition #[290, 29]): ∀ (a : Iota), Or (Eq (cd (skS.0 3 i2003_11_14_17_20_21603 a)) True) (Eq False True) % 5.29/5.47 Clause #293 (by clausification #[288]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rr a (skS.0 4 a a_1)) True) % 5.29/5.47 Clause #294 (by superposition #[293, 29]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_20_21603 (skS.0 4 i2003_11_14_17_20_21603 a)) True) (Eq False True) % 5.29/5.47 Clause #295 (by clausification #[292]): ∀ (a : Iota), Eq (cd (skS.0 3 i2003_11_14_17_20_21603 a)) True % 5.29/5.47 Clause #296 (by superposition #[295, 196]): ∀ (a : Iota), Or (Eq True False) (Eq (cc (skS.0 3 i2003_11_14_17_20_21603 a)) False) % 5.29/5.47 Clause #301 (by clausification #[296]): ∀ (a : Iota), Eq (cc (skS.0 3 i2003_11_14_17_20_21603 a)) False % 5.29/5.47 Clause #304 (by clausification #[294]): ∀ (a : Iota), Eq (rr i2003_11_14_17_20_21603 (skS.0 4 i2003_11_14_17_20_21603 a)) True % 5.29/5.47 Clause #305 (by superposition #[304, 276]): ∀ (a a_1 : Iota), % 5.29/5.47 Or (Eq True False) (Or (Eq (rr i2003_11_14_17_20_21603 a) False) (Eq (skS.0 4 i2003_11_14_17_20_21603 a_1) a)) % 5.29/5.47 Clause #306 (by superposition #[304, 285]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (skS.0 2 i2003_11_14_17_20_21603 a) (skS.0 4 i2003_11_14_17_20_21603 a_1)) % 5.29/5.47 Clause #310 (by superposition #[291, 29]): ∀ (a : Iota), Or (Eq (rr i2003_11_14_17_20_21603 (skS.0 3 i2003_11_14_17_20_21603 a)) True) (Eq False True) % 5.29/5.47 Clause #311 (by clausification #[310]): ∀ (a : Iota), Eq (rr i2003_11_14_17_20_21603 (skS.0 3 i2003_11_14_17_20_21603 a)) True % 5.29/5.47 Clause #321 (by clausification #[305]): ∀ (a a_1 : Iota), Or (Eq (rr i2003_11_14_17_20_21603 a) False) (Eq (skS.0 4 i2003_11_14_17_20_21603 a_1) a) % 5.29/5.47 Clause #324 (by superposition #[321, 311]): ∀ (a a_1 : Iota), Or (Eq (skS.0 4 i2003_11_14_17_20_21603 a) (skS.0 3 i2003_11_14_17_20_21603 a_1)) (Eq False True) % 5.29/5.47 Clause #328 (by clausification #[306]): ∀ (a a_1 : Iota), Eq (skS.0 2 i2003_11_14_17_20_21603 a) (skS.0 4 i2003_11_14_17_20_21603 a_1) % 5.29/5.47 Clause #329 (by superposition #[328, 265]): ∀ (a : Iota), Eq (cc (skS.0 4 i2003_11_14_17_20_21603 a)) True % 5.29/5.47 Clause #337 (by clausification #[324]): ∀ (a a_1 : Iota), Eq (skS.0 4 i2003_11_14_17_20_21603 a) (skS.0 3 i2003_11_14_17_20_21603 a_1) % 5.29/5.47 Clause #342 (by superposition #[337, 301]): ∀ (a : Iota), Eq (cc (skS.0 4 i2003_11_14_17_20_21603 a)) False % 5.29/5.47 Clause #344 (by superposition #[342, 329]): Eq False True % 5.29/5.47 Clause #347 (by clausification #[344]): False % 5.29/5.47 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------