%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM310_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n019.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:23:08 PM UTC 2026
% Result : Theorem 0.29s 0.51s
% Output : Proof 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM310_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.15/0.33 % Computer : n019.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 20:49:00 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.29/0.51 % SZS status Theorem
% 0.29/0.51 % SZS output start Proof
% 0.29/0.51 tff(vwelltypedRawtable_type, type, (
% 0.29/0.51 vwelltypedRawtable: ( vTType * vRawTable ) > $o)).
% 0.29/0.51 tff(vtcons_type, type, (
% 0.29/0.51 vtcons: ( vRow * vRawTable ) > vRawTable)).
% 0.29/0.51 tff(vprojectEmptyCol_type, type, (
% 0.29/0.51 vprojectEmptyCol: vRawTable > vRawTable)).
% 0.29/0.51 tff(vrt2_type, type, (
% 0.29/0.51 vrt2: vRawTable)).
% 0.29/0.51 tff(vrempty_type, type, (
% 0.29/0.51 vrempty: vRow)).
% 0.29/0.51 tff(vttempty_type, type, (
% 0.29/0.51 vttempty: vTType)).
% 0.29/0.51 tff(tptp_fun_Vr_307_type, type, (
% 0.29/0.51 tptp_fun_Vr_307: vRow)).
% 0.29/0.51 tff(vwelltypedRow_type, type, (
% 0.29/0.51 vwelltypedRow: ( vTType * vRow ) > $o)).
% 0.29/0.51 tff(1,plain,
% 0.29/0.51 (^[VwildcardName0: vRow, Vt: vRawTable] : refl((vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt))) <=> (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt))))),
% 0.29/0.51 inference(bind,[status(th)],[])).
% 0.29/0.51 tff(2,plain,
% 0.29/0.51 (![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt))) <=> ![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt)))),
% 0.29/0.51 inference(quant_intro,[status(thm)],[1])).
% 0.29/0.51 tff(3,plain,
% 0.29/0.51 (![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt))) <=> ![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt)))),
% 0.29/0.51 inference(rewrite,[status(thm)],[])).
% 0.29/0.51 tff(4,axiom,(![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''projectEmptyCol-1'')).
% 0.29/0.51 tff(5,plain,
% 0.29/0.51 (![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.29/0.51 tff(6,plain,(
% 0.29/0.51 ![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt)))),
% 0.29/0.51 inference(skolemize,[status(sab)],[5])).
% 0.29/0.51 tff(7,plain,
% 0.29/0.51 (![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.29/0.51 tff(8,plain,
% 0.29/0.51 ((~![VwildcardName0: vRow, Vt: vRawTable] : (vprojectEmptyCol(vtcons(VwildcardName0, Vt)) = vtcons(vrempty, vprojectEmptyCol(Vt)))) | (vprojectEmptyCol(vtcons(Vr!307, vrt2)) = vtcons(vrempty, vprojectEmptyCol(vrt2)))),
% 0.29/0.51 inference(quant_inst,[status(thm)],[])).
% 0.29/0.51 tff(9,plain,
% 0.29/0.51 (vprojectEmptyCol(vtcons(Vr!307, vrt2)) = vtcons(vrempty, vprojectEmptyCol(vrt2))),
% 0.29/0.51 inference(unit_resolution,[status(thm)],[8, 7])).
% 0.29/0.51 tff(10,plain,
% 0.29/0.51 (vtcons(vrempty, vprojectEmptyCol(vrt2)) = vprojectEmptyCol(vtcons(Vr!307, vrt2))),
% 0.29/0.51 inference(symmetry,[status(thm)],[9])).
% 0.29/0.51 tff(11,plain,
% 0.29/0.51 (vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2))) <=> vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr!307, vrt2)))),
% 0.29/0.51 inference(monotonicity,[status(thm)],[10])).
% 0.29/0.51 tff(12,plain,
% 0.29/0.51 (vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr!307, vrt2))) <=> vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))),
% 0.29/0.51 inference(symmetry,[status(thm)],[11])).
% 0.29/0.51 tff(13,plain,
% 0.29/0.51 ((~vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr!307, vrt2)))) <=> (~vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2))))),
% 0.29/0.51 inference(monotonicity,[status(thm)],[12])).
% 0.29/0.51 tff(14,plain,
% 0.29/0.51 ((~![Vr: vRow] : vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr, vrt2)))) <=> (~![Vr: vRow] : vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr, vrt2))))),
% 0.29/0.51 inference(rewrite,[status(thm)],[])).
% 0.29/0.51 tff(15,axiom,(~![Vr: vRow] : vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr, vrt2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''welltypedEmptyProjection-tcons'')).
% 0.29/0.51 tff(16,plain,
% 0.29/0.51 (~![Vr: vRow] : vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr, vrt2)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.29/0.51 tff(17,plain,
% 0.29/0.51 (~![Vr: vRow] : vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr, vrt2)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[16, 14])).
% 0.29/0.51 tff(18,plain,
% 0.29/0.51 (~![Vr: vRow] : vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr, vrt2)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[17, 14])).
% 0.29/0.51 tff(19,plain,
% 0.29/0.51 (~![Vr: vRow] : vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr, vrt2)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[18, 14])).
% 0.29/0.51 tff(20,plain,(
% 0.29/0.51 ~vwelltypedRawtable(vttempty, vprojectEmptyCol(vtcons(Vr!307, vrt2)))),
% 0.29/0.51 inference(skolemize,[status(sab)],[19])).
% 0.29/0.51 tff(21,plain,
% 0.29/0.51 (~vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[20, 13])).
% 0.29/0.51 tff(22,plain,
% 0.29/0.51 (^[Vtt: vTType, Vr: vRow, Vt1: vRawTable] : refl((~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))))),
% 0.29/0.51 inference(bind,[status(th)],[])).
% 0.29/0.51 tff(23,plain,
% 0.29/0.51 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))) <=> ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.29/0.51 inference(quant_intro,[status(thm)],[22])).
% 0.29/0.51 tff(24,plain,
% 0.29/0.51 (^[Vtt: vTType, Vr: vRow, Vt1: vRawTable] : trans(trans(monotonicity(rewrite((vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)) <=> (~((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))))), ((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (~((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))))))), rewrite((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (~((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))), ((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))))), rewrite((~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))), ((vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))))),
% 0.29/0.51 inference(bind,[status(th)],[])).
% 0.29/0.51 tff(25,plain,
% 0.29/0.51 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.29/0.51 inference(quant_intro,[status(thm)],[24])).
% 0.29/0.51 tff(26,plain,
% 0.29/0.51 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1))) <=> ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.29/0.51 inference(rewrite,[status(thm)],[])).
% 0.29/0.51 tff(27,axiom,(![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''welltypedRawtable-1'')).
% 0.29/0.51 tff(28,plain,
% 0.29/0.51 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.29/0.51 tff(29,plain,(
% 0.29/0.53 ![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (vwelltypedRawtable(Vtt, vtcons(Vr, Vt1)) <=> (vwelltypedRow(Vtt, Vr) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.29/0.53 inference(skolemize,[status(sab)],[28])).
% 0.29/0.53 tff(30,plain,
% 0.29/0.53 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.29/0.53 inference(modus_ponens,[status(thm)],[29, 25])).
% 0.29/0.53 tff(31,plain,
% 0.29/0.53 (![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))),
% 0.29/0.53 inference(modus_ponens,[status(thm)],[30, 23])).
% 0.29/0.53 tff(32,plain,
% 0.29/0.53 ((~![Vtt: vTType, Vr: vRow, Vt1: vRawTable] : (~(((~vwelltypedRow(Vtt, Vr)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedRawtable(Vtt, vtcons(Vr, Vt1))))) | (~(((~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2)))) <=> vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))))),
% 0.29/0.53 inference(quant_inst,[status(thm)],[])).
% 0.29/0.53 tff(33,plain,
% 0.29/0.53 (~(((~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2)))) <=> vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2))))),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[32, 31])).
% 0.29/0.53 tff(34,plain,
% 0.29/0.53 (vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2)) <=> vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2))),
% 0.29/0.53 inference(rewrite,[status(thm)],[])).
% 0.29/0.53 tff(35,axiom,(vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''welltypedEmptyProjection-tcons-IH0'')).
% 0.29/0.53 tff(36,plain,
% 0.29/0.53 (vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2))),
% 0.29/0.53 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.29/0.53 tff(37,plain,
% 0.29/0.53 (vwelltypedRow(vttempty, vrempty) <=> vwelltypedRow(vttempty, vrempty)),
% 0.29/0.53 inference(rewrite,[status(thm)],[])).
% 0.29/0.53 tff(38,axiom,(vwelltypedRow(vttempty, vrempty)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''welltypedRow-0'')).
% 0.29/0.53 tff(39,plain,
% 0.29/0.53 (vwelltypedRow(vttempty, vrempty)),
% 0.29/0.53 inference(modus_ponens,[status(thm)],[38, 37])).
% 0.29/0.53 tff(40,plain,
% 0.29/0.53 ((~((~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2))))) | (~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2)))),
% 0.29/0.53 inference(tautology,[status(thm)],[])).
% 0.29/0.53 tff(41,plain,
% 0.29/0.53 (~((~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2))))),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[40, 39, 36])).
% 0.29/0.53 tff(42,plain,
% 0.29/0.53 ((((~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2)))) <=> vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))) | ((~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2)))) | vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))),
% 0.29/0.53 inference(tautology,[status(thm)],[])).
% 0.29/0.53 tff(43,plain,
% 0.29/0.53 ((((~vwelltypedRow(vttempty, vrempty)) | (~vwelltypedRawtable(vttempty, vprojectEmptyCol(vrt2)))) <=> vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))) | vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[42, 41])).
% 0.29/0.53 tff(44,plain,
% 0.29/0.53 (vwelltypedRawtable(vttempty, vtcons(vrempty, vprojectEmptyCol(vrt2)))),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[43, 33])).
% 0.29/0.53 tff(45,plain,
% 0.29/0.53 ($false),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[44, 21])).
% 0.29/0.53 % SZS output end Proof
% 0.29/0.53 % E exiting
%------------------------------------------------------------------------------