%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM309_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n004.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 238.38s 238.70s % Output : Proof 238.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM309_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.16/0.34 % Computer : n004.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:46:17 EDT 2026 % 0.16/0.34 % CPUTime : % 238.38/238.70 SZS status Theorem for theBenchmark.p % 238.38/238.70 SZS output start Proof for theBenchmark.p % 238.38/238.70 Clause #143 (by assumption #[]): Eq (∀ (Vrt : vRawTable), Eq (vrawUnion vtempty Vrt) Vrt) True % 238.38/238.70 Clause #292 (by assumption #[]): Eq % 238.38/238.70 (Not % 238.38/238.70 (∀ (Vtt : vTType) (Vrt1 : vRawTable), % 238.38/238.70 And (vwelltypedRawtable Vtt vtempty) (vwelltypedRawtable Vtt Vrt1) → % 238.38/238.70 vwelltypedRawtable Vtt (vrawUnion vtempty Vrt1))) % 238.38/238.70 True % 238.38/238.70 Clause #709 (by clausification #[143]): ∀ (a : vRawTable), Eq (Eq (vrawUnion vtempty a) a) True % 238.38/238.70 Clause #710 (by clausification #[709]): ∀ (a : vRawTable), Eq (vrawUnion vtempty a) a % 238.38/238.70 Clause #1206 (by clausification #[292]): Eq % 238.38/238.70 (∀ (Vtt : vTType) (Vrt1 : vRawTable), % 238.38/238.70 And (vwelltypedRawtable Vtt vtempty) (vwelltypedRawtable Vtt Vrt1) → % 238.38/238.70 vwelltypedRawtable Vtt (vrawUnion vtempty Vrt1)) % 238.38/238.70 False % 238.38/238.70 Clause #1207 (by clausification #[1206]): ∀ (a : vTType), % 238.38/238.70 Eq % 238.38/238.70 (Not % 238.38/238.70 (∀ (Vrt1 : vRawTable), % 238.38/238.70 And (vwelltypedRawtable (skS.0 48 a) vtempty) (vwelltypedRawtable (skS.0 48 a) Vrt1) → % 238.38/238.70 vwelltypedRawtable (skS.0 48 a) (vrawUnion vtempty Vrt1))) % 238.38/238.70 True % 238.38/238.70 Clause #1208 (by clausification #[1207]): ∀ (a : vTType), % 238.38/238.70 Eq % 238.38/238.70 (∀ (Vrt1 : vRawTable), % 238.38/238.70 And (vwelltypedRawtable (skS.0 48 a) vtempty) (vwelltypedRawtable (skS.0 48 a) Vrt1) → % 238.38/238.70 vwelltypedRawtable (skS.0 48 a) (vrawUnion vtempty Vrt1)) % 238.38/238.70 False % 238.38/238.70 Clause #1209 (by clausification #[1208]): ∀ (a : vTType) (a_1 : vRawTable), % 238.38/238.70 Eq % 238.38/238.70 (Not % 238.38/238.70 (And (vwelltypedRawtable (skS.0 48 a) vtempty) (vwelltypedRawtable (skS.0 48 a) (skS.0 49 a a_1)) → % 238.38/238.70 vwelltypedRawtable (skS.0 48 a) (vrawUnion vtempty (skS.0 49 a a_1)))) % 238.38/238.70 True % 238.38/238.70 Clause #1210 (by clausification #[1209]): ∀ (a : vTType) (a_1 : vRawTable), % 238.38/238.70 Eq % 238.38/238.70 (And (vwelltypedRawtable (skS.0 48 a) vtempty) (vwelltypedRawtable (skS.0 48 a) (skS.0 49 a a_1)) → % 238.38/238.70 vwelltypedRawtable (skS.0 48 a) (vrawUnion vtempty (skS.0 49 a a_1))) % 238.38/238.70 False % 238.38/238.70 Clause #1211 (by clausification #[1210]): ∀ (a : vTType) (a_1 : vRawTable), % 238.38/238.70 Eq (And (vwelltypedRawtable (skS.0 48 a) vtempty) (vwelltypedRawtable (skS.0 48 a) (skS.0 49 a a_1))) True % 238.38/238.70 Clause #1212 (by clausification #[1210]): ∀ (a : vTType) (a_1 : vRawTable), Eq (vwelltypedRawtable (skS.0 48 a) (vrawUnion vtempty (skS.0 49 a a_1))) False % 238.38/238.70 Clause #1213 (by clausification #[1211]): ∀ (a : vTType) (a_1 : vRawTable), Eq (vwelltypedRawtable (skS.0 48 a) (skS.0 49 a a_1)) True % 238.38/238.70 Clause #16348 (by forward demodulation #[1212, 710]): ∀ (a : vTType) (a_1 : vRawTable), Eq (vwelltypedRawtable (skS.0 48 a) (skS.0 49 a a_1)) False % 238.38/238.70 Clause #16349 (by superposition #[16348, 1213]): Eq False True % 238.38/238.70 Clause #16354 (by clausification #[16349]): False % 238.38/238.70 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------