%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : COM271_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:58:15 AM UTC 2026
% Result : Theorem 166.83s 107.83s
% Output : Refutation 167.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 338
% Syntax : Number of formulae : 678 ( 345 unt; 0 typ; 0 def)
% Number of atoms : 2226 (1881 equ; 0 cnn)
% Maximal formula atoms : 100 ( 3 avg)
% Number of connectives : 7270 ( 587 ~; 410 |; 899 &;5135 @)
% ( 0 <=>; 239 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 6 avg)
% Number of types : 27 ( 26 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 104 ( 102 usr; 28 con; 0-4 aty)
% Number of variables : 2486 ( 0 ^;1780 !; 706 ?;2486 :)
% Comments :
%------------------------------------------------------------------------------
thf(vEntry_type,type,
vEntry: $tType ).
thf(vYN_type,type,
vYN: $tType ).
thf(vMapConf_type,type,
vMapConf: $tType ).
thf(vOptAType_type,type,
vOptAType: $tType ).
thf(vATMap_type,type,
vATMap: $tType ).
thf(vQuestionnaire_type,type,
vQuestionnaire: $tType ).
thf(vOptMapConf_type,type,
vOptMapConf: $tType ).
thf(vQConf_type,type,
vQConf: $tType ).
thf(vstring_type,type,
vstring: $tType ).
thf(vchar_type,type,
vchar: $tType ).
thf(vAval_type,type,
vAval: $tType ).
thf(vOptQConf_type,type,
vOptQConf: $tType ).
thf(vOptQuestion_type,type,
vOptQuestion: $tType ).
thf(vAnsMap_type,type,
vAnsMap: $tType ).
thf(vExp_type,type,
vExp: $tType ).
thf(vQMap_type,type,
vQMap: $tType ).
thf(vQID_type,type,
vQID: $tType ).
thf(vLabel_type,type,
vLabel: $tType ).
thf(vOptAval_type,type,
vOptAval: $tType ).
thf(vnat_type,type,
vnat: $tType ).
thf(vOptExp_type,type,
vOptExp: $tType ).
thf(vGID_type,type,
vGID: $tType ).
thf(vATList_type,type,
vATList: $tType ).
thf(vBinOpT_type,type,
vBinOpT: $tType ).
thf(vUnOpT_type,type,
vUnOpT: $tType ).
thf(vAType_type,type,
vAType: $tType ).
thf(vconstant_decl,type,
vconstant: vAval > vExp ).
thf(vqmempty_decl,type,
vqmempty: vQMap ).
thf(vquestion_decl,type,
vquestion: vQID > vLabel > vAType > vEntry ).
thf(vsomeExp_decl,type,
vsomeExp: vExp > vOptExp ).
thf(vsubop_decl,type,
vsubop: vBinOpT ).
thf(vqcond_decl,type,
vqcond: vExp > vQuestionnaire > vQuestionnaire > vQuestionnaire ).
thf(vandop_decl,type,
vandop: vBinOpT ).
thf(vnotop_decl,type,
vnotop: vUnOpT ).
thf(vNum_decl,type,
vNum: vnat > vAval ).
thf(vnoAType_decl,type,
vnoAType: vOptAType ).
thf(vyes_decl,type,
vyes: vYN ).
thf(ve1_decl,type,
ve1: vExp ).
thf(vT_decl,type,
vT: vstring > vAval ).
thf(vNumber_decl,type,
vNumber: vAType ).
thf(vdivop_decl,type,
vdivop: vBinOpT ).
thf(vzero_decl,type,
vzero: vnat ).
thf(vsucc_decl,type,
vsucc: vnat > vnat ).
thf(vabind_decl,type,
vabind: vQID > vAval > vAnsMap > vAnsMap ).
thf(vnoAval_decl,type,
vnoAval: vOptAval ).
thf(vYesNo_decl,type,
vYesNo: vAType ).
thf(vdefquestion_decl,type,
vdefquestion: vQID > vLabel > vAType > vEntry ).
thf(vunop_decl,type,
vunop: vUnOpT > vExp > vExp ).
thf(vaempty_decl,type,
vaempty: vAnsMap ).
thf(vqseq_decl,type,
vqseq: vQuestionnaire > vQuestionnaire > vQuestionnaire ).
thf(vmulop_decl,type,
vmulop: vBinOpT ).
thf(vqempty_decl,type,
vqempty: vQuestionnaire ).
thf(vsomeQConf_decl,type,
vsomeQConf: vQConf > vOptQConf ).
thf(vnoQConf_decl,type,
vnoQConf: vOptQConf ).
thf(vnoExp_decl,type,
vnoExp: vOptExp ).
thf(vbinop_decl,type,
vbinop: vExp > vBinOpT > vExp > vExp ).
thf(vB_decl,type,
vB: vYN > vAval ).
thf(vQC_decl,type,
vQC: vAnsMap > vQMap > vQuestionnaire > vQConf ).
thf(vorop_decl,type,
vorop: vBinOpT ).
thf(veqop_decl,type,
veqop: vBinOpT ).
thf(vText_decl,type,
vText: vAType ).
thf(vsomeAval_decl,type,
vsomeAval: vAval > vOptAval ).
thf(vqsingle_decl,type,
vqsingle: vEntry > vQuestionnaire ).
thf(vMC_decl,type,
vMC: vATMap > vATMap > vMapConf ).
thf(vaddop_decl,type,
vaddop: vBinOpT ).
thf(vsomeQuestion_decl,type,
vsomeQuestion: vQID > vLabel > vAType > vOptQuestion ).
thf(vltop_decl,type,
vltop: vBinOpT ).
thf(vqvar_decl,type,
vqvar: vQID > vExp ).
thf(vatmbind_decl,type,
vatmbind: vQID > vAType > vATMap > vATMap ).
thf(vgtop_decl,type,
vgtop: vBinOpT ).
thf(vqmbind_decl,type,
vqmbind: vQID > vLabel > vAType > vQMap > vQMap ).
thf(vask_decl,type,
vask: vQID > vEntry ).
thf(vsomeAType_decl,type,
vsomeAType: vAType > vOptAType ).
thf(ve2_decl,type,
ve2: vExp ).
thf(vnoQuestion_decl,type,
vnoQuestion: vOptQuestion ).
thf(vqgroup_decl,type,
vqgroup: vGID > vQuestionnaire > vQuestionnaire ).
thf(vatmempty_decl,type,
vatmempty: vATMap ).
thf(vno_decl,type,
vno: vYN ).
thf(vvalue_decl,type,
vvalue: vQID > vAType > vExp > vEntry ).
thf(vgetAnswer_decl,type,
vgetAnswer: vLabel > vAType > vAval ).
thf(vecheck_decl,type,
vecheck: vATMap > vExp > vOptAType ).
thf(vgetAM_decl,type,
vgetAM: vQConf > vAnsMap ).
thf(vaskText_decl,type,
vaskText: vLabel > vstring ).
thf(vminus_decl,type,
vminus: vnat > vnat > vnat ).
thf(vtypeOf_decl,type,
vtypeOf: vAval > vAType ).
thf(vevalBinOp_decl,type,
vevalBinOp: vBinOpT > vAval > vAval > vOptExp ).
thf(vgetQM_decl,type,
vgetQM: vQConf > vQMap ).
thf(vplus_decl,type,
vplus: vnat > vnat > vnat ).
thf(vexpIsValue_decl,type,
vexpIsValue: vExp > $o ).
thf(vaskYesNo_decl,type,
vaskYesNo: vLabel > vYN ).
thf(visValue_decl,type,
visValue: vQuestionnaire > $o ).
thf(vtypeAM_decl,type,
vtypeAM: vAnsMap > vATMap ).
thf(vlookupQMap_decl,type,
vlookupQMap: vQID > vQMap > vOptQuestion ).
thf(vaskNumber_decl,type,
vaskNumber: vLabel > vnat ).
thf(vdivide_decl,type,
vdivide: vnat > vnat > vnat ).
thf(vappendATMap_decl,type,
vappendATMap: vATMap > vATMap > vATMap ).
thf(vor_decl,type,
vor: vYN > vYN > vYN ).
thf(visSomeAType_decl,type,
visSomeAType: vOptAType > $o ).
thf(vpred_decl,type,
vpred: vnat > vnat ).
thf(vlookupATMap_decl,type,
vlookupATMap: vQID > vATMap > vOptAType ).
thf(vqcappend_decl,type,
vqcappend: vQConf > vQuestionnaire > vQConf ).
thf(visSomeQC_decl,type,
visSomeQC: vOptQConf > $o ).
thf(visSomeAval_decl,type,
visSomeAval: vOptAval > $o ).
thf(vgetQuest_decl,type,
vgetQuest: vQConf > vQuestionnaire ).
thf(vevalUnOp_decl,type,
vevalUnOp: vUnOpT > vAval > vOptExp ).
thf(vcheckBinOp_decl,type,
vcheckBinOp: vBinOpT > vAType > vAType > vOptAType ).
thf(vnot_decl,type,
vnot: vYN > vYN ).
thf(vreduce_decl,type,
vreduce: vQuestionnaire > vAnsMap > vQMap > vOptQConf ).
thf(vmultiply_decl,type,
vmultiply: vnat > vnat > vnat ).
thf(vappendAnsMap_decl,type,
vappendAnsMap: vAnsMap > vAnsMap > vAnsMap ).
thf(vcheckUnOp_decl,type,
vcheckUnOp: vUnOpT > vAType > vOptAType ).
thf(vtypeQM_decl,type,
vtypeQM: vQMap > vATMap ).
thf(visSomeExp_decl,type,
visSomeExp: vOptExp > $o ).
thf(vintersectATM_decl,type,
vintersectATM: vATMap > vATMap > vATMap ).
thf(vlt_decl,type,
vlt: vnat > vnat > vYN ).
thf(vgt_decl,type,
vgt: vnat > vnat > vYN ).
thf(vlookupAnsMap_decl,type,
vlookupAnsMap: vQID > vAnsMap > vOptAval ).
thf(vreduceExp_decl,type,
vreduceExp: vExp > vAnsMap > vOptExp ).
thf(vand_decl,type,
vand: vYN > vYN > vYN ).
thf(visSomeQuestion_decl,type,
visSomeQuestion: vOptQuestion > $o ).
thf(vptcheck_decl,type,
vptcheck: vMapConf > vQuestionnaire > vMapConf > $o ).
thf(vgetQuestionLabel_decl,type,
vgetQuestionLabel: vOptQuestion > vLabel ).
thf(vgetAType_decl,type,
vgetAType: vOptAType > vAType ).
thf(vgetQuestionAType_decl,type,
vgetQuestionAType: vOptQuestion > vAType ).
thf(vgetQC_decl,type,
vgetQC: vOptQConf > vQConf ).
thf(vgetExpValue_decl,type,
vgetExpValue: vExp > vAval ).
thf(vgetAval_decl,type,
vgetAval: vOptAval > vAval ).
thf(vgetExp_decl,type,
vgetExp: vOptExp > vExp ).
thf(282,axiom,
( ( vNumber @ ( vNumber @ ( vaddop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-0') ).
thf(5116,plain,
( ( vNumber @ ( vNumber @ ( vaddop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[282]) ).
thf(205,axiom,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( ( ( A @ vgetQuest )
= D )
& ( A
= ( D @ ( C @ ( B @ vQC ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuest-INV') ).
thf(1454,plain,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( ( ( A @ vgetQuest )
= D )
& ( A
= ( D @ ( C @ ( B @ vQC ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[205]) ).
thf(247,axiom,
vandop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-andop-orop') ).
thf(1633,plain,
vandop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[247]) ).
thf(301,axiom,
! [A: vQID,B: vAType,C: vATMap] :
( ( C @ ( B @ ( A @ vatmbind ) ) @ ( A @ vlookupATMap ) )
= ( B @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupATMap-1') ).
thf(5260,plain,
! [A: vQID,B: vAType,C: vATMap] :
( ( C @ ( B @ ( A @ vatmbind ) ) @ ( A @ vlookupATMap ) )
= ( B @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[301]) ).
thf(113,axiom,
! [A: vQID,B: vQID,C: vAType,D: vATMap] :
( ( A != B )
=> ( ( D @ ( C @ ( B @ vatmbind ) ) @ ( A @ vlookupATMap ) )
= ( D @ ( A @ vlookupATMap ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupATMap-2') ).
thf(893,plain,
! [A: vQID,B: vQID,C: vAType,D: vATMap] :
( ( A != B )
=> ( ( D @ ( C @ ( B @ vatmbind ) ) @ ( A @ vlookupATMap ) )
= ( D @ ( A @ vlookupATMap ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(6,axiom,
! [A: vnat] :
( ( A @ vsucc @ vpred )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred-1') ).
thf(365,plain,
! [A: vnat] :
( ( A @ vsucc @ vpred )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(187,axiom,
! [A: vstring,B: vstring] :
( ( ( A @ vT )
= ( B @ vT ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-T') ).
thf(1369,plain,
! [A: vstring,B: vstring] :
( ( ( A @ vT )
= ( B @ vT ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[187]) ).
thf(256,axiom,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vdivop @ vevalBinOp ) ) )
= ( B @ ( A @ vdivide ) @ vNum @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-3') ).
thf(1686,plain,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vdivop @ vevalBinOp ) ) )
= ( B @ ( A @ vdivide ) @ vNum @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[256]) ).
thf(4,axiom,
! [A: vnat] :
( ? [B: vnat] :
( ( ( A @ vpred )
= B )
& ( A
= ( B @ vsucc ) ) )
| ( ( ( A @ vpred )
= vzero )
& ( A = vzero ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred-INV') ).
thf(352,plain,
! [A: vnat] :
( ? [B: vnat] :
( ( ( A @ vpred )
= B )
& ( A
= ( B @ vsucc ) ) )
| ( ( ( A @ vpred )
= vzero )
& ( A = vzero ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(126,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire,D: vQuestionnaire] :
( ( D @ ( C @ ( B @ ( A @ vQC ) ) @ vqcappend ) )
= ( D @ ( C @ vqseq ) @ ( B @ ( A @ vQC ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qcappend-0') ).
thf(977,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire,D: vQuestionnaire] :
( ( D @ ( C @ ( B @ ( A @ vQC ) ) @ vqcappend ) )
= ( D @ ( C @ vqseq ) @ ( B @ ( A @ vQC ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(134,axiom,
veqop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-ltop') ).
thf(1005,plain,
veqop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(57,axiom,
! [A: vMapConf] :
? [B: vATMap,C: vATMap] :
( A
= ( C @ ( B @ vMC ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-MapConf') ).
thf(683,plain,
! [A: vMapConf] :
? [B: vATMap,C: vATMap] :
( A
= ( C @ ( B @ vMC ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(150,axiom,
vaddop != vsubop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-subop') ).
thf(1068,plain,
vaddop != vsubop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(339,axiom,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vltop @ vevalBinOp ) ) )
= ( B @ ( A @ vlt ) @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-5') ).
thf(5644,plain,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vltop @ vevalBinOp ) ) )
= ( B @ ( A @ vlt ) @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[339]) ).
thf(70,axiom,
! [A: vOptExp] :
( ~ ( A @ visSomeExp )
=> ( A = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-false-INV') ).
thf(741,plain,
! [A: vOptExp] :
( ~ ( A @ visSomeExp )
=> ( A = vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(267,axiom,
! [A: vBinOpT,B: vAType,C: vAType] :
( ? [D: vBinOpT,E: vAType,F: vAType] :
( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= vnoAType )
& ( C = F )
& ( B = E )
& ( A = D )
& ( D != veqop )
& ( ( F != vYesNo )
| ( E != vYesNo )
| ( D != vorop ) )
& ( ( F != vYesNo )
| ( E != vYesNo )
| ( D != vandop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vltop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vgtop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vdivop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vmulop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vsubop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vaddop ) ) )
| ? [D: vAType,E: vAType] :
( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = E )
& ( B = D )
& ( A = veqop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vYesNo )
& ( B = vYesNo )
& ( A = vorop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vYesNo )
& ( B = vYesNo )
& ( A = vandop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vltop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vgtop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vdivop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vmulop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vsubop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vaddop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-INV') ).
thf(1728,plain,
! [A: vBinOpT,B: vAType,C: vAType] :
( ? [D: vBinOpT,E: vAType,F: vAType] :
( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= vnoAType )
& ( C = F )
& ( B = E )
& ( A = D )
& ( D != veqop )
& ( ( F != vYesNo )
| ( E != vYesNo )
| ( D != vorop ) )
& ( ( F != vYesNo )
| ( E != vYesNo )
| ( D != vandop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vltop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vgtop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vdivop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vmulop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vsubop ) )
& ( ( F != vNumber )
| ( E != vNumber )
| ( D != vaddop ) ) )
| ? [D: vAType,E: vAType] :
( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = E )
& ( B = D )
& ( A = veqop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vYesNo )
& ( B = vYesNo )
& ( A = vorop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vYesNo )
& ( B = vYesNo )
& ( A = vandop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vltop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vgtop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vdivop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vmulop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vsubop ) )
| ( ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) )
& ( C = vNumber )
& ( B = vNumber )
& ( A = vaddop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[267]) ).
thf(106,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vGID,F: vATMap] :
( ( D @ ( F @ vMC ) @ ( B @ ( E @ vqgroup ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqgroup_inv') ).
thf(873,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vGID,F: vATMap] :
( ( D @ ( F @ vMC ) @ ( B @ ( E @ vqgroup ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(10,axiom,
! [A: vOptAval] :
( ? [B: vAval] :
( A
= ( B @ vsomeAval ) )
| ( A = vnoAval ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptAval') ).
thf(379,plain,
! [A: vOptAval] :
( ? [B: vAval] :
( A
= ( B @ vsomeAval ) )
| ( A = vnoAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(223,axiom,
! [A: vYN,B: vYN] :
( ( ( B != vno )
| ( A != vno ) )
=> ( ( B @ ( A @ vor ) )
= vyes ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','or-1') ).
thf(1533,plain,
! [A: vYN,B: vYN] :
( ( ( B != vno )
| ( A != vno ) )
=> ( ( B @ ( A @ vor ) )
= vyes ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[223]) ).
thf(303,axiom,
! [A: vYN,B: vYN] :
( ( B @ vB @ ( A @ vB @ ( vandop @ vevalBinOp ) ) )
= ( B @ ( A @ vand ) @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-6') ).
thf(5383,plain,
! [A: vYN,B: vYN] :
( ( B @ vB @ ( A @ vB @ ( vandop @ vevalBinOp ) ) )
= ( B @ ( A @ vand ) @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[303]) ).
thf(334,axiom,
! [A: vATMap,B: vnat] :
( ( B @ vNum @ vconstant @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-1') ).
thf(5614,plain,
! [A: vATMap,B: vnat] :
( ( B @ vNum @ vconstant @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[334]) ).
thf(203,axiom,
veqop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-orop') ).
thf(1437,plain,
veqop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[203]) ).
thf(145,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C
= ( A @ ( D @ ( G @ vatmbind ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tdefquestion_inv3') ).
thf(1041,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C
= ( A @ ( D @ ( G @ vatmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(37,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vATMap,G: vATMap,H: vQuestionnaire] :
( ( ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( G @ ( E @ vMC ) @ ( H @ ( B @ vqseq ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) )
=> ? [I: vATMap,J: vATMap] : ( J @ ( I @ vMC ) @ ( H @ ( D @ ( F @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqseq_inv2') ).
thf(582,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vATMap,G: vATMap,H: vQuestionnaire] :
( ( ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( G @ ( E @ vMC ) @ ( H @ ( B @ vqseq ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) )
=> ? [I: vATMap,J: vATMap] : ( J @ ( I @ vMC ) @ ( H @ ( D @ ( F @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(76,axiom,
! [A: vAnsMap,B: vQMap] :
( ( B @ ( A @ ( vqempty @ vreduce ) ) )
= vnoQConf ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-0') ).
thf(762,plain,
! [A: vAnsMap,B: vQMap] :
( ( B @ ( A @ ( vqempty @ vreduce ) ) )
= vnoQConf ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(258,axiom,
! [A: vExp,B: vExp,C: vAnsMap,D: vBinOpT] :
( ( ( C @ ( B @ vreduceExp ) @ visSomeExp )
& ~ ( B @ vexpIsValue )
& ( A @ vexpIsValue ) )
=> ( ( C @ ( B @ ( D @ ( A @ vbinop ) ) @ vreduceExp ) )
= ( C @ ( B @ vreduceExp ) @ vgetExp @ ( D @ ( A @ vbinop ) ) @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-4') ).
thf(1692,plain,
! [A: vExp,B: vExp,C: vAnsMap,D: vBinOpT] :
( ( ( C @ ( B @ vreduceExp ) @ visSomeExp )
& ~ ( B @ vexpIsValue )
& ( A @ vexpIsValue ) )
=> ( ( C @ ( B @ ( D @ ( A @ vbinop ) ) @ vreduceExp ) )
= ( C @ ( B @ vreduceExp ) @ vgetExp @ ( D @ ( A @ vbinop ) ) @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[258]) ).
thf(313,axiom,
! [A: vExp] : ( A @ vsomeExp @ visSomeExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-1') ).
thf(5529,plain,
! [A: vExp] : ( A @ vsomeExp @ visSomeExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[313]) ).
thf(162,axiom,
! [A: vAval] :
( ( A @ vsomeAval @ vgetAval )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAval-0') ).
thf(1173,plain,
! [A: vAval] :
( ( A @ vsomeAval @ vgetAval )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[162]) ).
thf(212,axiom,
vmulop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-ltop') ).
thf(1486,plain,
vmulop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[212]) ).
thf(284,axiom,
! [A: vExp,B: vAnsMap,C: vUnOpT] :
( ( ~ ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( A @ ( C @ vunop ) @ vreduceExp ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-10') ).
thf(5120,plain,
! [A: vExp,B: vAnsMap,C: vUnOpT] :
( ( ~ ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( A @ ( C @ vunop ) @ vreduceExp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[284]) ).
thf(251,axiom,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vaddop @ vevalBinOp ) ) )
= ( B @ ( A @ vplus ) @ vNum @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-0') ).
thf(1671,plain,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vaddop @ vevalBinOp ) ) )
= ( B @ ( A @ vplus ) @ vNum @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[251]) ).
thf(239,axiom,
vdivop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-gtop') ).
thf(1608,plain,
vdivop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[239]) ).
thf(12,axiom,
! [A: vQID] :
( ( vqmempty @ ( A @ vlookupQMap ) )
= vnoQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupQMap-0') ).
thf(384,plain,
! [A: vQID] :
( ( vqmempty @ ( A @ vlookupQMap ) )
= vnoQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(326,axiom,
! [A: vAnsMap,B: vBinOpT,C: vAType,D: vExp] :
( ( ( ( A @ ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ vreduceExp ) )
= ( D @ vsomeExp ) )
& ( ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ve1 @ vexpIsValue )
& ~ ( ve2 @ vexpIsValue )
& ( A @ ( ve2 @ vreduceExp ) @ visSomeExp ) )
=> ( ( D @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExpPreservation-binop-expIsValue-True-expIsValue-False-isSomeExp-True') ).
thf(5589,plain,
! [A: vAnsMap,B: vBinOpT,C: vAType,D: vExp] :
( ( ( ( A @ ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ vreduceExp ) )
= ( D @ vsomeExp ) )
& ( ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ve1 @ vexpIsValue )
& ~ ( ve2 @ vexpIsValue )
& ( A @ ( ve2 @ vreduceExp ) @ visSomeExp ) )
=> ( ( D @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[326]) ).
thf(274,axiom,
! [A: vExp,B: vAnsMap,C: vBinOpT,D: vExp] :
( ( ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( D @ ( C @ ( A @ vbinop ) ) @ vreduceExp ) )
= ( D @ ( C @ ( B @ ( A @ vreduceExp ) @ vgetExp @ vbinop ) ) @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-6') ).
thf(1867,plain,
! [A: vExp,B: vAnsMap,C: vBinOpT,D: vExp] :
( ( ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( D @ ( C @ ( A @ vbinop ) ) @ vreduceExp ) )
= ( D @ ( C @ ( B @ ( A @ vreduceExp ) @ vgetExp @ vbinop ) ) @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[274]) ).
thf(60,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( F @ ( B @ vqseq ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ? [G: vATMap,H: vATMap] : ( H @ ( G @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqseq_inv1') ).
thf(698,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( F @ ( B @ vqseq ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ? [G: vATMap,H: vATMap] : ( H @ ( G @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(1,conjecture,
! [A: vAnsMap,B: vBinOpT,C: vAType,D: vExp] :
( ( ( ( A @ ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ vreduceExp ) )
= ( D @ vsomeExp ) )
& ( ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ve1 @ vexpIsValue )
& ~ ( ve2 @ vexpIsValue ) )
=> ( ( D @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExpPreservation-binop-expIsValue-True-expIsValue-False') ).
thf(2,negated_conjecture,
~ ! [A: vAnsMap,B: vBinOpT,C: vAType,D: vExp] :
( ( ( ( A @ ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ vreduceExp ) )
= ( D @ vsomeExp ) )
& ( ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ve1 @ vexpIsValue )
& ~ ( ve2 @ vexpIsValue ) )
=> ( ( D @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(340,plain,
~ ! [A: vAnsMap,B: vBinOpT,C: vAType,D: vExp] :
( ( ( ( A @ ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ vreduceExp ) )
= ( D @ vsomeExp ) )
& ( ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ve1 @ vexpIsValue )
& ~ ( ve2 @ vexpIsValue ) )
=> ( ( D @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(300,axiom,
! [A: vATMap,B: vExp] :
( ? [C: vUnOpT,D: vExp,E: vOptAType,F: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= vnoAType )
& ( B
= ( D @ ( C @ vunop ) ) )
& ( A = F )
& ~ ( E @ visSomeAType )
& ( E
= ( D @ ( F @ vecheck ) ) ) )
| ? [C: vUnOpT,D: vExp,E: vOptAType,F: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( E @ vgetAType @ ( C @ vcheckUnOp ) ) )
& ( B
= ( D @ ( C @ vunop ) ) )
& ( A = F )
& ( E @ visSomeAType )
& ( E
= ( D @ ( F @ vecheck ) ) ) )
| ? [C: vATMap,D: vOptAType,E: vExp,F: vOptAType,G: vExp,H: vBinOpT] :
( ( ( B @ ( A @ vecheck ) )
= vnoAType )
& ( B
= ( G @ ( H @ ( E @ vbinop ) ) ) )
& ( A = C )
& ~ ( ( F @ visSomeAType )
& ( D @ visSomeAType ) )
& ( F
= ( G @ ( C @ vecheck ) ) )
& ( D
= ( E @ ( C @ vecheck ) ) ) )
| ? [C: vATMap,D: vOptAType,E: vExp,F: vOptAType,G: vExp,H: vBinOpT] :
( ( ( B @ ( A @ vecheck ) )
= ( F @ vgetAType @ ( D @ vgetAType @ ( H @ vcheckBinOp ) ) ) )
& ( B
= ( G @ ( H @ ( E @ vbinop ) ) ) )
& ( A = C )
& ( F @ visSomeAType )
& ( D @ visSomeAType )
& ( F
= ( G @ ( C @ vecheck ) ) )
& ( D
= ( E @ ( C @ vecheck ) ) ) )
| ? [C: vQID,D: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( D @ ( C @ vlookupATMap ) ) )
& ( B
= ( C @ vqvar ) )
& ( A = D ) )
| ? [C: vstring,D: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) )
& ( B
= ( C @ vT @ vconstant ) )
& ( A = D ) )
| ? [C: vnat,D: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) )
& ( B
= ( C @ vNum @ vconstant ) )
& ( A = D ) )
| ? [C: vATMap,D: vYN] :
( ( ( B @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) )
& ( B
= ( D @ vB @ vconstant ) )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-INV') ).
thf(5192,plain,
! [A: vATMap,B: vExp] :
( ? [C: vUnOpT,D: vExp,E: vOptAType,F: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= vnoAType )
& ( B
= ( D @ ( C @ vunop ) ) )
& ( A = F )
& ~ ( E @ visSomeAType )
& ( E
= ( D @ ( F @ vecheck ) ) ) )
| ? [C: vUnOpT,D: vExp,E: vOptAType,F: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( E @ vgetAType @ ( C @ vcheckUnOp ) ) )
& ( B
= ( D @ ( C @ vunop ) ) )
& ( A = F )
& ( E @ visSomeAType )
& ( E
= ( D @ ( F @ vecheck ) ) ) )
| ? [C: vATMap,D: vOptAType,E: vExp,F: vOptAType,G: vExp,H: vBinOpT] :
( ( ( B @ ( A @ vecheck ) )
= vnoAType )
& ( B
= ( G @ ( H @ ( E @ vbinop ) ) ) )
& ( A = C )
& ~ ( ( F @ visSomeAType )
& ( D @ visSomeAType ) )
& ( F
= ( G @ ( C @ vecheck ) ) )
& ( D
= ( E @ ( C @ vecheck ) ) ) )
| ? [C: vATMap,D: vOptAType,E: vExp,F: vOptAType,G: vExp,H: vBinOpT] :
( ( ( B @ ( A @ vecheck ) )
= ( F @ vgetAType @ ( D @ vgetAType @ ( H @ vcheckBinOp ) ) ) )
& ( B
= ( G @ ( H @ ( E @ vbinop ) ) ) )
& ( A = C )
& ( F @ visSomeAType )
& ( D @ visSomeAType )
& ( F
= ( G @ ( C @ vecheck ) ) )
& ( D
= ( E @ ( C @ vecheck ) ) ) )
| ? [C: vQID,D: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( D @ ( C @ vlookupATMap ) ) )
& ( B
= ( C @ vqvar ) )
& ( A = D ) )
| ? [C: vstring,D: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) )
& ( B
= ( C @ vT @ vconstant ) )
& ( A = D ) )
| ? [C: vnat,D: vATMap] :
( ( ( B @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) )
& ( B
= ( C @ vNum @ vconstant ) )
& ( A = D ) )
| ? [C: vATMap,D: vYN] :
( ( ( B @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) )
& ( B
= ( D @ vB @ vconstant ) )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[300]) ).
thf(294,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( G @ ( B @ vecheck ) )
= ( D @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tvalue_inv2') ).
thf(5161,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( G @ ( B @ vecheck ) )
= ( D @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[294]) ).
thf(72,axiom,
! [A: vYN,B: vYN] :
( ( ( B != vyes )
| ( A != vyes ) )
=> ( ( B @ ( A @ vand ) )
= vno ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and-1') ).
thf(747,plain,
! [A: vYN,B: vYN] :
( ( ( B != vyes )
| ( A != vyes ) )
=> ( ( B @ ( A @ vand ) )
= vno ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(15,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( ( C @ ( F @ ( D @ vsomeQuestion ) ) )
= ( E @ ( B @ ( A @ vsomeQuestion ) ) ) )
=> ( ( C = E )
& ( F = B )
& ( D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someQuestion') ).
thf(417,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( ( C @ ( F @ ( D @ vsomeQuestion ) ) )
= ( E @ ( B @ ( A @ vsomeQuestion ) ) ) )
=> ( ( C = E )
& ( F = B )
& ( D = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(110,axiom,
vqempty @ visValue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-0') ).
thf(885,plain,
vqempty @ visValue,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(241,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( B @ ( F @ vlookupATMap ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tvalue_inv1') ).
thf(1613,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( B @ ( F @ vlookupATMap ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[241]) ).
thf(192,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQID] :
( ( C @ ( B @ ( A @ vquestion ) ) )
!= ( D @ vask ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-question-ask') ).
thf(1386,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID] :
( ( C @ ( B @ ( A @ vquestion ) ) )
!= ( D @ vask ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[192]) ).
thf(186,axiom,
vaddop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-gtop') ).
thf(1366,plain,
vaddop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[186]) ).
thf(244,axiom,
vdivop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-andop') ).
thf(1623,plain,
vdivop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[244]) ).
thf(336,axiom,
! [A: vOptExp] :
( ( A @ visSomeExp )
=> ? [B: vExp] :
( A
= ( B @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-true-INV') ).
thf(5621,plain,
! [A: vOptExp] :
( ( A @ visSomeExp )
=> ? [B: vExp] :
( A
= ( B @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[336]) ).
thf(261,axiom,
! [A: vQID,B: vAnsMap] :
( ~ ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-2') ).
thf(1709,plain,
! [A: vQID,B: vAnsMap] :
( ~ ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[261]) ).
thf(201,axiom,
! [A: vATMap] :
( ( A @ ( vatmempty @ vappendATMap ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendATMap-0') ).
thf(1430,plain,
! [A: vATMap] :
( ( A @ ( vatmempty @ vappendATMap ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[201]) ).
thf(299,axiom,
! [A: vAval,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vconstant )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-constant-binop') ).
thf(5188,plain,
! [A: vAval,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vconstant )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[299]) ).
thf(95,axiom,
! [A: vAval,B: vQID] :
( ( A @ vconstant )
!= ( B @ vqvar ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-constant-qvar') ).
thf(838,plain,
! [A: vAval,B: vQID] :
( ( A @ vconstant )
!= ( B @ vqvar ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(219,axiom,
veqop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-andop') ).
thf(1511,plain,
veqop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[219]) ).
thf(176,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( J @ ( F @ ( H @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( J @ ( D @ vqseq ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( I = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqseq_inv4') ).
thf(1279,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( J @ ( F @ ( H @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( J @ ( D @ vqseq ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( I = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[176]) ).
thf(232,axiom,
~ ( vnoQConf @ visSomeQC ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-0') ).
thf(1577,plain,
~ ( vnoQConf @ visSomeQC ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[232]) ).
thf(297,axiom,
! [A: vOptAType] :
( ? [B: vAType] :
( A
= ( B @ vsomeAType ) )
| ( A = vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptAType') ).
thf(5182,plain,
! [A: vOptAType] :
( ? [B: vAType] :
( A
= ( B @ vsomeAType ) )
| ( A = vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[297]) ).
thf(26,axiom,
vYesNo != vText,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-YesNo-Text') ).
thf(504,plain,
vYesNo != vText,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(275,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( ( D @ ( E @ vMC ) @ ( G @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( D @ ( E @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( ( F @ ( C @ vecheck ) )
= ( vYesNo @ vsomeAType ) ) )
=> ( D @ ( E @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond') ).
thf(1871,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( ( D @ ( E @ vMC ) @ ( G @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( D @ ( E @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( ( F @ ( C @ vecheck ) )
= ( vYesNo @ vsomeAType ) ) )
=> ( D @ ( E @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[275]) ).
thf(226,axiom,
! [A: vEntry] :
( ? [B: vQID] :
( A
= ( B @ vask ) )
| ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vdefquestion ) ) ) )
| ? [B: vQID,C: vAType,D: vExp] :
( A
= ( D @ ( C @ ( B @ vvalue ) ) ) )
| ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vquestion ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-Entry') ).
thf(1545,plain,
! [A: vEntry] :
( ? [B: vQID] :
( A
= ( B @ vask ) )
| ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vdefquestion ) ) ) )
| ? [B: vQID,C: vAType,D: vExp] :
( A
= ( D @ ( C @ ( B @ vvalue ) ) ) )
| ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vquestion ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[226]) ).
thf(50,axiom,
! [A: vnat] :
( ( A @ ( vzero @ vgt ) )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt-0') ).
thf(638,plain,
! [A: vnat] :
( ( A @ ( vzero @ vgt ) )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(190,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vATMap,G: vATMap,H: vExp,I: vQuestionnaire] :
( ( ( D @ ( F @ vMC ) @ ( I @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( G @ ( E @ vMC ) @ ( I @ ( B @ ( H @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) )
=> ( E = F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond_inv6') ).
thf(1379,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vATMap,G: vATMap,H: vExp,I: vQuestionnaire] :
( ( ( D @ ( F @ vMC ) @ ( I @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( G @ ( E @ vMC ) @ ( I @ ( B @ ( H @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) )
=> ( E = F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[190]) ).
thf(220,axiom,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( ( ( A @ vgetAM )
= B )
& ( A
= ( D @ ( C @ ( B @ vQC ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAM-INV') ).
thf(1514,plain,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( ( ( A @ vgetAM )
= B )
& ( A
= ( D @ ( C @ ( B @ vQC ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[220]) ).
thf(280,axiom,
! [A: vExp] :
( ( A @ vexpIsValue )
=> ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-true-INV') ).
thf(1890,plain,
! [A: vExp] :
( ( A @ vexpIsValue )
=> ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[280]) ).
thf(331,axiom,
! [A: vATMap,B: vExp,C: vUnOpT] :
( ( B @ ( A @ vecheck ) @ visSomeAType )
=> ( ( B @ ( C @ vunop ) @ ( A @ vecheck ) )
= ( B @ ( A @ vecheck ) @ vgetAType @ ( C @ vcheckUnOp ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-6') ).
thf(5604,plain,
! [A: vATMap,B: vExp,C: vUnOpT] :
( ( B @ ( A @ vecheck ) @ visSomeAType )
=> ( ( B @ ( C @ vunop ) @ ( A @ vecheck ) )
= ( B @ ( A @ vecheck ) @ vgetAType @ ( C @ vcheckUnOp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[331]) ).
thf(109,axiom,
! [A: vQID,B: vQMap,C: vAnsMap] :
( ( B @ ( A @ vlookupQMap ) @ visSomeQuestion )
=> ( ( B @ ( C @ ( A @ vask @ vqsingle @ vreduce ) ) )
= ( B @ ( A @ vlookupQMap ) @ vgetQuestionAType @ ( B @ ( A @ vlookupQMap ) @ vgetQuestionLabel @ ( A @ vquestion ) ) @ vqsingle @ ( B @ ( C @ vQC ) ) @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-6') ).
thf(881,plain,
! [A: vQID,B: vQMap,C: vAnsMap] :
( ( B @ ( A @ vlookupQMap ) @ visSomeQuestion )
=> ( ( B @ ( C @ ( A @ vask @ vqsingle @ vreduce ) ) )
= ( B @ ( A @ vlookupQMap ) @ vgetQuestionAType @ ( B @ ( A @ vlookupQMap ) @ vgetQuestionLabel @ ( A @ vquestion ) ) @ vqsingle @ ( B @ ( C @ vQC ) ) @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(335,axiom,
! [A: vExp,B: vAnsMap,C: vUnOpT] :
( ( ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( A @ ( C @ vunop ) @ vreduceExp ) )
= ( B @ ( A @ vreduceExp ) @ vgetExp @ ( C @ vunop ) @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-9') ).
thf(5617,plain,
! [A: vExp,B: vAnsMap,C: vUnOpT] :
( ( ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( A @ ( C @ vunop ) @ vreduceExp ) )
= ( B @ ( A @ vreduceExp ) @ vgetExp @ ( C @ vunop ) @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[335]) ).
thf(213,axiom,
! [A: vBinOpT] :
( ( A = vorop )
| ( A = vandop )
| ( A = vltop )
| ( A = vgtop )
| ( A = veqop )
| ( A = vdivop )
| ( A = vmulop )
| ( A = vsubop )
| ( A = vaddop ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-BinOpT') ).
thf(1489,plain,
! [A: vBinOpT] :
( ( A = vorop )
| ( A = vandop )
| ( A = vltop )
| ( A = vgtop )
| ( A = veqop )
| ( A = vdivop )
| ( A = vmulop )
| ( A = vsubop )
| ( A = vaddop ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[213]) ).
thf(312,axiom,
! [A: vQMap,B: vAType,C: vAnsMap,D: vQID,E: vExp] :
( ( ( C @ ( E @ vreduceExp ) @ visSomeExp )
& ~ ( E @ vexpIsValue ) )
=> ( ( A @ ( C @ ( E @ ( B @ ( D @ vvalue ) ) @ vqsingle @ vreduce ) ) )
= ( C @ ( E @ vreduceExp ) @ vgetExp @ ( B @ ( D @ vvalue ) ) @ vqsingle @ ( A @ ( C @ vQC ) ) @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-3') ).
thf(5526,plain,
! [A: vQMap,B: vAType,C: vAnsMap,D: vQID,E: vExp] :
( ( ( C @ ( E @ vreduceExp ) @ visSomeExp )
& ~ ( E @ vexpIsValue ) )
=> ( ( A @ ( C @ ( E @ ( B @ ( D @ vvalue ) ) @ vqsingle @ vreduce ) ) )
= ( C @ ( E @ vreduceExp ) @ vgetExp @ ( B @ ( D @ vvalue ) ) @ vqsingle @ ( A @ ( C @ vQC ) ) @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[312]) ).
thf(329,axiom,
! [A: vQMap,B: vAType,C: vAnsMap,D: vQID,E: vExp] :
( ( ~ ( C @ ( E @ vreduceExp ) @ visSomeExp )
& ~ ( E @ vexpIsValue ) )
=> ( ( A @ ( C @ ( E @ ( B @ ( D @ vvalue ) ) @ vqsingle @ vreduce ) ) )
= vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-4') ).
thf(5597,plain,
! [A: vQMap,B: vAType,C: vAnsMap,D: vQID,E: vExp] :
( ( ~ ( C @ ( E @ vreduceExp ) @ visSomeExp )
& ~ ( E @ vexpIsValue ) )
=> ( ( A @ ( C @ ( E @ ( B @ ( D @ vvalue ) ) @ vqsingle @ vreduce ) ) )
= vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[329]) ).
thf(9,axiom,
! [A: vOptQuestion] :
( ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vsomeQuestion ) ) ) )
| ( A = vnoQuestion ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptQuestion') ).
thf(376,plain,
! [A: vOptQuestion] :
( ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vsomeQuestion ) ) ) )
| ( A = vnoQuestion ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(53,axiom,
vgtop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-gtop-ltop') ).
thf(646,plain,
vgtop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(29,axiom,
! [A: vQMap,B: vAnsMap,C: vQuestionnaire,D: vAnsMap,E: vQuestionnaire,F: vQMap] :
( ( ( E @ ( A @ ( D @ vQC ) ) )
= ( C @ ( F @ ( B @ vQC ) ) ) )
=> ( ( E = C )
& ( A = F )
& ( D = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-QC') ).
thf(514,plain,
! [A: vQMap,B: vAnsMap,C: vQuestionnaire,D: vAnsMap,E: vQuestionnaire,F: vQMap] :
( ( ( E @ ( A @ ( D @ vQC ) ) )
= ( C @ ( F @ ( B @ vQC ) ) ) )
=> ( ( E = C )
& ( A = F )
& ( D = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(191,axiom,
! [A: vQuestionnaire] :
( ( A @ visValue )
=> ( A = vqempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-true-INV') ).
thf(1383,plain,
! [A: vQuestionnaire] :
( ( A @ visValue )
=> ( A = vqempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[191]) ).
thf(177,axiom,
! [A: vQMap,B: vQID,C: vLabel,D: vAType,E: vQID,F: vAType,G: vQMap,H: vLabel] :
( ( ( A @ ( D @ ( H @ ( E @ vqmbind ) ) ) )
= ( G @ ( F @ ( C @ ( B @ vqmbind ) ) ) ) )
=> ( ( A = G )
& ( D = F )
& ( H = C )
& ( E = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qmbind') ).
thf(1283,plain,
! [A: vQMap,B: vQID,C: vLabel,D: vAType,E: vQID,F: vAType,G: vQMap,H: vLabel] :
( ( ( A @ ( D @ ( H @ ( E @ vqmbind ) ) ) )
= ( G @ ( F @ ( C @ ( B @ vqmbind ) ) ) ) )
=> ( ( A = G )
& ( D = F )
& ( H = C )
& ( E = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[177]) ).
thf(24,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( F
= ( B @ ( D @ ( G @ vatmbind ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tquestion_inv2') ).
thf(480,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( F
= ( B @ ( D @ ( G @ vatmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(108,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( vqmempty
!= ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qmempty-qmbind') ).
thf(877,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( vqmempty
!= ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(104,axiom,
! [A: vQID] :
( ( vatmempty @ ( A @ vlookupATMap ) )
= vnoAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupATMap-0') ).
thf(866,plain,
! [A: vQID] :
( ( vatmempty @ ( A @ vlookupATMap ) )
= vnoAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(132,axiom,
! [A: vEntry,B: vGID,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qsingle-qgroup') ).
thf(998,plain,
! [A: vEntry,B: vGID,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(202,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vATMap,G: vATMap,H: vExp,I: vQuestionnaire] :
( ( ( D @ ( F @ vMC ) @ ( I @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( G @ ( E @ vMC ) @ ( I @ ( B @ ( H @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) )
=> ( G = D ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond_inv7') ).
thf(1433,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vATMap,G: vATMap,H: vExp,I: vQuestionnaire] :
( ( ( D @ ( F @ vMC ) @ ( I @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
& ( G @ ( E @ vMC ) @ ( I @ ( B @ ( H @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) )
=> ( G = D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[202]) ).
thf(221,axiom,
! [A: vUnOpT,B: vExp,C: vUnOpT,D: vExp] :
( ( ( B @ ( A @ vunop ) )
= ( D @ ( C @ vunop ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-unop') ).
thf(1521,plain,
! [A: vUnOpT,B: vExp,C: vUnOpT,D: vExp] :
( ( ( B @ ( A @ vunop ) )
= ( D @ ( C @ vunop ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[221]) ).
thf(27,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vminus ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','minus-0') ).
thf(507,plain,
! [A: vnat] :
( ( vzero @ ( A @ vminus ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(259,axiom,
! [A: vAnsMap] :
( ? [B: vQID,C: vAval,D: vAnsMap] :
( ( ( A @ vtypeAM )
= ( D @ vtypeAM @ ( C @ vtypeOf @ ( B @ vatmbind ) ) ) )
& ( A
= ( D @ ( C @ ( B @ vabind ) ) ) ) )
| ( ( ( A @ vtypeAM )
= vatmempty )
& ( A = vaempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeAM-INV') ).
thf(1696,plain,
! [A: vAnsMap] :
( ? [B: vQID,C: vAval,D: vAnsMap] :
( ( ( A @ vtypeAM )
= ( D @ vtypeAM @ ( C @ vtypeOf @ ( B @ vatmbind ) ) ) )
& ( A
= ( D @ ( C @ ( B @ vabind ) ) ) ) )
| ( ( ( A @ vtypeAM )
= vatmempty )
& ( A = vaempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[259]) ).
thf(273,axiom,
! [A: vExp] :
( vnoExp
!= ( A @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noExp-someExp') ).
thf(1863,plain,
! [A: vExp] :
( vnoExp
!= ( A @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[273]) ).
thf(238,axiom,
! [A: vEntry,B: vExp,C: vQuestionnaire,D: vQuestionnaire] :
( ( A @ vqsingle )
!= ( D @ ( C @ ( B @ vqcond ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qsingle-qcond') ).
thf(1604,plain,
! [A: vEntry,B: vExp,C: vQuestionnaire,D: vQuestionnaire] :
( ( A @ vqsingle )
!= ( D @ ( C @ ( B @ vqcond ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[238]) ).
thf(168,axiom,
! [A: vQID,B: vQID,C: vAval,D: vAnsMap] :
( ( A != B )
=> ( ( D @ ( C @ ( B @ vabind ) ) @ ( A @ vlookupAnsMap ) )
= ( D @ ( A @ vlookupAnsMap ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupAnsMap-2') ).
thf(1199,plain,
! [A: vQID,B: vQID,C: vAval,D: vAnsMap] :
( ( A != B )
=> ( ( D @ ( C @ ( B @ vabind ) ) @ ( A @ vlookupAnsMap ) )
= ( D @ ( A @ vlookupAnsMap ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[168]) ).
thf(289,axiom,
( ( vYesNo @ ( vYesNo @ ( vandop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-6') ).
thf(5142,plain,
( ( vYesNo @ ( vYesNo @ ( vandop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[289]) ).
thf(32,axiom,
! [A: vQID,B: vExp,C: vAType,D: vQID,E: vAType,F: vExp] :
( ( ( F @ ( C @ ( D @ vvalue ) ) )
= ( B @ ( E @ ( A @ vvalue ) ) ) )
=> ( ( F = B )
& ( C = E )
& ( D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-value') ).
thf(534,plain,
! [A: vQID,B: vExp,C: vAType,D: vQID,E: vAType,F: vExp] :
( ( ( F @ ( C @ ( D @ vvalue ) ) )
= ( B @ ( E @ ( A @ vvalue ) ) ) )
=> ( ( F = B )
& ( C = E )
& ( D = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(317,axiom,
! [A: vExp,B: vExp,C: vAnsMap,D: vBinOpT] :
( ( ~ ( C @ ( B @ vreduceExp ) @ visSomeExp )
& ~ ( B @ vexpIsValue )
& ( A @ vexpIsValue ) )
=> ( ( C @ ( B @ ( D @ ( A @ vbinop ) ) @ vreduceExp ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-5') ).
thf(5540,plain,
! [A: vExp,B: vExp,C: vAnsMap,D: vBinOpT] :
( ( ~ ( C @ ( B @ vreduceExp ) @ visSomeExp )
& ~ ( B @ vexpIsValue )
& ( A @ vexpIsValue ) )
=> ( ( C @ ( B @ ( D @ ( A @ vbinop ) ) @ vreduceExp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[317]) ).
thf(248,axiom,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vdivide ) )
= vzero )
& ( B = D )
& ( A = C )
& ( ( D @ ( C @ vgt ) )
!= vyes ) )
| ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vdivide ) )
= ( D @ ( D @ ( C @ vminus ) @ vdivide ) @ vsucc ) )
& ( B = D )
& ( A = C )
& ( ( D @ ( C @ vgt ) )
= vyes ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','divide-INV') ).
thf(1636,plain,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vdivide ) )
= vzero )
& ( B = D )
& ( A = C )
& ( ( D @ ( C @ vgt ) )
!= vyes ) )
| ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vdivide ) )
= ( D @ ( D @ ( C @ vminus ) @ vdivide ) @ vsucc ) )
& ( B = D )
& ( A = C )
& ( ( D @ ( C @ vgt ) )
= vyes ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[248]) ).
thf(84,axiom,
vmulop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-andop') ).
thf(798,plain,
vmulop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(117,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( H @ ( F @ ( G @ vMC ) @ vptcheck ) ) )
& ( F @ ( G @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( C @ ( B @ vMC ) @ ( H @ ( D @ vqseq ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqseq') ).
thf(910,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( H @ ( F @ ( G @ vMC ) @ vptcheck ) ) )
& ( F @ ( G @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( C @ ( B @ vMC ) @ ( H @ ( D @ vqseq ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(333,axiom,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vmulop @ vevalBinOp ) ) )
= ( B @ ( A @ vmultiply ) @ vNum @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-2') ).
thf(5611,plain,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vmulop @ vevalBinOp ) ) )
= ( B @ ( A @ vmultiply ) @ vNum @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[333]) ).
thf(253,axiom,
! [A: vOptAType] :
( ( A @ visSomeAType )
=> ? [B: vAType] :
( A
= ( B @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-true-INV') ).
thf(1676,plain,
! [A: vOptAType] :
( ( A @ visSomeAType )
=> ? [B: vAType] :
( A
= ( B @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[253]) ).
thf(47,axiom,
! [A: vnat,B: vnat] :
( ( ( B @ ( A @ vgt ) )
= vyes )
=> ( ( B @ ( A @ vdivide ) )
= ( B @ ( B @ ( A @ vminus ) @ vdivide ) @ vsucc ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','divide-0') ).
thf(630,plain,
! [A: vnat,B: vnat] :
( ( ( B @ ( A @ vgt ) )
= vyes )
=> ( ( B @ ( A @ vdivide ) )
= ( B @ ( B @ ( A @ vminus ) @ vdivide ) @ vsucc ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(89,axiom,
! [A: vOptQConf] :
( ~ ( A @ visSomeQC )
=> ( A = vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-false-INV') ).
thf(815,plain,
! [A: vOptQConf] :
( ~ ( A @ visSomeQC )
=> ( A = vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(142,axiom,
vaddop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-eqop') ).
thf(1032,plain,
vaddop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(46,axiom,
! [A: vnat,B: vnat] :
( ( ( A @ vNum )
= ( B @ vNum ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-Num') ).
thf(625,plain,
! [A: vnat,B: vnat] :
( ( ( A @ vNum )
= ( B @ vNum ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(55,axiom,
! [A: vAval] :
( ? [B: vstring] :
( ( ( A @ vtypeOf )
= vText )
& ( A
= ( B @ vT ) ) )
| ? [B: vnat] :
( ( ( A @ vtypeOf )
= vNumber )
& ( A
= ( B @ vNum ) ) )
| ? [B: vYN] :
( ( ( A @ vtypeOf )
= vYesNo )
& ( A
= ( B @ vB ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-INV') ).
thf(665,plain,
! [A: vAval] :
( ? [B: vstring] :
( ( ( A @ vtypeOf )
= vText )
& ( A
= ( B @ vT ) ) )
| ? [B: vnat] :
( ( ( A @ vtypeOf )
= vNumber )
& ( A
= ( B @ vNum ) ) )
| ? [B: vYN] :
( ( ( A @ vtypeOf )
= vYesNo )
& ( A
= ( B @ vB ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(315,axiom,
! [A: vATMap,B: vQID] :
( ( B @ vqvar @ ( A @ vecheck ) )
= ( A @ ( B @ vlookupATMap ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-3') ).
thf(5534,plain,
! [A: vATMap,B: vQID] :
( ( B @ vqvar @ ( A @ vecheck ) )
= ( A @ ( B @ vlookupATMap ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[315]) ).
thf(112,axiom,
! [A: vQID,B: vAType,C: vQID,D: vAType,E: vExp,F: vLabel] :
( ( E @ ( B @ ( C @ vvalue ) ) )
!= ( D @ ( F @ ( A @ vdefquestion ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-value-defquestion') ).
thf(889,plain,
! [A: vQID,B: vAType,C: vQID,D: vAType,E: vExp,F: vLabel] :
( ( E @ ( B @ ( C @ vvalue ) ) )
!= ( D @ ( F @ ( A @ vdefquestion ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(153,axiom,
! [A: vBinOpT,B: vAval,C: vAval] :
( ( ( A != veqop )
& ( ! [D: vYN] :
( C
!= ( D @ vB ) )
| ! [D: vYN] :
( B
!= ( D @ vB ) )
| ( A != vorop ) )
& ( ! [D: vYN] :
( C
!= ( D @ vB ) )
| ! [D: vYN] :
( B
!= ( D @ vB ) )
| ( A != vandop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vltop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vgtop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vdivop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vmulop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vsubop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vaddop ) ) )
=> ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-10') ).
thf(1079,plain,
! [A: vBinOpT,B: vAval,C: vAval] :
( ( ( A != veqop )
& ( ! [D: vYN] :
( C
!= ( D @ vB ) )
| ! [D: vYN] :
( B
!= ( D @ vB ) )
| ( A != vorop ) )
& ( ! [D: vYN] :
( C
!= ( D @ vB ) )
| ! [D: vYN] :
( B
!= ( D @ vB ) )
| ( A != vandop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vltop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vgtop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vdivop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vmulop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vsubop ) )
& ( ! [D: vnat] :
( C
!= ( D @ vNum ) )
| ! [D: vnat] :
( B
!= ( D @ vNum ) )
| ( A != vaddop ) ) )
=> ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(74,axiom,
( ( vno @ vnot )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-1') ).
thf(757,plain,
( ( vno @ vnot )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(64,axiom,
vmulop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-eqop') ).
thf(710,plain,
vmulop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(96,axiom,
! [A: vstring] :
( ( A @ vT @ vtypeOf )
= vText ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-2') ).
thf(842,plain,
! [A: vstring] :
( ( A @ vT @ vtypeOf )
= vText ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(136,axiom,
! [A: vAval] :
( ? [B: vstring] :
( A
= ( B @ vT ) )
| ? [B: vnat] :
( A
= ( B @ vNum ) )
| ? [B: vYN] :
( A
= ( B @ vB ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-Aval') ).
thf(1012,plain,
! [A: vAval] :
( ? [B: vstring] :
( A
= ( B @ vT ) )
| ? [B: vnat] :
( A
= ( B @ vNum ) )
| ? [B: vYN] :
( A
= ( B @ vB ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(167,axiom,
! [A: vQID,B: vUnOpT,C: vExp] :
( ( A @ vqvar )
!= ( C @ ( B @ vunop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qvar-unop') ).
thf(1195,plain,
! [A: vQID,B: vUnOpT,C: vExp] :
( ( A @ vqvar )
!= ( C @ ( B @ vunop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(199,axiom,
! [A: vQMap] :
( ? [B: vQID,C: vLabel,D: vAType,E: vQMap] :
( A
= ( E @ ( D @ ( C @ ( B @ vqmbind ) ) ) ) )
| ( A = vqmempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-QMap') ).
thf(1407,plain,
! [A: vQMap] :
( ? [B: vQID,C: vLabel,D: vAType,E: vQMap] :
( A
= ( E @ ( D @ ( C @ ( B @ vqmbind ) ) ) ) )
| ( A = vqmempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[199]) ).
thf(197,axiom,
! [A: vQConf] : ( A @ vsomeQConf @ visSomeQC ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-1') ).
thf(1402,plain,
! [A: vQConf] : ( A @ vsomeQConf @ visSomeQC ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[197]) ).
thf(184,axiom,
! [A: vQID,B: vAType,C: vATMap,D: vATMap] :
( ( D @ ( C @ ( B @ ( A @ vatmbind ) ) @ vappendATMap ) )
= ( D @ ( C @ vappendATMap ) @ ( B @ ( A @ vatmbind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendATMap-1') ).
thf(1360,plain,
! [A: vQID,B: vAType,C: vATMap,D: vATMap] :
( ( D @ ( C @ ( B @ ( A @ vatmbind ) ) @ vappendATMap ) )
= ( D @ ( C @ vappendATMap ) @ ( B @ ( A @ vatmbind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[184]) ).
thf(235,axiom,
! [A: vOptQConf] :
( ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) )
| ( A = vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptQConf') ).
thf(1592,plain,
! [A: vOptQConf] :
( ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) )
| ( A = vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[235]) ).
thf(156,axiom,
vdivop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-orop') ).
thf(1143,plain,
vdivop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(43,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vGID,F: vATMap] :
( ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ( D @ ( F @ vMC ) @ ( B @ ( E @ vqgroup ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqgroup') ).
thf(615,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vGID,F: vATMap] :
( ( D @ ( F @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ( D @ ( F @ vMC ) @ ( B @ ( E @ vqgroup ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(149,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( C @ ( F @ ( D @ vquestion ) ) )
!= ( E @ ( B @ ( A @ vdefquestion ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-question-defquestion') ).
thf(1064,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( C @ ( F @ ( D @ vquestion ) ) )
!= ( E @ ( B @ ( A @ vdefquestion ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(127,axiom,
! [A: vLabel] :
( ( vNumber @ ( A @ vgetAnswer ) )
= ( A @ vaskNumber @ vNum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-1') ).
thf(980,plain,
! [A: vLabel] :
( ( vNumber @ ( A @ vgetAnswer ) )
= ( A @ vaskNumber @ vNum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(264,axiom,
! [A: vATMap,B: vATMap,C: vAType,D: vQID,E: vExp] :
( ( ( ( E @ ( B @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ( B @ ( D @ vlookupATMap ) )
= vnoAType ) )
=> ( A @ ( B @ ( C @ ( D @ vatmbind ) ) @ vMC ) @ ( E @ ( C @ ( D @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tvalue') ).
thf(1719,plain,
! [A: vATMap,B: vATMap,C: vAType,D: vQID,E: vExp] :
( ( ( ( E @ ( B @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ( B @ ( D @ vlookupATMap ) )
= vnoAType ) )
=> ( A @ ( B @ ( C @ ( D @ vatmbind ) ) @ vMC ) @ ( E @ ( C @ ( D @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[264]) ).
thf(105,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tquestion_inv3') ).
thf(869,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(129,axiom,
! [A: vQID] :
( ( vaempty @ ( A @ vlookupAnsMap ) )
= vnoAval ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupAnsMap-0') ).
thf(989,plain,
! [A: vQID] :
( ( vaempty @ ( A @ vlookupAnsMap ) )
= vnoAval ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(101,axiom,
! [A: vQuestionnaire] :
( ( A != vqempty )
=> ~ ( A @ visValue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-1') ).
thf(857,plain,
! [A: vQuestionnaire] :
( ( A != vqempty )
=> ~ ( A @ visValue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(180,axiom,
! [A: vATMap] :
( ? [B: vQID,C: vAType,D: vATMap] :
( A
= ( D @ ( C @ ( B @ vatmbind ) ) ) )
| ( A = vatmempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-ATMap') ).
thf(1329,plain,
! [A: vATMap] :
( ? [B: vQID,C: vAType,D: vATMap] :
( A
= ( D @ ( C @ ( B @ vatmbind ) ) ) )
| ( A = vatmempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[180]) ).
thf(141,axiom,
! [A: vQConf] :
( vnoQConf
!= ( A @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noQConf-someQConf') ).
thf(1028,plain,
! [A: vQConf] :
( vnoQConf
!= ( A @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(73,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap,E: vQID] :
( ( C @ ( D @ vMC ) @ ( E @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Task_inv4') ).
thf(753,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap,E: vQID] :
( ( C @ ( D @ vMC ) @ ( E @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(302,axiom,
! [A: vBinOpT,B: vAval,C: vAval] :
( ? [D: vBinOpT,E: vAval,F: vAval] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= vnoExp )
& ( C = F )
& ( B = E )
& ( A = D )
& ( D != veqop )
& ( ! [G: vYN] :
( F
!= ( G @ vB ) )
| ! [G: vYN] :
( E
!= ( G @ vB ) )
| ( D != vorop ) )
& ( ! [G: vYN] :
( F
!= ( G @ vB ) )
| ! [G: vYN] :
( E
!= ( G @ vB ) )
| ( D != vandop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vltop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vgtop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vdivop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vmulop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vsubop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vaddop ) ) )
| ? [D: vAval,E: vAval] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( vno @ vB @ vconstant @ vsomeExp ) )
& ( C = E )
& ( B = D )
& ( A = veqop )
& ( D != E ) )
| ? [D: vAval,E: vAval] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) )
& ( C = E )
& ( B = D )
& ( A = veqop )
& ( D = E ) )
| ? [D: vYN,E: vYN] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vor ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vB ) )
& ( B
= ( D @ vB ) )
& ( A = vorop ) )
| ? [D: vYN,E: vYN] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vand ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vB ) )
& ( B
= ( D @ vB ) )
& ( A = vandop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vlt ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vltop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vgt ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vgtop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vdivide ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vdivop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vmultiply ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vmulop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vminus ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vsubop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vplus ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vaddop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-INV') ).
thf(5263,plain,
! [A: vBinOpT,B: vAval,C: vAval] :
( ? [D: vBinOpT,E: vAval,F: vAval] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= vnoExp )
& ( C = F )
& ( B = E )
& ( A = D )
& ( D != veqop )
& ( ! [G: vYN] :
( F
!= ( G @ vB ) )
| ! [G: vYN] :
( E
!= ( G @ vB ) )
| ( D != vorop ) )
& ( ! [G: vYN] :
( F
!= ( G @ vB ) )
| ! [G: vYN] :
( E
!= ( G @ vB ) )
| ( D != vandop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vltop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vgtop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vdivop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vmulop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vsubop ) )
& ( ! [G: vnat] :
( F
!= ( G @ vNum ) )
| ! [G: vnat] :
( E
!= ( G @ vNum ) )
| ( D != vaddop ) ) )
| ? [D: vAval,E: vAval] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( vno @ vB @ vconstant @ vsomeExp ) )
& ( C = E )
& ( B = D )
& ( A = veqop )
& ( D != E ) )
| ? [D: vAval,E: vAval] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) )
& ( C = E )
& ( B = D )
& ( A = veqop )
& ( D = E ) )
| ? [D: vYN,E: vYN] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vor ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vB ) )
& ( B
= ( D @ vB ) )
& ( A = vorop ) )
| ? [D: vYN,E: vYN] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vand ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vB ) )
& ( B
= ( D @ vB ) )
& ( A = vandop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vlt ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vltop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vgt ) @ vB @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vgtop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vdivide ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vdivop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vmultiply ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vmulop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vminus ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vsubop ) )
| ? [D: vnat,E: vnat] :
( ( ( C @ ( B @ ( A @ vevalBinOp ) ) )
= ( E @ ( D @ vplus ) @ vNum @ vconstant @ vsomeExp ) )
& ( C
= ( E @ vNum ) )
& ( B
= ( D @ vNum ) )
& ( A = vaddop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[302]) ).
thf(160,axiom,
! [A: vAnsMap,B: vAnsMap] :
( ? [C: vQID,D: vAval,E: vAnsMap,F: vAnsMap] :
( ( ( B @ ( A @ vappendAnsMap ) )
= ( F @ ( E @ vappendAnsMap ) @ ( D @ ( C @ vabind ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vabind ) ) ) ) )
| ? [C: vAnsMap] :
( ( ( B @ ( A @ vappendAnsMap ) )
= C )
& ( B = C )
& ( A = vaempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendAnsMap-INV') ).
thf(1155,plain,
! [A: vAnsMap,B: vAnsMap] :
( ? [C: vQID,D: vAval,E: vAnsMap,F: vAnsMap] :
( ( ( B @ ( A @ vappendAnsMap ) )
= ( F @ ( E @ vappendAnsMap ) @ ( D @ ( C @ vabind ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vabind ) ) ) ) )
| ? [C: vAnsMap] :
( ( ( B @ ( A @ vappendAnsMap ) )
= C )
& ( B = C )
& ( A = vaempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(58,axiom,
! [A: vQConf,B: vQuestionnaire] :
? [C: vAnsMap,D: vQMap,E: vQuestionnaire,F: vQuestionnaire] :
( ( ( B @ ( A @ vqcappend ) )
= ( F @ ( E @ vqseq ) @ ( D @ ( C @ vQC ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vQC ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qcappend-INV') ).
thf(686,plain,
! [A: vQConf,B: vQuestionnaire] :
? [C: vAnsMap,D: vQMap,E: vQuestionnaire,F: vQuestionnaire] :
( ( ( B @ ( A @ vqcappend ) )
= ( F @ ( E @ vqseq ) @ ( D @ ( C @ vQC ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vQC ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(152,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vQuestionnaire,D: vQuestionnaire,E: vExp] :
( ( C @ ( D @ vqseq ) )
!= ( B @ ( A @ ( E @ vqcond ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qseq-qcond') ).
thf(1075,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vQuestionnaire,D: vQuestionnaire,E: vExp] :
( ( C @ ( D @ vqseq ) )
!= ( B @ ( A @ ( E @ vqcond ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(23,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( vnoQuestion
!= ( C @ ( B @ ( A @ vsomeQuestion ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noQuestion-someQuestion') ).
thf(476,plain,
! [A: vQID,B: vLabel,C: vAType] :
( vnoQuestion
!= ( C @ ( B @ ( A @ vsomeQuestion ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(45,axiom,
vaddop != vdivop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-divop') ).
thf(622,plain,
vaddop != vdivop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(173,axiom,
! [A: vQuestionnaire,B: vAnsMap,C: vQMap] :
( ( C @ ( B @ ( A @ ( vqempty @ vqseq ) @ vreduce ) ) )
= ( A @ ( C @ ( B @ vQC ) ) @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-8') ).
thf(1263,plain,
! [A: vQuestionnaire,B: vAnsMap,C: vQMap] :
( ( C @ ( B @ ( A @ ( vqempty @ vqseq ) @ vreduce ) ) )
= ( A @ ( C @ ( B @ vQC ) ) @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(61,axiom,
! [A: vQuestionnaire,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqseq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qseq') ).
thf(701,plain,
! [A: vQuestionnaire,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqseq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(69,axiom,
vsubop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-ltop') ).
thf(738,plain,
vsubop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(224,axiom,
! [A: vAnsMap] :
( ( A @ ( vaempty @ vappendAnsMap ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendAnsMap-0') ).
thf(1539,plain,
! [A: vAnsMap] :
( ( A @ ( vaempty @ vappendAnsMap ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[224]) ).
thf(174,axiom,
! [A: vYN] :
( ( ( ( A @ vnot )
= vyes )
& ( A = vno ) )
| ( ( ( A @ vnot )
= vno )
& ( A = vyes ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-INV') ).
thf(1266,plain,
! [A: vYN] :
( ( ( ( A @ vnot )
= vyes )
& ( A = vno ) )
| ( ( ( A @ vnot )
= vno )
& ( A = vyes ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(250,axiom,
! [A: vATMap] :
( ( A @ ( vatmempty @ vintersectATM ) )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersectATM-0') ).
thf(1668,plain,
! [A: vATMap] :
( ( A @ ( vatmempty @ vintersectATM ) )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[250]) ).
thf(166,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vsucc @ vlt ) )
= ( A @ ( A @ vlt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lt-2') ).
thf(1192,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vsucc @ vlt ) )
= ( A @ ( A @ vlt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(133,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) @ vtypeQM )
= ( D @ vtypeQM @ ( C @ ( A @ vatmbind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeQM-1') ).
thf(1002,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) @ vtypeQM )
= ( D @ vtypeQM @ ( C @ ( A @ vatmbind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(276,axiom,
! [A: vOptExp] :
( ? [B: vExp] :
( A
= ( B @ vsomeExp ) )
| ( A = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptExp') ).
thf(1874,plain,
! [A: vOptExp] :
( ? [B: vExp] :
( A
= ( B @ vsomeExp ) )
| ( A = vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[276]) ).
thf(35,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vQuestionnaire,D: vQuestionnaire] :
( ( ( B @ ( A @ vqseq ) )
= ( D @ ( C @ vqseq ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qseq') ).
thf(569,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vQuestionnaire,D: vQuestionnaire] :
( ( ( B @ ( A @ vqseq ) )
= ( D @ ( C @ vqseq ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(237,axiom,
! [A: vQID,B: vQID] :
( ( ( A @ vqvar )
= ( B @ vqvar ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qvar') ).
thf(1599,plain,
! [A: vQID,B: vQID] :
( ( ( A @ vqvar )
= ( B @ vqvar ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[237]) ).
thf(263,axiom,
! [A: vQID,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vqvar )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qvar-binop') ).
thf(1715,plain,
! [A: vQID,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vqvar )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[263]) ).
thf(8,axiom,
! [A: vnat,B: vnat] :
( ( ( A @ vsucc )
= ( B @ vsucc ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-succ') ).
thf(371,plain,
! [A: vnat,B: vnat] :
( ( ( A @ vsucc )
= ( B @ vsucc ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(194,axiom,
! [A: vYN] :
( ( A @ vB @ vtypeOf )
= vYesNo ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-0') ).
thf(1393,plain,
! [A: vYN] :
( ( A @ vB @ vtypeOf )
= vYesNo ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[194]) ).
thf(270,axiom,
( ( vNumber @ ( vNumber @ ( vgtop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-4') ).
thf(1857,plain,
( ( vNumber @ ( vNumber @ ( vgtop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[270]) ).
thf(318,axiom,
( ( vNumber @ ( vNumber @ ( vdivop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-3') ).
thf(5544,plain,
( ( vNumber @ ( vNumber @ ( vdivop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[318]) ).
thf(123,axiom,
~ ( vnoAType @ visSomeAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-0') ).
thf(938,plain,
~ ( vnoAType @ visSomeAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(48,axiom,
! [A: vOptAType] :
( ~ ( A @ visSomeAType )
=> ( A = vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-false-INV') ).
thf(633,plain,
! [A: vOptAType] :
( ~ ( A @ visSomeAType )
=> ( A = vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(231,axiom,
! [A: vQID,B: vAnsMap,C: vAval,D: vAval,E: vQID,F: vAnsMap] :
( ( ( F @ ( C @ ( E @ vabind ) ) )
= ( B @ ( D @ ( A @ vabind ) ) ) )
=> ( ( F = B )
& ( C = D )
& ( E = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-abind') ).
thf(1563,plain,
! [A: vQID,B: vAnsMap,C: vAval,D: vAval,E: vQID,F: vAnsMap] :
( ( ( F @ ( C @ ( E @ vabind ) ) )
= ( B @ ( D @ ( A @ vabind ) ) ) )
=> ( ( F = B )
& ( C = D )
& ( E = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[231]) ).
thf(161,axiom,
! [A: vLabel] :
( ( vText @ ( A @ vgetAnswer ) )
= ( A @ vaskText @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-2') ).
thf(1170,plain,
! [A: vLabel] :
( ( vText @ ( A @ vgetAnswer ) )
= ( A @ vaskText @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(143,axiom,
! [A: vOptAval] :
( ( A @ visSomeAval )
=> ? [B: vAval] :
( A
= ( B @ vsomeAval ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-true-INV') ).
thf(1035,plain,
! [A: vOptAval] :
( ( A @ visSomeAval )
=> ? [B: vAval] :
( A
= ( B @ vsomeAval ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(151,axiom,
! [A: vQID,B: vQMap,C: vAnsMap] :
( ~ ( B @ ( A @ vlookupQMap ) @ visSomeQuestion )
=> ( ( B @ ( C @ ( A @ vask @ vqsingle @ vreduce ) ) )
= vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-7') ).
thf(1071,plain,
! [A: vQID,B: vQMap,C: vAnsMap] :
( ~ ( B @ ( A @ vlookupQMap ) @ visSomeQuestion )
=> ( ( B @ ( C @ ( A @ vask @ vqsingle @ vreduce ) ) )
= vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(66,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( ( C @ ( F @ ( D @ vdefquestion ) ) )
= ( E @ ( B @ ( A @ vdefquestion ) ) ) )
=> ( ( C = E )
& ( F = B )
& ( D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-defquestion') ).
thf(718,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( ( C @ ( F @ ( D @ vdefquestion ) ) )
= ( E @ ( B @ ( A @ vdefquestion ) ) ) )
=> ( ( C = E )
& ( F = B )
& ( D = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(77,axiom,
! [A: vQID,B: vATMap,C: vAType,D: vATMap] :
( ~ ( ( ( B @ ( A @ vlookupATMap ) @ vgetAType )
= C )
& ( B @ ( A @ vlookupATMap ) @ visSomeAType ) )
=> ( ( B @ ( D @ ( C @ ( A @ vatmbind ) ) @ vintersectATM ) )
= ( B @ ( D @ vintersectATM ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersectATM-2') ).
thf(765,plain,
! [A: vQID,B: vATMap,C: vAType,D: vATMap] :
( ~ ( ( ( B @ ( A @ vlookupATMap ) @ vgetAType )
= C )
& ( B @ ( A @ vlookupATMap ) @ visSomeAType ) )
=> ( ( B @ ( D @ ( C @ ( A @ vatmbind ) ) @ vintersectATM ) )
= ( B @ ( D @ vintersectATM ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(262,axiom,
! [A: vExp] :
( ? [B: vUnOpT,C: vExp] :
( A
= ( C @ ( B @ vunop ) ) )
| ? [B: vExp,C: vBinOpT,D: vExp] :
( A
= ( D @ ( C @ ( B @ vbinop ) ) ) )
| ? [B: vQID] :
( A
= ( B @ vqvar ) )
| ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-Exp') ).
thf(1712,plain,
! [A: vExp] :
( ? [B: vUnOpT,C: vExp] :
( A
= ( C @ ( B @ vunop ) ) )
| ? [B: vExp,C: vBinOpT,D: vExp] :
( A
= ( D @ ( C @ ( B @ vbinop ) ) ) )
| ? [B: vQID] :
( A
= ( B @ vqvar ) )
| ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[262]) ).
thf(14,axiom,
! [A: vAval,B: vAval] :
( ( ( A @ vsomeAval )
= ( B @ vsomeAval ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someAval') ).
thf(412,plain,
! [A: vAval,B: vAval] :
( ( ( A @ vsomeAval )
= ( B @ vsomeAval ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(157,axiom,
vgtop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-gtop-andop') ).
thf(1146,plain,
vgtop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(211,axiom,
vaddop != vmulop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-mulop') ).
thf(1483,plain,
vaddop != vmulop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[211]) ).
thf(227,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( A @ ( G @ vlookupATMap ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tdefquestion_inv1') ).
thf(1548,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( A @ ( G @ vlookupATMap ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[227]) ).
thf(332,axiom,
! [A: vAval,B: vAval] :
( ( A != B )
=> ( ( B @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vno @ vB @ vconstant @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-9') ).
thf(5608,plain,
! [A: vAval,B: vAval] :
( ( A != B )
=> ( ( B @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vno @ vB @ vconstant @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[332]) ).
thf(188,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ? [H: vATMap,I: vATMap] : ( I @ ( H @ vMC ) @ ( G @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond_inv3') ).
thf(1374,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ? [H: vATMap,I: vATMap] : ( I @ ( H @ vMC ) @ ( G @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[188]) ).
thf(178,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap] :
( ( D @ ( C @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) )
=> ( D = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqempty_inv2') ).
thf(1301,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap] :
( ( D @ ( C @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) )
=> ( D = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[178]) ).
thf(236,axiom,
! [A: vQID,B: vAType,C: vQID,D: vAType,E: vExp,F: vLabel] :
( ( B @ ( F @ ( C @ vquestion ) ) )
!= ( E @ ( D @ ( A @ vvalue ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-question-value') ).
thf(1595,plain,
! [A: vQID,B: vAType,C: vQID,D: vAType,E: vExp,F: vLabel] :
( ( B @ ( F @ ( C @ vquestion ) ) )
!= ( E @ ( D @ ( A @ vvalue ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[236]) ).
thf(38,axiom,
! [A: vATMap,B: vATMap] :
( ? [C: vQID,D: vAType,E: vATMap,F: vATMap] :
( ( ( B @ ( A @ vappendATMap ) )
= ( F @ ( E @ vappendATMap ) @ ( D @ ( C @ vatmbind ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vatmbind ) ) ) ) )
| ? [C: vATMap] :
( ( ( B @ ( A @ vappendATMap ) )
= C )
& ( B = C )
& ( A = vatmempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendATMap-INV') ).
thf(584,plain,
! [A: vATMap,B: vATMap] :
( ? [C: vQID,D: vAType,E: vATMap,F: vATMap] :
( ( ( B @ ( A @ vappendATMap ) )
= ( F @ ( E @ vappendATMap ) @ ( D @ ( C @ vatmbind ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vatmbind ) ) ) ) )
| ? [C: vATMap] :
( ( ( B @ ( A @ vappendATMap ) )
= C )
& ( B = C )
& ( A = vatmempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(67,axiom,
vsubop != vdivop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-divop') ).
thf(732,plain,
vsubop != vdivop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(307,axiom,
! [A: vAType] :
( vnoAType
!= ( A @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noAType-someAType') ).
thf(5395,plain,
! [A: vAType] :
( vnoAType
!= ( A @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[307]) ).
thf(78,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vExp,K: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( K @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( K @ ( D @ ( J @ vqcond ) ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( H = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond_inv4') ).
thf(772,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vExp,K: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( K @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( K @ ( D @ ( J @ vqcond ) ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( H = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(243,axiom,
! [A: vQuestionnaire] :
( ? [B: vGID,C: vQuestionnaire] :
( A
= ( C @ ( B @ vqgroup ) ) )
| ? [B: vExp,C: vQuestionnaire,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vqcond ) ) ) )
| ? [B: vQuestionnaire,C: vQuestionnaire] :
( A
= ( C @ ( B @ vqseq ) ) )
| ? [B: vEntry] :
( A
= ( B @ vqsingle ) )
| ( A = vqempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-Questionnaire') ).
thf(1620,plain,
! [A: vQuestionnaire] :
( ? [B: vGID,C: vQuestionnaire] :
( A
= ( C @ ( B @ vqgroup ) ) )
| ? [B: vExp,C: vQuestionnaire,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vqcond ) ) ) )
| ? [B: vQuestionnaire,C: vQuestionnaire] :
( A
= ( C @ ( B @ vqseq ) ) )
| ? [B: vEntry] :
( A
= ( B @ vqsingle ) )
| ( A = vqempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[243]) ).
thf(338,axiom,
! [A: vUnOpT,B: vAval] :
( ? [C: vUnOpT,D: vAval] :
( ( ( B @ ( A @ vevalUnOp ) )
= vnoExp )
& ( B = D )
& ( A = C )
& ( ! [E: vYN] :
( D
!= ( E @ vB ) )
| ( C != vnotop ) ) )
| ? [C: vYN] :
( ( ( B @ ( A @ vevalUnOp ) )
= ( C @ vnot @ vB @ vconstant @ vsomeExp ) )
& ( B
= ( C @ vB ) )
& ( A = vnotop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalUnOp-INV') ).
thf(5627,plain,
! [A: vUnOpT,B: vAval] :
( ? [C: vUnOpT,D: vAval] :
( ( ( B @ ( A @ vevalUnOp ) )
= vnoExp )
& ( B = D )
& ( A = C )
& ( ! [E: vYN] :
( D
!= ( E @ vB ) )
| ( C != vnotop ) ) )
| ? [C: vYN] :
( ( ( B @ ( A @ vevalUnOp ) )
= ( C @ vnot @ vB @ vconstant @ vsomeExp ) )
& ( B
= ( C @ vB ) )
& ( A = vnotop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[338]) ).
thf(107,axiom,
~ ( vnoExp @ visSomeExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-0') ).
thf(875,plain,
~ ( vnoExp @ visSomeExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(36,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( B @ ( G @ vlookupATMap ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tquestion_inv1') ).
thf(579,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( B @ ( G @ vlookupATMap ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(309,axiom,
! [A: vAType] :
( ( A @ vsomeAType @ vgetAType )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAType-0') ).
thf(5503,plain,
! [A: vAType] :
( ( A @ vsomeAType @ vgetAType )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[309]) ).
thf(51,axiom,
! [A: vATMap,B: vATMap,C: vAType,D: vLabel,E: vQID] :
( ( ( A @ ( E @ vlookupATMap ) )
= vnoAType )
=> ( A @ ( C @ ( E @ vatmbind ) ) @ ( B @ vMC ) @ ( C @ ( D @ ( E @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tdefquestion') ).
thf(641,plain,
! [A: vATMap,B: vATMap,C: vAType,D: vLabel,E: vQID] :
( ( ( A @ ( E @ vlookupATMap ) )
= vnoAType )
=> ( A @ ( C @ ( E @ vatmbind ) ) @ ( B @ vMC ) @ ( C @ ( D @ ( E @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(319,axiom,
! [A: vAval] :
( ( A @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-8') ).
thf(5546,plain,
! [A: vAval] :
( ( A @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[319]) ).
thf(20,axiom,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vminus ) )
= ( C @ ( D @ vminus ) @ vpred ) )
& ( B
= ( C @ vsucc ) )
& ( A = D ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vminus ) )
= C )
& ( B = vzero )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','minus-INV') ).
thf(445,plain,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vminus ) )
= ( C @ ( D @ vminus ) @ vpred ) )
& ( B
= ( C @ vsucc ) )
& ( A = D ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vminus ) )
= C )
& ( B = vzero )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(11,axiom,
( ( vqmempty @ vtypeQM )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeQM-0') ).
thf(382,plain,
( ( vqmempty @ vtypeQM )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(322,axiom,
! [A: vExp,B: vExp,C: vExp,D: vExp,E: vBinOpT,F: vBinOpT] :
( ( ( A @ ( E @ ( D @ vbinop ) ) )
= ( B @ ( F @ ( C @ vbinop ) ) ) )
=> ( ( A = B )
& ( E = F )
& ( D = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-binop') ).
thf(5567,plain,
! [A: vExp,B: vExp,C: vExp,D: vExp,E: vBinOpT,F: vBinOpT] :
( ( ( A @ ( E @ ( D @ vbinop ) ) )
= ( B @ ( F @ ( C @ vbinop ) ) ) )
=> ( ( A = B )
& ( E = F )
& ( D = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[322]) ).
thf(283,axiom,
( ( vNumber @ ( vNumber @ ( vmulop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-2') ).
thf(5118,plain,
( ( vNumber @ ( vNumber @ ( vmulop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[283]) ).
thf(65,axiom,
! [A: vQConf,B: vQConf] :
( ( ( A @ vsomeQConf )
= ( B @ vsomeQConf ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someQConf') ).
thf(713,plain,
! [A: vQConf,B: vQConf] :
( ( ( A @ vsomeQConf )
= ( B @ vsomeQConf ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(147,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap,E: vQID] :
( ( C @ ( D @ vMC ) @ ( E @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( B @ ( E @ vlookupATMap ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Task_inv1') ).
thf(1058,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap,E: vQID] :
( ( C @ ( D @ vMC ) @ ( E @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( ( B @ ( E @ vlookupATMap ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(86,axiom,
vmulop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-gtop') ).
thf(804,plain,
vmulop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(183,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap] :
( ( D @ ( C @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqempty_inv1') ).
thf(1356,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap] :
( ( D @ ( C @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[183]) ).
thf(3,axiom,
( ( vzero @ vpred )
= vzero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred-0') ).
thf(350,plain,
( ( vzero @ vpred )
= vzero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(217,axiom,
! [A: vQID,B: vATMap,C: vAType,D: vATMap] :
( ( ( ( B @ ( A @ vlookupATMap ) @ vgetAType )
= C )
& ( B @ ( A @ vlookupATMap ) @ visSomeAType ) )
=> ( ( B @ ( D @ ( C @ ( A @ vatmbind ) ) @ vintersectATM ) )
= ( B @ ( D @ vintersectATM ) @ ( C @ ( A @ vatmbind ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersectATM-1') ).
thf(1503,plain,
! [A: vQID,B: vATMap,C: vAType,D: vATMap] :
( ( ( ( B @ ( A @ vlookupATMap ) @ vgetAType )
= C )
& ( B @ ( A @ vlookupATMap ) @ visSomeAType ) )
=> ( ( B @ ( D @ ( C @ ( A @ vatmbind ) ) @ vintersectATM ) )
= ( B @ ( D @ vintersectATM ) @ ( C @ ( A @ vatmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[217]) ).
thf(298,axiom,
! [A: vQID,B: vATMap,C: vAType,D: vATMap] :
( ( ( ( D @ ( A @ vlookupATMap ) )
= vnoAType )
& ( ( B @ ( A @ vlookupATMap ) )
= ( C @ vsomeAType ) ) )
=> ( B @ ( D @ ( C @ ( A @ vatmbind ) ) @ vMC ) @ ( A @ vask @ vqsingle @ ( B @ ( D @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Task') ).
thf(5185,plain,
! [A: vQID,B: vATMap,C: vAType,D: vATMap] :
( ( ( ( D @ ( A @ vlookupATMap ) )
= vnoAType )
& ( ( B @ ( A @ vlookupATMap ) )
= ( C @ vsomeAType ) ) )
=> ( B @ ( D @ ( C @ ( A @ vatmbind ) ) @ vMC ) @ ( A @ vask @ vqsingle @ ( B @ ( D @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[298]) ).
thf(42,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vGID,D: vQuestionnaire,E: vExp] :
( ( B @ ( D @ ( E @ vqcond ) ) )
!= ( A @ ( C @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qcond-qgroup') ).
thf(611,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vGID,D: vQuestionnaire,E: vExp] :
( ( B @ ( D @ ( E @ vqcond ) ) )
!= ( A @ ( C @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(328,axiom,
! [A: vAType] : ( A @ vsomeAType @ visSomeAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-1') ).
thf(5595,plain,
! [A: vAType] : ( A @ vsomeAType @ visSomeAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[328]) ).
thf(291,axiom,
! [A: vExp] :
( ~ ( A @ vexpIsValue )
=> ? [B: vExp] :
( ( A = B )
& ! [C: vAval] :
( B
!= ( C @ vconstant ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-false-INV') ).
thf(5148,plain,
! [A: vExp] :
( ~ ( A @ vexpIsValue )
=> ? [B: vExp] :
( ( A = B )
& ! [C: vAval] :
( B
!= ( C @ vconstant ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[291]) ).
thf(181,axiom,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vlt ) )
= ( D @ ( D @ vlt ) ) )
& ( B
= ( C @ vsucc ) )
& ( A
= ( D @ vsucc ) ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vlt ) )
= vyes )
& ( B
= ( C @ vsucc ) )
& ( A = vzero ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vlt ) )
= vno )
& ( B = vzero )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lt-INV') ).
thf(1332,plain,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vlt ) )
= ( D @ ( D @ vlt ) ) )
& ( B
= ( C @ vsucc ) )
& ( A
= ( D @ vsucc ) ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vlt ) )
= vyes )
& ( B
= ( C @ vsucc ) )
& ( A = vzero ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vlt ) )
= vno )
& ( B = vzero )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[181]) ).
thf(171,axiom,
! [A: vQMap,B: vQID,C: vAType,D: vLabel,E: vQID] :
( ( E != B )
=> ( ( A @ ( C @ ( D @ ( B @ vqmbind ) ) ) @ ( E @ vlookupQMap ) )
= ( A @ ( E @ vlookupQMap ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupQMap-2') ).
thf(1258,plain,
! [A: vQMap,B: vQID,C: vAType,D: vLabel,E: vQID] :
( ( E != B )
=> ( ( A @ ( C @ ( D @ ( B @ vqmbind ) ) ) @ ( E @ vlookupQMap ) )
= ( A @ ( E @ vlookupQMap ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[171]) ).
thf(293,axiom,
! [A: vATMap,B: vstring] :
( ( B @ vT @ vconstant @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-2') ).
thf(5158,plain,
! [A: vATMap,B: vstring] :
( ( B @ vT @ vconstant @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[293]) ).
thf(115,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( ~ ( D @ ( C @ ( A @ vreduce ) ) @ visSomeQC )
& ! [E: vQuestionnaire] :
( ( B != E )
| ( A != vqempty ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ vqseq ) @ vreduce ) ) )
= vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-10') ).
thf(900,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( ~ ( D @ ( C @ ( A @ vreduce ) ) @ visSomeQC )
& ! [E: vQuestionnaire] :
( ( B != E )
| ( A != vqempty ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ vqseq ) @ vreduce ) ) )
= vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(93,axiom,
! [A: vQID,B: vAval,C: vAnsMap] :
( vaempty
!= ( C @ ( B @ ( A @ vabind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-aempty-abind') ).
thf(831,plain,
! [A: vQID,B: vAval,C: vAnsMap] :
( vaempty
!= ( C @ ( B @ ( A @ vabind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(310,axiom,
! [A: vUnOpT,B: vAType] :
( ? [C: vUnOpT,D: vAType] :
( ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType )
& ( B = D )
& ( A = C )
& ( ( D != vYesNo )
| ( C != vnotop ) ) )
| ( ( ( B @ ( A @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) )
& ( B = vYesNo )
& ( A = vnotop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-INV') ).
thf(5506,plain,
! [A: vUnOpT,B: vAType] :
( ? [C: vUnOpT,D: vAType] :
( ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType )
& ( B = D )
& ( A = C )
& ( ( D != vYesNo )
| ( C != vnotop ) ) )
| ( ( ( B @ ( A @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) )
& ( B = vYesNo )
& ( A = vnotop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[310]) ).
thf(81,axiom,
! [A: vUnOpT,B: vAval] :
( ( ! [C: vYN] :
( B
!= ( C @ vB ) )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vevalUnOp ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalUnOp-1') ).
thf(784,plain,
! [A: vUnOpT,B: vAval] :
( ( ! [C: vYN] :
( B
!= ( C @ vB ) )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vevalUnOp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(214,axiom,
! [A: vOptQConf] :
( ( A @ visSomeQC )
=> ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-true-INV') ).
thf(1492,plain,
! [A: vOptQConf] :
( ( A @ visSomeQC )
=> ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[214]) ).
thf(225,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ? [H: vATMap,I: vATMap] : ( I @ ( H @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond_inv2') ).
thf(1542,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ? [H: vATMap,I: vATMap] : ( I @ ( H @ vMC ) @ ( B @ ( A @ ( C @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[225]) ).
thf(5,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vminus ) )
= ( B @ ( A @ vminus ) @ vpred ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','minus-1') ).
thf(362,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vminus ) )
= ( B @ ( A @ vminus ) @ vpred ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(265,axiom,
! [A: vATMap,B: vYN] :
( ( B @ vB @ vconstant @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-0') ).
thf(1722,plain,
! [A: vATMap,B: vYN] :
( ( B @ vB @ vconstant @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[265]) ).
thf(103,axiom,
! [A: vYN] :
( ( A = vno )
| ( A = vyes ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-YN') ).
thf(863,plain,
! [A: vYN] :
( ( A = vno )
| ( A = vyes ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(54,axiom,
! [A: vYN,B: vYN] :
( ? [C: vYN,D: vYN] :
( ( ( B @ ( A @ vor ) )
= vyes )
& ( B = D )
& ( A = C )
& ( ( D != vno )
| ( C != vno ) ) )
| ( ( ( B @ ( A @ vor ) )
= vno )
& ( B = vno )
& ( A = vno ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','or-INV') ).
thf(649,plain,
! [A: vYN,B: vYN] :
( ? [C: vYN,D: vYN] :
( ( ( B @ ( A @ vor ) )
= vyes )
& ( B = D )
& ( A = C )
& ( ( D != vno )
| ( C != vno ) ) )
| ( ( ( B @ ( A @ vor ) )
= vno )
& ( B = vno )
& ( A = vno ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(17,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vsucc @ vgt ) )
= ( A @ ( A @ vgt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt-2') ).
thf(434,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vsucc @ vgt ) )
= ( A @ ( A @ vgt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(314,axiom,
! [A: vQID,B: vAnsMap] :
( ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= ( B @ ( A @ vlookupAnsMap ) @ vgetAval @ vconstant @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-1') ).
thf(5531,plain,
! [A: vQID,B: vAnsMap] :
( ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= ( B @ ( A @ vlookupAnsMap ) @ vgetAval @ vconstant @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[314]) ).
thf(39,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQID] :
( ( C @ ( B @ ( A @ vdefquestion ) ) )
!= ( D @ vask ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-defquestion-ask') ).
thf(599,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID] :
( ( C @ ( B @ ( A @ vdefquestion ) ) )
!= ( D @ vask ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(189,axiom,
! [A: vQConf] :
( ( A @ vsomeQConf @ vgetQC )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQC-0') ).
thf(1376,plain,
! [A: vQConf] :
( ( A @ vsomeQConf @ vgetQC )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[189]) ).
thf(324,axiom,
( ( vaempty @ vtypeAM )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeAM-0') ).
thf(5584,plain,
( ( vaempty @ vtypeAM )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[324]) ).
thf(277,axiom,
! [A: vExp] :
( ! [B: vAval] :
( A
!= ( B @ vconstant ) )
=> ~ ( A @ vexpIsValue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-1') ).
thf(1877,plain,
! [A: vExp] :
( ! [B: vAval] :
( A
!= ( B @ vconstant ) )
=> ~ ( A @ vexpIsValue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[277]) ).
thf(246,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQM )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQM-0') ).
thf(1630,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQM )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[246]) ).
thf(25,axiom,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vgt ) )
= ( C @ ( C @ vgt ) ) )
& ( B
= ( D @ vsucc ) )
& ( A
= ( C @ vsucc ) ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vgt ) )
= vyes )
& ( B = vzero )
& ( A
= ( C @ vsucc ) ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vgt ) )
= vno )
& ( B = C )
& ( A = vzero ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt-INV') ).
thf(483,plain,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vgt ) )
= ( C @ ( C @ vgt ) ) )
& ( B
= ( D @ vsucc ) )
& ( A
= ( C @ vsucc ) ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vgt ) )
= vyes )
& ( B = vzero )
& ( A
= ( C @ vsucc ) ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vgt ) )
= vno )
& ( B = C )
& ( A = vzero ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(98,axiom,
! [A: vOptQuestion] :
( ~ ( A @ visSomeQuestion )
=> ( A = vnoQuestion ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-false-INV') ).
thf(848,plain,
! [A: vOptQuestion] :
( ~ ( A @ visSomeQuestion )
=> ( A = vnoQuestion ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(306,axiom,
! [A: vQMap,B: vAType,C: vAnsMap,D: vQID,E: vExp] :
( ( E @ vexpIsValue )
=> ( ( A @ ( C @ ( E @ ( B @ ( D @ vvalue ) ) @ vqsingle @ vreduce ) ) )
= ( vqempty @ ( A @ ( C @ ( E @ vgetExpValue @ ( D @ vabind ) ) @ vQC ) ) @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-2') ).
thf(5392,plain,
! [A: vQMap,B: vAType,C: vAnsMap,D: vQID,E: vExp] :
( ( E @ vexpIsValue )
=> ( ( A @ ( C @ ( E @ ( B @ ( D @ vvalue ) ) @ vqsingle @ vreduce ) ) )
= ( vqempty @ ( A @ ( C @ ( E @ vgetExpValue @ ( D @ vabind ) ) @ vQC ) ) @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[306]) ).
thf(158,axiom,
! [A: vQID,B: vAval,C: vAnsMap] :
( ( C @ ( B @ ( A @ vabind ) ) @ ( A @ vlookupAnsMap ) )
= ( B @ vsomeAval ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupAnsMap-1') ).
thf(1149,plain,
! [A: vQID,B: vAval,C: vAnsMap] :
( ( C @ ( B @ ( A @ vabind ) ) @ ( A @ vlookupAnsMap ) )
= ( B @ vsomeAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[158]) ).
thf(206,axiom,
vltop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-ltop-andop') ).
thf(1460,plain,
vltop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[206]) ).
thf(88,axiom,
! [A: vExp,B: vQuestionnaire,C: vQuestionnaire] :
( vqempty
!= ( C @ ( B @ ( A @ vqcond ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qcond') ).
thf(811,plain,
! [A: vExp,B: vQuestionnaire,C: vQuestionnaire] :
( vqempty
!= ( C @ ( B @ ( A @ vqcond ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(13,axiom,
! [A: vQID,B: vQMap] :
( ? [C: vQMap,D: vQID,E: vAType,F: vLabel,G: vQID] :
( ( ( B @ ( A @ vlookupQMap ) )
= ( C @ ( G @ vlookupQMap ) ) )
& ( B
= ( C @ ( E @ ( F @ ( D @ vqmbind ) ) ) ) )
& ( A = G )
& ( G != D ) )
| ? [C: vQMap,D: vQID,E: vAType,F: vLabel,G: vQID] :
( ( ( B @ ( A @ vlookupQMap ) )
= ( E @ ( F @ ( G @ vsomeQuestion ) ) ) )
& ( B
= ( C @ ( E @ ( F @ ( D @ vqmbind ) ) ) ) )
& ( A = G )
& ( G = D ) )
| ? [C: vQID] :
( ( ( B @ ( A @ vlookupQMap ) )
= vnoQuestion )
& ( B = vqmempty )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupQMap-INV') ).
thf(387,plain,
! [A: vQID,B: vQMap] :
( ? [C: vQMap,D: vQID,E: vAType,F: vLabel,G: vQID] :
( ( ( B @ ( A @ vlookupQMap ) )
= ( C @ ( G @ vlookupQMap ) ) )
& ( B
= ( C @ ( E @ ( F @ ( D @ vqmbind ) ) ) ) )
& ( A = G )
& ( G != D ) )
| ? [C: vQMap,D: vQID,E: vAType,F: vLabel,G: vQID] :
( ( ( B @ ( A @ vlookupQMap ) )
= ( E @ ( F @ ( G @ vsomeQuestion ) ) ) )
& ( B
= ( C @ ( E @ ( F @ ( D @ vqmbind ) ) ) ) )
& ( A = G )
& ( G = D ) )
| ? [C: vQID] :
( ( ( B @ ( A @ vlookupQMap ) )
= vnoQuestion )
& ( B = vqmempty )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(125,axiom,
! [A: vATMap,B: vATMap] :
( ? [C: vATMap,D: vATMap,E: vOptAType,F: vAType,G: vATMap,H: vQID] :
( ( ( B @ ( A @ vintersectATM ) )
= D )
& ( B = C )
& ( A
= ( G @ ( F @ ( H @ vatmbind ) ) ) )
& ~ ( ( ( E @ vgetAType )
= F )
& ( E @ visSomeAType ) )
& ( E
= ( C @ ( H @ vlookupATMap ) ) )
& ( D
= ( C @ ( G @ vintersectATM ) ) ) )
| ? [C: vATMap,D: vATMap,E: vOptAType,F: vAType,G: vATMap,H: vQID] :
( ( ( B @ ( A @ vintersectATM ) )
= ( D @ ( F @ ( H @ vatmbind ) ) ) )
& ( B = C )
& ( A
= ( G @ ( F @ ( H @ vatmbind ) ) ) )
& ( ( E @ vgetAType )
= F )
& ( E @ visSomeAType )
& ( E
= ( C @ ( H @ vlookupATMap ) ) )
& ( D
= ( C @ ( G @ vintersectATM ) ) ) )
| ? [C: vATMap] :
( ( ( B @ ( A @ vintersectATM ) )
= vatmempty )
& ( B = C )
& ( A = vatmempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersectATM-INV') ).
thf(943,plain,
! [A: vATMap,B: vATMap] :
( ? [C: vATMap,D: vATMap,E: vOptAType,F: vAType,G: vATMap,H: vQID] :
( ( ( B @ ( A @ vintersectATM ) )
= D )
& ( B = C )
& ( A
= ( G @ ( F @ ( H @ vatmbind ) ) ) )
& ~ ( ( ( E @ vgetAType )
= F )
& ( E @ visSomeAType ) )
& ( E
= ( C @ ( H @ vlookupATMap ) ) )
& ( D
= ( C @ ( G @ vintersectATM ) ) ) )
| ? [C: vATMap,D: vATMap,E: vOptAType,F: vAType,G: vATMap,H: vQID] :
( ( ( B @ ( A @ vintersectATM ) )
= ( D @ ( F @ ( H @ vatmbind ) ) ) )
& ( B = C )
& ( A
= ( G @ ( F @ ( H @ vatmbind ) ) ) )
& ( ( E @ vgetAType )
= F )
& ( E @ visSomeAType )
& ( E
= ( C @ ( H @ vlookupATMap ) ) )
& ( D
= ( C @ ( G @ vintersectATM ) ) ) )
| ? [C: vATMap] :
( ( ( B @ ( A @ vintersectATM ) )
= vatmempty )
& ( B = C )
& ( A = vatmempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(139,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vmultiply ) )
= ( B @ ( A @ vmultiply ) @ ( A @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','multiply-1') ).
thf(1022,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vmultiply ) )
= ( B @ ( A @ vmultiply ) @ ( A @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(121,axiom,
vyes != vno,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-yes-no') ).
thf(932,plain,
vyes != vno,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(148,axiom,
! [A: vOptAval] :
( ~ ( A @ visSomeAval )
=> ( A = vnoAval ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-false-INV') ).
thf(1061,plain,
! [A: vOptAval] :
( ~ ( A @ visSomeAval )
=> ( A = vnoAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(118,axiom,
~ ( vnoQuestion @ visSomeQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-0') ).
thf(912,plain,
~ ( vnoQuestion @ visSomeQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(128,axiom,
! [A: vQuestionnaire] :
( ~ ( A @ visValue )
=> ? [B: vQuestionnaire] :
( ( A = B )
& ( B != vqempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-false-INV') ).
thf(983,plain,
! [A: vQuestionnaire] :
( ~ ( A @ visValue )
=> ? [B: vQuestionnaire] :
( ( A = B )
& ( B != vqempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(195,axiom,
vmulop != vdivop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-divop') ).
thf(1396,plain,
vmulop != vdivop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[195]) ).
thf(80,axiom,
! [A: vQID,B: vAType,C: vATMap] :
( vatmempty
!= ( C @ ( B @ ( A @ vatmbind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-atmempty-atmbind') ).
thf(780,plain,
! [A: vQID,B: vAType,C: vATMap] :
( vatmempty
!= ( C @ ( B @ ( A @ vatmbind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(137,axiom,
! [A: vYN,B: vnat] :
( ( A @ vB )
!= ( B @ vNum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-B-Num') ).
thf(1015,plain,
! [A: vYN,B: vnat] :
( ( A @ vB )
!= ( B @ vNum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(163,axiom,
! [A: vAval,B: vAval] :
( ( ( A @ vconstant )
= ( B @ vconstant ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-constant') ).
thf(1176,plain,
! [A: vAval,B: vAval] :
( ( ( A @ vconstant )
= ( B @ vconstant ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[163]) ).
thf(209,axiom,
vltop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-ltop-orop') ).
thf(1477,plain,
vltop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[209]) ).
thf(99,axiom,
! [A: vATMap,B: vATMap,C: vAType,D: vLabel,E: vQID] :
( ( ( B @ ( E @ vlookupATMap ) )
= vnoAType )
=> ( A @ ( B @ ( C @ ( E @ vatmbind ) ) @ vMC ) @ ( C @ ( D @ ( E @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tquestion') ).
thf(851,plain,
! [A: vATMap,B: vATMap,C: vAType,D: vLabel,E: vQID] :
( ( ( B @ ( E @ vlookupATMap ) )
= vnoAType )
=> ( A @ ( B @ ( C @ ( E @ vatmbind ) ) @ vMC ) @ ( C @ ( D @ ( E @ vquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(59,axiom,
! [A: vQMap,B: vAType,C: vLabel,D: vAnsMap,E: vQID] :
( ( A @ ( D @ ( B @ ( C @ ( E @ vquestion ) ) @ vqsingle @ vreduce ) ) )
= ( vqempty @ ( A @ ( D @ ( B @ ( C @ vgetAnswer ) @ ( E @ vabind ) ) @ vQC ) ) @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-1') ).
thf(695,plain,
! [A: vQMap,B: vAType,C: vLabel,D: vAnsMap,E: vQID] :
( ( A @ ( D @ ( B @ ( C @ ( E @ vquestion ) ) @ vqsingle @ vreduce ) ) )
= ( vqempty @ ( A @ ( D @ ( B @ ( C @ vgetAnswer ) @ ( E @ vabind ) ) @ vQC ) ) @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(49,axiom,
~ ( vnoAval @ visSomeAval ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-0') ).
thf(636,plain,
~ ( vnoAval @ visSomeAval ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(146,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( ( C @ ( F @ ( D @ vquestion ) ) )
= ( E @ ( B @ ( A @ vquestion ) ) ) )
=> ( ( C = E )
& ( F = B )
& ( D = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-question') ).
thf(1044,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID,E: vAType,F: vLabel] :
( ( ( C @ ( F @ ( D @ vquestion ) ) )
= ( E @ ( B @ ( A @ vquestion ) ) ) )
=> ( ( C = E )
& ( F = B )
& ( D = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(16,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vsucc @ vgt ) )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt-1') ).
thf(431,plain,
! [A: vnat] :
( ( vzero @ ( A @ vsucc @ vgt ) )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(288,axiom,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vsubop @ vevalBinOp ) ) )
= ( B @ ( A @ vminus ) @ vNum @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-1') ).
thf(5139,plain,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vsubop @ vevalBinOp ) ) )
= ( B @ ( A @ vminus ) @ vNum @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[288]) ).
thf(22,axiom,
! [A: vnat] :
( ( A @ vsucc @ ( vzero @ vlt ) )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lt-1') ).
thf(473,plain,
! [A: vnat] :
( ( A @ vsucc @ ( vzero @ vlt ) )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(245,axiom,
! [A: vYN,B: vstring] :
( ( A @ vB )
!= ( B @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-B-T') ).
thf(1626,plain,
! [A: vYN,B: vstring] :
( ( A @ vB )
!= ( B @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[245]) ).
thf(179,axiom,
! [A: vQID,B: vAnsMap] :
( ? [C: vQID,D: vAval,E: vAnsMap,F: vQID] :
( ( ( B @ ( A @ vlookupAnsMap ) )
= ( E @ ( F @ vlookupAnsMap ) ) )
& ( B
= ( E @ ( D @ ( C @ vabind ) ) ) )
& ( A = F )
& ( F != C ) )
| ? [C: vQID,D: vAval,E: vAnsMap,F: vQID] :
( ( ( B @ ( A @ vlookupAnsMap ) )
= ( D @ vsomeAval ) )
& ( B
= ( E @ ( D @ ( C @ vabind ) ) ) )
& ( A = F )
& ( F = C ) )
| ? [C: vQID] :
( ( ( B @ ( A @ vlookupAnsMap ) )
= vnoAval )
& ( B = vaempty )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupAnsMap-INV') ).
thf(1304,plain,
! [A: vQID,B: vAnsMap] :
( ? [C: vQID,D: vAval,E: vAnsMap,F: vQID] :
( ( ( B @ ( A @ vlookupAnsMap ) )
= ( E @ ( F @ vlookupAnsMap ) ) )
& ( B
= ( E @ ( D @ ( C @ vabind ) ) ) )
& ( A = F )
& ( F != C ) )
| ? [C: vQID,D: vAval,E: vAnsMap,F: vQID] :
( ( ( B @ ( A @ vlookupAnsMap ) )
= ( D @ vsomeAval ) )
& ( B
= ( E @ ( D @ ( C @ vabind ) ) ) )
& ( A = F )
& ( F = C ) )
| ? [C: vQID] :
( ( ( B @ ( A @ vlookupAnsMap ) )
= vnoAval )
& ( B = vaempty )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(169,axiom,
! [A: vBinOpT,B: vAType,C: vAType] :
( ( ( A != veqop )
& ( ( C != vYesNo )
| ( B != vYesNo )
| ( A != vorop ) )
& ( ( C != vYesNo )
| ( B != vYesNo )
| ( A != vandop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vltop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vgtop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vdivop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vmulop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vsubop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vaddop ) ) )
=> ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-9') ).
thf(1203,plain,
! [A: vBinOpT,B: vAType,C: vAType] :
( ( ( A != veqop )
& ( ( C != vYesNo )
| ( B != vYesNo )
| ( A != vorop ) )
& ( ( C != vYesNo )
| ( B != vYesNo )
| ( A != vandop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vltop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vgtop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vdivop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vmulop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vsubop ) )
& ( ( C != vNumber )
| ( B != vNumber )
| ( A != vaddop ) ) )
=> ( ( C @ ( B @ ( A @ vcheckBinOp ) ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[169]) ).
thf(31,axiom,
vNumber != vText,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Number-Text') ).
thf(531,plain,
vNumber != vText,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(33,axiom,
! [A: vYN,B: vYN] :
( ( ( A @ vB )
= ( B @ vB ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-B') ).
thf(548,plain,
! [A: vYN,B: vYN] :
( ( ( A @ vB )
= ( B @ vB ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(44,axiom,
! [A: vQID,B: vQID] :
( ( ( A @ vask )
= ( B @ vask ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-ask') ).
thf(617,plain,
! [A: vQID,B: vQID] :
( ( ( A @ vask )
= ( B @ vask ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(34,axiom,
! [A: vYN,B: vYN] :
( ? [C: vYN,D: vYN] :
( ( ( B @ ( A @ vand ) )
= vno )
& ( B = D )
& ( A = C )
& ( ( D != vyes )
| ( C != vyes ) ) )
| ( ( ( B @ ( A @ vand ) )
= vyes )
& ( B = vyes )
& ( A = vyes ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and-INV') ).
thf(553,plain,
! [A: vYN,B: vYN] :
( ? [C: vYN,D: vYN] :
( ( ( B @ ( A @ vand ) )
= vno )
& ( B = D )
& ( A = C )
& ( ( D != vyes )
| ( C != vyes ) ) )
| ( ( ( B @ ( A @ vand ) )
= vyes )
& ( B = vyes )
& ( A = vyes ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(164,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( ( D @ ( C @ ( A @ vreduce ) ) @ visSomeQC )
& ! [E: vQuestionnaire] :
( ( B != E )
| ( A != vqempty ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ vqseq ) @ vreduce ) ) )
= ( B @ ( D @ ( C @ ( A @ vreduce ) ) @ vgetQC @ vqcappend ) @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-9') ).
thf(1181,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( ( D @ ( C @ ( A @ vreduce ) ) @ visSomeQC )
& ! [E: vQuestionnaire] :
( ( B != E )
| ( A != vqempty ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ vqseq ) @ vreduce ) ) )
= ( B @ ( D @ ( C @ ( A @ vreduce ) ) @ vgetQC @ vqcappend ) @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(228,axiom,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( ( ( A @ vgetQM )
= C )
& ( A
= ( D @ ( C @ ( B @ vQC ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQM-INV') ).
thf(1551,plain,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( ( ( A @ vgetQM )
= C )
& ( A
= ( D @ ( C @ ( B @ vQC ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[228]) ).
thf(83,axiom,
vaddop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-ltop') ).
thf(795,plain,
vaddop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(56,axiom,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) @ ( A @ vlookupQMap ) )
= ( C @ ( B @ ( A @ vsomeQuestion ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupQMap-1') ).
thf(680,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) @ ( A @ vlookupQMap ) )
= ( C @ ( B @ ( A @ vsomeQuestion ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(79,axiom,
! [A: vEntry,B: vQuestionnaire,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqseq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qsingle-qseq') ).
thf(776,plain,
! [A: vEntry,B: vQuestionnaire,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqseq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(337,axiom,
! [A: vQID,B: vAval,C: vAnsMap] :
( ( C @ ( B @ ( A @ vabind ) ) @ vtypeAM )
= ( C @ vtypeAM @ ( B @ vtypeOf @ ( A @ vatmbind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeAM-1') ).
thf(5624,plain,
! [A: vQID,B: vAval,C: vAnsMap] :
( ( C @ ( B @ ( A @ vabind ) ) @ vtypeAM )
= ( C @ vtypeAM @ ( B @ vtypeOf @ ( A @ vatmbind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[337]) ).
thf(140,axiom,
vaddop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-orop') ).
thf(1025,plain,
vaddop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(327,axiom,
! [A: vAnsMap,B: vAType,C: vExp] :
( ( ( ( A @ ( ve2 @ vreduceExp ) )
= ( C @ vsomeExp ) )
& ( ( ve2 @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) )
=> ( ( C @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExpPreservation-binop-IH1') ).
thf(5592,plain,
! [A: vAnsMap,B: vAType,C: vExp] :
( ( ( ( A @ ( ve2 @ vreduceExp ) )
= ( C @ vsomeExp ) )
& ( ( ve2 @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) )
=> ( ( C @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[327]) ).
thf(222,axiom,
! [A: vQID,B: vLabel,C: vAType] : ( C @ ( B @ ( A @ vsomeQuestion ) ) @ visSomeQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-1') ).
thf(1531,plain,
! [A: vQID,B: vLabel,C: vAType] : ( C @ ( B @ ( A @ vsomeQuestion ) ) @ visSomeQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[222]) ).
thf(62,axiom,
! [A: vATMap,B: vATMap] : ( B @ ( A @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqempty') ).
thf(705,plain,
! [A: vATMap,B: vATMap] : ( B @ ( A @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(240,axiom,
! [A: vAval] : ( A @ vsomeAval @ visSomeAval ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-1') ).
thf(1611,plain,
! [A: vAval] : ( A @ vsomeAval @ visSomeAval ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[240]) ).
thf(305,axiom,
! [A: vExp,B: vExp,C: vBinOpT,D: vAnsMap] :
( ( ( B @ vexpIsValue )
& ( A @ vexpIsValue ) )
=> ( ( D @ ( B @ ( C @ ( A @ vbinop ) ) @ vreduceExp ) )
= ( B @ vgetExpValue @ ( A @ vgetExpValue @ ( C @ vevalBinOp ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-3') ).
thf(5388,plain,
! [A: vExp,B: vExp,C: vBinOpT,D: vAnsMap] :
( ( ( B @ vexpIsValue )
& ( A @ vexpIsValue ) )
=> ( ( D @ ( B @ ( C @ ( A @ vbinop ) ) @ vreduceExp ) )
= ( B @ vgetExpValue @ ( A @ vgetExpValue @ ( C @ vevalBinOp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[305]) ).
thf(308,axiom,
! [A: vExp,B: vAnsMap] :
( ? [C: vUnOpT,D: vExp,E: vOptExp,F: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = F )
& ( A
= ( D @ ( C @ vunop ) ) )
& ~ ( E @ visSomeExp )
& ( E
= ( F @ ( D @ vreduceExp ) ) )
& ~ ( D @ vexpIsValue ) )
| ? [C: vUnOpT,D: vExp,E: vOptExp,F: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( E @ vgetExp @ ( C @ vunop ) @ vsomeExp ) )
& ( B = F )
& ( A
= ( D @ ( C @ vunop ) ) )
& ( E @ visSomeExp )
& ( E
= ( F @ ( D @ vreduceExp ) ) )
& ~ ( D @ vexpIsValue ) )
| ? [C: vUnOpT,D: vExp,E: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( D @ vgetExpValue @ ( C @ vevalUnOp ) ) )
& ( B = E )
& ( A
= ( D @ ( C @ vunop ) ) )
& ( D @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ~ ( D @ visSomeExp )
& ( D
= ( E @ ( C @ vreduceExp ) ) )
& ~ ( C @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= ( F @ ( G @ ( D @ vgetExp @ vbinop ) ) @ vsomeExp ) )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ( D @ visSomeExp )
& ( D
= ( E @ ( C @ vreduceExp ) ) )
& ~ ( C @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ~ ( D @ visSomeExp )
& ( D
= ( E @ ( F @ vreduceExp ) ) )
& ~ ( F @ vexpIsValue )
& ( C @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= ( D @ vgetExp @ ( G @ ( C @ vbinop ) ) @ vsomeExp ) )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ( D @ visSomeExp )
& ( D
= ( E @ ( F @ vreduceExp ) ) )
& ~ ( F @ vexpIsValue )
& ( C @ vexpIsValue ) )
| ? [C: vExp,D: vBinOpT,E: vExp,F: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( E @ vgetExpValue @ ( C @ vgetExpValue @ ( D @ vevalBinOp ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vbinop ) ) ) )
& ( E @ vexpIsValue )
& ( C @ vexpIsValue ) )
| ? [C: vQID,D: vOptAval,E: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = E )
& ( A
= ( C @ vqvar ) )
& ~ ( D @ visSomeAval )
& ( D
= ( E @ ( C @ vlookupAnsMap ) ) ) )
| ? [C: vQID,D: vOptAval,E: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( D @ vgetAval @ vconstant @ vsomeExp ) )
& ( B = E )
& ( A
= ( C @ vqvar ) )
& ( D @ visSomeAval )
& ( D
= ( E @ ( C @ vlookupAnsMap ) ) ) )
| ? [C: vAval,D: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = D )
& ( A
= ( C @ vconstant ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-INV') ).
thf(5399,plain,
! [A: vExp,B: vAnsMap] :
( ? [C: vUnOpT,D: vExp,E: vOptExp,F: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = F )
& ( A
= ( D @ ( C @ vunop ) ) )
& ~ ( E @ visSomeExp )
& ( E
= ( F @ ( D @ vreduceExp ) ) )
& ~ ( D @ vexpIsValue ) )
| ? [C: vUnOpT,D: vExp,E: vOptExp,F: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( E @ vgetExp @ ( C @ vunop ) @ vsomeExp ) )
& ( B = F )
& ( A
= ( D @ ( C @ vunop ) ) )
& ( E @ visSomeExp )
& ( E
= ( F @ ( D @ vreduceExp ) ) )
& ~ ( D @ vexpIsValue ) )
| ? [C: vUnOpT,D: vExp,E: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( D @ vgetExpValue @ ( C @ vevalUnOp ) ) )
& ( B = E )
& ( A
= ( D @ ( C @ vunop ) ) )
& ( D @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ~ ( D @ visSomeExp )
& ( D
= ( E @ ( C @ vreduceExp ) ) )
& ~ ( C @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= ( F @ ( G @ ( D @ vgetExp @ vbinop ) ) @ vsomeExp ) )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ( D @ visSomeExp )
& ( D
= ( E @ ( C @ vreduceExp ) ) )
& ~ ( C @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ~ ( D @ visSomeExp )
& ( D
= ( E @ ( F @ vreduceExp ) ) )
& ~ ( F @ vexpIsValue )
& ( C @ vexpIsValue ) )
| ? [C: vExp,D: vOptExp,E: vAnsMap,F: vExp,G: vBinOpT] :
( ( ( B @ ( A @ vreduceExp ) )
= ( D @ vgetExp @ ( G @ ( C @ vbinop ) ) @ vsomeExp ) )
& ( B = E )
& ( A
= ( F @ ( G @ ( C @ vbinop ) ) ) )
& ( D @ visSomeExp )
& ( D
= ( E @ ( F @ vreduceExp ) ) )
& ~ ( F @ vexpIsValue )
& ( C @ vexpIsValue ) )
| ? [C: vExp,D: vBinOpT,E: vExp,F: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( E @ vgetExpValue @ ( C @ vgetExpValue @ ( D @ vevalBinOp ) ) ) )
& ( B = F )
& ( A
= ( E @ ( D @ ( C @ vbinop ) ) ) )
& ( E @ vexpIsValue )
& ( C @ vexpIsValue ) )
| ? [C: vQID,D: vOptAval,E: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = E )
& ( A
= ( C @ vqvar ) )
& ~ ( D @ visSomeAval )
& ( D
= ( E @ ( C @ vlookupAnsMap ) ) ) )
| ? [C: vQID,D: vOptAval,E: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= ( D @ vgetAval @ vconstant @ vsomeExp ) )
& ( B = E )
& ( A
= ( C @ vqvar ) )
& ( D @ visSomeAval )
& ( D
= ( E @ ( C @ vlookupAnsMap ) ) ) )
| ? [C: vAval,D: vAnsMap] :
( ( ( B @ ( A @ vreduceExp ) )
= vnoExp )
& ( B = D )
& ( A
= ( C @ vconstant ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[308]) ).
thf(63,axiom,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vQC ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-QConf') ).
thf(707,plain,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vQC ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(216,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( E
= ( B @ ( D @ ( F @ vatmbind ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tvalue_inv3') ).
thf(1499,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( E
= ( B @ ( D @ ( F @ vatmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[216]) ).
thf(82,axiom,
! [A: vEntry] :
( vqempty
!= ( A @ vqsingle ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qsingle') ).
thf(791,plain,
! [A: vEntry] :
( vqempty
!= ( A @ vqsingle ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(165,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tvalue_inv4') ).
thf(1188,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID,G: vExp] :
( ( C @ ( E @ vMC ) @ ( G @ ( D @ ( F @ vvalue ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( C = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[165]) ).
thf(19,axiom,
! [A: vAval] :
( vnoAval
!= ( A @ vsomeAval ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noAval-someAval') ).
thf(441,plain,
! [A: vAval] :
( vnoAval
!= ( A @ vsomeAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(144,axiom,
vYesNo != vNumber,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-YesNo-Number') ).
thf(1038,plain,
vYesNo != vNumber,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(254,axiom,
( ( vYesNo @ ( vYesNo @ ( vorop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-7') ).
thf(1679,plain,
( ( vYesNo @ ( vYesNo @ ( vorop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[254]) ).
thf(116,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionAType )
= C ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuestionAType-0') ).
thf(907,plain,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionAType )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(154,axiom,
vdivop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-eqop') ).
thf(1130,plain,
vdivop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(233,axiom,
! [A: vQID,B: vAval,C: vAnsMap,D: vAnsMap] :
( ( D @ ( C @ ( B @ ( A @ vabind ) ) @ vappendAnsMap ) )
= ( D @ ( C @ vappendAnsMap ) @ ( B @ ( A @ vabind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendAnsMap-1') ).
thf(1579,plain,
! [A: vQID,B: vAval,C: vAnsMap,D: vAnsMap] :
( ( D @ ( C @ ( B @ ( A @ vabind ) ) @ vappendAnsMap ) )
= ( D @ ( C @ vappendAnsMap ) @ ( B @ ( A @ vabind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[233]) ).
thf(198,axiom,
vgtop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-gtop-orop') ).
thf(1404,plain,
vgtop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[198]) ).
thf(71,axiom,
! [A: vAType] :
( ( A = vText )
| ( A = vNumber )
| ( A = vYesNo ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-AType') ).
thf(744,plain,
! [A: vAType] :
( ( A = vText )
| ( A = vNumber )
| ( A = vYesNo ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(182,axiom,
vdivop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-ltop') ).
thf(1353,plain,
vdivop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[182]) ).
thf(135,axiom,
! [A: vGID,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qgroup') ).
thf(1008,plain,
! [A: vGID,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(278,axiom,
! [A: vATMap,B: vExp,C: vExp,D: vBinOpT] :
( ( ( C @ ( A @ vecheck ) @ visSomeAType )
& ( B @ ( A @ vecheck ) @ visSomeAType ) )
=> ( ( C @ ( D @ ( B @ vbinop ) ) @ ( A @ vecheck ) )
= ( C @ ( A @ vecheck ) @ vgetAType @ ( B @ ( A @ vecheck ) @ vgetAType @ ( D @ vcheckBinOp ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-4') ).
thf(1881,plain,
! [A: vATMap,B: vExp,C: vExp,D: vBinOpT] :
( ( ( C @ ( A @ vecheck ) @ visSomeAType )
& ( B @ ( A @ vecheck ) @ visSomeAType ) )
=> ( ( C @ ( D @ ( B @ vbinop ) ) @ ( A @ vecheck ) )
= ( C @ ( A @ vecheck ) @ vgetAType @ ( B @ ( A @ vecheck ) @ vgetAType @ ( D @ vcheckBinOp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[278]) ).
thf(242,axiom,
vsubop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-eqop') ).
thf(1617,plain,
vsubop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[242]) ).
thf(97,axiom,
! [A: vUnOpT] : ( A = vnotop ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-UnOpT') ).
thf(845,plain,
! [A: vUnOpT] : ( A = vnotop ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(296,axiom,
! [A: vYN] :
( ( A @ vB @ ( vnotop @ vevalUnOp ) )
= ( A @ vnot @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalUnOp-0') ).
thf(5179,plain,
! [A: vYN] :
( ( A @ vB @ ( vnotop @ vevalUnOp ) )
= ( A @ vnot @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[296]) ).
thf(304,axiom,
( ( vNumber @ ( vNumber @ ( vsubop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-1') ).
thf(5386,plain,
( ( vNumber @ ( vNumber @ ( vsubop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[304]) ).
thf(249,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vExp,D: vQuestionnaire,E: vQuestionnaire,F: vExp] :
( ( ( D @ ( E @ ( F @ vqcond ) ) )
= ( B @ ( A @ ( C @ vqcond ) ) ) )
=> ( ( D = B )
& ( E = A )
& ( F = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qcond') ).
thf(1654,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vExp,D: vQuestionnaire,E: vQuestionnaire,F: vExp] :
( ( ( D @ ( E @ ( F @ vqcond ) ) )
= ( B @ ( A @ ( C @ vqcond ) ) ) )
=> ( ( D = B )
& ( E = A )
& ( F = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[249]) ).
thf(75,axiom,
vsubop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-gtop') ).
thf(759,plain,
vsubop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(7,axiom,
! [A: vnat] :
( ? [B: vnat] :
( A
= ( B @ vsucc ) )
| ( A = vzero ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-nat') ).
thf(368,plain,
! [A: vnat] :
( ? [B: vnat] :
( A
= ( B @ vsucc ) )
| ( A = vzero ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(193,axiom,
vsubop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-andop') ).
thf(1390,plain,
vsubop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[193]) ).
thf(285,axiom,
! [A: vExp,B: vUnOpT,C: vAnsMap] :
( ( A @ vexpIsValue )
=> ( ( C @ ( A @ ( B @ vunop ) @ vreduceExp ) )
= ( A @ vgetExpValue @ ( B @ vevalUnOp ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-8') ).
thf(5124,plain,
! [A: vExp,B: vUnOpT,C: vAnsMap] :
( ( A @ vexpIsValue )
=> ( ( C @ ( A @ ( B @ vunop ) @ vreduceExp ) )
= ( A @ vgetExpValue @ ( B @ vevalUnOp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[285]) ).
thf(175,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vlt ) )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lt-0') ).
thf(1276,plain,
! [A: vnat] :
( ( vzero @ ( A @ vlt ) )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
thf(170,axiom,
! [A: vEntry,B: vEntry] :
( ( ( A @ vqsingle )
= ( B @ vqsingle ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qsingle') ).
thf(1253,plain,
! [A: vEntry,B: vEntry] :
( ( ( A @ vqsingle )
= ( B @ vqsingle ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[170]) ).
thf(252,axiom,
( ( vYesNo @ ( vnotop @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-0') ).
thf(1674,plain,
( ( vYesNo @ ( vnotop @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[252]) ).
thf(269,axiom,
! [A: vAType,B: vAType] :
( ( B @ ( A @ ( veqop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-8') ).
thf(1854,plain,
! [A: vAType,B: vAType] :
( ( B @ ( A @ ( veqop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[269]) ).
thf(330,axiom,
! [A: vATMap,B: vExp,C: vUnOpT] :
( ~ ( B @ ( A @ vecheck ) @ visSomeAType )
=> ( ( B @ ( C @ vunop ) @ ( A @ vecheck ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-7') ).
thf(5600,plain,
! [A: vATMap,B: vExp,C: vUnOpT] :
( ~ ( B @ ( A @ vecheck ) @ visSomeAType )
=> ( ( B @ ( C @ vunop ) @ ( A @ vecheck ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[330]) ).
thf(218,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus-1') ).
thf(1508,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[218]) ).
thf(287,axiom,
! [A: vATMap,B: vExp,C: vExp,D: vBinOpT] :
( ~ ( ( C @ ( A @ vecheck ) @ visSomeAType )
& ( B @ ( A @ vecheck ) @ visSomeAType ) )
=> ( ( C @ ( D @ ( B @ vbinop ) ) @ ( A @ vecheck ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-5') ).
thf(5132,plain,
! [A: vATMap,B: vExp,C: vExp,D: vBinOpT] :
( ~ ( ( C @ ( A @ vecheck ) @ visSomeAType )
& ( B @ ( A @ vecheck ) @ visSomeAType ) )
=> ( ( C @ ( D @ ( B @ vbinop ) ) @ ( A @ vecheck ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[287]) ).
thf(131,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQuest )
= C ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuest-0') ).
thf(995,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQuest )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(229,axiom,
vaddop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-andop') ).
thf(1558,plain,
vaddop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[229]) ).
thf(272,axiom,
! [A: vAval] : ( A @ vconstant @ vexpIsValue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-0') ).
thf(1861,plain,
! [A: vAval] : ( A @ vconstant @ vexpIsValue ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[272]) ).
thf(257,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID] :
( ( ( ( A @ ( F @ vlookupATMap ) )
= ( D @ vsomeAType ) )
& ( C @ ( E @ vMC ) @ ( F @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) )
=> ( E
= ( B @ ( D @ ( F @ vatmbind ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Task_inv3') ).
thf(1689,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vATMap,F: vQID] :
( ( ( ( A @ ( F @ vlookupATMap ) )
= ( D @ vsomeAType ) )
& ( C @ ( E @ vMC ) @ ( F @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) ) )
=> ( E
= ( B @ ( D @ ( F @ vatmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[257]) ).
thf(28,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vGID,D: vQuestionnaire] :
( ( B @ ( A @ vqseq ) )
!= ( D @ ( C @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qseq-qgroup') ).
thf(510,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vGID,D: vQuestionnaire] :
( ( B @ ( A @ vqseq ) )
!= ( D @ ( C @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(260,axiom,
! [A: vAval,B: vAnsMap] :
( ( B @ ( A @ vconstant @ vreduceExp ) )
= vnoExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-0') ).
thf(1706,plain,
! [A: vAval,B: vAnsMap] :
( ( B @ ( A @ vconstant @ vreduceExp ) )
= vnoExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[260]) ).
thf(320,axiom,
! [A: vQMap,B: vQuestionnaire,C: vExp,D: vAnsMap,E: vQuestionnaire] :
( ( ( D @ ( C @ vreduceExp ) @ visSomeExp )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vno @ vB @ vconstant ) ) )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vyes @ vB @ vconstant ) ) ) )
=> ( ( A @ ( D @ ( E @ ( B @ ( C @ vqcond ) ) @ vreduce ) ) )
= ( E @ ( B @ ( D @ ( C @ vreduceExp ) @ vgetExp @ vqcond ) ) @ ( A @ ( D @ vQC ) ) @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-13') ).
thf(5549,plain,
! [A: vQMap,B: vQuestionnaire,C: vExp,D: vAnsMap,E: vQuestionnaire] :
( ( ( D @ ( C @ vreduceExp ) @ visSomeExp )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vno @ vB @ vconstant ) ) )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vyes @ vB @ vconstant ) ) ) )
=> ( ( A @ ( D @ ( E @ ( B @ ( C @ vqcond ) ) @ vreduce ) ) )
= ( E @ ( B @ ( D @ ( C @ vreduceExp ) @ vgetExp @ vqcond ) ) @ ( A @ ( D @ vQC ) ) @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[320]) ).
thf(290,axiom,
! [A: vExp,B: vAnsMap,C: vBinOpT,D: vExp] :
( ( ~ ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( D @ ( C @ ( A @ vbinop ) ) @ vreduceExp ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-7') ).
thf(5144,plain,
! [A: vExp,B: vAnsMap,C: vBinOpT,D: vExp] :
( ( ~ ( B @ ( A @ vreduceExp ) @ visSomeExp )
& ~ ( A @ vexpIsValue ) )
=> ( ( B @ ( D @ ( C @ ( A @ vbinop ) ) @ vreduceExp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[290]) ).
thf(281,axiom,
! [A: vQuestionnaire,B: vAnsMap,C: vQMap] :
( ? [D: vGID,E: vQuestionnaire,F: vAnsMap,G: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( E @ ( G @ ( F @ vQC ) ) @ vsomeQConf ) )
& ( C = G )
& ( B = F )
& ( A
= ( E @ ( D @ vqgroup ) ) ) )
| ? [D: vQMap,E: vOptExp,F: vQuestionnaire,G: vExp,H: vAnsMap,I: vQuestionnaire] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = D )
& ( B = H )
& ( A
= ( I @ ( F @ ( G @ vqcond ) ) ) )
& ~ ( E @ visSomeExp )
& ( E
= ( H @ ( G @ vreduceExp ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vno @ vB @ vconstant ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vyes @ vB @ vconstant ) ) ) )
| ? [D: vQMap,E: vOptExp,F: vQuestionnaire,G: vExp,H: vAnsMap,I: vQuestionnaire] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( I @ ( F @ ( E @ vgetExp @ vqcond ) ) @ ( D @ ( H @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = H )
& ( A
= ( I @ ( F @ ( G @ vqcond ) ) ) )
& ( E @ visSomeExp )
& ( E
= ( H @ ( G @ vreduceExp ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vno @ vB @ vconstant ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vyes @ vB @ vconstant ) ) ) )
| ? [D: vQuestionnaire,E: vQuestionnaire,F: vAnsMap,G: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( E @ ( G @ ( F @ vQC ) ) @ vsomeQConf ) )
& ( C = G )
& ( B = F )
& ( A
= ( E @ ( D @ ( vno @ vB @ vconstant @ vqcond ) ) ) ) )
| ? [D: vQuestionnaire,E: vQuestionnaire,F: vAnsMap,G: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( D @ ( G @ ( F @ vQC ) ) @ vsomeQConf ) )
& ( C = G )
& ( B = F )
& ( A
= ( E @ ( D @ ( vyes @ vB @ vconstant @ vqcond ) ) ) ) )
| ? [D: vQMap,E: vQuestionnaire,F: vAnsMap,G: vQuestionnaire,H: vOptQConf] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = D )
& ( B = F )
& ( A
= ( G @ ( E @ vqseq ) ) )
& ~ ( H @ visSomeQC )
& ( H
= ( D @ ( F @ ( E @ vreduce ) ) ) )
& ! [I: vQuestionnaire] :
( ( G != I )
| ( E != vqempty ) ) )
| ? [D: vQMap,E: vQuestionnaire,F: vAnsMap,G: vQuestionnaire,H: vOptQConf] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( G @ ( H @ vgetQC @ vqcappend ) @ vsomeQConf ) )
& ( C = D )
& ( B = F )
& ( A
= ( G @ ( E @ vqseq ) ) )
& ( H @ visSomeQC )
& ( H
= ( D @ ( F @ ( E @ vreduce ) ) ) )
& ! [I: vQuestionnaire] :
( ( G != I )
| ( E != vqempty ) ) )
| ? [D: vQuestionnaire,E: vAnsMap,F: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( D @ ( F @ ( E @ vQC ) ) @ vsomeQConf ) )
& ( C = F )
& ( B = E )
& ( A
= ( D @ ( vqempty @ vqseq ) ) ) )
| ? [D: vQID,E: vOptQuestion,F: vQMap,G: vAnsMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = F )
& ( B = G )
& ( A
= ( D @ vask @ vqsingle ) )
& ~ ( E @ visSomeQuestion )
& ( E
= ( F @ ( D @ vlookupQMap ) ) ) )
| ? [D: vQID,E: vOptQuestion,F: vQMap,G: vAnsMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( E @ vgetQuestionAType @ ( E @ vgetQuestionLabel @ ( D @ vquestion ) ) @ vqsingle @ ( F @ ( G @ vQC ) ) @ vsomeQConf ) )
& ( C = F )
& ( B = G )
& ( A
= ( D @ vask @ vqsingle ) )
& ( E @ visSomeQuestion )
& ( E
= ( F @ ( D @ vlookupQMap ) ) ) )
| ? [D: vQMap,E: vAType,F: vLabel,G: vAnsMap,H: vQID] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( vqempty @ ( D @ ( E @ ( F @ ( H @ vqmbind ) ) ) @ ( G @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = G )
& ( A
= ( E @ ( F @ ( H @ vdefquestion ) ) @ vqsingle ) ) )
| ? [D: vQMap,E: vAType,F: vOptExp,G: vAnsMap,H: vQID,I: vExp] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = D )
& ( B = G )
& ( A
= ( I @ ( E @ ( H @ vvalue ) ) @ vqsingle ) )
& ~ ( F @ visSomeExp )
& ( F
= ( G @ ( I @ vreduceExp ) ) )
& ~ ( I @ vexpIsValue ) )
| ? [D: vQMap,E: vAType,F: vOptExp,G: vAnsMap,H: vQID,I: vExp] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( F @ vgetExp @ ( E @ ( H @ vvalue ) ) @ vqsingle @ ( D @ ( G @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = G )
& ( A
= ( I @ ( E @ ( H @ vvalue ) ) @ vqsingle ) )
& ( F @ visSomeExp )
& ( F
= ( G @ ( I @ vreduceExp ) ) )
& ~ ( I @ vexpIsValue ) )
| ? [D: vQMap,E: vAType,F: vAnsMap,G: vQID,H: vExp] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( vqempty @ ( D @ ( F @ ( H @ vgetExpValue @ ( G @ vabind ) ) @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = F )
& ( A
= ( H @ ( E @ ( G @ vvalue ) ) @ vqsingle ) )
& ( H @ vexpIsValue ) )
| ? [D: vQMap,E: vAType,F: vLabel,G: vAval,H: vAnsMap,I: vQID] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( vqempty @ ( D @ ( H @ ( G @ ( I @ vabind ) ) @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = H )
& ( A
= ( E @ ( F @ ( I @ vquestion ) ) @ vqsingle ) )
& ( G
= ( E @ ( F @ vgetAnswer ) ) ) )
| ? [D: vAnsMap,E: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = E )
& ( B = D )
& ( A = vqempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-INV') ).
thf(1893,plain,
! [A: vQuestionnaire,B: vAnsMap,C: vQMap] :
( ? [D: vGID,E: vQuestionnaire,F: vAnsMap,G: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( E @ ( G @ ( F @ vQC ) ) @ vsomeQConf ) )
& ( C = G )
& ( B = F )
& ( A
= ( E @ ( D @ vqgroup ) ) ) )
| ? [D: vQMap,E: vOptExp,F: vQuestionnaire,G: vExp,H: vAnsMap,I: vQuestionnaire] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = D )
& ( B = H )
& ( A
= ( I @ ( F @ ( G @ vqcond ) ) ) )
& ~ ( E @ visSomeExp )
& ( E
= ( H @ ( G @ vreduceExp ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vno @ vB @ vconstant ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vyes @ vB @ vconstant ) ) ) )
| ? [D: vQMap,E: vOptExp,F: vQuestionnaire,G: vExp,H: vAnsMap,I: vQuestionnaire] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( I @ ( F @ ( E @ vgetExp @ vqcond ) ) @ ( D @ ( H @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = H )
& ( A
= ( I @ ( F @ ( G @ vqcond ) ) ) )
& ( E @ visSomeExp )
& ( E
= ( H @ ( G @ vreduceExp ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vno @ vB @ vconstant ) ) )
& ! [J: vQuestionnaire,K: vQuestionnaire] :
( ( I != K )
| ( F != J )
| ( G
!= ( vyes @ vB @ vconstant ) ) ) )
| ? [D: vQuestionnaire,E: vQuestionnaire,F: vAnsMap,G: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( E @ ( G @ ( F @ vQC ) ) @ vsomeQConf ) )
& ( C = G )
& ( B = F )
& ( A
= ( E @ ( D @ ( vno @ vB @ vconstant @ vqcond ) ) ) ) )
| ? [D: vQuestionnaire,E: vQuestionnaire,F: vAnsMap,G: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( D @ ( G @ ( F @ vQC ) ) @ vsomeQConf ) )
& ( C = G )
& ( B = F )
& ( A
= ( E @ ( D @ ( vyes @ vB @ vconstant @ vqcond ) ) ) ) )
| ? [D: vQMap,E: vQuestionnaire,F: vAnsMap,G: vQuestionnaire,H: vOptQConf] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = D )
& ( B = F )
& ( A
= ( G @ ( E @ vqseq ) ) )
& ~ ( H @ visSomeQC )
& ( H
= ( D @ ( F @ ( E @ vreduce ) ) ) )
& ! [I: vQuestionnaire] :
( ( G != I )
| ( E != vqempty ) ) )
| ? [D: vQMap,E: vQuestionnaire,F: vAnsMap,G: vQuestionnaire,H: vOptQConf] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( G @ ( H @ vgetQC @ vqcappend ) @ vsomeQConf ) )
& ( C = D )
& ( B = F )
& ( A
= ( G @ ( E @ vqseq ) ) )
& ( H @ visSomeQC )
& ( H
= ( D @ ( F @ ( E @ vreduce ) ) ) )
& ! [I: vQuestionnaire] :
( ( G != I )
| ( E != vqempty ) ) )
| ? [D: vQuestionnaire,E: vAnsMap,F: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( D @ ( F @ ( E @ vQC ) ) @ vsomeQConf ) )
& ( C = F )
& ( B = E )
& ( A
= ( D @ ( vqempty @ vqseq ) ) ) )
| ? [D: vQID,E: vOptQuestion,F: vQMap,G: vAnsMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = F )
& ( B = G )
& ( A
= ( D @ vask @ vqsingle ) )
& ~ ( E @ visSomeQuestion )
& ( E
= ( F @ ( D @ vlookupQMap ) ) ) )
| ? [D: vQID,E: vOptQuestion,F: vQMap,G: vAnsMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( E @ vgetQuestionAType @ ( E @ vgetQuestionLabel @ ( D @ vquestion ) ) @ vqsingle @ ( F @ ( G @ vQC ) ) @ vsomeQConf ) )
& ( C = F )
& ( B = G )
& ( A
= ( D @ vask @ vqsingle ) )
& ( E @ visSomeQuestion )
& ( E
= ( F @ ( D @ vlookupQMap ) ) ) )
| ? [D: vQMap,E: vAType,F: vLabel,G: vAnsMap,H: vQID] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( vqempty @ ( D @ ( E @ ( F @ ( H @ vqmbind ) ) ) @ ( G @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = G )
& ( A
= ( E @ ( F @ ( H @ vdefquestion ) ) @ vqsingle ) ) )
| ? [D: vQMap,E: vAType,F: vOptExp,G: vAnsMap,H: vQID,I: vExp] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = D )
& ( B = G )
& ( A
= ( I @ ( E @ ( H @ vvalue ) ) @ vqsingle ) )
& ~ ( F @ visSomeExp )
& ( F
= ( G @ ( I @ vreduceExp ) ) )
& ~ ( I @ vexpIsValue ) )
| ? [D: vQMap,E: vAType,F: vOptExp,G: vAnsMap,H: vQID,I: vExp] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( F @ vgetExp @ ( E @ ( H @ vvalue ) ) @ vqsingle @ ( D @ ( G @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = G )
& ( A
= ( I @ ( E @ ( H @ vvalue ) ) @ vqsingle ) )
& ( F @ visSomeExp )
& ( F
= ( G @ ( I @ vreduceExp ) ) )
& ~ ( I @ vexpIsValue ) )
| ? [D: vQMap,E: vAType,F: vAnsMap,G: vQID,H: vExp] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( vqempty @ ( D @ ( F @ ( H @ vgetExpValue @ ( G @ vabind ) ) @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = F )
& ( A
= ( H @ ( E @ ( G @ vvalue ) ) @ vqsingle ) )
& ( H @ vexpIsValue ) )
| ? [D: vQMap,E: vAType,F: vLabel,G: vAval,H: vAnsMap,I: vQID] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= ( vqempty @ ( D @ ( H @ ( G @ ( I @ vabind ) ) @ vQC ) ) @ vsomeQConf ) )
& ( C = D )
& ( B = H )
& ( A
= ( E @ ( F @ ( I @ vquestion ) ) @ vqsingle ) )
& ( G
= ( E @ ( F @ vgetAnswer ) ) ) )
| ? [D: vAnsMap,E: vQMap] :
( ( ( C @ ( B @ ( A @ vreduce ) ) )
= vnoQConf )
& ( C = E )
& ( B = D )
& ( A = vqempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[281]) ).
thf(286,axiom,
! [A: vExp,B: vUnOpT,C: vExp,D: vExp,E: vBinOpT] :
( ( A @ ( E @ ( D @ vbinop ) ) )
!= ( C @ ( B @ vunop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-binop-unop') ).
thf(5128,plain,
! [A: vExp,B: vUnOpT,C: vExp,D: vExp,E: vBinOpT] :
( ( A @ ( E @ ( D @ vbinop ) ) )
!= ( C @ ( B @ vunop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[286]) ).
thf(295,axiom,
! [A: vQMap,B: vQuestionnaire,C: vExp,D: vAnsMap,E: vQuestionnaire] :
( ( ~ ( D @ ( C @ vreduceExp ) @ visSomeExp )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vno @ vB @ vconstant ) ) )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vyes @ vB @ vconstant ) ) ) )
=> ( ( A @ ( D @ ( E @ ( B @ ( C @ vqcond ) ) @ vreduce ) ) )
= vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-14') ).
thf(5164,plain,
! [A: vQMap,B: vQuestionnaire,C: vExp,D: vAnsMap,E: vQuestionnaire] :
( ( ~ ( D @ ( C @ vreduceExp ) @ visSomeExp )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vno @ vB @ vconstant ) ) )
& ! [F: vQuestionnaire,G: vQuestionnaire] :
( ( E != G )
| ( B != F )
| ( C
!= ( vyes @ vB @ vconstant ) ) ) )
=> ( ( A @ ( D @ ( E @ ( B @ ( C @ vqcond ) ) @ vreduce ) ) )
= vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[295]) ).
thf(119,axiom,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vmultiply ) )
= ( C @ ( D @ vmultiply ) @ ( D @ vplus ) ) )
& ( B
= ( C @ vsucc ) )
& ( A = D ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vmultiply ) )
= vzero )
& ( B = vzero )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','multiply-INV') ).
thf(914,plain,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vmultiply ) )
= ( C @ ( D @ vmultiply ) @ ( D @ vplus ) ) )
& ( B
= ( C @ vsucc ) )
& ( A = D ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vmultiply ) )
= vzero )
& ( B = vzero )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(204,axiom,
! [A: vQID,B: vATMap,C: vATMap,D: vAType,E: vQID,F: vAType] :
( ( ( C @ ( D @ ( E @ vatmbind ) ) )
= ( B @ ( F @ ( A @ vatmbind ) ) ) )
=> ( ( C = B )
& ( D = F )
& ( E = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-atmbind') ).
thf(1440,plain,
! [A: vQID,B: vATMap,C: vATMap,D: vAType,E: vQID,F: vAType] :
( ( ( C @ ( D @ ( E @ vatmbind ) ) )
= ( B @ ( F @ ( A @ vatmbind ) ) ) )
=> ( ( C = B )
& ( D = F )
& ( E = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[204]) ).
thf(120,axiom,
vmulop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-orop') ).
thf(929,plain,
vmulop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(155,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap] :
( ( ( B @ ( A @ vMC ) )
= ( D @ ( C @ vMC ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-MC') ).
thf(1133,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap] :
( ( ( B @ ( A @ vMC ) )
= ( D @ ( C @ vMC ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(266,axiom,
! [A: vAnsMap,B: vAType,C: vExp] :
( ( ( ( A @ ( ve1 @ vreduceExp ) )
= ( C @ vsomeExp ) )
& ( ( ve1 @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) )
=> ( ( C @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExpPreservation-binop-IH0') ).
thf(1725,plain,
! [A: vAnsMap,B: vAType,C: vExp] :
( ( ( ( A @ ( ve1 @ vreduceExp ) )
= ( C @ vsomeExp ) )
& ( ( ve1 @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) )
=> ( ( C @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[266]) ).
thf(94,axiom,
! [A: vLabel] :
( ( vYesNo @ ( A @ vgetAnswer ) )
= ( A @ vaskYesNo @ vB ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-0') ).
thf(835,plain,
! [A: vLabel] :
( ( vYesNo @ ( A @ vgetAnswer ) )
= ( A @ vaskYesNo @ vB ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(100,axiom,
veqop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-gtop') ).
thf(854,plain,
veqop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(311,axiom,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ( ( F @ ( C @ vecheck ) )
= ( vYesNo @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond_inv1') ).
thf(5522,plain,
! [A: vATMap,B: vQuestionnaire,C: vATMap,D: vATMap,E: vATMap,F: vExp,G: vQuestionnaire] :
( ( E @ ( D @ vMC ) @ ( G @ ( B @ ( F @ vqcond ) ) @ ( A @ ( C @ vMC ) @ vptcheck ) ) )
=> ( ( F @ ( C @ vecheck ) )
= ( vYesNo @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[311]) ).
thf(210,axiom,
! [A: vOptQuestion] :
( ( A @ visSomeQuestion )
=> ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vsomeQuestion ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-true-INV') ).
thf(1480,plain,
! [A: vOptQuestion] :
( ( A @ visSomeQuestion )
=> ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vsomeQuestion ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[210]) ).
thf(40,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vExp,K: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( K @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( K @ ( D @ ( J @ vqcond ) ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( F = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqcond_inv5') ).
thf(603,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vExp,K: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( K @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( K @ ( D @ ( J @ vqcond ) ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( F = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(68,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetAM )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAM-0') ).
thf(735,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetAM )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(90,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( J @ ( F @ ( H @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( J @ ( D @ vqseq ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( G = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqseq_inv3') ).
thf(818,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vQuestionnaire,E: vATMap,F: vATMap,G: vATMap,H: vATMap,I: vATMap,J: vQuestionnaire] :
( ( ( C @ ( B @ vMC ) @ ( J @ ( F @ ( H @ vMC ) @ vptcheck ) ) )
& ( F @ ( H @ vMC ) @ ( D @ ( A @ ( E @ vMC ) @ vptcheck ) ) )
& ( I @ ( G @ vMC ) @ ( J @ ( D @ vqseq ) @ ( A @ ( E @ vMC ) @ vptcheck ) ) ) )
=> ( G = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(316,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap,E: vQID] :
( ( C @ ( D @ vMC ) @ ( E @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ? [F: vAType] :
( ( A @ ( E @ vlookupATMap ) )
= ( F @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Task_inv2') ).
thf(5537,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vATMap,E: vQID] :
( ( C @ ( D @ vMC ) @ ( E @ vask @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ? [F: vAType] :
( ( A @ ( E @ vlookupATMap ) )
= ( F @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[316]) ).
thf(271,axiom,
( ( vNumber @ ( vNumber @ ( vltop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-5') ).
thf(1859,plain,
( ( vNumber @ ( vNumber @ ( vltop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[271]) ).
thf(85,axiom,
! [A: vnat,B: vnat] :
( ( ( B @ ( A @ vgt ) )
!= vyes )
=> ( ( B @ ( A @ vdivide ) )
= vzero ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','divide-1') ).
thf(801,plain,
! [A: vnat,B: vnat] :
( ( ( B @ ( A @ vgt ) )
!= vyes )
=> ( ( B @ ( A @ vdivide ) )
= vzero ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(185,axiom,
vsubop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-orop') ).
thf(1363,plain,
vsubop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[185]) ).
thf(215,axiom,
! [A: vnat,B: vstring] :
( ( A @ vNum )
!= ( B @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Num-T') ).
thf(1495,plain,
! [A: vnat,B: vstring] :
( ( A @ vNum )
!= ( B @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[215]) ).
thf(87,axiom,
! [A: vAval,B: vUnOpT,C: vExp] :
( ( A @ vconstant )
!= ( C @ ( B @ vunop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-constant-unop') ).
thf(807,plain,
! [A: vAval,B: vUnOpT,C: vExp] :
( ( A @ vconstant )
!= ( C @ ( B @ vunop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(18,axiom,
! [A: vnat] :
( vzero
!= ( A @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-zero-succ') ).
thf(437,plain,
! [A: vnat] :
( vzero
!= ( A @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(230,axiom,
( ( vyes @ vnot )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-0') ).
thf(1561,plain,
( ( vyes @ vnot )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[230]) ).
thf(325,axiom,
! [A: vYN,B: vYN] :
( ( B @ vB @ ( A @ vB @ ( vorop @ vevalBinOp ) ) )
= ( B @ ( A @ vor ) @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-7') ).
thf(5586,plain,
! [A: vYN,B: vYN] :
( ( B @ vB @ ( A @ vB @ ( vorop @ vevalBinOp ) ) )
= ( B @ ( A @ vor ) @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[325]) ).
thf(92,axiom,
vsubop != vmulop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-mulop') ).
thf(828,plain,
vsubop != vmulop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(208,axiom,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( F = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tdefquestion_inv2') ).
thf(1473,plain,
! [A: vATMap,B: vATMap,C: vATMap,D: vAType,E: vLabel,F: vATMap,G: vQID] :
( ( C @ ( F @ vMC ) @ ( D @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ ( B @ vMC ) @ vptcheck ) ) )
=> ( F = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[208]) ).
thf(111,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vmultiply ) )
= vzero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','multiply-0') ).
thf(886,plain,
! [A: vnat] :
( ( vzero @ ( A @ vmultiply ) )
= vzero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(114,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionLabel )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuestionLabel-0') ).
thf(897,plain,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionLabel )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(200,axiom,
! [A: vLabel,B: vAType] :
( ? [C: vLabel] :
( ( ( B @ ( A @ vgetAnswer ) )
= ( C @ vaskText @ vT ) )
& ( B = vText )
& ( A = C ) )
| ? [C: vLabel] :
( ( ( B @ ( A @ vgetAnswer ) )
= ( C @ vaskNumber @ vNum ) )
& ( B = vNumber )
& ( A = C ) )
| ? [C: vLabel] :
( ( ( B @ ( A @ vgetAnswer ) )
= ( C @ vaskYesNo @ vB ) )
& ( B = vYesNo )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-INV') ).
thf(1410,plain,
! [A: vLabel,B: vAType] :
( ? [C: vLabel] :
( ( ( B @ ( A @ vgetAnswer ) )
= ( C @ vaskText @ vT ) )
& ( B = vText )
& ( A = C ) )
| ? [C: vLabel] :
( ( ( B @ ( A @ vgetAnswer ) )
= ( C @ vaskNumber @ vNum ) )
& ( B = vNumber )
& ( A = C ) )
| ? [C: vLabel] :
( ( ( B @ ( A @ vgetAnswer ) )
= ( C @ vaskYesNo @ vB ) )
& ( B = vYesNo )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[200]) ).
thf(321,axiom,
! [A: vExp] :
( ( A @ vsomeExp @ vgetExp )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getExp-0') ).
thf(5564,plain,
! [A: vExp] :
( ( A @ vsomeExp @ vgetExp )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[321]) ).
thf(268,axiom,
! [A: vQID,B: vATMap] :
( ? [C: vQID,D: vAType,E: vATMap,F: vQID] :
( ( ( B @ ( A @ vlookupATMap ) )
= ( E @ ( F @ vlookupATMap ) ) )
& ( B
= ( E @ ( D @ ( C @ vatmbind ) ) ) )
& ( A = F )
& ( F != C ) )
| ? [C: vQID,D: vAType,E: vATMap,F: vQID] :
( ( ( B @ ( A @ vlookupATMap ) )
= ( D @ vsomeAType ) )
& ( B
= ( E @ ( D @ ( C @ vatmbind ) ) ) )
& ( A = F )
& ( F = C ) )
| ? [C: vQID] :
( ( ( B @ ( A @ vlookupATMap ) )
= vnoAType )
& ( B = vatmempty )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupATMap-INV') ).
thf(1829,plain,
! [A: vQID,B: vATMap] :
( ? [C: vQID,D: vAType,E: vATMap,F: vQID] :
( ( ( B @ ( A @ vlookupATMap ) )
= ( E @ ( F @ vlookupATMap ) ) )
& ( B
= ( E @ ( D @ ( C @ vatmbind ) ) ) )
& ( A = F )
& ( F != C ) )
| ? [C: vQID,D: vAType,E: vATMap,F: vQID] :
( ( ( B @ ( A @ vlookupATMap ) )
= ( D @ vsomeAType ) )
& ( B
= ( E @ ( D @ ( C @ vatmbind ) ) ) )
& ( A = F )
& ( F = C ) )
| ? [C: vQID] :
( ( ( B @ ( A @ vlookupATMap ) )
= vnoAType )
& ( B = vatmempty )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[268]) ).
thf(172,axiom,
( ( vyes @ ( vyes @ vand ) )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and-0') ).
thf(1261,plain,
( ( vyes @ ( vyes @ vand ) )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(159,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vplus ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus-0') ).
thf(1152,plain,
! [A: vnat] :
( ( vzero @ ( A @ vplus ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(102,axiom,
! [A: vGID,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ vqgroup ) @ vreduce ) ) )
= ( B @ ( D @ ( C @ vQC ) ) @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-15') ).
thf(860,plain,
! [A: vGID,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ vqgroup ) @ vreduce ) ) )
= ( B @ ( D @ ( C @ vQC ) ) @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(52,axiom,
( ( vno @ ( vno @ vor ) )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','or-0') ).
thf(644,plain,
( ( vno @ ( vno @ vor ) )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(21,axiom,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vplus ) )
= ( C @ ( D @ vplus ) @ vsucc ) )
& ( B
= ( C @ vsucc ) )
& ( A = D ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vplus ) )
= C )
& ( B = vzero )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus-INV') ).
thf(459,plain,
! [A: vnat,B: vnat] :
( ? [C: vnat,D: vnat] :
( ( ( B @ ( A @ vplus ) )
= ( C @ ( D @ vplus ) @ vsucc ) )
& ( B
= ( C @ vsucc ) )
& ( A = D ) )
| ? [C: vnat] :
( ( ( B @ ( A @ vplus ) )
= C )
& ( B = vzero )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(130,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ ( vyes @ vB @ vconstant @ vqcond ) ) @ vreduce ) ) )
= ( A @ ( D @ ( C @ vQC ) ) @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-11') ).
thf(992,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ ( vyes @ vB @ vconstant @ vqcond ) ) @ vreduce ) ) )
= ( A @ ( D @ ( C @ vQC ) ) @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(91,axiom,
! [A: vUnOpT,B: vAType] :
( ( ( B != vYesNo )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-1') ).
thf(822,plain,
! [A: vUnOpT,B: vAType] :
( ( ( B != vYesNo )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(279,axiom,
! [A: vAType,B: vAType] :
( ( ( A @ vsomeAType )
= ( B @ vsomeAType ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someAType') ).
thf(1885,plain,
! [A: vAType,B: vAType] :
( ( ( A @ vsomeAType )
= ( B @ vsomeAType ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[279]) ).
thf(196,axiom,
! [A: vQMap,B: vAType,C: vLabel,D: vAnsMap,E: vQID] :
( ( A @ ( D @ ( B @ ( C @ ( E @ vdefquestion ) ) @ vqsingle @ vreduce ) ) )
= ( vqempty @ ( A @ ( B @ ( C @ ( E @ vqmbind ) ) ) @ ( D @ vQC ) ) @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-5') ).
thf(1399,plain,
! [A: vQMap,B: vAType,C: vLabel,D: vAnsMap,E: vQID] :
( ( A @ ( D @ ( B @ ( C @ ( E @ vdefquestion ) ) @ vqsingle @ vreduce ) ) )
= ( vqempty @ ( A @ ( B @ ( C @ ( E @ vqmbind ) ) ) @ ( D @ vQC ) ) @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[196]) ).
thf(41,axiom,
! [A: vQID,B: vAType,C: vExp,D: vQID] :
( ( C @ ( B @ ( A @ vvalue ) ) )
!= ( D @ vask ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-value-ask') ).
thf(607,plain,
! [A: vQID,B: vAType,C: vExp,D: vQID] :
( ( C @ ( B @ ( A @ vvalue ) ) )
!= ( D @ vask ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(234,axiom,
! [A: vGID,B: vQuestionnaire,C: vGID,D: vQuestionnaire] :
( ( ( B @ ( A @ vqgroup ) )
= ( D @ ( C @ vqgroup ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qgroup') ).
thf(1582,plain,
! [A: vGID,B: vQuestionnaire,C: vGID,D: vQuestionnaire] :
( ( ( B @ ( A @ vqgroup ) )
= ( D @ ( C @ vqgroup ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[234]) ).
thf(138,axiom,
! [A: vnat] :
( ( A @ vNum @ vtypeOf )
= vNumber ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-1') ).
thf(1019,plain,
! [A: vnat] :
( ( A @ vNum @ vtypeOf )
= vNumber ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(323,axiom,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vgtop @ vevalBinOp ) ) )
= ( B @ ( A @ vgt ) @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-4') ).
thf(5581,plain,
! [A: vnat,B: vnat] :
( ( B @ vNum @ ( A @ vNum @ ( vgtop @ vevalBinOp ) ) )
= ( B @ ( A @ vgt ) @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[323]) ).
thf(30,axiom,
! [A: vAval] :
( ( A @ vconstant @ vgetExpValue )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getExpValue-0') ).
thf(528,plain,
! [A: vAval] :
( ( A @ vconstant @ vgetExpValue )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(292,axiom,
! [A: vAnsMap,B: vBinOpT,C: vAType,D: vExp] :
( ( ( ( A @ ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ vreduceExp ) )
= ( D @ vsomeExp ) )
& ( ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ve1 @ vexpIsValue )
& ~ ( ve2 @ vexpIsValue )
& ~ ( A @ ( ve2 @ vreduceExp ) @ visSomeExp ) )
=> ( ( D @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExpPreservation-binop-expIsValue-True-expIsValue-False-isSomeExp-False') ).
thf(5155,plain,
! [A: vAnsMap,B: vBinOpT,C: vAType,D: vExp] :
( ( ( ( A @ ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ vreduceExp ) )
= ( D @ vsomeExp ) )
& ( ( ve2 @ ( B @ ( ve1 @ vbinop ) ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ( ve1 @ vexpIsValue )
& ~ ( ve2 @ vexpIsValue )
& ~ ( A @ ( ve2 @ vreduceExp ) @ visSomeExp ) )
=> ( ( D @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[292]) ).
thf(124,axiom,
! [A: vAnsMap] :
( ? [B: vQID,C: vAval,D: vAnsMap] :
( A
= ( D @ ( C @ ( B @ vabind ) ) ) )
| ( A = vaempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-AnsMap') ).
thf(940,plain,
! [A: vAnsMap] :
( ? [B: vQID,C: vAval,D: vAnsMap] :
( A
= ( D @ ( C @ ( B @ vabind ) ) ) )
| ( A = vaempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(122,axiom,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ ( vno @ vB @ vconstant @ vqcond ) ) @ vreduce ) ) )
= ( B @ ( D @ ( C @ vQC ) ) @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-12') ).
thf(935,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vAnsMap,D: vQMap] :
( ( D @ ( C @ ( B @ ( A @ ( vno @ vB @ vconstant @ vqcond ) ) @ vreduce ) ) )
= ( B @ ( D @ ( C @ vQC ) ) @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(255,axiom,
! [A: vExp,B: vExp] :
( ( ( A @ vsomeExp )
= ( B @ vsomeExp ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someExp') ).
thf(1681,plain,
! [A: vExp,B: vExp] :
( ( ( A @ vsomeExp )
= ( B @ vsomeExp ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[255]) ).
thf(207,axiom,
! [A: vQMap] :
( ? [B: vQID,C: vLabel,D: vAType,E: vQMap] :
( ( ( A @ vtypeQM )
= ( E @ vtypeQM @ ( D @ ( B @ vatmbind ) ) ) )
& ( A
= ( E @ ( D @ ( C @ ( B @ vqmbind ) ) ) ) ) )
| ( ( ( A @ vtypeQM )
= vatmempty )
& ( A = vqmempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeQM-INV') ).
thf(1463,plain,
! [A: vQMap] :
( ? [B: vQID,C: vLabel,D: vAType,E: vQMap] :
( ( ( A @ vtypeQM )
= ( E @ vtypeQM @ ( D @ ( B @ vatmbind ) ) ) )
& ( A
= ( E @ ( D @ ( C @ ( B @ vqmbind ) ) ) ) ) )
| ( ( ( A @ vtypeQM )
= vatmempty )
& ( A = vqmempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[207]) ).
thf(14486,plain,
$false,
inference(e,[status(thm)],[5116,1454,1633,5260,893,365,1369,1686,352,977,1005,683,1068,5644,741,1728,873,379,1533,5383,5614,1437,1041,582,762,1692,5529,1173,1486,5120,1671,1608,384,5589,1867,698,340,5192,5161,747,417,885,1613,1386,1366,1623,5621,1709,1430,5188,838,1511,1279,1577,5182,504,1871,1545,638,1379,1514,1890,5604,881,5617,1489,5526,5597,376,646,514,1383,1283,480,877,866,998,1433,1521,507,1696,1863,1604,1199,5142,534,5540,1636,798,910,5611,1676,630,815,1032,625,665,5534,889,1079,757,710,842,1012,1195,1407,1402,1360,1592,1143,615,1064,980,1719,869,989,857,1329,1028,753,5263,1155,686,1075,476,622,1263,701,738,1539,1266,1668,1192,1002,1874,569,1599,1715,371,1393,1857,5544,938,633,1563,1170,1035,1071,718,765,1712,412,1146,1483,1548,5608,1374,1301,1595,584,732,5395,772,1620,5627,875,579,5503,641,5546,445,382,5567,5118,713,1058,804,1356,350,1503,5185,611,5595,5148,1332,1258,5158,900,831,5506,784,1492,1542,362,1722,863,649,434,5531,599,1376,5584,1877,1630,483,848,5392,1149,1460,811,387,943,1022,932,1061,912,983,1396,780,1015,1176,1477,851,695,636,1044,431,5139,473,1626,1304,1203,531,548,617,553,1181,1551,795,680,776,5624,1025,5592,1531,705,1611,5388,5399,707,1499,791,1188,441,1038,1679,907,1130,1579,1404,744,1353,1008,1881,1617,845,5179,5386,1654,759,368,1390,5124,1276,1253,1674,1854,5600,1508,5132,995,1558,1861,1689,510,1706,5549,5144,1893,5128,5164,914,1440,929,1133,1725,835,854,5522,1480,603,735,818,5537,1859,801,1363,1495,807,437,1561,5586,828,1473,886,897,1410,5564,1829,1261,1152,860,644,459,992,822,1885,1399,607,1582,1019,5581,528,5155,940,935,1681,1463]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM271_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.14/0.40 % Computer : n006.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sat Sep 26 23:50:40 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.87/1.01 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.31/1.43 % [INFO] Parsing done (411ms).
% 2.31/1.44 % [INFO] Running in sequential loop mode.
% 3.26/1.83 % [INFO] eprover registered as external prover.
% 3.26/1.84 % [INFO] Scanning for conjecture ...
% 3.80/2.08 % [INFO] Found a conjecture (or negated_conjecture) and 363 axioms. Running axiom selection ...
% 4.32/2.27 % [INFO] Axiom selection finished. Selected 337 axioms (removed 26 axioms).
% 6.40/2.70 % [INFO] Problem is typed first-order (TPTP TFF).
% 6.40/2.74 % [INFO] Type checking passed.
% 6.40/2.74 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 10.65/3.75 % [INFO] [Domain constraints] Detected constraint on vAType
% 10.65/3.75 % [INFO] [Domain constraints] dom(vAType) ⊆ {vYesNo,vNumber,vText}
% 11.06/3.84 % [INFO] [Domain constraints] Detected constraint on vUnOpT
% 11.06/3.84 % [INFO] [Domain constraints] dom(vUnOpT) ⊆ {vnotop}
% 11.06/3.85 % [INFO] [Domain constraints] Detected constraint on vYN
% 11.06/3.85 % [INFO] [Domain constraints] dom(vYN) ⊆ {vyes,vno}
% 12.59/4.25 % [INFO] [Domain constraints] Detected constraint on vYN
% 12.59/4.25 % [INFO] [Domain constraints] dom(vYN) ⊆ {vyes,vno}
% 13.42/4.46 % [INFO] [Domain constraints] Detected constraint on vBinOpT
% 13.42/4.46 % [INFO] [Domain constraints] dom(vBinOpT) ⊆ {vandop,vaddop,vgtop,veqop,vdivop,vmulop,vltop,vsubop,vorop}
% 166.83/107.82 % External prover 'e' found a proof!
% 166.83/107.82 % [INFO] Killing All external provers ...
% 166.83/107.83 % Time passed: 107278ms (effective reasoning time: 106374ms)
% 166.83/107.83 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 166.83/107.83 % Axioms used in derivation (337): getQC-0, EQ-succ, lt-2, DIFF-subop-eqop, evalBinOp-10, pred-0, reduceExp-10, intersectATM-INV, multiply-1, DIFF-divop-eqop, checkBinOp-6, dom-AType, typeAM-INV, dom-Entry, isSomeAType-1, reduceExpPreservation-binop-IH0, EQ-qvar, Tdefquestion_inv3, echeck-0, reduceExp-7, reduce-7, DIFF-value-defquestion, isValue-true-INV, lookupAnsMap-1, reduce-0, DIFF-eqop-andop, lt-INV, DIFF-gtop-orop, Tqcond_inv5, Task_inv3, echeck-4, isSomeAType-false-INV, typeOf-0, Tvalue_inv2, DIFF-qempty-qsingle, EQ-B, dom-OptQConf, getExp-0, reduceExp-6, reduce-INV, reduceExp-INV, typeQM-0, evalBinOp-6, DIFF-eqop-orop, getAType-0, DIFF-subop-divop, Task_inv2, evalBinOp-2, gt-2, DIFF-subop-mulop, checkBinOp-1, DIFF-qsingle-qseq, lookupQMap-1, reduceExp-2, isSomeQC-0, isSomeQuestion-1, dom-YN, divide-0, Tqseq, getAM-0, plus-1, getAnswer-1, multiply-0, reduce-13, appendAnsMap-0, evalUnOp-0, isSomeQC-false-INV, intersectATM-1, DIFF-addop-subop, dom-AnsMap, appendATMap-0, DIFF-value-ask, DIFF-subop-andop, reduce-11, EQ-qsingle, pred-INV, checkBinOp-4, lookupATMap-0, isSomeQuestion-false-INV, lookupATMap-INV, evalBinOp-INV, reduceExpPreservation-binop-expIsValue-True-expIsValue-False-isSomeExp-True, isSomeExp-true-INV, expIsValue-false-INV, reduce-4, divide-1, DIFF-ltop-andop, EQ-unop, reduceExp-8, evalBinOp-0, DIFF-ltop-orop, dom-BinOpT, getAnswer-0, or-0, EQ-someQConf, reduce-15, gt-0, reduce-1, getExpValue-0, EQ-value, minus-0, dom-OptExp, isValue-1, EQ-someExp, lookupAnsMap-0, DIFF-qseq-qcond, EQ-Num, dom-Questionnaire, evalBinOp-5, reduceExp-5, dom-OptQuestion, DIFF-B-Num, DIFF-subop-gtop, reduceExpPreservation-binop-IH1, DIFF-divop-orop, Tvalue_inv1, dom-OptAType, getQuest-INV, echeck-3, checkUnOp-1, appendAnsMap-INV, DIFF-andop-orop, reduce-10, DIFF-mulop-gtop, and-INV, reduceExp-1, evalBinOp-9, isSomeQuestion-0, dom-QMap, typeOf-1, Tqgroup, intersectATM-0, multiply-INV, Tqseq_inv3, DIFF-qsingle-qcond, isSomeAType-true-INV, isValue-false-INV, EQ-someAType, DIFF-YesNo-Text, isSomeAval-false-INV, typeOf-INV, DIFF-question-defquestion, dom-ATMap, echeck-7, DIFF-Number-Text, Tqempty_inv2, checkBinOp-0, EQ-qseq, DIFF-mulop-orop, reduce-14, appendAnsMap-1, pred-1, reduce-9, EQ-question, lookupQMap-2, Tquestion_inv2, dom-Aval, EQ-binop, typeQM-1, DIFF-qempty-qgroup, DIFF-mulop-andop, lookupQMap-INV, typeAM-1, DIFF-defquestion-ask, DIFF-addop-mulop, dom-UnOpT, DIFF-divop-andop, getAnswer-2, reduce-5, lookupAnsMap-INV, evalBinOp-1, Tqempty, checkBinOp-3, gt-INV, isValue-0, getQM-INV, reduce-12, DIFF-mulop-ltop, reduce-2, Tquestion_inv1, lt-0, reduceExp-4, DIFF-noQConf-someQConf, and-1, EQ-ask, DIFF-mulop-eqop, checkBinOp-8, EQ-abind, or-INV, reduceExp-9, EQ-constant, Task_inv4, DIFF-qvar-unop, DIFF-eqop-ltop, dom-OptAval, evalBinOp-4, or-1, checkUnOp-0, Tqcond, EQ-qmbind, echeck-INV, DIFF-noAval-someAval, isSomeAval-true-INV, DIFF-yes-no, DIFF-qsingle-qgroup, DIFF-YesNo-Number, not-0, Tqcond_inv4, getAM-INV, EQ-qcond, isSomeQuestion-true-INV, DIFF-qcond-qgroup, DIFF-qseq-qgroup, echeck-1, minus-1, lookupATMap-1, Tvalue_inv4, evalBinOp-8, not-INV, getQuestionAType-0, Tquestion_inv3, DIFF-qempty-qseq, DIFF-divop-ltop, DIFF-noQuestion-someQuestion, dom-QConf, dom-Exp, typeOf-2, reduce-8, EQ-someAval, EQ-atmbind, DIFF-qmempty-qmbind, checkBinOp-7, Tqempty_inv1, isSomeAType-0, qcappend-0, DIFF-aempty-abind, DIFF-addop-gtop, reduceExp-0, DIFF-Num-T, isSomeExp-1, Tqseq_inv2, evalUnOp-INV, DIFF-question-value, minus-INV, DIFF-addop-orop, DIFF-question-ask, checkBinOp-5, DIFF-constant-binop, Tvalue, reduce-6, not-1, Tquestion, DIFF-gtop-andop, Tdefquestion, lt-1, EQ-qgroup, getQuestionLabel-0, Tqcond_inv7, getQM-0, getAval-0, appendATMap-INV, checkBinOp-9, DIFF-zero-succ, reduceExp-3, typeAM-0, isSomeAval-1, Tqgroup_inv, DIFF-subop-ltop, Tvalue_inv3, DIFF-subop-orop, Tdefquestion_inv2, echeck-5, divide-INV, isSomeAval-0, expIsValue-0, Tqseq_inv4, isSomeQC-true-INV, DIFF-mulop-divop, checkBinOp-2, DIFF-qvar-binop, DIFF-eqop-gtop, isSomeExp-false-INV, DIFF-gtop-ltop, DIFF-atmempty-atmbind, checkUnOp-INV, and-0, EQ-T, Tqcond_inv2, DIFF-addop-divop, expIsValue-1, appendATMap-1, Tqseq_inv1, echeck-6, DIFF-constant-qvar, getQuest-0, isSomeExp-0, DIFF-binop-unop, Tqcond_inv6, DIFF-addop-eqop, getAnswer-INV, gt-1, plus-INV, lookupAnsMap-2, EQ-defquestion, DIFF-addop-ltop, lookupATMap-2, evalBinOp-7, DIFF-noAType-someAType, DIFF-qempty-qcond, Task_inv1, Task, echeck-2, Tdefquestion_inv1, DIFF-constant-unop, dom-nat, qcappend-INV, evalUnOp-1, DIFF-noExp-someExp, checkBinOp-INV, reduceExpPreservation-binop-expIsValue-True-expIsValue-False-isSomeExp-False, intersectATM-2, reduce-3, Tqcond_inv1, lookupQMap-0, dom-MapConf, isSomeQC-1, DIFF-divop-gtop, EQ-QC, evalBinOp-3, EQ-MC, DIFF-B-T, plus-0, EQ-someQuestion, Tqcond_inv3, typeQM-INV, DIFF-addop-andop, expIsValue-true-INV
% 166.83/107.83 % No. of inferences in proof: 678
% 166.83/107.83 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 107278 ms resp. 106374 ms w/o parsing
% 167.32/107.97 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 167.32/107.98 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------