%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM276_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n005.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:05 PM UTC 2026
% Result : Theorem 0.29s 0.50s
% Output : Proof 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM276_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.15/0.32 % Computer : n005.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Mon May 4 20:09:47 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.29/0.50 % SZS status Theorem
% 0.29/0.50 % SZS output start Proof
% 0.29/0.50 tff(vsomeExp_type, type, (
% 0.29/0.50 vsomeExp: vExp > vOptExp)).
% 0.29/0.50 tff(tptp_fun_Veres_229_type, type, (
% 0.29/0.50 tptp_fun_Veres_229: ( vAval * vAval * vBinOpT ) > vExp)).
% 0.29/0.50 tff(tptp_fun_Vbot_232_type, type, (
% 0.29/0.50 tptp_fun_Vbot_232: vBinOpT)).
% 0.29/0.50 tff(tptp_fun_VwildcardName00_101_type, type, (
% 0.29/0.50 tptp_fun_VwildcardName00_101: vExp > vAval)).
% 0.29/0.50 tff(ve1_type, type, (
% 0.29/0.50 ve1: vExp)).
% 0.29/0.50 tff(ve2_type, type, (
% 0.29/0.50 ve2: vExp)).
% 0.29/0.50 tff(vreduceExp_type, type, (
% 0.29/0.50 vreduceExp: ( vExp * vAnsMap ) > vOptExp)).
% 0.29/0.50 tff(tptp_fun_Vam_231_type, type, (
% 0.29/0.50 tptp_fun_Vam_231: vAnsMap)).
% 0.29/0.50 tff(vbinop_type, type, (
% 0.29/0.50 vbinop: ( vExp * vBinOpT * vExp ) > vExp)).
% 0.29/0.50 tff(vevalBinOp_type, type, (
% 0.29/0.50 vevalBinOp: ( vBinOpT * vAval * vAval ) > vOptExp)).
% 0.29/0.50 tff(vgetExpValue_type, type, (
% 0.29/0.50 vgetExpValue: vExp > vAval)).
% 0.29/0.50 tff(vconstant_type, type, (
% 0.29/0.50 vconstant: vAval > vExp)).
% 0.29/0.50 tff(vsomeAType_type, type, (
% 0.29/0.50 vsomeAType: vAType > vOptAType)).
% 0.29/0.50 tff(tptp_fun_VwildcardName0_66_type, type, (
% 0.29/0.50 tptp_fun_VwildcardName0_66: vOptAType > vAType)).
% 0.29/0.50 tff(tptp_fun_Vat_230_type, type, (
% 0.29/0.50 tptp_fun_Vat_230: vAType)).
% 0.29/0.50 tff(vecheck_type, type, (
% 0.29/0.50 vecheck: ( vATMap * vExp ) > vOptAType)).
% 0.29/0.50 tff(vtypeAM_type, type, (
% 0.29/0.50 vtypeAM: vAnsMap > vATMap)).
% 0.29/0.50 tff(visSomeAType_type, type, (
% 0.29/0.50 visSomeAType: vOptAType > $o)).
% 0.29/0.50 tff(vexpIsValue_type, type, (
% 0.29/0.50 vexpIsValue: vExp > $o)).
% 0.29/0.50 tff(1,plain,
% 0.29/0.50 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav) <=> ![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(2,plain,
% 0.29/0.50 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav) <=> ![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(3,axiom,(![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''getExpValue-0'')).
% 0.29/0.50 tff(4,plain,
% 0.29/0.50 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.29/0.50 tff(5,plain,(
% 0.29/0.50 ![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.29/0.50 inference(skolemize,[status(sab)],[4])).
% 0.29/0.50 tff(6,plain,
% 0.29/0.50 (![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.29/0.50 tff(7,plain,
% 0.29/0.50 ((~![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)) | (vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))) = tptp_fun_VwildcardName00_101(ve2))),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.50 tff(8,plain,
% 0.29/0.50 (vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))) = tptp_fun_VwildcardName00_101(ve2)),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[7, 6])).
% 0.29/0.50 tff(9,plain,
% 0.29/0.50 ((~![Vav: vAval] : (vgetExpValue(vconstant(Vav)) = Vav)) | (vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))) = tptp_fun_VwildcardName00_101(ve1))),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.50 tff(10,plain,
% 0.29/0.50 (vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))) = tptp_fun_VwildcardName00_101(ve1)),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[9, 6])).
% 0.29/0.50 tff(11,plain,
% 0.29/0.50 (vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))) = vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2))),
% 0.29/0.50 inference(monotonicity,[status(thm)],[10, 8])).
% 0.29/0.50 tff(12,plain,
% 0.29/0.50 (vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2)) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))),
% 0.29/0.50 inference(symmetry,[status(thm)],[11])).
% 0.29/0.50 tff(13,plain,
% 0.29/0.50 (^[VwildcardName0: vAType] : refl(visSomeAType(vsomeAType(VwildcardName0)) <=> visSomeAType(vsomeAType(VwildcardName0)))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(14,plain,
% 0.29/0.50 (![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0)) <=> ![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0))),
% 0.29/0.50 inference(quant_intro,[status(thm)],[13])).
% 0.29/0.50 tff(15,plain,
% 0.29/0.50 (![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0)) <=> ![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(16,axiom,(![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''isSomeAType-1'')).
% 0.29/0.50 tff(17,plain,
% 0.29/0.50 (![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.29/0.50 tff(18,plain,(
% 0.29/0.50 ![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0))),
% 0.29/0.50 inference(skolemize,[status(sab)],[17])).
% 0.29/0.50 tff(19,plain,
% 0.29/0.50 (![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[18, 14])).
% 0.29/0.50 tff(20,plain,
% 0.29/0.50 ((~![VwildcardName0: vAType] : visSomeAType(vsomeAType(VwildcardName0))) | visSomeAType(vsomeAType(Vat!230))),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.50 tff(21,plain,
% 0.29/0.50 (visSomeAType(vsomeAType(Vat!230))),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[20, 19])).
% 0.29/0.50 tff(22,plain,
% 0.29/0.50 (^[VOptAType0: vOptAType] : refl(((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0)))) <=> ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0)))))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(23,plain,
% 0.29/0.50 (![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0)))) <=> ![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0))))),
% 0.29/0.50 inference(quant_intro,[status(thm)],[22])).
% 0.29/0.50 tff(24,plain,
% 0.29/0.50 (![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0))) <=> ![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0)))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(25,plain,
% 0.29/0.50 (^[VOptAType0: vOptAType] : rewrite((visSomeAType(VOptAType0) => ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0))) <=> ((~visSomeAType(VOptAType0)) | ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0))))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(26,plain,
% 0.29/0.50 (![VOptAType0: vOptAType] : (visSomeAType(VOptAType0) => ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0))) <=> ![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0)))),
% 0.29/0.50 inference(quant_intro,[status(thm)],[25])).
% 0.29/0.50 tff(27,axiom,(![VOptAType0: vOptAType] : (visSomeAType(VOptAType0) => ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''isSomeAType-true-INV'')).
% 0.29/0.50 tff(28,plain,
% 0.29/0.50 (![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.29/0.50 tff(29,plain,
% 0.29/0.50 (![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | ?[VwildcardName0: vAType] : (VOptAType0 = vsomeAType(VwildcardName0)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[28, 24])).
% 0.29/0.50 tff(30,plain,(
% 0.29/0.50 ![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0))))),
% 0.29/0.50 inference(skolemize,[status(sab)],[29])).
% 0.29/0.50 tff(31,plain,
% 0.29/0.50 (![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0))))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[30, 23])).
% 0.29/0.50 tff(32,plain,
% 0.29/0.50 (((~![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0))))) | ((~visSomeAType(vsomeAType(Vat!230))) | (vsomeAType(Vat!230) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230)))))) <=> ((~![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0))))) | (~visSomeAType(vsomeAType(Vat!230))) | (vsomeAType(Vat!230) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230)))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(33,plain,
% 0.29/0.50 ((~![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0))))) | ((~visSomeAType(vsomeAType(Vat!230))) | (vsomeAType(Vat!230) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230)))))),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.50 tff(34,plain,
% 0.29/0.50 ((~![VOptAType0: vOptAType] : ((~visSomeAType(VOptAType0)) | (VOptAType0 = vsomeAType(tptp_fun_VwildcardName0_66(VOptAType0))))) | (~visSomeAType(vsomeAType(Vat!230))) | (vsomeAType(Vat!230) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230))))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[33, 32])).
% 0.29/0.50 tff(35,plain,
% 0.29/0.50 (vsomeAType(Vat!230) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230)))),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[34, 31, 21])).
% 0.29/0.50 tff(36,plain,
% 0.29/0.50 (((vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot!232, ve2))) & (vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!232, ve2)) = vsomeAType(Vat!230))) & ![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00)))) <=> (vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot!232, ve2))) & (vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!232, ve2)) = vsomeAType(Vat!230)) & ![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(37,plain,
% 0.29/0.50 ((~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((~(vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00)))) <=> (~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((~(vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(38,plain,
% 0.29/0.50 ((~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((((vexpIsValue(ve2) & vexpIsValue(ve1)) & (~vexpIsValue(vbinop(ve1, Vbot, ve2)))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat))) => ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00)))) <=> (~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((~(vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(39,axiom,(~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((((vexpIsValue(ve2) & vexpIsValue(ve1)) & (~vexpIsValue(vbinop(ve1, Vbot, ve2)))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat))) => ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''reduceExpProgress-binop-expIsValue-True-expIsValue-True'')).
% 0.29/0.50 tff(40,plain,
% 0.29/0.50 (~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((~(vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[39, 38])).
% 0.29/0.50 tff(41,plain,
% 0.29/0.50 (~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((~(vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[40, 37])).
% 0.29/0.50 tff(42,plain,
% 0.29/0.50 (~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((~(vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[41, 37])).
% 0.29/0.50 tff(43,plain,
% 0.29/0.50 (~![Vbot: vBinOpT, Vam: vAnsMap, Vat: vAType] : ((~(vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres00: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres00)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[42, 37])).
% 0.29/0.50 tff(44,plain,
% 0.29/0.50 (vexpIsValue(ve2) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot!232, ve2))) & (vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!232, ve2)) = vsomeAType(Vat!230)) & ![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[43, 36])).
% 0.29/0.50 tff(45,plain,
% 0.29/0.50 (vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!232, ve2)) = vsomeAType(Vat!230)),
% 0.29/0.50 inference(and_elim,[status(thm)],[44])).
% 0.29/0.50 tff(46,plain,
% 0.29/0.50 (vexpIsValue(ve2)),
% 0.29/0.50 inference(and_elim,[status(thm)],[44])).
% 0.29/0.50 tff(47,plain,
% 0.29/0.50 (^[Ve: vExp] : refl(((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))) <=> ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(48,plain,
% 0.29/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.29/0.50 inference(quant_intro,[status(thm)],[47])).
% 0.29/0.50 tff(49,plain,
% 0.29/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(50,plain,
% 0.29/0.50 (^[Ve: vExp] : rewrite((![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve))) <=> ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))))))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(51,plain,
% 0.29/0.50 (![Ve: vExp] : (![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.29/0.50 inference(quant_intro,[status(thm)],[50])).
% 0.29/0.50 tff(52,axiom,(![Ve: vExp] : (![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''expIsValue-1'')).
% 0.29/0.50 tff(53,plain,
% 0.29/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[52, 51])).
% 0.29/0.50 tff(54,plain,
% 0.29/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[53, 49])).
% 0.29/0.50 tff(55,plain,(
% 0.29/0.50 ![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.29/0.50 inference(skolemize,[status(sab)],[54])).
% 0.29/0.50 tff(56,plain,
% 0.29/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[55, 48])).
% 0.29/0.50 tff(57,plain,
% 0.29/0.50 (((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | ((~vexpIsValue(ve2)) | (ve2 = vconstant(tptp_fun_VwildcardName00_101(ve2))))) <=> ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | (~vexpIsValue(ve2)) | (ve2 = vconstant(tptp_fun_VwildcardName00_101(ve2))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(58,plain,
% 0.29/0.50 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | ((~vexpIsValue(ve2)) | (ve2 = vconstant(tptp_fun_VwildcardName00_101(ve2))))),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.50 tff(59,plain,
% 0.29/0.50 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | (~vexpIsValue(ve2)) | (ve2 = vconstant(tptp_fun_VwildcardName00_101(ve2)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.29/0.50 tff(60,plain,
% 0.29/0.50 (ve2 = vconstant(tptp_fun_VwildcardName00_101(ve2))),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[59, 56, 46])).
% 0.29/0.50 tff(61,plain,
% 0.29/0.50 (vconstant(tptp_fun_VwildcardName00_101(ve2)) = ve2),
% 0.29/0.50 inference(symmetry,[status(thm)],[60])).
% 0.29/0.50 tff(62,plain,
% 0.29/0.50 (vexpIsValue(ve1)),
% 0.29/0.50 inference(and_elim,[status(thm)],[44])).
% 0.29/0.50 tff(63,plain,
% 0.29/0.50 (((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | ((~vexpIsValue(ve1)) | (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1))))) <=> ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | (~vexpIsValue(ve1)) | (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(64,plain,
% 0.29/0.50 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | ((~vexpIsValue(ve1)) | (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1))))),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.50 tff(65,plain,
% 0.29/0.50 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | (~vexpIsValue(ve1)) | (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.29/0.50 tff(66,plain,
% 0.29/0.50 (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1))),
% 0.29/0.50 inference(unit_resolution,[status(thm)],[65, 56, 62])).
% 0.29/0.50 tff(67,plain,
% 0.29/0.50 (vconstant(tptp_fun_VwildcardName00_101(ve1)) = ve1),
% 0.29/0.50 inference(symmetry,[status(thm)],[66])).
% 0.29/0.50 tff(68,plain,
% 0.29/0.50 (vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))) = vbinop(ve1, Vbot!232, ve2)),
% 0.29/0.50 inference(monotonicity,[status(thm)],[67, 61])).
% 0.29/0.50 tff(69,plain,
% 0.29/0.50 (vecheck(vtypeAM(Vam!231), vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2)))) = vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!232, ve2))),
% 0.29/0.50 inference(monotonicity,[status(thm)],[68])).
% 0.29/0.50 tff(70,plain,
% 0.29/0.50 (vecheck(vtypeAM(Vam!231), vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2)))) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230)))),
% 0.29/0.50 inference(transitivity,[status(thm)],[69, 45, 35])).
% 0.29/0.50 tff(71,plain,
% 0.29/0.50 (^[Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : refl(((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot)))) <=> ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot)))))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(72,plain,
% 0.29/0.50 (![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot)))) <=> ![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot))))),
% 0.29/0.50 inference(quant_intro,[status(thm)],[71])).
% 0.29/0.50 tff(73,plain,
% 0.29/0.50 (![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres))) <=> ![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres)))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(74,plain,
% 0.29/0.50 (^[Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : rewrite(((vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat)) => ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres))) <=> ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres))))),
% 0.29/0.50 inference(bind,[status(th)],[])).
% 0.29/0.50 tff(75,plain,
% 0.29/0.50 (![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat)) => ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres))) <=> ![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres)))),
% 0.29/0.50 inference(quant_intro,[status(thm)],[74])).
% 0.29/0.50 tff(76,axiom,(![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat)) => ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOpProgress')).
% 0.29/0.50 tff(77,plain,
% 0.29/0.50 (![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.29/0.50 tff(78,plain,
% 0.29/0.50 (![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | ?[Veres: vExp] : (vevalBinOp(Vbot, Va, Va1) = vsomeExp(Veres)))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[77, 73])).
% 0.29/0.50 tff(79,plain,(
% 0.29/0.50 ![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot))))),
% 0.29/0.50 inference(skolemize,[status(sab)],[78])).
% 0.29/0.50 tff(80,plain,
% 0.29/0.50 (![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot))))),
% 0.29/0.50 inference(modus_ponens,[status(thm)],[79, 72])).
% 0.29/0.50 tff(81,plain,
% 0.29/0.50 (((~![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot))))) | ((~(vecheck(vtypeAM(Vam!231), vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2)))) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230))))) | (vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2)) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232))))) <=> ((~![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot))))) | (~(vecheck(vtypeAM(Vam!231), vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2)))) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230))))) | (vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2)) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232))))),
% 0.29/0.50 inference(rewrite,[status(thm)],[])).
% 0.29/0.50 tff(82,plain,
% 0.29/0.50 ((~![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot))))) | ((~(vecheck(vtypeAM(Vam!231), vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2)))) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230))))) | (vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2)) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232))))),
% 0.29/0.50 inference(quant_inst,[status(thm)],[])).
% 0.29/0.51 tff(83,plain,
% 0.29/0.51 ((~![Vbot: vBinOpT, Va: vAval, Vatm: vATMap, Va1: vAval, Vat: vAType] : ((~(vecheck(Vatm, vbinop(vconstant(Va), Vbot, vconstant(Va1))) = vsomeAType(Vat))) | (vevalBinOp(Vbot, Va, Va1) = vsomeExp(tptp_fun_Veres_229(Va1, Va, Vbot))))) | (~(vecheck(vtypeAM(Vam!231), vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2)))) = vsomeAType(tptp_fun_VwildcardName0_66(vsomeAType(Vat!230))))) | (vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2)) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[82, 81])).
% 0.29/0.51 tff(84,plain,
% 0.29/0.51 (vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2)) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232))),
% 0.29/0.51 inference(unit_resolution,[status(thm)],[83, 80, 70])).
% 0.29/0.51 tff(85,plain,
% 0.29/0.51 (vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232)) = vevalBinOp(Vbot!232, tptp_fun_VwildcardName00_101(ve1), tptp_fun_VwildcardName00_101(ve2))),
% 0.29/0.51 inference(symmetry,[status(thm)],[84])).
% 0.29/0.51 tff(86,plain,
% 0.29/0.51 (vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232)) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))),
% 0.29/0.51 inference(transitivity,[status(thm)],[85, 12])).
% 0.29/0.51 tff(87,plain,
% 0.29/0.51 (vbinop(ve1, Vbot!232, ve2) = vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2)))),
% 0.29/0.51 inference(symmetry,[status(thm)],[68])).
% 0.29/0.51 tff(88,plain,
% 0.29/0.51 (vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231)),
% 0.29/0.51 inference(monotonicity,[status(thm)],[87])).
% 0.29/0.51 tff(89,plain,
% 0.29/0.51 ((vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232))) <=> (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))))),
% 0.29/0.51 inference(monotonicity,[status(thm)],[88, 86])).
% 0.29/0.51 tff(90,plain,
% 0.29/0.51 ((vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))) <=> (vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232)))),
% 0.29/0.51 inference(symmetry,[status(thm)],[89])).
% 0.29/0.51 tff(91,plain,
% 0.29/0.51 (vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1))) <=> vexpIsValue(ve1)),
% 0.29/0.51 inference(monotonicity,[status(thm)],[67])).
% 0.29/0.51 tff(92,plain,
% 0.29/0.51 (vexpIsValue(ve1) <=> vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))),
% 0.29/0.51 inference(symmetry,[status(thm)],[91])).
% 0.29/0.51 tff(93,plain,
% 0.29/0.51 (vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[62, 92])).
% 0.29/0.51 tff(94,plain,
% 0.29/0.51 (vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2))) <=> vexpIsValue(ve2)),
% 0.29/0.51 inference(monotonicity,[status(thm)],[61])).
% 0.29/0.51 tff(95,plain,
% 0.29/0.51 (vexpIsValue(ve2) <=> vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))),
% 0.29/0.51 inference(symmetry,[status(thm)],[94])).
% 0.29/0.51 tff(96,plain,
% 0.29/0.51 (vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[46, 95])).
% 0.29/0.51 tff(97,plain,
% 0.29/0.51 (^[Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : refl(((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))) <=> ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))))),
% 0.29/0.51 inference(bind,[status(th)],[])).
% 0.29/0.51 tff(98,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))) <=> ![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))),
% 0.29/0.51 inference(quant_intro,[status(thm)],[97])).
% 0.29/0.51 tff(99,plain,
% 0.29/0.51 (^[Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : trans(monotonicity(trans(monotonicity(rewrite((vexpIsValue(Ve1) & vexpIsValue(Ve2)) <=> (~((~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))))), ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) <=> (~(~((~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))))))), rewrite((~(~((~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))))) <=> ((~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))), ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) <=> ((~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))))), (((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))) <=> (((~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))))), rewrite((((~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))) <=> ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))), (((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))) <=> ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))))),
% 0.29/0.51 inference(bind,[status(th)],[])).
% 0.29/0.51 tff(100,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))) <=> ![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))),
% 0.29/0.51 inference(quant_intro,[status(thm)],[99])).
% 0.29/0.51 tff(101,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))) <=> ![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))))),
% 0.29/0.51 inference(rewrite,[status(thm)],[])).
% 0.29/0.51 tff(102,plain,
% 0.29/0.51 (^[Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : rewrite(((vexpIsValue(Ve1) & vexpIsValue(Ve2)) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))) <=> ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))))),
% 0.29/0.51 inference(bind,[status(th)],[])).
% 0.29/0.51 tff(103,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vexpIsValue(Ve1) & vexpIsValue(Ve2)) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2)))) <=> ![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))))),
% 0.29/0.51 inference(quant_intro,[status(thm)],[102])).
% 0.29/0.51 tff(104,axiom,(![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vexpIsValue(Ve1) & vexpIsValue(Ve2)) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''reduceExp-3'')).
% 0.29/0.51 tff(105,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[104, 103])).
% 0.29/0.51 tff(106,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[105, 101])).
% 0.29/0.51 tff(107,plain,(
% 0.29/0.51 ![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((~(vexpIsValue(Ve1) & vexpIsValue(Ve2))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))))),
% 0.29/0.51 inference(skolemize,[status(sab)],[106])).
% 0.29/0.51 tff(108,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[107, 100])).
% 0.29/0.51 tff(109,plain,
% 0.29/0.51 (![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[108, 98])).
% 0.29/0.51 tff(110,plain,
% 0.29/0.51 (((~![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))) | ((vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))))) <=> ((~![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))) | (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))))),
% 0.29/0.51 inference(rewrite,[status(thm)],[])).
% 0.29/0.51 tff(111,plain,
% 0.29/0.51 ((~![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))) | ((vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))))),
% 0.29/0.51 inference(quant_inst,[status(thm)],[])).
% 0.29/0.51 tff(112,plain,
% 0.29/0.51 ((~![Ve1: vExp, Ve2: vExp, Vop: vBinOpT, Vam: vAnsMap] : ((vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vevalBinOp(Vop, vgetExpValue(Ve1), vgetExpValue(Ve2))) | (~vexpIsValue(Ve2)) | (~vexpIsValue(Ve1)))) | (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1))))),
% 0.29/0.51 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.29/0.53 tff(113,plain,
% 0.29/0.53 ((vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve2)))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1))))),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[112, 109])).
% 0.29/0.53 tff(114,plain,
% 0.29/0.53 (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!232, vconstant(tptp_fun_VwildcardName00_101(ve2))), Vam!231) = vevalBinOp(Vbot!232, vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve1))), vgetExpValue(vconstant(tptp_fun_VwildcardName00_101(ve2))))),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[113, 96, 93])).
% 0.29/0.53 tff(115,plain,
% 0.29/0.53 (vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232))),
% 0.29/0.53 inference(modus_ponens,[status(thm)],[114, 90])).
% 0.29/0.53 tff(116,plain,
% 0.29/0.53 (^[Veres00: vExp] : refl((~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00))) <=> (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00))))),
% 0.29/0.53 inference(bind,[status(th)],[])).
% 0.29/0.53 tff(117,plain,
% 0.29/0.53 (![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00))) <=> ![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00)))),
% 0.29/0.53 inference(quant_intro,[status(thm)],[116])).
% 0.29/0.53 tff(118,plain,
% 0.29/0.53 (![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00)))),
% 0.29/0.53 inference(and_elim,[status(thm)],[44])).
% 0.29/0.53 tff(119,plain,
% 0.29/0.53 (![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00)))),
% 0.29/0.53 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.29/0.53 tff(120,plain,
% 0.29/0.53 ((~![Veres00: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(Veres00)))) | (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232))))),
% 0.29/0.53 inference(quant_inst,[status(thm)],[])).
% 0.29/0.53 tff(121,plain,
% 0.29/0.53 (~(vreduceExp(vbinop(ve1, Vbot!232, ve2), Vam!231) = vsomeExp(tptp_fun_Veres_229(tptp_fun_VwildcardName00_101(ve2), tptp_fun_VwildcardName00_101(ve1), Vbot!232)))),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[120, 119])).
% 0.29/0.53 tff(122,plain,
% 0.29/0.53 ($false),
% 0.29/0.53 inference(unit_resolution,[status(thm)],[121, 115])).
% 0.29/0.53 % SZS output end Proof
% 0.29/0.53 % E exiting
%------------------------------------------------------------------------------