Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : COM258_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n028.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.29s 0.50s
% Output   : Proof 0.29s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : COM258_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12  % Command    : run_E %s %d THM
% 0.13/0.32  % Computer : n028.cluster.edu
% 0.13/0.32  % Model    : x86_64 x86_64
% 0.13/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32  % Memory   : 8042.1875MB
% 0.13/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32  % CPULimit   : 300
% 0.13/0.32  % WCLimit    : 300
% 0.13/0.32  % DateTime   : Mon May  4 19:52:02 EDT 2026
% 0.13/0.32  % CPUTime    : 
% 0.29/0.50  % SZS status Theorem
% 0.29/0.50  % SZS output start Proof
% 0.29/0.50  tff(vptcheck_type, type, (
% 0.29/0.50     vptcheck: ( vMapConf * vQuestionnaire * vMapConf ) > $o)).
% 0.29/0.50  tff(vMC_type, type, (
% 0.29/0.50     vMC: ( vATMap * vATMap ) > vMapConf)).
% 0.29/0.50  tff(tptp_fun_Vqtm1_233_type, type, (
% 0.29/0.50     tptp_fun_Vqtm1_233: vATMap)).
% 0.29/0.50  tff(tptp_fun_Vatm1_229_type, type, (
% 0.29/0.50     tptp_fun_Vatm1_229: vATMap)).
% 0.29/0.50  tff(tptp_fun_Vqr_232_type, type, (
% 0.29/0.50     tptp_fun_Vqr_232: vQuestionnaire)).
% 0.29/0.50  tff(vtypeQM_type, type, (
% 0.29/0.50     vtypeQM: vQMap > vATMap)).
% 0.29/0.50  tff(tptp_fun_Vqmr_227_type, type, (
% 0.29/0.50     tptp_fun_Vqmr_227: vQMap)).
% 0.29/0.50  tff(vtypeAM_type, type, (
% 0.29/0.50     vtypeAM: vAnsMap > vATMap)).
% 0.29/0.50  tff(tptp_fun_Vamr_230_type, type, (
% 0.29/0.50     tptp_fun_Vamr_230: vAnsMap)).
% 0.29/0.50  tff(tptp_fun_Vqm2_221_type, type, (
% 0.29/0.50     tptp_fun_Vqm2_221: ( vQuestionnaire * vATMap * vATMap ) > vATMap)).
% 0.29/0.50  tff(tptp_fun_Vqm_231_type, type, (
% 0.29/0.50     tptp_fun_Vqm_231: vQMap)).
% 0.29/0.50  tff(tptp_fun_Vam_228_type, type, (
% 0.29/0.50     tptp_fun_Vam_228: vAnsMap)).
% 0.29/0.50  tff(vq2_type, type, (
% 0.29/0.50     vq2: vQuestionnaire)).
% 0.29/0.50  tff(tptp_fun_Vatm2_222_type, type, (
% 0.29/0.50     tptp_fun_Vatm2_222: ( vQuestionnaire * vATMap * vATMap ) > vATMap)).
% 0.29/0.50  tff(vgetQuest_type, type, (
% 0.29/0.50     vgetQuest: vQConf > vQuestionnaire)).
% 0.29/0.50  tff(vQC_type, type, (
% 0.29/0.50     vQC: ( vAnsMap * vQMap * vQuestionnaire ) > vQConf)).
% 0.29/0.50  tff(vgetQC_type, type, (
% 0.29/0.50     vgetQC: vOptQConf > vQConf)).
% 0.29/0.50  tff(vsomeQConf_type, type, (
% 0.29/0.50     vsomeQConf: vQConf > vOptQConf)).
% 0.29/0.50  tff(vreduce_type, type, (
% 0.29/0.50     vreduce: ( vQuestionnaire * vAnsMap * vQMap ) > vOptQConf)).
% 0.29/0.50  tff(vqseq_type, type, (
% 0.29/0.50     vqseq: ( vQuestionnaire * vQuestionnaire ) > vQuestionnaire)).
% 0.29/0.50  tff(vq1_type, type, (
% 0.29/0.50     vq1: vQuestionnaire)).
% 0.29/0.50  tff(vqempty_type, type, (
% 0.29/0.50     vqempty: vQuestionnaire)).
% 0.29/0.50  tff(vgetQM_type, type, (
% 0.29/0.50     vgetQM: vQConf > vQMap)).
% 0.29/0.50  tff(vgetAM_type, type, (
% 0.29/0.50     vgetAM: vQConf > vAnsMap)).
% 0.29/0.50  tff(1,plain,
% 0.29/0.50      (^[VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : refl((vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq) <=> (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq))),
% 0.29/0.50      inference(bind,[status(th)],[])).
% 0.29/0.50  tff(2,plain,
% 0.29/0.50      (![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.29/0.50      inference(quant_intro,[status(thm)],[1])).
% 0.29/0.50  tff(3,plain,
% 0.29/0.50      (![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.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(4,axiom,(![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQuest-0'')).
% 0.29/0.50  tff(5,plain,
% 0.29/0.50      (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[4, 3])).
% 0.29/0.50  tff(6,plain,(
% 0.29/0.50      ![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.29/0.50      inference(skolemize,[status(sab)],[5])).
% 0.29/0.50  tff(7,plain,
% 0.29/0.50      (![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[6, 2])).
% 0.29/0.50  tff(8,plain,
% 0.29/0.50      ((~![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)) | (vgetQuest(vQC(Vam!228, Vqm!231, vq2)) = vq2)),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(9,plain,
% 0.29/0.50      (vgetQuest(vQC(Vam!228, Vqm!231, vq2)) = vq2),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[8, 7])).
% 0.29/0.50  tff(10,plain,
% 0.29/0.50      (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc) <=> ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(11,plain,
% 0.29/0.50      (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc) <=> ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(12,axiom,(![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQC-0'')).
% 0.29/0.50  tff(13,plain,
% 0.29/0.50      (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[12, 11])).
% 0.29/0.50  tff(14,plain,(
% 0.29/0.50      ![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.29/0.50      inference(skolemize,[status(sab)],[13])).
% 0.29/0.50  tff(15,plain,
% 0.29/0.50      (![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[14, 10])).
% 0.29/0.50  tff(16,plain,
% 0.29/0.50      ((~![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)) | (vgetQC(vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))) = vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(17,plain,
% 0.29/0.50      (vgetQC(vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))) = vQC(Vamr!230, Vqmr!227, Vqr!232)),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[16, 15])).
% 0.29/0.50  tff(18,plain,
% 0.29/0.50      ((~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqseq(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] : ((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqseq(vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1))))),
% 0.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(19,plain,
% 0.29/0.50      ((~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1))) & (vreduce(vqseq(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] : ((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqseq(vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1))))),
% 0.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(20,axiom,(~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1))) & (vreduce(vqseq(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-qseq-qempty'')).
% 0.29/0.50  tff(21,plain,
% 0.29/0.50      (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqseq(vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[20, 19])).
% 0.29/0.50  tff(22,plain,
% 0.29/0.50      (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqseq(vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[21, 18])).
% 0.29/0.50  tff(23,plain,
% 0.29/0.50      (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqseq(vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[22, 18])).
% 0.29/0.50  tff(24,plain,
% 0.29/0.50      (~![Vqtm1: vATMap, Vqr: vQuestionnaire, Vqm: vQMap, Vamr: vAnsMap, Vatm1: vATMap, Vam: vAnsMap, Vqmr: vQMap] : ((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqseq(vq1, vq2), vMC(Vatm1, Vqtm1)) & (vreduce(vqseq(vq1, vq2), Vam, Vqm) = vsomeQConf(vQC(Vamr, Vqmr, Vqr))))) | vptcheck(vMC(vtypeAM(Vamr), vtypeQM(Vqmr)), Vqr, vMC(Vatm1, Vqtm1)))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[23, 18])).
% 0.29/0.50  tff(25,plain,(
% 0.29/0.50      ~((~((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233)) & (vreduce(vqseq(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.29/0.50      inference(skolemize,[status(sab)],[24])).
% 0.29/0.50  tff(26,plain,
% 0.29/0.50      ((vq1 = vqempty) & vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233)) & (vreduce(vqseq(vq1, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232)))),
% 0.29/0.50      inference(or_elim,[status(thm)],[25])).
% 0.29/0.50  tff(27,plain,
% 0.29/0.50      (vreduce(vqseq(vq1, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.29/0.50      inference(and_elim,[status(thm)],[26])).
% 0.29/0.50  tff(28,plain,
% 0.29/0.50      (vq1 = vqempty),
% 0.29/0.50      inference(and_elim,[status(thm)],[26])).
% 0.29/0.50  tff(29,plain,
% 0.29/0.50      (vqempty = vq1),
% 0.29/0.50      inference(symmetry,[status(thm)],[28])).
% 0.29/0.50  tff(30,plain,
% 0.29/0.50      (vqseq(vqempty, vq2) = vqseq(vq1, vq2)),
% 0.29/0.50      inference(monotonicity,[status(thm)],[29])).
% 0.29/0.50  tff(31,plain,
% 0.29/0.50      (vreduce(vqseq(vqempty, vq2), Vam!228, Vqm!231) = vreduce(vqseq(vq1, vq2), Vam!228, Vqm!231)),
% 0.29/0.50      inference(monotonicity,[status(thm)],[30])).
% 0.29/0.50  tff(32,plain,
% 0.29/0.50      (^[Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : refl((vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs))) <=> (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs))))),
% 0.29/0.50      inference(bind,[status(th)],[])).
% 0.29/0.50  tff(33,plain,
% 0.29/0.50      (![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs))) <=> ![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs)))),
% 0.29/0.50      inference(quant_intro,[status(thm)],[32])).
% 0.29/0.50  tff(34,plain,
% 0.29/0.50      (![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs))) <=> ![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs)))),
% 0.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(35,axiom,(![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''reduce-8'')).
% 0.29/0.50  tff(36,plain,
% 0.29/0.50      (![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs)))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[35, 34])).
% 0.29/0.50  tff(37,plain,(
% 0.29/0.50      ![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs)))),
% 0.29/0.50      inference(skolemize,[status(sab)],[36])).
% 0.29/0.50  tff(38,plain,
% 0.29/0.50      (![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs)))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[37, 33])).
% 0.29/0.50  tff(39,plain,
% 0.29/0.50      ((~![Vqs: vQuestionnaire, Vam: vAnsMap, Vqm: vQMap] : (vreduce(vqseq(vqempty, Vqs), Vam, Vqm) = vsomeQConf(vQC(Vam, Vqm, Vqs)))) | (vreduce(vqseq(vqempty, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vam!228, Vqm!231, vq2)))),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(40,plain,
% 0.29/0.50      (vreduce(vqseq(vqempty, vq2), Vam!228, Vqm!231) = vsomeQConf(vQC(Vam!228, Vqm!231, vq2))),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[39, 38])).
% 0.29/0.50  tff(41,plain,
% 0.29/0.50      (vsomeQConf(vQC(Vam!228, Vqm!231, vq2)) = vreduce(vqseq(vqempty, vq2), Vam!228, Vqm!231)),
% 0.29/0.50      inference(symmetry,[status(thm)],[40])).
% 0.29/0.50  tff(42,plain,
% 0.29/0.50      (vsomeQConf(vQC(Vam!228, Vqm!231, vq2)) = vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.29/0.50      inference(transitivity,[status(thm)],[41, 31, 27])).
% 0.29/0.50  tff(43,plain,
% 0.29/0.50      (vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2))) = vgetQC(vsomeQConf(vQC(Vamr!230, Vqmr!227, Vqr!232)))),
% 0.29/0.50      inference(monotonicity,[status(thm)],[42])).
% 0.29/0.50  tff(44,plain,
% 0.29/0.50      ((~![Vqc: vQConf] : (vgetQC(vsomeQConf(Vqc)) = Vqc)) | (vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2))) = vQC(Vam!228, Vqm!231, vq2))),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(45,plain,
% 0.29/0.50      (vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2))) = vQC(Vam!228, Vqm!231, vq2)),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[44, 15])).
% 0.29/0.50  tff(46,plain,
% 0.29/0.50      (vQC(Vam!228, Vqm!231, vq2) = vgetQC(vsomeQConf(vQC(Vam!228, Vqm!231, vq2)))),
% 0.29/0.50      inference(symmetry,[status(thm)],[45])).
% 0.29/0.50  tff(47,plain,
% 0.29/0.50      (vQC(Vam!228, Vqm!231, vq2) = vQC(Vamr!230, Vqmr!227, Vqr!232)),
% 0.29/0.50      inference(transitivity,[status(thm)],[46, 43, 17])).
% 0.29/0.50  tff(48,plain,
% 0.29/0.50      (vgetQuest(vQC(Vam!228, Vqm!231, vq2)) = vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.29/0.50      inference(monotonicity,[status(thm)],[47])).
% 0.29/0.50  tff(49,plain,
% 0.29/0.50      (vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232)) = vgetQuest(vQC(Vam!228, Vqm!231, vq2))),
% 0.29/0.50      inference(symmetry,[status(thm)],[48])).
% 0.29/0.50  tff(50,plain,
% 0.29/0.50      ((~![VwildcardName0: vAnsMap, VwildcardName1: vQMap, Vq: vQuestionnaire] : (vgetQuest(vQC(VwildcardName0, VwildcardName1, Vq)) = Vq)) | (vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqr!232)),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(51,plain,
% 0.29/0.50      (vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqr!232),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[50, 7])).
% 0.29/0.50  tff(52,plain,
% 0.29/0.50      (Vqr!232 = vgetQuest(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.29/0.50      inference(symmetry,[status(thm)],[51])).
% 0.29/0.50  tff(53,plain,
% 0.29/0.50      (Vqr!232 = vq2),
% 0.29/0.50      inference(transitivity,[status(thm)],[52, 49, 9])).
% 0.29/0.50  tff(54,plain,
% 0.29/0.50      (^[VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : refl((vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm) <=> (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm))),
% 0.29/0.50      inference(bind,[status(th)],[])).
% 0.29/0.50  tff(55,plain,
% 0.29/0.50      (![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.29/0.50      inference(quant_intro,[status(thm)],[54])).
% 0.29/0.50  tff(56,plain,
% 0.29/0.50      (![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.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(57,axiom,(![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQM-0'')).
% 0.29/0.50  tff(58,plain,
% 0.29/0.50      (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[57, 56])).
% 0.29/0.50  tff(59,plain,(
% 0.29/0.50      ![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.29/0.50      inference(skolemize,[status(sab)],[58])).
% 0.29/0.50  tff(60,plain,
% 0.29/0.50      (![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[59, 55])).
% 0.29/0.50  tff(61,plain,
% 0.29/0.50      ((~![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)) | (vgetQM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqmr!227)),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(62,plain,
% 0.29/0.50      (vgetQM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vqmr!227),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[61, 60])).
% 0.29/0.50  tff(63,plain,
% 0.29/0.50      (vgetQM(vQC(Vam!228, Vqm!231, vq2)) = vgetQM(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.29/0.50      inference(monotonicity,[status(thm)],[47])).
% 0.29/0.50  tff(64,plain,
% 0.29/0.50      ((~![VwildcardName0: vAnsMap, Vqm: vQMap, VwildcardName1: vQuestionnaire] : (vgetQM(vQC(VwildcardName0, Vqm, VwildcardName1)) = Vqm)) | (vgetQM(vQC(Vam!228, Vqm!231, vq2)) = Vqm!231)),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(65,plain,
% 0.29/0.50      (vgetQM(vQC(Vam!228, Vqm!231, vq2)) = Vqm!231),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[64, 60])).
% 0.29/0.50  tff(66,plain,
% 0.29/0.50      (Vqm!231 = vgetQM(vQC(Vam!228, Vqm!231, vq2))),
% 0.29/0.50      inference(symmetry,[status(thm)],[65])).
% 0.29/0.50  tff(67,plain,
% 0.29/0.50      (Vqm!231 = Vqmr!227),
% 0.29/0.50      inference(transitivity,[status(thm)],[66, 63, 62])).
% 0.29/0.50  tff(68,plain,
% 0.29/0.50      (vtypeQM(Vqm!231) = vtypeQM(Vqmr!227)),
% 0.29/0.50      inference(monotonicity,[status(thm)],[67])).
% 0.29/0.50  tff(69,plain,
% 0.29/0.50      (^[Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : refl((vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam) <=> (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam))),
% 0.29/0.50      inference(bind,[status(th)],[])).
% 0.29/0.50  tff(70,plain,
% 0.29/0.50      (![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.29/0.50      inference(quant_intro,[status(thm)],[69])).
% 0.29/0.50  tff(71,plain,
% 0.29/0.50      (![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.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(72,axiom,(![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getAM-0'')).
% 0.29/0.50  tff(73,plain,
% 0.29/0.50      (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[72, 71])).
% 0.29/0.50  tff(74,plain,(
% 0.29/0.50      ![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.29/0.50      inference(skolemize,[status(sab)],[73])).
% 0.29/0.50  tff(75,plain,
% 0.29/0.50      (![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[74, 70])).
% 0.29/0.50  tff(76,plain,
% 0.29/0.50      ((~![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)) | (vgetAM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vamr!230)),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(77,plain,
% 0.29/0.50      (vgetAM(vQC(Vamr!230, Vqmr!227, Vqr!232)) = Vamr!230),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[76, 75])).
% 0.29/0.50  tff(78,plain,
% 0.29/0.50      (vgetAM(vQC(Vam!228, Vqm!231, vq2)) = vgetAM(vQC(Vamr!230, Vqmr!227, Vqr!232))),
% 0.29/0.50      inference(monotonicity,[status(thm)],[47])).
% 0.29/0.50  tff(79,plain,
% 0.29/0.50      ((~![Vam: vAnsMap, VwildcardName0: vQMap, VwildcardName1: vQuestionnaire] : (vgetAM(vQC(Vam, VwildcardName0, VwildcardName1)) = Vam)) | (vgetAM(vQC(Vam!228, Vqm!231, vq2)) = Vam!228)),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(80,plain,
% 0.29/0.50      (vgetAM(vQC(Vam!228, Vqm!231, vq2)) = Vam!228),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[79, 75])).
% 0.29/0.50  tff(81,plain,
% 0.29/0.50      (Vam!228 = vgetAM(vQC(Vam!228, Vqm!231, vq2))),
% 0.29/0.50      inference(symmetry,[status(thm)],[80])).
% 0.29/0.50  tff(82,plain,
% 0.29/0.50      (Vam!228 = Vamr!230),
% 0.29/0.50      inference(transitivity,[status(thm)],[81, 78, 77])).
% 0.29/0.50  tff(83,plain,
% 0.29/0.50      (vtypeAM(Vam!228) = vtypeAM(Vamr!230)),
% 0.29/0.50      inference(monotonicity,[status(thm)],[82])).
% 0.29/0.50  tff(84,plain,
% 0.29/0.50      (vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)) = vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227))),
% 0.29/0.50      inference(monotonicity,[status(thm)],[83, 68])).
% 0.29/0.50  tff(85,plain,
% 0.29/0.50      (vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)) = vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231))),
% 0.29/0.50      inference(symmetry,[status(thm)],[84])).
% 0.29/0.50  tff(86,plain,
% 0.29/0.50      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) <=> vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.50      inference(monotonicity,[status(thm)],[85, 53])).
% 0.29/0.50  tff(87,plain,
% 0.29/0.50      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.50      inference(symmetry,[status(thm)],[86])).
% 0.29/0.50  tff(88,plain,
% 0.29/0.50      (^[Vatm: vATMap, Vqm: vATMap] : refl(vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)) <=> vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)))),
% 0.29/0.50      inference(bind,[status(th)],[])).
% 0.29/0.50  tff(89,plain,
% 0.29/0.50      (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)) <=> ![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.29/0.50      inference(quant_intro,[status(thm)],[88])).
% 0.29/0.50  tff(90,plain,
% 0.29/0.50      (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm)) <=> ![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.29/0.50      inference(rewrite,[status(thm)],[])).
% 0.29/0.50  tff(91,axiom,(![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqempty'')).
% 0.29/0.50  tff(92,plain,
% 0.29/0.50      (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[91, 90])).
% 0.29/0.50  tff(93,plain,(
% 0.29/0.50      ![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.29/0.50      inference(skolemize,[status(sab)],[92])).
% 0.29/0.50  tff(94,plain,
% 0.29/0.50      (![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[93, 89])).
% 0.29/0.50  tff(95,plain,
% 0.29/0.50      ((~![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.29/0.50      inference(quant_inst,[status(thm)],[])).
% 0.29/0.50  tff(96,plain,
% 0.29/0.50      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.29/0.50      inference(unit_resolution,[status(thm)],[95, 94])).
% 0.29/0.50  tff(97,plain,
% 0.29/0.50      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.50      inference(monotonicity,[status(thm)],[30])).
% 0.29/0.50  tff(98,plain,
% 0.29/0.50      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.50      inference(symmetry,[status(thm)],[97])).
% 0.29/0.50  tff(99,plain,
% 0.29/0.50      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.50      inference(and_elim,[status(thm)],[26])).
% 0.29/0.50  tff(100,plain,
% 0.29/0.50      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.50      inference(modus_ponens,[status(thm)],[99, 98])).
% 0.29/0.50  tff(101,plain,
% 0.29/0.50      (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : refl((vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) <=> (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))))),
% 0.29/0.50      inference(bind,[status(th)],[])).
% 0.29/0.50  tff(102,plain,
% 0.29/0.50      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))),
% 0.29/0.50      inference(quant_intro,[status(thm)],[101])).
% 0.29/0.50  tff(103,plain,
% 0.29/0.50      (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : trans(monotonicity(trans(monotonicity(rewrite((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) <=> (~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))))), ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) <=> (~(~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))))))), rewrite((~(~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))), ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))))), (((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1)))) <=> (((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1)))))), rewrite((((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1)))) <=> (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))), (((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1)))) <=> (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))))),
% 0.29/0.50      inference(bind,[status(th)],[])).
% 0.29/0.50  tff(104,plain,
% 0.29/0.50      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1)))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))),
% 0.29/0.51      inference(quant_intro,[status(thm)],[103])).
% 0.29/0.51  tff(105,plain,
% 0.29/0.51      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))),
% 0.29/0.51      inference(rewrite,[status(thm)],[])).
% 0.29/0.51  tff(106,plain,
% 0.29/0.51      (^[Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : rewrite(((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) => ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.51      inference(bind,[status(th)],[])).
% 0.29/0.51  tff(107,plain,
% 0.29/0.51      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) => ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) <=> ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))),
% 0.29/0.51      inference(quant_intro,[status(thm)],[106])).
% 0.29/0.51  tff(108,axiom,(![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) => ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqseq_inv2'')).
% 0.29/0.51  tff(109,plain,
% 0.29/0.51      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[108, 107])).
% 0.29/0.51  tff(110,plain,
% 0.29/0.51      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | ?[Vatm2: vATMap, Vqm2: vATMap] : vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[109, 105])).
% 0.29/0.51  tff(111,plain,(
% 0.29/0.51      ![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)))) | vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))))),
% 0.29/0.51      inference(skolemize,[status(sab)],[110])).
% 0.29/0.51  tff(112,plain,
% 0.29/0.51      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[111, 104])).
% 0.29/0.51  tff(113,plain,
% 0.29/0.51      (![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[112, 102])).
% 0.29/0.51  tff(114,plain,
% 0.29/0.51      (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.29/0.51      inference(rewrite,[status(thm)],[])).
% 0.29/0.51  tff(115,plain,
% 0.29/0.51      ((vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231))))) <=> ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.29/0.51      inference(rewrite,[status(thm)],[])).
% 0.29/0.51  tff(116,plain,
% 0.29/0.51      (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | ((~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.29/0.51      inference(monotonicity,[status(thm)],[115])).
% 0.29/0.51  tff(117,plain,
% 0.29/0.51      (((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.29/0.51      inference(transitivity,[status(thm)],[116, 114])).
% 0.29/0.51  tff(118,plain,
% 0.29/0.51      ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.29/0.51      inference(quant_inst,[status(thm)],[])).
% 0.29/0.51  tff(119,plain,
% 0.29/0.51      ((~![Vqm: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(tptp_fun_Vatm2_222(Vq2, Vatm1, Vqm1), tptp_fun_Vqm2_221(Vq2, Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))) | vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) | (~vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqempty, vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[118, 117])).
% 0.29/0.51  tff(120,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.51      inference(unit_resolution,[status(thm)],[119, 113, 100, 96])).
% 0.29/0.51  tff(121,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[120, 87])).
% 0.29/0.51  tff(122,plain,
% 0.29/0.51      (vqseq(vq1, vq2) = vqseq(vqempty, vq2)),
% 0.29/0.51      inference(symmetry,[status(thm)],[30])).
% 0.29/0.51  tff(123,plain,
% 0.29/0.51      (vqseq(vqempty, Vqr!232) = vqseq(vq1, vq2)),
% 0.29/0.51      inference(monotonicity,[status(thm)],[29, 53])).
% 0.29/0.51  tff(124,plain,
% 0.29/0.51      (vqseq(vqempty, Vqr!232) = vqseq(vqempty, vq2)),
% 0.29/0.51      inference(transitivity,[status(thm)],[123, 122])).
% 0.29/0.51  tff(125,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.51      inference(monotonicity,[status(thm)],[124])).
% 0.29/0.51  tff(126,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.51      inference(symmetry,[status(thm)],[125])).
% 0.29/0.51  tff(127,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.51      inference(monotonicity,[status(thm)],[85, 30])).
% 0.29/0.51  tff(128,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, vq2), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.51      inference(symmetry,[status(thm)],[127])).
% 0.29/0.51  tff(129,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vqseq(vq1, vq2), vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.51      inference(transitivity,[status(thm)],[128, 126])).
% 0.29/0.51  tff(130,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[99, 129])).
% 0.29/0.51  tff(131,plain,
% 0.29/0.51      ((~![Vatm: vATMap, Vqm: vATMap] : vptcheck(vMC(Vatm, Vqm), vqempty, vMC(Vatm, Vqm))) | vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))),
% 0.29/0.51      inference(quant_inst,[status(thm)],[])).
% 0.29/0.51  tff(132,plain,
% 0.29/0.51      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))),
% 0.29/0.51      inference(unit_resolution,[status(thm)],[131, 94])).
% 0.29/0.51  tff(133,plain,
% 0.29/0.51      (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : refl(((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))),
% 0.29/0.51      inference(bind,[status(th)],[])).
% 0.29/0.51  tff(134,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.51      inference(quant_intro,[status(thm)],[133])).
% 0.29/0.51  tff(135,plain,
% 0.29/0.51      (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : trans(monotonicity(trans(monotonicity(rewrite((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) <=> (~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))), ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> (~(~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))))), rewrite((~(~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))), ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))), (((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2)) <=> (((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2)))), rewrite((((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2)) <=> ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))), (((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2)) <=> ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))))),
% 0.29/0.51      inference(bind,[status(th)],[])).
% 0.29/0.51  tff(136,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.51      inference(quant_intro,[status(thm)],[135])).
% 0.29/0.51  tff(137,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2))),
% 0.29/0.51      inference(rewrite,[status(thm)],[])).
% 0.29/0.51  tff(138,plain,
% 0.29/0.51      (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : trans(monotonicity(rewrite(((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) <=> (vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))), ((((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vqmr = Vqm2)) <=> ((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vqmr = Vqm2)))), rewrite(((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vqmr = Vqm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2))), ((((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vqmr = Vqm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2))))),
% 0.29/0.51      inference(bind,[status(th)],[])).
% 0.29/0.51  tff(139,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vqmr = Vqm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2))),
% 0.29/0.51      inference(quant_intro,[status(thm)],[138])).
% 0.29/0.51  tff(140,axiom,(![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vqmr = Vqm2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqseq_inv4'')).
% 0.29/0.51  tff(141,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[140, 139])).
% 0.29/0.51  tff(142,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[141, 137])).
% 0.29/0.51  tff(143,plain,(
% 0.29/0.51      ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vqmr = Vqm2))),
% 0.29/0.51      inference(skolemize,[status(sab)],[142])).
% 0.29/0.51  tff(144,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[143, 136])).
% 0.29/0.51  tff(145,plain,
% 0.29/0.51      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.51      inference(modus_ponens,[status(thm)],[144, 134])).
% 0.29/0.51  tff(146,plain,
% 0.29/0.51      (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(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, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.29/0.51      inference(rewrite,[status(thm)],[])).
% 0.29/0.51  tff(147,plain,
% 0.29/0.51      (((Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.29/0.51      inference(rewrite,[status(thm)],[])).
% 0.29/0.51  tff(148,plain,
% 0.29/0.51      (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(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, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))))),
% 0.29/0.52      inference(monotonicity,[status(thm)],[147])).
% 0.29/0.52  tff(149,plain,
% 0.29/0.52      (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(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, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.29/0.52      inference(transitivity,[status(thm)],[148, 146])).
% 0.29/0.52  tff(150,plain,
% 0.29/0.52      ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.29/0.52      inference(quant_inst,[status(thm)],[])).
% 0.29/0.52  tff(151,plain,
% 0.29/0.52      ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vqmr = Vqm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.29/0.52      inference(modus_ponens,[status(thm)],[150, 149])).
% 0.29/0.52  tff(152,plain,
% 0.29/0.52      ((Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.29/0.52      inference(unit_resolution,[status(thm)],[151, 145, 132, 130])).
% 0.29/0.52  tff(153,plain,
% 0.29/0.52      (Vqtm1!233 = tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))),
% 0.29/0.52      inference(unit_resolution,[status(thm)],[152, 121])).
% 0.29/0.52  tff(154,plain,
% 0.29/0.52      (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : refl(((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))),
% 0.29/0.52      inference(bind,[status(th)],[])).
% 0.29/0.52  tff(155,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.52      inference(quant_intro,[status(thm)],[154])).
% 0.29/0.52  tff(156,plain,
% 0.29/0.52      (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : trans(monotonicity(trans(monotonicity(rewrite((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) <=> (~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))), ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> (~(~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))))), rewrite((~(~((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))), ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) <=> ((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))))), (((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2)) <=> (((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2)))), rewrite((((~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2)) <=> ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))), (((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2)) <=> ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))))),
% 0.29/0.52      inference(bind,[status(th)],[])).
% 0.29/0.52  tff(157,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.52      inference(quant_intro,[status(thm)],[156])).
% 0.29/0.52  tff(158,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2))),
% 0.29/0.52      inference(rewrite,[status(thm)],[])).
% 0.29/0.52  tff(159,plain,
% 0.29/0.52      (^[Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : trans(monotonicity(rewrite(((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) <=> (vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))), ((((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vatmr = Vatm2)) <=> ((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vatmr = Vatm2)))), rewrite(((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vatmr = Vatm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2))), ((((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vatmr = Vatm2)) <=> ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2))))),
% 0.29/0.52      inference(bind,[status(th)],[])).
% 0.29/0.52  tff(160,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vatmr = Vatm2)) <=> ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2))),
% 0.29/0.52      inference(quant_intro,[status(thm)],[159])).
% 0.29/0.52  tff(161,axiom,(![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : (((vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))) => (Vatmr = Vatm2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Tqseq_inv3'')).
% 0.29/0.52  tff(162,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2))),
% 0.29/0.52      inference(modus_ponens,[status(thm)],[161, 160])).
% 0.29/0.52  tff(163,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2))),
% 0.29/0.52      inference(modus_ponens,[status(thm)],[162, 158])).
% 0.29/0.52  tff(164,plain,(
% 0.29/0.52      ![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((~(vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr)) & vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1)) & vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2)))) | (Vatmr = Vatm2))),
% 0.29/0.52      inference(skolemize,[status(sab)],[163])).
% 0.29/0.52  tff(165,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.52      inference(modus_ponens,[status(thm)],[164, 157])).
% 0.29/0.52  tff(166,plain,
% 0.29/0.52      (![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))),
% 0.29/0.52      inference(modus_ponens,[status(thm)],[165, 155])).
% 0.29/0.52  tff(167,plain,
% 0.29/0.52      (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm2_222(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, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.52      inference(rewrite,[status(thm)],[])).
% 0.29/0.52  tff(168,plain,
% 0.29/0.52      (((Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))) <=> ((~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.52      inference(rewrite,[status(thm)],[])).
% 0.29/0.52  tff(169,plain,
% 0.29/0.52      (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(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, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))))),
% 0.29/0.52      inference(monotonicity,[status(thm)],[168])).
% 0.29/0.52  tff(170,plain,
% 0.29/0.52      (((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(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, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.52      inference(transitivity,[status(thm)],[169, 167])).
% 0.29/0.52  tff(171,plain,
% 0.29/0.52      ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | ((Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))))),
% 0.29/0.52      inference(quant_inst,[status(thm)],[])).
% 0.29/0.52  tff(172,plain,
% 0.29/0.52      ((~![Vqm: vATMap, Vatm2: vATMap, Vqm2: vATMap, Vq1: vQuestionnaire, Vatm: vATMap, Vqm1: vATMap, Vatmr: vATMap, Vatm1: vATMap, Vqmr: vATMap, Vq2: vQuestionnaire] : ((Vatmr = Vatm2) | (~vptcheck(vMC(Vatm, Vqm), vqseq(Vq1, Vq2), vMC(Vatmr, Vqmr))) | (~vptcheck(vMC(Vatm, Vqm), Vq1, vMC(Vatm1, Vqm1))) | (~vptcheck(vMC(Vatm1, Vqm1), Vq2, vMC(Vatm2, Vqm2))))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqseq(vqempty, Vqr!232), vMC(Vatm1!229, Vqtm1!233))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), vqempty, vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)))) | (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.29/0.55      inference(modus_ponens,[status(thm)],[171, 170])).
% 0.29/0.55  tff(173,plain,
% 0.29/0.55      ((~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))) | (Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.29/0.55      inference(unit_resolution,[status(thm)],[172, 166, 132, 130])).
% 0.29/0.55  tff(174,plain,
% 0.29/0.55      (Vatm1!229 = tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))),
% 0.29/0.55      inference(unit_resolution,[status(thm)],[173, 121])).
% 0.29/0.55  tff(175,plain,
% 0.29/0.55      (vMC(Vatm1!229, Vqtm1!233) = vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))),
% 0.29/0.55      inference(monotonicity,[status(thm)],[174, 153])).
% 0.29/0.55  tff(176,plain,
% 0.29/0.55      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233)) <=> vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231))))),
% 0.29/0.55      inference(monotonicity,[status(thm)],[85, 53, 175])).
% 0.29/0.55  tff(177,plain,
% 0.29/0.55      (vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!231)), vq2, vMC(tptp_fun_Vatm2_222(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)), tptp_fun_Vqm2_221(vq2, vtypeAM(Vam!228), vtypeQM(Vqm!231)))) <=> vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.55      inference(symmetry,[status(thm)],[176])).
% 0.29/0.55  tff(178,plain,
% 0.29/0.55      (vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.55      inference(modus_ponens,[status(thm)],[120, 177])).
% 0.29/0.55  tff(179,plain,
% 0.29/0.55      (~vptcheck(vMC(vtypeAM(Vamr!230), vtypeQM(Vqmr!227)), Vqr!232, vMC(Vatm1!229, Vqtm1!233))),
% 0.29/0.55      inference(or_elim,[status(thm)],[25])).
% 0.29/0.55  tff(180,plain,
% 0.29/0.55      ($false),
% 0.29/0.55      inference(unit_resolution,[status(thm)],[179, 178])).
% 0.29/0.55  % SZS output end Proof
% 0.29/0.55  % E exiting
%------------------------------------------------------------------------------