%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : COM267_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 : n009.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:14 AM UTC 2026
% Result : Theorem 110.22s 94.21s
% Output : Refutation 110.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 247
% Syntax : Number of formulae : 496 ( 213 unt; 0 typ; 0 def)
% Number of atoms : 1508 (1183 equ; 0 cnn)
% Maximal formula atoms : 100 ( 3 avg)
% Number of connectives : 5502 ( 299 ~; 202 |; 595 &;4191 @)
% ( 0 <=>; 215 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 7 avg)
% Number of types : 27 ( 26 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 85 ( 83 usr; 18 con; 0-4 aty)
% Number of variables : 2132 ( 0 ^;1541 !; 591 ?;2132 :)
% 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(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(vT_decl,type,
vT: vstring > vAval ).
thf(vNumber_decl,type,
vNumber: vAType ).
thf(vabind_decl,type,
vabind: vQID > vAval > vAnsMap > vAnsMap ).
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(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(vqsingle_decl,type,
vqsingle: vEntry > vQuestionnaire ).
thf(vMC_decl,type,
vMC: vATMap > vATMap > vMapConf ).
thf(vsomeQuestion_decl,type,
vsomeQuestion: vQID > vLabel > vAType > vOptQuestion ).
thf(vqvar_decl,type,
vqvar: vQID > vExp ).
thf(vatmbind_decl,type,
vatmbind: vQID > vAType > vATMap > vATMap ).
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(vtypeOf_decl,type,
vtypeOf: vAval > vAType ).
thf(vevalBinOp_decl,type,
vevalBinOp: vBinOpT > vAval > vAval > vOptExp ).
thf(vgetQM_decl,type,
vgetQM: vQConf > vQMap ).
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(vappendATMap_decl,type,
vappendATMap: vATMap > vATMap > vATMap ).
thf(vor_decl,type,
vor: vYN > vYN > vYN ).
thf(visSomeAType_decl,type,
visSomeAType: vOptAType > $o ).
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(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(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(82,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(809,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)],[82]) ).
thf(47,axiom,
! [A: vExp] :
( ( A @ vsomeExp @ vgetExp )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getExp-0') ).
thf(629,plain,
! [A: vExp] :
( ( A @ vsomeExp @ vgetExp )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(243,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(4835,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)],[243]) ).
thf(96,axiom,
! [A: vLabel] :
( ( vYesNo @ ( A @ vgetAnswer ) )
= ( A @ vaskYesNo @ vB ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-0') ).
thf(893,plain,
! [A: vLabel] :
( ( vYesNo @ ( A @ vgetAnswer ) )
= ( A @ vaskYesNo @ vB ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(110,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(962,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)],[110]) ).
thf(207,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(4682,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)],[207]) ).
thf(166,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(1295,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)],[166]) ).
thf(27,axiom,
! [A: vUnOpT] : ( A = vnotop ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-UnOpT') ).
thf(352,plain,
! [A: vUnOpT] : ( A = vnotop ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(101,axiom,
! [A: vExp] :
( ! [B: vAval] :
( A
!= ( B @ vconstant ) )
=> ~ ( A @ vexpIsValue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-1') ).
thf(909,plain,
! [A: vExp] :
( ! [B: vAval] :
( A
!= ( B @ vconstant ) )
=> ~ ( A @ vexpIsValue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(1,conjecture,
! [A: vQMap,B: vAType,C: vATMap,D: vATMap,E: vLabel,F: vAnsMap,G: vQID] :
( ( ( D @ ( C @ vMC ) @ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ vtypeQM @ ( F @ vtypeAM @ vMC ) @ vptcheck ) ) )
& ~ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ visValue ) )
=> ? [H: vAnsMap,I: vQMap,J: vQuestionnaire] :
( ( A @ ( F @ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ vreduce ) ) )
= ( J @ ( I @ ( H @ vQC ) ) @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Progress-qsingle-defquestion') ).
thf(2,negated_conjecture,
~ ! [A: vQMap,B: vAType,C: vATMap,D: vATMap,E: vLabel,F: vAnsMap,G: vQID] :
( ( ( D @ ( C @ vMC ) @ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ vtypeQM @ ( F @ vtypeAM @ vMC ) @ vptcheck ) ) )
& ~ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ visValue ) )
=> ? [H: vAnsMap,I: vQMap,J: vQuestionnaire] :
( ( A @ ( F @ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ vreduce ) ) )
= ( J @ ( I @ ( H @ vQC ) ) @ vsomeQConf ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(249,plain,
~ ! [A: vQMap,B: vAType,C: vATMap,D: vATMap,E: vLabel,F: vAnsMap,G: vQID] :
( ( ( D @ ( C @ vMC ) @ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ ( A @ vtypeQM @ ( F @ vtypeAM @ vMC ) @ vptcheck ) ) )
& ~ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ visValue ) )
=> ? [H: vAnsMap,I: vQMap,J: vQuestionnaire] :
( ( A @ ( F @ ( B @ ( E @ ( G @ vdefquestion ) ) @ vqsingle @ vreduce ) ) )
= ( J @ ( I @ ( H @ vQC ) ) @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(149,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(1200,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)],[149]) ).
thf(214,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(4711,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)],[214]) ).
thf(51,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( vnoQuestion
!= ( C @ ( B @ ( A @ vsomeQuestion ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noQuestion-someQuestion') ).
thf(655,plain,
! [A: vQID,B: vLabel,C: vAType] :
( vnoQuestion
!= ( C @ ( B @ ( A @ vsomeQuestion ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(57,axiom,
! [A: vYN,B: vstring] :
( ( A @ vB )
!= ( B @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-B-T') ).
thf(677,plain,
! [A: vYN,B: vstring] :
( ( A @ vB )
!= ( B @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(211,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(4697,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)],[211]) ).
thf(236,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(4807,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)],[236]) ).
thf(196,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(4633,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)],[196]) ).
thf(36,axiom,
! [A: vnat] :
( ( A @ vNum @ vtypeOf )
= vNumber ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-1') ).
thf(384,plain,
! [A: vnat] :
( ( A @ vNum @ vtypeOf )
= vNumber ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(138,axiom,
! [A: vATMap] :
( ( A @ ( vatmempty @ vappendATMap ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendATMap-0') ).
thf(1137,plain,
! [A: vATMap] :
( ( A @ ( vatmempty @ vappendATMap ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(169,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(1310,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)],[169]) ).
thf(201,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(4650,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)],[201]) ).
thf(102,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(913,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)],[102]) ).
thf(38,axiom,
! [A: vLabel] :
( ( vText @ ( A @ vgetAnswer ) )
= ( A @ vaskText @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-2') ).
thf(404,plain,
! [A: vLabel] :
( ( vText @ ( A @ vgetAnswer ) )
= ( A @ vaskText @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(148,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(1196,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)],[148]) ).
thf(135,axiom,
! [A: vYN] :
( ( A @ vB @ vtypeOf )
= vYesNo ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-0') ).
thf(1127,plain,
! [A: vYN] :
( ( A @ vB @ vtypeOf )
= vYesNo ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(14,axiom,
! [A: vnat,B: vnat] :
( ( ( A @ vNum )
= ( B @ vNum ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-Num') ).
thf(288,plain,
! [A: vnat,B: vnat] :
( ( ( A @ vNum )
= ( B @ vNum ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(181,axiom,
! [A: vEntry,B: vQuestionnaire,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqseq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qsingle-qseq') ).
thf(1359,plain,
! [A: vEntry,B: vQuestionnaire,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqseq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[181]) ).
thf(20,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(320,plain,
! [A: vQID,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vqvar )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(154,axiom,
! [A: vGID,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qgroup') ).
thf(1228,plain,
! [A: vGID,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(4,axiom,
! [A: vAType,B: vAType] :
( ( B @ ( A @ ( veqop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-8') ).
thf(257,plain,
! [A: vAType,B: vAType] :
( ( B @ ( A @ ( veqop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(113,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(973,plain,
! [A: vAnsMap] :
( ? [B: vQID,C: vAval,D: vAnsMap] :
( A
= ( D @ ( C @ ( B @ vabind ) ) ) )
| ( A = vaempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(94,axiom,
! [A: vExp,B: vQuestionnaire,C: vQuestionnaire] :
( vqempty
!= ( C @ ( B @ ( A @ vqcond ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qcond') ).
thf(885,plain,
! [A: vExp,B: vQuestionnaire,C: vQuestionnaire] :
( vqempty
!= ( C @ ( B @ ( A @ vqcond ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(70,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(724,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)],[70]) ).
thf(167,axiom,
! [A: vMapConf] :
? [B: vATMap,C: vATMap] :
( A
= ( C @ ( B @ vMC ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-MapConf') ).
thf(1298,plain,
! [A: vMapConf] :
? [B: vATMap,C: vATMap] :
( A
= ( C @ ( B @ vMC ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(158,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(1264,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)],[158]) ).
thf(87,axiom,
! [A: vYN,B: vYN] :
( ( ( B != vyes )
| ( A != vyes ) )
=> ( ( B @ ( A @ vand ) )
= vno ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and-1') ).
thf(838,plain,
! [A: vYN,B: vYN] :
( ( ( B != vyes )
| ( A != vyes ) )
=> ( ( B @ ( A @ vand ) )
= vno ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(170,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(1313,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)],[170]) ).
thf(187,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(1379,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)],[187]) ).
thf(193,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(4617,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)],[193]) ).
thf(156,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(1247,plain,
! [A: vOptQuestion] :
( ( A @ visSomeQuestion )
=> ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vsomeQuestion ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(172,axiom,
! [A: vATMap,B: vATMap] : ( B @ ( A @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Tqempty') ).
thf(1319,plain,
! [A: vATMap,B: vATMap] : ( B @ ( A @ vMC ) @ ( vqempty @ ( B @ ( A @ vMC ) @ vptcheck ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(131,axiom,
! [A: vAType] :
( vnoAType
!= ( A @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noAType-someAType') ).
thf(1100,plain,
! [A: vAType] :
( vnoAType
!= ( A @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(155,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(1232,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)],[155]) ).
thf(185,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(1373,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)],[185]) ).
thf(49,axiom,
! [A: vnat,B: vstring] :
( ( A @ vNum )
!= ( B @ vT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Num-T') ).
thf(646,plain,
! [A: vnat,B: vstring] :
( ( A @ vNum )
!= ( B @ vT ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(188,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(1383,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)],[188]) ).
thf(146,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(1183,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)],[146]) ).
thf(208,axiom,
! [A: vEntry,B: vEntry] :
( ( ( A @ vqsingle )
= ( B @ vqsingle ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qsingle') ).
thf(4686,plain,
! [A: vEntry,B: vEntry] :
( ( ( A @ vqsingle )
= ( B @ vqsingle ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[208]) ).
thf(111,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(966,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)],[111]) ).
thf(12,axiom,
! [A: vOptAType] :
( ( A @ visSomeAType )
=> ? [B: vAType] :
( A
= ( B @ vsomeAType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-true-INV') ).
thf(280,plain,
! [A: vOptAType] :
( ( A @ visSomeAType )
=> ? [B: vAType] :
( A
= ( B @ vsomeAType ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(92,axiom,
! [A: vAval] : ( A @ vconstant @ vexpIsValue ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-0') ).
thf(877,plain,
! [A: vAval] : ( A @ vconstant @ vexpIsValue ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(15,axiom,
! [A: vOptAType] :
( ~ ( A @ visSomeAType )
=> ( A = vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-false-INV') ).
thf(293,plain,
! [A: vOptAType] :
( ~ ( A @ visSomeAType )
=> ( A = vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(127,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(1072,plain,
! [A: vQID,B: vAType,C: vATMap] :
( ( C @ ( B @ ( A @ vatmbind ) ) @ ( A @ vlookupATMap ) )
= ( B @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(192,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(1394,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)],[192]) ).
thf(240,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(4825,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)],[240]) ).
thf(40,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(411,plain,
! [A: vAval,B: vExp,C: vBinOpT,D: vExp] :
( ( A @ vconstant )
!= ( D @ ( C @ ( B @ vbinop ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(199,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(4643,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)],[199]) ).
thf(216,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(4718,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)],[216]) ).
thf(226,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(4751,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)],[226]) ).
thf(60,axiom,
! [A: vAval,B: vQID] :
( ( A @ vconstant )
!= ( B @ vqvar ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-constant-qvar') ).
thf(687,plain,
! [A: vAval,B: vQID] :
( ( A @ vconstant )
!= ( B @ vqvar ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(132,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(1104,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)],[132]) ).
thf(7,axiom,
veqop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-orop') ).
thf(265,plain,
veqop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(90,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(849,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)],[90]) ).
thf(247,axiom,
( ( vaempty @ vtypeAM )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeAM-0') ).
thf(4853,plain,
( ( vaempty @ vtypeAM )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[247]) ).
thf(35,axiom,
! [A: vYN,B: vnat] :
( ( A @ vB )
!= ( B @ vNum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-B-Num') ).
thf(380,plain,
! [A: vYN,B: vnat] :
( ( A @ vB )
!= ( B @ vNum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(104,axiom,
! [A: vAType,B: vAType] :
( ( ( A @ vsomeAType )
= ( B @ vsomeAType ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someAType') ).
thf(942,plain,
! [A: vAType,B: vAType] :
( ( ( A @ vsomeAType )
= ( B @ vsomeAType ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(32,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(366,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)],[32]) ).
thf(79,axiom,
! [A: vQID,B: vQID] :
( ( ( A @ vask )
= ( B @ vask ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-ask') ).
thf(798,plain,
! [A: vQID,B: vQID] :
( ( ( A @ vask )
= ( B @ vask ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(108,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionAType )
= C ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuestionAType-0') ).
thf(957,plain,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionAType )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(117,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(1021,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)],[117]) ).
thf(120,axiom,
! [A: vOptAType] :
( ? [B: vAType] :
( A
= ( B @ vsomeAType ) )
| ( A = vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptAType') ).
thf(1042,plain,
! [A: vOptAType] :
( ? [B: vAType] :
( A
= ( B @ vsomeAType ) )
| ( A = vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(180,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(1355,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)],[180]) ).
thf(151,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(1217,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)],[151]) ).
thf(39,axiom,
! [A: vQID,B: vUnOpT,C: vExp] :
( ( A @ vqvar )
!= ( C @ ( B @ vunop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qvar-unop') ).
thf(407,plain,
! [A: vQID,B: vUnOpT,C: vExp] :
( ( A @ vqvar )
!= ( C @ ( B @ vunop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(184,axiom,
! [A: vQuestionnaire] :
( ( A != vqempty )
=> ~ ( A @ visValue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-1') ).
thf(1370,plain,
! [A: vQuestionnaire] :
( ( A != vqempty )
=> ~ ( A @ visValue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[184]) ).
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(4821,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(83,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(825,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)],[83]) ).
thf(176,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetAM )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAM-0') ).
thf(1343,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetAM )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[176]) ).
thf(5,axiom,
( ( vYesNo @ ( vYesNo @ ( vandop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-6') ).
thf(260,plain,
( ( vYesNo @ ( vYesNo @ ( vandop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(26,axiom,
! [A: vstring] :
( ( A @ vT @ vtypeOf )
= vText ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeOf-2') ).
thf(349,plain,
! [A: vstring] :
( ( A @ vT @ vtypeOf )
= vText ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(89,axiom,
( ( vno @ vnot )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-1') ).
thf(847,plain,
( ( vno @ vnot )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(93,axiom,
! [A: vUnOpT,B: vAType] :
( ( ( B != vYesNo )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-1') ).
thf(879,plain,
! [A: vUnOpT,B: vAType] :
( ( ( B != vYesNo )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vcheckUnOp ) )
= vnoAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(95,axiom,
! [A: vQID,B: vAval,C: vAnsMap] :
( vaempty
!= ( C @ ( B @ ( A @ vabind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-aempty-abind') ).
thf(889,plain,
! [A: vQID,B: vAval,C: vAnsMap] :
( vaempty
!= ( C @ ( B @ ( A @ vabind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(223,axiom,
! [A: vQConf] : ( A @ vsomeQConf @ visSomeQC ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-1') ).
thf(4740,plain,
! [A: vQConf] : ( A @ vsomeQConf @ visSomeQC ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[223]) ).
thf(21,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(324,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)],[21]) ).
thf(63,axiom,
! [A: vYN] :
( ( A @ vB @ ( vnotop @ vevalUnOp ) )
= ( A @ vnot @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalUnOp-0') ).
thf(697,plain,
! [A: vYN] :
( ( A @ vB @ ( vnotop @ vevalUnOp ) )
= ( A @ vnot @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(91,axiom,
! [A: vOptQConf] :
( ~ ( A @ visSomeQC )
=> ( A = vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-false-INV') ).
thf(874,plain,
! [A: vOptQConf] :
( ~ ( A @ visSomeQC )
=> ( A = vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(50,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(650,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)],[50]) ).
thf(46,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(615,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)],[46]) ).
thf(125,axiom,
! [A: vAval,B: vAval] :
( ( ( A @ vconstant )
= ( B @ vconstant ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-constant') ).
thf(1064,plain,
! [A: vAval,B: vAval] :
( ( ( A @ vconstant )
= ( B @ vconstant ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(197,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQuest )
= C ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuest-0') ).
thf(4636,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQuest )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[197]) ).
thf(130,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(1096,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)],[130]) ).
thf(245,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(4840,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)],[245]) ).
thf(238,axiom,
! [A: vEntry,B: vExp,C: vQuestionnaire,D: vQuestionnaire] :
( ( A @ vqsingle )
!= ( D @ ( C @ ( B @ vqcond ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qsingle-qcond') ).
thf(4817,plain,
! [A: vEntry,B: vExp,C: vQuestionnaire,D: vQuestionnaire] :
( ( A @ vqsingle )
!= ( D @ ( C @ ( B @ vqcond ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[238]) ).
thf(160,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(1270,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)],[160]) ).
thf(19,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(317,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)],[19]) ).
thf(43,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(488,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)],[43]) ).
thf(55,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(669,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)],[55]) ).
thf(128,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(1075,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)],[128]) ).
thf(150,axiom,
! [A: vATMap,B: vnat] :
( ( B @ vNum @ vconstant @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-1') ).
thf(1214,plain,
! [A: vATMap,B: vnat] :
( ( B @ vNum @ vconstant @ ( A @ vecheck ) )
= ( vNumber @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(237,axiom,
! [A: vOptQConf] :
( ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) )
| ( A = vnoQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptQConf') ).
thf(4814,plain,
! [A: vOptQConf] :
( ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) )
| ( A = vnoQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[237]) ).
thf(112,axiom,
vyes != vno,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-yes-no') ).
thf(970,plain,
vyes != vno,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(202,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(4653,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)],[202]) ).
thf(175,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(1329,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)],[175]) ).
thf(235,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(4804,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)],[235]) ).
thf(174,axiom,
! [A: vQConf,B: vQConf] :
( ( ( A @ vsomeQConf )
= ( B @ vsomeQConf ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someQConf') ).
thf(1324,plain,
! [A: vQConf,B: vQConf] :
( ( ( A @ vsomeQConf )
= ( B @ vsomeQConf ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(71,axiom,
! [A: vYN,B: vYN] :
( ( ( A @ vB )
= ( B @ vB ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-B') ).
thf(738,plain,
! [A: vYN,B: vYN] :
( ( ( A @ vB )
= ( B @ vB ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(69,axiom,
! [A: vAval] :
( ( A @ vconstant @ vgetExpValue )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getExpValue-0') ).
thf(721,plain,
! [A: vAval] :
( ( A @ vconstant @ vgetExpValue )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(103,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(938,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQMap] :
( vqmempty
!= ( D @ ( C @ ( B @ ( A @ vqmbind ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(30,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(360,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)],[30]) ).
thf(228,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(4765,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)],[228]) ).
thf(118,axiom,
! [A: vATMap,B: vstring] :
( ( B @ vT @ vconstant @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-2') ).
thf(1035,plain,
! [A: vATMap,B: vstring] :
( ( B @ vT @ vconstant @ ( A @ vecheck ) )
= ( vText @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(144,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(1167,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)],[144]) ).
thf(78,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(794,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)],[78]) ).
thf(75,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(765,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)],[75]) ).
thf(124,axiom,
! [A: vYN] :
( ( ( ( A @ vnot )
= vyes )
& ( A = vno ) )
| ( ( ( A @ vnot )
= vno )
& ( A = vyes ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-INV') ).
thf(1054,plain,
! [A: vYN] :
( ( ( ( A @ vnot )
= vyes )
& ( A = vno ) )
| ( ( ( A @ vnot )
= vno )
& ( A = vyes ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(53,axiom,
! [A: vQID,B: vQID] :
( ( ( A @ vqvar )
= ( B @ vqvar ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-qvar') ).
thf(662,plain,
! [A: vQID,B: vQID] :
( ( ( A @ vqvar )
= ( B @ vqvar ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(68,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(718,plain,
! [A: vAval,B: vAval] :
( ( A != B )
=> ( ( B @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vno @ vB @ vconstant @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(100,axiom,
! [A: vQID] :
( ( vatmempty @ ( A @ vlookupATMap ) )
= vnoAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupATMap-0') ).
thf(906,plain,
! [A: vQID] :
( ( vatmempty @ ( A @ vlookupATMap ) )
= vnoAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(213,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(4708,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)],[213]) ).
thf(168,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(1301,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)],[168]) ).
thf(16,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(296,plain,
! [A: vOptQuestion] :
( ? [B: vQID,C: vLabel,D: vAType] :
( A
= ( D @ ( C @ ( B @ vsomeQuestion ) ) ) )
| ( A = vnoQuestion ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(140,axiom,
! [A: vQID,B: vLabel,C: vAType] : ( C @ ( B @ ( A @ vsomeQuestion ) ) @ visSomeQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-1') ).
thf(1154,plain,
! [A: vQID,B: vLabel,C: vAType] : ( C @ ( B @ ( A @ vsomeQuestion ) ) @ visSomeQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(62,axiom,
vYesNo != vNumber,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-YesNo-Number') ).
thf(694,plain,
vYesNo != vNumber,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(190,axiom,
vqempty @ visValue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-0') ).
thf(1389,plain,
vqempty @ visValue,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[190]) ).
thf(234,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(4801,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)],[234]) ).
thf(72,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(743,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)],[72]) ).
thf(229,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(4769,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)],[229]) ).
thf(134,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(1124,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)],[134]) ).
thf(105,axiom,
! [A: vExp] :
( ( A @ vexpIsValue )
=> ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','expIsValue-true-INV') ).
thf(947,plain,
! [A: vExp] :
( ( A @ vexpIsValue )
=> ? [B: vAval] :
( A
= ( B @ vconstant ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(153,axiom,
! [A: vQID,B: vAType,C: vATMap] :
( vatmempty
!= ( C @ ( B @ ( A @ vatmbind ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-atmempty-atmbind') ).
thf(1224,plain,
! [A: vQID,B: vAType,C: vATMap] :
( vatmempty
!= ( C @ ( B @ ( A @ vatmbind ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(212,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(4704,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)],[212]) ).
thf(85,axiom,
! [A: vQuestionnaire,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqseq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qseq') ).
thf(831,plain,
! [A: vQuestionnaire,B: vQuestionnaire] :
( vqempty
!= ( B @ ( A @ vqseq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(58,axiom,
! [A: vOptExp] :
( ~ ( A @ visSomeExp )
=> ( A = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-false-INV') ).
thf(681,plain,
! [A: vOptExp] :
( ~ ( A @ visSomeExp )
=> ( A = vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(164,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(1282,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)],[164]) ).
thf(10,axiom,
vYesNo != vText,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-YesNo-Text') ).
thf(274,plain,
vYesNo != vText,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
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(4828,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(34,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(377,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)],[34]) ).
thf(9,axiom,
vandop != vorop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-andop-orop') ).
thf(271,plain,
vandop != vorop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(186,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(1376,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)],[186]) ).
thf(210,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(4694,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)],[210]) ).
thf(37,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(387,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)],[37]) ).
thf(25,axiom,
! [A: vAval,B: vUnOpT,C: vExp] :
( ( A @ vconstant )
!= ( C @ ( B @ vunop ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-constant-unop') ).
thf(345,plain,
! [A: vAval,B: vUnOpT,C: vExp] :
( ( A @ vconstant )
!= ( C @ ( B @ vunop ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(142,axiom,
! [A: vAnsMap] :
( ( A @ ( vaempty @ vappendAnsMap ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','appendAnsMap-0') ).
thf(1162,plain,
! [A: vAnsMap] :
( ( A @ ( vaempty @ vappendAnsMap ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(42,axiom,
! [A: vstring,B: vstring] :
( ( ( A @ vT )
= ( B @ vT ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-T') ).
thf(483,plain,
! [A: vstring,B: vstring] :
( ( ( A @ vT )
= ( B @ vT ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(64,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(700,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)],[64]) ).
thf(217,axiom,
! [A: vQConf] :
( ( A @ vsomeQConf @ vgetQC )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQC-0') ).
thf(4720,plain,
! [A: vQConf] :
( ( A @ vsomeQConf @ vgetQC )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[217]) ).
thf(17,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(299,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)],[17]) ).
thf(157,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(1250,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)],[157]) ).
thf(3,axiom,
( ( vYesNo @ ( vYesNo @ ( vorop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkBinOp-7') ).
thf(255,plain,
( ( vYesNo @ ( vYesNo @ ( vorop @ vcheckBinOp ) ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(28,axiom,
! [A: vOptExp] :
( ? [B: vExp] :
( A
= ( B @ vsomeExp ) )
| ( A = vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptExp') ).
thf(355,plain,
! [A: vOptExp] :
( ? [B: vExp] :
( A
= ( B @ vsomeExp ) )
| ( A = vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(145,axiom,
~ ( vnoQConf @ visSomeQC ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-0') ).
thf(1181,plain,
~ ( vnoQConf @ visSomeQC ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(122,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(1049,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)],[122]) ).
thf(107,axiom,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionLabel )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQuestionLabel-0') ).
thf(954,plain,
! [A: vQID,B: vLabel,C: vAType] :
( ( C @ ( B @ ( A @ vsomeQuestion ) ) @ vgetQuestionLabel )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(159,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(1267,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)],[159]) ).
thf(66,axiom,
! [A: vAval] :
( ( A @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','evalBinOp-8') ).
thf(705,plain,
! [A: vAval] :
( ( A @ ( A @ ( veqop @ vevalBinOp ) ) )
= ( vyes @ vB @ vconstant @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(141,axiom,
! [A: vYN,B: vYN] :
( ( ( B != vno )
| ( A != vno ) )
=> ( ( B @ ( A @ vor ) )
= vyes ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','or-1') ).
thf(1156,plain,
! [A: vYN,B: vYN] :
( ( ( B != vno )
| ( A != vno ) )
=> ( ( B @ ( A @ vor ) )
= vyes ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(56,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(673,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)],[56]) ).
thf(23,axiom,
! [A: vOptExp] :
( ( A @ visSomeExp )
=> ? [B: vExp] :
( A
= ( B @ vsomeExp ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-true-INV') ).
thf(338,plain,
! [A: vOptExp] :
( ( A @ visSomeExp )
=> ? [B: vExp] :
( A
= ( B @ vsomeExp ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(222,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(4737,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)],[222]) ).
thf(136,axiom,
! [A: vATMap,B: vQID] :
( ( B @ vqvar @ ( A @ vecheck ) )
= ( A @ ( B @ vlookupATMap ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-3') ).
thf(1130,plain,
! [A: vATMap,B: vQID] :
( ( B @ vqvar @ ( A @ vecheck ) )
= ( A @ ( B @ vlookupATMap ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(165,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(1285,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)],[165]) ).
thf(22,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(331,plain,
! [A: vUnOpT,B: vAval] :
( ( ! [C: vYN] :
( B
!= ( C @ vB ) )
| ( A != vnotop ) )
=> ( ( B @ ( A @ vevalUnOp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(147,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(1186,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)],[147]) ).
thf(119,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(1038,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)],[119]) ).
thf(33,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(370,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)],[33]) ).
thf(65,axiom,
! [A: vExp] : ( A @ vsomeExp @ visSomeExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-1') ).
thf(703,plain,
! [A: vExp] : ( A @ vsomeExp @ visSomeExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(194,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(4624,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)],[194]) ).
thf(152,axiom,
! [A: vATMap] :
( ( A @ ( vatmempty @ vintersectATM ) )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','intersectATM-0') ).
thf(1221,plain,
! [A: vATMap] :
( ( A @ ( vatmempty @ vintersectATM ) )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(225,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(4748,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)],[225]) ).
thf(123,axiom,
( ( vyes @ ( vyes @ vand ) )
= vyes ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','and-0') ).
thf(1052,plain,
( ( vyes @ ( vyes @ vand ) )
= vyes ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(139,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(1140,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)],[139]) ).
thf(18,axiom,
! [A: vQID,B: vAnsMap] :
( ~ ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= vnoExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-2') ).
thf(314,plain,
! [A: vQID,B: vAnsMap] :
( ~ ( B @ ( A @ vlookupAnsMap ) @ visSomeAval )
=> ( ( B @ ( A @ vqvar @ vreduceExp ) )
= vnoExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(161,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(1272,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID] :
( ( C @ ( B @ ( A @ vdefquestion ) ) )
!= ( D @ vask ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(244,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(4838,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)],[244]) ).
thf(45,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(595,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)],[45]) ).
thf(198,axiom,
! [A: vEntry,B: vGID,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqgroup ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qsingle-qgroup') ).
thf(4639,plain,
! [A: vEntry,B: vGID,C: vQuestionnaire] :
( ( A @ vqsingle )
!= ( C @ ( B @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[198]) ).
thf(171,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(1316,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)],[171]) ).
thf(219,axiom,
! [A: vQuestionnaire] :
( ( A @ visValue )
=> ( A = vqempty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-true-INV') ).
thf(4727,plain,
! [A: vQuestionnaire] :
( ( A @ visValue )
=> ( A = vqempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[219]) ).
thf(73,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(759,plain,
! [A: vQuestionnaire,B: vQuestionnaire,C: vGID,D: vQuestionnaire] :
( ( B @ ( A @ vqseq ) )
!= ( D @ ( C @ vqgroup ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(200,axiom,
! [A: vQConf] :
( vnoQConf
!= ( A @ vsomeQConf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noQConf-someQConf') ).
thf(4646,plain,
! [A: vQConf] :
( vnoQConf
!= ( A @ vsomeQConf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[200]) ).
thf(88,axiom,
! [A: vQID] :
( ( vqmempty @ ( A @ vlookupQMap ) )
= vnoQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lookupQMap-0') ).
thf(844,plain,
! [A: vQID] :
( ( vqmempty @ ( A @ vlookupQMap ) )
= vnoQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(173,axiom,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vQC ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-QConf') ).
thf(1321,plain,
! [A: vQConf] :
? [B: vAnsMap,C: vQMap,D: vQuestionnaire] :
( A
= ( D @ ( C @ ( B @ vQC ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(203,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(4656,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)],[203]) ).
thf(114,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(976,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)],[114]) ).
thf(99,axiom,
! [A: vYN] :
( ( A = vno )
| ( A = vyes ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-YN') ).
thf(903,plain,
! [A: vYN] :
( ( A = vno )
| ( A = vyes ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(115,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(1010,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)],[115]) ).
thf(191,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(1390,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)],[191]) ).
thf(220,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(4730,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)],[220]) ).
thf(206,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(4678,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)],[206]) ).
thf(162,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(1276,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)],[162]) ).
thf(189,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(1385,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)],[189]) ).
thf(97,axiom,
! [A: vOptQuestion] :
( ~ ( A @ visSomeQuestion )
=> ( A = vnoQuestion ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-false-INV') ).
thf(896,plain,
! [A: vOptQuestion] :
( ~ ( A @ visSomeQuestion )
=> ( A = vnoQuestion ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(48,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(632,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)],[48]) ).
thf(215,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(4715,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)],[215]) ).
thf(232,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(4791,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)],[232]) ).
thf(248,axiom,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQM )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getQM-0') ).
thf(4855,plain,
! [A: vAnsMap,B: vQMap,C: vQuestionnaire] :
( ( C @ ( B @ ( A @ vQC ) ) @ vgetQM )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[248]) ).
thf(54,axiom,
! [A: vAType] : ( A @ vsomeAType @ visSomeAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-1') ).
thf(667,plain,
! [A: vAType] : ( A @ vsomeAType @ visSomeAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(74,axiom,
( ( vYesNo @ ( vnotop @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','checkUnOp-0') ).
thf(763,plain,
( ( vYesNo @ ( vnotop @ vcheckUnOp ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(98,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(899,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)],[98]) ).
thf(59,axiom,
! [A: vAType] :
( ( A = vText )
| ( A = vNumber )
| ( A = vYesNo ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-AType') ).
thf(684,plain,
! [A: vAType] :
( ( A = vText )
| ( A = vNumber )
| ( A = vYesNo ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(121,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(1045,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)],[121]) ).
thf(137,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(1133,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)],[137]) ).
thf(178,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(1348,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)],[178]) ).
thf(233,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(4794,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)],[233]) ).
thf(163,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(1280,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)],[163]) ).
thf(246,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(4843,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)],[246]) ).
thf(231,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(4787,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)],[231]) ).
thf(77,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(790,plain,
! [A: vQID,B: vAType,C: vExp,D: vQID] :
( ( C @ ( B @ ( A @ vvalue ) ) )
!= ( D @ vask ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(205,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(4663,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)],[205]) ).
thf(106,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(950,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)],[106]) ).
thf(86,axiom,
! [A: vATMap,B: vYN] :
( ( B @ vB @ vconstant @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','echeck-0') ).
thf(835,plain,
! [A: vATMap,B: vYN] :
( ( B @ vB @ vconstant @ ( A @ vecheck ) )
= ( vYesNo @ vsomeAType ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(6,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(262,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)],[6]) ).
thf(182,axiom,
! [A: vEntry] :
( vqempty
!= ( A @ vqsingle ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-qempty-qsingle') ).
thf(1363,plain,
! [A: vEntry] :
( vqempty
!= ( A @ vqsingle ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[182]) ).
thf(24,axiom,
! [A: vExp] :
( vnoExp
!= ( A @ vsomeExp ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noExp-someExp') ).
thf(341,plain,
! [A: vExp] :
( vnoExp
!= ( A @ vsomeExp ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(227,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(4755,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)],[227]) ).
thf(8,axiom,
veqop != vandop,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-eqop-andop') ).
thf(268,plain,
veqop != vandop,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(84,axiom,
! [A: vAval,B: vAnsMap] :
( ( B @ ( A @ vconstant @ vreduceExp ) )
= vnoExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduceExp-0') ).
thf(828,plain,
! [A: vAval,B: vAnsMap] :
( ( B @ ( A @ vconstant @ vreduceExp ) )
= vnoExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(109,axiom,
~ ( vnoQuestion @ visSomeQuestion ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQuestion-0') ).
thf(960,plain,
~ ( vnoQuestion @ visSomeQuestion ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(143,axiom,
( ( vyes @ vnot )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not-0') ).
thf(1165,plain,
( ( vyes @ vnot )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(177,axiom,
( ( vqmempty @ vtypeQM )
= vatmempty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','typeQM-0') ).
thf(1346,plain,
( ( vqmempty @ vtypeQM )
= vatmempty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[177]) ).
thf(13,axiom,
! [A: vExp,B: vExp] :
( ( ( A @ vsomeExp )
= ( B @ vsomeExp ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-someExp') ).
thf(283,plain,
! [A: vExp,B: vExp] :
( ( ( A @ vsomeExp )
= ( B @ vsomeExp ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(41,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(415,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)],[41]) ).
thf(29,axiom,
~ ( vnoExp @ visSomeExp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeExp-0') ).
thf(358,plain,
~ ( vnoExp @ visSomeExp ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(81,axiom,
( ( vno @ ( vno @ vor ) )
= vno ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','or-0') ).
thf(807,plain,
( ( vno @ ( vno @ vor ) )
= vno ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(129,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(1093,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)],[129]) ).
thf(179,axiom,
! [A: vAnsMap,B: vQMap] :
( ( B @ ( A @ ( vqempty @ vreduce ) ) )
= vnoQConf ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','reduce-0') ).
thf(1352,plain,
! [A: vAnsMap,B: vQMap] :
( ( B @ ( A @ ( vqempty @ vreduce ) ) )
= vnoQConf ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(242,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(4831,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)],[242]) ).
thf(204,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(4659,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)],[204]) ).
thf(209,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(4691,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)],[209]) ).
thf(133,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(1120,plain,
! [A: vQID,B: vLabel,C: vAType,D: vQID] :
( ( C @ ( B @ ( A @ vquestion ) ) )
!= ( D @ vask ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(11,axiom,
vNumber != vText,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-Number-Text') ).
thf(277,plain,
vNumber != vText,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(61,axiom,
! [A: vLabel] :
( ( vNumber @ ( A @ vgetAnswer ) )
= ( A @ vaskNumber @ vNum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAnswer-1') ).
thf(691,plain,
! [A: vLabel] :
( ( vNumber @ ( A @ vgetAnswer ) )
= ( A @ vaskNumber @ vNum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(80,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(803,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)],[80]) ).
thf(183,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(1367,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)],[183]) ).
thf(195,axiom,
! [A: vQuestionnaire] :
( ~ ( A @ visValue )
=> ? [B: vQuestionnaire] :
( ( A = B )
& ( B != vqempty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isValue-false-INV') ).
thf(4627,plain,
! [A: vQuestionnaire] :
( ~ ( A @ visValue )
=> ? [B: vQuestionnaire] :
( ( A = B )
& ( B != vqempty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[195]) ).
thf(218,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(4723,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)],[218]) ).
thf(230,axiom,
! [A: vOptQConf] :
( ( A @ visSomeQC )
=> ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeQC-true-INV') ).
thf(4784,plain,
! [A: vOptQConf] :
( ( A @ visSomeQC )
=> ? [B: vQConf] :
( A
= ( B @ vsomeQConf ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[230]) ).
thf(52,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(659,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)],[52]) ).
thf(44,axiom,
! [A: vAType] :
( ( A @ vsomeAType @ vgetAType )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','getAType-0') ).
thf(592,plain,
! [A: vAType] :
( ( A @ vsomeAType @ vgetAType )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(126,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(1069,plain,
! [A: vATMap] :
( ? [B: vQID,C: vAType,D: vATMap] :
( A
= ( D @ ( C @ ( B @ vatmbind ) ) ) )
| ( A = vatmempty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(31,axiom,
~ ( vnoAType @ visSomeAType ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeAType-0') ).
thf(364,plain,
~ ( vnoAType @ visSomeAType ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(67,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(708,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)],[67]) ).
thf(224,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(4742,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)],[224]) ).
thf(76,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(775,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)],[76]) ).
thf(116,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(1014,plain,
! [A: vExp] :
( ~ ( A @ vexpIsValue )
=> ? [B: vExp] :
( ( A = B )
& ! [C: vAval] :
( B
!= ( C @ vconstant ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(221,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(4734,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)],[221]) ).
thf(4887,plain,
$false,
inference(e,[status(thm)],[809,629,4835,893,962,4682,1295,352,909,249,1200,4711,655,677,4697,4807,4633,384,1137,1310,4650,913,404,1196,1127,288,1359,320,1228,257,973,885,724,1298,1264,838,1313,1379,4617,1247,1319,1100,1232,1373,646,1383,1183,4686,966,280,877,293,1072,1394,4825,411,4643,4718,4751,687,1104,265,849,4853,380,942,366,798,957,1021,1042,1355,1217,407,1370,4821,825,1343,260,349,847,879,889,4740,324,697,874,650,615,1064,4636,1096,4840,4817,1270,317,488,669,1075,1214,4814,970,4653,1329,4804,1324,738,721,938,360,4765,1035,1167,794,765,1054,662,718,906,4708,1301,296,1154,694,1389,4801,743,4769,1124,947,1224,4704,831,681,1282,274,4828,377,271,1376,4694,387,345,1162,483,700,4720,299,1250,255,355,1181,1049,954,1267,705,1156,673,338,4737,1130,1285,331,1186,1038,370,703,4624,1221,4748,1052,1140,314,1272,4838,595,4639,1316,4727,759,4646,844,1321,4656,976,903,1010,1390,4730,4678,1276,1385,896,632,4715,4791,4855,667,763,899,684,1045,1133,1348,4794,1280,4843,4787,790,4663,950,835,262,1363,341,4755,268,828,960,1165,1346,283,415,358,807,1093,1352,4831,4659,4691,1120,277,691,803,1367,4627,4723,4784,659,592,1069,364,708,4742,775,1014,4734]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM267_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.12/0.39 % Computer : n009.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sat Sep 26 23:50:44 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 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.85/0.98 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.84/1.40 % [INFO] Parsing done (411ms).
% 2.32/1.41 % [INFO] Running in sequential loop mode.
% 3.03/1.79 % [INFO] eprover registered as external prover.
% 3.22/1.80 % [INFO] Scanning for conjecture ...
% 3.67/2.04 % [INFO] Found a conjecture (or negated_conjecture) and 359 axioms. Running axiom selection ...
% 4.27/2.23 % [INFO] Axiom selection finished. Selected 246 axioms (removed 113 axioms).
% 5.11/2.58 % [INFO] Problem is typed first-order (TPTP TFF).
% 5.46/2.61 % [INFO] Type checking passed.
% 5.46/2.61 % [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 ...
% 7.73/3.13 % [INFO] [Domain constraints] Detected constraint on vUnOpT
% 7.73/3.13 % [INFO] [Domain constraints] dom(vUnOpT) ⊆ {vnotop}
% 9.51/3.76 % [INFO] [Domain constraints] Detected constraint on vAType
% 9.51/3.76 % [INFO] [Domain constraints] dom(vAType) ⊆ {vYesNo,vNumber,vText}
% 10.26/3.93 % [INFO] [Domain constraints] Detected constraint on vYN
% 10.26/3.93 % [INFO] [Domain constraints] dom(vYN) ⊆ {vyes,vno}
% 10.78/4.08 % [INFO] [Domain constraints] Detected constraint on vYN
% 10.78/4.08 % [INFO] [Domain constraints] dom(vYN) ⊆ {vyes,vno}
% 110.22/94.21 % External prover 'e' found a proof!
% 110.22/94.21 % [INFO] Killing All external provers ...
% 110.22/94.21 % Time passed: 93674ms (effective reasoning time: 92792ms)
% 110.22/94.21 % 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)>
% 110.22/94.21 % Axioms used in derivation (246): Task_inv2, getQC-0, reduceExp-10, intersectATM-INV, 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, Tqcond_inv5, reduce-0, DIFF-eqop-andop, 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-qsingle-qseq, lookupQMap-1, reduceExp-2, isSomeQC-0, isSomeQuestion-1, dom-YN, getAnswer-1, Tqseq, getAM-0, reduce-13, appendAnsMap-0, evalUnOp-0, isSomeQC-false-INV, intersectATM-1, dom-AnsMap, appendATMap-0, DIFF-value-ask, reduce-11, EQ-qsingle, lookupATMap-0, isSomeQuestion-false-INV, lookupATMap-INV, isSomeExp-true-INV, expIsValue-false-INV, reduce-4, EQ-unop, reduceExp-8, getAnswer-0, or-0, EQ-someQConf, reduce-15, reduce-1, getExpValue-0, EQ-value, dom-OptExp, isValue-1, EQ-someExp, dom-Questionnaire, DIFF-qseq-qcond, EQ-Num, reduceExp-5, dom-OptQuestion, DIFF-B-Num, Tvalue_inv1, dom-OptAType, getQuest-INV, echeck-3, checkUnOp-1, appendAnsMap-INV, DIFF-andop-orop, intersectATM-0, reduce-10, and-INV, reduceExp-1, evalBinOp-9, isSomeQuestion-0, dom-QMap, typeOf-1, Tqgroup, Tqseq_inv3, DIFF-qsingle-qcond, isSomeAType-true-INV, isValue-false-INV, EQ-someAType, DIFF-YesNo-Text, typeOf-INV, DIFF-question-defquestion, dom-ATMap, echeck-7, DIFF-Number-Text, Tqempty_inv2, reduce-9, EQ-qseq, reduce-14, appendAnsMap-1, EQ-question, lookupQMap-2, Tquestion_inv2, dom-Aval, EQ-binop, typeQM-1, DIFF-qempty-qgroup, lookupQMap-INV, typeAM-1, DIFF-defquestion-ask, dom-UnOpT, Tqempty, getAnswer-2, reduce-5, isValue-0, reduceExp-4, getQM-INV, reduce-12, reduce-2, Tquestion_inv1, DIFF-noQConf-someQConf, and-1, EQ-ask, checkBinOp-8, EQ-abind, or-INV, reduceExp-9, EQ-constant, Task_inv4, DIFF-qvar-unop, or-1, checkUnOp-0, Tqcond, EQ-qmbind, echeck-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, lookupATMap-1, Tvalue_inv4, evalBinOp-8, not-INV, getQuestionAType-0, Tquestion_inv3, DIFF-qempty-qseq, DIFF-noQuestion-someQuestion, dom-QConf, dom-Exp, typeOf-2, reduce-8, EQ-atmbind, DIFF-aempty-abind, DIFF-qmempty-qmbind, checkBinOp-7, Tqempty_inv1, isSomeAType-0, qcappend-0, reduceExp-0, DIFF-Num-T, isSomeExp-1, Tqseq_inv2, evalUnOp-INV, DIFF-question-ask, DIFF-question-value, DIFF-constant-binop, Tvalue, reduce-6, not-1, Tquestion, Tdefquestion, EQ-qgroup, getQuestionLabel-0, Tqcond_inv7, getQM-0, appendATMap-INV, reduceExp-3, typeAM-0, Tqgroup_inv, Tvalue_inv3, Tdefquestion_inv2, echeck-5, expIsValue-0, Tqseq_inv4, isSomeQC-true-INV, Tqcond_inv2, DIFF-qvar-binop, isSomeExp-false-INV, DIFF-atmempty-atmbind, checkUnOp-INV, and-0, EQ-T, expIsValue-1, appendATMap-1, Tqseq_inv1, echeck-6, DIFF-constant-qvar, getQuest-0, isSomeExp-0, DIFF-binop-unop, Tqcond_inv6, getAnswer-INV, lookupATMap-2, lookupAnsMap-2, EQ-defquestion, evalBinOp-7, DIFF-noAType-someAType, DIFF-qempty-qcond, Task_inv1, Task, echeck-2, Tdefquestion_inv1, DIFF-noExp-someExp, DIFF-constant-unop, qcappend-INV, evalUnOp-1, EQ-MC, intersectATM-2, reduce-3, Tqcond_inv1, lookupQMap-0, dom-MapConf, isSomeQC-1, expIsValue-true-INV, EQ-QC, DIFF-B-T, EQ-someQuestion, Tqcond_inv3, typeQM-INV
% 110.22/94.21 % No. of inferences in proof: 496
% 110.22/94.21 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 93674 ms resp. 92792 ms w/o parsing
% 110.99/94.46 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 110.99/94.47 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------