%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM128+1 : TPTP v9.2.0. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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:45:55 PM UTC 2025 % Result : Theorem 31.63s 31.82s % Output : Proof 31.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : COM128+1 : TPTP v9.2.0. Released v6.4.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n013.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 15:57:38 EDT 2025 % 0.13/0.34 % CPUTime : % 31.63/31.82 SZS status Theorem for theBenchmark.p % 31.63/31.82 SZS output start Proof for theBenchmark.p % 31.63/31.82 Clause #9 (by assumption #[]): Eq % 31.63/31.82 (∀ (VVar0 VExp0 Vx Vv : Iota), % 31.63/31.82 And (Eq VVar0 Vv) (Eq VExp0 (vvar Vx)) → % 31.63/31.82 And (Eq Vx Vv → visFreeVar VVar0 VExp0) (visFreeVar VVar0 VExp0 → Eq Vx Vv)) % 31.63/31.82 True % 31.63/31.82 Clause #11 (by assumption #[]): Eq % 31.63/31.82 (∀ (VVar0 VExp0 Ve1 Vv Ve2 : Iota), % 31.63/31.82 And (Eq VVar0 Vv) (Eq VExp0 (vapp Ve1 Ve2)) → % 31.63/31.82 And (Or (visFreeVar Vv Ve1) (visFreeVar Vv Ve2) → visFreeVar VVar0 VExp0) % 31.63/31.82 (visFreeVar VVar0 VExp0 → Or (visFreeVar Vv Ve1) (visFreeVar Vv Ve2))) % 31.63/31.82 True % 31.63/31.82 Clause #27 (by assumption #[]): Eq (∀ (Vv Ve : Iota), Eq (vgensym Ve) Vv → Not (visFreeVar Vv Ve)) True % 31.63/31.82 Clause #64 (by assumption #[]): Eq (Not (∀ (Ve Ve1 Vx Vfresh : Iota), Eq Vfresh (vgensym (vapp (vapp Ve Ve1) (vvar Vx))) → Ne Vx Vfresh)) True % 31.63/31.82 Clause #144 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (Ve : Iota), Eq (vgensym Ve) a → Not (visFreeVar a Ve)) True % 31.63/31.82 Clause #145 (by clausification #[144]): ∀ (a a_1 : Iota), Eq (Eq (vgensym a) a_1 → Not (visFreeVar a_1 a)) True % 31.63/31.82 Clause #146 (by clausification #[145]): ∀ (a a_1 : Iota), Or (Eq (Eq (vgensym a) a_1) False) (Eq (Not (visFreeVar a_1 a)) True) % 31.63/31.82 Clause #147 (by clausification #[146]): ∀ (a a_1 : Iota), Or (Eq (Not (visFreeVar a a_1)) True) (Ne (vgensym a_1) a) % 31.63/31.82 Clause #148 (by clausification #[147]): ∀ (a a_1 : Iota), Or (Ne (vgensym a) a_1) (Eq (visFreeVar a_1 a) False) % 31.63/31.82 Clause #149 (by destructive equality resolution #[148]): ∀ (a : Iota), Eq (visFreeVar (vgensym a) a) False % 31.63/31.82 Clause #285 (by clausification #[9]): ∀ (a : Iota), % 31.63/31.82 Eq % 31.63/31.82 (∀ (VExp0 Vx Vv : Iota), % 31.63/31.82 And (Eq a Vv) (Eq VExp0 (vvar Vx)) → And (Eq Vx Vv → visFreeVar a VExp0) (visFreeVar a VExp0 → Eq Vx Vv)) % 31.63/31.82 True % 31.63/31.82 Clause #286 (by clausification #[285]): ∀ (a a_1 : Iota), % 31.63/31.82 Eq % 31.63/31.82 (∀ (Vx Vv : Iota), % 31.63/31.82 And (Eq a Vv) (Eq a_1 (vvar Vx)) → And (Eq Vx Vv → visFreeVar a a_1) (visFreeVar a a_1 → Eq Vx Vv)) % 31.63/31.82 True % 31.63/31.82 Clause #287 (by clausification #[286]): ∀ (a a_1 a_2 : Iota), % 31.63/31.82 Eq % 31.63/31.82 (∀ (Vv : Iota), % 31.63/31.82 And (Eq a Vv) (Eq a_1 (vvar a_2)) → And (Eq a_2 Vv → visFreeVar a a_1) (visFreeVar a a_1 → Eq a_2 Vv)) % 31.63/31.82 True % 31.63/31.82 Clause #288 (by clausification #[287]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.82 Eq (And (Eq a a_1) (Eq a_2 (vvar a_3)) → And (Eq a_3 a_1 → visFreeVar a a_2) (visFreeVar a a_2 → Eq a_3 a_1)) True % 31.63/31.82 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.82 Or (Eq (And (Eq a a_1) (Eq a_2 (vvar a_3))) False) % 31.63/31.82 (Eq (And (Eq a_3 a_1 → visFreeVar a a_2) (visFreeVar a a_2 → Eq a_3 a_1)) True) % 31.63/31.82 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.82 Or (Eq (And (Eq a a_1 → visFreeVar a_2 a_3) (visFreeVar a_2 a_3 → Eq a a_1)) True) % 31.63/31.82 (Or (Eq (Eq a_2 a_1) False) (Eq (Eq a_3 (vvar a)) False)) % 31.63/31.82 Clause #292 (by clausification #[290]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.82 Or (Eq (Eq a a_1) False) (Or (Eq (Eq a_2 (vvar a_3)) False) (Eq (Eq a_3 a_1 → visFreeVar a a_2) True)) % 31.63/31.82 Clause #299 (by clausification #[64]): Eq (∀ (Ve Ve1 Vx Vfresh : Iota), Eq Vfresh (vgensym (vapp (vapp Ve Ve1) (vvar Vx))) → Ne Vx Vfresh) False % 31.63/31.82 Clause #300 (by clausification #[299]): ∀ (a : Iota), % 31.63/31.82 Eq (Not (∀ (Ve1 Vx Vfresh : Iota), Eq Vfresh (vgensym (vapp (vapp (skS.0 0 a) Ve1) (vvar Vx))) → Ne Vx Vfresh)) True % 31.63/31.82 Clause #301 (by clausification #[300]): ∀ (a : Iota), % 31.63/31.82 Eq (∀ (Ve1 Vx Vfresh : Iota), Eq Vfresh (vgensym (vapp (vapp (skS.0 0 a) Ve1) (vvar Vx))) → Ne Vx Vfresh) False % 31.63/31.82 Clause #302 (by clausification #[301]): ∀ (a a_1 : Iota), % 31.63/31.82 Eq % 31.63/31.82 (Not (∀ (Vx Vfresh : Iota), Eq Vfresh (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar Vx))) → Ne Vx Vfresh)) % 31.63/31.82 True % 31.63/31.82 Clause #303 (by clausification #[302]): ∀ (a a_1 : Iota), % 31.63/31.82 Eq (∀ (Vx Vfresh : Iota), Eq Vfresh (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar Vx))) → Ne Vx Vfresh) % 31.63/31.82 False % 31.63/31.82 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), % 31.63/31.82 Eq % 31.63/31.82 (Not % 31.63/31.82 (∀ (Vfresh : Iota), % 31.63/31.82 Eq Vfresh (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2)))) → % 31.63/31.82 Ne (skS.0 2 a a_1 a_2) Vfresh)) % 31.63/31.85 True % 31.63/31.85 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 : Iota), % 31.63/31.85 Eq % 31.63/31.85 (∀ (Vfresh : Iota), % 31.63/31.85 Eq Vfresh (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2)))) → % 31.63/31.85 Ne (skS.0 2 a a_1 a_2) Vfresh) % 31.63/31.85 False % 31.63/31.85 Clause #306 (by clausification #[305]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.85 Eq % 31.63/31.85 (Not % 31.63/31.85 (Eq (skS.0 3 a a_1 a_2 a_3) (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2)))) → % 31.63/31.85 Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3))) % 31.63/31.85 True % 31.63/31.85 Clause #307 (by clausification #[306]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.85 Eq % 31.63/31.85 (Eq (skS.0 3 a a_1 a_2 a_3) (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2)))) → % 31.63/31.85 Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) % 31.63/31.85 False % 31.63/31.85 Clause #308 (by clausification #[307]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.85 Eq (Eq (skS.0 3 a a_1 a_2 a_3) (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2))))) True % 31.63/31.85 Clause #309 (by clausification #[307]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Ne (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3)) False % 31.63/31.85 Clause #310 (by clausification #[308]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.85 Eq (skS.0 3 a a_1 a_2 a_3) (vgensym (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2)))) % 31.63/31.85 Clause #312 (by superposition #[310, 149]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.85 Eq (visFreeVar (skS.0 3 a a_1 a_2 a_3) (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2)))) False % 31.63/31.85 Clause #396 (by clausification #[11]): ∀ (a : Iota), % 31.63/31.85 Eq % 31.63/31.85 (∀ (VExp0 Ve1 Vv Ve2 : Iota), % 31.63/31.85 And (Eq a Vv) (Eq VExp0 (vapp Ve1 Ve2)) → % 31.63/31.85 And (Or (visFreeVar Vv Ve1) (visFreeVar Vv Ve2) → visFreeVar a VExp0) % 31.63/31.85 (visFreeVar a VExp0 → Or (visFreeVar Vv Ve1) (visFreeVar Vv Ve2))) % 31.63/31.85 True % 31.63/31.85 Clause #397 (by clausification #[396]): ∀ (a a_1 : Iota), % 31.63/31.85 Eq % 31.63/31.85 (∀ (Ve1 Vv Ve2 : Iota), % 31.63/31.85 And (Eq a Vv) (Eq a_1 (vapp Ve1 Ve2)) → % 31.63/31.85 And (Or (visFreeVar Vv Ve1) (visFreeVar Vv Ve2) → visFreeVar a a_1) % 31.63/31.85 (visFreeVar a a_1 → Or (visFreeVar Vv Ve1) (visFreeVar Vv Ve2))) % 31.63/31.85 True % 31.63/31.85 Clause #398 (by clausification #[397]): ∀ (a a_1 a_2 : Iota), % 31.63/31.85 Eq % 31.63/31.85 (∀ (Vv Ve2 : Iota), % 31.63/31.85 And (Eq a Vv) (Eq a_1 (vapp a_2 Ve2)) → % 31.63/31.85 And (Or (visFreeVar Vv a_2) (visFreeVar Vv Ve2) → visFreeVar a a_1) % 31.63/31.85 (visFreeVar a a_1 → Or (visFreeVar Vv a_2) (visFreeVar Vv Ve2))) % 31.63/31.85 True % 31.63/31.85 Clause #399 (by clausification #[398]): ∀ (a a_1 a_2 a_3 : Iota), % 31.63/31.85 Eq % 31.63/31.85 (∀ (Ve2 : Iota), % 31.63/31.85 And (Eq a a_1) (Eq a_2 (vapp a_3 Ve2)) → % 31.63/31.85 And (Or (visFreeVar a_1 a_3) (visFreeVar a_1 Ve2) → visFreeVar a a_2) % 31.63/31.85 (visFreeVar a a_2 → Or (visFreeVar a_1 a_3) (visFreeVar a_1 Ve2))) % 31.63/31.85 True % 31.63/31.85 Clause #400 (by clausification #[399]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.63/31.85 Eq % 31.63/31.85 (And (Eq a a_1) (Eq a_2 (vapp a_3 a_4)) → % 31.63/31.85 And (Or (visFreeVar a_1 a_3) (visFreeVar a_1 a_4) → visFreeVar a a_2) % 31.63/31.85 (visFreeVar a a_2 → Or (visFreeVar a_1 a_3) (visFreeVar a_1 a_4))) % 31.63/31.85 True % 31.63/31.85 Clause #401 (by clausification #[400]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.63/31.85 Or (Eq (And (Eq a a_1) (Eq a_2 (vapp a_3 a_4))) False) % 31.63/31.85 (Eq % 31.63/31.85 (And (Or (visFreeVar a_1 a_3) (visFreeVar a_1 a_4) → visFreeVar a a_2) % 31.63/31.85 (visFreeVar a a_2 → Or (visFreeVar a_1 a_3) (visFreeVar a_1 a_4))) % 31.63/31.85 True) % 31.63/31.85 Clause #402 (by clausification #[401]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.63/31.85 Or % 31.63/31.85 (Eq % 31.63/31.85 (And (Or (visFreeVar a a_1) (visFreeVar a a_2) → visFreeVar a_3 a_4) % 31.63/31.85 (visFreeVar a_3 a_4 → Or (visFreeVar a a_1) (visFreeVar a a_2))) % 31.63/31.85 True) % 31.63/31.85 (Or (Eq (Eq a_3 a) False) (Eq (Eq a_4 (vapp a_1 a_2)) False)) % 31.63/31.85 Clause #404 (by clausification #[402]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.63/31.85 Or (Eq (Eq a a_1) False) % 31.63/31.85 (Or (Eq (Eq a_2 (vapp a_3 a_4)) False) (Eq (Or (visFreeVar a_1 a_3) (visFreeVar a_1 a_4) → visFreeVar a a_2) True)) % 31.63/31.85 Clause #5020 (by clausification #[292]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (Eq a (vvar a_1)) False) (Or (Eq (Eq a_1 a_2 → visFreeVar a_3 a) True) (Ne a_3 a_2)) % 31.63/31.85 Clause #5021 (by clausification #[5020]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (Eq a a_1 → visFreeVar a_2 a_3) True) (Or (Ne a_2 a_1) (Ne a_3 (vvar a))) % 31.71/31.92 Clause #5022 (by clausification #[5021]): ∀ (a a_1 a_2 a_3 : Iota), % 31.71/31.92 Or (Ne a a_1) (Or (Ne a_2 (vvar a_3)) (Or (Eq (Eq a_3 a_1) False) (Eq (visFreeVar a a_2) True))) % 31.71/31.92 Clause #5023 (by clausification #[5022]): ∀ (a a_1 a_2 a_3 : Iota), Or (Ne a a_1) (Or (Ne a_2 (vvar a_3)) (Or (Eq (visFreeVar a a_2) True) (Ne a_3 a_1))) % 31.71/31.92 Clause #5024 (by destructive equality resolution #[5023]): ∀ (a a_1 a_2 : Iota), Or (Ne a (vvar a_1)) (Or (Eq (visFreeVar a_2 a) True) (Ne a_1 a_2)) % 31.71/31.92 Clause #5025 (by destructive equality resolution #[5024]): ∀ (a a_1 : Iota), Or (Eq (visFreeVar a (vvar a_1)) True) (Ne a_1 a) % 31.71/31.92 Clause #5026 (by destructive equality resolution #[5025]): ∀ (a : Iota), Eq (visFreeVar a (vvar a)) True % 31.71/31.92 Clause #5115 (by clausification #[309]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 2 a a_1 a_2) (skS.0 3 a a_1 a_2 a_3) % 31.71/31.92 Clause #5699 (by forward demodulation #[312, 5115]): ∀ (a a_1 a_2 : Iota), % 31.71/31.92 Eq (visFreeVar (skS.0 2 a a_1 a_2) (vapp (vapp (skS.0 0 a) (skS.0 1 a a_1)) (vvar (skS.0 2 a a_1 a_2)))) False % 31.71/31.92 Clause #6927 (by clausification #[404]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.71/31.92 Or (Eq (Eq a (vapp a_1 a_2)) False) % 31.71/31.92 (Or (Eq (Or (visFreeVar a_3 a_1) (visFreeVar a_3 a_2) → visFreeVar a_4 a) True) (Ne a_4 a_3)) % 31.71/31.92 Clause #6928 (by clausification #[6927]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.71/31.92 Or (Eq (Or (visFreeVar a a_1) (visFreeVar a a_2) → visFreeVar a_3 a_4) True) (Or (Ne a_3 a) (Ne a_4 (vapp a_1 a_2))) % 31.71/31.92 Clause #6929 (by clausification #[6928]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.71/31.92 Or (Ne a a_1) % 31.71/31.92 (Or (Ne a_2 (vapp a_3 a_4)) % 31.71/31.92 (Or (Eq (Or (visFreeVar a_1 a_3) (visFreeVar a_1 a_4)) False) (Eq (visFreeVar a a_2) True))) % 31.71/31.92 Clause #6930 (by clausification #[6929]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.71/31.92 Or (Ne a a_1) (Or (Ne a_2 (vapp a_3 a_4)) (Or (Eq (visFreeVar a a_2) True) (Eq (visFreeVar a_1 a_4) False))) % 31.71/31.92 Clause #6932 (by destructive equality resolution #[6930]): ∀ (a a_1 a_2 a_3 : Iota), Or (Ne a (vapp a_1 a_2)) (Or (Eq (visFreeVar a_3 a) True) (Eq (visFreeVar a_3 a_2) False)) % 31.71/31.92 Clause #6933 (by destructive equality resolution #[6932]): ∀ (a a_1 a_2 : Iota), Or (Eq (visFreeVar a (vapp a_1 a_2)) True) (Eq (visFreeVar a a_2) False) % 31.71/31.92 Clause #6937 (by superposition #[6933, 5026]): ∀ (a a_1 : Iota), Or (Eq (visFreeVar a (vapp a_1 (vvar a))) True) (Eq False True) % 31.71/31.92 Clause #6940 (by clausification #[6937]): ∀ (a a_1 : Iota), Eq (visFreeVar a (vapp a_1 (vvar a))) True % 31.71/31.92 Clause #6941 (by superposition #[6940, 5699]): Eq True False % 31.71/31.92 Clause #6984 (by clausification #[6941]): False % 31.71/31.92 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------