%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM283_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n008.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:06 PM UTC 2026
% Result : Theorem 0.40s 0.59s
% Output : Proof 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM283_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.15/0.33 % Computer : n008.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 20:16:45 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.40/0.59 % SZS status Theorem
% 0.40/0.59 % SZS output start Proof
% 0.40/0.59 tff(vsomeRawTable_type, type, (
% 0.40/0.59 vsomeRawTable: vRawTable > vOptRawTable)).
% 0.40/0.59 tff(tptp_fun_Vrt20_307_type, type, (
% 0.40/0.59 tptp_fun_Vrt20_307: ( vName * vRawTable ) > vRawTable)).
% 0.40/0.59 tff(vdropFirstColRaw_type, type, (
% 0.40/0.59 vdropFirstColRaw: vRawTable > vRawTable)).
% 0.40/0.59 tff(tptp_fun_Vrt_311_type, type, (
% 0.40/0.59 tptp_fun_Vrt_311: vRawTable)).
% 0.40/0.59 tff(tptp_fun_Vn_309_type, type, (
% 0.40/0.59 tptp_fun_Vn_309: vName)).
% 0.40/0.59 tff(vfindCol_type, type, (
% 0.40/0.59 vfindCol: ( vName * vAttrL * vRawTable ) > vOptRawTable)).
% 0.40/0.59 tff(vacons_type, type, (
% 0.40/0.59 vacons: ( vName * vAttrL ) > vAttrL)).
% 0.40/0.59 tff(val1_type, type, (
% 0.40/0.59 val1: vAttrL)).
% 0.40/0.59 tff(tptp_fun_Vn1_312_type, type, (
% 0.40/0.59 tptp_fun_Vn1_312: vName)).
% 0.40/0.59 tff(vsomeFType_type, type, (
% 0.40/0.59 vsomeFType: vFType > vOptFType)).
% 0.40/0.59 tff(tptp_fun_Vft_310_type, type, (
% 0.40/0.59 tptp_fun_Vft_310: vFType)).
% 0.40/0.59 tff(vfindColType_type, type, (
% 0.40/0.59 vfindColType: ( vName * vTType ) > vOptFType)).
% 0.40/0.59 tff(tptp_fun_Vttr_57_type, type, (
% 0.40/0.59 tptp_fun_Vttr_57: ( vAttrL * vTType ) > vTType)).
% 0.40/0.59 tff(tptp_fun_Vtt_308_type, type, (
% 0.40/0.59 tptp_fun_Vtt_308: vTType)).
% 0.40/0.59 tff(vmatchingAttrL_type, type, (
% 0.40/0.59 vmatchingAttrL: ( vTType * vAttrL ) > $o)).
% 0.40/0.59 tff(vwelltypedRawtable_type, type, (
% 0.40/0.59 vwelltypedRawtable: ( vTType * vRawTable ) > $o)).
% 0.40/0.59 tff(vttcons_type, type, (
% 0.40/0.59 vttcons: ( vName * vFType * vTType ) > vTType)).
% 0.40/0.59 tff(tptp_fun_VwildcardName0_56_type, type, (
% 0.40/0.59 tptp_fun_VwildcardName0_56: ( vAttrL * vTType ) > vFType)).
% 0.40/0.59 tff(tptp_fun_Va2_55_type, type, (
% 0.40/0.59 tptp_fun_Va2_55: ( vAttrL * vTType ) > vName)).
% 0.40/0.59 tff(tptp_fun_Val_54_type, type, (
% 0.40/0.59 tptp_fun_Val_54: ( vAttrL * vTType ) > vAttrL)).
% 0.40/0.59 tff(vttempty_type, type, (
% 0.40/0.59 vttempty: vTType)).
% 0.40/0.59 tff(vaempty_type, type, (
% 0.40/0.59 vaempty: vAttrL)).
% 0.40/0.59 tff(tptp_fun_Va20_50_type, type, (
% 0.40/0.59 tptp_fun_Va20_50: vAttrL > vName)).
% 0.40/0.59 tff(tptp_fun_Val0_49_type, type, (
% 0.40/0.59 tptp_fun_Val0_49: vAttrL > vAttrL)).
% 0.40/0.59 tff(tptp_fun_Vttr0_51_type, type, (
% 0.40/0.59 tptp_fun_Vttr0_51: vTType > vTType)).
% 0.40/0.59 tff(tptp_fun_VwildcardName00_52_type, type, (
% 0.40/0.59 tptp_fun_VwildcardName00_52: vTType > vFType)).
% 0.40/0.59 tff(tptp_fun_Va10_53_type, type, (
% 0.40/0.59 tptp_fun_Va10_53: vTType > vName)).
% 0.40/0.59 tff(1,plain,
% 0.40/0.59 ((((~(Vn!309 = Vn1!312)) & vwelltypedRawtable(Vtt!308, Vrt!311) & vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1)) & (vfindColType(Vn!309, Vtt!308) = vsomeFType(Vft!310))) & ![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20)))) <=> ((~(Vn!309 = Vn1!312)) & vwelltypedRawtable(Vtt!308, Vrt!311) & vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1)) & (vfindColType(Vn!309, Vtt!308) = vsomeFType(Vft!310)) & ![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20))))),
% 0.40/0.59 inference(rewrite,[status(thm)],[])).
% 0.40/0.59 tff(2,plain,
% 0.40/0.59 ((~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : ((~((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, vacons(Vn1, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20)))) <=> (~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : ((~((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, vacons(Vn1, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20))))),
% 0.40/0.59 inference(rewrite,[status(thm)],[])).
% 0.40/0.59 tff(3,plain,
% 0.40/0.59 ((~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : (((((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt)) & vmatchingAttrL(Vtt, vacons(Vn1, val1))) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20)))) <=> (~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : ((~((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, vacons(Vn1, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20))))),
% 0.40/0.59 inference(rewrite,[status(thm)],[])).
% 0.40/0.59 tff(4,axiom,(~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : (((((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt)) & vmatchingAttrL(Vtt, vacons(Vn1, val1))) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''findColTypeImpliesfindCol-acons-n-n1-False'')).
% 0.40/0.59 tff(5,plain,
% 0.40/0.59 (~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : ((~((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, vacons(Vn1, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.40/0.59 tff(6,plain,
% 0.40/0.59 (~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : ((~((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, vacons(Vn1, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[5, 2])).
% 0.40/0.59 tff(7,plain,
% 0.40/0.59 (~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : ((~((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, vacons(Vn1, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.40/0.59 tff(8,plain,
% 0.40/0.59 (~![Vn1: vName, Vrt: vRawTable, Vft: vFType, Vn: vName, Vtt: vTType] : ((~((~(Vn = Vn1)) & vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, vacons(Vn1, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, vacons(Vn1, val1), Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[7, 2])).
% 0.40/0.59 tff(9,plain,
% 0.40/0.59 ((~(Vn!309 = Vn1!312)) & vwelltypedRawtable(Vtt!308, Vrt!311) & vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1)) & (vfindColType(Vn!309, Vtt!308) = vsomeFType(Vft!310)) & ![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20)))),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[8, 1])).
% 0.40/0.59 tff(10,plain,
% 0.40/0.59 (vfindColType(Vn!309, Vtt!308) = vsomeFType(Vft!310)),
% 0.40/0.59 inference(and_elim,[status(thm)],[9])).
% 0.40/0.59 tff(11,plain,
% 0.40/0.59 ((vacons(Vn1!312, val1) = vaempty) <=> (vaempty = vacons(Vn1!312, val1))),
% 0.40/0.59 inference(commutativity,[status(thm)],[])).
% 0.40/0.59 tff(12,plain,
% 0.40/0.59 ((vaempty = vacons(Vn1!312, val1)) <=> (vacons(Vn1!312, val1) = vaempty)),
% 0.40/0.59 inference(symmetry,[status(thm)],[11])).
% 0.40/0.59 tff(13,plain,
% 0.40/0.59 ((~(vaempty = vacons(Vn1!312, val1))) <=> (~(vacons(Vn1!312, val1) = vaempty))),
% 0.40/0.59 inference(monotonicity,[status(thm)],[12])).
% 0.40/0.59 tff(14,plain,
% 0.40/0.59 (^[VName0: vName, VAttrL0: vAttrL] : refl((~(vaempty = vacons(VName0, VAttrL0))) <=> (~(vaempty = vacons(VName0, VAttrL0))))),
% 0.40/0.59 inference(bind,[status(th)],[])).
% 0.40/0.59 tff(15,plain,
% 0.40/0.59 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0))) <=> ![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 0.40/0.59 inference(quant_intro,[status(thm)],[14])).
% 0.40/0.59 tff(16,plain,
% 0.40/0.59 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0))) <=> ![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 0.40/0.59 inference(rewrite,[status(thm)],[])).
% 0.40/0.59 tff(17,axiom,(![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''DIFF-aempty-acons'')).
% 0.40/0.59 tff(18,plain,
% 0.40/0.59 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[17, 16])).
% 0.40/0.59 tff(19,plain,(
% 0.40/0.59 ![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 0.40/0.59 inference(skolemize,[status(sab)],[18])).
% 0.40/0.59 tff(20,plain,
% 0.40/0.59 (![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[19, 15])).
% 0.40/0.59 tff(21,plain,
% 0.40/0.59 ((~![VName0: vName, VAttrL0: vAttrL] : (~(vaempty = vacons(VName0, VAttrL0)))) | (~(vaempty = vacons(Vn1!312, val1)))),
% 0.40/0.59 inference(quant_inst,[status(thm)],[])).
% 0.40/0.59 tff(22,plain,
% 0.40/0.59 (~(vaempty = vacons(Vn1!312, val1))),
% 0.40/0.59 inference(unit_resolution,[status(thm)],[21, 20])).
% 0.40/0.59 tff(23,plain,
% 0.40/0.59 (~(vacons(Vn1!312, val1) = vaempty)),
% 0.40/0.59 inference(modus_ponens,[status(thm)],[22, 13])).
% 0.40/0.59 tff(24,plain,
% 0.40/0.59 (((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty))) | (vacons(Vn1!312, val1) = vaempty)),
% 0.40/0.59 inference(tautology,[status(thm)],[])).
% 0.40/0.59 tff(25,plain,
% 0.40/0.59 ((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty))),
% 0.40/0.59 inference(unit_resolution,[status(thm)],[24, 23])).
% 0.40/0.59 tff(26,plain,
% 0.40/0.59 (vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))),
% 0.40/0.59 inference(and_elim,[status(thm)],[9])).
% 0.40/0.59 tff(27,plain,
% 0.40/0.59 (^[VTType0: vTType, VAttrL0: vAttrL] : refl(((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))))) <=> ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))))))),
% 0.40/0.59 inference(bind,[status(th)],[])).
% 0.40/0.59 tff(28,plain,
% 0.40/0.59 (![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))))) <=> ![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))),
% 0.40/0.59 inference(quant_intro,[status(thm)],[27])).
% 0.40/0.59 tff(29,plain,
% 0.40/0.59 (^[VTType0: vTType, VAttrL0: vAttrL] : trans(monotonicity(rewrite(((VTType0 = vttempty) & (VAttrL0 = vaempty)) <=> (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty))))), rewrite((vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)) & (VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0))) & (VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))) <=> (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))))), ((((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | (vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)) & (VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0))) & (VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))) <=> ((~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~vmatchingAttrL(VTType0, VAttrL0)) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))))))), rewrite(((~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~vmatchingAttrL(VTType0, VAttrL0)) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))))) <=> ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))), ((((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | (vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)) & (VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0))) & (VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))) <=> ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(30,plain,
% 0.40/0.60 (![VTType0: vTType, VAttrL0: vAttrL] : (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | (vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)) & (VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0))) & (VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))))) <=> ![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[29])).
% 0.40/0.60 tff(31,plain,
% 0.40/0.60 (![VTType0: vTType, VAttrL0: vAttrL] : (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val)))) <=> ![VTType0: vTType, VAttrL0: vAttrL] : (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))),
% 0.40/0.60 inference(rewrite,[status(thm)],[])).
% 0.40/0.60 tff(32,plain,
% 0.40/0.60 (^[VTType0: vTType, VAttrL0: vAttrL] : trans(monotonicity(rewrite((((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, Va1: vName, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : ((((VTType0 = vttcons(Va1, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))) & (Va1 = Va2)) & vmatchingAttrL(Vttr, Val))) <=> (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))), ((vmatchingAttrL(VTType0, VAttrL0) => (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, Va1: vName, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : ((((VTType0 = vttcons(Va1, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))) & (Va1 = Va2)) & vmatchingAttrL(Vttr, Val)))) <=> (vmatchingAttrL(VTType0, VAttrL0) => (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))))), rewrite((vmatchingAttrL(VTType0, VAttrL0) => (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))) <=> (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))), ((vmatchingAttrL(VTType0, VAttrL0) => (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, Va1: vName, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : ((((VTType0 = vttcons(Va1, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))) & (Va1 = Va2)) & vmatchingAttrL(Vttr, Val)))) <=> (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(33,plain,
% 0.40/0.60 (![VTType0: vTType, VAttrL0: vAttrL] : (vmatchingAttrL(VTType0, VAttrL0) => (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, Va1: vName, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : ((((VTType0 = vttcons(Va1, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))) & (Va1 = Va2)) & vmatchingAttrL(Vttr, Val)))) <=> ![VTType0: vTType, VAttrL0: vAttrL] : (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[32])).
% 0.40/0.60 tff(34,axiom,(![VTType0: vTType, VAttrL0: vAttrL] : (vmatchingAttrL(VTType0, VAttrL0) => (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | ?[Vttr: vTType, Va1: vName, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : ((((VTType0 = vttcons(Va1, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))) & (Va1 = Va2)) & vmatchingAttrL(Vttr, Val))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''matchingAttrL-true-INV'')).
% 0.40/0.60 tff(35,plain,
% 0.40/0.60 (![VTType0: vTType, VAttrL0: vAttrL] : (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.40/0.60 tff(36,plain,
% 0.40/0.60 (![VTType0: vTType, VAttrL0: vAttrL] : (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | ?[Vttr: vTType, VwildcardName0: vFType, Va2: vName, Val: vAttrL] : (vmatchingAttrL(Vttr, Val) & (VTType0 = vttcons(Va2, VwildcardName0, Vttr)) & (VAttrL0 = vacons(Va2, Val))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[35, 31])).
% 0.40/0.60 tff(37,plain,(
% 0.40/0.60 ![VTType0: vTType, VAttrL0: vAttrL] : (((VTType0 = vttempty) & (VAttrL0 = vaempty)) | (~vmatchingAttrL(VTType0, VAttrL0)) | (vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)) & (VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0))) & (VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))),
% 0.40/0.60 inference(skolemize,[status(sab)],[36])).
% 0.40/0.60 tff(38,plain,
% 0.40/0.60 (![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[37, 30])).
% 0.40/0.60 tff(39,plain,
% 0.40/0.60 (![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[38, 28])).
% 0.40/0.60 tff(40,plain,
% 0.40/0.60 (((~![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))) | ((~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))))))) <=> ((~![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))) | (~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))))))),
% 0.40/0.60 inference(rewrite,[status(thm)],[])).
% 0.40/0.60 tff(41,plain,
% 0.40/0.60 ((~![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))) | ((~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))))))),
% 0.40/0.60 inference(quant_inst,[status(thm)],[])).
% 0.40/0.60 tff(42,plain,
% 0.40/0.60 ((~![VTType0: vTType, VAttrL0: vAttrL] : ((~vmatchingAttrL(VTType0, VAttrL0)) | (~((~(VAttrL0 = vaempty)) | (~(VTType0 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0))) | (~(VTType0 = vttcons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_VwildcardName0_56(VAttrL0, VTType0), tptp_fun_Vttr_57(VAttrL0, VTType0)))) | (~(VAttrL0 = vacons(tptp_fun_Va2_55(VAttrL0, VTType0), tptp_fun_Val_54(VAttrL0, VTType0)))))))) | (~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.40/0.60 tff(43,plain,
% 0.40/0.60 ((~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))))),
% 0.40/0.60 inference(unit_resolution,[status(thm)],[42, 39, 26])).
% 0.40/0.60 tff(44,plain,
% 0.40/0.60 (~((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))))),
% 0.40/0.60 inference(unit_resolution,[status(thm)],[43, 25])).
% 0.40/0.60 tff(45,plain,
% 0.40/0.60 (((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))) | (Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))),
% 0.40/0.60 inference(tautology,[status(thm)],[])).
% 0.40/0.60 tff(46,plain,
% 0.40/0.60 (Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.60 inference(unit_resolution,[status(thm)],[45, 44])).
% 0.40/0.60 tff(47,plain,
% 0.40/0.60 (vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = Vtt!308),
% 0.40/0.60 inference(symmetry,[status(thm)],[46])).
% 0.40/0.60 tff(48,plain,
% 0.40/0.60 (vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))) = vfindColType(Vn!309, Vtt!308)),
% 0.40/0.60 inference(monotonicity,[status(thm)],[47])).
% 0.40/0.60 tff(49,plain,
% 0.40/0.60 (((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))) | (vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))),
% 0.40/0.60 inference(tautology,[status(thm)],[])).
% 0.40/0.60 tff(50,plain,
% 0.40/0.60 (vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.60 inference(unit_resolution,[status(thm)],[49, 44])).
% 0.40/0.60 tff(51,plain,
% 0.40/0.60 (^[VwildcardName0: vTType, VwildcardName1: vAttrL] : refl(((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))))) <=> ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(52,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))))) <=> ![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[51])).
% 0.40/0.60 tff(53,plain,
% 0.40/0.60 (^[VwildcardName0: vTType, VwildcardName1: vAttrL] : rewrite(((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))) <=> ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(54,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))) <=> ![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[53])).
% 0.40/0.60 tff(55,plain,
% 0.40/0.60 (^[VwildcardName0: vTType, VwildcardName1: vAttrL] : rewrite(((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))) <=> ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(56,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))) <=> ![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[55])).
% 0.40/0.60 tff(57,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))))))) <=> ![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0)))))))),
% 0.40/0.60 inference(rewrite,[status(thm)],[])).
% 0.40/0.60 tff(58,plain,
% 0.40/0.60 (^[VwildcardName0: vTType, VwildcardName1: vAttrL] : trans(monotonicity(rewrite((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vaempty))) & (![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))) | ![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))))) <=> (((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0)))))), (((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vaempty))) & (![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))) | ![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))))) => (~vmatchingAttrL(VwildcardName0, VwildcardName1))) <=> ((((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))))) => (~vmatchingAttrL(VwildcardName0, VwildcardName1))))), rewrite(((((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))))) => (~vmatchingAttrL(VwildcardName0, VwildcardName1))) <=> ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0)))))))), (((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vaempty))) & (![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))) | ![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))))) => (~vmatchingAttrL(VwildcardName0, VwildcardName1))) <=> ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0)))))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(59,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vaempty))) & (![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))) | ![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))))) => (~vmatchingAttrL(VwildcardName0, VwildcardName1))) <=> ![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0)))))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[58])).
% 0.40/0.60 tff(60,axiom,(![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((((~(VwildcardName0 = vttempty)) | (~(VwildcardName1 = vaempty))) & (![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0))) | ![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))))) => (~vmatchingAttrL(VwildcardName0, VwildcardName1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''matchingAttrL-2'')).
% 0.40/0.60 tff(61,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0)))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.40/0.60 tff(62,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~(((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty))) & (![Va20: vName, Val0: vAttrL] : (~(VwildcardName1 = vacons(Va20, Val0))) | ![Va10: vName, VwildcardName00: vFType, Vttr0: vTType] : (~(VwildcardName0 = vttcons(Va10, VwildcardName00, Vttr0)))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[61, 57])).
% 0.40/0.60 tff(63,plain,(
% 0.40/0.60 ![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | ((~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0))))))),
% 0.40/0.60 inference(skolemize,[status(sab)],[62])).
% 0.40/0.60 tff(64,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | ((VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1))) & (VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[63, 56])).
% 0.40/0.60 tff(65,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[64, 54])).
% 0.40/0.60 tff(66,plain,
% 0.40/0.60 (![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[65, 52])).
% 0.40/0.60 tff(67,plain,
% 0.40/0.60 (((~![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))) | ((~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))) | (~(Vtt!308 = vttcons(tptp_fun_Va10_53(Vtt!308), tptp_fun_VwildcardName00_52(Vtt!308), tptp_fun_Vttr0_51(Vtt!308)))))))) <=> ((~![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))) | (~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))) | (~(Vtt!308 = vttcons(tptp_fun_Va10_53(Vtt!308), tptp_fun_VwildcardName00_52(Vtt!308), tptp_fun_Vttr0_51(Vtt!308)))))))),
% 0.40/0.60 inference(rewrite,[status(thm)],[])).
% 0.40/0.60 tff(68,plain,
% 0.40/0.60 ((~![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))) | ((~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))) | (~(Vtt!308 = vttcons(tptp_fun_Va10_53(Vtt!308), tptp_fun_VwildcardName00_52(Vtt!308), tptp_fun_Vttr0_51(Vtt!308)))))))),
% 0.40/0.60 inference(quant_inst,[status(thm)],[])).
% 0.40/0.60 tff(69,plain,
% 0.40/0.60 ((~![VwildcardName0: vTType, VwildcardName1: vAttrL] : ((~vmatchingAttrL(VwildcardName0, VwildcardName1)) | (~((~(VwildcardName1 = vaempty)) | (~(VwildcardName0 = vttempty)))) | (~((~(VwildcardName1 = vacons(tptp_fun_Va20_50(VwildcardName1), tptp_fun_Val0_49(VwildcardName1)))) | (~(VwildcardName0 = vttcons(tptp_fun_Va10_53(VwildcardName0), tptp_fun_VwildcardName00_52(VwildcardName0), tptp_fun_Vttr0_51(VwildcardName0)))))))) | (~vmatchingAttrL(Vtt!308, vacons(Vn1!312, val1))) | (~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))) | (~(Vtt!308 = vttcons(tptp_fun_Va10_53(Vtt!308), tptp_fun_VwildcardName00_52(Vtt!308), tptp_fun_Vttr0_51(Vtt!308))))))),
% 0.40/0.60 inference(modus_ponens,[status(thm)],[68, 67])).
% 0.40/0.60 tff(70,plain,
% 0.40/0.60 ((~((~(vacons(Vn1!312, val1) = vaempty)) | (~(Vtt!308 = vttempty)))) | (~((~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))) | (~(Vtt!308 = vttcons(tptp_fun_Va10_53(Vtt!308), tptp_fun_VwildcardName00_52(Vtt!308), tptp_fun_Vttr0_51(Vtt!308))))))),
% 0.40/0.60 inference(unit_resolution,[status(thm)],[69, 66, 26])).
% 0.40/0.60 tff(71,plain,
% 0.40/0.60 (~((~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))) | (~(Vtt!308 = vttcons(tptp_fun_Va10_53(Vtt!308), tptp_fun_VwildcardName00_52(Vtt!308), tptp_fun_Vttr0_51(Vtt!308)))))),
% 0.40/0.60 inference(unit_resolution,[status(thm)],[70, 25])).
% 0.40/0.60 tff(72,plain,
% 0.40/0.60 (((~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))) | (~(Vtt!308 = vttcons(tptp_fun_Va10_53(Vtt!308), tptp_fun_VwildcardName00_52(Vtt!308), tptp_fun_Vttr0_51(Vtt!308))))) | (vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))))),
% 0.40/0.60 inference(tautology,[status(thm)],[])).
% 0.40/0.60 tff(73,plain,
% 0.40/0.60 (vacons(Vn1!312, val1) = vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1)))),
% 0.40/0.60 inference(unit_resolution,[status(thm)],[72, 71])).
% 0.40/0.60 tff(74,plain,
% 0.40/0.60 (vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(Vn1!312, val1)),
% 0.40/0.60 inference(symmetry,[status(thm)],[73])).
% 0.40/0.60 tff(75,plain,
% 0.40/0.60 (vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.60 inference(transitivity,[status(thm)],[74, 50])).
% 0.40/0.60 tff(76,plain,
% 0.40/0.60 (^[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))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(77,plain,
% 0.40/0.60 (![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)))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[76])).
% 0.40/0.60 tff(78,plain,
% 0.40/0.60 (^[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))))))),
% 0.40/0.60 inference(bind,[status(th)],[])).
% 0.40/0.60 tff(79,plain,
% 0.40/0.60 (![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)))))),
% 0.40/0.60 inference(quant_intro,[status(thm)],[78])).
% 0.40/0.60 tff(80,plain,
% 0.40/0.60 (![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)))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(81,plain,
% 0.40/0.61 (^[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))))),
% 0.40/0.61 inference(bind,[status(th)],[])).
% 0.40/0.61 tff(82,plain,
% 0.40/0.61 (![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)))),
% 0.40/0.61 inference(quant_intro,[status(thm)],[81])).
% 0.40/0.61 tff(83,axiom,(![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1)) => ((VName0 = VName1) & (VAttrL0 = VAttrL1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''EQ-acons'')).
% 0.40/0.61 tff(84,plain,
% 0.40/0.61 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.40/0.61 tff(85,plain,
% 0.40/0.61 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[84, 80])).
% 0.40/0.61 tff(86,plain,(
% 0.40/0.61 ![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | ((VName0 = VName1) & (VAttrL0 = VAttrL1)))),
% 0.40/0.61 inference(skolemize,[status(sab)],[85])).
% 0.40/0.61 tff(87,plain,
% 0.40/0.61 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[86, 79])).
% 0.40/0.61 tff(88,plain,
% 0.40/0.61 (![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[87, 77])).
% 0.40/0.61 tff(89,plain,
% 0.40/0.61 (((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))))) <=> ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | (~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(90,plain,
% 0.40/0.61 ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))))),
% 0.40/0.61 inference(quant_inst,[status(thm)],[])).
% 0.40/0.61 tff(91,plain,
% 0.40/0.61 ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | (~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.40/0.61 tff(92,plain,
% 0.40/0.61 (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[91, 88, 75])).
% 0.40/0.61 tff(93,plain,
% 0.40/0.61 (((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))) | (tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.61 inference(tautology,[status(thm)],[])).
% 0.40/0.61 tff(94,plain,
% 0.40/0.61 (tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[93, 92])).
% 0.40/0.61 tff(95,plain,
% 0.40/0.61 (((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(Vn1!312, val1))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1)))))) <=> ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | (~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(Vn1!312, val1))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1)))))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(96,plain,
% 0.40/0.61 ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | ((~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(Vn1!312, val1))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1)))))),
% 0.40/0.61 inference(quant_inst,[status(thm)],[])).
% 0.40/0.61 tff(97,plain,
% 0.40/0.61 ((~![VName0: vName, VAttrL0: vAttrL, VName1: vName, VAttrL1: vAttrL] : ((~(vacons(VName0, VAttrL0) = vacons(VName1, VAttrL1))) | (~((~(VName0 = VName1)) | (~(VAttrL0 = VAttrL1)))))) | (~(vacons(tptp_fun_Va20_50(vacons(Vn1!312, val1)), tptp_fun_Val0_49(vacons(Vn1!312, val1))) = vacons(Vn1!312, val1))) | (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1))))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.40/0.61 tff(98,plain,
% 0.40/0.61 (~((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1)))),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[97, 88, 74])).
% 0.40/0.61 tff(99,plain,
% 0.40/0.61 (((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1))) | (tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)),
% 0.40/0.61 inference(tautology,[status(thm)],[])).
% 0.40/0.61 tff(100,plain,
% 0.40/0.61 (tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[99, 98])).
% 0.40/0.61 tff(101,plain,
% 0.40/0.61 (Vn1!312 = tptp_fun_Va20_50(vacons(Vn1!312, val1))),
% 0.40/0.61 inference(symmetry,[status(thm)],[100])).
% 0.40/0.61 tff(102,plain,
% 0.40/0.61 (Vn1!312 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)),
% 0.40/0.61 inference(transitivity,[status(thm)],[101, 94])).
% 0.40/0.61 tff(103,plain,
% 0.40/0.61 ((Vn!309 = Vn1!312) <=> (Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.61 inference(monotonicity,[status(thm)],[102])).
% 0.40/0.61 tff(104,plain,
% 0.40/0.61 ((~(Vn!309 = Vn1!312)) <=> (~(Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)))),
% 0.40/0.61 inference(monotonicity,[status(thm)],[103])).
% 0.40/0.61 tff(105,plain,
% 0.40/0.61 (~(Vn!309 = Vn1!312)),
% 0.40/0.61 inference(and_elim,[status(thm)],[9])).
% 0.40/0.61 tff(106,plain,
% 0.40/0.61 (~(Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[105, 104])).
% 0.40/0.61 tff(107,plain,
% 0.40/0.61 (^[Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : refl(((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr))) <=> ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr))))),
% 0.40/0.61 inference(bind,[status(th)],[])).
% 0.40/0.61 tff(108,plain,
% 0.40/0.61 (![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr))) <=> ![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))),
% 0.40/0.61 inference(quant_intro,[status(thm)],[107])).
% 0.40/0.61 tff(109,plain,
% 0.40/0.61 (![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr))) <=> ![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(110,plain,
% 0.40/0.61 (^[Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : rewrite(((~(Vn = Va)) => (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr))) <=> ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr))))),
% 0.40/0.61 inference(bind,[status(th)],[])).
% 0.40/0.61 tff(111,plain,
% 0.40/0.61 (![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((~(Vn = Va)) => (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr))) <=> ![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))),
% 0.40/0.61 inference(quant_intro,[status(thm)],[110])).
% 0.40/0.61 tff(112,axiom,(![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((~(Vn = Va)) => (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''findColType-2'')).
% 0.40/0.61 tff(113,plain,
% 0.40/0.61 (![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[112, 111])).
% 0.40/0.61 tff(114,plain,
% 0.40/0.61 (![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[113, 109])).
% 0.40/0.61 tff(115,plain,(
% 0.40/0.61 ![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))),
% 0.40/0.61 inference(skolemize,[status(sab)],[114])).
% 0.40/0.61 tff(116,plain,
% 0.40/0.61 (![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[115, 108])).
% 0.40/0.61 tff(117,plain,
% 0.40/0.61 (((~![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))) | ((Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))) = vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))))) <=> ((~![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))) | (Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))) = vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(118,plain,
% 0.40/0.61 ((~![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))) | ((Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))) = vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))))),
% 0.40/0.61 inference(quant_inst,[status(thm)],[])).
% 0.40/0.61 tff(119,plain,
% 0.40/0.61 ((~![Vn: vName, Va: vName, Vft: vFType, Vttr: vTType] : ((Vn = Va) | (vfindColType(Vn, vttcons(Va, Vft, Vttr)) = vfindColType(Vn, Vttr)))) | (Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))) = vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.40/0.61 tff(120,plain,
% 0.40/0.61 ((Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))) = vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[119, 116])).
% 0.40/0.61 tff(121,plain,
% 0.40/0.61 (vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))) = vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[120, 106])).
% 0.40/0.61 tff(122,plain,
% 0.40/0.61 (vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vfindColType(Vn!309, vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))),
% 0.40/0.61 inference(symmetry,[status(thm)],[121])).
% 0.40/0.61 tff(123,plain,
% 0.40/0.61 (vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310)),
% 0.40/0.61 inference(transitivity,[status(thm)],[122, 48, 10])).
% 0.40/0.61 tff(124,plain,
% 0.40/0.61 (vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311) <=> vwelltypedRawtable(Vtt!308, Vrt!311)),
% 0.40/0.61 inference(monotonicity,[status(thm)],[47])).
% 0.40/0.61 tff(125,plain,
% 0.40/0.61 (vwelltypedRawtable(Vtt!308, Vrt!311) <=> vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311)),
% 0.40/0.61 inference(symmetry,[status(thm)],[124])).
% 0.40/0.61 tff(126,plain,
% 0.40/0.61 (vwelltypedRawtable(Vtt!308, Vrt!311)),
% 0.40/0.61 inference(and_elim,[status(thm)],[9])).
% 0.40/0.61 tff(127,plain,
% 0.40/0.61 (vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311)),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[126, 125])).
% 0.40/0.61 tff(128,plain,
% 0.40/0.61 (^[Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : refl(((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt))) <=> ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt))))),
% 0.40/0.61 inference(bind,[status(th)],[])).
% 0.40/0.61 tff(129,plain,
% 0.40/0.61 (![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt))) <=> ![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))),
% 0.40/0.61 inference(quant_intro,[status(thm)],[128])).
% 0.40/0.61 tff(130,plain,
% 0.40/0.61 (![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt))) <=> ![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(131,plain,
% 0.40/0.61 (^[Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : rewrite((vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt) => vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt))) <=> ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt))))),
% 0.40/0.61 inference(bind,[status(th)],[])).
% 0.40/0.61 tff(132,plain,
% 0.40/0.61 (![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : (vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt) => vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt))) <=> ![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))),
% 0.40/0.61 inference(quant_intro,[status(thm)],[131])).
% 0.40/0.61 tff(133,axiom,(![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : (vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt) => vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','dropFirstColRawPreservesWelltypedRaw')).
% 0.40/0.61 tff(134,plain,
% 0.40/0.61 (![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.40/0.61 tff(135,plain,
% 0.40/0.61 (![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[134, 130])).
% 0.40/0.61 tff(136,plain,(
% 0.40/0.61 ![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))),
% 0.40/0.61 inference(skolemize,[status(sab)],[135])).
% 0.40/0.61 tff(137,plain,
% 0.40/0.61 (![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[136, 129])).
% 0.40/0.61 tff(138,plain,
% 0.40/0.61 (((~![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))) | ((~vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311)) | vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311)))) <=> ((~![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))) | (~vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311)) | vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311)))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(139,plain,
% 0.40/0.61 ((~![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))) | ((~vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311)) | vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311)))),
% 0.40/0.61 inference(quant_inst,[status(thm)],[])).
% 0.40/0.61 tff(140,plain,
% 0.40/0.61 ((~![Vn: vName, Vft: vFType, Vttrest: vTType, Vrt: vRawTable] : ((~vwelltypedRawtable(vttcons(Vn, Vft, Vttrest), Vrt)) | vwelltypedRawtable(Vttrest, vdropFirstColRaw(Vrt)))) | (~vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311)) | vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[139, 138])).
% 0.40/0.61 tff(141,plain,
% 0.40/0.61 ((~vwelltypedRawtable(vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)), Vrt!311)) | vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[140, 137])).
% 0.40/0.61 tff(142,plain,
% 0.40/0.61 (vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[141, 127])).
% 0.40/0.61 tff(143,plain,
% 0.40/0.61 (((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = Vn1!312)) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1))) | (tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1)),
% 0.40/0.61 inference(tautology,[status(thm)],[])).
% 0.40/0.61 tff(144,plain,
% 0.40/0.61 (tptp_fun_Val0_49(vacons(Vn1!312, val1)) = val1),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[143, 98])).
% 0.40/0.61 tff(145,plain,
% 0.40/0.61 (((~(tptp_fun_Va20_50(vacons(Vn1!312, val1)) = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308))) | (~(tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)))) | (tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.61 inference(tautology,[status(thm)],[])).
% 0.40/0.61 tff(146,plain,
% 0.40/0.61 (tptp_fun_Val0_49(vacons(Vn1!312, val1)) = tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[145, 92])).
% 0.40/0.61 tff(147,plain,
% 0.40/0.61 (tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308) = tptp_fun_Val0_49(vacons(Vn1!312, val1))),
% 0.40/0.61 inference(symmetry,[status(thm)],[146])).
% 0.40/0.61 tff(148,plain,
% 0.40/0.61 (tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308) = val1),
% 0.40/0.61 inference(transitivity,[status(thm)],[147, 144])).
% 0.40/0.61 tff(149,plain,
% 0.40/0.61 (vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308)) <=> vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)),
% 0.40/0.61 inference(monotonicity,[status(thm)],[148])).
% 0.40/0.61 tff(150,plain,
% 0.40/0.61 (((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))) | (~(Vtt!308 = vttcons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_VwildcardName0_56(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)))) | (~(vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))))) | vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.61 inference(tautology,[status(thm)],[])).
% 0.40/0.61 tff(151,plain,
% 0.40/0.61 (vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), tptp_fun_Val_54(vacons(Vn1!312, val1), Vtt!308))),
% 0.40/0.61 inference(unit_resolution,[status(thm)],[150, 44])).
% 0.40/0.61 tff(152,plain,
% 0.40/0.61 (vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)),
% 0.40/0.61 inference(modus_ponens,[status(thm)],[151, 149])).
% 0.40/0.61 tff(153,plain,
% 0.40/0.61 (^[Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : refl(((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))),
% 0.40/0.61 inference(bind,[status(th)],[])).
% 0.40/0.61 tff(154,plain,
% 0.40/0.61 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> ![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 0.40/0.61 inference(quant_intro,[status(thm)],[153])).
% 0.40/0.61 tff(155,plain,
% 0.40/0.61 (^[Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : trans(monotonicity(trans(monotonicity(rewrite((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) <=> (~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> (~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))))), rewrite((~(~((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) <=> ((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt)))) <=> (((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt)))))), rewrite((((~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt)))) <=> ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt)))) <=> ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))))),
% 0.40/0.61 inference(bind,[status(th)],[])).
% 0.40/0.61 tff(156,plain,
% 0.40/0.61 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt)))) <=> ![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 0.40/0.61 inference(quant_intro,[status(thm)],[155])).
% 0.40/0.61 tff(157,plain,
% 0.40/0.61 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20))) <=> ![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.61 inference(rewrite,[status(thm)],[])).
% 0.40/0.61 tff(158,plain,
% 0.40/0.61 (^[Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : trans(monotonicity(rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) <=> (vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20))) <=> ((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20))))), rewrite(((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20)))), ((((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20)))))),
% 0.40/0.62 inference(bind,[status(th)],[])).
% 0.40/0.62 tff(159,plain,
% 0.40/0.62 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20))) <=> ![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.62 inference(quant_intro,[status(thm)],[158])).
% 0.40/0.62 tff(160,axiom,(![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : (((vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1)) & (vfindColType(Vn, Vtt) = vsomeFType(Vft))) => ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''findColTypeImpliesfindCol-acons-IH0'')).
% 0.40/0.62 tff(161,plain,
% 0.40/0.62 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[160, 159])).
% 0.40/0.62 tff(162,plain,
% 0.40/0.62 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | ?[Vrt20: vRawTable] : (vfindCol(Vn, val1, Vrt) = vsomeRawTable(Vrt20)))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[161, 157])).
% 0.40/0.62 tff(163,plain,(
% 0.40/0.62 ![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((~(vwelltypedRawtable(Vtt, Vrt) & vmatchingAttrL(Vtt, val1) & (vfindColType(Vn, Vtt) = vsomeFType(Vft)))) | (vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))))),
% 0.40/0.62 inference(skolemize,[status(sab)],[162])).
% 0.40/0.62 tff(164,plain,
% 0.40/0.62 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[163, 156])).
% 0.40/0.62 tff(165,plain,
% 0.40/0.62 (![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[164, 154])).
% 0.40/0.62 tff(166,plain,
% 0.40/0.62 (((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | (~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310))))),
% 0.40/0.62 inference(rewrite,[status(thm)],[])).
% 0.40/0.62 tff(167,plain,
% 0.40/0.62 (((vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310)))) <=> ((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310))))),
% 0.40/0.62 inference(rewrite,[status(thm)],[])).
% 0.40/0.62 tff(168,plain,
% 0.40/0.62 (((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310)))))),
% 0.40/0.62 inference(monotonicity,[status(thm)],[167])).
% 0.40/0.62 tff(169,plain,
% 0.40/0.62 (((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | (~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310))))),
% 0.40/0.62 inference(transitivity,[status(thm)],[168, 166])).
% 0.40/0.62 tff(170,plain,
% 0.40/0.62 ((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | ((vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310))))),
% 0.40/0.62 inference(quant_inst,[status(thm)],[])).
% 0.40/0.62 tff(171,plain,
% 0.40/0.62 ((~![Vtt: vTType, Vrt: vRawTable, Vn: vName, Vft: vFType] : ((vfindCol(Vn, val1, Vrt) = vsomeRawTable(tptp_fun_Vrt20_307(Vn, Vrt))) | (~vwelltypedRawtable(Vtt, Vrt)) | (~vmatchingAttrL(Vtt, val1)) | (~(vfindColType(Vn, Vtt) = vsomeFType(Vft))))) | (~vmatchingAttrL(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), val1)) | (vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))) | (~vwelltypedRawtable(tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308), vdropFirstColRaw(Vrt!311))) | (~(vfindColType(Vn!309, tptp_fun_Vttr_57(vacons(Vn1!312, val1), Vtt!308)) = vsomeFType(Vft!310)))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[170, 169])).
% 0.40/0.62 tff(172,plain,
% 0.40/0.62 (vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))),
% 0.40/0.62 inference(unit_resolution,[status(thm)],[171, 165, 152, 142, 123])).
% 0.40/0.62 tff(173,plain,
% 0.40/0.62 (^[Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : refl(((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr)))) <=> ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr)))))),
% 0.40/0.62 inference(bind,[status(th)],[])).
% 0.40/0.62 tff(174,plain,
% 0.40/0.62 (![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr)))) <=> ![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))),
% 0.40/0.62 inference(quant_intro,[status(thm)],[173])).
% 0.40/0.62 tff(175,plain,
% 0.40/0.62 (![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr)))) <=> ![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))),
% 0.40/0.62 inference(rewrite,[status(thm)],[])).
% 0.40/0.62 tff(176,plain,
% 0.40/0.62 (^[Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : rewrite(((~(Vn = Vn1)) => (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr)))) <=> ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr)))))),
% 0.40/0.62 inference(bind,[status(th)],[])).
% 0.40/0.62 tff(177,plain,
% 0.40/0.62 (![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((~(Vn = Vn1)) => (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr)))) <=> ![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))),
% 0.40/0.62 inference(quant_intro,[status(thm)],[176])).
% 0.40/0.62 tff(178,axiom,(![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((~(Vn = Vn1)) => (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''findCol-2'')).
% 0.40/0.62 tff(179,plain,
% 0.40/0.62 (![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[178, 177])).
% 0.40/0.62 tff(180,plain,
% 0.40/0.62 (![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[179, 175])).
% 0.40/0.62 tff(181,plain,(
% 0.40/0.62 ![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))),
% 0.40/0.62 inference(skolemize,[status(sab)],[180])).
% 0.40/0.62 tff(182,plain,
% 0.40/0.62 (![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[181, 174])).
% 0.40/0.62 tff(183,plain,
% 0.40/0.62 (((~![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))) | ((Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindCol(Vn!309, vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1), Vrt!311) = vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311))))) <=> ((~![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))) | (Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindCol(Vn!309, vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1), Vrt!311) = vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311))))),
% 0.40/0.62 inference(rewrite,[status(thm)],[])).
% 0.40/0.62 tff(184,plain,
% 0.40/0.62 ((~![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))) | ((Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindCol(Vn!309, vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1), Vrt!311) = vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311))))),
% 0.40/0.62 inference(quant_inst,[status(thm)],[])).
% 0.40/0.62 tff(185,plain,
% 0.40/0.62 ((~![Vn: vName, Vn1: vName, Valr: vAttrL, Vrtr: vRawTable] : ((Vn = Vn1) | (vfindCol(Vn, vacons(Vn1, Valr), Vrtr) = vfindCol(Vn, Valr, vdropFirstColRaw(Vrtr))))) | (Vn!309 = tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308)) | (vfindCol(Vn!309, vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1), Vrt!311) = vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311)))),
% 0.40/0.62 inference(modus_ponens,[status(thm)],[184, 183])).
% 0.40/0.62 tff(186,plain,
% 0.40/0.62 (vfindCol(Vn!309, vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1), Vrt!311) = vfindCol(Vn!309, val1, vdropFirstColRaw(Vrt!311))),
% 0.40/0.62 inference(unit_resolution,[status(thm)],[185, 182, 106])).
% 0.40/0.62 tff(187,plain,
% 0.40/0.62 (tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308) = tptp_fun_Va20_50(vacons(Vn1!312, val1))),
% 0.40/0.62 inference(symmetry,[status(thm)],[94])).
% 0.40/0.62 tff(188,plain,
% 0.40/0.62 (tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308) = Vn1!312),
% 0.40/0.62 inference(transitivity,[status(thm)],[187, 100])).
% 0.40/0.62 tff(189,plain,
% 0.40/0.62 (vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1) = vacons(Vn1!312, val1)),
% 0.40/0.62 inference(monotonicity,[status(thm)],[188])).
% 0.40/0.62 tff(190,plain,
% 0.40/0.62 (vacons(Vn1!312, val1) = vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1)),
% 0.40/0.62 inference(symmetry,[status(thm)],[189])).
% 0.40/0.62 tff(191,plain,
% 0.40/0.62 (vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vfindCol(Vn!309, vacons(tptp_fun_Va2_55(vacons(Vn1!312, val1), Vtt!308), val1), Vrt!311)),
% 0.40/0.62 inference(monotonicity,[status(thm)],[190])).
% 0.40/0.62 tff(192,plain,
% 0.40/0.62 (vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))),
% 0.46/0.64 inference(transitivity,[status(thm)],[191, 186, 172])).
% 0.46/0.64 tff(193,plain,
% 0.46/0.64 (^[Vrt20: vRawTable] : refl((~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20))) <=> (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20))))),
% 0.46/0.64 inference(bind,[status(th)],[])).
% 0.46/0.64 tff(194,plain,
% 0.46/0.64 (![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20))) <=> ![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20)))),
% 0.46/0.64 inference(quant_intro,[status(thm)],[193])).
% 0.46/0.64 tff(195,plain,
% 0.46/0.64 (![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20)))),
% 0.46/0.64 inference(and_elim,[status(thm)],[9])).
% 0.46/0.64 tff(196,plain,
% 0.46/0.64 (![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20)))),
% 0.46/0.64 inference(modus_ponens,[status(thm)],[195, 194])).
% 0.46/0.64 tff(197,plain,
% 0.46/0.64 ((~![Vrt20: vRawTable] : (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(Vrt20)))) | (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311)))))),
% 0.46/0.64 inference(quant_inst,[status(thm)],[])).
% 0.46/0.64 tff(198,plain,
% 0.46/0.64 (~(vfindCol(Vn!309, vacons(Vn1!312, val1), Vrt!311) = vsomeRawTable(tptp_fun_Vrt20_307(Vn!309, vdropFirstColRaw(Vrt!311))))),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[197, 196])).
% 0.46/0.64 tff(199,plain,
% 0.46/0.64 ($false),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[198, 192])).
% 0.46/0.64 % SZS output end Proof
% 0.46/0.64 % E exiting
%------------------------------------------------------------------------------