%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS089+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:36 PM UTC 2025 % Result : Unsatisfiable 70.96s 71.17s % Output : Proof 71.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS089+1 : TPTP v9.2.0. Released v3.1.0. % 0.07/0.13 % Command : duper %s % 0.14/0.34 % Computer : n020.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 10:17:38 EDT 2025 % 0.14/0.34 % CPUTime : % 70.96/71.17 SZS status Theorem for theBenchmark.p % 70.96/71.17 SZS output start Proof for theBenchmark.p % 70.96/71.17 Clause #11 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 70.96/71.17 Clause #13 (by assumption #[]): Eq % 70.96/71.17 (∀ (X : Iota), % 70.96/71.17 cUnsatisfiable X → % 70.96/71.17 Exists fun Y0 => % 70.96/71.17 Exists fun Y1 => % 70.96/71.17 Exists fun Y2 => And (And (And (And (And (rr X Y0) (rr X Y1)) (rr X Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 70.96/71.17 True % 70.96/71.17 Clause #14 (by assumption #[]): Eq (∀ (X : Iota), cowlThing X → Exists fun Y => And (rp X Y) (Eq Y ispy)) True % 70.96/71.17 Clause #15 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rp X Y) (rinvP Y X)) True % 70.96/71.17 Clause #16 (by assumption #[]): Eq % 70.96/71.17 (∀ (X0 X1 X2 : Iota), % 70.96/71.17 And (And (rinvP ispy X0) (rinvP ispy X1)) (rinvP ispy X2) → Or (Or (Eq X0 X1) (Eq X0 X2)) (Eq X1 X2)) % 70.96/71.17 True % 70.96/71.17 Clause #18 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_19_53168) True % 70.96/71.17 Clause #49 (by clausification #[11]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 70.96/71.17 Clause #51 (by clausification #[49]): ∀ (a : Iota), Eq (cowlThing a) True % 70.96/71.17 Clause #99 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rp a Y) (rinvP Y a)) True % 70.96/71.17 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), Eq (Iff (rp a a_1) (rinvP a_1 a)) True % 70.96/71.17 Clause #102 (by clausification #[100]): ∀ (a a_1 : Iota), Or (Eq (rp a a_1) False) (Eq (rinvP a_1 a) True) % 70.96/71.17 Clause #103 (by clausification #[14]): ∀ (a : Iota), Eq (cowlThing a → Exists fun Y => And (rp a Y) (Eq Y ispy)) True % 70.96/71.17 Clause #104 (by clausification #[103]): ∀ (a : Iota), Or (Eq (cowlThing a) False) (Eq (Exists fun Y => And (rp a Y) (Eq Y ispy)) True) % 70.96/71.17 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Or (Eq (cowlThing a) False) (Eq (And (rp a (skS.0 0 a a_1)) (Eq (skS.0 0 a a_1) ispy)) True) % 70.96/71.17 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), Or (Eq (cowlThing a) False) (Eq (Eq (skS.0 0 a a_1) ispy) True) % 70.96/71.17 Clause #107 (by clausification #[105]): ∀ (a a_1 : Iota), Or (Eq (cowlThing a) False) (Eq (rp a (skS.0 0 a a_1)) True) % 70.96/71.17 Clause #108 (by clausification #[106]): ∀ (a a_1 : Iota), Or (Eq (cowlThing a) False) (Eq (skS.0 0 a a_1) ispy) % 70.96/71.17 Clause #109 (by forward demodulation #[108, 51]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (skS.0 0 a a_1) ispy) % 70.96/71.17 Clause #110 (by clausification #[109]): ∀ (a a_1 : Iota), Eq (skS.0 0 a a_1) ispy % 70.96/71.17 Clause #111 (by forward demodulation #[107, 51]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (rp a (skS.0 0 a a_1)) True) % 70.96/71.17 Clause #112 (by clausification #[111]): ∀ (a a_1 : Iota), Eq (rp a (skS.0 0 a a_1)) True % 70.96/71.17 Clause #113 (by forward demodulation #[112, 110]): ∀ (a : Iota), Eq (rp a ispy) True % 70.96/71.17 Clause #114 (by superposition #[113, 102]): ∀ (a : Iota), Or (Eq True False) (Eq (rinvP ispy a) True) % 70.96/71.17 Clause #115 (by clausification #[114]): ∀ (a : Iota), Eq (rinvP ispy a) True % 70.96/71.17 Clause #117 (by clausification #[13]): ∀ (a : Iota), % 70.96/71.17 Eq % 70.96/71.17 (cUnsatisfiable a → % 70.96/71.17 Exists fun Y0 => % 70.96/71.17 Exists fun Y1 => % 70.96/71.17 Exists fun Y2 => And (And (And (And (And (rr a Y0) (rr a Y1)) (rr a Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 70.96/71.17 True % 70.96/71.17 Clause #118 (by clausification #[117]): ∀ (a : Iota), % 70.96/71.17 Or (Eq (cUnsatisfiable a) False) % 70.96/71.17 (Eq % 70.96/71.17 (Exists fun Y0 => % 70.96/71.17 Exists fun Y1 => % 70.96/71.17 Exists fun Y2 => And (And (And (And (And (rr a Y0) (rr a Y1)) (rr a Y2)) (Ne Y0 Y1)) (Ne Y0 Y2)) (Ne Y1 Y2)) % 70.96/71.17 True) % 70.96/71.17 Clause #119 (by clausification #[118]): ∀ (a a_1 : Iota), % 70.96/71.17 Or (Eq (cUnsatisfiable a) False) % 70.96/71.17 (Eq % 70.96/71.17 (Exists fun Y1 => % 70.96/71.17 Exists fun Y2 => % 70.96/71.17 And % 70.96/71.17 (And (And (And (And (rr a (skS.0 1 a a_1)) (rr a Y1)) (rr a Y2)) (Ne (skS.0 1 a a_1) Y1)) % 70.96/71.17 (Ne (skS.0 1 a a_1) Y2)) % 70.96/71.17 (Ne Y1 Y2)) % 70.96/71.17 True) % 70.96/71.17 Clause #120 (by clausification #[119]): ∀ (a a_1 a_2 : Iota), % 70.96/71.17 Or (Eq (cUnsatisfiable a) False) % 70.96/71.17 (Eq % 70.96/71.17 (Exists fun Y2 => % 70.96/71.17 And % 70.96/71.17 (And % 70.96/71.17 (And (And (And (rr a (skS.0 1 a a_1)) (rr a (skS.0 2 a a_1 a_2))) (rr a Y2)) % 70.96/71.17 (Ne (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 70.96/71.17 (Ne (skS.0 1 a a_1) Y2)) % 70.96/71.17 (Ne (skS.0 2 a a_1 a_2) Y2)) % 71.04/71.20 True) % 71.04/71.20 Clause #121 (by clausification #[120]): ∀ (a a_1 a_2 a_3 : Iota), % 71.04/71.20 Or (Eq (cUnsatisfiable a) False) % 71.04/71.20 (Eq % 71.04/71.20 (And % 71.04/71.20 (And % 71.04/71.20 (And (And (And (rr a (skS.0 1 a a_1)) (rr a (skS.0 2 a a_1 a_2))) (rr a (skS.0 3 a a_1 a_2 a_3))) % 71.04/71.20 (Ne (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 71.04/71.20 (Ne (skS.0 1 a a_1) (skS.0 3 a a_1 a_2 a_3))) % 71.04/71.20 (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 71.04/71.20 True) % 71.04/71.20 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) True) % 71.04/71.20 Clause #123 (by clausification #[121]): ∀ (a a_1 a_2 a_3 : Iota), % 71.04/71.20 Or (Eq (cUnsatisfiable a) False) % 71.04/71.20 (Eq % 71.04/71.20 (And % 71.04/71.20 (And (And (And (rr a (skS.0 1 a a_1)) (rr a (skS.0 2 a a_1 a_2))) (rr a (skS.0 3 a a_1 a_2 a_3))) % 71.04/71.20 (Ne (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 71.04/71.20 (Ne (skS.0 1 a a_1) (skS.0 3 a a_1 a_2 a_3))) % 71.04/71.20 True) % 71.04/71.20 Clause #124 (by clausification #[122]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cUnsatisfiable a) False) (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 71.04/71.20 Clause #125 (by superposition #[124, 18]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Ne (skS.0 2 i2003_11_14_17_19_53168 a a_1) (skS.0 3 i2003_11_14_17_19_53168 a a_1 a_2)) (Eq False True) % 71.04/71.20 Clause #126 (by clausification #[16]): ∀ (a : Iota), % 71.04/71.20 Eq % 71.04/71.20 (∀ (X1 X2 : Iota), % 71.04/71.20 And (And (rinvP ispy a) (rinvP ispy X1)) (rinvP ispy X2) → Or (Or (Eq a X1) (Eq a X2)) (Eq X1 X2)) % 71.04/71.20 True % 71.04/71.20 Clause #127 (by clausification #[126]): ∀ (a a_1 : Iota), % 71.04/71.20 Eq % 71.04/71.20 (∀ (X2 : Iota), % 71.04/71.20 And (And (rinvP ispy a) (rinvP ispy a_1)) (rinvP ispy X2) → Or (Or (Eq a a_1) (Eq a X2)) (Eq a_1 X2)) % 71.04/71.20 True % 71.04/71.20 Clause #128 (by clausification #[127]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Eq (And (And (rinvP ispy a) (rinvP ispy a_1)) (rinvP ispy a_2) → Or (Or (Eq a a_1) (Eq a a_2)) (Eq a_1 a_2)) True % 71.04/71.20 Clause #129 (by clausification #[128]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (And (And (rinvP ispy a) (rinvP ispy a_1)) (rinvP ispy a_2)) False) % 71.04/71.20 (Eq (Or (Or (Eq a a_1) (Eq a a_2)) (Eq a_1 a_2)) True) % 71.04/71.20 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (Or (Or (Eq a a_1) (Eq a a_2)) (Eq a_1 a_2)) True) % 71.04/71.20 (Or (Eq (And (rinvP ispy a) (rinvP ispy a_1)) False) (Eq (rinvP ispy a_2) False)) % 71.04/71.20 Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (And (rinvP ispy a) (rinvP ispy a_1)) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_2) False) (Or (Eq (Or (Eq a a_1) (Eq a a_2)) True) (Eq (Eq a_1 a_2) True))) % 71.04/71.20 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (rinvP ispy a) False) % 71.04/71.20 (Or (Eq (Or (Eq a_1 a_2) (Eq a_1 a)) True) % 71.04/71.20 (Or (Eq (Eq a_2 a) True) (Or (Eq (rinvP ispy a_1) False) (Eq (rinvP ispy a_2) False)))) % 71.04/71.20 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (rinvP ispy a) False) % 71.04/71.20 (Or (Eq (Eq a_1 a) True) % 71.04/71.20 (Or (Eq (rinvP ispy a_2) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_1) False) (Or (Eq (Eq a_2 a_1) True) (Eq (Eq a_2 a) True))))) % 71.04/71.20 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (rinvP ispy a) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_1) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_2) False) (Or (Eq (Eq a_1 a_2) True) (Or (Eq (Eq a_1 a) True) (Eq a_2 a))))) % 71.04/71.20 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (rinvP ispy a) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_1) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_2) False) (Or (Eq (Eq a_1 a) True) (Or (Eq a_2 a) (Eq a_1 a_2))))) % 71.04/71.20 Clause #136 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (rinvP ispy a) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_1) False) (Or (Eq (rinvP ispy a_2) False) (Or (Eq a_2 a) (Or (Eq a_1 a_2) (Eq a_1 a))))) % 71.04/71.20 Clause #137 (by superposition #[136, 115]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (rinvP ispy a) False) % 71.04/71.20 (Or (Eq (rinvP ispy a_1) False) (Or (Eq a_1 a_2) (Or (Eq a a_1) (Or (Eq a a_2) (Eq False True))))) % 71.04/71.20 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 71.04/71.20 Or (Eq (rinvP ispy a) False) (Or (Eq (rinvP ispy a_1) False) (Or (Eq a_1 a_2) (Or (Eq a a_1) (Eq a a_2)))) % 71.04/71.20 Clause #139 (by superposition #[138, 115]): ∀ (a a_1 a_2 : Iota), Or (Eq (rinvP ispy a) False) (Or (Eq a a_1) (Or (Eq a_2 a) (Or (Eq a_2 a_1) (Eq False True)))) % 71.24/71.44 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : Iota), Or (Eq (rinvP ispy a) False) (Or (Eq a a_1) (Or (Eq a_2 a) (Eq a_2 a_1))) % 71.24/71.44 Clause #141 (by superposition #[140, 115]): ∀ (a a_1 a_2 : Iota), Or (Eq a a_1) (Or (Eq a_2 a) (Or (Eq a_2 a_1) (Eq False True))) % 71.24/71.44 Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 : Iota), Or (Eq a a_1) (Or (Eq a_2 a) (Eq a_2 a_1)) % 71.24/71.44 Clause #179 (by clausification #[123]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Ne (skS.0 1 a a_1) (skS.0 3 a a_1 a_2 a_3)) True) % 71.24/71.44 Clause #180 (by clausification #[123]): ∀ (a a_1 a_2 a_3 : Iota), % 71.24/71.44 Or (Eq (cUnsatisfiable a) False) % 71.24/71.44 (Eq % 71.24/71.44 (And (And (And (rr a (skS.0 1 a a_1)) (rr a (skS.0 2 a a_1 a_2))) (rr a (skS.0 3 a a_1 a_2 a_3))) % 71.24/71.44 (Ne (skS.0 1 a a_1) (skS.0 2 a a_1 a_2))) % 71.24/71.44 True) % 71.24/71.44 Clause #181 (by clausification #[179]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cUnsatisfiable a) False) (Ne (skS.0 1 a a_1) (skS.0 3 a a_1 a_2 a_3)) % 71.24/71.44 Clause #182 (by superposition #[181, 18]): ∀ (a a_1 a_2 : Iota), % 71.24/71.44 Or (Ne (skS.0 1 i2003_11_14_17_19_53168 a) (skS.0 3 i2003_11_14_17_19_53168 a a_1 a_2)) (Eq False True) % 71.24/71.44 Clause #183 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), Ne (skS.0 2 i2003_11_14_17_19_53168 a a_1) (skS.0 3 i2003_11_14_17_19_53168 a a_1 a_2) % 71.24/71.44 Clause #184 (by superposition #[183, 142]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 71.24/71.44 Or (Eq a (skS.0 3 i2003_11_14_17_19_53168 a_1 a_2 a_3)) % 71.24/71.44 (Or (Eq a a_4) (Ne (skS.0 2 i2003_11_14_17_19_53168 a_1 a_2) a_4)) % 71.24/71.44 Clause #411 (by clausification #[180]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Ne (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) True) % 71.24/71.44 Clause #413 (by clausification #[411]): ∀ (a a_1 a_2 : Iota), Or (Eq (cUnsatisfiable a) False) (Ne (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)) % 71.24/71.44 Clause #414 (by superposition #[413, 18]): ∀ (a a_1 : Iota), Or (Ne (skS.0 1 i2003_11_14_17_19_53168 a) (skS.0 2 i2003_11_14_17_19_53168 a a_1)) (Eq False True) % 71.24/71.44 Clause #421 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), Ne (skS.0 1 i2003_11_14_17_19_53168 a) (skS.0 3 i2003_11_14_17_19_53168 a a_1 a_2) % 71.24/71.44 Clause #533 (by destructive equality resolution #[184]): ∀ (a a_1 a_2 a_3 : Iota), % 71.24/71.44 Or (Eq a (skS.0 3 i2003_11_14_17_19_53168 a_1 a_2 a_3)) (Eq a (skS.0 2 i2003_11_14_17_19_53168 a_1 a_2)) % 71.24/71.44 Clause #540 (by superposition #[533, 421]): ∀ (a a_1 a_2 : Iota), Or (Eq a (skS.0 2 i2003_11_14_17_19_53168 a_1 a_2)) (Ne (skS.0 1 i2003_11_14_17_19_53168 a_1) a) % 71.24/71.44 Clause #12273 (by clausification #[414]): ∀ (a a_1 : Iota), Ne (skS.0 1 i2003_11_14_17_19_53168 a) (skS.0 2 i2003_11_14_17_19_53168 a a_1) % 71.24/71.44 Clause #30069 (by destructive equality resolution #[540]): ∀ (a a_1 : Iota), Eq (skS.0 1 i2003_11_14_17_19_53168 a) (skS.0 2 i2003_11_14_17_19_53168 a a_1) % 71.24/71.44 Clause #30070 (by forward contextual literal cutting #[30069, 12273]): False % 71.24/71.44 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------