%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM310_1 : TPTP v9.3.0. Released v9.3.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 : Tue May 5 06:18:15 PM UTC 2026 % Result : Theorem 17.54s 17.77s % Output : Proof 17.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : COM310_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.16/0.34 % Computer : n022.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 20:48:20 EDT 2026 % 0.16/0.34 % CPUTime : % 17.54/17.77 SZS status Theorem for theBenchmark.p % 17.54/17.77 SZS output start Proof for theBenchmark.p % 17.54/17.77 Clause #106 (by assumption #[]): Eq (vwelltypedRow vttempty vrempty) True % 17.54/17.77 Clause #112 (by assumption #[]): Eq % 17.54/17.77 (∀ (Vtt : vTType) (Vr : vRow) (Vt1 : vRawTable), % 17.54/17.77 Iff (vwelltypedRawtable Vtt (vtcons Vr Vt1)) (And (vwelltypedRow Vtt Vr) (vwelltypedRawtable Vtt Vt1))) % 17.54/17.77 True % 17.54/17.77 Clause #191 (by assumption #[]): Eq % 17.54/17.77 (∀ (VwildcardName0 : vRow) (Vt : vRawTable), % 17.54/17.77 Eq (vprojectEmptyCol (vtcons VwildcardName0 Vt)) (vtcons vrempty (vprojectEmptyCol Vt))) % 17.54/17.77 True % 17.54/17.77 Clause #292 (by assumption #[]): Eq (vwelltypedRawtable vttempty (vprojectEmptyCol vrt2)) True % 17.54/17.77 Clause #293 (by assumption #[]): Eq (Not (∀ (Vr : vRow), vwelltypedRawtable vttempty (vprojectEmptyCol (vtcons Vr vrt2)))) True % 17.54/17.77 Clause #932 (by clausification #[293]): Eq (∀ (Vr : vRow), vwelltypedRawtable vttempty (vprojectEmptyCol (vtcons Vr vrt2))) False % 17.54/17.77 Clause #933 (by clausification #[932]): ∀ (a : vRow), Eq (Not (vwelltypedRawtable vttempty (vprojectEmptyCol (vtcons (skS.0 27 a) vrt2)))) True % 17.54/17.77 Clause #934 (by clausification #[933]): ∀ (a : vRow), Eq (vwelltypedRawtable vttempty (vprojectEmptyCol (vtcons (skS.0 27 a) vrt2))) False % 17.54/17.77 Clause #1899 (by clausification #[112]): ∀ (a : vTType), % 17.54/17.77 Eq % 17.54/17.77 (∀ (Vr : vRow) (Vt1 : vRawTable), % 17.54/17.77 Iff (vwelltypedRawtable a (vtcons Vr Vt1)) (And (vwelltypedRow a Vr) (vwelltypedRawtable a Vt1))) % 17.54/17.77 True % 17.54/17.77 Clause #1900 (by clausification #[1899]): ∀ (a : vTType) (a_1 : vRow), % 17.54/17.77 Eq % 17.54/17.77 (∀ (Vt1 : vRawTable), % 17.54/17.77 Iff (vwelltypedRawtable a (vtcons a_1 Vt1)) (And (vwelltypedRow a a_1) (vwelltypedRawtable a Vt1))) % 17.54/17.77 True % 17.54/17.77 Clause #1901 (by clausification #[1900]): ∀ (a : vTType) (a_1 : vRow) (a_2 : vRawTable), % 17.54/17.77 Eq (Iff (vwelltypedRawtable a (vtcons a_1 a_2)) (And (vwelltypedRow a a_1) (vwelltypedRawtable a a_2))) True % 17.54/17.77 Clause #1902 (by clausification #[1901]): ∀ (a : vTType) (a_1 : vRow) (a_2 : vRawTable), % 17.54/17.77 Or (Eq (vwelltypedRawtable a (vtcons a_1 a_2)) True) (Eq (And (vwelltypedRow a a_1) (vwelltypedRawtable a a_2)) False) % 17.54/17.77 Clause #1904 (by clausification #[1902]): ∀ (a : vTType) (a_1 : vRow) (a_2 : vRawTable), % 17.54/17.77 Or (Eq (vwelltypedRawtable a (vtcons a_1 a_2)) True) % 17.54/17.77 (Or (Eq (vwelltypedRow a a_1) False) (Eq (vwelltypedRawtable a a_2) False)) % 17.54/17.77 Clause #1905 (by superposition #[1904, 106]): ∀ (a : vRawTable), % 17.54/17.77 Or (Eq (vwelltypedRawtable vttempty (vtcons vrempty a)) True) % 17.54/17.77 (Or (Eq (vwelltypedRawtable vttempty a) False) (Eq False True)) % 17.54/17.77 Clause #2012 (by clausification #[1905]): ∀ (a : vRawTable), % 17.54/17.77 Or (Eq (vwelltypedRawtable vttempty (vtcons vrempty a)) True) (Eq (vwelltypedRawtable vttempty a) False) % 17.54/17.77 Clause #2013 (by superposition #[2012, 292]): Or (Eq (vwelltypedRawtable vttempty (vtcons vrempty (vprojectEmptyCol vrt2))) True) (Eq False True) % 17.54/17.77 Clause #2022 (by clausification #[2013]): Eq (vwelltypedRawtable vttempty (vtcons vrempty (vprojectEmptyCol vrt2))) True % 17.54/17.77 Clause #3393 (by clausification #[191]): ∀ (a : vRow), Eq (∀ (Vt : vRawTable), Eq (vprojectEmptyCol (vtcons a Vt)) (vtcons vrempty (vprojectEmptyCol Vt))) True % 17.54/17.77 Clause #3394 (by clausification #[3393]): ∀ (a : vRow) (a_1 : vRawTable), Eq (Eq (vprojectEmptyCol (vtcons a a_1)) (vtcons vrempty (vprojectEmptyCol a_1))) True % 17.54/17.77 Clause #3395 (by clausification #[3394]): ∀ (a : vRow) (a_1 : vRawTable), Eq (vprojectEmptyCol (vtcons a a_1)) (vtcons vrempty (vprojectEmptyCol a_1)) % 17.54/17.77 Clause #3396 (by backward demodulation #[3395, 934]): Eq (vwelltypedRawtable vttempty (vtcons vrempty (vprojectEmptyCol vrt2))) False % 17.54/17.77 Clause #3409 (by superposition #[3396, 2022]): Eq False True % 17.54/17.77 Clause #3412 (by clausification #[3409]): False % 17.54/17.77 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------