%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM254_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n024.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.15s 0.35s
% Output : Proof 0.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : COM254_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.06 % Command : run_E %s %d THM
% 0.06/0.24 % Computer : n024.cluster.edu
% 0.06/0.24 % Model : x86_64 x86_64
% 0.06/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.24 % Memory : 8042.1875MB
% 0.06/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.24 % CPULimit : 300
% 0.06/0.24 % WCLimit : 300
% 0.06/0.24 % DateTime : Mon May 4 14:45:58 EDT 2026
% 0.06/0.24 % CPUTime :
% 0.15/0.35 % SZS status Theorem
% 0.15/0.35 % SZS output start Proof
% 0.15/0.35 tff(vptcheck_type, type, (
% 0.15/0.35 vptcheck: ( vMapConf * vQuestionnaire * vMapConf ) > $o)).
% 0.15/0.35 tff(vMC_type, type, (
% 0.15/0.35 vMC: ( vATMap * vATMap ) > vMapConf)).
% 0.15/0.35 tff(tptp_fun_Vqtm1_233_type, type, (
% 0.15/0.35 tptp_fun_Vqtm1_233: vATMap)).
% 0.15/0.35 tff(tptp_fun_Vatm1_229_type, type, (
% 0.15/0.35 tptp_fun_Vatm1_229: vATMap)).
% 0.15/0.35 tff(tptp_fun_Vqr_232_type, type, (
% 0.15/0.35 tptp_fun_Vqr_232: vQuestionnaire)).
% 0.15/0.35 tff(vtypeQM_type, type, (
% 0.15/0.35 vtypeQM: vQMap > vATMap)).
% 0.15/0.35 tff(tptp_fun_Vqmr_227_type, type, (
% 0.15/0.35 tptp_fun_Vqmr_227: vQMap)).
% 0.15/0.35 tff(vtypeAM_type, type, (
% 0.15/0.35 vtypeAM: vAnsMap > vATMap)).
% 0.15/0.35 tff(tptp_fun_Vamr_230_type, type, (
% 0.15/0.35 tptp_fun_Vamr_230: vAnsMap)).
% 0.15/0.35 tff(tptp_fun_Vqm1_225_type, type, (
% 0.15/0.35 tptp_fun_Vqm1_225: ( vQuestionnaire * vATMap * vATMap ) > vATMap)).
% 0.15/0.35 tff(tptp_fun_Vqm_231_type, type, (
% 0.15/0.35 tptp_fun_Vqm_231: vQMap)).
% 0.15/0.35 tff(tptp_fun_Vam_228_type, type, (
% 0.15/0.35 tptp_fun_Vam_228: vAnsMap)).
% 0.15/0.35 tff(vq2_type, type, (
% 0.15/0.35 vq2: vQuestionnaire)).
% 0.15/0.35 tff(tptp_fun_Vatm1_226_type, type, (
% 0.15/0.35 tptp_fun_Vatm1_226: ( vQuestionnaire * vATMap * vATMap ) > vATMap)).
% 0.15/0.35 tff(tptp_fun_Vqm1_223_type, type, (
% 0.15/0.35 tptp_fun_Vqm1_223: ( vATMap * vQuestionnaire * vATMap ) > vATMap)).
% 0.15/0.35 tff(vq1_type, type, (
% 0.15/0.35 vq1: vQuestionnaire)).
% 0.15/0.35 tff(tptp_fun_Vatm1_224_type, type, (
% 0.15/0.35 tptp_fun_Vatm1_224: ( vATMap * vQuestionnaire * vATMap ) > vATMap)).
% 0.15/0.35 tff(vqcond_type, type, (
% 0.15/0.35 vqcond: ( vExp * vQuestionnaire * vQuestionnaire ) > vQuestionnaire)).
% 0.15/0.35 tff(vconstant_type, type, (
% 0.15/0.35 vconstant: vAval > vExp)).
% 0.15/0.35 tff(vB_type, type, (
% 0.15/0.35 vB: vYN > vAval)).
% 0.15/0.35 tff(vno_type, type, (
% 0.15/0.35 vno: vYN)).
% 0.15/0.35 tff(vsomeQConf_type, type, (
% 0.15/0.35 vsomeQConf: vQConf > vOptQConf)).
% 0.15/0.35 tff(vQC_type, type, (
% 0.15/0.35 vQC: ( vAnsMap * vQMap * vQuestionnaire ) > vQConf)).
% 0.15/0.35 tff(vreduce_type, type, (
% 0.15/0.35 vreduce: ( vQuestionnaire * vAnsMap * vQMap ) > vOptQConf)).
% 0.15/0.35 tff(vgetQuest_type, type, (
% 0.15/0.35 vgetQuest: vQConf > vQuestionnaire)).
% 0.15/0.35 tff(vgetQC_type, type, (
% 0.15/0.35 vgetQC: vOptQConf > vQConf)).
% 0.15/0.35 tff(vgetQM_type, type, (
% 0.15/0.35 vgetQM: vQConf > vQMap)).
% 0.15/0.35 tff(vgetAM_type, type, (
% 0.15/0.35 vgetAM: vQConf > vAnsMap)).
% 0.15/0.35 tff(1,plain,
% 0.15/0.35 ((~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~(vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))) <=> (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~(vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1))))),
% 0.15/0.35 inference(rewrite,[status(thm)],[])).
% 0.15/0.35 tff(2,plain,
% 0.15/0.35 ((~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr)))) => vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))) <=> (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~(vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1))))),
% 0.15/0.35 inference(rewrite,[status(thm)],[])).
% 0.15/0.35 tff(3,axiom,(~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), 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-qcond-constant-B-no'')).
% 0.15/0.36 tff(4,plain,
% 0.15/0.36 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~(vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.15/0.36 tff(5,plain,
% 0.15/0.36 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~(vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[4, 1])).
% 0.15/0.36 tff(6,plain,
% 0.15/0.36 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~(vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.15/0.36 tff(7,plain,
% 0.15/0.36 (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~(vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[6, 1])).
% 0.15/0.36 tff(8,plain,(
% 0.15/0.36 ~((~(vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))))) | vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233)))),
% 0.15/0.36 inference(skolemize,[status(sab)],[7])).
% 0.15/0.36 tff(9,plain,
% 0.15/0.36 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233)) & (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232)))),
% 0.15/0.36 inference(or_elim,[status(thm)],[8])).
% 0.15/0.36 tff(10,plain,
% 0.15/0.36 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.15/0.36 inference(and_elim,[status(thm)],[9])).
% 0.15/0.36 tff(11,plain,
% 0.15/0.36 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : refl(((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm)))))),
% 0.15/0.36 inference(bind,[status(th)],[])).
% 0.15/0.36 tff(12,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm)))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm))))),
% 0.15/0.36 inference(quant_intro,[status(thm)],[11])).
% 0.15/0.36 tff(13,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(rewrite,[status(thm)],[])).
% 0.15/0.36 tff(14,plain,
% 0.15/0.36 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : rewrite((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) => ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))),
% 0.15/0.36 inference(bind,[status(th)],[])).
% 0.15/0.36 tff(15,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) => ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(quant_intro,[status(thm)],[14])).
% 0.15/0.36 tff(16,axiom,(![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) => ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqcond_inv2'')).
% 0.15/0.36 tff(17,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.15/0.36 tff(18,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.15/0.36 tff(19,plain,(
% 0.15/0.36 ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm))))),
% 0.15/0.36 inference(skolemize,[status(sab)],[18])).
% 0.15/0.36 tff(20,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm))))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[19, 12])).
% 0.15/0.36 tff(21,plain,
% 0.15/0.36 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))),
% 0.15/0.36 inference(rewrite,[status(thm)],[])).
% 0.15/0.36 tff(22,plain,
% 0.15/0.36 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))),
% 0.15/0.36 inference(quant_inst,[status(thm)],[])).
% 0.15/0.36 tff(23,plain,
% 0.15/0.36 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq1, vMC(tptp_fun_Vatm1_224(Vatm, Vq1, Vqm), tptp_fun_Vqm1_223(Vatm, Vq1, Vqm))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.15/0.36 tff(24,plain,
% 0.15/0.36 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))),
% 0.15/0.36 inference(unit_resolution,[status(thm)],[23, 20, 10])).
% 0.15/0.36 tff(25,plain,
% 0.15/0.36 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : refl(((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm)))))),
% 0.15/0.36 inference(bind,[status(th)],[])).
% 0.15/0.36 tff(26,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm)))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm))))),
% 0.15/0.36 inference(quant_intro,[status(thm)],[25])).
% 0.15/0.36 tff(27,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(rewrite,[status(thm)],[])).
% 0.15/0.36 tff(28,plain,
% 0.15/0.36 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : rewrite((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) => ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.36 inference(bind,[status(th)],[])).
% 0.15/0.36 tff(29,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) => ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(quant_intro,[status(thm)],[28])).
% 0.15/0.36 tff(30,axiom,(![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) => ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqcond_inv3'')).
% 0.15/0.36 tff(31,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.15/0.36 tff(32,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | ?[Vatm1: vATMap, Vqm1: vATMap] : vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[31, 27])).
% 0.15/0.36 tff(33,plain,(
% 0.15/0.36 ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm))))),
% 0.15/0.36 inference(skolemize,[status(sab)],[32])).
% 0.15/0.36 tff(34,plain,
% 0.15/0.36 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm))))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[33, 26])).
% 0.15/0.36 tff(35,plain,
% 0.15/0.36 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.15/0.36 inference(rewrite,[status(thm)],[])).
% 0.15/0.36 tff(36,plain,
% 0.15/0.36 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.15/0.36 inference(quant_inst,[status(thm)],[])).
% 0.15/0.36 tff(37,plain,
% 0.15/0.36 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vatmr: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | vptcheck(vMC(Vatm, Vqm), Vq2, vMC(tptp_fun_Vatm1_226(Vq2, Vatm, Vqm), tptp_fun_Vqm1_225(Vq2, Vatm, Vqm))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[36, 35])).
% 0.15/0.36 tff(38,plain,
% 0.15/0.36 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.36 inference(unit_resolution,[status(thm)],[37, 34, 10])).
% 0.15/0.36 tff(39,plain,
% 0.15/0.36 (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : refl(((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))),
% 0.15/0.36 inference(bind,[status(th)],[])).
% 0.15/0.36 tff(40,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.36 inference(quant_intro,[status(thm)],[39])).
% 0.15/0.36 tff(41,plain,
% 0.15/0.36 (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(trans(monotonicity(rewrite((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) <=> (~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> (~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))))), rewrite((~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2)) <=> (((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2)))), rewrite((((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2)) <=> ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2)) <=> ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))))),
% 0.15/0.36 inference(bind,[status(th)],[])).
% 0.15/0.36 tff(42,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.36 inference(quant_intro,[status(thm)],[41])).
% 0.15/0.36 tff(43,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2))),
% 0.15/0.36 inference(rewrite,[status(thm)],[])).
% 0.15/0.36 tff(44,plain,
% 0.15/0.36 (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) <=> (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vqm1 = Vqm2)) <=> ((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vqm1 = Vqm2)))), rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vqm1 = Vqm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vqm1 = Vqm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2))))),
% 0.15/0.36 inference(bind,[status(th)],[])).
% 0.15/0.36 tff(45,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vqm1 = Vqm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2))),
% 0.15/0.36 inference(quant_intro,[status(thm)],[44])).
% 0.15/0.36 tff(46,axiom,(![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vqm1 = Vqm2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqcond_inv5'')).
% 0.15/0.36 tff(47,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.15/0.36 tff(48,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[47, 43])).
% 0.15/0.36 tff(49,plain,(
% 0.15/0.36 ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vqm1 = Vqm2))),
% 0.15/0.36 inference(skolemize,[status(sab)],[48])).
% 0.15/0.36 tff(50,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[49, 42])).
% 0.15/0.36 tff(51,plain,
% 0.15/0.36 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.36 inference(modus_ponens,[status(thm)],[50, 40])).
% 0.15/0.36 tff(52,plain,
% 0.15/0.36 (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.15/0.36 inference(rewrite,[status(thm)],[])).
% 0.15/0.36 tff(53,plain,
% 0.15/0.36 (((tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.15/0.36 inference(rewrite,[status(thm)],[])).
% 0.15/0.36 tff(54,plain,
% 0.15/0.36 (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))))),
% 0.15/0.37 inference(monotonicity,[status(thm)],[53])).
% 0.15/0.37 tff(55,plain,
% 0.15/0.37 (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.15/0.37 inference(transitivity,[status(thm)],[54, 52])).
% 0.15/0.37 tff(56,plain,
% 0.15/0.37 ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.15/0.37 inference(quant_inst,[status(thm)],[])).
% 0.15/0.37 tff(57,plain,
% 0.15/0.37 ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqm1 = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.15/0.37 inference(modus_ponens,[status(thm)],[56, 55])).
% 0.15/0.37 tff(58,plain,
% 0.15/0.37 (tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))),
% 0.15/0.37 inference(unit_resolution,[status(thm)],[57, 51, 10, 38, 24])).
% 0.15/0.37 tff(59,plain,
% 0.15/0.37 (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : refl(((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))),
% 0.15/0.37 inference(bind,[status(th)],[])).
% 0.15/0.37 tff(60,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.37 inference(quant_intro,[status(thm)],[59])).
% 0.15/0.37 tff(61,plain,
% 0.15/0.37 (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(trans(monotonicity(rewrite((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) <=> (~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> (~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))))), rewrite((~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2)) <=> (((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2)))), rewrite((((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2)) <=> ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2)) <=> ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))))),
% 0.15/0.37 inference(bind,[status(th)],[])).
% 0.15/0.37 tff(62,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.37 inference(quant_intro,[status(thm)],[61])).
% 0.15/0.37 tff(63,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2))),
% 0.15/0.37 inference(rewrite,[status(thm)],[])).
% 0.15/0.37 tff(64,plain,
% 0.15/0.37 (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) <=> (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vatm1 = Vatm2)) <=> ((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vatm1 = Vatm2)))), rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vatm1 = Vatm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vatm1 = Vatm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2))))),
% 0.15/0.37 inference(bind,[status(th)],[])).
% 0.15/0.37 tff(65,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vatm1 = Vatm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2))),
% 0.15/0.37 inference(quant_intro,[status(thm)],[64])).
% 0.15/0.37 tff(66,axiom,(![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))) => (Vatm1 = Vatm2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqcond_inv4'')).
% 0.15/0.37 tff(67,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2))),
% 0.15/0.37 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.15/0.37 tff(68,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2))),
% 0.15/0.37 inference(modus_ponens,[status(thm)],[67, 63])).
% 0.15/0.37 tff(69,plain,(
% 0.15/0.37 ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2)))) | (Vatm1 = Vatm2))),
% 0.15/0.37 inference(skolemize,[status(sab)],[68])).
% 0.15/0.37 tff(70,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.37 inference(modus_ponens,[status(thm)],[69, 62])).
% 0.15/0.37 tff(71,plain,
% 0.15/0.37 (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))),
% 0.15/0.37 inference(modus_ponens,[status(thm)],[70, 60])).
% 0.15/0.37 tff(72,plain,
% 0.15/0.37 (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) <=> ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.37 inference(rewrite,[status(thm)],[])).
% 0.15/0.37 tff(73,plain,
% 0.15/0.37 (((tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.37 inference(rewrite,[status(thm)],[])).
% 0.15/0.37 tff(74,plain,
% 0.15/0.37 (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.15/0.37 inference(monotonicity,[status(thm)],[73])).
% 0.15/0.37 tff(75,plain,
% 0.15/0.37 (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.37 inference(transitivity,[status(thm)],[74, 72])).
% 0.15/0.37 tff(76,plain,
% 0.15/0.37 ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | ((tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.15/0.37 inference(quant_inst,[status(thm)],[])).
% 0.15/0.37 tff(77,plain,
% 0.15/0.37 ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatm1 = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.15/0.37 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.15/0.37 tff(78,plain,
% 0.15/0.37 (tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)) = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))),
% 0.15/0.37 inference(unit_resolution,[status(thm)],[77, 71, 10, 38, 24])).
% 0.15/0.37 tff(79,plain,
% 0.15/0.37 (vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) = vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.15/0.37 inference(monotonicity,[status(thm)],[78, 58])).
% 0.15/0.37 tff(80,plain,
% 0.15/0.37 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))) <=> vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.37 inference(monotonicity,[status(thm)],[79])).
% 0.15/0.37 tff(81,plain,
% 0.15/0.37 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) <=> vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))),
% 0.15/0.37 inference(symmetry,[status(thm)],[80])).
% 0.15/0.37 tff(82,plain,
% 0.15/0.37 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))),
% 0.15/0.37 inference(modus_ponens,[status(thm)],[38, 81])).
% 0.15/0.37 tff(83,plain,
% 0.15/0.37 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : refl(((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))),
% 0.15/0.37 inference(bind,[status(th)],[])).
% 0.15/0.37 tff(84,plain,
% 0.15/0.37 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.37 inference(quant_intro,[status(thm)],[83])).
% 0.15/0.37 tff(85,plain,
% 0.15/0.37 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(trans(monotonicity(rewrite((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) <=> (~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> (~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))))), rewrite((~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1)) <=> (((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1)))), rewrite((((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1)) <=> ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1)) <=> ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))))),
% 0.15/0.37 inference(bind,[status(th)],[])).
% 0.15/0.37 tff(86,plain,
% 0.15/0.37 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1)) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.38 inference(quant_intro,[status(thm)],[85])).
% 0.15/0.38 tff(87,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1)) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1))),
% 0.15/0.38 inference(rewrite,[status(thm)],[])).
% 0.15/0.38 tff(88,plain,
% 0.15/0.38 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) <=> (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vqmr = Vqm1)) <=> ((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vqmr = Vqm1)))), rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vqmr = Vqm1)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vqmr = Vqm1)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1))))),
% 0.15/0.38 inference(bind,[status(th)],[])).
% 0.15/0.38 tff(89,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vqmr = Vqm1)) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1))),
% 0.15/0.38 inference(quant_intro,[status(thm)],[88])).
% 0.15/0.38 tff(90,axiom,(![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vqmr = Vqm1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqcond_inv7'')).
% 0.15/0.38 tff(91,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.15/0.38 tff(92,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[91, 87])).
% 0.15/0.38 tff(93,plain,(
% 0.15/0.38 ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vqmr = Vqm1))),
% 0.15/0.38 inference(skolemize,[status(sab)],[92])).
% 0.15/0.38 tff(94,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[93, 86])).
% 0.15/0.38 tff(95,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[94, 84])).
% 0.15/0.38 tff(96,plain,
% 0.15/0.38 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))),
% 0.15/0.38 inference(rewrite,[status(thm)],[])).
% 0.15/0.38 tff(97,plain,
% 0.15/0.38 (((Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))) <=> ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))),
% 0.15/0.38 inference(rewrite,[status(thm)],[])).
% 0.15/0.38 tff(98,plain,
% 0.15/0.38 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))))),
% 0.15/0.38 inference(monotonicity,[status(thm)],[97])).
% 0.15/0.38 tff(99,plain,
% 0.15/0.38 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))),
% 0.15/0.38 inference(transitivity,[status(thm)],[98, 96])).
% 0.15/0.38 tff(100,plain,
% 0.15/0.38 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))),
% 0.15/0.38 inference(quant_inst,[status(thm)],[])).
% 0.15/0.38 tff(101,plain,
% 0.15/0.38 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vqmr = Vqm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[100, 99])).
% 0.15/0.38 tff(102,plain,
% 0.15/0.38 ((Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))),
% 0.15/0.38 inference(unit_resolution,[status(thm)],[101, 95, 10, 24])).
% 0.15/0.38 tff(103,plain,
% 0.15/0.38 (Vqtm1!233 = tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))),
% 0.15/0.38 inference(unit_resolution,[status(thm)],[102, 82])).
% 0.15/0.38 tff(104,plain,
% 0.15/0.38 (Vqtm1!233 = tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))),
% 0.15/0.38 inference(transitivity,[status(thm)],[103, 58])).
% 0.15/0.38 tff(105,plain,
% 0.15/0.38 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : refl(((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))),
% 0.15/0.38 inference(bind,[status(th)],[])).
% 0.15/0.38 tff(106,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.38 inference(quant_intro,[status(thm)],[105])).
% 0.15/0.38 tff(107,plain,
% 0.15/0.38 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(trans(monotonicity(rewrite((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) <=> (~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> (~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))))), rewrite((~(~((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))), ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1)) <=> (((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1)))), rewrite((((~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1)) <=> ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))), (((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1)) <=> ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))))),
% 0.15/0.38 inference(bind,[status(th)],[])).
% 0.15/0.38 tff(108,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1)) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.38 inference(quant_intro,[status(thm)],[107])).
% 0.15/0.38 tff(109,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1)) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1))),
% 0.15/0.38 inference(rewrite,[status(thm)],[])).
% 0.15/0.38 tff(110,plain,
% 0.15/0.38 (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : trans(monotonicity(rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) <=> (vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vatmr = Vatm1)) <=> ((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vatmr = Vatm1)))), rewrite(((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vatmr = Vatm1)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1))), ((((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vatmr = Vatm1)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1))))),
% 0.15/0.38 inference(bind,[status(th)],[])).
% 0.15/0.38 tff(111,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vatmr = Vatm1)) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1))),
% 0.15/0.38 inference(quant_intro,[status(thm)],[110])).
% 0.15/0.38 tff(112,axiom,(![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))) => (Vatmr = Vatm1))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqcond_inv6'')).
% 0.15/0.38 tff(113,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[112, 111])).
% 0.15/0.38 tff(114,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[113, 109])).
% 0.15/0.38 tff(115,plain,(
% 0.15/0.38 ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1)))) | (Vatmr = Vatm1))),
% 0.15/0.38 inference(skolemize,[status(sab)],[114])).
% 0.15/0.38 tff(116,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[115, 108])).
% 0.15/0.38 tff(117,plain,
% 0.15/0.38 (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))),
% 0.15/0.38 inference(modus_ponens,[status(thm)],[116, 106])).
% 0.15/0.38 tff(118,plain,
% 0.15/0.38 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))),
% 0.15/0.38 inference(rewrite,[status(thm)],[])).
% 0.15/0.38 tff(119,plain,
% 0.15/0.38 (((Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))) <=> ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))),
% 0.15/0.39 inference(rewrite,[status(thm)],[])).
% 0.15/0.39 tff(120,plain,
% 0.15/0.39 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))))),
% 0.15/0.39 inference(monotonicity,[status(thm)],[119])).
% 0.15/0.39 tff(121,plain,
% 0.15/0.39 (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))),
% 0.15/0.39 inference(transitivity,[status(thm)],[120, 118])).
% 0.15/0.39 tff(122,plain,
% 0.15/0.39 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | ((Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))))),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(123,plain,
% 0.15/0.39 ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vexp: vExp, Vq2: vQuestionnaire] : ((Vatmr = Vatm1) | (~vptcheck(vMC(Vatm, Vqm), vqcond(Vexp, Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), Vq2, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqcond(vconstant(vB(vno)), vq1, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq1, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.15/0.39 tff(124,plain,
% 0.15/0.39 ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)), tptp_fun_Vqm1_223(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231)))),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[123, 117, 10, 24])).
% 0.15/0.39 tff(125,plain,
% 0.15/0.39 (Vatm1!229 = tptp_fun_Vatm1_224(vtypeAM(Vam!228), vq1, vtypeQM(Vqm!231))),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[124, 82])).
% 0.15/0.39 tff(126,plain,
% 0.15/0.39 (Vatm1!229 = tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))),
% 0.15/0.39 inference(transitivity,[status(thm)],[125, 78])).
% 0.15/0.39 tff(127,plain,
% 0.15/0.39 (vMC(Vatm1!229, Vqtm1!233) = vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.15/0.39 inference(monotonicity,[status(thm)],[126, 104])).
% 0.15/0.39 tff(128,plain,
% 0.15/0.39 (^[VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : refl((vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq) <=> (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq))),
% 0.15/0.39 inference(bind,[status(th)],[])).
% 0.15/0.39 tff(129,plain,
% 0.15/0.39 (![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.15/0.39 inference(quant_intro,[status(thm)],[128])).
% 0.15/0.39 tff(130,plain,
% 0.15/0.39 (![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.15/0.39 inference(rewrite,[status(thm)],[])).
% 0.15/0.39 tff(131,axiom,(![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQuest-0'')).
% 0.15/0.39 tff(132,plain,
% 0.15/0.39 (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[131, 130])).
% 0.15/0.39 tff(133,plain,(
% 0.15/0.39 ![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.15/0.39 inference(skolemize,[status(sab)],[132])).
% 0.15/0.39 tff(134,plain,
% 0.15/0.39 (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[133, 129])).
% 0.15/0.39 tff(135,plain,
% 0.15/0.39 ((~![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)) | (vgetQuest(vQC(Vam!228, Vqm!231, vq2)) = vq2)),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(136,plain,
% 0.15/0.39 (vgetQuest(vQC(Vam!228, Vqm!231, vq2)) = vq2),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[135, 134])).
% 0.15/0.39 tff(137,plain,
% 0.15/0.39 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc) <=> ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.15/0.39 inference(rewrite,[status(thm)],[])).
% 0.15/0.39 tff(138,plain,
% 0.15/0.39 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc) <=> ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.15/0.39 inference(rewrite,[status(thm)],[])).
% 0.15/0.39 tff(139,axiom,(![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQC-0'')).
% 0.15/0.39 tff(140,plain,
% 0.15/0.39 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[139, 138])).
% 0.15/0.39 tff(141,plain,(
% 0.15/0.39 ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.15/0.39 inference(skolemize,[status(sab)],[140])).
% 0.15/0.39 tff(142,plain,
% 0.15/0.39 (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[141, 137])).
% 0.15/0.39 tff(143,plain,
% 0.15/0.39 ((~![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)) | (vgetQC(vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))) = vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(144,plain,
% 0.15/0.39 (vgetQC(vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))) = vQC(Vamr!230, Vqmr!227, Vqr!232)),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[143, 142])).
% 0.15/0.39 tff(145,plain,
% 0.15/0.39 (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.15/0.39 inference(and_elim,[status(thm)],[9])).
% 0.15/0.39 tff(146,plain,
% 0.15/0.39 (^[Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : refl((vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2))) <=> (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2))))),
% 0.15/0.39 inference(bind,[status(th)],[])).
% 0.15/0.39 tff(147,plain,
% 0.15/0.39 (![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2))) <=> ![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2)))),
% 0.15/0.39 inference(quant_intro,[status(thm)],[146])).
% 0.15/0.39 tff(148,plain,
% 0.15/0.39 (![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2))) <=> ![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2)))),
% 0.15/0.39 inference(rewrite,[status(thm)],[])).
% 0.15/0.39 tff(149,axiom,(![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''reduce-12'')).
% 0.15/0.39 tff(150,plain,
% 0.15/0.39 (![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2)))),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[149, 148])).
% 0.15/0.39 tff(151,plain,(
% 0.15/0.39 ![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2)))),
% 0.15/0.39 inference(skolemize,[status(sab)],[150])).
% 0.15/0.39 tff(152,plain,
% 0.15/0.39 (![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2)))),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[151, 147])).
% 0.15/0.39 tff(153,plain,
% 0.15/0.39 ((~![Vqs1: vQuestionnaire, Vqs2: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqcond(vconstant(vB(vno)), Vqs1, Vqs2), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs2)))) | (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vam!228, Vqm!231, vq2)))),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(154,plain,
% 0.15/0.39 (vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vam!228, Vqm!231, vq2))),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[153, 152])).
% 0.15/0.39 tff(155,plain,
% 0.15/0.39 (vsomeQConf(vQC(Vam!228, Vqm!231, vq2)) = vreduce(vqcond(vconstant(vB(vno)), vq1, vq2), Vam!228, Vqm!231)),
% 0.15/0.39 inference(symmetry,[status(thm)],[154])).
% 0.15/0.39 tff(156,plain,
% 0.15/0.39 (vsomeQConf(vQC(Vam!228, Vqm!231, vq2)) = vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.15/0.39 inference(transitivity,[status(thm)],[155, 145])).
% 0.15/0.39 tff(157,plain,
% 0.15/0.39 (vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2))) = vgetQC(vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232)))),
% 0.15/0.39 inference(monotonicity,[status(thm)],[156])).
% 0.15/0.39 tff(158,plain,
% 0.15/0.39 ((~![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)) | (vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2))) = vQC(Vam!228, Vqm!231, vq2))),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(159,plain,
% 0.15/0.39 (vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2))) = vQC(Vam!228, Vqm!231, vq2)),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[158, 142])).
% 0.15/0.39 tff(160,plain,
% 0.15/0.39 (vQC(Vam!228, Vqm!231, vq2) = vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2)))),
% 0.15/0.39 inference(symmetry,[status(thm)],[159])).
% 0.15/0.39 tff(161,plain,
% 0.15/0.39 (vQC(Vam!228, Vqm!231, vq2) = vQC(Vamr!230, Vqmr!227, Vqr!232)),
% 0.15/0.39 inference(transitivity,[status(thm)],[160, 157, 144])).
% 0.15/0.39 tff(162,plain,
% 0.15/0.39 (vgetQuest(vQC(Vam!228, Vqm!231, vq2)) = vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.15/0.39 inference(monotonicity,[status(thm)],[161])).
% 0.15/0.39 tff(163,plain,
% 0.15/0.39 (vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232)) = vgetQuest(vQC(Vam!228, Vqm!231, vq2))),
% 0.15/0.39 inference(symmetry,[status(thm)],[162])).
% 0.15/0.39 tff(164,plain,
% 0.15/0.39 ((~![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)) | (vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqr!232)),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(165,plain,
% 0.15/0.39 (vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqr!232),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[164, 134])).
% 0.15/0.39 tff(166,plain,
% 0.15/0.39 (Vqr!232 = vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.15/0.39 inference(symmetry,[status(thm)],[165])).
% 0.15/0.39 tff(167,plain,
% 0.15/0.39 (Vqr!232 = vq2),
% 0.15/0.39 inference(transitivity,[status(thm)],[166, 163, 136])).
% 0.15/0.39 tff(168,plain,
% 0.15/0.39 (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.39 inference(monotonicity,[status(thm)],[167, 127])).
% 0.15/0.39 tff(169,plain,
% 0.15/0.39 (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233))),
% 0.15/0.39 inference(symmetry,[status(thm)],[168])).
% 0.15/0.39 tff(170,plain,
% 0.15/0.39 (^[VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : refl((vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm) <=> (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm))),
% 0.15/0.39 inference(bind,[status(th)],[])).
% 0.15/0.39 tff(171,plain,
% 0.15/0.39 (![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.15/0.39 inference(quant_intro,[status(thm)],[170])).
% 0.15/0.39 tff(172,plain,
% 0.15/0.39 (![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.15/0.39 inference(rewrite,[status(thm)],[])).
% 0.15/0.39 tff(173,axiom,(![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQM-0'')).
% 0.15/0.39 tff(174,plain,
% 0.15/0.39 (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[173, 172])).
% 0.15/0.39 tff(175,plain,(
% 0.15/0.39 ![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.15/0.39 inference(skolemize,[status(sab)],[174])).
% 0.15/0.39 tff(176,plain,
% 0.15/0.39 (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.15/0.39 inference(modus_ponens,[status(thm)],[175, 171])).
% 0.15/0.39 tff(177,plain,
% 0.15/0.39 ((~![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)) | (vgetQM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqmr!227)),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(178,plain,
% 0.15/0.39 (vgetQM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqmr!227),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[177, 176])).
% 0.15/0.39 tff(179,plain,
% 0.15/0.39 (vgetQM(vQC(Vam!228, Vqm!231, vq2)) = vgetQM(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.15/0.39 inference(monotonicity,[status(thm)],[161])).
% 0.15/0.39 tff(180,plain,
% 0.15/0.39 ((~![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)) | (vgetQM(vQC(Vam!228, Vqm!231, vq2)) = Vqm!231)),
% 0.15/0.39 inference(quant_inst,[status(thm)],[])).
% 0.15/0.39 tff(181,plain,
% 0.15/0.39 (vgetQM(vQC(Vam!228, Vqm!231, vq2)) = Vqm!231),
% 0.15/0.39 inference(unit_resolution,[status(thm)],[180, 176])).
% 0.15/0.39 tff(182,plain,
% 0.15/0.39 (Vqm!231 = vgetQM(vQC(Vam!228, Vqm!231, vq2))),
% 0.15/0.39 inference(symmetry,[status(thm)],[181])).
% 0.15/0.39 tff(183,plain,
% 0.15/0.39 (Vqm!231 = Vqmr!227),
% 0.15/0.39 inference(transitivity,[status(thm)],[182, 179, 178])).
% 0.15/0.39 tff(184,plain,
% 0.15/0.39 (vtypeQM(Vqm!231) = vtypeQM(Vqmr!227)),
% 0.15/0.39 inference(monotonicity,[status(thm)],[183])).
% 0.15/0.39 tff(185,plain,
% 0.15/0.39 (^[Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : refl((vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam) <=> (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam))),
% 0.15/0.39 inference(bind,[status(th)],[])).
% 0.15/0.39 tff(186,plain,
% 0.15/0.39 (![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.15/0.39 inference(quant_intro,[status(thm)],[185])).
% 0.15/0.39 tff(187,plain,
% 0.15/0.39 (![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.15/0.41 inference(rewrite,[status(thm)],[])).
% 0.15/0.41 tff(188,axiom,(![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getAM-0'')).
% 0.15/0.41 tff(189,plain,
% 0.15/0.41 (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.15/0.41 inference(modus_ponens,[status(thm)],[188, 187])).
% 0.15/0.41 tff(190,plain,(
% 0.15/0.41 ![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.15/0.41 inference(skolemize,[status(sab)],[189])).
% 0.15/0.41 tff(191,plain,
% 0.15/0.41 (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.15/0.41 inference(modus_ponens,[status(thm)],[190, 186])).
% 0.15/0.41 tff(192,plain,
% 0.15/0.41 ((~![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)) | (vgetAM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vamr!230)),
% 0.15/0.41 inference(quant_inst,[status(thm)],[])).
% 0.15/0.41 tff(193,plain,
% 0.15/0.41 (vgetAM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vamr!230),
% 0.15/0.41 inference(unit_resolution,[status(thm)],[192, 191])).
% 0.15/0.41 tff(194,plain,
% 0.15/0.41 (vgetAM(vQC(Vam!228, Vqm!231, vq2)) = vgetAM(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.15/0.41 inference(monotonicity,[status(thm)],[161])).
% 0.15/0.41 tff(195,plain,
% 0.15/0.41 ((~![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)) | (vgetAM(vQC(Vam!228, Vqm!231, vq2)) = Vam!228)),
% 0.15/0.41 inference(quant_inst,[status(thm)],[])).
% 0.15/0.41 tff(196,plain,
% 0.15/0.41 (vgetAM(vQC(Vam!228, Vqm!231, vq2)) = Vam!228),
% 0.15/0.41 inference(unit_resolution,[status(thm)],[195, 191])).
% 0.15/0.41 tff(197,plain,
% 0.15/0.41 (Vam!228 = vgetAM(vQC(Vam!228, Vqm!231, vq2))),
% 0.15/0.41 inference(symmetry,[status(thm)],[196])).
% 0.15/0.41 tff(198,plain,
% 0.15/0.41 (Vam!228 = Vamr!230),
% 0.15/0.41 inference(transitivity,[status(thm)],[197, 194, 193])).
% 0.15/0.41 tff(199,plain,
% 0.15/0.41 (vtypeAM(Vam!228) = vtypeAM(Vamr!230)),
% 0.15/0.41 inference(monotonicity,[status(thm)],[198])).
% 0.15/0.41 tff(200,plain,
% 0.15/0.41 (vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)) = vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227))),
% 0.15/0.41 inference(monotonicity,[status(thm)],[199, 184])).
% 0.15/0.41 tff(201,plain,
% 0.15/0.41 (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.41 inference(monotonicity,[status(thm)],[200])).
% 0.15/0.41 tff(202,plain,
% 0.15/0.41 (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vq2, vMC(tptp_fun_Vatm1_226(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm1_225(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.15/0.41 inference(modus_ponens,[status(thm)],[38, 201])).
% 0.15/0.41 tff(203,plain,
% 0.15/0.41 (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233))),
% 0.15/0.41 inference(modus_ponens,[status(thm)],[202, 169])).
% 0.15/0.41 tff(204,plain,
% 0.15/0.41 (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233))),
% 0.15/0.41 inference(or_elim,[status(thm)],[8])).
% 0.15/0.41 tff(205,plain,
% 0.15/0.41 ($false),
% 0.15/0.41 inference(unit_resolution,[status(thm)],[204, 203])).
% 0.15/0.41 % SZS output end Proof
% 0.15/0.41 % E exiting
%------------------------------------------------------------------------------