%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : COM277_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 : n020.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:16 AM UTC 2026
% Result : Theorem 93.60s 48.35s
% Output : Refutation 88.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 335
% Syntax : Number of formulae : 672 ( 345 unt; 0 typ; 0 def)
% Number of atoms : 2196 (1858 equ; 0 cnn)
% Maximal formula atoms : 100 ( 3 avg)
% Number of connectives : 7129 ( 589 ~; 410 |; 881 &;5016 @)
% ( 0 <=>; 233 =>; 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 : 103 ( 101 usr; 27 con; 0-4 aty)
% Number of variables : 2464 ( 0 ^;1753 !; 711 ?;2464 :)
% 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(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(113,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(892,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)],[113]) ).
thf(144,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(1036,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)],[144]) ).
thf(214,axiom,
! [A: vnat,B: vstring] :
( ( A @ vNum )
!= ( B @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Num-T') ).
thf(1501,plain,
! [A: vnat,B: vstring] :
( ( A @ vNum )
!= ( B @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[214]) ).
thf(277,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(1879,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)],[277]) ).
thf(282,axiom,
( ( vNumber @ ( vNumber @ ( vmulop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-2') ).
thf(5116,plain,
( ( vNumber @ ( vNumber @ ( vmulop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[282]) ).
thf(7,axiom,
! [A: vnat] :
( ? [B: vnat] :
( A
= ( B @ vsucc ) )
| ( A = vzero ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-nat') ).
thf(365,plain,
! [A: vnat] :
( ? [B: vnat] :
( A
= ( B @ vsucc ) )
| ( A = vzero ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(229,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(1559,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)],[229]) ).
thf(3,axiom,
( ( vzero @ vpred )
= vzero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred-0') ).
thf(347,plain,
( ( vzero @ vpred )
= vzero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(305,axiom,
! [A: vAType] :
( vnoAType
!= ( A @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noAType-someAType') ).
thf(5390,plain,
! [A: vAType] :
( vnoAType
!= ( A @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[305]) ).
thf(227,axiom,
vaddop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-andop') ).
thf(1554,plain,
vaddop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[227]) ).
thf(140,axiom,
vaddop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-eqop') ).
thf(1024,plain,
vaddop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(207,axiom,
vltop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-ltop-orop') ).
thf(1469,plain,
vltop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[207]) ).
thf(161,axiom,
! [A: vAval,B: vAval] :
( ( ( A @ vconstant )
= ( B @ vconstant ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-constant') ).
thf(1168,plain,
! [A: vAval,B: vAval] :
( ( ( A @ vconstant )
= ( B @ vconstant ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(76,axiom,
! [A: vAnsMap,B: vQMap] :
( ( B @ ( A @ ( vqempty @ vreduce ) ) )
= vnoQConf ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-0') ).
thf(760,plain,
! [A: vAnsMap,B: vQMap] :
( ( B @ ( A @ ( vqempty @ vreduce ) ) )
= vnoQConf ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(270,axiom,
! [A: vExp] :
( vnoExp
!= ( A @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noExp-someExp') ).
thf(1855,plain,
! [A: vExp] :
( vnoExp
!= ( A @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[270]) ).
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(683,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(131,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(994,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)],[131]) ).
thf(199,axiom,
! [A: vATMap] :
( ( A @ ( vatmempty @ vappendATMap ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendATMap-0') ).
thf(1422,plain,
! [A: vATMap] :
( ( A @ ( vatmempty @ vappendATMap ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[199]) ).
thf(225,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(1544,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)],[225]) ).
thf(107,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(873,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)],[107]) ).
thf(234,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(1591,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)],[234]) ).
thf(11,axiom,
( ( vqmempty @ vtypeQM )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeQM-0') ).
thf(379,plain,
( ( vqmempty @ vtypeQM )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(303,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(5383,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)],[303]) ).
thf(162,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(1173,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)],[162]) ).
thf(109,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vmultiply ) )
= vzero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','multiply-0') ).
thf(878,plain,
! [A: vnat] :
( ( vzero @ ( A @ vmultiply ) )
= vzero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
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(511,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(44,axiom,
! [A: vQID,B: vQID] :
( ( ( A @ vask )
= ( B @ vask ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-ask') ).
thf(614,plain,
! [A: vQID,B: vQID] :
( ( ( A @ vask )
= ( B @ vask ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(257,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(1692,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)],[257]) ).
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(677,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(259,axiom,
! [A: vQID,B: vAnsMap] :
( ~ ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-2') ).
thf(1705,plain,
! [A: vQID,B: vAnsMap] :
( ~ ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[259]) ).
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(384,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(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(550,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(273,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(1867,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)],[273]) ).
thf(175,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(1275,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)],[175]) ).
thf(290,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(5146,plain,
! [A: vExp] :
( ~ ( A @ vexpIsValue )
=> ? [B: vExp] :
( ( A = B )
& ! [C: vAval] :
( B
!= ( C @ vconstant ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[290]) ).
thf(149,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(1063,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)],[149]) ).
thf(121,axiom,
~ ( vnoAType @ visSomeAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-0') ).
thf(930,plain,
~ ( vnoAType @ visSomeAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(93,axiom,
! [A: vLabel] :
( ( vYesNo @ ( A @ vgetAnswer ) )
= ( A @ vaskYesNo @ vB ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-0') ).
thf(829,plain,
! [A: vLabel] :
( ( vYesNo @ ( A @ vgetAnswer ) )
= ( A @ vaskYesNo @ vB ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(194,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(1391,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)],[194]) ).
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(782,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(111,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(885,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)],[111]) ).
thf(240,axiom,
vsubop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-eqop') ).
thf(1613,plain,
vsubop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[240]) ).
thf(247,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(1650,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)],[247]) ).
thf(209,axiom,
vaddop != vmulop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-mulop') ).
thf(1475,plain,
vaddop != vmulop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[209]) ).
thf(186,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(1366,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)],[186]) ).
thf(221,axiom,
! [A: vYN,B: vYN] :
( ( ( B != vno )
| ( A != vno ) )
=> ( ( B @ ( A @ vor ) )
= vyes ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','or-1') ).
thf(1529,plain,
! [A: vYN,B: vYN] :
( ( ( B != vno )
| ( A != vno ) )
=> ( ( B @ ( A @ vor ) )
= vyes ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[221]) ).
thf(171,axiom,
! [A: vYN] :
( ( ( ( A @ vnot )
= vyes )
& ( A = vno ) )
| ( ( ( A @ vnot )
= vno )
& ( A = vyes ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-INV') ).
thf(1254,plain,
! [A: vYN] :
( ( ( ( A @ vnot )
= vyes )
& ( A = vno ) )
| ( ( ( A @ vnot )
= vno )
& ( A = vyes ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[171]) ).
thf(334,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(5621,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)],[334]) ).
thf(314,axiom,
! [A: vATMap,B: vQID] :
( ( B @ vqvar @ ( A @ vecheck ) )
= ( A @ ( B @ vlookupATMap ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-3') ).
thf(5533,plain,
! [A: vATMap,B: vQID] :
( ( B @ vqvar @ ( A @ vecheck ) )
= ( A @ ( B @ vlookupATMap ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[314]) ).
thf(327,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(5585,plain,
! [A: vAval,B: vAval] :
( ( A != B )
=> ( ( B @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vno @ vB @ vconstant @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[327]) ).
thf(67,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(719,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)],[67]) ).
thf(27,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vminus ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','minus-0') ).
thf(504,plain,
! [A: vnat] :
( ( vzero @ ( A @ vminus ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(172,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vlt ) )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lt-0') ).
thf(1264,plain,
! [A: vnat] :
( ( vzero @ ( A @ vlt ) )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(45,axiom,
vaddop != vdivop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-divop') ).
thf(619,plain,
vaddop != vdivop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(86,axiom,
vmulop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-gtop') ).
thf(802,plain,
vmulop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(166,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(1191,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)],[166]) ).
thf(62,axiom,
! [A: vQuestionnaire,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqseq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qseq') ).
thf(702,plain,
! [A: vQuestionnaire,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqseq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
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(751,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(286,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(5130,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)],[286]) ).
thf(205,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(1455,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)],[205]) ).
thf(115,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(902,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)],[115]) ).
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(638,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(217,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus-1') ).
thf(1514,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[217]) ).
thf(333,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(5604,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)],[333]) ).
thf(239,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(1609,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)],[239]) ).
thf(124,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(969,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)],[124]) ).
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(770,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(110,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(881,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)],[110]) ).
thf(310,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(5521,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)],[310]) ).
thf(158,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(1147,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)],[158]) ).
thf(119,axiom,
vyes != vno,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-yes-no') ).
thf(924,plain,
vyes != vno,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(206,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(1465,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)],[206]) ).
thf(248,axiom,
! [A: vATMap] :
( ( A @ ( vatmempty @ vintersectATM ) )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersectATM-0') ).
thf(1664,plain,
! [A: vATMap] :
( ( A @ ( vatmempty @ vintersectATM ) )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[248]) ).
thf(262,axiom,
! [A: vATMap,B: vYN] :
( ( B @ vB @ vconstant @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-0') ).
thf(1714,plain,
! [A: vATMap,B: vYN] :
( ( B @ vB @ vconstant @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[262]) ).
thf(82,axiom,
! [A: vEntry] :
( vqempty
!= ( A @ vqsingle ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qsingle') ).
thf(789,plain,
! [A: vEntry] :
( vqempty
!= ( A @ vqsingle ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(246,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(1632,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)],[246]) ).
thf(10,axiom,
! [A: vOptAval] :
( ? [B: vAval] :
( A
= ( B @ vsomeAval ) )
| ( A = vnoAval ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptAval') ).
thf(376,plain,
! [A: vOptAval] :
( ? [B: vAval] :
( A
= ( B @ vsomeAval ) )
| ( A = vnoAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
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(646,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(254,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(1682,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)],[254]) ).
thf(292,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(5156,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)],[292]) ).
thf(139,axiom,
! [A: vQConf] :
( vnoQConf
!= ( A @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noQConf-someQConf') ).
thf(1020,plain,
! [A: vQConf] :
( vnoQConf
!= ( A @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(253,axiom,
! [A: vExp,B: vExp] :
( ( ( A @ vsomeExp )
= ( B @ vsomeExp ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someExp') ).
thf(1677,plain,
! [A: vExp,B: vExp] :
( ( ( A @ vsomeExp )
= ( B @ vsomeExp ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[253]) ).
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(480,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(127,axiom,
! [A: vQID] :
( ( vaempty @ ( A @ vlookupAnsMap ) )
= vnoAval ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupAnsMap-0') ).
thf(981,plain,
! [A: vQID] :
( ( vaempty @ ( A @ vlookupAnsMap ) )
= vnoAval ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(195,axiom,
! [A: vQConf] : ( A @ vsomeQConf @ visSomeQC ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-1') ).
thf(1394,plain,
! [A: vQConf] : ( A @ vsomeQConf @ visSomeQC ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[195]) ).
thf(180,axiom,
vdivop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-ltop') ).
thf(1345,plain,
vdivop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[180]) ).
thf(16,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vsucc @ vgt ) )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt-1') ).
thf(428,plain,
! [A: vnat] :
( ( vzero @ ( A @ vsucc @ vgt ) )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
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(507,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(108,axiom,
vqempty @ visValue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-0') ).
thf(877,plain,
vqempty @ visValue,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
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(692,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(243,axiom,
! [A: vYN,B: vstring] :
( ( A @ vB )
!= ( B @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-B-T') ).
thf(1622,plain,
! [A: vYN,B: vstring] :
( ( A @ vB )
!= ( B @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[243]) ).
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(774,plain,
! [A: vEntry,B: vQuestionnaire,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqseq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(236,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(1600,plain,
! [A: vEntry,B: vExp,C: vQuestionnaire,D: vQuestionnaire] :
( ( A @ vqsingle )
!= ( D @ ( C @ ( B @ vqcond ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[236]) ).
thf(287,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(5137,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)],[287]) ).
thf(272,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(1863,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)],[272]) ).
thf(237,axiom,
vdivop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-gtop') ).
thf(1604,plain,
vdivop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[237]) ).
thf(294,axiom,
! [A: vYN] :
( ( A @ vB @ ( vnotop @ vevalUnOp ) )
= ( A @ vnot @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalUnOp-0') ).
thf(5174,plain,
! [A: vYN] :
( ( A @ vB @ ( vnotop @ vevalUnOp ) )
= ( A @ vnot @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[294]) ).
thf(313,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(5530,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)],[313]) ).
thf(83,axiom,
vaddop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-ltop') ).
thf(793,plain,
vaddop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(318,axiom,
! [A: vAval] :
( ( A @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-8') ).
thf(5545,plain,
! [A: vAval] :
( ( A @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[318]) ).
thf(289,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(5142,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)],[289]) ).
thf(12,axiom,
! [A: vQID] :
( ( vqmempty @ ( A @ vlookupQMap ) )
= vnoQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupQMap-0') ).
thf(381,plain,
! [A: vQID] :
( ( vqmempty @ ( A @ vlookupQMap ) )
= vnoQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(260,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(1708,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)],[260]) ).
thf(150,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(1067,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)],[150]) ).
thf(66,axiom,
! [A: vQConf,B: vQConf] :
( ( ( A @ vsomeQConf )
= ( B @ vsomeQConf ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someQConf') ).
thf(714,plain,
! [A: vQConf,B: vQConf] :
( ( ( A @ vsomeQConf )
= ( B @ vsomeQConf ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(284,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(5122,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)],[284]) ).
thf(92,axiom,
! [A: vQID,B: vAval,C: vAnsMap] :
( vaempty
!= ( C @ ( B @ ( A @ vabind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-aempty-abind') ).
thf(825,plain,
! [A: vQID,B: vAval,C: vAnsMap] :
( vaempty
!= ( C @ ( B @ ( A @ vabind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
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(778,plain,
! [A: vQID,B: vAType,C: vATMap] :
( vatmempty
!= ( C @ ( B @ ( A @ vatmbind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(183,axiom,
vsubop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-orop') ).
thf(1355,plain,
vsubop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[183]) ).
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(349,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(213,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(1487,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)],[213]) ).
thf(48,axiom,
! [A: vOptAType] :
( ~ ( A @ visSomeAType )
=> ( A = vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-false-INV') ).
thf(630,plain,
! [A: vOptAType] :
( ~ ( A @ visSomeAType )
=> ( A = vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(242,axiom,
vdivop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-andop') ).
thf(1619,plain,
vdivop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[242]) ).
thf(330,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(5594,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)],[330]) ).
thf(278,axiom,
! [A: vAType,B: vAType] :
( ( ( A @ vsomeAType )
= ( B @ vsomeAType ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someAType') ).
thf(1883,plain,
! [A: vAType,B: vAType] :
( ( ( A @ vsomeAType )
= ( B @ vsomeAType ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[278]) ).
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(566,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(295,axiom,
! [A: vOptAType] :
( ? [B: vAType] :
( A
= ( B @ vsomeAType ) )
| ( A = vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptAType') ).
thf(5177,plain,
! [A: vOptAType] :
( ? [B: vAType] :
( A
= ( B @ vsomeAType ) )
| ( A = vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[295]) ).
thf(112,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionLabel )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuestionLabel-0') ).
thf(889,plain,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionLabel )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(75,axiom,
vsubop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-gtop') ).
thf(757,plain,
vsubop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(230,axiom,
~ ( vnoQConf @ visSomeQC ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-0') ).
thf(1573,plain,
~ ( vnoQConf @ visSomeQC ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[230]) ).
thf(279,axiom,
! [A: vExp] :
( ( A @ vexpIsValue )
=> ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-true-INV') ).
thf(1888,plain,
! [A: vExp] :
( ( A @ vexpIsValue )
=> ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[279]) ).
thf(177,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(1296,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)],[177]) ).
thf(321,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(5566,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)],[321]) ).
thf(141,axiom,
! [A: vOptAval] :
( ( A @ visSomeAval )
=> ? [B: vAval] :
( A
= ( B @ vsomeAval ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-true-INV') ).
thf(1027,plain,
! [A: vOptAval] :
( ( A @ visSomeAval )
=> ? [B: vAval] :
( A
= ( B @ vsomeAval ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
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(456,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(97,axiom,
! [A: vOptQuestion] :
( ~ ( A @ visSomeQuestion )
=> ( A = vnoQuestion ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-false-INV') ).
thf(842,plain,
! [A: vOptQuestion] :
( ~ ( A @ visSomeQuestion )
=> ( A = vnoQuestion ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(198,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(1402,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)],[198]) ).
thf(71,axiom,
! [A: vAType] :
( ( A = vText )
| ( A = vNumber )
| ( A = vYesNo ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-AType') ).
thf(742,plain,
! [A: vAType] :
( ( A = vText )
| ( A = vNumber )
| ( A = vYesNo ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(224,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(1541,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)],[224]) ).
thf(268,axiom,
( ( vNumber @ ( vNumber @ ( vltop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-5') ).
thf(1851,plain,
( ( vNumber @ ( vNumber @ ( vltop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[268]) ).
thf(138,axiom,
vaddop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-orop') ).
thf(1017,plain,
vaddop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(189,axiom,
! [A: vQuestionnaire] :
( ( A @ visValue )
=> ( A = vqempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-true-INV') ).
thf(1375,plain,
! [A: vQuestionnaire] :
( ( A @ visValue )
=> ( A = vqempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[189]) ).
thf(200,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(1425,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)],[200]) ).
thf(251,axiom,
! [A: vOptAType] :
( ( A @ visSomeAType )
=> ? [B: vAType] :
( A
= ( B @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-true-INV') ).
thf(1672,plain,
! [A: vOptAType] :
( ( A @ visSomeAType )
=> ? [B: vAType] :
( A
= ( B @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[251]) ).
thf(155,axiom,
vgtop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-gtop-andop') ).
thf(1138,plain,
vgtop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(106,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(869,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( vqmempty
!= ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(102,axiom,
! [A: vYN] :
( ( A = vno )
| ( A = vyes ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-YN') ).
thf(857,plain,
! [A: vYN] :
( ( A = vno )
| ( A = vyes ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(325,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(5577,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)],[325]) ).
thf(308,axiom,
! [A: vAType] :
( ( A @ vsomeAType @ vgetAType )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAType-0') ).
thf(5502,plain,
! [A: vAType] :
( ( A @ vsomeAType @ vgetAType )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[308]) ).
thf(185,axiom,
! [A: vstring,B: vstring] :
( ( ( A @ vT )
= ( B @ vT ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-T') ).
thf(1361,plain,
! [A: vstring,B: vstring] :
( ( ( A @ vT )
= ( B @ vT ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[185]) ).
thf(328,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(5588,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)],[328]) ).
thf(203,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(1446,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)],[203]) ).
thf(304,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(5387,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)],[304]) ).
thf(63,axiom,
! [A: vATMap,B: vATMap] : ( B @ ( A @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqempty') ).
thf(706,plain,
! [A: vATMap,B: vATMap] : ( B @ ( A @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(46,axiom,
! [A: vnat,B: vnat] :
( ( ( A @ vNum )
= ( B @ vNum ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-Num') ).
thf(622,plain,
! [A: vnat,B: vnat] :
( ( ( A @ vNum )
= ( B @ vNum ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(179,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(1324,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)],[179]) ).
thf(132,axiom,
veqop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-ltop') ).
thf(997,plain,
veqop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(233,axiom,
! [A: vOptQConf] :
( ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) )
| ( A = vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptQConf') ).
thf(1588,plain,
! [A: vOptQConf] :
( ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) )
| ( A = vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[233]) ).
thf(191,axiom,
vsubop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-andop') ).
thf(1382,plain,
vsubop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[191]) ).
thf(307,axiom,
! [A: vAnsMap,B: vAType] :
( ( ( ( ve1 @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) )
& ~ ( ve1 @ vexpIsValue ) )
=> ? [C: vExp] :
( ( A @ ( ve1 @ vreduceExp ) )
= ( C @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExpProgress-unop-IH0') ).
thf(5498,plain,
! [A: vAnsMap,B: vAType] :
( ( ( ( ve1 @ ( A @ vtypeAM @ vecheck ) )
= ( B @ vsomeAType ) )
& ~ ( ve1 @ vexpIsValue ) )
=> ? [C: vExp] :
( ( A @ ( ve1 @ vreduceExp ) )
= ( C @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[307]) ).
thf(128,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(984,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)],[128]) ).
thf(201,axiom,
veqop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-orop') ).
thf(1429,plain,
veqop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[201]) ).
thf(168,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(1246,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)],[168]) ).
thf(264,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(1720,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)],[264]) ).
thf(210,axiom,
vmulop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-ltop') ).
thf(1478,plain,
vmulop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[210]) ).
thf(169,axiom,
( ( vyes @ ( vyes @ vand ) )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and-0') ).
thf(1249,plain,
( ( vyes @ ( vyes @ vand ) )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[169]) ).
thf(148,axiom,
vaddop != vsubop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-subop') ).
thf(1060,plain,
vaddop != vsubop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(145,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(1050,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)],[145]) ).
thf(291,axiom,
! [A: vATMap,B: vstring] :
( ( B @ vT @ vconstant @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-2') ).
thf(5153,plain,
! [A: vATMap,B: vstring] :
( ( B @ vT @ vconstant @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[291]) ).
thf(167,axiom,
! [A: vEntry,B: vEntry] :
( ( ( A @ vqsingle )
= ( B @ vqsingle ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qsingle') ).
thf(1241,plain,
! [A: vEntry,B: vEntry] :
( ( ( A @ vqsingle )
= ( B @ vqsingle ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(49,axiom,
~ ( vnoAval @ visSomeAval ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-0') ).
thf(633,plain,
~ ( vnoAval @ visSomeAval ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(87,axiom,
! [A: vOptQConf] :
( ~ ( A @ visSomeQC )
=> ( A = vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-false-INV') ).
thf(805,plain,
! [A: vOptQConf] :
( ~ ( A @ visSomeQC )
=> ( A = vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(118,axiom,
vmulop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-orop') ).
thf(921,plain,
vmulop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(151,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(1071,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)],[151]) ).
thf(165,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(1187,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)],[165]) ).
thf(241,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(1616,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)],[241]) ).
thf(285,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(5126,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)],[285]) ).
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(662,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(323,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(5571,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)],[323]) ).
thf(266,axiom,
! [A: vAType,B: vAType] :
( ( B @ ( A @ ( veqop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-8') ).
thf(1846,plain,
! [A: vAType,B: vAType] :
( ( B @ ( A @ ( veqop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[266]) ).
thf(117,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(906,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)],[117]) ).
thf(154,axiom,
vdivop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-orop') ).
thf(1135,plain,
vdivop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(170,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(1251,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)],[170]) ).
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(745,plain,
! [A: vYN,B: vYN] :
( ( ( B != vyes )
| ( A != vyes ) )
=> ( ( B @ ( A @ vand ) )
= vno ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(235,axiom,
! [A: vQID,B: vQID] :
( ( ( A @ vqvar )
= ( B @ vqvar ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qvar') ).
thf(1595,plain,
! [A: vQID,B: vQID] :
( ( ( A @ vqvar )
= ( B @ vqvar ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[235]) ).
thf(311,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(5525,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)],[311]) ).
thf(68,axiom,
vsubop != vdivop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-divop') ).
thf(733,plain,
vsubop != vdivop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(331,axiom,
! [A: vOptExp] :
( ( A @ visSomeExp )
=> ? [B: vExp] :
( A
= ( B @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-true-INV') ).
thf(5598,plain,
! [A: vOptExp] :
( ( A @ visSomeExp )
=> ? [B: vExp] :
( A
= ( B @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[331]) ).
thf(135,axiom,
! [A: vYN,B: vnat] :
( ( A @ vB )
!= ( B @ vNum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-B-Num') ).
thf(1007,plain,
! [A: vYN,B: vnat] :
( ( A @ vB )
!= ( B @ vNum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(153,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(1125,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)],[153]) ).
thf(193,axiom,
vmulop != vdivop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-divop') ).
thf(1388,plain,
vmulop != vdivop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[193]) ).
thf(65,axiom,
vmulop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-eqop') ).
thf(711,plain,
vmulop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
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(579,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(222,axiom,
! [A: vAnsMap] :
( ( A @ ( vaempty @ vappendAnsMap ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendAnsMap-0') ).
thf(1535,plain,
! [A: vAnsMap] :
( ( A @ ( vaempty @ vappendAnsMap ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[222]) ).
thf(219,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(1520,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)],[219]) ).
thf(33,axiom,
! [A: vYN,B: vYN] :
( ( ( A @ vB )
= ( B @ vB ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-B') ).
thf(545,plain,
! [A: vYN,B: vYN] :
( ( ( A @ vB )
= ( B @ vB ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(116,axiom,
~ ( vnoQuestion @ visSomeQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-0') ).
thf(904,plain,
~ ( vnoQuestion @ visSomeQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(126,axiom,
! [A: vQuestionnaire] :
( ~ ( A @ visValue )
=> ? [B: vQuestionnaire] :
( ( A = B )
& ( B != vqempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-false-INV') ).
thf(975,plain,
! [A: vQuestionnaire] :
( ~ ( A @ visValue )
=> ? [B: vQuestionnaire] :
( ( A = B )
& ( B != vqempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(52,axiom,
( ( vno @ ( vno @ vor ) )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','or-0') ).
thf(641,plain,
( ( vno @ ( vno @ vor ) )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(283,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(5118,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)],[283]) ).
thf(316,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(5539,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)],[316]) ).
thf(174,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(1271,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)],[174]) ).
thf(188,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(1371,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)],[188]) ).
thf(336,axiom,
! [A: vAType] : ( A @ vsomeAType @ visSomeAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-1') ).
thf(5634,plain,
! [A: vAType] : ( A @ vsomeAType @ visSomeAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[336]) ).
thf(252,axiom,
( ( vYesNo @ ( vYesNo @ ( vorop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-7') ).
thf(1675,plain,
( ( vYesNo @ ( vYesNo @ ( vorop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[252]) ).
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(604,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(269,axiom,
! [A: vAval] : ( A @ vconstant @ vexpIsValue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-0') ).
thf(1853,plain,
! [A: vAval] : ( A @ vconstant @ vexpIsValue ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[269]) ).
thf(136,axiom,
! [A: vnat] :
( ( A @ vNum @ vtypeOf )
= vNumber ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-1') ).
thf(1011,plain,
! [A: vnat] :
( ( A @ vNum @ vtypeOf )
= vNumber ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(69,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetAM )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAM-0') ).
thf(736,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetAM )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(130,axiom,
! [A: vEntry,B: vGID,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qsingle-qgroup') ).
thf(990,plain,
! [A: vEntry,B: vGID,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(6,axiom,
! [A: vnat] :
( ( A @ vsucc @ vpred )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pred-1') ).
thf(362,plain,
! [A: vnat] :
( ( A @ vsucc @ vpred )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(157,axiom,
! [A: vnat] :
( ( vzero @ ( A @ vplus ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','plus-0') ).
thf(1144,plain,
! [A: vnat] :
( ( vzero @ ( A @ vplus ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(18,axiom,
! [A: vnat] :
( vzero
!= ( A @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-zero-succ') ).
thf(434,plain,
! [A: vnat] :
( vzero
!= ( A @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(104,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(863,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)],[104]) ).
thf(152,axiom,
vdivop != veqop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-divop-eqop') ).
thf(1122,plain,
vdivop != veqop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(302,axiom,
( ( vNumber @ ( vNumber @ ( vsubop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-1') ).
thf(5381,plain,
( ( vNumber @ ( vNumber @ ( vsubop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[302]) ).
thf(249,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(1667,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)],[249]) ).
thf(281,axiom,
( ( vNumber @ ( vNumber @ ( vaddop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-0') ).
thf(5114,plain,
( ( vNumber @ ( vNumber @ ( vaddop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[281]) ).
thf(276,axiom,
~ ( vnoExp @ visSomeExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-0') ).
thf(1877,plain,
~ ( vnoExp @ visSomeExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[276]) ).
thf(228,axiom,
( ( vyes @ vnot )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-0') ).
thf(1557,plain,
( ( vyes @ vnot )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[228]) ).
thf(265,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(1821,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)],[265]) ).
thf(99,axiom,
veqop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-gtop') ).
thf(848,plain,
veqop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(296,axiom,
! [A: vQID,B: vUnOpT,C: vExp] :
( ( A @ vqvar )
!= ( C @ ( B @ vunop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qvar-unop') ).
thf(5180,plain,
! [A: vQID,B: vUnOpT,C: vExp] :
( ( A @ vqvar )
!= ( C @ ( B @ vunop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[296]) ).
thf(176,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(1293,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)],[176]) ).
thf(122,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(932,plain,
! [A: vAnsMap] :
( ? [B: vQID,C: vAval,D: vAnsMap] :
( A
= ( D @ ( C @ ( B @ vabind ) ) ) )
| ( A = vaempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(256,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(1688,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)],[256]) ).
thf(320,axiom,
! [A: vExp] :
( ( A @ vsomeExp @ vgetExp )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getExp-0') ).
thf(5563,plain,
! [A: vExp] :
( ( A @ vsomeExp @ vgetExp )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[320]) ).
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(477,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(85,axiom,
! [A: vnat,B: vnat] :
( ( ( B @ ( A @ vgt ) )
!= vyes )
=> ( ( B @ ( A @ vdivide ) )
= vzero ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','divide-1') ).
thf(799,plain,
! [A: vnat,B: vnat] :
( ( ( B @ ( A @ vgt ) )
!= vyes )
=> ( ( B @ ( A @ vdivide ) )
= vzero ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(159,axiom,
! [A: vLabel] :
( ( vText @ ( A @ vgetAnswer ) )
= ( A @ vaskText @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-2') ).
thf(1162,plain,
! [A: vLabel] :
( ( vText @ ( A @ vgetAnswer ) )
= ( A @ vaskText @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(196,axiom,
vgtop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-gtop-orop') ).
thf(1396,plain,
vgtop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[196]) ).
thf(60,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(695,plain,
! [A: vQID,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vqvar )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
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(608,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(133,axiom,
! [A: vGID,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qgroup') ).
thf(1000,plain,
! [A: vGID,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(100,axiom,
! [A: vQuestionnaire] :
( ( A != vqempty )
=> ~ ( A @ visValue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-1') ).
thf(851,plain,
! [A: vQuestionnaire] :
( ( A != vqempty )
=> ~ ( A @ visValue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(19,axiom,
! [A: vAval] :
( vnoAval
!= ( A @ vsomeAval ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noAval-someAval') ).
thf(438,plain,
! [A: vAval] :
( vnoAval
!= ( A @ vsomeAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
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(431,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vsucc @ vgt ) )
= ( A @ ( A @ vgt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
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(473,plain,
! [A: vQID,B: vLabel,C: vAType] :
( vnoQuestion
!= ( C @ ( B @ ( A @ vsomeQuestion ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(244,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQM )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQM-0') ).
thf(1626,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQM )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[244]) ).
thf(319,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(5548,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)],[319]) ).
thf(275,axiom,
! [A: vExp] :
( ! [B: vAval] :
( A
!= ( B @ vconstant ) )
=> ~ ( A @ vexpIsValue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-1') ).
thf(1873,plain,
! [A: vExp] :
( ! [B: vAval] :
( A
!= ( B @ vconstant ) )
=> ~ ( A @ vexpIsValue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[275]) ).
thf(312,axiom,
! [A: vExp] : ( A @ vsomeExp @ visSomeExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-1') ).
thf(5528,plain,
! [A: vExp] : ( A @ vsomeExp @ visSomeExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[312]) ).
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(531,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(57,axiom,
! [A: vMapConf] :
? [B: vATMap,C: vATMap] :
( A
= ( C @ ( B @ vMC ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-MapConf') ).
thf(680,plain,
! [A: vMapConf] :
? [B: vATMap,C: vATMap] :
( A
= ( C @ ( B @ vMC ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(120,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(927,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)],[120]) ).
thf(208,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(1472,plain,
! [A: vOptQuestion] :
( ( A @ visSomeQuestion )
=> ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vsomeQuestion ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[208]) ).
thf(95,axiom,
! [A: vstring] :
( ( A @ vT @ vtypeOf )
= vText ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-2') ).
thf(836,plain,
! [A: vstring] :
( ( A @ vT @ vtypeOf )
= vText ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(89,axiom,
! [A: vUnOpT,B: vAType] :
( ( ( B != vYesNo )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-1') ).
thf(812,plain,
! [A: vUnOpT,B: vAType] :
( ( ( B != vYesNo )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(216,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(1509,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)],[216]) ).
thf(226,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(1547,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)],[226]) ).
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(414,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(70,axiom,
vsubop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-ltop') ).
thf(739,plain,
vsubop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(187,axiom,
! [A: vQConf] :
( ( A @ vsomeQConf @ vgetQC )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQC-0') ).
thf(1368,plain,
! [A: vQConf] :
( ( A @ vsomeQConf @ vgetQC )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[187]) ).
thf(173,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(1267,plain,
! [A: vAval,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vconstant )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(30,axiom,
! [A: vAval] :
( ( A @ vconstant @ vgetExpValue )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getExpValue-0') ).
thf(525,plain,
! [A: vAval] :
( ( A @ vconstant @ vgetExpValue )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(335,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(5624,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)],[335]) ).
thf(14,axiom,
! [A: vAval,B: vAval] :
( ( ( A @ vsomeAval )
= ( B @ vsomeAval ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someAval') ).
thf(409,plain,
! [A: vAval,B: vAval] :
( ( ( A @ vsomeAval )
= ( B @ vsomeAval ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(212,axiom,
! [A: vOptQConf] :
( ( A @ visSomeQC )
=> ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-true-INV') ).
thf(1484,plain,
! [A: vOptQConf] :
( ( A @ visSomeQC )
=> ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[212]) ).
thf(202,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(1432,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)],[202]) ).
thf(204,axiom,
vltop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-ltop-andop') ).
thf(1452,plain,
vltop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[204]) ).
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(359,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vminus ) )
= ( B @ ( A @ vminus ) @ vpred ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(53,axiom,
vgtop != vltop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-gtop-ltop') ).
thf(643,plain,
vgtop != vltop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(261,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(1711,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)],[261]) ).
thf(146,axiom,
! [A: vOptAval] :
( ~ ( A @ visSomeAval )
=> ( A = vnoAval ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-false-INV') ).
thf(1053,plain,
! [A: vOptAval] :
( ~ ( A @ visSomeAval )
=> ( A = vnoAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(317,axiom,
( ( vNumber @ ( vNumber @ ( vdivop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-3') ).
thf(5543,plain,
( ( vNumber @ ( vNumber @ ( vdivop @ vcheckBinOp ) ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[317]) ).
thf(22,axiom,
! [A: vnat] :
( ( A @ vsucc @ ( vzero @ vlt ) )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lt-1') ).
thf(470,plain,
! [A: vnat] :
( ( A @ vsucc @ ( vzero @ vlt ) )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
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(576,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(223,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(1538,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)],[223]) ).
thf(88,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(808,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)],[88]) ).
thf(184,axiom,
vaddop != vgtop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-addop-gtop') ).
thf(1358,plain,
vaddop != vgtop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[184]) ).
thf(267,axiom,
( ( vNumber @ ( vNumber @ ( vgtop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-4') ).
thf(1849,plain,
( ( vNumber @ ( vNumber @ ( vgtop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[267]) ).
thf(156,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(1141,plain,
! [A: vQID,B: vAval,C: vAnsMap] :
( ( C @ ( B @ ( A @ vabind ) ) @ ( A @ vlookupAnsMap ) )
= ( B @ vsomeAval ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(258,axiom,
! [A: vAval,B: vAnsMap] :
( ( B @ ( A @ vconstant @ vreduceExp ) )
= vnoExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-0') ).
thf(1702,plain,
! [A: vAval,B: vAnsMap] :
( ( B @ ( A @ vconstant @ vreduceExp ) )
= vnoExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[258]) ).
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(600,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(250,axiom,
( ( vYesNo @ ( vnotop @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-0') ).
thf(1670,plain,
( ( vYesNo @ ( vnotop @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[250]) ).
thf(263,axiom,
! [A: vOptExp] :
( ~ ( A @ visSomeExp )
=> ( A = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-false-INV') ).
thf(1717,plain,
! [A: vOptExp] :
( ~ ( A @ visSomeExp )
=> ( A = vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[263]) ).
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(612,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(98,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(845,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)],[98]) ).
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(627,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(163,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(1180,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)],[163]) ).
thf(255,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(1685,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)],[255]) ).
thf(315,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(5536,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)],[315]) ).
thf(178,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(1321,plain,
! [A: vATMap] :
( ? [B: vQID,C: vAType,D: vATMap] :
( A
= ( D @ ( C @ ( B @ vatmbind ) ) ) )
| ( A = vatmempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[178]) ).
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(581,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(218,axiom,
veqop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-andop') ).
thf(1517,plain,
veqop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[218]) ).
thf(231,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(1575,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)],[231]) ).
thf(8,axiom,
! [A: vnat,B: vnat] :
( ( ( A @ vsucc )
= ( B @ vsucc ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-succ') ).
thf(368,plain,
! [A: vnat,B: vnat] :
( ( ( A @ vsucc )
= ( B @ vsucc ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(297,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(5184,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)],[297]) ).
thf(300,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(5258,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)],[300]) ).
thf(61,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(699,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)],[61]) ).
thf(192,axiom,
! [A: vYN] :
( ( A @ vB @ vtypeOf )
= vYesNo ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-0') ).
thf(1385,plain,
! [A: vYN] :
( ( A @ vB @ vtypeOf )
= vYesNo ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[192]) ).
thf(211,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(1481,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)],[211]) ).
thf(245,axiom,
vandop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-andop-orop') ).
thf(1629,plain,
vandop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[245]) ).
thf(306,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(5394,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)],[306]) ).
thf(309,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(5505,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)],[309]) ).
thf(142,axiom,
vYesNo != vNumber,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-YesNo-Number') ).
thf(1030,plain,
vYesNo != vNumber,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(114,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionAType )
= C ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuestionAType-0') ).
thf(899,plain,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionAType )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(94,axiom,
! [A: vAval,B: vQID] :
( ( A @ vconstant )
!= ( B @ vqvar ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-constant-qvar') ).
thf(832,plain,
! [A: vAval,B: vQID] :
( ( A @ vconstant )
!= ( B @ vqvar ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(238,axiom,
! [A: vAval] : ( A @ vsomeAval @ visSomeAval ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAval-1') ).
thf(1607,plain,
! [A: vAval] : ( A @ vsomeAval @ visSomeAval ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[238]) ).
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(763,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(298,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(5187,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)],[298]) ).
thf(181,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(1348,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)],[181]) ).
thf(232,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(1578,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)],[232]) ).
thf(90,axiom,
! [A: vExp,B: vQuestionnaire,C: vQuestionnaire] :
( vqempty
!= ( C @ ( B @ ( A @ vqcond ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qcond') ).
thf(818,plain,
! [A: vExp,B: vQuestionnaire,C: vQuestionnaire] :
( vqempty
!= ( C @ ( B @ ( A @ vqcond ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(101,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(854,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)],[101]) ).
thf(220,axiom,
! [A: vQID,B: vLabel,C: vAType] : ( C @ ( B @ ( A @ vsomeQuestion ) ) @ visSomeQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-1') ).
thf(1527,plain,
! [A: vQID,B: vLabel,C: vAType] : ( C @ ( B @ ( A @ vsomeQuestion ) ) @ visSomeQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[220]) ).
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(373,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(105,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(867,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)],[105]) ).
thf(332,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(5601,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)],[332]) ).
thf(271,axiom,
! [A: vAval,B: vUnOpT,C: vExp] :
( ( A @ vconstant )
!= ( C @ ( B @ vunop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-constant-unop') ).
thf(1859,plain,
! [A: vAval,B: vUnOpT,C: vExp] :
( ( A @ vconstant )
!= ( C @ ( B @ vunop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[271]) ).
thf(293,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(5159,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)],[293]) ).
thf(147,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(1056,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)],[147]) ).
thf(143,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(1033,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)],[143]) ).
thf(280,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(1891,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)],[280]) ).
thf(301,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(5378,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)],[301]) ).
thf(50,axiom,
! [A: vnat] :
( ( A @ ( vzero @ vgt ) )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','gt-0') ).
thf(635,plain,
! [A: vnat] :
( ( A @ ( vzero @ vgt ) )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(160,axiom,
! [A: vAval] :
( ( A @ vsomeAval @ vgetAval )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAval-0') ).
thf(1165,plain,
! [A: vAval] :
( ( A @ vsomeAval @ vgetAval )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(84,axiom,
vmulop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-mulop-andop') ).
thf(796,plain,
vmulop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(96,axiom,
! [A: vUnOpT] : ( A = vnotop ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-UnOpT') ).
thf(839,plain,
! [A: vUnOpT] : ( A = vnotop ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(129,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQuest )
= C ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuest-0') ).
thf(987,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQuest )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(182,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(1352,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)],[182]) ).
thf(103,axiom,
! [A: vQID] :
( ( vatmempty @ ( A @ vlookupATMap ) )
= vnoAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupATMap-0') ).
thf(860,plain,
! [A: vQID] :
( ( vatmempty @ ( A @ vlookupATMap ) )
= vnoAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(91,axiom,
vsubop != vmulop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-subop-mulop') ).
thf(822,plain,
vsubop != vmulop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(134,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(1004,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)],[134]) ).
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(442,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(26,axiom,
vYesNo != vText,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-YesNo-Text') ).
thf(501,plain,
vYesNo != vText,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(288,axiom,
( ( vYesNo @ ( vYesNo @ ( vandop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-6') ).
thf(5140,plain,
( ( vYesNo @ ( vYesNo @ ( vandop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[288]) ).
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(596,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(190,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(1378,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID] :
( ( C @ ( B @ ( A @ vquestion ) ) )
!= ( D @ vask ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[190]) ).
thf(326,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(5581,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)],[326]) ).
thf(31,axiom,
vNumber != vText,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Number-Text') ).
thf(528,plain,
vNumber != vText,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(215,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(1505,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)],[215]) ).
thf(197,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(1399,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)],[197]) ).
thf(329,axiom,
! [A: vATMap,B: vnat] :
( ( B @ vNum @ vconstant @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-1') ).
thf(5591,plain,
! [A: vATMap,B: vnat] :
( ( B @ vNum @ vconstant @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[329]) ).
thf(1,conjecture,
! [A: vAnsMap,B: vUnOpT,C: vAType] :
( ( ( ( ve1 @ ( B @ vunop ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ~ ( ve1 @ ( B @ vunop ) @ vexpIsValue )
& ~ ( ve1 @ vexpIsValue )
& ~ ( A @ ( ve1 @ vreduceExp ) @ visSomeExp ) )
=> ? [D: vExp] :
( ( A @ ( ve1 @ ( B @ vunop ) @ vreduceExp ) )
= ( D @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExpProgress-unop-expIsValue-False-isSomeExp-False') ).
thf(2,negated_conjecture,
~ ! [A: vAnsMap,B: vUnOpT,C: vAType] :
( ( ( ( ve1 @ ( B @ vunop ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ~ ( ve1 @ ( B @ vunop ) @ vexpIsValue )
& ~ ( ve1 @ vexpIsValue )
& ~ ( A @ ( ve1 @ vreduceExp ) @ visSomeExp ) )
=> ? [D: vExp] :
( ( A @ ( ve1 @ ( B @ vunop ) @ vreduceExp ) )
= ( D @ vsomeExp ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(337,plain,
~ ! [A: vAnsMap,B: vUnOpT,C: vAType] :
( ( ( ( ve1 @ ( B @ vunop ) @ ( A @ vtypeAM @ vecheck ) )
= ( C @ vsomeAType ) )
& ~ ( ve1 @ ( B @ vunop ) @ vexpIsValue )
& ~ ( ve1 @ vexpIsValue )
& ~ ( A @ ( ve1 @ vreduceExp ) @ visSomeExp ) )
=> ? [D: vExp] :
( ( A @ ( ve1 @ ( B @ vunop ) @ vreduceExp ) )
= ( D @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(123,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(935,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)],[123]) ).
thf(164,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vsucc @ vlt ) )
= ( A @ ( A @ vlt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lt-2') ).
thf(1184,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vsucc @ vlt ) )
= ( A @ ( A @ vlt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(322,axiom,
( ( vaempty @ vtypeAM )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeAM-0') ).
thf(5569,plain,
( ( vaempty @ vtypeAM )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[322]) ).
thf(299,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(5255,plain,
! [A: vQID,B: vAType,C: vATMap] :
( ( C @ ( B @ ( A @ vatmbind ) ) @ ( A @ vlookupATMap ) )
= ( B @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[299]) ).
thf(74,axiom,
( ( vno @ vnot )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-1') ).
thf(755,plain,
( ( vno @ vnot )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(324,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(5574,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)],[324]) ).
thf(64,axiom,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vQC ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-QConf') ).
thf(708,plain,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vQC ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(137,axiom,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vmultiply ) )
= ( B @ ( A @ vmultiply ) @ ( A @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','multiply-1') ).
thf(1014,plain,
! [A: vnat,B: vnat] :
( ( B @ vsucc @ ( A @ vmultiply ) )
= ( B @ ( A @ vmultiply ) @ ( A @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(274,axiom,
! [A: vOptExp] :
( ? [B: vExp] :
( A
= ( B @ vsomeExp ) )
| ( A = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptExp') ).
thf(1870,plain,
! [A: vOptExp] :
( ? [B: vExp] :
( A
= ( B @ vsomeExp ) )
| ( A = vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[274]) ).
thf(125,axiom,
! [A: vLabel] :
( ( vNumber @ ( A @ vgetAnswer ) )
= ( A @ vaskNumber @ vNum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-1') ).
thf(972,plain,
! [A: vLabel] :
( ( vNumber @ ( A @ vgetAnswer ) )
= ( A @ vaskNumber @ vNum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(14009,plain,
$false,
inference(e,[status(thm)],[892,1036,1501,1879,5116,365,1559,347,5390,1554,1024,1469,1168,760,1855,683,994,1422,1544,873,1591,379,5383,1173,878,511,614,1692,677,1705,384,550,1867,1275,5146,1063,930,829,1391,782,885,1613,1650,1475,1366,1529,1254,5621,5533,5585,719,504,1264,619,802,1191,702,751,5130,1455,902,638,1514,5604,1609,969,770,881,5521,1147,924,1465,1664,1714,789,1632,376,646,1682,5156,1020,1677,480,981,1394,1345,428,507,877,692,1622,774,1600,5137,1863,1604,5174,5530,793,5545,5142,381,1708,1067,714,5122,825,778,1355,349,1487,630,1619,5594,1883,566,5177,889,757,1573,1888,1296,5566,1027,456,842,1402,742,1541,1851,1017,1375,1425,1672,1138,869,857,5577,5502,1361,5588,1446,5387,706,622,1324,997,1588,1382,5498,984,1429,1246,1720,1478,1249,1060,1050,5153,1241,633,805,921,1071,1187,1616,5126,662,5571,1846,906,1135,1251,745,1595,5525,733,5598,1007,1125,1388,711,579,1535,1520,545,904,975,641,5118,5539,1271,1371,5634,1675,604,1853,1011,736,990,362,1144,434,863,1122,5381,1667,5114,1877,1557,1821,848,5180,1293,932,1688,5563,477,799,1162,1396,695,608,1000,851,438,431,473,1626,5548,1873,5528,531,680,927,1472,836,812,1509,1547,414,739,1368,1267,525,5624,409,1484,1432,1452,359,643,1711,1053,5543,470,576,1538,808,1358,1849,1141,1702,600,1670,1717,612,845,627,1180,1685,5536,1321,581,1517,1575,368,5184,5258,699,1385,1481,1629,5394,5505,1030,899,832,1607,763,5187,1348,1578,818,854,1527,373,867,5601,1859,5159,1056,1033,1891,5378,635,1165,796,839,987,1352,860,822,1004,442,501,5140,596,1378,5581,528,1505,1399,5591,337,935,1184,5569,5255,755,5574,708,1014,1870,972]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM277_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % 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.13/0.39 % Computer : n020.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sat Sep 26 23:52:20 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 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.88/0.99 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.41/1.40 % [INFO] Parsing done (408ms).
% 2.41/1.41 % [INFO] Running in sequential loop mode.
% 3.05/1.79 % [INFO] eprover registered as external prover.
% 3.24/1.80 % [INFO] Scanning for conjecture ...
% 3.43/2.03 % [INFO] Found a conjecture (or negated_conjecture) and 360 axioms. Running axiom selection ...
% 4.29/2.23 % [INFO] Axiom selection finished. Selected 334 axioms (removed 26 axioms).
% 5.70/2.65 % [INFO] Problem is typed first-order (TPTP TFF).
% 5.70/2.68 % [INFO] Type checking passed.
% 5.70/2.69 % [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 ...
% 9.56/3.63 % [INFO] [Domain constraints] Detected constraint on vAType
% 9.56/3.63 % [INFO] [Domain constraints] dom(vAType) ⊆ {vYesNo,vNumber,vText}
% 9.90/3.71 % [INFO] [Domain constraints] Detected constraint on vUnOpT
% 9.90/3.71 % [INFO] [Domain constraints] dom(vUnOpT) ⊆ {vnotop}
% 9.90/3.73 % [INFO] [Domain constraints] Detected constraint on vYN
% 9.90/3.73 % [INFO] [Domain constraints] dom(vYN) ⊆ {vyes,vno}
% 11.05/4.12 % [INFO] [Domain constraints] Detected constraint on vYN
% 11.05/4.12 % [INFO] [Domain constraints] dom(vYN) ⊆ {vyes,vno}
% 12.04/4.30 % [INFO] [Domain constraints] Detected constraint on vBinOpT
% 12.04/4.31 % [INFO] [Domain constraints] dom(vBinOpT) ⊆ {vandop,vaddop,vgtop,veqop,vdivop,vmulop,vltop,vsubop,vorop}
% 93.60/48.34 % External prover 'e' found a proof!
% 93.60/48.34 % [INFO] Killing All external provers ...
% 93.60/48.34 % Time passed: 47804ms (effective reasoning time: 46924ms)
% 93.60/48.34 % 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)>
% 93.60/48.35 % Axioms used in derivation (334): 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, 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, 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, DIFF-divop-orop, Tvalue_inv1, dom-OptAType, getQuest-INV, reduceExpProgress-unop-IH0, 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, 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
% 93.60/48.35 % No. of inferences in proof: 672
% 93.60/48.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 47804 ms resp. 46924 ms w/o parsing
% 88.58/48.57 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 88.58/48.57 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------