%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM263_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n023.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:04 PM UTC 2026
% Result : Theorem 0.38s 0.60s
% Output : Proof 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM263_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.15/0.33 % Computer : n023.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 19:57:55 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.38/0.60 % SZS status Theorem
% 0.38/0.60 % SZS output start Proof
% 0.38/0.60 tff(tptp_fun_Vt_233_type, type, (
% 0.38/0.60 tptp_fun_Vt_233: vAType)).
% 0.38/0.60 tff(vtypeOf_type, type, (
% 0.38/0.60 vtypeOf: vAval > vAType)).
% 0.38/0.60 tff(vgetExpValue_type, type, (
% 0.38/0.60 vgetExpValue: vExp > vAval)).
% 0.38/0.60 tff(tptp_fun_Vexp_227_type, type, (
% 0.38/0.60 tptp_fun_Vexp_227: vExp)).
% 0.38/0.60 tff(vgetAType_type, type, (
% 0.38/0.60 vgetAType: vOptAType > vAType)).
% 0.38/0.60 tff(vsomeAType_type, type, (
% 0.38/0.60 vsomeAType: vAType > vOptAType)).
% 0.38/0.60 tff(vNumber_type, type, (
% 0.38/0.60 vNumber: vAType)).
% 0.38/0.60 tff(tptp_fun_Vav0_198_type, type, (
% 0.38/0.60 tptp_fun_Vav0_198: vAnsMap > vAval)).
% 0.38/0.60 tff(tptp_fun_Vamr_232_type, type, (
% 0.38/0.60 tptp_fun_Vamr_232: vAnsMap)).
% 0.38/0.60 tff(vtypeAM_type, type, (
% 0.38/0.60 vtypeAM: vAnsMap > vATMap)).
% 0.38/0.60 tff(tptp_fun_Vam_230_type, type, (
% 0.38/0.60 tptp_fun_Vam_230: vAnsMap)).
% 0.38/0.60 tff(tptp_fun_Vamr0_197_type, type, (
% 0.38/0.60 tptp_fun_Vamr0_197: vAnsMap > vAnsMap)).
% 0.38/0.60 tff(tptp_fun_Vqid_228_type, type, (
% 0.38/0.60 tptp_fun_Vqid_228: vQID)).
% 0.38/0.60 tff(tptp_fun_Vqid0_199_type, type, (
% 0.38/0.60 tptp_fun_Vqid0_199: vAnsMap > vQID)).
% 0.38/0.60 tff(vatmbind_type, type, (
% 0.38/0.60 vatmbind: ( vQID * vAType * vATMap ) > vATMap)).
% 0.38/0.60 tff(vabind_type, type, (
% 0.38/0.60 vabind: ( vQID * vAval * vAnsMap ) > vAnsMap)).
% 0.38/0.60 tff(vgetAM_type, type, (
% 0.38/0.60 vgetAM: vQConf > vAnsMap)).
% 0.38/0.60 tff(vQC_type, type, (
% 0.38/0.60 vQC: ( vAnsMap * vQMap * vQuestionnaire ) > vQConf)).
% 0.38/0.60 tff(vqempty_type, type, (
% 0.38/0.60 vqempty: vQuestionnaire)).
% 0.38/0.60 tff(tptp_fun_Vqm_234_type, type, (
% 0.38/0.60 tptp_fun_Vqm_234: vQMap)).
% 0.38/0.60 tff(tptp_fun_Vqr_235_type, type, (
% 0.38/0.60 tptp_fun_Vqr_235: vQuestionnaire)).
% 0.38/0.60 tff(tptp_fun_Vqmr_229_type, type, (
% 0.38/0.60 tptp_fun_Vqmr_229: vQMap)).
% 0.38/0.60 tff(vgetQC_type, type, (
% 0.38/0.60 vgetQC: vOptQConf > vQConf)).
% 0.38/0.60 tff(vsomeQConf_type, type, (
% 0.38/0.60 vsomeQConf: vQConf > vOptQConf)).
% 0.38/0.60 tff(vreduce_type, type, (
% 0.38/0.60 vreduce: ( vQuestionnaire * vAnsMap * vQMap ) > vOptQConf)).
% 0.38/0.60 tff(vqsingle_type, type, (
% 0.38/0.60 vqsingle: vEntry > vQuestionnaire)).
% 0.38/0.60 tff(vvalue_type, type, (
% 0.38/0.60 vvalue: ( vQID * vAType * vExp ) > vEntry)).
% 0.38/0.60 tff(vptcheck_type, type, (
% 0.38/0.60 vptcheck: ( vMapConf * vQuestionnaire * vMapConf ) > $o)).
% 0.38/0.60 tff(vMC_type, type, (
% 0.38/0.60 vMC: ( vATMap * vATMap ) > vMapConf)).
% 0.38/0.60 tff(tptp_fun_Vqtm1_236_type, type, (
% 0.38/0.60 tptp_fun_Vqtm1_236: vATMap)).
% 0.38/0.60 tff(tptp_fun_Vatm1_231_type, type, (
% 0.38/0.60 tptp_fun_Vatm1_231: vATMap)).
% 0.38/0.60 tff(vtypeQM_type, type, (
% 0.38/0.60 vtypeQM: vQMap > vATMap)).
% 0.38/0.60 tff(vexpIsValue_type, type, (
% 0.38/0.60 vexpIsValue: vExp > $o)).
% 0.38/0.60 tff(vatmempty_type, type, (
% 0.38/0.60 vatmempty: vATMap)).
% 0.38/0.60 tff(vaempty_type, type, (
% 0.38/0.60 vaempty: vAnsMap)).
% 0.38/0.60 tff(vNum_type, type, (
% 0.38/0.60 vNum: vnat > vAval)).
% 0.38/0.60 tff(tptp_fun_VwildcardName01_68_type, type, (
% 0.38/0.60 tptp_fun_VwildcardName01_68: vAval > vnat)).
% 0.38/0.60 tff(vYesNo_type, type, (
% 0.38/0.60 vYesNo: vAType)).
% 0.38/0.60 tff(vB_type, type, (
% 0.38/0.60 vB: vYN > vAval)).
% 0.38/0.60 tff(tptp_fun_VwildcardName00_69_type, type, (
% 0.38/0.60 tptp_fun_VwildcardName00_69: vAval > vYN)).
% 0.38/0.60 tff(vText_type, type, (
% 0.38/0.60 vText: vAType)).
% 0.38/0.60 tff(vT_type, type, (
% 0.38/0.60 vT: vstring > vAval)).
% 0.38/0.60 tff(tptp_fun_VwildcardName02_67_type, type, (
% 0.38/0.60 tptp_fun_VwildcardName02_67: vAval > vstring)).
% 0.38/0.60 tff(tptp_fun_VwildcardName00_101_type, type, (
% 0.38/0.60 tptp_fun_VwildcardName00_101: vExp > vAval)).
% 0.38/0.60 tff(vconstant_type, type, (
% 0.38/0.60 vconstant: vAval > vExp)).
% 0.38/0.60 tff(vecheck_type, type, (
% 0.38/0.60 vecheck: ( vATMap * vExp ) > vOptAType)).
% 0.38/0.60 tff(vgetQuest_type, type, (
% 0.38/0.60 vgetQuest: vQConf > vQuestionnaire)).
% 0.38/0.60 tff(vgetQM_type, type, (
% 0.38/0.60 vgetQM: vQConf > vQMap)).
% 0.38/0.60 tff(1,plain,
% 0.38/0.60 (![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype) <=> ![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(2,plain,
% 0.38/0.60 (![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype) <=> ![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(3,axiom,(![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getAType-0'')).
% 0.38/0.60 tff(4,plain,
% 0.38/0.60 (![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.38/0.60 tff(5,plain,(
% 0.38/0.60 ![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)),
% 0.38/0.60 inference(skolemize,[status(sab)],[4])).
% 0.38/0.60 tff(6,plain,
% 0.38/0.60 (![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.38/0.60 tff(7,plain,
% 0.38/0.60 ((~![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)) | (vgetAType(vsomeAType(Vt!233)) = Vt!233)),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(8,plain,
% 0.38/0.60 (vgetAType(vsomeAType(Vt!233)) = Vt!233),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[7, 6])).
% 0.38/0.60 tff(9,plain,
% 0.38/0.60 (^[Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : refl((vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr))) <=> (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(10,plain,
% 0.38/0.60 (![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr))) <=> ![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[9])).
% 0.38/0.60 tff(11,plain,
% 0.38/0.60 (![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr))) <=> ![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr)))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(12,axiom,(![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''typeAM-1'')).
% 0.38/0.60 tff(13,plain,
% 0.38/0.60 (![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.38/0.60 tff(14,plain,(
% 0.38/0.60 ![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr)))),
% 0.38/0.60 inference(skolemize,[status(sab)],[13])).
% 0.38/0.60 tff(15,plain,
% 0.38/0.60 (![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[14, 10])).
% 0.38/0.60 tff(16,plain,
% 0.38/0.60 ((~![Vqid: vQID, Vav: vAval, Vamr: vAnsMap] : (vtypeAM(vabind(Vqid, Vav, Vamr)) = vatmbind(Vqid, vtypeOf(Vav), vtypeAM(Vamr)))) | (vtypeAM(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(17,plain,
% 0.38/0.60 (vtypeAM(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[16, 15])).
% 0.38/0.60 tff(18,plain,
% 0.38/0.60 (^[Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : refl((vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam) <=> (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(19,plain,
% 0.38/0.60 (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam) <=> ![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.38/0.60 inference(quant_intro,[status(thm)],[18])).
% 0.38/0.60 tff(20,plain,
% 0.38/0.60 (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam) <=> ![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(21,axiom,(![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getAM-0'')).
% 0.38/0.60 tff(22,plain,
% 0.38/0.60 (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.38/0.60 tff(23,plain,(
% 0.38/0.60 ![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.38/0.60 inference(skolemize,[status(sab)],[22])).
% 0.38/0.60 tff(24,plain,
% 0.38/0.60 (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[23, 19])).
% 0.38/0.60 tff(25,plain,
% 0.38/0.60 ((~![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)) | (vgetAM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(26,plain,
% 0.38/0.60 (vgetAM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[25, 24])).
% 0.38/0.60 tff(27,plain,
% 0.38/0.60 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc) <=> ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(28,plain,
% 0.38/0.60 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc) <=> ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(29,axiom,(![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQC-0'')).
% 0.38/0.60 tff(30,plain,
% 0.38/0.60 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[29, 28])).
% 0.38/0.60 tff(31,plain,(
% 0.38/0.60 ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.38/0.60 inference(skolemize,[status(sab)],[30])).
% 0.38/0.60 tff(32,plain,
% 0.38/0.60 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[31, 27])).
% 0.38/0.60 tff(33,plain,
% 0.38/0.60 ((~![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)) | (vgetQC(vsomeQConf(vQC(Vamr!232, Vqmr!229, Vqr!235))) = vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(34,plain,
% 0.38/0.60 (vgetQC(vsomeQConf(vQC(Vamr!232, Vqmr!229, Vqr!235))) = vQC(Vamr!232, Vqmr!229, Vqr!235)),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[33, 32])).
% 0.38/0.60 tff(35,plain,
% 0.38/0.60 ((~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : ((~(vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1)) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))) <=> (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : ((~(vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1)) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(36,plain,
% 0.38/0.60 ((~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : (((vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1))) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr)))) => vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))) <=> (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : ((~(vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1)) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(37,axiom,(~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : (((vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1))) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr)))) => vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Preservation-qsingle-value-expIsValue-True'')).
% 0.38/0.60 tff(38,plain,
% 0.38/0.60 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : ((~(vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1)) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.38/0.60 tff(39,plain,
% 0.38/0.60 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : ((~(vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1)) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[38, 35])).
% 0.38/0.60 tff(40,plain,
% 0.38/0.60 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : ((~(vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1)) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.38/0.60 tff(41,plain,
% 0.38/0.60 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vt: vAType, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap, Vqid: vQID, Vexp: vExp] : ((~(vexpIsValue(Vexp) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vvalue(Vqid, Vt, Vexp)), vMC(Vatm1, Vqtm1)) & (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[40, 35])).
% 0.38/0.60 tff(42,plain,(
% 0.38/0.60 ~((~(vexpIsValue(Vexp!227) & vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236)) & (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(Vamr!232, Vqmr!229, Vqr!235))))) | vptcheck(vMC(vtypeAM(Vamr!232), vtypeQM(Vqmr!229)), Vqr!235, vMC(Vatm1!231, Vqtm1!236)))),
% 0.38/0.60 inference(skolemize,[status(sab)],[41])).
% 0.38/0.60 tff(43,plain,
% 0.38/0.60 (vexpIsValue(Vexp!227) & vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236)) & (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(Vamr!232, Vqmr!229, Vqr!235)))),
% 0.38/0.60 inference(or_elim,[status(thm)],[42])).
% 0.38/0.60 tff(44,plain,
% 0.38/0.60 (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.60 inference(and_elim,[status(thm)],[43])).
% 0.38/0.60 tff(45,plain,
% 0.38/0.60 (vexpIsValue(Vexp!227)),
% 0.38/0.60 inference(and_elim,[status(thm)],[43])).
% 0.38/0.60 tff(46,plain,
% 0.38/0.60 (^[Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : refl(((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty)))) <=> ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty)))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(47,plain,
% 0.38/0.60 (![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty)))) <=> ![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[46])).
% 0.38/0.60 tff(48,plain,
% 0.38/0.60 (![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty)))) <=> ![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(49,plain,
% 0.38/0.60 (^[Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : rewrite((vexpIsValue(Vexp) => (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty)))) <=> ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty)))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(50,plain,
% 0.38/0.60 (![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : (vexpIsValue(Vexp) => (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty)))) <=> ![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[49])).
% 0.38/0.60 tff(51,axiom,(![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : (vexpIsValue(Vexp) => (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''reduce-2'')).
% 0.38/0.60 tff(52,plain,
% 0.38/0.60 (![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[51, 50])).
% 0.38/0.60 tff(53,plain,
% 0.38/0.60 (![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[52, 48])).
% 0.38/0.60 tff(54,plain,(
% 0.38/0.60 ![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))),
% 0.38/0.60 inference(skolemize,[status(sab)],[53])).
% 0.38/0.60 tff(55,plain,
% 0.38/0.60 (![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[54, 47])).
% 0.38/0.60 tff(56,plain,
% 0.38/0.60 (((~![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))) | ((~vexpIsValue(Vexp!227)) | (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))))) <=> ((~![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))) | (~vexpIsValue(Vexp!227)) | (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(57,plain,
% 0.38/0.60 ((~![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))) | ((~vexpIsValue(Vexp!227)) | (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(58,plain,
% 0.38/0.60 ((~![Vqm: vQMap, Vt: vAType, Vam: vAnsMap, Vqid: vQID, Vexp: vExp] : ((~vexpIsValue(Vexp)) | (vreduce(vqsingle(vvalue(Vqid, Vt, Vexp)), Vam, Vqm) = vsomeQConf(vQC(vabind(Vqid, vgetExpValue(Vexp), Vam), Vqm, vqempty))))) | (~vexpIsValue(Vexp!227)) | (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.38/0.60 tff(59,plain,
% 0.38/0.60 (vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234) = vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[58, 55, 45])).
% 0.38/0.60 tff(60,plain,
% 0.38/0.60 (vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vreduce(vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), Vam!230, Vqm!234)),
% 0.38/0.60 inference(symmetry,[status(thm)],[59])).
% 0.38/0.60 tff(61,plain,
% 0.38/0.60 (vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vsomeQConf(vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.60 inference(transitivity,[status(thm)],[60, 44])).
% 0.38/0.60 tff(62,plain,
% 0.38/0.60 (vgetQC(vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))) = vgetQC(vsomeQConf(vQC(Vamr!232, Vqmr!229, Vqr!235)))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[61])).
% 0.38/0.60 tff(63,plain,
% 0.38/0.60 ((~![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)) | (vgetQC(vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))) = vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(64,plain,
% 0.38/0.60 (vgetQC(vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))) = vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[63, 32])).
% 0.38/0.60 tff(65,plain,
% 0.38/0.60 (vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty) = vgetQC(vsomeQConf(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)))),
% 0.38/0.60 inference(symmetry,[status(thm)],[64])).
% 0.38/0.60 tff(66,plain,
% 0.38/0.60 (vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty) = vQC(Vamr!232, Vqmr!229, Vqr!235)),
% 0.38/0.60 inference(transitivity,[status(thm)],[65, 62, 34])).
% 0.38/0.60 tff(67,plain,
% 0.38/0.60 (vgetAM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vgetAM(vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[66])).
% 0.38/0.60 tff(68,plain,
% 0.38/0.60 (vgetAM(vQC(Vamr!232, Vqmr!229, Vqr!235)) = vgetAM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))),
% 0.38/0.60 inference(symmetry,[status(thm)],[67])).
% 0.38/0.60 tff(69,plain,
% 0.38/0.60 ((~![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)) | (vgetAM(vQC(Vamr!232, Vqmr!229, Vqr!235)) = Vamr!232)),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(70,plain,
% 0.38/0.60 (vgetAM(vQC(Vamr!232, Vqmr!229, Vqr!235)) = Vamr!232),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[69, 24])).
% 0.38/0.60 tff(71,plain,
% 0.38/0.60 (Vamr!232 = vgetAM(vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.60 inference(symmetry,[status(thm)],[70])).
% 0.38/0.60 tff(72,plain,
% 0.38/0.60 (Vamr!232 = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)),
% 0.38/0.60 inference(transitivity,[status(thm)],[71, 68, 26])).
% 0.38/0.60 tff(73,plain,
% 0.38/0.60 (vtypeAM(Vamr!232) = vtypeAM(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[72])).
% 0.38/0.60 tff(74,plain,
% 0.38/0.60 ((vaempty = Vamr!232) <=> (Vamr!232 = vaempty)),
% 0.38/0.60 inference(commutativity,[status(thm)],[])).
% 0.38/0.60 tff(75,plain,
% 0.38/0.60 (vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230) = vgetAM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))),
% 0.38/0.60 inference(symmetry,[status(thm)],[26])).
% 0.38/0.60 tff(76,plain,
% 0.38/0.60 (vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230) = Vamr!232),
% 0.38/0.60 inference(transitivity,[status(thm)],[75, 67, 70])).
% 0.38/0.60 tff(77,plain,
% 0.38/0.60 ((vaempty = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)) <=> (vaempty = Vamr!232)),
% 0.38/0.60 inference(monotonicity,[status(thm)],[76])).
% 0.38/0.60 tff(78,plain,
% 0.38/0.60 ((vaempty = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)) <=> (Vamr!232 = vaempty)),
% 0.38/0.60 inference(transitivity,[status(thm)],[77, 74])).
% 0.38/0.60 tff(79,plain,
% 0.38/0.60 ((~(vaempty = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230))) <=> (~(Vamr!232 = vaempty))),
% 0.38/0.60 inference(monotonicity,[status(thm)],[78])).
% 0.38/0.60 tff(80,plain,
% 0.38/0.60 (^[VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : refl((~(vaempty = vabind(VQID0, VAval0, VAnsMap0))) <=> (~(vaempty = vabind(VQID0, VAval0, VAnsMap0))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(81,plain,
% 0.38/0.60 (![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0))) <=> ![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0)))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[80])).
% 0.38/0.60 tff(82,plain,
% 0.38/0.60 (![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0))) <=> ![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0)))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(83,axiom,(![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''DIFF-aempty-abind'')).
% 0.38/0.60 tff(84,plain,
% 0.38/0.60 (![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.38/0.60 tff(85,plain,(
% 0.38/0.60 ![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0)))),
% 0.38/0.60 inference(skolemize,[status(sab)],[84])).
% 0.38/0.60 tff(86,plain,
% 0.38/0.60 (![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0)))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[85, 81])).
% 0.38/0.60 tff(87,plain,
% 0.38/0.60 ((~![VQID0: vQID, VAval0: vAval, VAnsMap0: vAnsMap] : (~(vaempty = vabind(VQID0, VAval0, VAnsMap0)))) | (~(vaempty = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)))),
% 0.38/0.60 inference(quant_inst,[status(thm)],[])).
% 0.38/0.60 tff(88,plain,
% 0.38/0.60 (~(vaempty = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[87, 86])).
% 0.38/0.60 tff(89,plain,
% 0.38/0.60 (~(Vamr!232 = vaempty)),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[88, 79])).
% 0.38/0.60 tff(90,plain,
% 0.38/0.60 (((~(Vamr!232 = vaempty)) | (~(vtypeAM(Vamr!232) = vatmempty))) | (Vamr!232 = vaempty)),
% 0.38/0.60 inference(tautology,[status(thm)],[])).
% 0.38/0.60 tff(91,plain,
% 0.38/0.60 ((~(Vamr!232 = vaempty)) | (~(vtypeAM(Vamr!232) = vatmempty))),
% 0.38/0.60 inference(unit_resolution,[status(thm)],[90, 89])).
% 0.38/0.60 tff(92,plain,
% 0.38/0.60 (^[VAnsMap0: vAnsMap] : refl(((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0)))))))) <=> ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0)))))))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(93,plain,
% 0.38/0.60 (![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0)))))))) <=> ![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[92])).
% 0.38/0.60 tff(94,plain,
% 0.38/0.60 (^[VAnsMap0: vAnsMap] : rewrite((((VAnsMap0 = vaempty) & (vtypeAM(VAnsMap0) = vatmempty)) | ((VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0))) & (vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0)))))) <=> ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0)))))))))),
% 0.38/0.60 inference(bind,[status(th)],[])).
% 0.38/0.60 tff(95,plain,
% 0.38/0.60 (![VAnsMap0: vAnsMap] : (((VAnsMap0 = vaempty) & (vtypeAM(VAnsMap0) = vatmempty)) | ((VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0))) & (vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0)))))) <=> ![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))),
% 0.38/0.60 inference(quant_intro,[status(thm)],[94])).
% 0.38/0.60 tff(96,plain,
% 0.38/0.60 (![VAnsMap0: vAnsMap] : (((VAnsMap0 = vaempty) & (vtypeAM(VAnsMap0) = vatmempty)) | ?[Vqid0: vQID, Vav0: vAval, Vamr0: vAnsMap] : ((VAnsMap0 = vabind(Vqid0, Vav0, Vamr0)) & (vtypeAM(VAnsMap0) = vatmbind(Vqid0, vtypeOf(Vav0), vtypeAM(Vamr0))))) <=> ![VAnsMap0: vAnsMap] : (((VAnsMap0 = vaempty) & (vtypeAM(VAnsMap0) = vatmempty)) | ?[Vqid0: vQID, Vav0: vAval, Vamr0: vAnsMap] : ((VAnsMap0 = vabind(Vqid0, Vav0, Vamr0)) & (vtypeAM(VAnsMap0) = vatmbind(Vqid0, vtypeOf(Vav0), vtypeAM(Vamr0)))))),
% 0.38/0.60 inference(rewrite,[status(thm)],[])).
% 0.38/0.60 tff(97,axiom,(![VAnsMap0: vAnsMap] : (((VAnsMap0 = vaempty) & (vtypeAM(VAnsMap0) = vatmempty)) | ?[Vqid0: vQID, Vav0: vAval, Vamr0: vAnsMap] : ((VAnsMap0 = vabind(Vqid0, Vav0, Vamr0)) & (vtypeAM(VAnsMap0) = vatmbind(Vqid0, vtypeOf(Vav0), vtypeAM(Vamr0)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''typeAM-INV'')).
% 0.38/0.60 tff(98,plain,
% 0.38/0.60 (![VAnsMap0: vAnsMap] : (((VAnsMap0 = vaempty) & (vtypeAM(VAnsMap0) = vatmempty)) | ?[Vqid0: vQID, Vav0: vAval, Vamr0: vAnsMap] : ((VAnsMap0 = vabind(Vqid0, Vav0, Vamr0)) & (vtypeAM(VAnsMap0) = vatmbind(Vqid0, vtypeOf(Vav0), vtypeAM(Vamr0)))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[97, 96])).
% 0.38/0.60 tff(99,plain,(
% 0.38/0.60 ![VAnsMap0: vAnsMap] : (((VAnsMap0 = vaempty) & (vtypeAM(VAnsMap0) = vatmempty)) | ((VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0))) & (vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))),
% 0.38/0.60 inference(skolemize,[status(sab)],[98])).
% 0.38/0.60 tff(100,plain,
% 0.38/0.60 (![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))),
% 0.38/0.60 inference(modus_ponens,[status(thm)],[99, 95])).
% 0.38/0.60 tff(101,plain,
% 0.38/0.60 (![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[100, 93])).
% 0.38/0.61 tff(102,plain,
% 0.38/0.61 (((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | ((~((~(Vamr!232 = vaempty)) | (~(vtypeAM(Vamr!232) = vatmempty)))) | (~((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))))))))) <=> ((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | (~((~(Vamr!232 = vaempty)) | (~(vtypeAM(Vamr!232) = vatmempty)))) | (~((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))))))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(103,plain,
% 0.38/0.61 ((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | ((~((~(Vamr!232 = vaempty)) | (~(vtypeAM(Vamr!232) = vatmempty)))) | (~((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))))))))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(104,plain,
% 0.38/0.61 ((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | (~((~(Vamr!232 = vaempty)) | (~(vtypeAM(Vamr!232) = vatmempty)))) | (~((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232)))))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.38/0.61 tff(105,plain,
% 0.38/0.61 ((~((~(Vamr!232 = vaempty)) | (~(vtypeAM(Vamr!232) = vatmempty)))) | (~((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232)))))))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[104, 101])).
% 0.38/0.61 tff(106,plain,
% 0.38/0.61 (~((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))))))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[105, 91])).
% 0.38/0.61 tff(107,plain,
% 0.38/0.61 (((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232)))))) | (vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))))),
% 0.38/0.61 inference(tautology,[status(thm)],[])).
% 0.38/0.61 tff(108,plain,
% 0.38/0.61 (vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232)))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[107, 106])).
% 0.38/0.61 tff(109,plain,
% 0.38/0.61 (vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vtypeAM(Vamr!232)),
% 0.38/0.61 inference(symmetry,[status(thm)],[108])).
% 0.38/0.61 tff(110,plain,
% 0.38/0.61 (vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230))),
% 0.38/0.61 inference(transitivity,[status(thm)],[109, 73, 17])).
% 0.38/0.61 tff(111,plain,
% 0.38/0.61 (^[VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : refl(((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1))))) <=> ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1))))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(112,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1))))) <=> ![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[111])).
% 0.38/0.61 tff(113,plain,
% 0.38/0.61 (^[VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : rewrite(((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1))) <=> ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1))))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(114,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1))) <=> ![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[113])).
% 0.38/0.61 tff(115,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1))) <=> ![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1)))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(116,plain,
% 0.38/0.61 (^[VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : trans(monotonicity(rewrite((((VQID0 = VQID1) & (VAType0 = VAType1)) & (VATMap0 = VATMap1)) <=> ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1))), (((vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1)) => (((VQID0 = VQID1) & (VAType0 = VAType1)) & (VATMap0 = VATMap1))) <=> ((vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1)) => ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1))))), rewrite(((vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1)) => ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1))) <=> ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1)))), (((vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1)) => (((VQID0 = VQID1) & (VAType0 = VAType1)) & (VATMap0 = VATMap1))) <=> ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1)))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(117,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1)) => (((VQID0 = VQID1) & (VAType0 = VAType1)) & (VATMap0 = VATMap1))) <=> ![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1)))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[116])).
% 0.38/0.61 tff(118,axiom,(![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1)) => (((VQID0 = VQID1) & (VAType0 = VAType1)) & (VATMap0 = VATMap1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''EQ-atmbind'')).
% 0.38/0.61 tff(119,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.38/0.61 tff(120,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[119, 115])).
% 0.38/0.61 tff(121,plain,(
% 0.38/0.61 ![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | ((VQID0 = VQID1) & (VAType0 = VAType1) & (VATMap0 = VATMap1)))),
% 0.38/0.61 inference(skolemize,[status(sab)],[120])).
% 0.38/0.61 tff(122,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[121, 114])).
% 0.38/0.61 tff(123,plain,
% 0.38/0.61 (![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[122, 112])).
% 0.38/0.61 tff(124,plain,
% 0.38/0.61 (((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | ((~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))))))) <=> ((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | (~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(125,plain,
% 0.38/0.61 (((~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230)))))) <=> ((~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(126,plain,
% 0.38/0.61 (((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | ((~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))))))) <=> ((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | ((~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227))))))))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[125])).
% 0.38/0.61 tff(127,plain,
% 0.38/0.61 (((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | ((~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))))))) <=> ((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | (~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))))))),
% 0.38/0.61 inference(transitivity,[status(thm)],[126, 124])).
% 0.38/0.61 tff(128,plain,
% 0.38/0.61 ((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | ((~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))))))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(129,plain,
% 0.38/0.61 ((~![VQID1: vQID, VATMap1: vATMap, VATMap0: vATMap, VAType0: vAType, VQID0: vQID, VAType1: vAType] : ((~(vatmbind(VQID0, VAType0, VATMap0) = vatmbind(VQID1, VAType1, VATMap1))) | (~((~(VQID0 = VQID1)) | (~(VAType0 = VAType1)) | (~(VATMap0 = VATMap1)))))) | (~(vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232))) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227))))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[128, 127])).
% 0.38/0.61 tff(130,plain,
% 0.38/0.61 (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[129, 123, 110])).
% 0.38/0.61 tff(131,plain,
% 0.38/0.61 (((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227))))) | (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227)))),
% 0.38/0.61 inference(tautology,[status(thm)],[])).
% 0.38/0.61 tff(132,plain,
% 0.38/0.61 (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[131, 130])).
% 0.38/0.61 tff(133,assumption,((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber))), introduced(assumption)).
% 0.38/0.61 tff(134,assumption,(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty), introduced(assumption)).
% 0.38/0.61 tff(135,plain,
% 0.38/0.61 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav) <=> ![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(136,plain,
% 0.38/0.61 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav) <=> ![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(137,axiom,(![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getExpValue-0'')).
% 0.38/0.61 tff(138,plain,
% 0.38/0.61 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.38/0.61 tff(139,plain,(
% 0.38/0.61 ![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.38/0.61 inference(skolemize,[status(sab)],[138])).
% 0.38/0.61 tff(140,plain,
% 0.38/0.61 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[139, 135])).
% 0.38/0.61 tff(141,plain,
% 0.38/0.61 ((~![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)) | (vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(Vexp!227))) = tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(142,plain,
% 0.38/0.61 (vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(Vexp!227))) = tptp_fun_VwildcardName00_101(Vexp!227)),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[141, 140])).
% 0.38/0.61 tff(143,plain,
% 0.38/0.61 (^[Ve: vExp] : refl(((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))) <=> ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(144,plain,
% 0.38/0.61 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[143])).
% 0.38/0.61 tff(145,plain,
% 0.38/0.61 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(146,plain,
% 0.38/0.61 (^[Ve: vExp] : rewrite((![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve))) <=> ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(147,plain,
% 0.38/0.61 (![Ve: vExp] : (![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[146])).
% 0.38/0.61 tff(148,axiom,(![Ve: vExp] : (![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''expIsValue-1'')).
% 0.38/0.61 tff(149,plain,
% 0.38/0.61 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[148, 147])).
% 0.38/0.61 tff(150,plain,
% 0.38/0.61 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[149, 145])).
% 0.38/0.61 tff(151,plain,(
% 0.38/0.61 ![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.38/0.61 inference(skolemize,[status(sab)],[150])).
% 0.38/0.61 tff(152,plain,
% 0.38/0.61 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[151, 144])).
% 0.38/0.61 tff(153,plain,
% 0.38/0.61 (((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | ((~vexpIsValue(Vexp!227)) | (Vexp!227 = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))))) <=> ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | (~vexpIsValue(Vexp!227)) | (Vexp!227 = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(154,plain,
% 0.38/0.61 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | ((~vexpIsValue(Vexp!227)) | (Vexp!227 = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(155,plain,
% 0.38/0.61 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | (~vexpIsValue(Vexp!227)) | (Vexp!227 = vconstant(tptp_fun_VwildcardName00_101(Vexp!227)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[154, 153])).
% 0.38/0.61 tff(156,plain,
% 0.38/0.61 (Vexp!227 = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[155, 152, 45])).
% 0.38/0.61 tff(157,plain,
% 0.38/0.61 (vgetExpValue(Vexp!227) = vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(Vexp!227)))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[156])).
% 0.38/0.61 tff(158,plain,
% 0.38/0.61 (vgetExpValue(Vexp!227) = tptp_fun_VwildcardName00_101(Vexp!227)),
% 0.38/0.61 inference(transitivity,[status(thm)],[157, 142])).
% 0.38/0.61 tff(159,plain,
% 0.38/0.61 (vtypeOf(vgetExpValue(Vexp!227)) = vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[158])).
% 0.38/0.61 tff(160,plain,
% 0.38/0.61 (vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vtypeOf(vgetExpValue(Vexp!227))),
% 0.38/0.61 inference(symmetry,[status(thm)],[159])).
% 0.38/0.61 tff(161,assumption,(~((~(tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) | (~(vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo)))), introduced(assumption)).
% 0.38/0.61 tff(162,plain,
% 0.38/0.61 (((~(tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) | (~(vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo))) | (vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo)),
% 0.38/0.61 inference(tautology,[status(thm)],[])).
% 0.38/0.61 tff(163,plain,
% 0.38/0.61 (vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[162, 161])).
% 0.38/0.61 tff(164,plain,
% 0.38/0.61 (vYesNo = vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.38/0.61 inference(symmetry,[status(thm)],[163])).
% 0.38/0.61 tff(165,plain,
% 0.38/0.61 (vYesNo = vtypeOf(vgetExpValue(Vexp!227))),
% 0.38/0.61 inference(transitivity,[status(thm)],[164, 160])).
% 0.38/0.61 tff(166,plain,
% 0.38/0.61 (vsomeAType(vYesNo) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[165])).
% 0.38/0.61 tff(167,plain,
% 0.38/0.61 (^[VwildcardName0: vATMap, Vn: vYN] : refl((vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo)) <=> (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo)))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(168,plain,
% 0.38/0.61 (![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo)) <=> ![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[167])).
% 0.38/0.61 tff(169,plain,
% 0.38/0.61 (![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo)) <=> ![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(170,axiom,(![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''echeck-0'')).
% 0.38/0.61 tff(171,plain,
% 0.38/0.61 (![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[170, 169])).
% 0.38/0.61 tff(172,plain,(
% 0.38/0.61 ![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))),
% 0.38/0.61 inference(skolemize,[status(sab)],[171])).
% 0.38/0.61 tff(173,plain,
% 0.38/0.61 (![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[172, 168])).
% 0.38/0.61 tff(174,plain,
% 0.38/0.61 ((~![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))) | (vecheck(vatmempty, vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vYesNo))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(175,plain,
% 0.38/0.61 (vecheck(vatmempty, vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vYesNo)),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[174, 173])).
% 0.38/0.61 tff(176,plain,
% 0.38/0.61 (((~(tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) | (~(vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo))) | (tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.38/0.61 inference(tautology,[status(thm)],[])).
% 0.38/0.61 tff(177,plain,
% 0.38/0.61 (tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[176, 161])).
% 0.38/0.61 tff(178,plain,
% 0.38/0.61 (vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))) = tptp_fun_VwildcardName00_101(Vexp!227)),
% 0.38/0.61 inference(symmetry,[status(thm)],[177])).
% 0.38/0.61 tff(179,plain,
% 0.38/0.61 (vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)))) = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[178])).
% 0.38/0.61 tff(180,plain,
% 0.38/0.61 (vconstant(tptp_fun_VwildcardName00_101(Vexp!227)) = vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.38/0.61 inference(symmetry,[status(thm)],[179])).
% 0.38/0.61 tff(181,plain,
% 0.38/0.61 (Vexp!227 = vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.38/0.61 inference(transitivity,[status(thm)],[156, 180])).
% 0.38/0.61 tff(182,plain,
% 0.38/0.61 (((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(vgetExpValue(Vexp!227))))) | (vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230))),
% 0.38/0.61 inference(tautology,[status(thm)],[])).
% 0.38/0.61 tff(183,plain,
% 0.38/0.61 (vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vtypeAM(Vam!230)),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[182, 130])).
% 0.38/0.61 tff(184,plain,
% 0.38/0.61 (vtypeAM(Vam!230) = vtypeAM(tptp_fun_Vamr0_197(Vamr!232))),
% 0.38/0.61 inference(symmetry,[status(thm)],[183])).
% 0.38/0.61 tff(185,plain,
% 0.38/0.61 (vtypeAM(Vam!230) = vatmempty),
% 0.38/0.61 inference(transitivity,[status(thm)],[184, 134])).
% 0.38/0.61 tff(186,plain,
% 0.38/0.61 (vecheck(vtypeAM(Vam!230), Vexp!227) = vecheck(vatmempty, vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)))))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[185, 181])).
% 0.38/0.61 tff(187,plain,
% 0.38/0.61 (vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))),
% 0.38/0.61 inference(and_elim,[status(thm)],[43])).
% 0.38/0.61 tff(188,plain,
% 0.38/0.61 (^[Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : refl(((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(189,plain,
% 0.38/0.61 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat))) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[188])).
% 0.38/0.61 tff(190,plain,
% 0.38/0.61 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat))) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(191,plain,
% 0.38/0.61 (^[Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : rewrite((vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (vecheck(Vatm, Vexp) = vsomeAType(Vat))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat))))),
% 0.38/0.61 inference(bind,[status(th)],[])).
% 0.38/0.61 tff(192,plain,
% 0.38/0.61 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : (vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (vecheck(Vatm, Vexp) = vsomeAType(Vat))) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))),
% 0.38/0.61 inference(quant_intro,[status(thm)],[191])).
% 0.38/0.61 tff(193,axiom,(![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : (vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (vecheck(Vatm, Vexp) = vsomeAType(Vat)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tvalue_inv2'')).
% 0.38/0.61 tff(194,plain,
% 0.38/0.61 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[193, 192])).
% 0.38/0.61 tff(195,plain,
% 0.38/0.61 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[194, 190])).
% 0.38/0.61 tff(196,plain,(
% 0.38/0.61 ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))),
% 0.38/0.61 inference(skolemize,[status(sab)],[195])).
% 0.38/0.61 tff(197,plain,
% 0.38/0.61 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[196, 189])).
% 0.38/0.61 tff(198,plain,
% 0.38/0.61 (((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))) | ((~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (vecheck(vtypeAM(Vam!230), Vexp!227) = vsomeAType(Vt!233)))) <=> ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))) | (~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (vecheck(vtypeAM(Vam!230), Vexp!227) = vsomeAType(Vt!233)))),
% 0.38/0.61 inference(rewrite,[status(thm)],[])).
% 0.38/0.61 tff(199,plain,
% 0.38/0.61 ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))) | ((~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (vecheck(vtypeAM(Vam!230), Vexp!227) = vsomeAType(Vt!233)))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(200,plain,
% 0.38/0.61 ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (vecheck(Vatm, Vexp) = vsomeAType(Vat)))) | (~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (vecheck(vtypeAM(Vam!230), Vexp!227) = vsomeAType(Vt!233))),
% 0.38/0.61 inference(modus_ponens,[status(thm)],[199, 198])).
% 0.38/0.61 tff(201,plain,
% 0.38/0.61 (vecheck(vtypeAM(Vam!230), Vexp!227) = vsomeAType(Vt!233)),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[200, 197, 187])).
% 0.38/0.61 tff(202,plain,
% 0.38/0.61 (vsomeAType(Vt!233) = vecheck(vtypeAM(Vam!230), Vexp!227)),
% 0.38/0.61 inference(symmetry,[status(thm)],[201])).
% 0.38/0.61 tff(203,plain,
% 0.38/0.61 (vsomeAType(Vt!233) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.38/0.61 inference(transitivity,[status(thm)],[202, 186, 175, 166])).
% 0.38/0.61 tff(204,plain,
% 0.38/0.61 (vgetAType(vsomeAType(Vt!233)) = vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227))))),
% 0.38/0.61 inference(monotonicity,[status(thm)],[203])).
% 0.38/0.61 tff(205,plain,
% 0.38/0.61 (vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))) = vgetAType(vsomeAType(Vt!233))),
% 0.38/0.61 inference(symmetry,[status(thm)],[204])).
% 0.38/0.61 tff(206,plain,
% 0.38/0.61 ((~![Vatype: vAType] : (vgetAType(vsomeAType(Vatype)) = Vatype)) | (vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))) = vtypeOf(vgetExpValue(Vexp!227)))),
% 0.38/0.61 inference(quant_inst,[status(thm)],[])).
% 0.38/0.61 tff(207,plain,
% 0.38/0.61 (vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))) = vtypeOf(vgetExpValue(Vexp!227))),
% 0.38/0.61 inference(unit_resolution,[status(thm)],[206, 6])).
% 0.38/0.61 tff(208,plain,
% 0.38/0.61 (vtypeOf(vgetExpValue(Vexp!227)) = vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227))))),
% 0.38/0.61 inference(symmetry,[status(thm)],[207])).
% 0.38/0.61 tff(209,plain,
% 0.38/0.61 (vtypeOf(vgetExpValue(Vexp!227)) = Vt!233),
% 0.38/0.61 inference(transitivity,[status(thm)],[208, 205, 8])).
% 0.38/0.61 tff(210,plain,
% 0.38/0.61 ((vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = Vt!233) <=> (vtypeOf(vgetExpValue(Vexp!227)) = Vt!233)),
% 0.38/0.61 inference(monotonicity,[status(thm)],[132])).
% 0.38/0.61 tff(211,plain,
% 0.38/0.61 ((Vt!233 = vtypeOf(tptp_fun_Vav0_198(Vamr!232))) <=> (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = Vt!233)),
% 0.38/0.62 inference(commutativity,[status(thm)],[])).
% 0.38/0.62 tff(212,plain,
% 0.38/0.62 ((Vt!233 = vtypeOf(tptp_fun_Vav0_198(Vamr!232))) <=> (vtypeOf(vgetExpValue(Vexp!227)) = Vt!233)),
% 0.38/0.62 inference(transitivity,[status(thm)],[211, 210])).
% 0.38/0.62 tff(213,plain,
% 0.38/0.62 ((~(Vt!233 = vtypeOf(tptp_fun_Vav0_198(Vamr!232)))) <=> (~(vtypeOf(vgetExpValue(Vexp!227)) = Vt!233))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[212])).
% 0.38/0.62 tff(214,plain,
% 0.38/0.62 (^[VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : refl((vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq) <=> (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(215,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq) <=> ![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.38/0.62 inference(quant_intro,[status(thm)],[214])).
% 0.38/0.62 tff(216,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq) <=> ![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(217,axiom,(![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQuest-0'')).
% 0.38/0.62 tff(218,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[217, 216])).
% 0.38/0.62 tff(219,plain,(
% 0.38/0.62 ![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.38/0.62 inference(skolemize,[status(sab)],[218])).
% 0.38/0.62 tff(220,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[219, 215])).
% 0.38/0.62 tff(221,plain,
% 0.38/0.62 ((~![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)) | (vgetQuest(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vqempty)),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(222,plain,
% 0.38/0.62 (vgetQuest(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vqempty),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[221, 220])).
% 0.38/0.62 tff(223,plain,
% 0.38/0.62 (vgetQuest(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vgetQuest(vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[66])).
% 0.38/0.62 tff(224,plain,
% 0.38/0.62 (vgetQuest(vQC(Vamr!232, Vqmr!229, Vqr!235)) = vgetQuest(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))),
% 0.38/0.62 inference(symmetry,[status(thm)],[223])).
% 0.38/0.62 tff(225,plain,
% 0.38/0.62 ((~![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)) | (vgetQuest(vQC(Vamr!232, Vqmr!229, Vqr!235)) = Vqr!235)),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(226,plain,
% 0.38/0.62 (vgetQuest(vQC(Vamr!232, Vqmr!229, Vqr!235)) = Vqr!235),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[225, 220])).
% 0.38/0.62 tff(227,plain,
% 0.38/0.62 (Vqr!235 = vgetQuest(vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.62 inference(symmetry,[status(thm)],[226])).
% 0.38/0.62 tff(228,plain,
% 0.38/0.62 (Vqr!235 = vqempty),
% 0.38/0.62 inference(transitivity,[status(thm)],[227, 224, 222])).
% 0.38/0.62 tff(229,plain,
% 0.38/0.62 (^[Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : refl(((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm)) <=> ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm)))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(230,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm)) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[229])).
% 0.38/0.62 tff(231,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm)) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(232,plain,
% 0.38/0.62 (^[Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : rewrite((vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (Vqm1 = Vqm)) <=> ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm)))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(233,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : (vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (Vqm1 = Vqm)) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[232])).
% 0.38/0.62 tff(234,axiom,(![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : (vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (Vqm1 = Vqm))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tvalue_inv4'')).
% 0.38/0.62 tff(235,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[234, 233])).
% 0.38/0.62 tff(236,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[235, 231])).
% 0.38/0.62 tff(237,plain,(
% 0.38/0.62 ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))),
% 0.38/0.62 inference(skolemize,[status(sab)],[236])).
% 0.38/0.62 tff(238,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[237, 230])).
% 0.38/0.62 tff(239,plain,
% 0.38/0.62 (((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))) | ((~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vqtm1!236 = vtypeQM(Vqm!234)))) <=> ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))) | (~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vqtm1!236 = vtypeQM(Vqm!234)))),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(240,plain,
% 0.38/0.62 ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))) | ((~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vqtm1!236 = vtypeQM(Vqm!234)))),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(241,plain,
% 0.38/0.62 ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vqm1 = Vqm))) | (~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vqtm1!236 = vtypeQM(Vqm!234))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[240, 239])).
% 0.38/0.62 tff(242,plain,
% 0.38/0.62 (Vqtm1!236 = vtypeQM(Vqm!234)),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[241, 238, 187])).
% 0.38/0.62 tff(243,plain,
% 0.38/0.62 (vtypeQM(Vqm!234) = Vqtm1!236),
% 0.38/0.62 inference(symmetry,[status(thm)],[242])).
% 0.38/0.62 tff(244,plain,
% 0.38/0.62 (^[VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : refl((vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm) <=> (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(245,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm) <=> ![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.38/0.62 inference(quant_intro,[status(thm)],[244])).
% 0.38/0.62 tff(246,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm) <=> ![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(247,axiom,(![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQM-0'')).
% 0.38/0.62 tff(248,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[247, 246])).
% 0.38/0.62 tff(249,plain,(
% 0.38/0.62 ![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.38/0.62 inference(skolemize,[status(sab)],[248])).
% 0.38/0.62 tff(250,plain,
% 0.38/0.62 (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[249, 245])).
% 0.38/0.62 tff(251,plain,
% 0.38/0.62 ((~![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)) | (vgetQM(vQC(Vamr!232, Vqmr!229, Vqr!235)) = Vqmr!229)),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(252,plain,
% 0.38/0.62 (vgetQM(vQC(Vamr!232, Vqmr!229, Vqr!235)) = Vqmr!229),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[251, 250])).
% 0.38/0.62 tff(253,plain,
% 0.38/0.62 (vgetQM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = vgetQM(vQC(Vamr!232, Vqmr!229, Vqr!235))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[66])).
% 0.38/0.62 tff(254,plain,
% 0.38/0.62 ((~![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)) | (vgetQM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = Vqm!234)),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(255,plain,
% 0.38/0.62 (vgetQM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty)) = Vqm!234),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[254, 250])).
% 0.38/0.62 tff(256,plain,
% 0.38/0.62 (Vqm!234 = vgetQM(vQC(vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230), Vqm!234, vqempty))),
% 0.38/0.62 inference(symmetry,[status(thm)],[255])).
% 0.38/0.62 tff(257,plain,
% 0.38/0.62 (Vqm!234 = Vqmr!229),
% 0.38/0.62 inference(transitivity,[status(thm)],[256, 253, 252])).
% 0.38/0.62 tff(258,plain,
% 0.38/0.62 (vtypeQM(Vqm!234) = vtypeQM(Vqmr!229)),
% 0.38/0.62 inference(monotonicity,[status(thm)],[257])).
% 0.38/0.62 tff(259,plain,
% 0.38/0.62 (vtypeQM(Vqmr!229) = vtypeQM(Vqm!234)),
% 0.38/0.62 inference(symmetry,[status(thm)],[258])).
% 0.38/0.62 tff(260,plain,
% 0.38/0.62 (vtypeQM(Vqmr!229) = Vqtm1!236),
% 0.38/0.62 inference(transitivity,[status(thm)],[259, 243])).
% 0.38/0.62 tff(261,plain,
% 0.38/0.62 (^[Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : refl(((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm))))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(262,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm))) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[261])).
% 0.38/0.62 tff(263,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm))) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(264,plain,
% 0.38/0.62 (^[Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : rewrite((vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (Vatm1 = vatmbind(Vqid, Vat, Vatm))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm))))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(265,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : (vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (Vatm1 = vatmbind(Vqid, Vat, Vatm))) <=> ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[264])).
% 0.38/0.62 tff(266,axiom,(![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : (vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1)) => (Vatm1 = vatmbind(Vqid, Vat, Vatm)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tvalue_inv3'')).
% 0.38/0.62 tff(267,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[266, 265])).
% 0.38/0.62 tff(268,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[267, 263])).
% 0.38/0.62 tff(269,plain,(
% 0.38/0.62 ![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))),
% 0.38/0.62 inference(skolemize,[status(sab)],[268])).
% 0.38/0.62 tff(270,plain,
% 0.38/0.62 (![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[269, 262])).
% 0.38/0.62 tff(271,plain,
% 0.38/0.62 (((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))) | ((~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vatm1!231 = vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230))))) <=> ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))) | (~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vatm1!231 = vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230))))),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(272,plain,
% 0.38/0.62 ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))) | ((~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vatm1!231 = vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230))))),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(273,plain,
% 0.38/0.62 ((~![Vqm: vATMap, Vatm: vATMap, Vqm1: vATMap, Vat: vAType, Vatm1: vATMap, Vqid: vQID, Vexp: vExp] : ((~vptcheck(vMC(Vatm, Vqm), vqsingle(vvalue(Vqid, Vat, Vexp)), vMC(Vatm1, Vqm1))) | (Vatm1 = vatmbind(Vqid, Vat, Vatm)))) | (~vptcheck(vMC(vtypeAM(Vam!230), vtypeQM(Vqm!234)), vqsingle(vvalue(Vqid!228, Vt!233, Vexp!227)), vMC(Vatm1!231, Vqtm1!236))) | (Vatm1!231 = vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230)))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[272, 271])).
% 0.38/0.62 tff(274,plain,
% 0.38/0.62 (Vatm1!231 = vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230))),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[273, 270, 187])).
% 0.38/0.62 tff(275,plain,
% 0.38/0.62 (vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230)) = Vatm1!231),
% 0.38/0.62 inference(symmetry,[status(thm)],[274])).
% 0.38/0.62 tff(276,assumption,(Vt!233 = vtypeOf(tptp_fun_Vav0_198(Vamr!232))), introduced(assumption)).
% 0.38/0.62 tff(277,plain,
% 0.38/0.62 (Vt!233 = vtypeOf(vgetExpValue(Vexp!227))),
% 0.38/0.62 inference(transitivity,[status(thm)],[276, 132])).
% 0.38/0.62 tff(278,plain,
% 0.38/0.62 (vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230)) = vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[277])).
% 0.38/0.62 tff(279,plain,
% 0.38/0.62 (vatmbind(Vqid!228, vtypeOf(vgetExpValue(Vexp!227)), vtypeAM(Vam!230)) = vatmbind(Vqid!228, Vt!233, vtypeAM(Vam!230))),
% 0.38/0.62 inference(symmetry,[status(thm)],[278])).
% 0.38/0.62 tff(280,plain,
% 0.38/0.62 (vtypeAM(Vamr!232) = Vatm1!231),
% 0.38/0.62 inference(transitivity,[status(thm)],[73, 17, 279, 275])).
% 0.38/0.62 tff(281,plain,
% 0.38/0.62 (vMC(vtypeAM(Vamr!232), vtypeQM(Vqmr!229)) = vMC(Vatm1!231, Vqtm1!236)),
% 0.38/0.62 inference(monotonicity,[status(thm)],[280, 260])).
% 0.38/0.62 tff(282,plain,
% 0.38/0.62 (vptcheck(vMC(vtypeAM(Vamr!232), vtypeQM(Vqmr!229)), Vqr!235, vMC(Vatm1!231, Vqtm1!236)) <=> vptcheck(vMC(Vatm1!231, Vqtm1!236), vqempty, vMC(Vatm1!231, Vqtm1!236))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[281, 228])).
% 0.38/0.62 tff(283,plain,
% 0.38/0.62 (vptcheck(vMC(Vatm1!231, Vqtm1!236), vqempty, vMC(Vatm1!231, Vqtm1!236)) <=> vptcheck(vMC(vtypeAM(Vamr!232), vtypeQM(Vqmr!229)), Vqr!235, vMC(Vatm1!231, Vqtm1!236))),
% 0.38/0.62 inference(symmetry,[status(thm)],[282])).
% 0.38/0.62 tff(284,plain,
% 0.38/0.62 (^[Vatm: vATMap, Vqm: vATMap] : refl(vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)) <=> vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(285,plain,
% 0.38/0.62 (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)) <=> ![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[284])).
% 0.38/0.62 tff(286,plain,
% 0.38/0.62 (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)) <=> ![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(287,axiom,(![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqempty'')).
% 0.38/0.62 tff(288,plain,
% 0.38/0.62 (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[287, 286])).
% 0.38/0.62 tff(289,plain,(
% 0.38/0.62 ![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.38/0.62 inference(skolemize,[status(sab)],[288])).
% 0.38/0.62 tff(290,plain,
% 0.38/0.62 (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[289, 285])).
% 0.38/0.62 tff(291,plain,
% 0.38/0.62 ((~![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))) | vptcheck(vMC(Vatm1!231, Vqtm1!236), vqempty, vMC(Vatm1!231, Vqtm1!236))),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(292,plain,
% 0.38/0.62 (vptcheck(vMC(Vatm1!231, Vqtm1!236), vqempty, vMC(Vatm1!231, Vqtm1!236))),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[291, 290])).
% 0.38/0.62 tff(293,plain,
% 0.38/0.62 (vptcheck(vMC(vtypeAM(Vamr!232), vtypeQM(Vqmr!229)), Vqr!235, vMC(Vatm1!231, Vqtm1!236))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[292, 283])).
% 0.38/0.62 tff(294,plain,
% 0.38/0.62 (~vptcheck(vMC(vtypeAM(Vamr!232), vtypeQM(Vqmr!229)), Vqr!235, vMC(Vatm1!231, Vqtm1!236))),
% 0.38/0.62 inference(or_elim,[status(thm)],[42])).
% 0.38/0.62 tff(295,plain,
% 0.38/0.62 ($false),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[294, 293])).
% 0.38/0.62 tff(296,plain,(~(Vt!233 = vtypeOf(tptp_fun_Vav0_198(Vamr!232)))), inference(lemma,lemma(discharge,[]))).
% 0.38/0.62 tff(297,plain,
% 0.38/0.62 (~(vtypeOf(vgetExpValue(Vexp!227)) = Vt!233)),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[296, 213])).
% 0.38/0.62 tff(298,plain,
% 0.38/0.62 ($false),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[297, 209])).
% 0.38/0.62 tff(299,plain,(((~(tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) | (~(vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty))), inference(lemma,lemma(discharge,[]))).
% 0.38/0.62 tff(300,plain,
% 0.38/0.62 ((~(tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) | (~(vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo))),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[299, 134])).
% 0.38/0.62 tff(301,plain,
% 0.38/0.62 (vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(Vexp!227))) = vgetExpValue(Vexp!227)),
% 0.38/0.62 inference(symmetry,[status(thm)],[157])).
% 0.38/0.62 tff(302,plain,
% 0.38/0.62 (tptp_fun_VwildcardName00_101(Vexp!227) = vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(Vexp!227)))),
% 0.38/0.62 inference(symmetry,[status(thm)],[142])).
% 0.38/0.62 tff(303,plain,
% 0.38/0.62 (tptp_fun_VwildcardName00_101(Vexp!227) = vgetExpValue(Vexp!227)),
% 0.38/0.62 inference(transitivity,[status(thm)],[302, 301])).
% 0.38/0.62 tff(304,plain,
% 0.38/0.62 (vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vtypeOf(vgetExpValue(Vexp!227))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[303])).
% 0.38/0.62 tff(305,plain,
% 0.38/0.62 (vtypeOf(vgetExpValue(Vexp!227)) = vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.38/0.62 inference(symmetry,[status(thm)],[304])).
% 0.38/0.62 tff(306,plain,
% 0.38/0.62 (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.38/0.62 inference(transitivity,[status(thm)],[132, 305])).
% 0.38/0.62 tff(307,plain,
% 0.38/0.62 ((vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo) <=> (vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo)),
% 0.38/0.62 inference(monotonicity,[status(thm)],[306])).
% 0.38/0.62 tff(308,assumption,(~((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText)))), introduced(assumption)).
% 0.38/0.62 tff(309,plain,
% 0.38/0.62 (((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText))) | (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText)),
% 0.38/0.62 inference(tautology,[status(thm)],[])).
% 0.38/0.62 tff(310,plain,
% 0.38/0.62 (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[309, 308])).
% 0.38/0.62 tff(311,plain,
% 0.38/0.62 (vText = vtypeOf(tptp_fun_Vav0_198(Vamr!232))),
% 0.38/0.62 inference(symmetry,[status(thm)],[310])).
% 0.38/0.62 tff(312,plain,
% 0.38/0.62 (vText = vtypeOf(vgetExpValue(Vexp!227))),
% 0.38/0.62 inference(transitivity,[status(thm)],[311, 132])).
% 0.38/0.62 tff(313,plain,
% 0.38/0.62 (vsomeAType(vText) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.38/0.62 inference(monotonicity,[status(thm)],[312])).
% 0.38/0.62 tff(314,plain,
% 0.38/0.62 (^[VwildcardName0: vATMap, Vn: vstring] : refl((vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText)) <=> (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText)))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(315,plain,
% 0.38/0.62 (![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText)) <=> ![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[314])).
% 0.38/0.62 tff(316,plain,
% 0.38/0.62 (![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText)) <=> ![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(317,axiom,(![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''echeck-2'')).
% 0.38/0.62 tff(318,plain,
% 0.38/0.62 (![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[317, 316])).
% 0.38/0.62 tff(319,plain,(
% 0.38/0.62 ![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))),
% 0.38/0.62 inference(skolemize,[status(sab)],[318])).
% 0.38/0.62 tff(320,plain,
% 0.38/0.62 (![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))),
% 0.38/0.62 inference(modus_ponens,[status(thm)],[319, 315])).
% 0.38/0.62 tff(321,plain,
% 0.38/0.62 ((~![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))) | (vecheck(vatmempty, vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vText))),
% 0.38/0.62 inference(quant_inst,[status(thm)],[])).
% 0.38/0.62 tff(322,plain,
% 0.38/0.62 (vecheck(vatmempty, vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vText)),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[321, 320])).
% 0.38/0.62 tff(323,plain,
% 0.38/0.62 (vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230) = vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230)),
% 0.38/0.62 inference(monotonicity,[status(thm)],[303])).
% 0.38/0.62 tff(324,plain,
% 0.38/0.62 (vabind(Vqid!228, vgetExpValue(Vexp!227), Vam!230) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230)),
% 0.38/0.62 inference(symmetry,[status(thm)],[323])).
% 0.38/0.62 tff(325,plain,
% 0.38/0.62 (((~(Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))) | (~(vtypeAM(Vamr!232) = vatmbind(tptp_fun_Vqid0_199(Vamr!232), vtypeOf(tptp_fun_Vav0_198(Vamr!232)), vtypeAM(tptp_fun_Vamr0_197(Vamr!232)))))) | (Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)))),
% 0.38/0.62 inference(tautology,[status(thm)],[])).
% 0.38/0.62 tff(326,plain,
% 0.38/0.62 (Vamr!232 = vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232))),
% 0.38/0.62 inference(unit_resolution,[status(thm)],[325, 106])).
% 0.38/0.62 tff(327,plain,
% 0.38/0.62 (vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = Vamr!232),
% 0.38/0.62 inference(symmetry,[status(thm)],[326])).
% 0.38/0.62 tff(328,plain,
% 0.38/0.62 (vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230)),
% 0.38/0.62 inference(transitivity,[status(thm)],[327, 71, 68, 26, 324])).
% 0.38/0.62 tff(329,plain,
% 0.38/0.62 (^[VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : refl(((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1))))) <=> ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1))))))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(330,plain,
% 0.38/0.62 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1))))) <=> ![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[329])).
% 0.38/0.62 tff(331,plain,
% 0.38/0.62 (^[VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : rewrite(((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1))) <=> ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1))))))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(332,plain,
% 0.38/0.62 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1))) <=> ![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[331])).
% 0.38/0.62 tff(333,plain,
% 0.38/0.62 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1))) <=> ![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1)))),
% 0.38/0.62 inference(rewrite,[status(thm)],[])).
% 0.38/0.62 tff(334,plain,
% 0.38/0.62 (^[VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : trans(monotonicity(rewrite((((VQID0 = VQID1) & (VAval0 = VAval1)) & (VAnsMap0 = VAnsMap1)) <=> ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1))), (((vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1)) => (((VQID0 = VQID1) & (VAval0 = VAval1)) & (VAnsMap0 = VAnsMap1))) <=> ((vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1)) => ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1))))), rewrite(((vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1)) => ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1))) <=> ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1)))), (((vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1)) => (((VQID0 = VQID1) & (VAval0 = VAval1)) & (VAnsMap0 = VAnsMap1))) <=> ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1)))))),
% 0.38/0.62 inference(bind,[status(th)],[])).
% 0.38/0.62 tff(335,plain,
% 0.38/0.62 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1)) => (((VQID0 = VQID1) & (VAval0 = VAval1)) & (VAnsMap0 = VAnsMap1))) <=> ![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1)))),
% 0.38/0.62 inference(quant_intro,[status(thm)],[334])).
% 0.38/0.62 tff(336,axiom,(![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1)) => (((VQID0 = VQID1) & (VAval0 = VAval1)) & (VAnsMap0 = VAnsMap1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''EQ-abind'')).
% 0.46/0.63 tff(337,plain,
% 0.46/0.63 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1)))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[336, 335])).
% 0.46/0.63 tff(338,plain,
% 0.46/0.63 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1)))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[337, 333])).
% 0.46/0.63 tff(339,plain,(
% 0.46/0.63 ![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | ((VQID0 = VQID1) & (VAval0 = VAval1) & (VAnsMap0 = VAnsMap1)))),
% 0.46/0.63 inference(skolemize,[status(sab)],[338])).
% 0.46/0.63 tff(340,plain,
% 0.46/0.63 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[339, 332])).
% 0.46/0.63 tff(341,plain,
% 0.46/0.63 (![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[340, 330])).
% 0.46/0.63 tff(342,plain,
% 0.46/0.63 (((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | ((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))))) <=> ((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | (~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))))),
% 0.46/0.63 inference(rewrite,[status(thm)],[])).
% 0.46/0.63 tff(343,plain,
% 0.46/0.63 (((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230))))) <=> ((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))))),
% 0.46/0.63 inference(rewrite,[status(thm)],[])).
% 0.46/0.63 tff(344,plain,
% 0.46/0.63 (((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | ((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))))) <=> ((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | ((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230))))))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[343])).
% 0.46/0.63 tff(345,plain,
% 0.46/0.63 (((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | ((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))))) <=> ((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | (~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))))),
% 0.46/0.63 inference(transitivity,[status(thm)],[344, 342])).
% 0.46/0.63 tff(346,plain,
% 0.46/0.63 ((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | ((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))))),
% 0.46/0.63 inference(quant_inst,[status(thm)],[])).
% 0.46/0.63 tff(347,plain,
% 0.46/0.63 ((~![VQID1: vQID, VAnsMap1: vAnsMap, VAval0: vAval, VAval1: vAval, VQID0: vQID, VAnsMap0: vAnsMap] : ((~(vabind(VQID0, VAval0, VAnsMap0) = vabind(VQID1, VAval1, VAnsMap1))) | (~((~(VAval0 = VAval1)) | (~(VQID0 = VQID1)) | (~(VAnsMap0 = VAnsMap1)))))) | (~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230))))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[346, 345])).
% 0.46/0.63 tff(348,plain,
% 0.46/0.63 ((~(vabind(tptp_fun_Vqid0_199(Vamr!232), tptp_fun_Vav0_198(Vamr!232), tptp_fun_Vamr0_197(Vamr!232)) = vabind(Vqid!228, tptp_fun_VwildcardName00_101(Vexp!227), Vam!230))) | (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230))))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[347, 341])).
% 0.46/0.63 tff(349,plain,
% 0.46/0.63 (~((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230)))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[348, 328])).
% 0.46/0.63 tff(350,plain,
% 0.46/0.63 (((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230))) | (tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(351,plain,
% 0.46/0.63 (tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227)),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[350, 349])).
% 0.46/0.63 tff(352,plain,
% 0.46/0.63 (((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText))) | (tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(353,plain,
% 0.46/0.63 (tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232)))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[352, 308])).
% 0.46/0.63 tff(354,plain,
% 0.46/0.63 (vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))) = tptp_fun_Vav0_198(Vamr!232)),
% 0.46/0.63 inference(symmetry,[status(thm)],[353])).
% 0.46/0.63 tff(355,plain,
% 0.46/0.63 (tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232)) = tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[351])).
% 0.46/0.63 tff(356,plain,
% 0.46/0.63 (tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227)) = tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))),
% 0.46/0.63 inference(symmetry,[status(thm)],[355])).
% 0.46/0.63 tff(357,plain,
% 0.46/0.63 (vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232)))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[356])).
% 0.46/0.63 tff(358,plain,
% 0.46/0.63 (vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))) = tptp_fun_VwildcardName00_101(Vexp!227)),
% 0.46/0.63 inference(transitivity,[status(thm)],[357, 354, 351])).
% 0.46/0.63 tff(359,plain,
% 0.46/0.63 (vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227)))) = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[358])).
% 0.46/0.63 tff(360,plain,
% 0.46/0.63 (vconstant(tptp_fun_VwildcardName00_101(Vexp!227)) = vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.46/0.63 inference(symmetry,[status(thm)],[359])).
% 0.46/0.63 tff(361,plain,
% 0.46/0.63 (Vexp!227 = vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.46/0.63 inference(transitivity,[status(thm)],[156, 360])).
% 0.46/0.63 tff(362,plain,
% 0.46/0.63 (vecheck(vtypeAM(Vam!230), Vexp!227) = vecheck(vatmempty, vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227)))))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[185, 361])).
% 0.46/0.63 tff(363,plain,
% 0.46/0.63 (vsomeAType(Vt!233) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.46/0.63 inference(transitivity,[status(thm)],[202, 362, 322, 313])).
% 0.46/0.63 tff(364,plain,
% 0.46/0.63 (vgetAType(vsomeAType(Vt!233)) = vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227))))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[363])).
% 0.46/0.63 tff(365,plain,
% 0.46/0.63 (vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))) = vgetAType(vsomeAType(Vt!233))),
% 0.46/0.63 inference(symmetry,[status(thm)],[364])).
% 0.46/0.63 tff(366,plain,
% 0.46/0.63 (vtypeOf(vgetExpValue(Vexp!227)) = Vt!233),
% 0.46/0.63 inference(transitivity,[status(thm)],[208, 365, 8])).
% 0.46/0.63 tff(367,plain,
% 0.46/0.63 ($false),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[297, 366])).
% 0.46/0.63 tff(368,plain,(((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty))), inference(lemma,lemma(discharge,[]))).
% 0.46/0.63 tff(369,plain,
% 0.46/0.63 ((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[368, 134])).
% 0.46/0.63 tff(370,plain,
% 0.46/0.63 (^[VAval0: vAval] : refl(((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo))))) <=> ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo))))))),
% 0.46/0.63 inference(bind,[status(th)],[])).
% 0.46/0.63 tff(371,plain,
% 0.46/0.63 (![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo))))) <=> ![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))),
% 0.46/0.63 inference(quant_intro,[status(thm)],[370])).
% 0.46/0.63 tff(372,plain,
% 0.46/0.63 (^[VAval0: vAval] : trans(monotonicity(rewrite(((VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0))) & (vtypeOf(VAval0) = vText)) <=> (~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText))))), rewrite(((VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0))) & (vtypeOf(VAval0) = vNumber)) <=> (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber))))), rewrite(((VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0))) & (vtypeOf(VAval0) = vYesNo)) <=> (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo))))), ((((VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0))) & (vtypeOf(VAval0) = vText)) | ((VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0))) & (vtypeOf(VAval0) = vNumber)) | ((VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0))) & (vtypeOf(VAval0) = vYesNo))) <=> ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo))))))), rewrite(((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo))))) <=> ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))), ((((VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0))) & (vtypeOf(VAval0) = vText)) | ((VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0))) & (vtypeOf(VAval0) = vNumber)) | ((VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0))) & (vtypeOf(VAval0) = vYesNo))) <=> ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))))),
% 0.46/0.63 inference(bind,[status(th)],[])).
% 0.46/0.63 tff(373,plain,
% 0.46/0.63 (![VAval0: vAval] : (((VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0))) & (vtypeOf(VAval0) = vText)) | ((VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0))) & (vtypeOf(VAval0) = vNumber)) | ((VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0))) & (vtypeOf(VAval0) = vYesNo))) <=> ![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))),
% 0.46/0.63 inference(quant_intro,[status(thm)],[372])).
% 0.46/0.63 tff(374,plain,
% 0.46/0.63 (![VAval0: vAval] : (?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)) | ?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo))) <=> ![VAval0: vAval] : (?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)) | ?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)))),
% 0.46/0.63 inference(rewrite,[status(thm)],[])).
% 0.46/0.63 tff(375,plain,
% 0.46/0.63 (^[VAval0: vAval] : trans(monotonicity(rewrite((?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber))) <=> (?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)))), (((?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber))) | ?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText))) <=> ((?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber))) | ?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText))))), rewrite(((?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber))) | ?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText))) <=> (?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)) | ?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)))), (((?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber))) | ?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText))) <=> (?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)) | ?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)))))),
% 0.46/0.63 inference(bind,[status(th)],[])).
% 0.46/0.63 tff(376,plain,
% 0.46/0.63 (![VAval0: vAval] : ((?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber))) | ?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText))) <=> ![VAval0: vAval] : (?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)) | ?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)))),
% 0.46/0.63 inference(quant_intro,[status(thm)],[375])).
% 0.46/0.63 tff(377,axiom,(![VAval0: vAval] : ((?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber))) | ?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''typeOf-INV'')).
% 0.46/0.63 tff(378,plain,
% 0.46/0.63 (![VAval0: vAval] : (?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)) | ?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[377, 376])).
% 0.46/0.63 tff(379,plain,
% 0.46/0.63 (![VAval0: vAval] : (?[VwildcardName02: vstring] : ((VAval0 = vT(VwildcardName02)) & (vtypeOf(VAval0) = vText)) | ?[VwildcardName01: vnat] : ((VAval0 = vNum(VwildcardName01)) & (vtypeOf(VAval0) = vNumber)) | ?[VwildcardName00: vYN] : ((VAval0 = vB(VwildcardName00)) & (vtypeOf(VAval0) = vYesNo)))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[378, 374])).
% 0.46/0.63 tff(380,plain,(
% 0.46/0.63 ![VAval0: vAval] : (((VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0))) & (vtypeOf(VAval0) = vText)) | ((VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0))) & (vtypeOf(VAval0) = vNumber)) | ((VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0))) & (vtypeOf(VAval0) = vYesNo)))),
% 0.46/0.63 inference(skolemize,[status(sab)],[379])).
% 0.46/0.63 tff(381,plain,
% 0.46/0.63 (![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[380, 373])).
% 0.46/0.63 tff(382,plain,
% 0.46/0.63 (![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[381, 371])).
% 0.46/0.63 tff(383,plain,
% 0.46/0.63 (((~![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))) | ((~((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo)))))) <=> ((~![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo)))))),
% 0.46/0.63 inference(rewrite,[status(thm)],[])).
% 0.46/0.63 tff(384,plain,
% 0.46/0.63 ((~![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))) | ((~((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo)))))),
% 0.46/0.63 inference(quant_inst,[status(thm)],[])).
% 0.46/0.63 tff(385,plain,
% 0.46/0.63 ((~![VAval0: vAval] : ((~((~(VAval0 = vT(tptp_fun_VwildcardName02_67(VAval0)))) | (~(vtypeOf(VAval0) = vText)))) | (~((~(VAval0 = vNum(tptp_fun_VwildcardName01_68(VAval0)))) | (~(vtypeOf(VAval0) = vNumber)))) | (~((~(VAval0 = vB(tptp_fun_VwildcardName00_69(VAval0)))) | (~(vtypeOf(VAval0) = vYesNo)))))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo))))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[384, 383])).
% 0.46/0.63 tff(386,plain,
% 0.46/0.63 ((~((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber)))) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo))))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[385, 382])).
% 0.46/0.63 tff(387,plain,
% 0.46/0.63 (~((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo)))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[386, 369, 133])).
% 0.46/0.63 tff(388,plain,
% 0.46/0.63 (((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo))) | (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo)),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(389,plain,
% 0.46/0.63 (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[388, 387])).
% 0.46/0.63 tff(390,plain,
% 0.46/0.63 (vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[389, 307])).
% 0.46/0.63 tff(391,plain,
% 0.46/0.63 (tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232)) = tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[351])).
% 0.46/0.63 tff(392,plain,
% 0.46/0.63 (tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)) = tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))),
% 0.46/0.63 inference(symmetry,[status(thm)],[391])).
% 0.46/0.63 tff(393,plain,
% 0.46/0.63 (vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232)))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[392])).
% 0.46/0.63 tff(394,plain,
% 0.46/0.63 (vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)))),
% 0.46/0.63 inference(symmetry,[status(thm)],[393])).
% 0.46/0.63 tff(395,plain,
% 0.46/0.63 ((tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232)))) <=> (tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[351, 394])).
% 0.46/0.63 tff(396,plain,
% 0.46/0.63 (((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo))) | (tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(397,plain,
% 0.46/0.63 (tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232)))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[396, 387])).
% 0.46/0.63 tff(398,plain,
% 0.46/0.63 (tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[397, 395])).
% 0.46/0.63 tff(399,plain,
% 0.46/0.63 ((~((~(tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) | (~(vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo)))) | (~(tptp_fun_VwildcardName00_101(Vexp!227) = vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) | (~(vtypeOf(tptp_fun_VwildcardName00_101(Vexp!227)) = vYesNo))),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(400,plain,
% 0.46/0.63 ($false),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[399, 398, 390, 300])).
% 0.46/0.63 tff(401,plain,((~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)) | (~((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber))))), inference(lemma,lemma(discharge,[]))).
% 0.46/0.63 tff(402,plain,
% 0.46/0.63 (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[401, 133])).
% 0.46/0.63 tff(403,plain,
% 0.46/0.63 (((~(tptp_fun_Vamr0_197(Vamr!232) = vaempty)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty))) | (vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(404,plain,
% 0.46/0.63 ((~(tptp_fun_Vamr0_197(Vamr!232) = vaempty)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[403, 402])).
% 0.46/0.63 tff(405,plain,
% 0.46/0.63 (((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | ((~((~(tptp_fun_Vamr0_197(Vamr!232) = vaempty)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)))) | (~((~(tptp_fun_Vamr0_197(Vamr!232) = vabind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232)))))))))) <=> ((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | (~((~(tptp_fun_Vamr0_197(Vamr!232) = vaempty)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)))) | (~((~(tptp_fun_Vamr0_197(Vamr!232) = vabind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232)))))))))),
% 0.46/0.63 inference(rewrite,[status(thm)],[])).
% 0.46/0.63 tff(406,plain,
% 0.46/0.63 ((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | ((~((~(tptp_fun_Vamr0_197(Vamr!232) = vaempty)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)))) | (~((~(tptp_fun_Vamr0_197(Vamr!232) = vabind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232)))))))))),
% 0.46/0.63 inference(quant_inst,[status(thm)],[])).
% 0.46/0.63 tff(407,plain,
% 0.46/0.63 ((~![VAnsMap0: vAnsMap] : ((~((~(VAnsMap0 = vaempty)) | (~(vtypeAM(VAnsMap0) = vatmempty)))) | (~((~(VAnsMap0 = vabind(tptp_fun_Vqid0_199(VAnsMap0), tptp_fun_Vav0_198(VAnsMap0), tptp_fun_Vamr0_197(VAnsMap0)))) | (~(vtypeAM(VAnsMap0) = vatmbind(tptp_fun_Vqid0_199(VAnsMap0), vtypeOf(tptp_fun_Vav0_198(VAnsMap0)), vtypeAM(tptp_fun_Vamr0_197(VAnsMap0))))))))) | (~((~(tptp_fun_Vamr0_197(Vamr!232) = vaempty)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)))) | (~((~(tptp_fun_Vamr0_197(Vamr!232) = vabind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))))))),
% 0.46/0.63 inference(modus_ponens,[status(thm)],[406, 405])).
% 0.46/0.63 tff(408,plain,
% 0.46/0.63 ((~((~(tptp_fun_Vamr0_197(Vamr!232) = vaempty)) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmempty)))) | (~((~(tptp_fun_Vamr0_197(Vamr!232) = vabind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))))))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[407, 101])).
% 0.46/0.63 tff(409,plain,
% 0.46/0.63 (~((~(tptp_fun_Vamr0_197(Vamr!232) = vabind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232)))))))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[408, 404])).
% 0.46/0.63 tff(410,plain,
% 0.46/0.63 (((~(tptp_fun_Vamr0_197(Vamr!232) = vabind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)), tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))))) | (vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232)))))),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(411,plain,
% 0.46/0.63 (vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[410, 409])).
% 0.46/0.63 tff(412,plain,
% 0.46/0.63 ((~![VwildcardName0: vATMap, Vn: vstring] : (vecheck(VwildcardName0, vconstant(vT(Vn))) = vsomeAType(vText))) | (vecheck(vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230))), vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vText))),
% 0.46/0.63 inference(quant_inst,[status(thm)],[])).
% 0.46/0.63 tff(413,plain,
% 0.46/0.63 (vecheck(vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230))), vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vText)),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[412, 320])).
% 0.46/0.63 tff(414,plain,
% 0.46/0.63 (((~(tptp_fun_Vqid0_199(Vamr!232) = Vqid!228)) | (~(tptp_fun_Vav0_198(Vamr!232) = tptp_fun_VwildcardName00_101(Vexp!227))) | (~(tptp_fun_Vamr0_197(Vamr!232) = Vam!230))) | (tptp_fun_Vamr0_197(Vamr!232) = Vam!230)),
% 0.46/0.63 inference(tautology,[status(thm)],[])).
% 0.46/0.63 tff(415,plain,
% 0.46/0.63 (tptp_fun_Vamr0_197(Vamr!232) = Vam!230),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[414, 349])).
% 0.46/0.63 tff(416,plain,
% 0.46/0.63 (tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232)) = tptp_fun_Vamr0_197(Vam!230)),
% 0.46/0.63 inference(monotonicity,[status(thm)],[415])).
% 0.46/0.63 tff(417,plain,
% 0.46/0.63 (vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))) = vtypeAM(tptp_fun_Vamr0_197(Vam!230))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[416])).
% 0.46/0.63 tff(418,plain,
% 0.46/0.63 (tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232)) = tptp_fun_Vav0_198(Vam!230)),
% 0.46/0.63 inference(monotonicity,[status(thm)],[415])).
% 0.46/0.63 tff(419,plain,
% 0.46/0.63 (vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))) = vtypeOf(tptp_fun_Vav0_198(Vam!230))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[418])).
% 0.46/0.63 tff(420,plain,
% 0.46/0.63 (tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)) = tptp_fun_Vqid0_199(Vam!230)),
% 0.46/0.63 inference(monotonicity,[status(thm)],[415])).
% 0.46/0.63 tff(421,plain,
% 0.46/0.63 (vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232)))) = vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230)))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[420, 419, 417])).
% 0.46/0.63 tff(422,assumption,(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))), introduced(assumption)).
% 0.46/0.63 tff(423,plain,
% 0.46/0.63 (vtypeAM(Vam!230) = vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230)))),
% 0.46/0.63 inference(transitivity,[status(thm)],[184, 422, 421])).
% 0.46/0.63 tff(424,plain,
% 0.46/0.63 (vecheck(vtypeAM(Vam!230), Vexp!227) = vecheck(vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230))), vconstant(vT(tptp_fun_VwildcardName02_67(tptp_fun_VwildcardName00_101(Vexp!227)))))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[423, 361])).
% 0.46/0.63 tff(425,plain,
% 0.46/0.63 (vsomeAType(Vt!233) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.46/0.63 inference(transitivity,[status(thm)],[202, 424, 413, 313])).
% 0.46/0.63 tff(426,plain,
% 0.46/0.63 (vgetAType(vsomeAType(Vt!233)) = vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227))))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[425])).
% 0.46/0.63 tff(427,plain,
% 0.46/0.63 (vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))) = vgetAType(vsomeAType(Vt!233))),
% 0.46/0.63 inference(symmetry,[status(thm)],[426])).
% 0.46/0.63 tff(428,plain,
% 0.46/0.63 (vtypeOf(vgetExpValue(Vexp!227)) = Vt!233),
% 0.46/0.63 inference(transitivity,[status(thm)],[208, 427, 8])).
% 0.46/0.63 tff(429,plain,
% 0.46/0.63 ($false),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[297, 428])).
% 0.46/0.63 tff(430,plain,(((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText))) | (~(vtypeAM(tptp_fun_Vamr0_197(Vamr!232)) = vatmbind(tptp_fun_Vqid0_199(tptp_fun_Vamr0_197(Vamr!232)), vtypeOf(tptp_fun_Vav0_198(tptp_fun_Vamr0_197(Vamr!232))), vtypeAM(tptp_fun_Vamr0_197(tptp_fun_Vamr0_197(Vamr!232))))))), inference(lemma,lemma(discharge,[]))).
% 0.46/0.63 tff(431,plain,
% 0.46/0.63 ((~(tptp_fun_Vav0_198(Vamr!232) = vT(tptp_fun_VwildcardName02_67(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vText))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[430, 411])).
% 0.46/0.63 tff(432,plain,
% 0.46/0.63 (~((~(tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo)))),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[386, 431, 133])).
% 0.46/0.63 tff(433,plain,
% 0.46/0.63 (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vYesNo),
% 0.46/0.63 inference(unit_resolution,[status(thm)],[388, 432])).
% 0.46/0.63 tff(434,plain,
% 0.46/0.63 (vYesNo = vtypeOf(tptp_fun_Vav0_198(Vamr!232))),
% 0.46/0.63 inference(symmetry,[status(thm)],[433])).
% 0.46/0.63 tff(435,plain,
% 0.46/0.63 (vYesNo = vtypeOf(vgetExpValue(Vexp!227))),
% 0.46/0.63 inference(transitivity,[status(thm)],[434, 132])).
% 0.46/0.63 tff(436,plain,
% 0.46/0.63 (vsomeAType(vYesNo) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.46/0.63 inference(monotonicity,[status(thm)],[435])).
% 0.46/0.63 tff(437,plain,
% 0.46/0.63 ((~![VwildcardName0: vATMap, Vn: vYN] : (vecheck(VwildcardName0, vconstant(vB(Vn))) = vsomeAType(vYesNo))) | (vecheck(vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230))), vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vYesNo))),
% 0.46/0.64 inference(quant_inst,[status(thm)],[])).
% 0.46/0.64 tff(438,plain,
% 0.46/0.64 (vecheck(vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230))), vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vYesNo)),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[437, 173])).
% 0.46/0.64 tff(439,plain,
% 0.46/0.64 (tptp_fun_Vav0_198(Vamr!232) = vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232)))),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[396, 432])).
% 0.46/0.64 tff(440,plain,
% 0.46/0.64 (vB(tptp_fun_VwildcardName00_69(tptp_fun_Vav0_198(Vamr!232))) = tptp_fun_Vav0_198(Vamr!232)),
% 0.46/0.64 inference(symmetry,[status(thm)],[439])).
% 0.46/0.64 tff(441,plain,
% 0.46/0.64 (vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))) = tptp_fun_VwildcardName00_101(Vexp!227)),
% 0.46/0.64 inference(transitivity,[status(thm)],[393, 440, 351])).
% 0.46/0.64 tff(442,plain,
% 0.46/0.64 (vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)))) = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.46/0.64 inference(monotonicity,[status(thm)],[441])).
% 0.46/0.64 tff(443,plain,
% 0.46/0.64 (vconstant(tptp_fun_VwildcardName00_101(Vexp!227)) = vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.46/0.64 inference(symmetry,[status(thm)],[442])).
% 0.46/0.64 tff(444,plain,
% 0.46/0.64 (Vexp!227 = vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.46/0.64 inference(transitivity,[status(thm)],[156, 443])).
% 0.46/0.64 tff(445,plain,
% 0.46/0.64 (vtypeAM(Vam!230) = vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230)))),
% 0.46/0.64 inference(transitivity,[status(thm)],[184, 411, 421])).
% 0.46/0.64 tff(446,plain,
% 0.46/0.64 (vecheck(vtypeAM(Vam!230), Vexp!227) = vecheck(vatmbind(tptp_fun_Vqid0_199(Vam!230), vtypeOf(tptp_fun_Vav0_198(Vam!230)), vtypeAM(tptp_fun_Vamr0_197(Vam!230))), vconstant(vB(tptp_fun_VwildcardName00_69(tptp_fun_VwildcardName00_101(Vexp!227)))))),
% 0.46/0.64 inference(monotonicity,[status(thm)],[445, 444])).
% 0.46/0.64 tff(447,plain,
% 0.46/0.64 (vsomeAType(Vt!233) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.46/0.64 inference(transitivity,[status(thm)],[202, 446, 438, 436])).
% 0.46/0.64 tff(448,plain,
% 0.46/0.64 (vgetAType(vsomeAType(Vt!233)) = vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227))))),
% 0.46/0.64 inference(monotonicity,[status(thm)],[447])).
% 0.46/0.64 tff(449,plain,
% 0.46/0.64 (vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))) = vgetAType(vsomeAType(Vt!233))),
% 0.46/0.64 inference(symmetry,[status(thm)],[448])).
% 0.46/0.64 tff(450,plain,
% 0.46/0.64 (vtypeOf(vgetExpValue(Vexp!227)) = Vt!233),
% 0.46/0.64 inference(transitivity,[status(thm)],[208, 449, 8])).
% 0.46/0.64 tff(451,plain,
% 0.46/0.64 ($false),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[297, 450])).
% 0.46/0.64 tff(452,plain,(~((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber)))), inference(lemma,lemma(discharge,[]))).
% 0.46/0.64 tff(453,plain,
% 0.46/0.64 (((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber))) | (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber)),
% 0.46/0.64 inference(tautology,[status(thm)],[])).
% 0.46/0.64 tff(454,plain,
% 0.46/0.64 (vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[453, 452])).
% 0.46/0.64 tff(455,plain,
% 0.46/0.64 (vNumber = vtypeOf(tptp_fun_Vav0_198(Vamr!232))),
% 0.46/0.64 inference(symmetry,[status(thm)],[454])).
% 0.46/0.64 tff(456,plain,
% 0.46/0.64 (vNumber = vtypeOf(vgetExpValue(Vexp!227))),
% 0.46/0.64 inference(transitivity,[status(thm)],[455, 132])).
% 0.46/0.64 tff(457,plain,
% 0.46/0.64 (vsomeAType(vNumber) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.46/0.64 inference(monotonicity,[status(thm)],[456])).
% 0.46/0.64 tff(458,plain,
% 0.46/0.64 (^[VwildcardName0: vATMap, Vn: vnat] : refl((vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber)) <=> (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber)))),
% 0.46/0.64 inference(bind,[status(th)],[])).
% 0.46/0.64 tff(459,plain,
% 0.46/0.64 (![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber)) <=> ![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber))),
% 0.46/0.64 inference(quant_intro,[status(thm)],[458])).
% 0.46/0.64 tff(460,plain,
% 0.46/0.64 (![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber)) <=> ![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber))),
% 0.46/0.64 inference(rewrite,[status(thm)],[])).
% 0.46/0.64 tff(461,axiom,(![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''echeck-1'')).
% 0.46/0.64 tff(462,plain,
% 0.46/0.64 (![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber))),
% 0.46/0.64 inference(modus_ponens,[status(thm)],[461, 460])).
% 0.46/0.64 tff(463,plain,(
% 0.46/0.64 ![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber))),
% 0.46/0.64 inference(skolemize,[status(sab)],[462])).
% 0.46/0.64 tff(464,plain,
% 0.46/0.64 (![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber))),
% 0.46/0.64 inference(modus_ponens,[status(thm)],[463, 459])).
% 0.46/0.64 tff(465,plain,
% 0.46/0.64 ((~![VwildcardName0: vATMap, Vn: vnat] : (vecheck(VwildcardName0, vconstant(vNum(Vn))) = vsomeAType(vNumber))) | (vecheck(vtypeAM(Vam!230), vconstant(vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vNumber))),
% 0.46/0.64 inference(quant_inst,[status(thm)],[])).
% 0.46/0.64 tff(466,plain,
% 0.46/0.64 (vecheck(vtypeAM(Vam!230), vconstant(vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227))))) = vsomeAType(vNumber)),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[465, 464])).
% 0.46/0.64 tff(467,plain,
% 0.46/0.64 (((~(tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))) | (~(vtypeOf(tptp_fun_Vav0_198(Vamr!232)) = vNumber))) | (tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))))),
% 0.46/0.64 inference(tautology,[status(thm)],[])).
% 0.46/0.64 tff(468,plain,
% 0.46/0.64 (tptp_fun_Vav0_198(Vamr!232) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232)))),
% 0.46/0.64 inference(unit_resolution,[status(thm)],[467, 452])).
% 0.46/0.64 tff(469,plain,
% 0.46/0.64 (vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))) = tptp_fun_Vav0_198(Vamr!232)),
% 0.46/0.64 inference(symmetry,[status(thm)],[468])).
% 0.46/0.64 tff(470,plain,
% 0.46/0.64 (tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232)) = tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.46/0.64 inference(monotonicity,[status(thm)],[351])).
% 0.46/0.64 tff(471,plain,
% 0.46/0.64 (tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227)) = tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232))),
% 0.46/0.64 inference(symmetry,[status(thm)],[470])).
% 0.46/0.64 tff(472,plain,
% 0.46/0.64 (vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227))) = vNum(tptp_fun_VwildcardName01_68(tptp_fun_Vav0_198(Vamr!232)))),
% 0.46/0.64 inference(monotonicity,[status(thm)],[471])).
% 0.46/0.64 tff(473,plain,
% 0.46/0.64 (vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227))) = tptp_fun_VwildcardName00_101(Vexp!227)),
% 0.46/0.64 inference(transitivity,[status(thm)],[472, 469, 351])).
% 0.46/0.64 tff(474,plain,
% 0.46/0.64 (vconstant(vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227)))) = vconstant(tptp_fun_VwildcardName00_101(Vexp!227))),
% 0.46/0.64 inference(monotonicity,[status(thm)],[473])).
% 0.46/0.64 tff(475,plain,
% 0.46/0.64 (vconstant(tptp_fun_VwildcardName00_101(Vexp!227)) = vconstant(vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.46/0.64 inference(symmetry,[status(thm)],[474])).
% 0.46/0.64 tff(476,plain,
% 0.46/0.64 (Vexp!227 = vconstant(vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227))))),
% 0.46/0.64 inference(transitivity,[status(thm)],[156, 475])).
% 0.46/0.64 tff(477,plain,
% 0.46/0.64 (vecheck(vtypeAM(Vam!230), Vexp!227) = vecheck(vtypeAM(Vam!230), vconstant(vNum(tptp_fun_VwildcardName01_68(tptp_fun_VwildcardName00_101(Vexp!227)))))),
% 0.46/0.66 inference(monotonicity,[status(thm)],[476])).
% 0.46/0.66 tff(478,plain,
% 0.46/0.66 (vsomeAType(Vt!233) = vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))),
% 0.46/0.66 inference(transitivity,[status(thm)],[202, 477, 466, 457])).
% 0.46/0.66 tff(479,plain,
% 0.46/0.66 (vgetAType(vsomeAType(Vt!233)) = vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227))))),
% 0.46/0.66 inference(monotonicity,[status(thm)],[478])).
% 0.46/0.66 tff(480,plain,
% 0.46/0.66 (vgetAType(vsomeAType(vtypeOf(vgetExpValue(Vexp!227)))) = vgetAType(vsomeAType(Vt!233))),
% 0.46/0.66 inference(symmetry,[status(thm)],[479])).
% 0.46/0.66 tff(481,plain,
% 0.46/0.66 (vtypeOf(vgetExpValue(Vexp!227)) = Vt!233),
% 0.46/0.66 inference(transitivity,[status(thm)],[208, 480, 8])).
% 0.46/0.66 tff(482,plain,
% 0.46/0.66 ($false),
% 0.46/0.66 inference(unit_resolution,[status(thm)],[297, 481])).
% 0.46/0.66 % SZS output end Proof
% 0.46/0.66 % E exiting
%------------------------------------------------------------------------------