%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM267_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:23:05 PM UTC 2026
% Result : Theorem 2.63s 2.81s
% Output : Proof 2.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : COM267_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.08 % Command : run_E %s %d THM
% 0.07/0.27 % Computer : n019.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % WCLimit : 300
% 0.07/0.27 % DateTime : Mon May 4 20:01:15 EDT 2026
% 0.07/0.27 % CPUTime :
% 2.63/2.81 % SZS status Theorem
% 2.63/2.81 % SZS output start Proof
% 2.63/2.81 tff(vsomeQConf_type, type, (
% 2.63/2.81 vsomeQConf: vQConf > vOptQConf)).
% 2.63/2.81 tff(vQC_type, type, (
% 2.63/2.81 vQC: ( vAnsMap * vQMap * vQuestionnaire ) > vQConf)).
% 2.63/2.81 tff(vqempty_type, type, (
% 2.63/2.81 vqempty: vQuestionnaire)).
% 2.63/2.81 tff(vqmbind_type, type, (
% 2.63/2.81 vqmbind: ( vQID * vLabel * vAType * vQMap ) > vQMap)).
% 2.63/2.81 tff(tptp_fun_Vqm_233_type, type, (
% 2.63/2.81 tptp_fun_Vqm_233: vQMap)).
% 2.63/2.81 tff(tptp_fun_Vt_232_type, type, (
% 2.63/2.81 tptp_fun_Vt_232: vAType)).
% 2.63/2.81 tff(tptp_fun_Vl_229_type, type, (
% 2.63/2.81 tptp_fun_Vl_229: vLabel)).
% 2.63/2.81 tff(tptp_fun_Vqid_227_type, type, (
% 2.63/2.81 tptp_fun_Vqid_227: vQID)).
% 2.63/2.81 tff(tptp_fun_Vam_228_type, type, (
% 2.63/2.81 tptp_fun_Vam_228: vAnsMap)).
% 2.63/2.81 tff(vreduce_type, type, (
% 2.63/2.81 vreduce: ( vQuestionnaire * vAnsMap * vQMap ) > vOptQConf)).
% 2.63/2.81 tff(vqsingle_type, type, (
% 2.63/2.81 vqsingle: vEntry > vQuestionnaire)).
% 2.63/2.81 tff(vdefquestion_type, type, (
% 2.63/2.81 vdefquestion: ( vQID * vLabel * vAType ) > vEntry)).
% 2.63/2.81 tff(vptcheck_type, type, (
% 2.63/2.81 vptcheck: ( vMapConf * vQuestionnaire * vMapConf ) > $o)).
% 2.63/2.81 tff(vMC_type, type, (
% 2.63/2.81 vMC: ( vATMap * vATMap ) > vMapConf)).
% 2.63/2.81 tff(tptp_fun_Vqtm2_230_type, type, (
% 2.63/2.81 tptp_fun_Vqtm2_230: vATMap)).
% 2.63/2.81 tff(tptp_fun_Vatm2_231_type, type, (
% 2.63/2.81 tptp_fun_Vatm2_231: vATMap)).
% 2.63/2.81 tff(vtypeQM_type, type, (
% 2.63/2.81 vtypeQM: vQMap > vATMap)).
% 2.63/2.81 tff(vtypeAM_type, type, (
% 2.63/2.81 vtypeAM: vAnsMap > vATMap)).
% 2.63/2.81 tff(visValue_type, type, (
% 2.63/2.81 visValue: vQuestionnaire > $o)).
% 2.63/2.81 tff(1,plain,
% 2.63/2.81 (^[Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : refl((vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty))) <=> (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty))))),
% 2.63/2.81 inference(bind,[status(th)],[])).
% 2.63/2.81 tff(2,plain,
% 2.63/2.81 (![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty))) <=> ![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty)))),
% 2.63/2.81 inference(quant_intro,[status(thm)],[1])).
% 2.63/2.81 tff(3,plain,
% 2.63/2.81 (![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty))) <=> ![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty)))),
% 2.63/2.81 inference(rewrite,[status(thm)],[])).
% 2.63/2.81 tff(4,axiom,(![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''reduce-5'')).
% 2.63/2.81 tff(5,plain,
% 2.63/2.81 (![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty)))),
% 2.63/2.81 inference(modus_ponens,[status(thm)],[4, 3])).
% 2.63/2.81 tff(6,plain,(
% 2.63/2.81 ![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty)))),
% 2.63/2.81 inference(skolemize,[status(sab)],[5])).
% 2.63/2.81 tff(7,plain,
% 2.63/2.81 (![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty)))),
% 2.63/2.81 inference(modus_ponens,[status(thm)],[6, 2])).
% 2.63/2.81 tff(8,plain,
% 2.63/2.81 ((~![Vqm: vQMap, Vt: vAType, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam, vqmbind(Vqid, Vl, Vt, Vqm), vqempty)))) | (vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam!228, vqmbind(Vqid!227, Vl!229, Vt!232, Vqm!233), vqempty)))),
% 2.63/2.81 inference(quant_inst,[status(thm)],[])).
% 2.63/2.81 tff(9,plain,
% 2.63/2.81 (vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam!228, vqmbind(Vqid!227, Vl!229, Vt!232, Vqm!233), vqempty))),
% 2.63/2.81 inference(unit_resolution,[status(thm)],[8, 7])).
% 2.63/2.81 tff(10,plain,
% 2.63/2.81 (^[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : refl((~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000)))) <=> (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000)))))),
% 2.63/2.81 inference(bind,[status(th)],[])).
% 2.63/2.81 tff(11,plain,
% 2.63/2.81 (![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000)))) <=> ![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.81 inference(quant_intro,[status(thm)],[10])).
% 2.63/2.81 tff(12,plain,
% 2.63/2.81 ((((~visValue(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)))) & vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!233)), vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), vMC(Vatm2!231, Vqtm2!230))) & ![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))) <=> ((~visValue(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)))) & vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!233)), vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), vMC(Vatm2!231, Vqtm2!230)) & ![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000)))))),
% 2.63/2.81 inference(rewrite,[status(thm)],[])).
% 2.63/2.81 tff(13,plain,
% 2.63/2.81 ((~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : ((~((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2)))) | ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))) <=> (~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : ((~((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2)))) | ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000)))))),
% 2.63/2.81 inference(rewrite,[status(thm)],[])).
% 2.63/2.81 tff(14,plain,
% 2.63/2.81 ((~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2))) => ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))) <=> (~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : ((~((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2)))) | ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000)))))),
% 2.63/2.81 inference(rewrite,[status(thm)],[])).
% 2.63/2.81 tff(15,axiom,(~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : (((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2))) => ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Progress-qsingle-defquestion'')).
% 2.63/2.83 tff(16,plain,
% 2.63/2.83 (~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : ((~((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2)))) | ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.83 inference(modus_ponens,[status(thm)],[15, 14])).
% 2.63/2.83 tff(17,plain,
% 2.63/2.83 (~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : ((~((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2)))) | ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.83 inference(modus_ponens,[status(thm)],[16, 13])).
% 2.63/2.83 tff(18,plain,
% 2.63/2.83 (~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : ((~((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2)))) | ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.83 inference(modus_ponens,[status(thm)],[17, 13])).
% 2.63/2.83 tff(19,plain,
% 2.63/2.83 (~![Vqm: vQMap, Vt: vAType, Vatm2: vATMap, Vqtm2: vATMap, Vl: vLabel, Vam: vAnsMap, Vqid: vQID] : ((~((~visValue(vqsingle(vdefquestion(Vqid, Vl, Vt)))) & vptcheck(vMC(vtypeAM(Vam), vtypeQM(Vqm)), vqsingle(vdefquestion(Vqid, Vl, Vt)), vMC(Vatm2, Vqtm2)))) | ?[Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (vreduce(vqsingle(vdefquestion(Vqid, Vl, Vt)), Vam, Vqm) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.83 inference(modus_ponens,[status(thm)],[18, 13])).
% 2.63/2.83 tff(20,plain,
% 2.63/2.83 ((~visValue(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)))) & vptcheck(vMC(vtypeAM(Vam!228), vtypeQM(Vqm!233)), vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), vMC(Vatm2!231, Vqtm2!230)) & ![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.83 inference(modus_ponens,[status(thm)],[19, 12])).
% 2.63/2.83 tff(21,plain,
% 2.63/2.83 (![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.83 inference(and_elim,[status(thm)],[20])).
% 2.63/2.83 tff(22,plain,
% 2.63/2.83 (![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))),
% 2.63/2.83 inference(modus_ponens,[status(thm)],[21, 11])).
% 2.63/2.83 tff(23,plain,
% 2.63/2.83 ((~![Vam00000: vAnsMap, Vqm00000: vQMap, Vq00000: vQuestionnaire] : (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam00000, Vqm00000, Vq00000))))) | (~(vreduce(vqsingle(vdefquestion(Vqid!227, Vl!229, Vt!232)), Vam!228, Vqm!233) = vsomeQConf(vQC(Vam!228, vqmbind(Vqid!227, Vl!229, Vt!232, Vqm!233), vqempty))))),
% 2.63/2.83 inference(quant_inst,[status(thm)],[])).
% 2.63/2.83 tff(24,plain,
% 2.63/2.83 ($false),
% 2.63/2.83 inference(unit_resolution,[status(thm)],[23, 22, 9])).
% 2.63/2.83 % SZS output end Proof
% 2.63/2.83 % E exiting
%------------------------------------------------------------------------------