%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM275_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.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.30s 0.50s
% Output : Proof 0.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM275_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.16/0.33 % Computer : n010.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 20:09:07 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.30/0.50 % SZS status Theorem
% 0.30/0.50 % SZS output start Proof
% 0.30/0.50 tff(vsomeExp_type, type, (
% 0.30/0.50 vsomeExp: vExp > vOptExp)).
% 0.30/0.50 tff(vbinop_type, type, (
% 0.30/0.50 vbinop: ( vExp * vBinOpT * vExp ) > vExp)).
% 0.30/0.50 tff(vgetExp_type, type, (
% 0.30/0.50 vgetExp: vOptExp > vExp)).
% 0.30/0.50 tff(vreduceExp_type, type, (
% 0.30/0.50 vreduceExp: ( vExp * vAnsMap ) > vOptExp)).
% 0.30/0.50 tff(tptp_fun_Vam_231_type, type, (
% 0.30/0.50 tptp_fun_Vam_231: vAnsMap)).
% 0.30/0.50 tff(ve2_type, type, (
% 0.30/0.50 ve2: vExp)).
% 0.30/0.50 tff(tptp_fun_Vbot_230_type, type, (
% 0.30/0.50 tptp_fun_Vbot_230: vBinOpT)).
% 0.30/0.50 tff(vconstant_type, type, (
% 0.30/0.50 vconstant: vAval > vExp)).
% 0.30/0.50 tff(tptp_fun_VwildcardName00_101_type, type, (
% 0.30/0.50 tptp_fun_VwildcardName00_101: vExp > vAval)).
% 0.30/0.50 tff(ve1_type, type, (
% 0.30/0.50 ve1: vExp)).
% 0.30/0.50 tff(vexpIsValue_type, type, (
% 0.30/0.50 vexpIsValue: vExp > $o)).
% 0.30/0.50 tff(vsomeAType_type, type, (
% 0.30/0.50 vsomeAType: vAType > vOptAType)).
% 0.30/0.50 tff(tptp_fun_Vat_229_type, type, (
% 0.30/0.50 tptp_fun_Vat_229: vAType)).
% 0.30/0.50 tff(vecheck_type, type, (
% 0.30/0.50 vecheck: ( vATMap * vExp ) > vOptAType)).
% 0.30/0.50 tff(vtypeAM_type, type, (
% 0.30/0.50 vtypeAM: vAnsMap > vATMap)).
% 0.30/0.50 tff(visSomeExp_type, type, (
% 0.30/0.50 visSomeExp: vOptExp > $o)).
% 0.30/0.50 tff(1,plain,
% 0.30/0.50 (((visSomeExp(vreduceExp(ve2, Vam!231)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot!230, ve2))) & (vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!230, ve2)) = vsomeAType(Vat!229))) & ![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000)))) <=> (visSomeExp(vreduceExp(ve2, Vam!231)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot!230, ve2))) & (vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!230, ve2)) = vsomeAType(Vat!229)) & ![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000))))),
% 0.30/0.50 inference(rewrite,[status(thm)],[])).
% 0.30/0.50 tff(2,plain,
% 0.30/0.50 ((~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : ((~(visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000)))) <=> (~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : ((~(visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000))))),
% 0.30/0.50 inference(rewrite,[status(thm)],[])).
% 0.30/0.50 tff(3,plain,
% 0.30/0.50 ((~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : (((((visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2))) & vexpIsValue(ve1)) & (~vexpIsValue(vbinop(ve1, Vbot, ve2)))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat))) => ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000)))) <=> (~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : ((~(visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000))))),
% 0.30/0.50 inference(rewrite,[status(thm)],[])).
% 0.30/0.50 tff(4,axiom,(~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : (((((visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2))) & vexpIsValue(ve1)) & (~vexpIsValue(vbinop(ve1, Vbot, ve2)))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat))) => ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''reduceExpProgress-binop-expIsValue-True-expIsValue-False-isSomeExp-True'')).
% 0.30/0.50 tff(5,plain,
% 0.30/0.50 (~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : ((~(visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000)))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.30/0.50 tff(6,plain,
% 0.30/0.50 (~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : ((~(visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000)))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[5, 2])).
% 0.30/0.50 tff(7,plain,
% 0.30/0.50 (~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : ((~(visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000)))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.30/0.50 tff(8,plain,
% 0.30/0.50 (~![Vam: vAnsMap, Vbot: vBinOpT, Vat: vAType] : ((~(visSomeExp(vreduceExp(ve2, Vam)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot, ve2))) & (vecheck(vtypeAM(Vam), vbinop(ve1, Vbot, ve2)) = vsomeAType(Vat)))) | ?[Veres000: vExp] : (vreduceExp(vbinop(ve1, Vbot, ve2), Vam) = vsomeExp(Veres000)))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[7, 2])).
% 0.30/0.50 tff(9,plain,
% 0.30/0.50 (visSomeExp(vreduceExp(ve2, Vam!231)) & (~vexpIsValue(ve2)) & vexpIsValue(ve1) & (~vexpIsValue(vbinop(ve1, Vbot!230, ve2))) & (vecheck(vtypeAM(Vam!231), vbinop(ve1, Vbot!230, ve2)) = vsomeAType(Vat!229)) & ![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000)))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[8, 1])).
% 0.30/0.50 tff(10,plain,
% 0.30/0.50 (vexpIsValue(ve1)),
% 0.30/0.50 inference(and_elim,[status(thm)],[9])).
% 0.30/0.50 tff(11,plain,
% 0.30/0.50 (^[Ve: vExp] : refl(((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))) <=> ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve)))))),
% 0.30/0.50 inference(bind,[status(th)],[])).
% 0.30/0.50 tff(12,plain,
% 0.30/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.30/0.50 inference(quant_intro,[status(thm)],[11])).
% 0.30/0.50 tff(13,plain,
% 0.30/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.30/0.50 inference(rewrite,[status(thm)],[])).
% 0.30/0.50 tff(14,plain,
% 0.30/0.50 (^[Ve: vExp] : rewrite((![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve))) <=> ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))))))),
% 0.30/0.50 inference(bind,[status(th)],[])).
% 0.30/0.50 tff(15,plain,
% 0.30/0.50 (![Ve: vExp] : (![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve))) <=> ![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.30/0.50 inference(quant_intro,[status(thm)],[14])).
% 0.30/0.50 tff(16,axiom,(![Ve: vExp] : (![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00))) => (~vexpIsValue(Ve)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''expIsValue-1'')).
% 0.30/0.50 tff(17,plain,
% 0.30/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.30/0.50 tff(18,plain,
% 0.30/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (~![VwildcardName00: vAval] : (~(Ve = vconstant(VwildcardName00)))))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.30/0.50 tff(19,plain,(
% 0.30/0.50 ![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.30/0.50 inference(skolemize,[status(sab)],[18])).
% 0.30/0.50 tff(20,plain,
% 0.30/0.50 (![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))),
% 0.30/0.50 inference(modus_ponens,[status(thm)],[19, 12])).
% 0.30/0.50 tff(21,plain,
% 0.30/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.30/0.51 inference(rewrite,[status(thm)],[])).
% 0.30/0.51 tff(22,plain,
% 0.30/0.51 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | ((~vexpIsValue(ve1)) | (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1))))),
% 0.30/0.51 inference(quant_inst,[status(thm)],[])).
% 0.30/0.51 tff(23,plain,
% 0.30/0.51 ((~![Ve: vExp] : ((~vexpIsValue(Ve)) | (Ve = vconstant(tptp_fun_VwildcardName00_101(Ve))))) | (~vexpIsValue(ve1)) | (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1)))),
% 0.30/0.51 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.30/0.51 tff(24,plain,
% 0.30/0.51 (ve1 = vconstant(tptp_fun_VwildcardName00_101(ve1))),
% 0.30/0.51 inference(unit_resolution,[status(thm)],[23, 20, 10])).
% 0.30/0.51 tff(25,plain,
% 0.30/0.51 (vconstant(tptp_fun_VwildcardName00_101(ve1)) = ve1),
% 0.30/0.51 inference(symmetry,[status(thm)],[24])).
% 0.30/0.51 tff(26,plain,
% 0.30/0.51 (vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1))) <=> vexpIsValue(ve1)),
% 0.30/0.51 inference(monotonicity,[status(thm)],[25])).
% 0.30/0.51 tff(27,plain,
% 0.30/0.51 (vexpIsValue(ve1) <=> vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))),
% 0.30/0.51 inference(symmetry,[status(thm)],[26])).
% 0.30/0.51 tff(28,plain,
% 0.30/0.51 (vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))),
% 0.30/0.51 inference(modus_ponens,[status(thm)],[10, 27])).
% 0.30/0.51 tff(29,plain,
% 0.30/0.51 (~vexpIsValue(ve2)),
% 0.30/0.51 inference(and_elim,[status(thm)],[9])).
% 0.30/0.51 tff(30,plain,
% 0.30/0.51 (visSomeExp(vreduceExp(ve2, Vam!231))),
% 0.30/0.51 inference(and_elim,[status(thm)],[9])).
% 0.30/0.51 tff(31,plain,
% 0.30/0.51 (^[Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : refl((vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1))) <=> (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1))))),
% 0.30/0.51 inference(bind,[status(th)],[])).
% 0.30/0.51 tff(32,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1))) <=> ![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))),
% 0.30/0.51 inference(quant_intro,[status(thm)],[31])).
% 0.30/0.51 tff(33,plain,
% 0.30/0.51 (^[Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : trans(monotonicity(trans(monotonicity(rewrite((vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam))) <=> (~(vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (~vexpIsValue(Ve1))))), ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) <=> (~(~(vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (~vexpIsValue(Ve1))))))), rewrite((~(~(vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (~vexpIsValue(Ve1))))) <=> (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (~vexpIsValue(Ve1)))), ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) <=> (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (~vexpIsValue(Ve1))))), (((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> ((vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (~vexpIsValue(Ve1))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))))), rewrite(((vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (~vexpIsValue(Ve1))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))), (((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))))),
% 0.30/0.51 inference(bind,[status(th)],[])).
% 0.30/0.51 tff(34,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> ![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))),
% 0.30/0.51 inference(quant_intro,[status(thm)],[33])).
% 0.30/0.51 tff(35,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> ![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))),
% 0.30/0.51 inference(rewrite,[status(thm)],[])).
% 0.30/0.51 tff(36,plain,
% 0.30/0.51 (^[Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : trans(monotonicity(rewrite(((vexpIsValue(Ve1) & (~vexpIsValue(Ve2))) & visSomeExp(vreduceExp(Ve2, Vam))) <=> (vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))), ((((vexpIsValue(Ve1) & (~vexpIsValue(Ve2))) & visSomeExp(vreduceExp(Ve2, Vam))) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> ((vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam))) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))))), rewrite(((vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam))) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))), ((((vexpIsValue(Ve1) & (~vexpIsValue(Ve2))) & visSomeExp(vreduceExp(Ve2, Vam))) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))))),
% 0.30/0.51 inference(bind,[status(th)],[])).
% 0.30/0.51 tff(37,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (((vexpIsValue(Ve1) & (~vexpIsValue(Ve2))) & visSomeExp(vreduceExp(Ve2, Vam))) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam)))))) <=> ![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))),
% 0.30/0.51 inference(quant_intro,[status(thm)],[36])).
% 0.30/0.51 tff(38,axiom,(![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (((vexpIsValue(Ve1) & (~vexpIsValue(Ve2))) & visSomeExp(vreduceExp(Ve2, Vam))) => (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''reduceExp-4'')).
% 0.30/0.51 tff(39,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))),
% 0.30/0.51 inference(modus_ponens,[status(thm)],[38, 37])).
% 0.30/0.51 tff(40,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))),
% 0.30/0.51 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.30/0.51 tff(41,plain,(
% 0.30/0.51 ![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : ((~(vexpIsValue(Ve1) & (~vexpIsValue(Ve2)) & visSomeExp(vreduceExp(Ve2, Vam)))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))))),
% 0.30/0.51 inference(skolemize,[status(sab)],[40])).
% 0.30/0.51 tff(42,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))),
% 0.30/0.51 inference(modus_ponens,[status(thm)],[41, 34])).
% 0.30/0.51 tff(43,plain,
% 0.30/0.51 (![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))),
% 0.30/0.51 inference(modus_ponens,[status(thm)],[42, 32])).
% 0.30/0.51 tff(44,plain,
% 0.30/0.51 (((~![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))) | (vexpIsValue(ve2) | (~visSomeExp(vreduceExp(ve2, Vam!231))) | (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))))) <=> ((~![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))) | vexpIsValue(ve2) | (~visSomeExp(vreduceExp(ve2, Vam!231))) | (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))))),
% 0.30/0.51 inference(rewrite,[status(thm)],[])).
% 0.30/0.51 tff(45,plain,
% 0.30/0.51 ((~![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))) | (vexpIsValue(ve2) | (~visSomeExp(vreduceExp(ve2, Vam!231))) | (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1)))))),
% 0.30/0.51 inference(quant_inst,[status(thm)],[])).
% 0.30/0.51 tff(46,plain,
% 0.30/0.51 ((~![Ve1: vExp, Ve2: vExp, Vam: vAnsMap, Vop: vBinOpT] : (vexpIsValue(Ve2) | (~visSomeExp(vreduceExp(Ve2, Vam))) | (vreduceExp(vbinop(Ve1, Vop, Ve2), Vam) = vsomeExp(vbinop(Ve1, Vop, vgetExp(vreduceExp(Ve2, Vam))))) | (~vexpIsValue(Ve1)))) | vexpIsValue(ve2) | (~visSomeExp(vreduceExp(ve2, Vam!231))) | (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1))))),
% 0.30/0.51 inference(modus_ponens,[status(thm)],[45, 44])).
% 0.30/0.51 tff(47,plain,
% 0.30/0.51 ((vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))) | (~vexpIsValue(vconstant(tptp_fun_VwildcardName00_101(ve1))))),
% 0.30/0.51 inference(unit_resolution,[status(thm)],[46, 43, 30, 29])).
% 0.30/0.51 tff(48,plain,
% 0.30/0.51 (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))),
% 0.30/0.53 inference(unit_resolution,[status(thm)],[47, 28])).
% 0.30/0.53 tff(49,plain,
% 0.30/0.53 (vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2) = vbinop(ve1, Vbot!230, ve2)),
% 0.30/0.53 inference(monotonicity,[status(thm)],[25])).
% 0.30/0.53 tff(50,plain,
% 0.30/0.53 (vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231) = vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231)),
% 0.30/0.53 inference(monotonicity,[status(thm)],[49])).
% 0.30/0.53 tff(51,plain,
% 0.30/0.53 (vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vreduceExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, ve2), Vam!231)),
% 0.30/0.53 inference(symmetry,[status(thm)],[50])).
% 0.30/0.53 tff(52,plain,
% 0.30/0.53 (vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))),
% 0.30/0.53 inference(transitivity,[status(thm)],[51, 48])).
% 0.30/0.53 tff(53,plain,
% 0.30/0.53 (^[Veres000: vExp] : refl((~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000))) <=> (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000))))),
% 0.30/0.53 inference(bind,[status(th)],[])).
% 0.30/0.53 tff(54,plain,
% 0.30/0.53 (![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000))) <=> ![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000)))),
% 0.30/0.53 inference(quant_intro,[status(thm)],[53])).
% 0.30/0.53 tff(55,plain,
% 0.30/0.53 (![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000)))),
% 0.30/0.53 inference(and_elim,[status(thm)],[9])).
% 0.30/0.53 tff(56,plain,
% 0.30/0.53 (![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000)))),
% 0.30/0.53 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.30/0.53 tff(57,plain,
% 0.30/0.53 ((~![Veres000: vExp] : (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(Veres000)))) | (~(vreduceExp(vbinop(ve1, Vbot!230, ve2), Vam!231) = vsomeExp(vbinop(vconstant(tptp_fun_VwildcardName00_101(ve1)), Vbot!230, vgetExp(vreduceExp(ve2, Vam!231))))))),
% 0.30/0.53 inference(quant_inst,[status(thm)],[])).
% 0.30/0.53 tff(58,plain,
% 0.30/0.53 ($false),
% 0.30/0.53 inference(unit_resolution,[status(thm)],[57, 56, 52])).
% 0.30/0.53 % SZS output end Proof
% 0.30/0.53 % E exiting
%------------------------------------------------------------------------------