%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS099+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.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 7.14s 7.43s % Output : Proof 7.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.21 % Problem : KRS099+1 : TPTP v9.2.0. Released v3.1.0. % 0.11/0.23 % Command : duper %s % 0.13/0.44 % Computer : n005.cluster.edu % 0.13/0.44 % Model : x86_64 x86_64 % 0.13/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.44 % Memory : 8042.1875MB % 0.13/0.44 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.44 % CPULimit : 300 % 0.13/0.44 % WCLimit : 300 % 0.13/0.44 % DateTime : Thu Oct 2 10:23:23 EDT 2025 % 0.13/0.44 % CPUTime : % 7.14/7.43 SZS status Theorem for theBenchmark.p % 7.14/7.43 SZS output start Proof for theBenchmark.p % 7.14/7.43 Clause #12 (by assumption #[]): Eq % 7.14/7.43 (∀ (X : Iota), % 7.14/7.43 Iff (cUnsatisfiable X) % 7.14/7.43 (And % 7.14/7.43 (And % 7.14/7.43 (And % 7.14/7.43 (Exists fun Y0 => % 7.14/7.43 Exists fun Y1 => % 7.14/7.43 Exists fun Y2 => % 7.14/7.43 And (And (And (And (And (rtt X Y0) (rtt X Y1)) (rtt X Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 7.14/7.43 (∀ (Y : Iota), rtt X Y → ca Y)) % 7.14/7.43 (∀ (Y0 Y1 : Iota), And (rtt X Y0) (rtt X Y1) → Eq Y0 Y1)) % 7.14/7.43 (∀ (Y0 Y1 : Iota), And (rtt X Y0) (rtt X Y1) → Eq Y0 Y1))) % 7.14/7.43 True % 7.14/7.43 Clause #15 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_20_29215) True % 7.14/7.43 Clause #92 (by clausification #[12]): ∀ (a : Iota), % 7.14/7.43 Eq % 7.14/7.43 (Iff (cUnsatisfiable a) % 7.14/7.43 (And % 7.14/7.43 (And % 7.14/7.43 (And % 7.14/7.43 (Exists fun Y0 => % 7.14/7.43 Exists fun Y1 => % 7.14/7.43 Exists fun Y2 => % 7.14/7.43 And (And (And (And (And (rtt a Y0) (rtt a Y1)) (rtt a Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 7.14/7.43 (∀ (Y : Iota), rtt a Y → ca Y)) % 7.14/7.43 (∀ (Y0 Y1 : Iota), And (rtt a Y0) (rtt a Y1) → Eq Y0 Y1)) % 7.14/7.43 (∀ (Y0 Y1 : Iota), And (rtt a Y0) (rtt a Y1) → Eq Y0 Y1))) % 7.14/7.43 True % 7.14/7.43 Clause #94 (by clausification #[92]): ∀ (a : Iota), % 7.14/7.43 Or (Eq (cUnsatisfiable a) False) % 7.14/7.43 (Eq % 7.14/7.43 (And % 7.14/7.43 (And % 7.14/7.43 (And % 7.14/7.43 (Exists fun Y0 => % 7.14/7.43 Exists fun Y1 => % 7.14/7.43 Exists fun Y2 => % 7.14/7.43 And (And (And (And (And (rtt a Y0) (rtt a Y1)) (rtt a Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 7.14/7.43 (∀ (Y : Iota), rtt a Y → ca Y)) % 7.14/7.43 (∀ (Y0 Y1 : Iota), And (rtt a Y0) (rtt a Y1) → Eq Y0 Y1)) % 7.14/7.43 (∀ (Y0 Y1 : Iota), And (rtt a Y0) (rtt a Y1) → Eq Y0 Y1)) % 7.14/7.43 True) % 7.14/7.43 Clause #129 (by clausification #[94]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (∀ (Y0 Y1 : Iota), And (rtt a Y0) (rtt a Y1) → Eq Y0 Y1) True) % 7.14/7.43 Clause #130 (by clausification #[94]): ∀ (a : Iota), % 7.14/7.43 Or (Eq (cUnsatisfiable a) False) % 7.14/7.43 (Eq % 7.14/7.43 (And % 7.14/7.43 (And % 7.14/7.43 (Exists fun Y0 => % 7.14/7.43 Exists fun Y1 => % 7.14/7.43 Exists fun Y2 => % 7.14/7.43 And (And (And (And (And (rtt a Y0) (rtt a Y1)) (rtt a Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 7.14/7.43 (∀ (Y : Iota), rtt a Y → ca Y)) % 7.14/7.43 (∀ (Y0 Y1 : Iota), And (rtt a Y0) (rtt a Y1) → Eq Y0 Y1)) % 7.14/7.43 True) % 7.14/7.43 Clause #131 (by clausification #[129]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (∀ (Y1 : Iota), And (rtt a a_1) (rtt a Y1) → Eq a_1 Y1) True) % 7.14/7.43 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rtt a a_1) (rtt a a_2) → Eq a_1 a_2) True) % 7.14/7.43 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 7.14/7.43 Or (Eq (cUnsatisfiable a) False) (Or (Eq (And (rtt a a_1) (rtt a a_2)) False) (Eq (Eq a_1 a_2) True)) % 7.14/7.43 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), % 7.14/7.43 Or (Eq (cUnsatisfiable a) False) (Or (Eq (Eq a_1 a_2) True) (Or (Eq (rtt a a_1) False) (Eq (rtt a a_2) False))) % 7.14/7.43 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), % 7.14/7.43 Or (Eq (cUnsatisfiable a) False) (Or (Eq (rtt a a_1) False) (Or (Eq (rtt a a_2) False) (Eq a_1 a_2))) % 7.14/7.43 Clause #136 (by superposition #[135, 15]): ∀ (a a_1 : Iota), % 7.14/7.43 Or (Eq (rtt i2003_11_14_17_20_29215 a) False) % 7.14/7.43 (Or (Eq (rtt i2003_11_14_17_20_29215 a_1) False) (Or (Eq a a_1) (Eq False True))) % 7.14/7.43 Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota), % 7.14/7.43 Or (Eq (rtt i2003_11_14_17_20_29215 a) False) (Or (Eq (rtt i2003_11_14_17_20_29215 a_1) False) (Eq a a_1)) % 7.14/7.43 Clause #138 (by clausification #[130]): ∀ (a : Iota), % 7.14/7.43 Or (Eq (cUnsatisfiable a) False) % 7.14/7.43 (Eq % 7.14/7.43 (And % 7.14/7.43 (Exists fun Y0 => % 7.14/7.43 Exists fun Y1 => % 7.14/7.43 Exists fun Y2 => % 7.14/7.43 And (And (And (And (And (rtt a Y0) (rtt a Y1)) (rtt a Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 7.14/7.43 (∀ (Y : Iota), rtt a Y → ca Y)) % 7.14/7.43 True) % 7.14/7.43 Clause #140 (by clausification #[138]): ∀ (a : Iota), % 7.14/7.43 Or (Eq (cUnsatisfiable a) False) % 7.14/7.43 (Eq % 7.14/7.43 (Exists fun Y0 => % 7.14/7.43 Exists fun Y1 => % 7.14/7.43 Exists fun Y2 => % 7.19/7.48 And (And (And (And (And (rtt a Y0) (rtt a Y1)) (rtt a Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 7.19/7.48 True) % 7.19/7.48 Clause #162 (by clausification #[140]): ∀ (a a_1 : Iota), % 7.19/7.48 Or (Eq (cUnsatisfiable a) False) % 7.19/7.48 (Eq % 7.19/7.48 (Exists fun Y1 => % 7.19/7.48 Exists fun Y2 => % 7.19/7.48 And % 7.19/7.48 (And (And (And (And (rtt a (skS.0 5 a a_1)) (rtt a Y1)) (rtt a Y2)) (Ne (skS.0 5 a a_1) Y1)) % 7.19/7.48 (Ne (skS.0 5 a a_1) Y2)) % 7.19/7.48 (Ne Y1 Y2)) % 7.19/7.48 True) % 7.19/7.48 Clause #163 (by clausification #[162]): ∀ (a a_1 a_2 : Iota), % 7.19/7.48 Or (Eq (cUnsatisfiable a) False) % 7.19/7.48 (Eq % 7.19/7.48 (Exists fun Y2 => % 7.19/7.48 And % 7.19/7.48 (And % 7.19/7.48 (And (And (And (rtt a (skS.0 5 a a_1)) (rtt a (skS.0 6 a a_1 a_2))) (rtt a Y2)) % 7.19/7.48 (Ne (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 7.19/7.48 (Ne (skS.0 5 a a_1) Y2)) % 7.19/7.48 (Ne (skS.0 6 a a_1 a_2) Y2)) % 7.19/7.48 True) % 7.19/7.48 Clause #164 (by clausification #[163]): ∀ (a a_1 a_2 a_3 : Iota), % 7.19/7.48 Or (Eq (cUnsatisfiable a) False) % 7.19/7.48 (Eq % 7.19/7.48 (And % 7.19/7.48 (And % 7.19/7.48 (And (And (And (rtt a (skS.0 5 a a_1)) (rtt a (skS.0 6 a a_1 a_2))) (rtt a (skS.0 7 a a_1 a_2 a_3))) % 7.19/7.48 (Ne (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 7.19/7.48 (Ne (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 7.19/7.48 (Ne (skS.0 6 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3))) % 7.19/7.48 True) % 7.19/7.48 Clause #166 (by clausification #[164]): ∀ (a a_1 a_2 a_3 : Iota), % 7.19/7.48 Or (Eq (cUnsatisfiable a) False) % 7.19/7.48 (Eq % 7.19/7.48 (And % 7.19/7.48 (And (And (And (rtt a (skS.0 5 a a_1)) (rtt a (skS.0 6 a a_1 a_2))) (rtt a (skS.0 7 a a_1 a_2 a_3))) % 7.19/7.48 (Ne (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 7.19/7.48 (Ne (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 7.19/7.48 True) % 7.19/7.48 Clause #291 (by clausification #[166]): ∀ (a a_1 a_2 a_3 : Iota), % 7.19/7.48 Or (Eq (cUnsatisfiable a) False) % 7.19/7.48 (Eq % 7.19/7.48 (And (And (And (rtt a (skS.0 5 a a_1)) (rtt a (skS.0 6 a a_1 a_2))) (rtt a (skS.0 7 a a_1 a_2 a_3))) % 7.19/7.48 (Ne (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 7.19/7.48 True) % 7.19/7.48 Clause #295 (by clausification #[291]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Ne (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) True) % 7.19/7.48 Clause #296 (by clausification #[291]): ∀ (a a_1 a_2 a_3 : Iota), % 7.19/7.48 Or (Eq (cUnsatisfiable a) False) % 7.19/7.48 (Eq (And (And (rtt a (skS.0 5 a a_1)) (rtt a (skS.0 6 a a_1 a_2))) (rtt a (skS.0 7 a a_1 a_2 a_3))) True) % 7.19/7.48 Clause #297 (by clausification #[295]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Ne (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 7.19/7.48 Clause #298 (by superposition #[297, 15]): ∀ (a a_1 : Iota), Or (Ne (skS.0 5 i2003_11_14_17_20_29215 a) (skS.0 6 i2003_11_14_17_20_29215 a a_1)) (Eq False True) % 7.19/7.48 Clause #299 (by clausification #[298]): ∀ (a a_1 : Iota), Ne (skS.0 5 i2003_11_14_17_20_29215 a) (skS.0 6 i2003_11_14_17_20_29215 a a_1) % 7.19/7.48 Clause #301 (by clausification #[296]): ∀ (a a_1 a_2 : Iota), % 7.19/7.48 Or (Eq (cUnsatisfiable a) False) (Eq (And (rtt a (skS.0 5 a a_1)) (rtt a (skS.0 6 a a_1 a_2))) True) % 7.19/7.48 Clause #325 (by clausification #[301]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rtt a (skS.0 6 a a_1 a_2)) True) % 7.19/7.48 Clause #326 (by clausification #[301]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rtt a (skS.0 5 a a_1)) True) % 7.19/7.48 Clause #327 (by superposition #[325, 15]): ∀ (a a_1 : Iota), Or (Eq (rtt i2003_11_14_17_20_29215 (skS.0 6 i2003_11_14_17_20_29215 a a_1)) True) (Eq False True) % 7.19/7.48 Clause #328 (by superposition #[326, 15]): ∀ (a : Iota), Or (Eq (rtt i2003_11_14_17_20_29215 (skS.0 5 i2003_11_14_17_20_29215 a)) True) (Eq False True) % 7.19/7.48 Clause #329 (by clausification #[328]): ∀ (a : Iota), Eq (rtt i2003_11_14_17_20_29215 (skS.0 5 i2003_11_14_17_20_29215 a)) True % 7.19/7.48 Clause #339 (by clausification #[327]): ∀ (a a_1 : Iota), Eq (rtt i2003_11_14_17_20_29215 (skS.0 6 i2003_11_14_17_20_29215 a a_1)) True % 7.19/7.48 Clause #340 (by superposition #[339, 137]): ∀ (a a_1 a_2 : Iota), % 7.19/7.48 Or (Eq True False) (Or (Eq (rtt i2003_11_14_17_20_29215 a) False) (Eq (skS.0 6 i2003_11_14_17_20_29215 a_1 a_2) a)) % 7.19/7.48 Clause #355 (by clausification #[340]): ∀ (a a_1 a_2 : Iota), Or (Eq (rtt i2003_11_14_17_20_29215 a) False) (Eq (skS.0 6 i2003_11_14_17_20_29215 a_1 a_2) a) % 7.19/7.48 Clause #357 (by superposition #[355, 329]): ∀ (a a_1 a_2 : Iota), % 7.19/7.49 Or (Eq (skS.0 6 i2003_11_14_17_20_29215 a a_1) (skS.0 5 i2003_11_14_17_20_29215 a_2)) (Eq False True) % 7.19/7.49 Clause #360 (by clausification #[357]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 6 i2003_11_14_17_20_29215 a a_1) (skS.0 5 i2003_11_14_17_20_29215 a_2) % 7.19/7.49 Clause #361 (by backward contextual literal cutting #[360, 299]): False % 7.19/7.49 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------