%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM251_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 06:21:38 PM UTC 2026 % Result : Theorem 27.69s 4.39s % Output : Proof 37.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM251_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.34 % Computer : n027.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 19:42:04 EDT 2026 % 0.16/0.34 % CPUTime : % 0.52/0.60 ________ _____ % 0.52/0.60 ___ __ \_________(_)________________________________ % 0.52/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.52/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.52/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.52/0.60 % 0.52/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.52/0.60 (2023-06-19) % 0.52/0.60 % 0.52/0.60 (c) Philipp Rümmer, 2009-2023 % 0.52/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.52/0.60 Amanda Stjerna. % 0.52/0.60 Free software under BSD-3-Clause. % 0.52/0.60 % 0.52/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.52/0.60 % 0.52/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.52/0.61 Running up to 7 provers in parallel. % 0.52/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.52/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.52/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.52/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.52/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.52/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.52/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 10.08/2.09 Prover 0: Preprocessing ... % 10.08/2.09 Prover 5: Preprocessing ... % 10.08/2.09 Prover 3: Preprocessing ... % 10.08/2.09 Prover 2: Preprocessing ... % 10.08/2.10 Prover 6: Preprocessing ... % 10.08/2.11 Prover 4: Preprocessing ... % 10.08/2.11 Prover 1: Preprocessing ... % 23.83/3.89 Prover 1: Warning: ignoring some quantifiers % 24.61/3.90 Prover 3: Warning: ignoring some quantifiers % 24.61/3.95 Prover 3: Constructing countermodel ... % 24.61/3.98 Prover 1: Constructing countermodel ... % 25.54/4.04 Prover 6: Proving ... % 27.69/4.39 Prover 3: proved (3765ms) % 27.69/4.39 % 27.69/4.39 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.69/4.39 % 27.69/4.39 Prover 6: stopped % 28.44/4.40 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 28.44/4.40 Prover 5: Proving ... % 28.44/4.40 Prover 5: stopped % 28.44/4.40 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 28.44/4.41 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 28.44/4.42 Prover 4: Warning: ignoring some quantifiers % 29.23/4.54 Prover 4: Constructing countermodel ... % 30.00/4.64 Prover 0: Proving ... % 30.00/4.64 Prover 0: stopped % 30.00/4.64 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 33.23/5.09 Prover 7: Preprocessing ... % 33.23/5.10 Prover 10: Preprocessing ... % 34.10/5.13 Prover 8: Preprocessing ... % 34.10/5.19 Prover 1: Found proof (size 10) % 34.10/5.19 Prover 1: proved (4571ms) % 34.10/5.19 Prover 4: stopped % 34.68/5.25 Prover 11: Preprocessing ... % 35.45/5.30 Prover 2: Proving ... % 35.45/5.30 Prover 2: stopped % 36.17/5.40 Prover 10: stopped % 36.17/5.41 Prover 7: stopped % 36.17/5.43 Prover 11: stopped % 37.53/5.71 Prover 8: Warning: ignoring some quantifiers % 37.53/5.74 Prover 8: Constructing countermodel ... % 37.53/5.76 Prover 8: stopped % 37.53/5.76 % 37.53/5.76 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.53/5.76 % 37.53/5.77 % SZS output start Proof for theBenchmark % 37.53/5.79 Assumptions after simplification: % 37.53/5.79 --------------------------------- % 37.53/5.79 % 37.53/5.79 (evalBinOp-0) % 37.95/5.84 vBinOpT(vaddop) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vAval] : ! [v3: % 37.95/5.84 vAval] : ! [v4: vOptExp] : ( ~ (vevalBinOp(vaddop, v2, v3) = v4) | ~ % 37.95/5.84 (vNum(v1) = v3) | ~ (vNum(v0) = v2) | ~ vnat(v1) | ~ vnat(v0) | ? [v5: % 37.95/5.84 vnat] : ? [v6: vAval] : ? [v7: vExp] : (vplus(v0, v1) = v5 & % 37.95/5.84 vsomeExp(v7) = v4 & vNum(v5) = v6 & vconstant(v6) = v7 & vOptExp(v4) & % 37.95/5.84 vnat(v5) & vExp(v7) & vAval(v6))) % 37.95/5.84 % 37.95/5.84 (evalBinOpProgress-addop-Num-Num) % 37.95/5.84 vBinOpT(vaddop) & ? [v0: vnat] : ? [v1: vnat] : ? [v2: vAval] : ? [v3: % 37.95/5.84 vATMap] : ? [v4: vAval] : ? [v5: vAType] : ? [v6: vExp] : ? [v7: vExp] : % 37.95/5.84 ? [v8: vExp] : ? [v9: vOptAType] : ? [v10: vOptExp] : (vecheck(v3, v8) = v9 % 37.95/5.84 & vevalBinOp(vaddop, v2, v4) = v10 & vNum(v1) = v4 & vNum(v0) = v2 & % 37.95/5.84 vsomeAType(v5) = v9 & vbinop(v6, vaddop, v7) = v8 & vconstant(v4) = v7 & % 37.95/5.84 vconstant(v2) = v6 & vAType(v5) & vOptExp(v10) & vnat(v1) & vnat(v0) & % 37.95/5.84 vExp(v8) & vExp(v7) & vExp(v6) & vAval(v4) & vAval(v2) & vATMap(v3) & % 37.95/5.84 vOptAType(v9) & ! [v11: vExp] : ( ~ (vsomeExp(v11) = v10) | ~ vExp(v11))) % 37.95/5.84 % 37.95/5.84 Further assumptions not needed in the proof: % 37.95/5.84 -------------------------------------------- % 37.95/5.84 DIFF-B-Num, DIFF-B-T, DIFF-Num-T, DIFF-Number-Text, DIFF-YesNo-Number, % 37.95/5.84 DIFF-YesNo-Text, DIFF-addop-andop, DIFF-addop-divop, DIFF-addop-eqop, % 37.95/5.84 DIFF-addop-gtop, DIFF-addop-ltop, DIFF-addop-mulop, DIFF-addop-orop, % 37.95/5.84 DIFF-addop-subop, DIFF-aempty-abind, DIFF-andop-orop, DIFF-atempty-atcons, % 37.95/5.84 DIFF-atmempty-atmbind, DIFF-binop-unop, DIFF-constant-binop, DIFF-constant-qvar, % 37.95/5.84 DIFF-constant-unop, DIFF-defquestion-ask, DIFF-divop-andop, DIFF-divop-eqop, % 37.95/5.84 DIFF-divop-gtop, DIFF-divop-ltop, DIFF-divop-orop, DIFF-eqop-andop, % 37.95/5.84 DIFF-eqop-gtop, DIFF-eqop-ltop, DIFF-eqop-orop, DIFF-gtop-andop, DIFF-gtop-ltop, % 37.95/5.84 DIFF-gtop-orop, DIFF-initGID-enumGID, DIFF-initLabel-enumLabel, % 37.95/5.84 DIFF-initQID-enumQID, DIFF-initchar-enumchar, DIFF-ltop-andop, DIFF-ltop-orop, % 37.95/5.84 DIFF-mulop-andop, DIFF-mulop-divop, DIFF-mulop-eqop, DIFF-mulop-gtop, % 37.95/5.84 DIFF-mulop-ltop, DIFF-mulop-orop, DIFF-noAType-someAType, DIFF-noAval-someAval, % 37.95/5.84 DIFF-noExp-someExp, DIFF-noMapConf-someMapConf, DIFF-noQConf-someQConf, % 37.95/5.84 DIFF-noQuestion-someQuestion, DIFF-qcond-qgroup, DIFF-qempty-qcond, % 37.95/5.84 DIFF-qempty-qgroup, DIFF-qempty-qseq, DIFF-qempty-qsingle, DIFF-qmempty-qmbind, % 37.95/5.84 DIFF-qseq-qcond, DIFF-qseq-qgroup, DIFF-qsingle-qcond, DIFF-qsingle-qgroup, % 37.95/5.84 DIFF-qsingle-qseq, DIFF-question-ask, DIFF-question-defquestion, % 37.95/5.84 DIFF-question-value, DIFF-qvar-binop, DIFF-qvar-unop, DIFF-sempty-scons, % 37.95/5.84 DIFF-subop-andop, DIFF-subop-divop, DIFF-subop-eqop, DIFF-subop-gtop, % 37.95/5.84 DIFF-subop-ltop, DIFF-subop-mulop, DIFF-subop-orop, DIFF-value-ask, % 37.95/5.84 DIFF-value-defquestion, DIFF-yes-no, DIFF-zero-succ, EQ-B, EQ-MC, EQ-Num, EQ-QC, % 37.95/5.84 EQ-T, EQ-abind, EQ-ask, EQ-atcons, EQ-atmbind, EQ-binop, EQ-constant, % 37.95/5.84 EQ-defquestion, EQ-enumGID, EQ-enumLabel, EQ-enumQID, EQ-enumchar, EQ-qcond, % 37.95/5.84 EQ-qgroup, EQ-qmbind, EQ-qseq, EQ-qsingle, EQ-question, EQ-qvar, EQ-scons, % 37.95/5.84 EQ-someAType, EQ-someAval, EQ-someExp, EQ-someMapConf, EQ-someQConf, % 37.95/5.84 EQ-someQuestion, EQ-succ, EQ-unop, EQ-value, Task, Task_inv1, Task_inv2, % 37.95/5.84 Task_inv3, Task_inv4, Tdefquestion, Tdefquestion_inv1, Tdefquestion_inv2, % 37.95/5.84 Tdefquestion_inv3, Tqcond, Tqcond_inv1, Tqcond_inv2, Tqcond_inv3, Tqcond_inv4, % 37.95/5.84 Tqcond_inv5, Tqcond_inv6, Tqcond_inv7, Tqempty, Tqempty_inv1, Tqempty_inv2, % 37.95/5.84 Tqgroup, Tqgroup_inv, Tqseq, Tqseq_inv1, Tqseq_inv2, Tqseq_inv3, Tqseq_inv4, % 37.95/5.84 Tquestion, Tquestion_inv1, Tquestion_inv2, Tquestion_inv3, Tvalue, Tvalue_inv1, % 37.95/5.84 Tvalue_inv2, Tvalue_inv3, Tvalue_inv4, and-0, and-1, and-INV, append-0, % 37.95/5.84 append-1, append-INV, appendATMap-0, appendATMap-1, appendATMap-INV, % 37.95/5.84 appendAnsMap-0, appendAnsMap-1, appendAnsMap-INV, checkBinOp-0, checkBinOp-1, % 37.95/5.84 checkBinOp-2, checkBinOp-3, checkBinOp-4, checkBinOp-5, checkBinOp-6, % 37.95/5.84 checkBinOp-7, checkBinOp-8, checkBinOp-9, checkBinOp-INV, checkUnOp-0, % 37.95/5.84 checkUnOp-1, checkUnOp-INV, divide-0, divide-1, divide-INV, dom-ATList, % 37.95/5.84 dom-ATMap, dom-AType, dom-AnsMap, dom-Aval, dom-BinOpT, dom-Entry, dom-Exp, % 37.95/5.84 dom-MapConf, dom-OptAType, dom-OptAval, dom-OptExp, dom-OptMapConf, % 37.95/5.84 dom-OptQConf, dom-OptQuestion, dom-QConf, dom-QMap, dom-Questionnaire, % 37.95/5.84 dom-UnOpT, dom-YN, dom-nat, dom-string, echeck-0, echeck-1, echeck-2, echeck-3, % 37.95/5.84 echeck-4, echeck-5, echeck-6, echeck-7, echeck-INV, evalBinOp-1, evalBinOp-10, % 37.95/5.84 evalBinOp-2, evalBinOp-3, evalBinOp-4, evalBinOp-5, evalBinOp-6, evalBinOp-7, % 37.95/5.84 evalBinOp-8, evalBinOp-9, evalBinOp-INV, evalUnOp-0, evalUnOp-1, evalUnOp-INV, % 37.95/5.84 expIsValue-0, expIsValue-1, expIsValue-false-INV, expIsValue-true-INV, getAM-0, % 37.95/5.84 getAM-INV, getAType-0, getAnswer-0, getAnswer-1, getAnswer-2, getAnswer-INV, % 37.95/5.84 getAval-0, getExp-0, getExpValue-0, getMapConf-0, getQC-0, getQM-0, getQM-INV, % 37.95/5.84 getQuest-0, getQuest-INV, getQuestionAType-0, getQuestionLabel-0, % 37.95/5.84 getQuestionQID-0, gt-0, gt-1, gt-2, gt-INV, intersectATM-0, intersectATM-1, % 37.95/5.84 intersectATM-2, intersectATM-INV, isSomeAType-0, isSomeAType-1, % 37.95/5.84 isSomeAType-false-INV, isSomeAType-true-INV, isSomeAval-0, isSomeAval-1, % 37.95/5.84 isSomeAval-false-INV, isSomeAval-true-INV, isSomeExp-0, isSomeExp-1, % 37.95/5.84 isSomeExp-false-INV, isSomeExp-true-INV, isSomeMapConf-0, isSomeMapConf-1, % 37.95/5.84 isSomeMapConf-false-INV, isSomeMapConf-true-INV, isSomeQC-0, isSomeQC-1, % 37.95/5.84 isSomeQC-false-INV, isSomeQC-true-INV, isSomeQuestion-0, isSomeQuestion-1, % 37.95/5.84 isSomeQuestion-false-INV, isSomeQuestion-true-INV, isValue-0, isValue-1, % 37.95/5.84 isValue-false-INV, isValue-true-INV, lookupATMap-0, lookupATMap-1, % 37.95/5.84 lookupATMap-2, lookupATMap-INV, lookupAnsMap-0, lookupAnsMap-1, lookupAnsMap-2, % 37.95/5.84 lookupAnsMap-INV, lookupQMap-0, lookupQMap-1, lookupQMap-2, lookupQMap-INV, % 37.95/5.84 lt-0, lt-1, lt-2, lt-INV, minus-0, minus-1, minus-INV, multiply-0, multiply-1, % 37.95/5.84 multiply-INV, not-0, not-1, not-INV, or-0, or-1, or-INV, plus-0, plus-1, % 37.95/5.84 plus-INV, pred-0, pred-1, pred-INV, qcappend-0, qcappend-INV, reduce-0, % 37.95/5.84 reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, % 37.95/5.84 reduce-2, reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, reduce-8, reduce-9, % 37.95/5.84 reduce-INV, reduceExp-0, reduceExp-1, reduceExp-10, reduceExp-2, reduceExp-3, % 37.95/5.84 reduceExp-4, reduceExp-5, reduceExp-6, reduceExp-7, reduceExp-8, reduceExp-9, % 37.95/5.84 reduceExp-INV, typeAM-0, typeAM-1, typeAM-INV, typeOf-0, typeOf-1, typeOf-2, % 37.95/5.84 typeOf-INV, typeQM-0, typeQM-1, typeQM-INV % 37.95/5.84 % 37.95/5.84 Those formulas are unsatisfiable: % 37.95/5.84 --------------------------------- % 37.95/5.84 % 37.95/5.84 Begin of proof % 37.95/5.84 | % 37.95/5.84 | ALPHA: (evalBinOp-0) implies: % 37.95/5.85 | (1) ! [v0: vnat] : ! [v1: vnat] : ! [v2: vAval] : ! [v3: vAval] : ! % 37.95/5.85 | [v4: vOptExp] : ( ~ (vevalBinOp(vaddop, v2, v3) = v4) | ~ (vNum(v1) = % 37.95/5.85 | v3) | ~ (vNum(v0) = v2) | ~ vnat(v1) | ~ vnat(v0) | ? [v5: % 37.95/5.85 | vnat] : ? [v6: vAval] : ? [v7: vExp] : (vplus(v0, v1) = v5 & % 37.95/5.85 | vsomeExp(v7) = v4 & vNum(v5) = v6 & vconstant(v6) = v7 & % 37.95/5.85 | vOptExp(v4) & vnat(v5) & vExp(v7) & vAval(v6))) % 37.95/5.85 | % 37.95/5.85 | ALPHA: (evalBinOpProgress-addop-Num-Num) implies: % 37.95/5.85 | (2) ? [v0: vnat] : ? [v1: vnat] : ? [v2: vAval] : ? [v3: vATMap] : ? % 37.95/5.85 | [v4: vAval] : ? [v5: vAType] : ? [v6: vExp] : ? [v7: vExp] : ? [v8: % 37.95/5.85 | vExp] : ? [v9: vOptAType] : ? [v10: vOptExp] : (vecheck(v3, v8) = % 37.95/5.85 | v9 & vevalBinOp(vaddop, v2, v4) = v10 & vNum(v1) = v4 & vNum(v0) = v2 % 37.95/5.85 | & vsomeAType(v5) = v9 & vbinop(v6, vaddop, v7) = v8 & vconstant(v4) = % 37.95/5.85 | v7 & vconstant(v2) = v6 & vAType(v5) & vOptExp(v10) & vnat(v1) & % 37.95/5.85 | vnat(v0) & vExp(v8) & vExp(v7) & vExp(v6) & vAval(v4) & vAval(v2) & % 37.95/5.85 | vATMap(v3) & vOptAType(v9) & ! [v11: vExp] : ( ~ (vsomeExp(v11) = % 37.95/5.85 | v10) | ~ vExp(v11))) % 37.95/5.85 | % 37.95/5.85 | DELTA: instantiating (2) with fresh symbols all_401_0, all_401_1, all_401_2, % 37.95/5.85 | all_401_3, all_401_4, all_401_5, all_401_6, all_401_7, all_401_8, % 37.95/5.85 | all_401_9, all_401_10 gives: % 37.95/5.85 | (3) vecheck(all_401_7, all_401_2) = all_401_1 & vevalBinOp(vaddop, % 37.95/5.85 | all_401_8, all_401_6) = all_401_0 & vNum(all_401_9) = all_401_6 & % 37.95/5.85 | vNum(all_401_10) = all_401_8 & vsomeAType(all_401_5) = all_401_1 & % 37.95/5.85 | vbinop(all_401_4, vaddop, all_401_3) = all_401_2 & vconstant(all_401_6) % 37.95/5.85 | = all_401_3 & vconstant(all_401_8) = all_401_4 & vAType(all_401_5) & % 37.95/5.85 | vOptExp(all_401_0) & vnat(all_401_9) & vnat(all_401_10) & % 37.95/5.85 | vExp(all_401_2) & vExp(all_401_3) & vExp(all_401_4) & vAval(all_401_6) % 37.95/5.85 | & vAval(all_401_8) & vATMap(all_401_7) & vOptAType(all_401_1) & ! [v0: % 37.95/5.85 | vExp] : ( ~ (vsomeExp(v0) = all_401_0) | ~ vExp(v0)) % 37.95/5.85 | % 37.95/5.85 | ALPHA: (3) implies: % 37.95/5.85 | (4) vnat(all_401_10) % 37.95/5.86 | (5) vnat(all_401_9) % 37.95/5.86 | (6) vNum(all_401_10) = all_401_8 % 37.95/5.86 | (7) vNum(all_401_9) = all_401_6 % 37.95/5.86 | (8) vevalBinOp(vaddop, all_401_8, all_401_6) = all_401_0 % 37.95/5.86 | (9) ! [v0: vExp] : ( ~ (vsomeExp(v0) = all_401_0) | ~ vExp(v0)) % 37.95/5.86 | % 37.95/5.86 | GROUND_INST: instantiating (1) with all_401_10, all_401_9, all_401_8, % 37.95/5.86 | all_401_6, all_401_0, simplifying with (4), (5), (6), (7), (8) % 37.95/5.86 | gives: % 37.95/5.86 | (10) ? [v0: vnat] : ? [v1: vAval] : ? [v2: vExp] : (vplus(all_401_10, % 37.95/5.86 | all_401_9) = v0 & vsomeExp(v2) = all_401_0 & vNum(v0) = v1 & % 37.95/5.86 | vconstant(v1) = v2 & vOptExp(all_401_0) & vnat(v0) & vExp(v2) & % 37.95/5.86 | vAval(v1)) % 37.95/5.86 | % 37.95/5.86 | DELTA: instantiating (10) with fresh symbols all_437_0, all_437_1, all_437_2 % 37.95/5.86 | gives: % 37.95/5.86 | (11) vplus(all_401_10, all_401_9) = all_437_2 & vsomeExp(all_437_0) = % 37.95/5.86 | all_401_0 & vNum(all_437_2) = all_437_1 & vconstant(all_437_1) = % 37.95/5.86 | all_437_0 & vOptExp(all_401_0) & vnat(all_437_2) & vExp(all_437_0) & % 37.95/5.86 | vAval(all_437_1) % 37.95/5.86 | % 37.95/5.86 | ALPHA: (11) implies: % 37.95/5.86 | (12) vExp(all_437_0) % 37.95/5.86 | (13) vsomeExp(all_437_0) = all_401_0 % 37.95/5.86 | % 37.95/5.86 | GROUND_INST: instantiating (9) with all_437_0, simplifying with (12), (13) % 37.95/5.86 | gives: % 37.95/5.86 | (14) $false % 37.95/5.86 | % 37.95/5.86 | CLOSE: (14) is inconsistent. % 37.95/5.86 | % 37.95/5.86 End of proof % 37.95/5.86 % SZS output end Proof for theBenchmark % 37.95/5.86 % 37.95/5.86 5260ms %------------------------------------------------------------------------------