%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM301_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.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:07 PM UTC 2026
% Result : Theorem 2.93s 3.19s
% Output : Proof 3.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : COM301_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.09 % Command : run_E %s %d THM
% 0.13/0.29 % Computer : n016.cluster.edu
% 0.13/0.29 % Model : x86_64 x86_64
% 0.13/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.29 % Memory : 8042.1875MB
% 0.13/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.29 % CPULimit : 300
% 0.13/0.29 % WCLimit : 300
% 0.13/0.29 % DateTime : Mon May 4 20:36:52 EDT 2026
% 0.13/0.29 % CPUTime :
% 2.93/3.19 % SZS status Theorem
% 2.93/3.19 % SZS output start Proof
% 2.93/3.19 tff(vsomeRawTable_type, type, (
% 2.93/3.19 vsomeRawTable: vRawTable > vOptRawTable)).
% 2.93/3.19 tff(tptp_fun_Vrt2_308_type, type, (
% 2.93/3.19 tptp_fun_Vrt2_308: ( vName * vAttrL * vRawTable ) > vRawTable)).
% 2.93/3.19 tff(tptp_fun_Vrt_313_type, type, (
% 2.93/3.19 tptp_fun_Vrt_313: vRawTable)).
% 2.93/3.19 tff(tptp_fun_Valt_314_type, type, (
% 2.93/3.19 tptp_fun_Valt_314: vAttrL)).
% 2.93/3.19 tff(tptp_fun_Vn_310_type, type, (
% 2.93/3.19 tptp_fun_Vn_310: vName)).
% 2.93/3.19 tff(vprojectCols_type, type, (
% 2.93/3.19 vprojectCols: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable)).
% 2.93/3.19 tff(vacons_type, type, (
% 2.93/3.19 vacons: ( vName * vAttrL ) > vAttrL)).
% 2.93/3.19 tff(val1_type, type, (
% 2.93/3.19 val1: vAttrL)).
% 2.93/3.19 tff(vfindCol_type, type, (
% 2.93/3.19 vfindCol: ( vName * vAttrL * vRawTable ) > vOptRawTable)).
% 2.93/3.19 tff(vsomeFType_type, type, (
% 2.93/3.19 vsomeFType: vFType > vOptFType)).
% 2.93/3.19 tff(vgetFType_type, type, (
% 2.93/3.19 vgetFType: vOptFType > vFType)).
% 2.93/3.19 tff(vfindColType_type, type, (
% 2.93/3.19 vfindColType: ( vName * vTType ) > vOptFType)).
% 2.93/3.19 tff(tptp_fun_Vtt_309_type, type, (
% 2.93/3.19 tptp_fun_Vtt_309: vTType)).
% 2.93/3.19 tff(tptp_fun_Va_251_type, type, (
% 2.93/3.19 tptp_fun_Va_251: vOptFType > vFType)).
% 2.93/3.19 tff(visSomeFType_type, type, (
% 2.93/3.19 visSomeFType: vOptFType > $o)).
% 2.93/3.19 tff(visSomeTType_type, type, (
% 2.93/3.19 visSomeTType: vOptTType > $o)).
% 2.93/3.19 tff(vprojectTypeAttrL_type, type, (
% 2.93/3.19 vprojectTypeAttrL: ( vAttrL * vTType ) > vOptTType)).
% 2.93/3.19 tff(vnoTType_type, type, (
% 2.93/3.19 vnoTType: vOptTType)).
% 2.93/3.19 tff(vsomeTType_type, type, (
% 2.93/3.19 vsomeTType: vTType > vOptTType)).
% 2.93/3.19 tff(tptp_fun_Vtt2_312_type, type, (
% 2.93/3.19 tptp_fun_Vtt2_312: vTType)).
% 2.93/3.19 tff(vmatchingAttrL_type, type, (
% 2.93/3.19 vmatchingAttrL: ( vTType * vAttrL ) > $o)).
% 2.93/3.19 tff(vwelltypedRawtable_type, type, (
% 2.93/3.19 vwelltypedRawtable: ( vTType * vRawTable ) > $o)).
% 2.93/3.19 tff(visSomeRawTable_type, type, (
% 2.93/3.19 visSomeRawTable: vOptRawTable > $o)).
% 2.93/3.19 tff(tptp_fun_Val2_311_type, type, (
% 2.93/3.19 tptp_fun_Val2_311: vAttrL)).
% 2.93/3.19 tff(vnoRawTable_type, type, (
% 2.93/3.19 vnoRawTable: vOptRawTable)).
% 2.93/3.19 tff(tptp_fun_Vn1_162_type, type, (
% 2.93/3.19 tptp_fun_Vn1_162: ( vRawTable * vAttrL * vAttrL ) > vName)).
% 2.93/3.19 tff(tptp_fun_Val21_163_type, type, (
% 2.93/3.19 tptp_fun_Val21_163: ( vRawTable * vAttrL * vAttrL ) > vAttrL)).
% 2.93/3.20 tff(tptp_fun_Val20_165_type, type, (
% 2.93/3.20 tptp_fun_Val20_165: ( vRawTable * vAttrL * vAttrL ) > vAttrL)).
% 2.93/3.20 tff(tptp_fun_Vn0_164_type, type, (
% 2.93/3.20 tptp_fun_Vn0_164: ( vRawTable * vAttrL * vAttrL ) > vName)).
% 2.93/3.20 tff(vattachColToFrontRaw_type, type, (
% 2.93/3.20 vattachColToFrontRaw: ( vRawTable * vRawTable ) > vRawTable)).
% 2.93/3.20 tff(vgetRawTable_type, type, (
% 2.93/3.20 vgetRawTable: vOptRawTable > vRawTable)).
% 2.93/3.20 tff(vprojectEmptyCol_type, type, (
% 2.93/3.20 vprojectEmptyCol: vRawTable > vRawTable)).
% 2.93/3.20 tff(vaempty_type, type, (
% 2.93/3.20 vaempty: vAttrL)).
% 2.93/3.20 tff(tptp_fun_Vrt20_307_type, type, (
% 2.93/3.20 tptp_fun_Vrt20_307: ( vAttrL * vRawTable ) > vRawTable)).
% 2.93/3.20 tff(tptp_fun_VwildcardName0_140_type, type, (
% 2.93/3.20 tptp_fun_VwildcardName0_140: vOptTType > vTType)).
% 2.93/3.20 tff(1,plain,
% 2.93/3.20 ((vsomeTType(Vtt2!312) = vnoTType) <=> (vnoTType = vsomeTType(Vtt2!312))),
% 2.93/3.20 inference(commutativity,[status(thm)],[])).
% 2.93/3.20 tff(2,plain,
% 2.93/3.20 ((((~(visSomeRawTable(vfindCol(Vn!310, val1, Vrt!313)) & visSomeRawTable(vprojectCols(Val2!311, val1, Vrt!313)))) & vwelltypedRawtable(Vtt!309, Vrt!313) & vmatchingAttrL(Vtt!309, Valt!314) & (vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vsomeTType(Vtt2!312))) & ![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000)))) <=> ((~(visSomeRawTable(vfindCol(Vn!310, val1, Vrt!313)) & visSomeRawTable(vprojectCols(Val2!311, val1, Vrt!313)))) & vwelltypedRawtable(Vtt!309, Vrt!313) & vmatchingAttrL(Vtt!309, Valt!314) & (vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vsomeTType(Vtt2!312)) & ![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000))))),
% 2.93/3.20 inference(rewrite,[status(thm)],[])).
% 2.93/3.20 tff(3,plain,
% 2.93/3.20 ((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : ((~((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000)))) <=> (~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : ((~((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000))))),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(4,plain,
% 3.00/3.20 ((~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : (((((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt)) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2))) => ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000)))) <=> (~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : ((~((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000))))),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(5,axiom,(~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : (((((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt)) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2))) => ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''projectColsProgress-acons-isSomeRawTable-isSomeRawTable-False'')).
% 3.00/3.20 tff(6,plain,
% 3.00/3.20 (~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : ((~((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[5, 4])).
% 3.00/3.20 tff(7,plain,
% 3.00/3.20 (~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : ((~((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[6, 3])).
% 3.00/3.20 tff(8,plain,
% 3.00/3.20 (~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : ((~((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[7, 3])).
% 3.00/3.20 tff(9,plain,
% 3.00/3.20 (~![Valt: vAttrL, Vrt: vRawTable, Vtt2: vTType, Val2: vAttrL, Vn: vName, Vtt: vTType] : ((~((~(visSomeRawTable(vfindCol(Vn, val1, Vrt)) & visSomeRawTable(vprojectCols(Val2, val1, Vrt)))) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(vacons(Vn, val1), Vtt) = vsomeTType(Vtt2)))) | ?[Vrt2000: vRawTable] : (vprojectCols(vacons(Vn, val1), Valt, Vrt) = vsomeRawTable(Vrt2000)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[8, 3])).
% 3.00/3.20 tff(10,plain,
% 3.00/3.20 ((~(visSomeRawTable(vfindCol(Vn!310, val1, Vrt!313)) & visSomeRawTable(vprojectCols(Val2!311, val1, Vrt!313)))) & vwelltypedRawtable(Vtt!309, Vrt!313) & vmatchingAttrL(Vtt!309, Valt!314) & (vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vsomeTType(Vtt2!312)) & ![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[9, 2])).
% 3.00/3.20 tff(11,plain,
% 3.00/3.20 (vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vsomeTType(Vtt2!312)),
% 3.00/3.20 inference(and_elim,[status(thm)],[10])).
% 3.00/3.20 tff(12,plain,
% 3.00/3.20 ((vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType) <=> (vsomeTType(Vtt2!312) = vnoTType)),
% 3.00/3.20 inference(monotonicity,[status(thm)],[11])).
% 3.00/3.20 tff(13,plain,
% 3.00/3.20 ((vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType) <=> (vnoTType = vsomeTType(Vtt2!312))),
% 3.00/3.20 inference(transitivity,[status(thm)],[12, 1])).
% 3.00/3.20 tff(14,plain,
% 3.00/3.20 ((vnoTType = vsomeTType(Vtt2!312)) <=> (vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType)),
% 3.00/3.20 inference(symmetry,[status(thm)],[13])).
% 3.00/3.20 tff(15,plain,
% 3.00/3.20 ((~(vnoTType = vsomeTType(Vtt2!312))) <=> (~(vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType))),
% 3.00/3.20 inference(monotonicity,[status(thm)],[14])).
% 3.00/3.20 tff(16,plain,
% 3.00/3.20 (^[VTType0: vTType] : refl((~(vnoTType = vsomeTType(VTType0))) <=> (~(vnoTType = vsomeTType(VTType0))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(17,plain,
% 3.00/3.20 (![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0))) <=> ![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0)))),
% 3.00/3.20 inference(quant_intro,[status(thm)],[16])).
% 3.00/3.20 tff(18,plain,
% 3.00/3.20 (![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0))) <=> ![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0)))),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(19,axiom,(![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''DIFF-noTType-someTType'')).
% 3.00/3.20 tff(20,plain,
% 3.00/3.20 (![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[19, 18])).
% 3.00/3.20 tff(21,plain,(
% 3.00/3.20 ![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0)))),
% 3.00/3.20 inference(skolemize,[status(sab)],[20])).
% 3.00/3.20 tff(22,plain,
% 3.00/3.20 (![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[21, 17])).
% 3.00/3.20 tff(23,plain,
% 3.00/3.20 ((~![VTType0: vTType] : (~(vnoTType = vsomeTType(VTType0)))) | (~(vnoTType = vsomeTType(Vtt2!312)))),
% 3.00/3.20 inference(quant_inst,[status(thm)],[])).
% 3.00/3.20 tff(24,plain,
% 3.00/3.20 (~(vnoTType = vsomeTType(Vtt2!312))),
% 3.00/3.20 inference(unit_resolution,[status(thm)],[23, 22])).
% 3.00/3.20 tff(25,plain,
% 3.00/3.20 (~(vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType)),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[24, 15])).
% 3.00/3.20 tff(26,plain,
% 3.00/3.20 (^[Va: vName, Vtt: vTType, Valr: vAttrL] : refl(((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt)))))) <=> ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt)))))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(27,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt)))))) <=> ![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))),
% 3.00/3.20 inference(quant_intro,[status(thm)],[26])).
% 3.00/3.20 tff(28,plain,
% 3.00/3.20 (^[Va: vName, Vtt: vTType, Valr: vAttrL] : trans(monotonicity(rewrite((visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt))) <=> (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt)))))), (((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))) <=> ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt)))))))), rewrite(((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt)))))) <=> ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))), (((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))) <=> ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(29,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))) <=> ![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))),
% 3.00/3.20 inference(quant_intro,[status(thm)],[28])).
% 3.00/3.20 tff(30,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))) <=> ![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt))))),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(31,plain,
% 3.00/3.20 (^[Va: vName, Vtt: vTType, Valr: vAttrL] : rewrite(((~(visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))) => (vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType)) <=> ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(32,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((~(visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))) => (vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType)) <=> ![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt))))),
% 3.00/3.20 inference(quant_intro,[status(thm)],[31])).
% 3.00/3.20 tff(33,axiom,(![Va: vName, Vtt: vTType, Valr: vAttrL] : ((~(visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt)))) => (vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''projectTypeAttrL-2'')).
% 3.00/3.20 tff(34,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt))))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[33, 32])).
% 3.00/3.20 tff(35,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt))))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[34, 30])).
% 3.00/3.20 tff(36,plain,(
% 3.00/3.20 ![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (visSomeFType(vfindColType(Va, Vtt)) & visSomeTType(vprojectTypeAttrL(Valr, Vtt))))),
% 3.00/3.20 inference(skolemize,[status(sab)],[35])).
% 3.00/3.20 tff(37,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[36, 29])).
% 3.00/3.20 tff(38,plain,
% 3.00/3.20 (![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[37, 27])).
% 3.00/3.20 tff(39,plain,
% 3.00/3.20 (((~![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))) | ((vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType) | (~((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))))))) <=> ((~![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))) | (vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType) | (~((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))))))),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(40,plain,
% 3.00/3.20 ((~![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))) | ((vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType) | (~((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))))))),
% 3.00/3.20 inference(quant_inst,[status(thm)],[])).
% 3.00/3.20 tff(41,plain,
% 3.00/3.20 ((~![Va: vName, Vtt: vTType, Valr: vAttrL] : ((vprojectTypeAttrL(vacons(Va, Valr), Vtt) = vnoTType) | (~((~visSomeFType(vfindColType(Va, Vtt))) | (~visSomeTType(vprojectTypeAttrL(Valr, Vtt))))))) | (vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType) | (~((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309)))))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[40, 39])).
% 3.00/3.20 tff(42,plain,
% 3.00/3.20 ((vprojectTypeAttrL(vacons(Vn!310, val1), Vtt!309) = vnoTType) | (~((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309)))))),
% 3.00/3.20 inference(unit_resolution,[status(thm)],[41, 38])).
% 3.00/3.20 tff(43,plain,
% 3.00/3.20 (~((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))))),
% 3.00/3.20 inference(unit_resolution,[status(thm)],[42, 25])).
% 3.00/3.20 tff(44,plain,
% 3.00/3.20 (((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309)))) | visSomeFType(vfindColType(Vn!310, Vtt!309))),
% 3.00/3.20 inference(tautology,[status(thm)],[])).
% 3.00/3.20 tff(45,plain,
% 3.00/3.20 (visSomeFType(vfindColType(Vn!310, Vtt!309))),
% 3.00/3.20 inference(unit_resolution,[status(thm)],[44, 43])).
% 3.00/3.20 tff(46,plain,
% 3.00/3.20 (^[VOptFType0: vOptFType] : refl(((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0)))) <=> ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0)))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(47,plain,
% 3.00/3.20 (![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0)))) <=> ![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0))))),
% 3.00/3.20 inference(quant_intro,[status(thm)],[46])).
% 3.00/3.20 tff(48,plain,
% 3.00/3.20 (![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | ?[Va: vFType] : (VOptFType0 = vsomeFType(Va))) <=> ![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | ?[Va: vFType] : (VOptFType0 = vsomeFType(Va)))),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(49,plain,
% 3.00/3.20 (^[VOptFType0: vOptFType] : rewrite((visSomeFType(VOptFType0) => ?[Va: vFType] : (VOptFType0 = vsomeFType(Va))) <=> ((~visSomeFType(VOptFType0)) | ?[Va: vFType] : (VOptFType0 = vsomeFType(Va))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(50,plain,
% 3.00/3.20 (![VOptFType0: vOptFType] : (visSomeFType(VOptFType0) => ?[Va: vFType] : (VOptFType0 = vsomeFType(Va))) <=> ![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | ?[Va: vFType] : (VOptFType0 = vsomeFType(Va)))),
% 3.00/3.20 inference(quant_intro,[status(thm)],[49])).
% 3.00/3.20 tff(51,axiom,(![VOptFType0: vOptFType] : (visSomeFType(VOptFType0) => ?[Va: vFType] : (VOptFType0 = vsomeFType(Va)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''isSomeFType-true-INV'')).
% 3.00/3.20 tff(52,plain,
% 3.00/3.20 (![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | ?[Va: vFType] : (VOptFType0 = vsomeFType(Va)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[51, 50])).
% 3.00/3.20 tff(53,plain,
% 3.00/3.20 (![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | ?[Va: vFType] : (VOptFType0 = vsomeFType(Va)))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[52, 48])).
% 3.00/3.20 tff(54,plain,(
% 3.00/3.20 ![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0))))),
% 3.00/3.20 inference(skolemize,[status(sab)],[53])).
% 3.00/3.20 tff(55,plain,
% 3.00/3.20 (![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0))))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[54, 47])).
% 3.00/3.20 tff(56,plain,
% 3.00/3.20 (((~![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0))))) | ((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (vfindColType(Vn!310, Vtt!309) = vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))))) <=> ((~![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0))))) | (~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (vfindColType(Vn!310, Vtt!309) = vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))))),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(57,plain,
% 3.00/3.20 ((~![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0))))) | ((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (vfindColType(Vn!310, Vtt!309) = vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))))),
% 3.00/3.20 inference(quant_inst,[status(thm)],[])).
% 3.00/3.20 tff(58,plain,
% 3.00/3.20 ((~![VOptFType0: vOptFType] : ((~visSomeFType(VOptFType0)) | (VOptFType0 = vsomeFType(tptp_fun_Va_251(VOptFType0))))) | (~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (vfindColType(Vn!310, Vtt!309) = vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309))))),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[57, 56])).
% 3.00/3.20 tff(59,plain,
% 3.00/3.20 (vfindColType(Vn!310, Vtt!309) = vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))),
% 3.00/3.20 inference(unit_resolution,[status(thm)],[58, 55, 45])).
% 3.00/3.20 tff(60,plain,
% 3.00/3.20 (vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309))) = vfindColType(Vn!310, Vtt!309)),
% 3.00/3.20 inference(symmetry,[status(thm)],[59])).
% 3.00/3.20 tff(61,plain,
% 3.00/3.20 (vgetFType(vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))) = vgetFType(vfindColType(Vn!310, Vtt!309))),
% 3.00/3.20 inference(monotonicity,[status(thm)],[60])).
% 3.00/3.20 tff(62,plain,
% 3.00/3.20 (![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va) <=> ![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va)),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(63,plain,
% 3.00/3.20 (![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va) <=> ![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va)),
% 3.00/3.20 inference(rewrite,[status(thm)],[])).
% 3.00/3.20 tff(64,axiom,(![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''getFType-0'')).
% 3.00/3.20 tff(65,plain,
% 3.00/3.20 (![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va)),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[64, 63])).
% 3.00/3.20 tff(66,plain,(
% 3.00/3.20 ![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va)),
% 3.00/3.20 inference(skolemize,[status(sab)],[65])).
% 3.00/3.20 tff(67,plain,
% 3.00/3.20 (![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va)),
% 3.00/3.20 inference(modus_ponens,[status(thm)],[66, 62])).
% 3.00/3.20 tff(68,plain,
% 3.00/3.20 ((~![Va: vFType] : (vgetFType(vsomeFType(Va)) = Va)) | (vgetFType(vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))) = tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))),
% 3.00/3.20 inference(quant_inst,[status(thm)],[])).
% 3.00/3.20 tff(69,plain,
% 3.00/3.20 (vgetFType(vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)))) = tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309))),
% 3.00/3.20 inference(unit_resolution,[status(thm)],[68, 67])).
% 3.00/3.20 tff(70,plain,
% 3.00/3.20 (tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)) = vgetFType(vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309))))),
% 3.00/3.20 inference(symmetry,[status(thm)],[69])).
% 3.00/3.20 tff(71,plain,
% 3.00/3.20 (tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309)) = vgetFType(vfindColType(Vn!310, Vtt!309))),
% 3.00/3.20 inference(transitivity,[status(thm)],[70, 61])).
% 3.00/3.20 tff(72,plain,
% 3.00/3.20 (vsomeFType(tptp_fun_Va_251(vfindColType(Vn!310, Vtt!309))) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309)))),
% 3.00/3.20 inference(monotonicity,[status(thm)],[71])).
% 3.00/3.20 tff(73,plain,
% 3.00/3.20 (vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309)))),
% 3.00/3.20 inference(transitivity,[status(thm)],[59, 72])).
% 3.00/3.20 tff(74,plain,
% 3.00/3.20 (vmatchingAttrL(Vtt!309, Valt!314)),
% 3.00/3.20 inference(and_elim,[status(thm)],[10])).
% 3.00/3.20 tff(75,plain,
% 3.00/3.20 (vwelltypedRawtable(Vtt!309, Vrt!313)),
% 3.00/3.20 inference(and_elim,[status(thm)],[10])).
% 3.00/3.20 tff(76,plain,
% 3.00/3.20 (^[Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : refl(((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(77,plain,
% 3.00/3.20 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> ![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 3.00/3.20 inference(quant_intro,[status(thm)],[76])).
% 3.00/3.20 tff(78,plain,
% 3.00/3.20 (^[Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : trans(monotonicity(trans(monotonicity(rewrite((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) <=> (~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> (~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))))), rewrite((~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt)))) <=> (((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt)))))), rewrite((((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt)))) <=> ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt)))) <=> ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))))),
% 3.00/3.20 inference(bind,[status(th)],[])).
% 3.00/3.20 tff(79,plain,
% 3.00/3.20 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt)))) <=> ![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 3.00/3.21 inference(quant_intro,[status(thm)],[78])).
% 3.00/3.21 tff(80,plain,
% 3.00/3.21 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2))) <=> ![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2)))),
% 3.00/3.21 inference(rewrite,[status(thm)],[])).
% 3.00/3.21 tff(81,plain,
% 3.00/3.21 (^[Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : trans(monotonicity(rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) <=> (vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2))) <=> ((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2))))), rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2)))))),
% 3.00/3.21 inference(bind,[status(th)],[])).
% 3.00/3.21 tff(82,plain,
% 3.00/3.21 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2))) <=> ![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2)))),
% 3.00/3.21 inference(quant_intro,[status(thm)],[81])).
% 3.00/3.21 tff(83,axiom,(![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','findColTypeImpliesfindCol')).
% 3.00/3.21 tff(84,plain,
% 3.00/3.21 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2)))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[83, 82])).
% 3.00/3.21 tff(85,plain,
% 3.00/3.21 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt2: vRawTable] : (vfindCol(Vn, Val, Vrt) = vsomeRawTable(Vrt2)))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[84, 80])).
% 3.00/3.21 tff(86,plain,(
% 3.00/3.21 ![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Val) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))))),
% 3.00/3.21 inference(skolemize,[status(sab)],[85])).
% 3.00/3.21 tff(87,plain,
% 3.00/3.21 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[86, 79])).
% 3.00/3.21 tff(88,plain,
% 3.00/3.21 (![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[87, 77])).
% 3.00/3.21 tff(89,plain,
% 3.00/3.21 (((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((~vmatchingAttrL(Vtt!309, Valt!314)) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))))) <=> ((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))))),
% 3.00/3.21 inference(rewrite,[status(thm)],[])).
% 3.00/3.21 tff(90,plain,
% 3.00/3.21 (((vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309)))))) <=> ((~vmatchingAttrL(Vtt!309, Valt!314)) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))))),
% 3.00/3.21 inference(rewrite,[status(thm)],[])).
% 3.00/3.21 tff(91,plain,
% 3.00/3.21 (((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))))) <=> ((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((~vmatchingAttrL(Vtt!309, Valt!314)) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313)))))),
% 3.00/3.21 inference(monotonicity,[status(thm)],[90])).
% 3.00/3.21 tff(92,plain,
% 3.00/3.21 (((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))))) <=> ((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))))),
% 3.00/3.21 inference(transitivity,[status(thm)],[91, 89])).
% 3.00/3.21 tff(93,plain,
% 3.00/3.21 ((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))))),
% 3.00/3.21 inference(quant_inst,[status(thm)],[])).
% 3.00/3.21 tff(94,plain,
% 3.00/3.21 ((~![Vrt: vRawTable, Vft: vFType, Val: vAttrL, Vn: vName, Vtt: vTType] : ((vfindCol(Vn, Val, Vrt) = vsomeRawTable(tptp_fun_Vrt2_308(Vn, Val, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Val)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vfindColType(Vn!310, Vtt!309) = vsomeFType(vgetFType(vfindColType(Vn!310, Vtt!309))))) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313)))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[93, 92])).
% 3.00/3.21 tff(95,plain,
% 3.00/3.21 (vfindCol(Vn!310, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))),
% 3.00/3.21 inference(unit_resolution,[status(thm)],[94, 88, 75, 74, 73])).
% 3.00/3.21 tff(96,assumption,(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))), introduced(assumption)).
% 3.00/3.21 tff(97,plain,
% 3.00/3.21 (^[Vrt2000: vRawTable] : refl((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000))) <=> (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000))))),
% 3.00/3.21 inference(bind,[status(th)],[])).
% 3.00/3.21 tff(98,plain,
% 3.00/3.21 (![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000))) <=> ![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000)))),
% 3.00/3.21 inference(quant_intro,[status(thm)],[97])).
% 3.00/3.21 tff(99,plain,
% 3.00/3.21 (![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000)))),
% 3.00/3.21 inference(and_elim,[status(thm)],[10])).
% 3.00/3.21 tff(100,plain,
% 3.00/3.21 (![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000)))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[99, 98])).
% 3.00/3.21 tff(101,plain,
% 3.00/3.21 ((~![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000)))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))))),
% 3.00/3.21 inference(quant_inst,[status(thm)],[])).
% 3.00/3.21 tff(102,plain,
% 3.00/3.21 ($false),
% 3.00/3.21 inference(unit_resolution,[status(thm)],[101, 100, 96])).
% 3.00/3.21 tff(103,plain,(~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))), inference(lemma,lemma(discharge,[]))).
% 3.00/3.21 tff(104,plain,
% 3.00/3.21 (((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)))))) | (vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))),
% 3.00/3.21 inference(tautology,[status(thm)],[])).
% 3.00/3.21 tff(105,plain,
% 3.00/3.21 ((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)))))),
% 3.00/3.21 inference(unit_resolution,[status(thm)],[104, 103])).
% 3.00/3.21 tff(106,plain,
% 3.00/3.21 ((vacons(Vn!310, val1) = vaempty) <=> (vaempty = vacons(Vn!310, val1))),
% 3.00/3.21 inference(commutativity,[status(thm)],[])).
% 3.00/3.21 tff(107,plain,
% 3.00/3.21 ((vaempty = vacons(Vn!310, val1)) <=> (vacons(Vn!310, val1) = vaempty)),
% 3.00/3.21 inference(symmetry,[status(thm)],[106])).
% 3.00/3.21 tff(108,plain,
% 3.00/3.21 ((~(vaempty = vacons(Vn!310, val1))) <=> (~(vacons(Vn!310, val1) = vaempty))),
% 3.00/3.21 inference(monotonicity,[status(thm)],[107])).
% 3.00/3.21 tff(109,plain,
% 3.00/3.21 (^[VName0: vName, VAttrL0: vAttrL] : refl((~(vaempty = vacons(VName0, VAttrL0))) <=> (~(vaempty = vacons(VName0, VAttrL0))))),
% 3.00/3.21 inference(bind,[status(th)],[])).
% 3.00/3.21 tff(110,plain,
% 3.00/3.21 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0))) <=> ![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 3.00/3.21 inference(quant_intro,[status(thm)],[109])).
% 3.00/3.21 tff(111,plain,
% 3.00/3.21 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0))) <=> ![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 3.00/3.21 inference(rewrite,[status(thm)],[])).
% 3.00/3.21 tff(112,axiom,(![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''DIFF-aempty-acons'')).
% 3.00/3.21 tff(113,plain,
% 3.00/3.21 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[112, 111])).
% 3.00/3.21 tff(114,plain,(
% 3.00/3.21 ![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 3.00/3.21 inference(skolemize,[status(sab)],[113])).
% 3.00/3.21 tff(115,plain,
% 3.00/3.21 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[114, 110])).
% 3.00/3.21 tff(116,plain,
% 3.00/3.21 ((~![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))) | (~(vaempty = vacons(Vn!310, val1)))),
% 3.00/3.21 inference(quant_inst,[status(thm)],[])).
% 3.00/3.21 tff(117,plain,
% 3.00/3.21 (~(vaempty = vacons(Vn!310, val1))),
% 3.00/3.21 inference(unit_resolution,[status(thm)],[116, 115])).
% 3.00/3.21 tff(118,plain,
% 3.00/3.21 (~(vacons(Vn!310, val1) = vaempty)),
% 3.00/3.21 inference(modus_ponens,[status(thm)],[117, 108])).
% 3.00/3.21 tff(119,plain,
% 3.00/3.21 (((~(vacons(Vn!310, val1) = vaempty)) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vprojectEmptyCol(Vrt!313))))) | (vacons(Vn!310, val1) = vaempty)),
% 3.00/3.21 inference(tautology,[status(thm)],[])).
% 3.00/3.21 tff(120,plain,
% 3.00/3.21 ((~(vacons(Vn!310, val1) = vaempty)) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vprojectEmptyCol(Vrt!313))))),
% 3.00/3.21 inference(unit_resolution,[status(thm)],[119, 118])).
% 3.00/3.21 tff(121,plain,
% 3.00/3.21 (^[VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : refl(((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0))))))) <=> ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0))))))))),
% 3.00/3.21 inference(bind,[status(th)],[])).
% 3.00/3.21 tff(122,plain,
% 3.00/3.21 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0))))))) <=> ![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))),
% 3.00/3.22 inference(quant_intro,[status(thm)],[121])).
% 3.00/3.22 tff(123,plain,
% 3.00/3.22 (^[VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : rewrite((((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))) | ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & (VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0))))) <=> ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0))))))))),
% 3.00/3.22 inference(bind,[status(th)],[])).
% 3.00/3.22 tff(124,plain,
% 3.00/3.22 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))) | ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & (VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0))))) <=> ![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))),
% 3.00/3.22 inference(quant_intro,[status(thm)],[123])).
% 3.00/3.22 tff(125,plain,
% 3.00/3.22 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20)))) <=> ![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20))))),
% 3.00/3.22 inference(rewrite,[status(thm)],[])).
% 3.00/3.22 tff(126,plain,
% 3.00/3.22 (^[VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : trans(monotonicity(rewrite((?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((((VAttrL0 = vaempty) & (VAttrL1 = VwildcardName00)) & (VRawTable0 = Vrt0)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(Vrt0)))) | ?[Vrt1: vRawTable, Vrest0: vOptRawTable, Vcol0: vOptRawTable, Val10: vAttrL, Val20: vAttrL, Vn0: vName] : ((((((((Vcol0 = vfindCol(Vn0, Val10, Vrt1)) & (Vrest0 = vprojectCols(Val20, Val10, Vrt1))) & visSomeRawTable(Vcol0)) & visSomeRawTable(Vrest0)) & (VAttrL0 = vacons(Vn0, Val20))) & (VAttrL1 = Val10)) & (VRawTable0 = Vrt1)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(Vcol0), vgetRawTable(Vrest0)))))) <=> (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20))))), trans(quant_intro(proof_bind(^[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))))), (((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) <=> (((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))))), rewrite((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)))), (((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21))))), ((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) <=> (((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)))), rewrite((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11))), ((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11)))), (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) <=> (((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)))), rewrite((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2))), (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2)))), ((((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) <=> (((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)))), rewrite((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable))), ((((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) <=> ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable))))), (?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) <=> ?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)))), trans(der(?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) <=> ?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21)))), elim_unused(?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) <=> ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21)))), (?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : ((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2)) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1))) & (VAttrL0 = vacons(Vn1, Val21)) & (VAttrL1 = Val11) & (VRawTable0 = Vrt2) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) <=> ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))))), (?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) <=> ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))))), (((?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((((VAttrL0 = vaempty) & (VAttrL1 = VwildcardName00)) & (VRawTable0 = Vrt0)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(Vrt0)))) | ?[Vrt1: vRawTable, Vrest0: vOptRawTable, Vcol0: vOptRawTable, Val10: vAttrL, Val20: vAttrL, Vn0: vName] : ((((((((Vcol0 = vfindCol(Vn0, Val10, Vrt1)) & (Vrest0 = vprojectCols(Val20, Val10, Vrt1))) & visSomeRawTable(Vcol0)) & visSomeRawTable(Vrest0)) & (VAttrL0 = vacons(Vn0, Val20))) & (VAttrL1 = Val10)) & (VRawTable0 = Vrt1)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(Vcol0), vgetRawTable(Vrest0)))))) | ?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable))) <=> ((((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20)))) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21)))))), rewrite(((((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20)))) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21)))) <=> (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20))))), (((?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((((VAttrL0 = vaempty) & (VAttrL1 = VwildcardName00)) & (VRawTable0 = Vrt0)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(Vrt0)))) | ?[Vrt1: vRawTable, Vrest0: vOptRawTable, Vcol0: vOptRawTable, Val10: vAttrL, Val20: vAttrL, Vn0: vName] : ((((((((Vcol0 = vfindCol(Vn0, Val10, Vrt1)) & (Vrest0 = vprojectCols(Val20, Val10, Vrt1))) & visSomeRawTable(Vcol0)) & visSomeRawTable(Vrest0)) & (VAttrL0 = vacons(Vn0, Val20))) & (VAttrL1 = Val10)) & (VRawTable0 = Vrt1)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(Vcol0), vgetRawTable(Vrest0)))))) | ?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable))) <=> (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20))))))),
% 3.00/3.22 inference(bind,[status(th)],[])).
% 3.00/3.22 tff(127,plain,
% 3.00/3.22 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((((VAttrL0 = vaempty) & (VAttrL1 = VwildcardName00)) & (VRawTable0 = Vrt0)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(Vrt0)))) | ?[Vrt1: vRawTable, Vrest0: vOptRawTable, Vcol0: vOptRawTable, Val10: vAttrL, Val20: vAttrL, Vn0: vName] : ((((((((Vcol0 = vfindCol(Vn0, Val10, Vrt1)) & (Vrest0 = vprojectCols(Val20, Val10, Vrt1))) & visSomeRawTable(Vcol0)) & visSomeRawTable(Vrest0)) & (VAttrL0 = vacons(Vn0, Val20))) & (VAttrL1 = Val10)) & (VRawTable0 = Vrt1)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(Vcol0), vgetRawTable(Vrest0)))))) | ?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable))) <=> ![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20))))),
% 3.00/3.22 inference(quant_intro,[status(thm)],[126])).
% 3.00/3.22 tff(128,axiom,(![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((((VAttrL0 = vaempty) & (VAttrL1 = VwildcardName00)) & (VRawTable0 = Vrt0)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(Vrt0)))) | ?[Vrt1: vRawTable, Vrest0: vOptRawTable, Vcol0: vOptRawTable, Val10: vAttrL, Val20: vAttrL, Vn0: vName] : ((((((((Vcol0 = vfindCol(Vn0, Val10, Vrt1)) & (Vrest0 = vprojectCols(Val20, Val10, Vrt1))) & visSomeRawTable(Vcol0)) & visSomeRawTable(Vrest0)) & (VAttrL0 = vacons(Vn0, Val20))) & (VAttrL1 = Val10)) & (VRawTable0 = Vrt1)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(Vcol0), vgetRawTable(Vrest0)))))) | ?[Vrt2: vRawTable, Vrest1: vOptRawTable, Vcol1: vOptRawTable, Val11: vAttrL, Val21: vAttrL, Vn1: vName] : (((((((Vcol1 = vfindCol(Vn1, Val11, Vrt2)) & (Vrest1 = vprojectCols(Val21, Val11, Vrt2))) & (~(visSomeRawTable(Vcol1) & visSomeRawTable(Vrest1)))) & (VAttrL0 = vacons(Vn1, Val21))) & (VAttrL1 = Val11)) & (VRawTable0 = Vrt2)) & (vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''projectCols-INV'')).
% 3.00/3.22 tff(129,plain,
% 3.00/3.22 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20))))),
% 3.00/3.22 inference(modus_ponens,[status(thm)],[128, 127])).
% 3.00/3.22 tff(130,plain,
% 3.00/3.22 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ?[Val21: vAttrL, Vn1: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(Vn1, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val21, VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(Vn1, Val21))) | ?[Val20: vAttrL, Vn0: vName] : ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(Val20, VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(Vn0, VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(Val20, VAttrL1, VRawTable0)) & (VAttrL0 = vacons(Vn0, Val20))))),
% 3.00/3.22 inference(modus_ponens,[status(thm)],[129, 125])).
% 3.00/3.22 tff(131,plain,(
% 3.00/3.22 ![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : (((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0))) & (VAttrL0 = vaempty)) | ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable) & (~(visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))) & (VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))) | ((vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) & visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)) & (VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))),
% 3.00/3.22 inference(skolemize,[status(sab)],[130])).
% 3.00/3.22 tff(132,plain,
% 3.00/3.22 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))),
% 3.00/3.22 inference(modus_ponens,[status(thm)],[131, 124])).
% 3.00/3.22 tff(133,plain,
% 3.00/3.22 (![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))),
% 3.00/3.22 inference(modus_ponens,[status(thm)],[132, 122])).
% 3.00/3.22 tff(134,plain,
% 3.00/3.22 (((~![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))) | ((~((~(vacons(Vn!310, val1) = vaempty)) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vprojectEmptyCol(Vrt!313)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))))))) | (~((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1))))))))) <=> ((~![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))) | (~((~(vacons(Vn!310, val1) = vaempty)) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vprojectEmptyCol(Vrt!313)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))))))) | (~((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1))))))))),
% 3.00/3.23 inference(rewrite,[status(thm)],[])).
% 3.00/3.23 tff(135,plain,
% 3.00/3.23 ((~![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))) | ((~((~(vacons(Vn!310, val1) = vaempty)) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vprojectEmptyCol(Vrt!313)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))))))) | (~((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1))))))))),
% 3.00/3.23 inference(quant_inst,[status(thm)],[])).
% 3.00/3.23 tff(136,plain,
% 3.00/3.23 ((~![VAttrL0: vAttrL, VAttrL1: vAttrL, VRawTable0: vRawTable] : ((~((~(VAttrL0 = vaempty)) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vprojectEmptyCol(VRawTable0)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))))) | (~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vnoRawTable)) | (~(VAttrL0 = vacons(tptp_fun_Vn1_162(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val21_163(VRawTable0, VAttrL1, VAttrL0)))))) | (~((~(vprojectCols(VAttrL0, VAttrL1, VRawTable0) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0), VAttrL1, VRawTable0))) | (~(VAttrL0 = vacons(tptp_fun_Vn0_164(VRawTable0, VAttrL1, VAttrL0), tptp_fun_Val20_165(VRawTable0, VAttrL1, VAttrL0)))))))) | (~((~(vacons(Vn!310, val1) = vaempty)) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vprojectEmptyCol(Vrt!313)))))) | (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))))))) | (~((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)))))))),
% 3.00/3.23 inference(modus_ponens,[status(thm)],[135, 134])).
% 3.00/3.23 tff(137,plain,
% 3.00/3.23 ((~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))))))) | (~((~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)), vgetRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn0_164(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val20_165(Vrt!313, Valt!314, vacons(Vn!310, val1)))))))),
% 3.00/3.23 inference(unit_resolution,[status(thm)],[136, 133, 120])).
% 3.00/3.23 tff(138,plain,
% 3.00/3.23 (~((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))))))),
% 3.00/3.23 inference(unit_resolution,[status(thm)],[137, 105])).
% 3.00/3.23 tff(139,plain,
% 3.00/3.23 (((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)))))) | (vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))))),
% 3.00/3.23 inference(tautology,[status(thm)],[])).
% 3.00/3.23 tff(140,plain,
% 3.00/3.23 (vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)))),
% 3.00/3.23 inference(unit_resolution,[status(thm)],[139, 138])).
% 3.00/3.23 tff(141,plain,
% 3.00/3.23 (vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1)),
% 3.00/3.23 inference(symmetry,[status(thm)],[140])).
% 3.00/3.23 tff(142,plain,
% 3.00/3.23 (^[VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : refl(((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1))))) <=> ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1))))))),
% 3.00/3.23 inference(bind,[status(th)],[])).
% 3.00/3.23 tff(143,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1))))) <=> ![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))),
% 3.00/3.23 inference(quant_intro,[status(thm)],[142])).
% 3.00/3.23 tff(144,plain,
% 3.00/3.23 (^[VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : rewrite(((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1))) <=> ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1))))))),
% 3.00/3.23 inference(bind,[status(th)],[])).
% 3.00/3.23 tff(145,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1))) <=> ![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))),
% 3.00/3.23 inference(quant_intro,[status(thm)],[144])).
% 3.00/3.23 tff(146,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1))) <=> ![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 3.00/3.23 inference(rewrite,[status(thm)],[])).
% 3.00/3.23 tff(147,plain,
% 3.00/3.23 (^[VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : rewrite(((vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1)) => ((VName0 = VName1) & (VAttrL0 = VAttrL1))) <=> ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1))))),
% 3.00/3.23 inference(bind,[status(th)],[])).
% 3.00/3.23 tff(148,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1)) => ((VName0 = VName1) & (VAttrL0 = VAttrL1))) <=> ![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 3.00/3.23 inference(quant_intro,[status(thm)],[147])).
% 3.00/3.23 tff(149,axiom,(![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1)) => ((VName0 = VName1) & (VAttrL0 = VAttrL1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''EQ-acons'')).
% 3.00/3.23 tff(150,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 3.00/3.23 inference(modus_ponens,[status(thm)],[149, 148])).
% 3.00/3.23 tff(151,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 3.00/3.23 inference(modus_ponens,[status(thm)],[150, 146])).
% 3.00/3.23 tff(152,plain,(
% 3.00/3.23 ![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 3.00/3.23 inference(skolemize,[status(sab)],[151])).
% 3.00/3.23 tff(153,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))),
% 3.00/3.23 inference(modus_ponens,[status(thm)],[152, 145])).
% 3.00/3.23 tff(154,plain,
% 3.00/3.23 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[153, 143])).
% 3.00/3.24 tff(155,plain,
% 3.00/3.24 (((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)))))) <=> ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | (~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)))))),
% 3.00/3.24 inference(rewrite,[status(thm)],[])).
% 3.00/3.24 tff(156,plain,
% 3.00/3.24 (((~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)) | (~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1))))) <=> ((~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)))))),
% 3.00/3.24 inference(rewrite,[status(thm)],[])).
% 3.00/3.24 tff(157,plain,
% 3.00/3.24 (((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)) | (~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)))))) <=> ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310))))))),
% 3.00/3.24 inference(monotonicity,[status(thm)],[156])).
% 3.00/3.24 tff(158,plain,
% 3.00/3.24 (((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)) | (~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)))))) <=> ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | (~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)))))),
% 3.00/3.24 inference(transitivity,[status(thm)],[157, 155])).
% 3.00/3.24 tff(159,plain,
% 3.00/3.24 ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)) | (~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)))))),
% 3.00/3.24 inference(quant_inst,[status(thm)],[])).
% 3.00/3.24 tff(160,plain,
% 3.00/3.24 ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | (~(vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1))) = vacons(Vn!310, val1))) | (~((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310))))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[159, 158])).
% 3.00/3.24 tff(161,plain,
% 3.00/3.24 (~((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)))),
% 3.00/3.24 inference(unit_resolution,[status(thm)],[160, 154, 141])).
% 3.00/3.24 tff(162,plain,
% 3.00/3.24 (((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310))) | (tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310)),
% 3.00/3.24 inference(tautology,[status(thm)],[])).
% 3.00/3.24 tff(163,plain,
% 3.00/3.24 (tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310),
% 3.00/3.24 inference(unit_resolution,[status(thm)],[162, 161])).
% 3.00/3.24 tff(164,plain,
% 3.00/3.24 (vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313) = vfindCol(Vn!310, Valt!314, Vrt!313)),
% 3.00/3.24 inference(monotonicity,[status(thm)],[163])).
% 3.00/3.24 tff(165,plain,
% 3.00/3.24 (visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)) <=> visSomeRawTable(vfindCol(Vn!310, Valt!314, Vrt!313))),
% 3.00/3.24 inference(monotonicity,[status(thm)],[164])).
% 3.00/3.24 tff(166,plain,
% 3.00/3.24 ((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) <=> (~visSomeRawTable(vfindCol(Vn!310, Valt!314, Vrt!313)))),
% 3.00/3.24 inference(monotonicity,[status(thm)],[165])).
% 3.00/3.24 tff(167,plain,
% 3.00/3.24 (((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)))))) | ((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))),
% 3.00/3.24 inference(tautology,[status(thm)],[])).
% 3.00/3.24 tff(168,plain,
% 3.00/3.24 ((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))),
% 3.00/3.24 inference(unit_resolution,[status(thm)],[167, 138])).
% 3.00/3.24 tff(169,plain,
% 3.00/3.24 (((~visSomeFType(vfindColType(Vn!310, Vtt!309))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309)))) | visSomeTType(vprojectTypeAttrL(val1, Vtt!309))),
% 3.00/3.24 inference(tautology,[status(thm)],[])).
% 3.00/3.24 tff(170,plain,
% 3.00/3.24 (visSomeTType(vprojectTypeAttrL(val1, Vtt!309))),
% 3.00/3.24 inference(unit_resolution,[status(thm)],[169, 43])).
% 3.00/3.24 tff(171,plain,
% 3.00/3.24 (^[VOptTType0: vOptTType] : refl(((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0)))) <=> ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0)))))),
% 3.00/3.24 inference(bind,[status(th)],[])).
% 3.00/3.24 tff(172,plain,
% 3.00/3.24 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0)))) <=> ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))),
% 3.00/3.24 inference(quant_intro,[status(thm)],[171])).
% 3.00/3.24 tff(173,plain,
% 3.00/3.24 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))) <=> ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 3.00/3.24 inference(rewrite,[status(thm)],[])).
% 3.00/3.24 tff(174,plain,
% 3.00/3.24 (^[VOptTType0: vOptTType] : rewrite((visSomeTType(VOptTType0) => ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))) <=> ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))))),
% 3.00/3.24 inference(bind,[status(th)],[])).
% 3.00/3.24 tff(175,plain,
% 3.00/3.24 (![VOptTType0: vOptTType] : (visSomeTType(VOptTType0) => ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0))) <=> ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 3.00/3.24 inference(quant_intro,[status(thm)],[174])).
% 3.00/3.24 tff(176,axiom,(![VOptTType0: vOptTType] : (visSomeTType(VOptTType0) => ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''isSomeTType-true-INV'')).
% 3.00/3.24 tff(177,plain,
% 3.00/3.24 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[176, 175])).
% 3.00/3.24 tff(178,plain,
% 3.00/3.24 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | ?[VwildcardName0: vTType] : (VOptTType0 = vsomeTType(VwildcardName0)))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[177, 173])).
% 3.00/3.24 tff(179,plain,(
% 3.00/3.24 ![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))),
% 3.00/3.24 inference(skolemize,[status(sab)],[178])).
% 3.00/3.24 tff(180,plain,
% 3.00/3.24 (![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[179, 172])).
% 3.00/3.24 tff(181,plain,
% 3.00/3.24 (((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | ((~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))) | (vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309)))))) <=> ((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))) | (vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309)))))),
% 3.00/3.24 inference(rewrite,[status(thm)],[])).
% 3.00/3.24 tff(182,plain,
% 3.00/3.24 ((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | ((~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))) | (vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309)))))),
% 3.00/3.24 inference(quant_inst,[status(thm)],[])).
% 3.00/3.24 tff(183,plain,
% 3.00/3.24 ((~![VOptTType0: vOptTType] : ((~visSomeTType(VOptTType0)) | (VOptTType0 = vsomeTType(tptp_fun_VwildcardName0_140(VOptTType0))))) | (~visSomeTType(vprojectTypeAttrL(val1, Vtt!309))) | (vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[182, 181])).
% 3.00/3.24 tff(184,plain,
% 3.00/3.24 (vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309)))),
% 3.00/3.24 inference(unit_resolution,[status(thm)],[183, 180, 170])).
% 3.00/3.24 tff(185,plain,
% 3.00/3.24 (^[Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : refl(((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) <=> ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))))),
% 3.00/3.24 inference(bind,[status(th)],[])).
% 3.00/3.24 tff(186,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) <=> ![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))),
% 3.00/3.24 inference(quant_intro,[status(thm)],[185])).
% 3.00/3.24 tff(187,plain,
% 3.00/3.24 (^[Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : trans(monotonicity(trans(monotonicity(rewrite((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) <=> (~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) <=> (~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))))))), rewrite((~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt)))) <=> (((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt)))))), rewrite((((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt)))) <=> ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt)))) <=> ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))))),
% 3.00/3.24 inference(bind,[status(th)],[])).
% 3.00/3.24 tff(188,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt)))) <=> ![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))),
% 3.00/3.24 inference(quant_intro,[status(thm)],[187])).
% 3.00/3.24 tff(189,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20))) <=> ![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20)))),
% 3.00/3.24 inference(rewrite,[status(thm)],[])).
% 3.00/3.24 tff(190,plain,
% 3.00/3.24 (^[Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : trans(monotonicity(rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) <=> (vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) => ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20))) <=> ((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) => ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20))))), rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) => ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) => ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20)))))),
% 3.00/3.24 inference(bind,[status(th)],[])).
% 3.00/3.24 tff(191,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) => ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20))) <=> ![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20)))),
% 3.00/3.24 inference(quant_intro,[status(thm)],[190])).
% 3.00/3.24 tff(192,axiom,(![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt)) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))) => ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''projectColsProgress-acons-IH0'')).
% 3.00/3.24 tff(193,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20)))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[192, 191])).
% 3.00/3.24 tff(194,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | ?[Vrt20: vRawTable] : (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(Vrt20)))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[193, 189])).
% 3.00/3.24 tff(195,plain,(
% 3.00/3.24 ![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, Valt) & (vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2)))) | (vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))))),
% 3.00/3.24 inference(skolemize,[status(sab)],[194])).
% 3.00/3.24 tff(196,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[195, 188])).
% 3.00/3.24 tff(197,plain,
% 3.00/3.24 (![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))),
% 3.00/3.24 inference(modus_ponens,[status(thm)],[196, 186])).
% 3.00/3.24 tff(198,plain,
% 3.00/3.24 (((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | ((~vmatchingAttrL(Vtt!309, Valt!314)) | (vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))))),
% 3.00/3.24 inference(rewrite,[status(thm)],[])).
% 3.00/3.24 tff(199,plain,
% 3.00/3.24 (((vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309)))))) <=> ((~vmatchingAttrL(Vtt!309, Valt!314)) | (vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))))),
% 3.00/3.24 inference(rewrite,[status(thm)],[])).
% 3.00/3.24 tff(200,plain,
% 3.00/3.24 (((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | ((vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | ((~vmatchingAttrL(Vtt!309, Valt!314)) | (vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309)))))))),
% 3.00/3.24 inference(monotonicity,[status(thm)],[199])).
% 3.00/3.24 tff(201,plain,
% 3.00/3.24 (((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | ((vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))))),
% 3.00/3.25 inference(transitivity,[status(thm)],[200, 198])).
% 3.00/3.25 tff(202,plain,
% 3.00/3.25 ((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | ((vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309))))))),
% 3.00/3.25 inference(quant_inst,[status(thm)],[])).
% 3.00/3.25 tff(203,plain,
% 3.00/3.25 ((~![Vtt: vTType, Vrt: vRawTable, Valt: vAttrL, Vtt2: vTType] : ((vprojectCols(val1, Valt, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Valt, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, Valt)) | (~(vprojectTypeAttrL(val1, Vtt) = vsomeTType(Vtt2))))) | (~vmatchingAttrL(Vtt!309, Valt!314)) | (vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) | (~vwelltypedRawtable(Vtt!309, Vrt!313)) | (~(vprojectTypeAttrL(val1, Vtt!309) = vsomeTType(tptp_fun_VwildcardName0_140(vprojectTypeAttrL(val1, Vtt!309)))))),
% 3.00/3.25 inference(modus_ponens,[status(thm)],[202, 201])).
% 3.00/3.25 tff(204,plain,
% 3.00/3.25 (vprojectCols(val1, Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))),
% 3.00/3.25 inference(unit_resolution,[status(thm)],[203, 197, 75, 74, 184])).
% 3.00/3.25 tff(205,plain,
% 3.00/3.25 (((~(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)) | (~(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)) = Vn!310))) | (tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1)),
% 3.00/3.25 inference(tautology,[status(thm)],[])).
% 3.00/3.25 tff(206,plain,
% 3.00/3.25 (tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)) = val1),
% 3.00/3.25 inference(unit_resolution,[status(thm)],[205, 161])).
% 3.00/3.25 tff(207,plain,
% 3.00/3.25 (vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313) = vprojectCols(val1, Valt!314, Vrt!313)),
% 3.00/3.25 inference(monotonicity,[status(thm)],[206])).
% 3.00/3.25 tff(208,plain,
% 3.00/3.25 (vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))),
% 3.00/3.25 inference(transitivity,[status(thm)],[207, 204])).
% 3.00/3.25 tff(209,plain,
% 3.00/3.25 (visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)) <=> visSomeRawTable(vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313)))),
% 3.00/3.25 inference(monotonicity,[status(thm)],[208])).
% 3.00/3.25 tff(210,plain,
% 3.00/3.25 (visSomeRawTable(vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313))) <=> visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))),
% 3.00/3.25 inference(symmetry,[status(thm)],[209])).
% 3.00/3.25 tff(211,plain,
% 3.00/3.25 (^[VwildcardName0: vRawTable] : refl(visSomeRawTable(vsomeRawTable(VwildcardName0)) <=> visSomeRawTable(vsomeRawTable(VwildcardName0)))),
% 3.00/3.25 inference(bind,[status(th)],[])).
% 3.00/3.25 tff(212,plain,
% 3.00/3.25 (![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0)) <=> ![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0))),
% 3.00/3.25 inference(quant_intro,[status(thm)],[211])).
% 3.00/3.25 tff(213,plain,
% 3.00/3.25 (![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0)) <=> ![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0))),
% 3.00/3.25 inference(rewrite,[status(thm)],[])).
% 3.00/3.25 tff(214,axiom,(![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''isSomeRawTable-1'')).
% 3.00/3.25 tff(215,plain,
% 3.00/3.25 (![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0))),
% 3.00/3.25 inference(modus_ponens,[status(thm)],[214, 213])).
% 3.00/3.25 tff(216,plain,(
% 3.00/3.25 ![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0))),
% 3.00/3.25 inference(skolemize,[status(sab)],[215])).
% 3.00/3.25 tff(217,plain,
% 3.00/3.25 (![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0))),
% 3.00/3.25 inference(modus_ponens,[status(thm)],[216, 212])).
% 3.00/3.25 tff(218,plain,
% 3.00/3.25 ((~![VwildcardName0: vRawTable] : visSomeRawTable(vsomeRawTable(VwildcardName0))) | visSomeRawTable(vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313)))),
% 3.00/3.25 inference(quant_inst,[status(thm)],[])).
% 3.00/3.25 tff(219,plain,
% 3.00/3.25 (visSomeRawTable(vsomeRawTable(tptp_fun_Vrt20_307(Valt!314, Vrt!313)))),
% 3.00/3.25 inference(unit_resolution,[status(thm)],[218, 217])).
% 3.00/3.25 tff(220,plain,
% 3.00/3.25 (visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))),
% 3.00/3.25 inference(modus_ponens,[status(thm)],[219, 210])).
% 3.00/3.25 tff(221,plain,
% 3.00/3.25 ((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313)))),
% 3.00/3.25 inference(tautology,[status(thm)],[])).
% 3.00/3.25 tff(222,plain,
% 3.00/3.25 (~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))),
% 3.00/3.25 inference(unit_resolution,[status(thm)],[221, 220, 168])).
% 3.00/3.25 tff(223,plain,
% 3.00/3.25 (~visSomeRawTable(vfindCol(Vn!310, Valt!314, Vrt!313))),
% 3.00/3.25 inference(modus_ponens,[status(thm)],[222, 166])).
% 3.00/3.25 tff(224,plain,
% 3.00/3.25 (^[VOptRawTable0: vOptRawTable] : refl((visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)) <=> (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)))),
% 3.00/3.25 inference(bind,[status(th)],[])).
% 3.00/3.25 tff(225,plain,
% 3.00/3.25 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)) <=> ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 3.00/3.25 inference(quant_intro,[status(thm)],[224])).
% 3.00/3.25 tff(226,plain,
% 3.00/3.25 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)) <=> ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 3.00/3.25 inference(rewrite,[status(thm)],[])).
% 3.00/3.25 tff(227,plain,
% 3.00/3.25 (^[VOptRawTable0: vOptRawTable] : rewrite(((~visSomeRawTable(VOptRawTable0)) => (VOptRawTable0 = vnoRawTable)) <=> (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable)))),
% 3.00/3.25 inference(bind,[status(th)],[])).
% 3.00/3.25 tff(228,plain,
% 3.00/3.25 (![VOptRawTable0: vOptRawTable] : ((~visSomeRawTable(VOptRawTable0)) => (VOptRawTable0 = vnoRawTable)) <=> ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 3.00/3.25 inference(quant_intro,[status(thm)],[227])).
% 3.00/3.25 tff(229,axiom,(![VOptRawTable0: vOptRawTable] : ((~visSomeRawTable(VOptRawTable0)) => (VOptRawTable0 = vnoRawTable))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''isSomeRawTable-false-INV'')).
% 3.00/3.25 tff(230,plain,
% 3.00/3.25 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 3.00/3.25 inference(modus_ponens,[status(thm)],[229, 228])).
% 3.00/3.25 tff(231,plain,
% 3.00/3.25 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 3.00/3.25 inference(modus_ponens,[status(thm)],[230, 226])).
% 3.00/3.25 tff(232,plain,(
% 3.00/3.25 ![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 3.00/3.25 inference(skolemize,[status(sab)],[231])).
% 3.00/3.29 tff(233,plain,
% 3.00/3.29 (![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))),
% 3.00/3.29 inference(modus_ponens,[status(thm)],[232, 225])).
% 3.00/3.29 tff(234,plain,
% 3.00/3.29 (((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | (visSomeRawTable(vfindCol(Vn!310, Valt!314, Vrt!313)) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vnoRawTable))) <=> ((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | visSomeRawTable(vfindCol(Vn!310, Valt!314, Vrt!313)) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vnoRawTable))),
% 3.00/3.29 inference(rewrite,[status(thm)],[])).
% 3.00/3.29 tff(235,plain,
% 3.00/3.29 ((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | (visSomeRawTable(vfindCol(Vn!310, Valt!314, Vrt!313)) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vnoRawTable))),
% 3.00/3.29 inference(quant_inst,[status(thm)],[])).
% 3.00/3.29 tff(236,plain,
% 3.00/3.29 ((~![VOptRawTable0: vOptRawTable] : (visSomeRawTable(VOptRawTable0) | (VOptRawTable0 = vnoRawTable))) | visSomeRawTable(vfindCol(Vn!310, Valt!314, Vrt!313)) | (vfindCol(Vn!310, Valt!314, Vrt!313) = vnoRawTable)),
% 3.00/3.29 inference(modus_ponens,[status(thm)],[235, 234])).
% 3.00/3.29 tff(237,plain,
% 3.00/3.29 (vfindCol(Vn!310, Valt!314, Vrt!313) = vnoRawTable),
% 3.00/3.29 inference(unit_resolution,[status(thm)],[236, 233, 223])).
% 3.00/3.29 tff(238,plain,
% 3.00/3.29 (vnoRawTable = vfindCol(Vn!310, Valt!314, Vrt!313)),
% 3.00/3.29 inference(symmetry,[status(thm)],[237])).
% 3.00/3.29 tff(239,plain,
% 3.00/3.29 (((~((~visSomeRawTable(vfindCol(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))) | (~visSomeRawTable(vprojectCols(tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)), Valt!314, Vrt!313))))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)) | (~(vacons(Vn!310, val1) = vacons(tptp_fun_Vn1_162(Vrt!313, Valt!314, vacons(Vn!310, val1)), tptp_fun_Val21_163(Vrt!313, Valt!314, vacons(Vn!310, val1)))))) | (vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable)),
% 3.00/3.29 inference(tautology,[status(thm)],[])).
% 3.00/3.29 tff(240,plain,
% 3.00/3.29 (vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vnoRawTable),
% 3.00/3.29 inference(unit_resolution,[status(thm)],[239, 138])).
% 3.00/3.29 tff(241,plain,
% 3.00/3.29 (vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))),
% 3.00/3.29 inference(transitivity,[status(thm)],[240, 238, 95])).
% 3.00/3.29 tff(242,plain,
% 3.00/3.29 ((~![Vrt2000: vRawTable] : (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(Vrt2000)))) | (~(vprojectCols(vacons(Vn!310, val1), Valt!314, Vrt!313) = vsomeRawTable(tptp_fun_Vrt2_308(Vn!310, Valt!314, Vrt!313))))),
% 3.00/3.29 inference(quant_inst,[status(thm)],[])).
% 3.00/3.29 tff(243,plain,
% 3.00/3.29 ($false),
% 3.00/3.29 inference(unit_resolution,[status(thm)],[242, 100, 241])).
% 3.00/3.29 % SZS output end Proof
% 3.00/3.29 % E exiting
%------------------------------------------------------------------------------