%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM306_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n021.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.28s 0.50s
% Output : Proof 0.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : COM306_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.11 % Command : run_E %s %d THM
% 0.13/0.32 % Computer : n021.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Mon May 4 20:43:27 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.28/0.50 % SZS status Theorem
% 0.28/0.50 % SZS output start Proof
% 0.28/0.50 tff(vsomeRawTable_type, type, (
% 0.28/0.50 vsomeRawTable: vRawTable > vOptRawTable)).
% 0.28/0.50 tff(tptp_fun_Vrt2_307_type, type, (
% 0.28/0.50 tptp_fun_Vrt2_307: ( vAttrL * vRawTable * vAttrL ) > vRawTable)).
% 0.28/0.50 tff(tptp_fun_VwildcardName00_47_type, type, (
% 0.28/0.50 tptp_fun_VwildcardName00_47: vTable > vAttrL)).
% 0.28/0.50 tff(tptp_fun_Vt_310_type, type, (
% 0.28/0.50 tptp_fun_Vt_310: vTable)).
% 0.28/0.50 tff(tptp_fun_VwildcardName00_48_type, type, (
% 0.28/0.50 tptp_fun_VwildcardName00_48: vTable > vRawTable)).
% 0.28/0.50 tff(tptp_fun_Val_311_type, type, (
% 0.28/0.50 tptp_fun_Val_311: vAttrL)).
% 0.28/0.50 tff(vnoRawTable_type, type, (
% 0.28/0.50 vnoRawTable: vOptRawTable)).
% 0.28/0.50 tff(vprojectCols_type, type, (
% 0.28/0.50 vprojectCols: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable)).
% 0.28/0.50 tff(vsomeTType_type, type, (
% 0.28/0.50 vsomeTType: vTType > vOptTType)).
% 0.28/0.50 tff(tptp_fun_VwildcardName0_140_type, type, (
% 0.28/0.50 tptp_fun_VwildcardName0_140: vOptTType > vTType)).
% 0.28/0.50 tff(tptp_fun_Vtt2_308_type, type, (
% 0.28/0.50 tptp_fun_Vtt2_308: vTType)).
% 0.28/0.50 tff(vprojectTypeAttrL_type, type, (
% 0.28/0.50 vprojectTypeAttrL: ( vAttrL * vTType ) > vOptTType)).
% 0.28/0.50 tff(tptp_fun_Vtt_309_type, type, (
% 0.28/0.50 tptp_fun_Vtt_309: vTType)).
% 0.28/0.50 tff(visSomeTType_type, type, (
% 0.28/0.50 visSomeTType: vOptTType > $o)).
% 0.28/0.50 tff(vprojectType_type, type, (
% 0.28/0.50 vprojectType: ( vSelect * vTType ) > vOptTType)).
% 0.28/0.50 tff(vlist_type, type, (
% 0.28/0.50 vlist: vAttrL > vSelect)).
% 0.28/0.50 tff(vsomeTable_type, type, (
% 0.28/0.50 vsomeTable: vTable > vOptTable)).
% 0.28/0.50 tff(vprojectTable_type, type, (
% 0.28/0.50 vprojectTable: ( vSelect * vTable ) > vOptTable)).
% 0.28/0.50 tff(vwelltypedtable_type, type, (
% 0.28/0.50 vwelltypedtable: ( vTType * vTable ) > $o)).
% 0.28/0.50 tff(visSomeRawTable_type, type, (
% 0.28/0.50 visSomeRawTable: vOptRawTable > $o)).
% 0.28/0.50 tff(vgetRaw_type, type, (
% 0.28/0.50 vgetRaw: vTable > vRawTable)).
% 0.28/0.50 tff(vgetAttrL_type, type, (
% 0.28/0.50 vgetAttrL: vTable > vAttrL)).
% 0.28/0.50 tff(vwelltypedRawtable_type, type, (
% 0.28/0.50 vwelltypedRawtable: ( vTType * vRawTable ) > $o)).
% 0.28/0.50 tff(tptp_fun_Vt1_81_type, type, (
% 0.28/0.50 tptp_fun_Vt1_81: ( vTable * vTType ) > vRawTable)).
% 0.28/0.50 tff(vtable_type, type, (
% 0.28/0.50 vtable: ( vAttrL * vRawTable ) > vTable)).
% 0.28/0.50 tff(tptp_fun_Val_82_type, type, (
% 0.28/0.50 tptp_fun_Val_82: ( vTable * vTType ) > vAttrL)).
% 0.28/0.50 tff(vmatchingAttrL_type, type, (
% 0.28/0.50 vmatchingAttrL: ( vTType * vAttrL ) > $o)).
% 0.28/0.50 tff(1,plain,
% 0.28/0.50 (^[VwildcardName0: vTType] : refl(visSomeTType(vsomeTType(VwildcardName0)) <=> visSomeTType(vsomeTType(VwildcardName0)))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(2,plain,
% 0.28/0.50 (![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0)) <=> ![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[1])).
% 0.28/0.50 tff(3,plain,
% 0.28/0.50 (![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0)) <=> ![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(4,axiom,(![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''isSomeTType-1'')).
% 0.28/0.50 tff(5,plain,
% 0.28/0.50 (![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.28/0.50 tff(6,plain,(
% 0.28/0.50 ![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0))),
% 0.28/0.50 inference(skolemize,[status(sab)],[5])).
% 0.28/0.50 tff(7,plain,
% 0.28/0.50 (![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.28/0.50 tff(8,plain,
% 0.28/0.50 ((~![VwildcardName0: vTType] : visSomeTType(vsomeTType(VwildcardName0))) | visSomeTType(vsomeTType(Vtt2!308))),
% 0.28/0.50 inference(quant_inst,[status(thm)],[])).
% 0.28/0.50 tff(9,plain,
% 0.28/0.50 (visSomeTType(vsomeTType(Vtt2!308))),
% 0.28/0.50 inference(unit_resolution,[status(thm)],[8, 7])).
% 0.28/0.50 tff(10,plain,
% 0.28/0.50 (^[VOptTType0: vOptTType] : refl(((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0)))) <=> ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0)))))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(11,plain,
% 0.28/0.50 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0)))) <=> ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[10])).
% 0.28/0.50 tff(12,plain,
% 0.28/0.50 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))) <=> ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(13,plain,
% 0.28/0.50 (^[VOptTType0: vOptTType] : rewrite((visSomeTType(VOptTType0) => ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))) <=> ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(14,plain,
% 0.28/0.50 (![VOptTType0: vOptTType] : (visSomeTType(VOptTType0) => ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))) <=> ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[13])).
% 0.28/0.50 tff(15,axiom,(![VOptTType0: vOptTType] : (visSomeTType(VOptTType0) => ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''isSomeTType-true-INV'')).
% 0.28/0.50 tff(16,plain,
% 0.28/0.50 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.28/0.50 tff(17,plain,
% 0.28/0.50 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[16, 12])).
% 0.28/0.50 tff(18,plain,(
% 0.28/0.50 ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))),
% 0.28/0.50 inference(skolemize,[status(sab)],[17])).
% 0.28/0.50 tff(19,plain,
% 0.28/0.50 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[18, 11])).
% 0.28/0.50 tff(20,plain,
% 0.28/0.50 (((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | ((~visSomeTType(vsomeTType(Vtt2!308))) | (vsomeTType(Vtt2!308) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))))) <=> ((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | (~visSomeTType(vsomeTType(Vtt2!308))) | (vsomeTType(Vtt2!308) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(21,plain,
% 0.28/0.50 ((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | ((~visSomeTType(vsomeTType(Vtt2!308))) | (vsomeTType(Vtt2!308) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))))),
% 0.28/0.50 inference(quant_inst,[status(thm)],[])).
% 0.28/0.50 tff(22,plain,
% 0.28/0.50 ((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | (~visSomeTType(vsomeTType(Vtt2!308))) | (vsomeTType(Vtt2!308) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.28/0.50 tff(23,plain,
% 0.28/0.50 (vsomeTType(Vtt2!308) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))),
% 0.28/0.50 inference(unit_resolution,[status(thm)],[22, 19, 9])).
% 0.28/0.50 tff(24,plain,
% 0.28/0.50 ((((~visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)))) & vwelltypedtable(Vtt!309, Vt!310) & (vprojectType(vlist(Val!311), Vtt!309) = vsomeTType(Vtt2!308))) & ![Vt200: vTable] : (~(vprojectTable(vlist(Val!311), Vt!310) = vsomeTable(Vt200)))) <=> ((~visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)))) & vwelltypedtable(Vtt!309, Vt!310) & (vprojectType(vlist(Val!311), Vtt!309) = vsomeTType(Vtt2!308)) & ![Vt200: vTable] : (~(vprojectTable(vlist(Val!311), Vt!310) = vsomeTable(Vt200))))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(25,plain,
% 0.28/0.50 ((~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((~((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2)))) | ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200)))) <=> (~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((~((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2)))) | ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200))))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(26,plain,
% 0.28/0.50 ((~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt)) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2))) => ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200)))) <=> (~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((~((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2)))) | ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200))))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(27,axiom,(~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt)) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2))) => ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''projectTableProgress-list-isSomeRawTable-False'')).
% 0.28/0.50 tff(28,plain,
% 0.28/0.50 (~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((~((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2)))) | ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.28/0.50 tff(29,plain,
% 0.28/0.50 (~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((~((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2)))) | ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[28, 25])).
% 0.28/0.50 tff(30,plain,
% 0.28/0.50 (~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((~((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2)))) | ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[29, 25])).
% 0.28/0.50 tff(31,plain,
% 0.28/0.50 (~![Val: vAttrL, Vt: vTable, Vtt: vTType, Vtt2: vTType] : ((~((~visSomeRawTable(vprojectCols(Val, vgetAttrL(Vt), vgetRaw(Vt)))) & vwelltypedtable(Vtt, Vt) & (vprojectType(vlist(Val), Vtt) = vsomeTType(Vtt2)))) | ?[Vt200: vTable] : (vprojectTable(vlist(Val), Vt) = vsomeTable(Vt200)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[30, 25])).
% 0.28/0.50 tff(32,plain,
% 0.28/0.50 ((~visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)))) & vwelltypedtable(Vtt!309, Vt!310) & (vprojectType(vlist(Val!311), Vtt!309) = vsomeTType(Vtt2!308)) & ![Vt200: vTable] : (~(vprojectTable(vlist(Val!311), Vt!310) = vsomeTable(Vt200)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[31, 24])).
% 0.28/0.50 tff(33,plain,
% 0.28/0.50 (vprojectType(vlist(Val!311), Vtt!309) = vsomeTType(Vtt2!308)),
% 0.28/0.50 inference(and_elim,[status(thm)],[32])).
% 0.28/0.50 tff(34,plain,
% 0.28/0.50 (^[Val: vAttrL, Vtt1: vTType] : refl((vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1)) <=> (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1)))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(35,plain,
% 0.28/0.50 (![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1)) <=> ![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[34])).
% 0.28/0.50 tff(36,plain,
% 0.28/0.50 (![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1)) <=> ![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(37,axiom,(![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''projectType-1'')).
% 0.28/0.50 tff(38,plain,
% 0.28/0.50 (![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.28/0.50 tff(39,plain,(
% 0.28/0.50 ![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1))),
% 0.28/0.50 inference(skolemize,[status(sab)],[38])).
% 0.28/0.50 tff(40,plain,
% 0.28/0.50 (![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.28/0.50 tff(41,plain,
% 0.28/0.50 ((~![Val: vAttrL, Vtt1: vTType] : (vprojectType(vlist(Val), Vtt1) = vprojectTypeAttrL(Val, Vtt1))) | (vprojectType(vlist(Val!311), Vtt!309) = vprojectTypeAttrL(Val!311, Vtt!309))),
% 0.28/0.50 inference(quant_inst,[status(thm)],[])).
% 0.28/0.50 tff(42,plain,
% 0.28/0.50 (vprojectType(vlist(Val!311), Vtt!309) = vprojectTypeAttrL(Val!311, Vtt!309)),
% 0.28/0.50 inference(unit_resolution,[status(thm)],[41, 40])).
% 0.28/0.50 tff(43,plain,
% 0.28/0.50 (vprojectTypeAttrL(Val!311, Vtt!309) = vprojectType(vlist(Val!311), Vtt!309)),
% 0.28/0.50 inference(symmetry,[status(thm)],[42])).
% 0.28/0.50 tff(44,plain,
% 0.28/0.50 (vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))),
% 0.28/0.50 inference(transitivity,[status(thm)],[43, 33, 23])).
% 0.28/0.50 tff(45,plain,
% 0.28/0.50 (^[VTable0: vTable] : refl((VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0))) <=> (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0))))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(46,plain,
% 0.28/0.50 (![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0))) <=> ![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[45])).
% 0.28/0.50 tff(47,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00)) <=> ![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(48,plain,
% 0.28/0.50 (^[VTable0: vTable] : trans(der(?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0)) <=> ?[Val0: vAttrL, VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))), elim_unused(?[Val0: vAttrL, VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00)) <=> ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))), (?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0)) <=> ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(49,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0)) <=> ![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[48])).
% 0.28/0.50 tff(50,axiom,(![VTable0: vTable] : ?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getAttrL-INV'')).
% 0.28/0.50 tff(51,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.28/0.50 tff(52,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[51, 47])).
% 0.28/0.50 tff(53,plain,(
% 0.28/0.50 ![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))),
% 0.28/0.50 inference(skolemize,[status(sab)],[52])).
% 0.28/0.50 tff(54,plain,
% 0.28/0.50 (![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[53, 46])).
% 0.28/0.50 tff(55,plain,
% 0.28/0.50 ((~![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))) | (Vt!310 = vtable(vgetAttrL(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)))),
% 0.28/0.50 inference(quant_inst,[status(thm)],[])).
% 0.28/0.50 tff(56,plain,
% 0.28/0.50 (Vt!310 = vtable(vgetAttrL(Vt!310), tptp_fun_VwildcardName00_48(Vt!310))),
% 0.28/0.50 inference(unit_resolution,[status(thm)],[55, 54])).
% 0.28/0.50 tff(57,plain,
% 0.28/0.50 (^[VTable0: vTable] : refl((VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0))) <=> (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0))))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(58,plain,
% 0.28/0.50 (![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0))) <=> ![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[57])).
% 0.28/0.50 tff(59,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0))) <=> ![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.28/0.50 inference(rewrite,[status(thm)],[])).
% 0.28/0.50 tff(60,plain,
% 0.28/0.50 (^[VTable0: vTable] : trans(der(?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0)) <=> ?[VwildcardName00: vAttrL, Vrt0: vRawTable] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))), elim_unused(?[VwildcardName00: vAttrL, Vrt0: vRawTable] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0))) <=> ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))), (?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0)) <=> ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))))),
% 0.28/0.50 inference(bind,[status(th)],[])).
% 0.28/0.50 tff(61,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0)) <=> ![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.28/0.50 inference(quant_intro,[status(thm)],[60])).
% 0.28/0.50 tff(62,axiom,(![VTable0: vTable] : ?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getRaw-INV'')).
% 0.28/0.50 tff(63,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.28/0.50 tff(64,plain,
% 0.28/0.50 (![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[63, 59])).
% 0.28/0.50 tff(65,plain,(
% 0.28/0.50 ![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))),
% 0.28/0.50 inference(skolemize,[status(sab)],[64])).
% 0.28/0.50 tff(66,plain,
% 0.28/0.50 (![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))),
% 0.28/0.50 inference(modus_ponens,[status(thm)],[65, 58])).
% 0.28/0.50 tff(67,plain,
% 0.28/0.50 ((~![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))) | (Vt!310 = vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)))),
% 0.28/0.50 inference(quant_inst,[status(thm)],[])).
% 0.28/0.50 tff(68,plain,
% 0.28/0.50 (Vt!310 = vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310))),
% 0.28/0.50 inference(unit_resolution,[status(thm)],[67, 66])).
% 0.28/0.50 tff(69,plain,
% 0.28/0.50 (vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = Vt!310),
% 0.28/0.50 inference(symmetry,[status(thm)],[68])).
% 0.28/0.50 tff(70,plain,
% 0.28/0.50 (vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(vgetAttrL(Vt!310), tptp_fun_VwildcardName00_48(Vt!310))),
% 0.28/0.51 inference(transitivity,[status(thm)],[69, 56])).
% 0.28/0.51 tff(71,plain,
% 0.28/0.51 (^[VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : refl(((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))) <=> ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(72,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[71])).
% 0.28/0.51 tff(73,plain,
% 0.28/0.51 (^[VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : rewrite(((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(74,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[73])).
% 0.28/0.51 tff(75,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(76,plain,
% 0.28/0.51 (^[VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : rewrite(((vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1)) => ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(77,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1)) => ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[76])).
% 0.28/0.51 tff(78,axiom,(![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1)) => ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''EQ-table'')).
% 0.28/0.51 tff(79,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.28/0.51 tff(80,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[79, 75])).
% 0.28/0.51 tff(81,plain,(
% 0.28/0.51 ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.28/0.51 inference(skolemize,[status(sab)],[80])).
% 0.28/0.51 tff(82,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[81, 74])).
% 0.28/0.51 tff(83,plain,
% 0.28/0.51 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[82, 72])).
% 0.28/0.51 tff(84,plain,
% 0.28/0.51 (((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | ((~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(vgetAttrL(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))) | (~(vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310))))))) <=> ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | (~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(vgetAttrL(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))) | (~(vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310))))))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(85,plain,
% 0.28/0.51 ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | ((~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(vgetAttrL(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))) | (~(vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310))))))),
% 0.28/0.51 inference(quant_inst,[status(thm)],[])).
% 0.28/0.51 tff(86,plain,
% 0.28/0.51 ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | (~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(vgetAttrL(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))) | (~(vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310)))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.28/0.51 tff(87,plain,
% 0.28/0.51 (~((~(tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))) | (~(vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310))))),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[86, 83, 70])).
% 0.28/0.51 tff(88,plain,
% 0.28/0.51 (((~(tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))) | (~(vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310)))) | (vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310))),
% 0.28/0.51 inference(tautology,[status(thm)],[])).
% 0.28/0.51 tff(89,plain,
% 0.28/0.51 (vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310)),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[88, 87])).
% 0.28/0.51 tff(90,plain,
% 0.28/0.51 (vwelltypedtable(Vtt!309, Vt!310)),
% 0.28/0.51 inference(and_elim,[status(thm)],[32])).
% 0.28/0.51 tff(91,plain,
% 0.28/0.51 (^[VTType0: vTType, VTable0: vTable] : refl(((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0)))))) <=> ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0)))))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(92,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0)))))) <=> ![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[91])).
% 0.28/0.51 tff(93,plain,
% 0.28/0.51 (^[VTType0: vTType, VTable0: vTable] : rewrite(((~vwelltypedtable(VTType0, VTable0)) | (vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0)) & (VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0))) & vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0)))) <=> ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0)))))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(94,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0)) & (VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0))) & vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0)))) <=> ![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[93])).
% 0.28/0.51 tff(95,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val))) <=> ![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(96,plain,
% 0.28/0.51 (^[VTType0: vTType, VTable0: vTable] : trans(monotonicity(trans(quant_intro(proof_bind(^[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : trans(monotonicity(rewrite((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) <=> ((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val))), (((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1)) <=> (((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1)))), rewrite((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1)) <=> ((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1))), (((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1)) <=> ((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1))))), (?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1)) <=> ?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)))), trans(der(?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)) <=> ?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val))), elim_unused(?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)) <=> ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val))), (?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)) <=> ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))), (?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1)) <=> ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))), ((vwelltypedtable(VTType0, VTable0) => ?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1))) <=> (vwelltypedtable(VTType0, VTable0) => ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val))))), rewrite((vwelltypedtable(VTType0, VTable0) => ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val))) <=> ((~vwelltypedtable(VTType0, VTable0)) | ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))), ((vwelltypedtable(VTType0, VTable0) => ?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1))) <=> ((~vwelltypedtable(VTType0, VTable0)) | ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(97,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : (vwelltypedtable(VTType0, VTable0) => ?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1))) <=> ![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[96])).
% 0.28/0.51 tff(98,axiom,(![VTType0: vTType, VTable0: vTable] : (vwelltypedtable(VTType0, VTable0) => ?[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : ((((VTType0 = Vtt) & (VTable0 = vtable(Val, Vt1))) & vmatchingAttrL(Vtt, Val)) & vwelltypedRawtable(Vtt, Vt1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''welltypedtable-true-INV'')).
% 0.28/0.51 tff(99,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[98, 97])).
% 0.28/0.51 tff(100,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | ?[Val: vAttrL, Vt1: vRawTable] : (vwelltypedRawtable(VTType0, Vt1) & (VTable0 = vtable(Val, Vt1)) & vmatchingAttrL(VTType0, Val)))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[99, 95])).
% 0.28/0.51 tff(101,plain,(
% 0.28/0.51 ![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0)) & (VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0))) & vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))),
% 0.28/0.51 inference(skolemize,[status(sab)],[100])).
% 0.28/0.51 tff(102,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[101, 94])).
% 0.28/0.51 tff(103,plain,
% 0.28/0.51 (![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[102, 92])).
% 0.28/0.51 tff(104,plain,
% 0.28/0.51 (((~![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))) | ((~vwelltypedtable(Vtt!309, Vt!310)) | (~((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309))))))) <=> ((~![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))) | (~vwelltypedtable(Vtt!309, Vt!310)) | (~((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309))))))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(105,plain,
% 0.28/0.51 ((~![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))) | ((~vwelltypedtable(Vtt!309, Vt!310)) | (~((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309))))))),
% 0.28/0.51 inference(quant_inst,[status(thm)],[])).
% 0.28/0.51 tff(106,plain,
% 0.28/0.51 ((~![VTType0: vTType, VTable0: vTable] : ((~vwelltypedtable(VTType0, VTable0)) | (~((~vwelltypedRawtable(VTType0, tptp_fun_Vt1_81(VTable0, VTType0))) | (~(VTable0 = vtable(tptp_fun_Val_82(VTable0, VTType0), tptp_fun_Vt1_81(VTable0, VTType0)))) | (~vmatchingAttrL(VTType0, tptp_fun_Val_82(VTable0, VTType0))))))) | (~vwelltypedtable(Vtt!309, Vt!310)) | (~((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309)))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[105, 104])).
% 0.28/0.51 tff(107,plain,
% 0.28/0.51 (~((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309))))),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[106, 103, 90])).
% 0.28/0.51 tff(108,plain,
% 0.28/0.51 (((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309)))) | (Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))),
% 0.28/0.51 inference(tautology,[status(thm)],[])).
% 0.28/0.51 tff(109,plain,
% 0.28/0.51 (Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309))),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[108, 107])).
% 0.28/0.51 tff(110,plain,
% 0.28/0.51 (vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309))),
% 0.28/0.51 inference(transitivity,[status(thm)],[69, 109])).
% 0.28/0.51 tff(111,plain,
% 0.28/0.51 (((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | ((~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))) | (~(vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309))))))) <=> ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | (~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))) | (~(vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309))))))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(112,plain,
% 0.28/0.51 ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | ((~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))) | (~(vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309))))))),
% 0.28/0.51 inference(quant_inst,[status(thm)],[])).
% 0.28/0.51 tff(113,plain,
% 0.28/0.51 ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | (~(vtable(tptp_fun_VwildcardName00_47(Vt!310), vgetRaw(Vt!310)) = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~((~(tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))) | (~(vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309)))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[112, 111])).
% 0.28/0.51 tff(114,plain,
% 0.28/0.51 (~((~(tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))) | (~(vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309))))),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[113, 83, 110])).
% 0.28/0.51 tff(115,plain,
% 0.28/0.51 (((~(tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))) | (~(vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309))),
% 0.28/0.51 inference(tautology,[status(thm)],[])).
% 0.28/0.51 tff(116,plain,
% 0.28/0.51 (vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309)),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[115, 114])).
% 0.28/0.51 tff(117,plain,
% 0.28/0.51 (tptp_fun_Vt1_81(Vt!310, Vtt!309) = vgetRaw(Vt!310)),
% 0.28/0.51 inference(symmetry,[status(thm)],[116])).
% 0.28/0.51 tff(118,plain,
% 0.28/0.51 (tptp_fun_Vt1_81(Vt!310, Vtt!309) = tptp_fun_VwildcardName00_48(Vt!310)),
% 0.28/0.51 inference(transitivity,[status(thm)],[117, 89])).
% 0.28/0.51 tff(119,plain,
% 0.28/0.51 (vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309)) <=> vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))),
% 0.28/0.51 inference(monotonicity,[status(thm)],[118])).
% 0.28/0.51 tff(120,plain,
% 0.28/0.51 (((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309)))) | vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))),
% 0.28/0.51 inference(tautology,[status(thm)],[])).
% 0.28/0.51 tff(121,plain,
% 0.28/0.51 (vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[120, 107])).
% 0.28/0.51 tff(122,plain,
% 0.28/0.51 (vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[121, 119])).
% 0.28/0.51 tff(123,plain,
% 0.28/0.51 (((~(tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))) | (~(vgetRaw(Vt!310) = tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309))),
% 0.28/0.51 inference(tautology,[status(thm)],[])).
% 0.28/0.51 tff(124,plain,
% 0.28/0.51 (tptp_fun_VwildcardName00_47(Vt!310) = tptp_fun_Val_82(Vt!310, Vtt!309)),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[123, 114])).
% 0.28/0.51 tff(125,plain,
% 0.28/0.51 (tptp_fun_Val_82(Vt!310, Vtt!309) = tptp_fun_VwildcardName00_47(Vt!310)),
% 0.28/0.51 inference(symmetry,[status(thm)],[124])).
% 0.28/0.51 tff(126,plain,
% 0.28/0.51 (vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309)) <=> vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))),
% 0.28/0.51 inference(monotonicity,[status(thm)],[125])).
% 0.28/0.51 tff(127,plain,
% 0.28/0.51 (((~vwelltypedRawtable(Vtt!309, tptp_fun_Vt1_81(Vt!310, Vtt!309))) | (~(Vt!310 = vtable(tptp_fun_Val_82(Vt!310, Vtt!309), tptp_fun_Vt1_81(Vt!310, Vtt!309)))) | (~vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309)))) | vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309))),
% 0.28/0.51 inference(tautology,[status(thm)],[])).
% 0.28/0.51 tff(128,plain,
% 0.28/0.51 (vmatchingAttrL(Vtt!309, tptp_fun_Val_82(Vt!310, Vtt!309))),
% 0.28/0.51 inference(unit_resolution,[status(thm)],[127, 107])).
% 0.28/0.51 tff(129,plain,
% 0.28/0.51 (vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[128, 126])).
% 0.28/0.51 tff(130,plain,
% 0.28/0.51 (^[Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : refl(((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) <=> ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(131,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) <=> ![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[130])).
% 0.28/0.51 tff(132,plain,
% 0.28/0.51 (^[Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : trans(monotonicity(trans(monotonicity(rewrite((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) <=> (~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) <=> (~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))))))), rewrite((~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt)))) <=> (((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt)))))), rewrite((((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt)))) <=> ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt)))) <=> ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(133,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt)))) <=> ![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[132])).
% 0.28/0.51 tff(134,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2))) <=> ![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2)))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(135,plain,
% 0.28/0.51 (^[Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : trans(monotonicity(rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) <=> (vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) => ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2))) <=> ((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) => ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2))))), rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) => ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) => ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2)))))),
% 0.28/0.51 inference(bind,[status(th)],[])).
% 0.28/0.51 tff(136,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) => ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2))) <=> ![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2)))),
% 0.28/0.51 inference(quant_intro,[status(thm)],[135])).
% 0.28/0.51 tff(137,axiom,(![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))) => ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','projectColsProgress')).
% 0.28/0.51 tff(138,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2)))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.28/0.51 tff(139,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2: vRawTable] : (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(Vrt2)))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[138, 134])).
% 0.28/0.51 tff(140,plain,(
% 0.28/0.51 ![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))))),
% 0.28/0.51 inference(skolemize,[status(sab)],[139])).
% 0.28/0.51 tff(141,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[140, 133])).
% 0.28/0.51 tff(142,plain,
% 0.28/0.51 (![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))),
% 0.28/0.51 inference(modus_ponens,[status(thm)],[141, 131])).
% 0.28/0.51 tff(143,plain,
% 0.28/0.51 (((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | ((~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))))) <=> ((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | (~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(144,plain,
% 0.28/0.51 (((vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))))) <=> ((~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))))),
% 0.28/0.51 inference(rewrite,[status(thm)],[])).
% 0.28/0.51 tff(145,plain,
% 0.28/0.51 (((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | ((vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))))) <=> ((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | ((~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))))))),
% 0.28/0.51 inference(monotonicity,[status(thm)],[144])).
% 0.28/0.51 tff(146,plain,
% 0.28/0.51 (((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | ((vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))))) <=> ((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | (~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))))),
% 0.28/0.51 inference(transitivity,[status(thm)],[145, 143])).
% 0.28/0.51 tff(147,plain,
% 0.28/0.51 ((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | ((vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308))))))),
% 0.28/0.52 inference(quant_inst,[status(thm)],[])).
% 0.28/0.52 tff(148,plain,
% 0.28/0.52 ((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val: vAttrL, Vtt: vTType] : ((vprojectCols(Val, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt2_307(Val, Vrt, Valt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(Val, Vtt) = vsomeTType(Vtt2))))) | (~vmatchingAttrL(Vtt!309, tptp_fun_VwildcardName00_47(Vt!310))) | (~vwelltypedRawtable(Vtt!309, tptp_fun_VwildcardName00_48(Vt!310))) | (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))) | (~(vprojectTypeAttrL(Val!311, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vsomeTType(Vtt2!308)))))),
% 0.28/0.52 inference(modus_ponens,[status(thm)],[147, 146])).
% 0.28/0.52 tff(149,plain,
% 0.28/0.52 (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))),
% 0.28/0.52 inference(unit_resolution,[status(thm)],[148, 142, 129, 122, 44])).
% 0.28/0.52 tff(150,plain,
% 0.28/0.52 (tptp_fun_VwildcardName00_48(Vt!310) = vgetRaw(Vt!310)),
% 0.28/0.52 inference(symmetry,[status(thm)],[89])).
% 0.28/0.52 tff(151,plain,
% 0.28/0.52 (((~(tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))) | (~(vgetRaw(Vt!310) = tptp_fun_VwildcardName00_48(Vt!310)))) | (tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310))),
% 0.28/0.52 inference(tautology,[status(thm)],[])).
% 0.28/0.52 tff(152,plain,
% 0.28/0.52 (tptp_fun_VwildcardName00_47(Vt!310) = vgetAttrL(Vt!310)),
% 0.28/0.52 inference(unit_resolution,[status(thm)],[151, 87])).
% 0.28/0.52 tff(153,plain,
% 0.28/0.52 (vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310)) = vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310))),
% 0.28/0.52 inference(monotonicity,[status(thm)],[152, 150])).
% 0.28/0.52 tff(154,plain,
% 0.28/0.52 (vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)) = vprojectCols(Val!311, tptp_fun_VwildcardName00_47(Vt!310), tptp_fun_VwildcardName00_48(Vt!310))),
% 0.28/0.52 inference(symmetry,[status(thm)],[153])).
% 0.28/0.52 tff(155,plain,
% 0.28/0.52 (~visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)))),
% 0.28/0.52 inference(and_elim,[status(thm)],[32])).
% 0.28/0.52 tff(156,plain,
% 0.28/0.52 (^[VOptRawTable0: vOptRawTable] : refl((visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)) <=> (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)))),
% 0.28/0.52 inference(bind,[status(th)],[])).
% 0.28/0.52 tff(157,plain,
% 0.28/0.52 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)) <=> ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 0.28/0.52 inference(quant_intro,[status(thm)],[156])).
% 0.28/0.52 tff(158,plain,
% 0.28/0.52 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)) <=> ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 0.28/0.52 inference(rewrite,[status(thm)],[])).
% 0.28/0.52 tff(159,plain,
% 0.28/0.52 (^[VOptRawTable0: vOptRawTable] : rewrite(((~visSomeRawTable(VOptRawTable0)) => (VOptRawTable0 = vnoRawTable)) <=> (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)))),
% 0.28/0.52 inference(bind,[status(th)],[])).
% 0.28/0.52 tff(160,plain,
% 0.28/0.52 (![VOptRawTable0: vOptRawTable] : ((~visSomeRawTable(VOptRawTable0)) => (VOptRawTable0 = vnoRawTable)) <=> ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 0.28/0.52 inference(quant_intro,[status(thm)],[159])).
% 0.28/0.52 tff(161,axiom,(![VOptRawTable0: vOptRawTable] : ((~visSomeRawTable(VOptRawTable0)) => (VOptRawTable0 = vnoRawTable))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''isSomeRawTable-false-INV'')).
% 0.28/0.52 tff(162,plain,
% 0.28/0.52 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 0.28/0.52 inference(modus_ponens,[status(thm)],[161, 160])).
% 0.28/0.52 tff(163,plain,
% 0.28/0.52 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 0.28/0.52 inference(modus_ponens,[status(thm)],[162, 158])).
% 0.28/0.52 tff(164,plain,(
% 0.28/0.52 ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 0.28/0.52 inference(skolemize,[status(sab)],[163])).
% 0.28/0.52 tff(165,plain,
% 0.28/0.52 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 0.28/0.52 inference(modus_ponens,[status(thm)],[164, 157])).
% 0.28/0.52 tff(166,plain,
% 0.28/0.52 (((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | (visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310))) | (vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)) = vnoRawTable))) <=> ((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310))) | (vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)) = vnoRawTable))),
% 0.28/0.52 inference(rewrite,[status(thm)],[])).
% 0.28/0.52 tff(167,plain,
% 0.28/0.52 ((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | (visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310))) | (vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)) = vnoRawTable))),
% 0.28/0.52 inference(quant_inst,[status(thm)],[])).
% 0.28/0.52 tff(168,plain,
% 0.28/0.52 ((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | visSomeRawTable(vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310))) | (vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)) = vnoRawTable)),
% 0.28/0.52 inference(modus_ponens,[status(thm)],[167, 166])).
% 0.28/0.52 tff(169,plain,
% 0.28/0.52 (vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310)) = vnoRawTable),
% 0.28/0.52 inference(unit_resolution,[status(thm)],[168, 165, 155])).
% 0.28/0.52 tff(170,plain,
% 0.28/0.52 (vnoRawTable = vprojectCols(Val!311, vgetAttrL(Vt!310), vgetRaw(Vt!310))),
% 0.28/0.52 inference(symmetry,[status(thm)],[169])).
% 0.28/0.52 tff(171,plain,
% 0.28/0.52 (vnoRawTable = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))),
% 0.28/0.52 inference(transitivity,[status(thm)],[170, 154, 149])).
% 0.28/0.52 tff(172,plain,
% 0.28/0.52 (^[VRawTable0: vRawTable] : refl((~(vnoRawTable = vsomeRawTable(VRawTable0))) <=> (~(vnoRawTable = vsomeRawTable(VRawTable0))))),
% 0.28/0.52 inference(bind,[status(th)],[])).
% 0.28/0.52 tff(173,plain,
% 0.28/0.52 (![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0))) <=> ![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0)))),
% 0.28/0.52 inference(quant_intro,[status(thm)],[172])).
% 0.28/0.52 tff(174,plain,
% 0.28/0.52 (![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0))) <=> ![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0)))),
% 0.28/0.52 inference(rewrite,[status(thm)],[])).
% 0.28/0.52 tff(175,axiom,(![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''DIFF-noRawTable-someRawTable'')).
% 0.28/0.52 tff(176,plain,
% 0.28/0.52 (![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0)))),
% 0.28/0.52 inference(modus_ponens,[status(thm)],[175, 174])).
% 0.28/0.52 tff(177,plain,(
% 0.28/0.52 ![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0)))),
% 0.28/0.52 inference(skolemize,[status(sab)],[176])).
% 0.28/0.52 tff(178,plain,
% 0.28/0.52 (![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0)))),
% 0.28/0.52 inference(modus_ponens,[status(thm)],[177, 173])).
% 0.28/0.52 tff(179,plain,
% 0.28/0.52 ((~![VRawTable0: vRawTable] : (~(vnoRawTable = vsomeRawTable(VRawTable0)))) | (~(vnoRawTable = vsomeRawTable(tptp_fun_Vrt2_307(Val!311, tptp_fun_VwildcardName00_48(Vt!310), tptp_fun_VwildcardName00_47(Vt!310)))))),
% 0.28/0.52 inference(quant_inst,[status(thm)],[])).
% 0.28/0.53 tff(180,plain,
% 0.28/0.53 ($false),
% 0.28/0.53 inference(unit_resolution,[status(thm)],[179, 178, 171])).
% 0.28/0.53 % SZS output end Proof
% 0.28/0.54 % E exiting
%------------------------------------------------------------------------------