%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS116+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n022.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:39 PM UTC 2025 % Result : Unsatisfiable 8.24s 8.43s % Output : Proof 8.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : KRS116+1 : TPTP v9.2.0. Released v3.1.0. % 0.07/0.15 % Command : duper %s % 0.14/0.38 % Computer : n022.cluster.edu % 0.14/0.38 % Model : x86_64 x86_64 % 0.14/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.38 % Memory : 8042.1875MB % 0.14/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.38 % CPULimit : 300 % 0.14/0.38 % WCLimit : 300 % 0.14/0.38 % DateTime : Thu Oct 2 10:19:38 EDT 2025 % 0.14/0.38 % CPUTime : % 8.24/8.43 SZS status Theorem for theBenchmark.p % 8.24/8.43 SZS output start Proof for theBenchmark.p % 8.24/8.43 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 8.24/8.43 Clause #2 (by assumption #[]): Eq (∀ (X : Iota), cUnsatisfiable X → ca X) True % 8.24/8.43 Clause #3 (by assumption #[]): Eq (∀ (X : Iota), cUnsatisfiable X → Exists fun Y => And (rs X Y) (ca_Ax2 Y)) True % 8.24/8.43 Clause #4 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca X) (Not (Exists fun Y => ra_Px1 X Y))) True % 8.24/8.43 Clause #5 (by assumption #[]): Eq (∀ (X : Iota), Iff (caxcomp X) (Exists fun Y0 => ra_Px1 X Y0)) True % 8.24/8.43 Clause #6 (by assumption #[]): Eq (∀ (X : Iota), Iff (cc X) (∀ (Y : Iota), rinvR X Y → ca_Vx7 Y)) True % 8.24/8.43 Clause #7 (by assumption #[]): Eq % 8.24/8.43 (∀ (X : Iota), % 8.24/8.43 Iff (ca_Ax2 X) % 8.24/8.43 (And % 8.24/8.43 (And % 8.24/8.43 (And % 8.24/8.43 (And (And (∀ (Y : Iota), rp X Y → ca_Vx3 Y) (∀ (Y : Iota), rp X Y → ca_Vx5 Y)) % 8.24/8.43 (∀ (Y : Iota), rr X Y → cc Y)) % 8.24/8.43 (Exists fun Y => And (rr X Y) (cowlThing Y))) % 8.24/8.43 (Exists fun Y => And (rp X Y) (cowlThing Y))) % 8.24/8.43 (∀ (Y : Iota), rp X Y → ca_Vx4 Y))) % 8.24/8.43 True % 8.24/8.43 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Vx3 X) (Exists fun Y => And (rr X Y) (cowlThing Y))) True % 8.24/8.43 Clause #9 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Vx4 X) (Exists fun Y => And (rp X Y) (cowlThing Y))) True % 8.24/8.43 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Vx5 X) (∀ (Y : Iota), rr X Y → cc Y)) True % 8.24/8.43 Clause #11 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Vx6 X) (∀ (Y : Iota), rinvS X Y → caxcomp Y)) True % 8.24/8.43 Clause #12 (by assumption #[]): Eq (∀ (X : Iota), Iff (ca_Vx7 X) (∀ (Y : Iota), rinvP X Y → ca_Vx6 Y)) True % 8.24/8.43 Clause #13 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvP X Y) (rp Y X)) True % 8.24/8.43 Clause #14 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvR X Y) (rr Y X)) True % 8.24/8.43 Clause #15 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rinvS X Y) (rs Y X)) True % 8.24/8.43 Clause #17 (by assumption #[]): Eq (cUnsatisfiable i2003_11_14_17_21_33997) True % 8.24/8.43 Clause #18 (by clausification #[2]): ∀ (a : Iota), Eq (cUnsatisfiable a → ca a) True % 8.24/8.43 Clause #19 (by clausification #[18]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (ca a) True) % 8.24/8.43 Clause #20 (by superposition #[19, 17]): Or (Eq (ca i2003_11_14_17_21_33997) True) (Eq False True) % 8.24/8.43 Clause #21 (by clausification #[20]): Eq (ca i2003_11_14_17_21_33997) True % 8.24/8.43 Clause #27 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 8.24/8.43 Clause #29 (by clausification #[27]): ∀ (a : Iota), Eq (cowlThing a) True % 8.24/8.43 Clause #36 (by clausification #[6]): ∀ (a : Iota), Eq (Iff (cc a) (∀ (Y : Iota), rinvR a Y → ca_Vx7 Y)) True % 8.24/8.43 Clause #38 (by clausification #[36]): ∀ (a : Iota), Or (Eq (cc a) False) (Eq (∀ (Y : Iota), rinvR a Y → ca_Vx7 Y) True) % 8.24/8.43 Clause #43 (by clausification #[38]): ∀ (a a_1 : Iota), Or (Eq (cc a) False) (Eq (rinvR a a_1 → ca_Vx7 a_1) True) % 8.24/8.43 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), Or (Eq (cc a) False) (Or (Eq (rinvR a a_1) False) (Eq (ca_Vx7 a_1) True)) % 8.24/8.43 Clause #45 (by clausification #[12]): ∀ (a : Iota), Eq (Iff (ca_Vx7 a) (∀ (Y : Iota), rinvP a Y → ca_Vx6 Y)) True % 8.24/8.43 Clause #47 (by clausification #[45]): ∀ (a : Iota), Or (Eq (ca_Vx7 a) False) (Eq (∀ (Y : Iota), rinvP a Y → ca_Vx6 Y) True) % 8.24/8.43 Clause #52 (by clausification #[3]): ∀ (a : Iota), Eq (cUnsatisfiable a → Exists fun Y => And (rs a Y) (ca_Ax2 Y)) True % 8.24/8.43 Clause #53 (by clausification #[52]): ∀ (a : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (Exists fun Y => And (rs a Y) (ca_Ax2 Y)) True) % 8.24/8.43 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (And (rs a (skS.0 2 a a_1)) (ca_Ax2 (skS.0 2 a a_1))) True) % 8.24/8.43 Clause #55 (by clausification #[54]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (ca_Ax2 (skS.0 2 a a_1)) True) % 8.24/8.43 Clause #56 (by clausification #[54]): ∀ (a a_1 : Iota), Or (Eq (cUnsatisfiable a) False) (Eq (rs a (skS.0 2 a a_1)) True) % 8.24/8.43 Clause #57 (by superposition #[55, 17]): ∀ (a : Iota), Or (Eq (ca_Ax2 (skS.0 2 i2003_11_14_17_21_33997 a)) True) (Eq False True) % 8.28/8.47 Clause #58 (by clausification #[47]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx7 a) False) (Eq (rinvP a a_1 → ca_Vx6 a_1) True) % 8.28/8.47 Clause #59 (by clausification #[58]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx7 a) False) (Or (Eq (rinvP a a_1) False) (Eq (ca_Vx6 a_1) True)) % 8.28/8.47 Clause #60 (by clausification #[11]): ∀ (a : Iota), Eq (Iff (ca_Vx6 a) (∀ (Y : Iota), rinvS a Y → caxcomp Y)) True % 8.28/8.47 Clause #62 (by clausification #[60]): ∀ (a : Iota), Or (Eq (ca_Vx6 a) False) (Eq (∀ (Y : Iota), rinvS a Y → caxcomp Y) True) % 8.28/8.47 Clause #67 (by clausification #[62]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx6 a) False) (Eq (rinvS a a_1 → caxcomp a_1) True) % 8.28/8.47 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx6 a) False) (Or (Eq (rinvS a a_1) False) (Eq (caxcomp a_1) True)) % 8.28/8.47 Clause #69 (by clausification #[10]): ∀ (a : Iota), Eq (Iff (ca_Vx5 a) (∀ (Y : Iota), rr a Y → cc Y)) True % 8.28/8.47 Clause #71 (by clausification #[69]): ∀ (a : Iota), Or (Eq (ca_Vx5 a) False) (Eq (∀ (Y : Iota), rr a Y → cc Y) True) % 8.28/8.47 Clause #76 (by clausification #[71]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx5 a) False) (Eq (rr a a_1 → cc a_1) True) % 8.28/8.47 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx5 a) False) (Or (Eq (rr a a_1) False) (Eq (cc a_1) True)) % 8.28/8.47 Clause #78 (by betaEtaReduce #[4]): Eq (∀ (X : Iota), Iff (ca X) (Not (Exists (ra_Px1 X)))) True % 8.28/8.47 Clause #79 (by clausification #[78]): ∀ (a : Iota), Eq (Iff (ca a) (Not (Exists (ra_Px1 a)))) True % 8.28/8.47 Clause #81 (by clausification #[79]): ∀ (a : Iota), Or (Eq (ca a) False) (Eq (Not (Exists (ra_Px1 a))) True) % 8.28/8.47 Clause #84 (by clausification #[81]): ∀ (a : Iota), Or (Eq (ca a) False) (Eq (Exists (ra_Px1 a)) False) % 8.28/8.47 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), Or (Eq (ca a) False) (Eq (ra_Px1 a a_1) False) % 8.28/8.47 Clause #86 (by superposition #[85, 21]): ∀ (a : Iota), Or (Eq (ra_Px1 i2003_11_14_17_21_33997 a) False) (Eq False True) % 8.28/8.47 Clause #87 (by clausification #[86]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_33997 a) False % 8.28/8.47 Clause #88 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvS a Y) (rs Y a)) True % 8.28/8.47 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), Eq (Iff (rinvS a a_1) (rs a_1 a)) True % 8.28/8.47 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), Or (Eq (rinvS a a_1) True) (Eq (rs a_1 a) False) % 8.28/8.47 Clause #93 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvR a Y) (rr Y a)) True % 8.28/8.47 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), Eq (Iff (rinvR a a_1) (rr a_1 a)) True % 8.28/8.47 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), Or (Eq (rinvR a a_1) True) (Eq (rr a_1 a) False) % 8.28/8.47 Clause #98 (by betaEtaReduce #[5]): Eq (∀ (X : Iota), Iff (caxcomp X) (Exists (ra_Px1 X))) True % 8.28/8.47 Clause #99 (by clausification #[98]): ∀ (a : Iota), Eq (Iff (caxcomp a) (Exists (ra_Px1 a))) True % 8.28/8.47 Clause #101 (by clausification #[99]): ∀ (a : Iota), Or (Eq (caxcomp a) False) (Eq (Exists (ra_Px1 a)) True) % 8.28/8.47 Clause #105 (by clausification #[101]): ∀ (a a_1 : Iota), Or (Eq (caxcomp a) False) (Eq (ra_Px1 a (skS.0 6 a a_1)) True) % 8.28/8.47 Clause #108 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rinvP a Y) (rp Y a)) True % 8.28/8.47 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (Iff (rinvP a a_1) (rp a_1 a)) True % 8.28/8.47 Clause #110 (by clausification #[109]): ∀ (a a_1 : Iota), Or (Eq (rinvP a a_1) True) (Eq (rp a_1 a) False) % 8.28/8.47 Clause #113 (by clausification #[7]): ∀ (a : Iota), % 8.28/8.47 Eq % 8.28/8.47 (Iff (ca_Ax2 a) % 8.28/8.47 (And % 8.28/8.47 (And % 8.28/8.47 (And % 8.28/8.47 (And (And (∀ (Y : Iota), rp a Y → ca_Vx3 Y) (∀ (Y : Iota), rp a Y → ca_Vx5 Y)) % 8.28/8.47 (∀ (Y : Iota), rr a Y → cc Y)) % 8.28/8.47 (Exists fun Y => And (rr a Y) (cowlThing Y))) % 8.28/8.47 (Exists fun Y => And (rp a Y) (cowlThing Y))) % 8.28/8.47 (∀ (Y : Iota), rp a Y → ca_Vx4 Y))) % 8.28/8.47 True % 8.28/8.47 Clause #115 (by clausification #[113]): ∀ (a : Iota), % 8.28/8.47 Or (Eq (ca_Ax2 a) False) % 8.28/8.47 (Eq % 8.28/8.47 (And % 8.28/8.47 (And % 8.28/8.47 (And % 8.28/8.47 (And (And (∀ (Y : Iota), rp a Y → ca_Vx3 Y) (∀ (Y : Iota), rp a Y → ca_Vx5 Y)) % 8.28/8.47 (∀ (Y : Iota), rr a Y → cc Y)) % 8.28/8.47 (Exists fun Y => And (rr a Y) (cowlThing Y))) % 8.28/8.50 (Exists fun Y => And (rp a Y) (cowlThing Y))) % 8.28/8.50 (∀ (Y : Iota), rp a Y → ca_Vx4 Y)) % 8.28/8.50 True) % 8.28/8.50 Clause #145 (by clausification #[57]): ∀ (a : Iota), Eq (ca_Ax2 (skS.0 2 i2003_11_14_17_21_33997 a)) True % 8.28/8.50 Clause #147 (by clausification #[8]): ∀ (a : Iota), Eq (Iff (ca_Vx3 a) (Exists fun Y => And (rr a Y) (cowlThing Y))) True % 8.28/8.50 Clause #149 (by clausification #[147]): ∀ (a : Iota), Or (Eq (ca_Vx3 a) False) (Eq (Exists fun Y => And (rr a Y) (cowlThing Y)) True) % 8.28/8.50 Clause #158 (by clausification #[149]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 a) False) (Eq (And (rr a (skS.0 11 a a_1)) (cowlThing (skS.0 11 a a_1))) True) % 8.28/8.50 Clause #160 (by clausification #[158]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 a) False) (Eq (rr a (skS.0 11 a a_1)) True) % 8.28/8.50 Clause #161 (by clausification #[9]): ∀ (a : Iota), Eq (Iff (ca_Vx4 a) (Exists fun Y => And (rp a Y) (cowlThing Y))) True % 8.28/8.50 Clause #162 (by clausification #[161]): ∀ (a : Iota), Or (Eq (ca_Vx4 a) True) (Eq (Exists fun Y => And (rp a Y) (cowlThing Y)) False) % 8.28/8.50 Clause #163 (by clausification #[161]): ∀ (a : Iota), Or (Eq (ca_Vx4 a) False) (Eq (Exists fun Y => And (rp a Y) (cowlThing Y)) True) % 8.28/8.50 Clause #164 (by clausification #[162]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx4 a) True) (Eq (And (rp a a_1) (cowlThing a_1)) False) % 8.28/8.50 Clause #165 (by clausification #[164]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx4 a) True) (Or (Eq (rp a a_1) False) (Eq (cowlThing a_1) False)) % 8.28/8.50 Clause #166 (by forward demodulation #[165, 29]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx4 a) True) (Or (Eq (rp a a_1) False) (Eq True False)) % 8.28/8.50 Clause #167 (by clausification #[166]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx4 a) True) (Eq (rp a a_1) False) % 8.28/8.50 Clause #168 (by clausification #[163]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx4 a) False) (Eq (And (rp a (skS.0 12 a a_1)) (cowlThing (skS.0 12 a a_1))) True) % 8.28/8.50 Clause #170 (by clausification #[168]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx4 a) False) (Eq (rp a (skS.0 12 a a_1)) True) % 8.28/8.50 Clause #171 (by superposition #[56, 17]): ∀ (a : Iota), Or (Eq (rs i2003_11_14_17_21_33997 (skS.0 2 i2003_11_14_17_21_33997 a)) True) (Eq False True) % 8.28/8.50 Clause #172 (by clausification #[171]): ∀ (a : Iota), Eq (rs i2003_11_14_17_21_33997 (skS.0 2 i2003_11_14_17_21_33997 a)) True % 8.28/8.50 Clause #173 (by superposition #[172, 90]): ∀ (a : Iota), Or (Eq (rinvS (skS.0 2 i2003_11_14_17_21_33997 a) i2003_11_14_17_21_33997) True) (Eq True False) % 8.28/8.50 Clause #174 (by clausification #[173]): ∀ (a : Iota), Eq (rinvS (skS.0 2 i2003_11_14_17_21_33997 a) i2003_11_14_17_21_33997) True % 8.28/8.50 Clause #208 (by clausification #[115]): ∀ (a : Iota), % 8.28/8.50 Or (Eq (ca_Ax2 a) False) % 8.28/8.50 (Eq % 8.28/8.50 (And % 8.28/8.50 (And % 8.28/8.50 (And (And (∀ (Y : Iota), rp a Y → ca_Vx3 Y) (∀ (Y : Iota), rp a Y → ca_Vx5 Y)) (∀ (Y : Iota), rr a Y → cc Y)) % 8.28/8.50 (Exists fun Y => And (rr a Y) (cowlThing Y))) % 8.28/8.50 (Exists fun Y => And (rp a Y) (cowlThing Y))) % 8.28/8.50 True) % 8.28/8.50 Clause #264 (by clausification #[208]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (Exists fun Y => And (rp a Y) (cowlThing Y)) True) % 8.28/8.50 Clause #265 (by clausification #[208]): ∀ (a : Iota), % 8.28/8.50 Or (Eq (ca_Ax2 a) False) % 8.28/8.50 (Eq % 8.28/8.50 (And (And (And (∀ (Y : Iota), rp a Y → ca_Vx3 Y) (∀ (Y : Iota), rp a Y → ca_Vx5 Y)) (∀ (Y : Iota), rr a Y → cc Y)) % 8.28/8.50 (Exists fun Y => And (rr a Y) (cowlThing Y))) % 8.28/8.50 True) % 8.28/8.50 Clause #266 (by clausification #[264]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Eq (And (rp a (skS.0 16 a a_1)) (cowlThing (skS.0 16 a a_1))) True) % 8.28/8.50 Clause #268 (by clausification #[266]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Eq (rp a (skS.0 16 a a_1)) True) % 8.28/8.50 Clause #269 (by superposition #[268, 145]): ∀ (a a_1 : Iota), % 8.28/8.50 Or (Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) (skS.0 16 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True) % 8.28/8.50 (Eq False True) % 8.28/8.50 Clause #270 (by clausification #[269]): ∀ (a a_1 : Iota), Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) (skS.0 16 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True % 8.28/8.50 Clause #275 (by superposition #[270, 167]): ∀ (a : Iota), Or (Eq (ca_Vx4 (skS.0 2 i2003_11_14_17_21_33997 a)) True) (Eq True False) % 8.28/8.53 Clause #280 (by clausification #[275]): ∀ (a : Iota), Eq (ca_Vx4 (skS.0 2 i2003_11_14_17_21_33997 a)) True % 8.28/8.53 Clause #281 (by superposition #[280, 170]): ∀ (a a_1 : Iota), % 8.28/8.53 Or (Eq True False) % 8.28/8.53 (Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True) % 8.28/8.53 Clause #296 (by clausification #[281]): ∀ (a a_1 : Iota), Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True % 8.28/8.53 Clause #299 (by superposition #[296, 110]): ∀ (a a_1 : Iota), % 8.28/8.53 Or (Eq (rinvP (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) (skS.0 2 i2003_11_14_17_21_33997 a)) True) % 8.28/8.53 (Eq True False) % 8.28/8.53 Clause #305 (by clausification #[299]): ∀ (a a_1 : Iota), Eq (rinvP (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) (skS.0 2 i2003_11_14_17_21_33997 a)) True % 8.28/8.53 Clause #315 (by clausification #[265]): ∀ (a : Iota), % 8.28/8.53 Or (Eq (ca_Ax2 a) False) % 8.28/8.53 (Eq (And (And (∀ (Y : Iota), rp a Y → ca_Vx3 Y) (∀ (Y : Iota), rp a Y → ca_Vx5 Y)) (∀ (Y : Iota), rr a Y → cc Y)) % 8.28/8.53 True) % 8.28/8.53 Clause #321 (by clausification #[315]): ∀ (a : Iota), % 8.28/8.53 Or (Eq (ca_Ax2 a) False) (Eq (And (∀ (Y : Iota), rp a Y → ca_Vx3 Y) (∀ (Y : Iota), rp a Y → ca_Vx5 Y)) True) % 8.28/8.53 Clause #325 (by clausification #[321]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (∀ (Y : Iota), rp a Y → ca_Vx5 Y) True) % 8.28/8.53 Clause #326 (by clausification #[321]): ∀ (a : Iota), Or (Eq (ca_Ax2 a) False) (Eq (∀ (Y : Iota), rp a Y → ca_Vx3 Y) True) % 8.28/8.53 Clause #327 (by clausification #[325]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Eq (rp a a_1 → ca_Vx5 a_1) True) % 8.28/8.53 Clause #328 (by clausification #[327]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Or (Eq (rp a a_1) False) (Eq (ca_Vx5 a_1) True)) % 8.28/8.53 Clause #329 (by superposition #[328, 145]): ∀ (a a_1 : Iota), Or (Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) a_1) False) (Or (Eq (ca_Vx5 a_1) True) (Eq False True)) % 8.28/8.53 Clause #330 (by clausification #[326]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Eq (rp a a_1 → ca_Vx3 a_1) True) % 8.28/8.53 Clause #331 (by clausification #[330]): ∀ (a a_1 : Iota), Or (Eq (ca_Ax2 a) False) (Or (Eq (rp a a_1) False) (Eq (ca_Vx3 a_1) True)) % 8.28/8.53 Clause #332 (by superposition #[331, 145]): ∀ (a a_1 : Iota), Or (Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) a_1) False) (Or (Eq (ca_Vx3 a_1) True) (Eq False True)) % 8.28/8.53 Clause #335 (by clausification #[332]): ∀ (a a_1 : Iota), Or (Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) a_1) False) (Eq (ca_Vx3 a_1) True) % 8.28/8.53 Clause #337 (by superposition #[335, 296]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx3 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True) (Eq False True) % 8.28/8.53 Clause #338 (by clausification #[329]): ∀ (a a_1 : Iota), Or (Eq (rp (skS.0 2 i2003_11_14_17_21_33997 a) a_1) False) (Eq (ca_Vx5 a_1) True) % 8.28/8.53 Clause #340 (by superposition #[338, 296]): ∀ (a a_1 : Iota), Or (Eq (ca_Vx5 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True) (Eq False True) % 8.28/8.53 Clause #345 (by clausification #[337]): ∀ (a a_1 : Iota), Eq (ca_Vx3 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True % 8.28/8.53 Clause #346 (by superposition #[345, 160]): ∀ (a a_1 a_2 : Iota), % 8.28/8.53 Or (Eq True False) % 8.28/8.53 (Eq % 8.28/8.53 (rr (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) % 8.28/8.53 (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2)) % 8.28/8.53 True) % 8.28/8.53 Clause #358 (by clausification #[340]): ∀ (a a_1 : Iota), Eq (ca_Vx5 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True % 8.28/8.53 Clause #359 (by superposition #[358, 77]): ∀ (a a_1 a_2 : Iota), % 8.28/8.53 Or (Eq True False) (Or (Eq (rr (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) False) (Eq (cc a_2) True)) % 8.28/8.53 Clause #362 (by clausification #[359]): ∀ (a a_1 a_2 : Iota), Or (Eq (rr (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) False) (Eq (cc a_2) True) % 8.28/8.53 Clause #495 (by clausification #[346]): ∀ (a a_1 a_2 : Iota), % 8.28/8.53 Eq % 8.28/8.53 (rr (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) % 8.28/8.53 (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2)) % 8.28/8.53 True % 8.28/8.53 Clause #496 (by superposition #[495, 362]): ∀ (a a_1 a_2 : Iota), % 8.28/8.53 Or (Eq True False) (Eq (cc (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2)) True) % 8.36/8.55 Clause #497 (by superposition #[495, 95]): ∀ (a a_1 a_2 : Iota), % 8.36/8.55 Or % 8.36/8.55 (Eq % 8.36/8.55 (rinvR (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) % 8.36/8.55 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) % 8.36/8.55 True) % 8.36/8.55 (Eq True False) % 8.36/8.55 Clause #499 (by clausification #[496]): ∀ (a a_1 a_2 : Iota), Eq (cc (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2)) True % 8.36/8.55 Clause #500 (by superposition #[499, 44]): ∀ (a a_1 a_2 a_3 : Iota), % 8.36/8.55 Or (Eq True False) % 8.36/8.55 (Or (Eq (rinvR (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) a_3) False) (Eq (ca_Vx7 a_3) True)) % 8.36/8.55 Clause #501 (by clausification #[500]): ∀ (a a_1 a_2 a_3 : Iota), % 8.36/8.55 Or (Eq (rinvR (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) a_3) False) (Eq (ca_Vx7 a_3) True) % 8.36/8.55 Clause #504 (by clausification #[497]): ∀ (a a_1 a_2 : Iota), % 8.36/8.55 Eq % 8.36/8.55 (rinvR (skS.0 11 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) % 8.36/8.55 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) % 8.36/8.55 True % 8.36/8.55 Clause #505 (by superposition #[504, 501]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (ca_Vx7 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True) % 8.36/8.55 Clause #506 (by clausification #[505]): ∀ (a a_1 : Iota), Eq (ca_Vx7 (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1)) True % 8.36/8.55 Clause #507 (by superposition #[506, 59]): ∀ (a a_1 a_2 : Iota), % 8.36/8.55 Or (Eq True False) % 8.36/8.55 (Or (Eq (rinvP (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) False) (Eq (ca_Vx6 a_2) True)) % 8.36/8.55 Clause #508 (by clausification #[507]): ∀ (a a_1 a_2 : Iota), % 8.36/8.55 Or (Eq (rinvP (skS.0 12 (skS.0 2 i2003_11_14_17_21_33997 a) a_1) a_2) False) (Eq (ca_Vx6 a_2) True) % 8.36/8.55 Clause #509 (by superposition #[508, 305]): ∀ (a : Iota), Or (Eq (ca_Vx6 (skS.0 2 i2003_11_14_17_21_33997 a)) True) (Eq False True) % 8.36/8.55 Clause #512 (by clausification #[509]): ∀ (a : Iota), Eq (ca_Vx6 (skS.0 2 i2003_11_14_17_21_33997 a)) True % 8.36/8.55 Clause #513 (by superposition #[512, 68]): ∀ (a a_1 : Iota), % 8.36/8.55 Or (Eq True False) (Or (Eq (rinvS (skS.0 2 i2003_11_14_17_21_33997 a) a_1) False) (Eq (caxcomp a_1) True)) % 8.36/8.55 Clause #514 (by clausification #[513]): ∀ (a a_1 : Iota), Or (Eq (rinvS (skS.0 2 i2003_11_14_17_21_33997 a) a_1) False) (Eq (caxcomp a_1) True) % 8.36/8.55 Clause #515 (by superposition #[514, 174]): Or (Eq (caxcomp i2003_11_14_17_21_33997) True) (Eq False True) % 8.36/8.55 Clause #531 (by clausification #[515]): Eq (caxcomp i2003_11_14_17_21_33997) True % 8.36/8.55 Clause #532 (by superposition #[531, 105]): ∀ (a : Iota), Or (Eq True False) (Eq (ra_Px1 i2003_11_14_17_21_33997 (skS.0 6 i2003_11_14_17_21_33997 a)) True) % 8.36/8.55 Clause #533 (by clausification #[532]): ∀ (a : Iota), Eq (ra_Px1 i2003_11_14_17_21_33997 (skS.0 6 i2003_11_14_17_21_33997 a)) True % 8.36/8.55 Clause #534 (by superposition #[533, 87]): Eq True False % 8.36/8.55 Clause #536 (by clausification #[534]): False % 8.36/8.55 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------