%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM256_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 : n017.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:39 PM UTC 2026 % Result : Theorem 29.36s 4.61s % Output : Proof 38.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM256_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.34 % Computer : n017.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:47:57 EDT 2026 % 0.16/0.34 % CPUTime : % 0.51/0.61 ________ _____ % 0.51/0.61 ___ __ \_________(_)________________________________ % 0.51/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.51/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.51/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.51/0.61 % 0.51/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.51/0.61 (2023-06-19) % 0.51/0.61 % 0.51/0.61 (c) Philipp Rümmer, 2009-2023 % 0.51/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.51/0.61 Amanda Stjerna. % 0.51/0.61 Free software under BSD-3-Clause. % 0.51/0.61 % 0.51/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.51/0.61 % 0.51/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.51/0.62 Running up to 7 provers in parallel. % 0.70/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.70/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.70/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.70/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.70/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.70/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.70/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.69/2.09 Prover 1: Preprocessing ... % 10.46/2.13 Prover 6: Preprocessing ... % 10.46/2.13 Prover 2: Preprocessing ... % 10.46/2.13 Prover 5: Preprocessing ... % 10.46/2.15 Prover 3: Preprocessing ... % 10.46/2.15 Prover 0: Preprocessing ... % 10.46/2.15 Prover 4: Preprocessing ... % 23.98/3.98 Prover 1: Warning: ignoring some quantifiers % 25.73/4.19 Prover 1: Constructing countermodel ... % 25.73/4.19 Prover 6: Proving ... % 26.28/4.21 Prover 3: Warning: ignoring some quantifiers % 26.28/4.23 Prover 3: Constructing countermodel ... % 26.28/4.29 Prover 5: Proving ... % 28.58/4.52 Prover 4: Warning: ignoring some quantifiers % 29.36/4.61 Prover 3: proved (3978ms) % 29.36/4.61 % 29.36/4.61 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 29.36/4.61 % 29.36/4.62 Prover 6: stopped % 29.36/4.64 Prover 5: stopped % 29.36/4.65 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.36/4.65 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.36/4.65 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 29.36/4.65 Prover 4: Constructing countermodel ... % 30.86/4.82 Prover 0: Proving ... % 30.86/4.82 Prover 0: stopped % 30.86/4.84 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 31.62/4.97 Prover 2: Proving ... % 31.62/4.97 Prover 2: stopped % 31.62/4.97 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 34.69/5.30 Prover 1: Found proof (size 14) % 34.69/5.30 Prover 1: proved (4674ms) % 34.69/5.30 Prover 4: stopped % 34.69/5.40 Prover 7: Preprocessing ... % 35.40/5.40 Prover 10: Preprocessing ... % 35.40/5.40 Prover 8: Preprocessing ... % 36.14/5.52 Prover 11: Preprocessing ... % 36.14/5.53 Prover 13: Preprocessing ... % 36.90/5.61 Prover 7: stopped % 36.90/5.62 Prover 11: stopped % 36.90/5.63 Prover 10: stopped % 37.50/5.73 Prover 13: stopped % 38.40/5.90 Prover 8: Warning: ignoring some quantifiers % 38.40/5.93 Prover 8: Constructing countermodel ... % 38.40/5.95 Prover 8: stopped % 38.40/5.95 % 38.40/5.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 38.40/5.95 % 38.40/5.95 % SZS output start Proof for theBenchmark % 38.40/5.98 Assumptions after simplification: % 38.40/5.98 --------------------------------- % 38.40/5.98 % 38.40/5.98 (Preservation-qempty) % 38.40/6.03 vQuestionnaire(vqempty) & ? [v0: vATMap] : ? [v1: vQuestionnaire] : ? [v2: % 38.40/6.03 vQMap] : ? [v3: vAnsMap] : ? [v4: vATMap] : ? [v5: vAnsMap] : ? [v6: % 38.40/6.03 vQMap] : ? [v7: vATMap] : ? [v8: vATMap] : ? [v9: vMapConf] : ? [v10: % 38.40/6.03 vMapConf] : ? [v11: vOptQConf] : ? [v12: vQConf] : ? [v13: vATMap] : ? % 38.40/6.03 [v14: vATMap] : ? [v15: vMapConf] : ? [v16: int] : ( ~ (v16 = 0) & % 38.40/6.03 vptcheck(v15, v1, v10) = v16 & vptcheck(v9, vqempty, v10) = 0 & vtypeQM(v6) % 38.40/6.03 = v14 & vtypeQM(v2) = v8 & vtypeAM(v5) = v7 & vtypeAM(v3) = v13 & % 38.40/6.03 vreduce(vqempty, v5, v2) = v11 & vQC(v3, v6, v1) = v12 & vsomeQConf(v12) = % 38.40/6.03 v11 & vMC(v13, v14) = v15 & vMC(v7, v8) = v9 & vMC(v4, v0) = v10 & vQMap(v6) % 38.40/6.03 & vQMap(v2) & vAnsMap(v5) & vAnsMap(v3) & vOptQConf(v11) & vQConf(v12) & % 38.40/6.03 vQuestionnaire(v1) & vATMap(v14) & vATMap(v13) & vATMap(v8) & vATMap(v7) & % 38.40/6.03 vATMap(v4) & vATMap(v0) & vMapConf(v15) & vMapConf(v10) & vMapConf(v9)) % 38.40/6.03 % 38.40/6.03 (isSomeQC-0) % 38.95/6.03 vOptQConf(vnoQConf) & ? [v0: int] : ( ~ (v0 = 0) & visSomeQC(vnoQConf) = v0) % 38.95/6.03 % 38.95/6.03 (isSomeQC-1) % 38.95/6.03 ! [v0: vQConf] : ! [v1: vOptQConf] : ( ~ (vsomeQConf(v0) = v1) | ~ % 38.95/6.03 vQConf(v0) | visSomeQC(v1) = 0) % 38.95/6.03 % 38.95/6.03 (reduce-0) % 38.95/6.03 vOptQConf(vnoQConf) & vQuestionnaire(vqempty) & ! [v0: vAnsMap] : ! [v1: % 38.95/6.03 vQMap] : ! [v2: vOptQConf] : (v2 = vnoQConf | ~ (vreduce(vqempty, v0, v1) % 38.95/6.03 = v2) | ~ vQMap(v1) | ~ vAnsMap(v0)) % 38.95/6.03 % 38.95/6.03 (function-axioms) % 38.95/6.05 ! [v0: vQMap] : ! [v1: vQMap] : ! [v2: vQMap] : ! [v3: vAType] : ! [v4: % 38.95/6.05 vLabel] : ! [v5: vQID] : (v1 = v0 | ~ (vqmbind(v5, v4, v3, v2) = v1) | ~ % 38.95/6.05 (vqmbind(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 38.95/6.05 MultipleValueBool] : ! [v2: vMapConf] : ! [v3: vQuestionnaire] : ! [v4: % 38.95/6.05 vMapConf] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, % 38.95/6.05 v2) = v0)) & ! [v0: vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : % 38.95/6.05 ! [v3: vAType] : ! [v4: vBinOpT] : (v1 = v0 | ~ (vcheckBinOp(v4, v3, v2) = % 38.95/6.05 v1) | ~ (vcheckBinOp(v4, v3, v2) = v0)) & ! [v0: vOptQConf] : ! [v1: % 38.95/6.05 vOptQConf] : ! [v2: vQMap] : ! [v3: vAnsMap] : ! [v4: vQuestionnaire] : % 38.95/6.05 (v1 = v0 | ~ (vreduce(v4, v3, v2) = v1) | ~ (vreduce(v4, v3, v2) = v0)) & ! % 38.95/6.05 [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vAval] : ! [v4: % 38.95/6.05 vBinOpT] : (v1 = v0 | ~ (vevalBinOp(v4, v3, v2) = v1) | ~ (vevalBinOp(v4, % 38.95/6.05 v3, v2) = v0)) & ! [v0: vQConf] : ! [v1: vQConf] : ! [v2: % 38.95/6.05 vQuestionnaire] : ! [v3: vQMap] : ! [v4: vAnsMap] : (v1 = v0 | ~ (vQC(v4, % 38.95/6.05 v3, v2) = v1) | ~ (vQC(v4, v3, v2) = v0)) & ! [v0: vATMap] : ! [v1: % 38.95/6.05 vATMap] : ! [v2: vATMap] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ % 38.95/6.05 (vatmbind(v4, v3, v2) = v1) | ~ (vatmbind(v4, v3, v2) = v0)) & ! [v0: % 38.95/6.05 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vAType] : ! [v3: vLabel] : % 38.95/6.05 ! [v4: vQID] : (v1 = v0 | ~ (vsomeQuestion(v4, v3, v2) = v1) | ~ % 38.95/6.05 (vsomeQuestion(v4, v3, v2) = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! % 38.95/6.05 [v2: vAnsMap] : ! [v3: vAval] : ! [v4: vQID] : (v1 = v0 | ~ (vabind(v4, v3, % 38.95/6.05 v2) = v1) | ~ (vabind(v4, v3, v2) = v0)) & ! [v0: vQuestionnaire] : ! % 38.95/6.05 [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! [v3: vQuestionnaire] : ! % 38.95/6.05 [v4: vExp] : (v1 = v0 | ~ (vqcond(v4, v3, v2) = v1) | ~ (vqcond(v4, v3, v2) % 38.95/6.05 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: vBinOpT] % 38.95/6.05 : ! [v4: vExp] : (v1 = v0 | ~ (vbinop(v4, v3, v2) = v1) | ~ (vbinop(v4, v3, % 38.95/6.05 v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! [v2: vAType] : ! % 38.95/6.05 [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ (vdefquestion(v4, v3, v2) = v1) | % 38.95/6.05 ~ (vdefquestion(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! % 38.95/6.05 [v2: vExp] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ (vvalue(v4, v3, % 38.95/6.05 v2) = v1) | ~ (vvalue(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: % 38.95/6.05 vEntry] : ! [v2: vAType] : ! [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ % 38.95/6.05 (vquestion(v4, v3, v2) = v1) | ~ (vquestion(v4, v3, v2) = v0)) & ! [v0: % 38.95/6.05 vOptAType] : ! [v1: vOptAType] : ! [v2: vExp] : ! [v3: vATMap] : (v1 = v0 % 38.95/6.05 | ~ (vecheck(v3, v2) = v1) | ~ (vecheck(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : ! [v3: vUnOpT] : (v1 = % 38.95/6.05 v0 | ~ (vcheckUnOp(v3, v2) = v1) | ~ (vcheckUnOp(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 38.95/6.05 ~ (vintersectATM(v3, v2) = v1) | ~ (vintersectATM(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 38.95/6.05 ~ (vappendATMap(v3, v2) = v1) | ~ (vappendATMap(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vOptAType] : ! [v1: vOptAType] : ! [v2: vATMap] : ! [v3: vQID] : (v1 = v0 % 38.95/6.05 | ~ (vlookupATMap(v3, v2) = v1) | ~ (vlookupATMap(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vOptExp] : ! [v1: vOptExp] : ! [v2: vAnsMap] : ! [v3: vExp] : (v1 = v0 | % 38.95/6.05 ~ (vreduceExp(v3, v2) = v1) | ~ (vreduceExp(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vUnOpT] : (v1 = v0 | % 38.95/6.05 ~ (vevalUnOp(v3, v2) = v1) | ~ (vevalUnOp(v3, v2) = v0)) & ! [v0: vAval] : % 38.95/6.05 ! [v1: vAval] : ! [v2: vAType] : ! [v3: vLabel] : (v1 = v0 | ~ % 38.95/6.05 (vgetAnswer(v3, v2) = v1) | ~ (vgetAnswer(v3, v2) = v0)) & ! [v0: vQConf] % 38.95/6.05 : ! [v1: vQConf] : ! [v2: vQuestionnaire] : ! [v3: vQConf] : (v1 = v0 | ~ % 38.95/6.05 (vqcappend(v3, v2) = v1) | ~ (vqcappend(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vQMap] : ! [v3: vQID] : (v1 % 38.95/6.05 = v0 | ~ (vlookupQMap(v3, v2) = v1) | ~ (vlookupQMap(v3, v2) = v0)) & ! % 38.95/6.05 [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vAnsMap] : ! [v3: vAnsMap] : (v1 = % 38.95/6.05 v0 | ~ (vappendAnsMap(v3, v2) = v1) | ~ (vappendAnsMap(v3, v2) = v0)) & ! % 38.95/6.05 [v0: vOptAval] : ! [v1: vOptAval] : ! [v2: vAnsMap] : ! [v3: vQID] : (v1 = % 38.95/6.05 v0 | ~ (vlookupAnsMap(v3, v2) = v1) | ~ (vlookupAnsMap(v3, v2) = v0)) & ! % 38.95/6.05 [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vATList] : (v1 = % 38.95/6.05 v0 | ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vnat] % 38.95/6.05 : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vdivide(v3, % 38.95/6.05 v2) = v1) | ~ (vdivide(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : % 38.95/6.05 ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vmultiply(v3, v2) = v1) | ~ % 38.95/6.05 (vmultiply(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : % 38.95/6.05 ! [v3: vnat] : (v1 = v0 | ~ (vminus(v3, v2) = v1) | ~ (vminus(v3, v2) = v0)) % 38.95/6.05 & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | % 38.95/6.05 ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: % 38.95/6.05 vYN] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 38.95/6.05 (vlt(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vnat] : ! [v3: % 38.95/6.05 vnat] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! [v0: % 38.95/6.05 vYN] : ! [v1: vYN] : ! [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vor(v3, % 38.95/6.05 v2) = v1) | ~ (vor(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! % 38.95/6.05 [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vand(v3, v2) = v1) | ~ (vand(v3, % 38.95/6.05 v2) = v0)) & ! [v0: vstring] : ! [v1: vstring] : ! [v2: vstring] : ! % 38.95/6.06 [v3: vchar] : (v1 = v0 | ~ (vscons(v3, v2) = v1) | ~ (vscons(v3, v2) = v0)) % 38.95/6.06 & ! [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vAType] : % 38.95/6.06 (v1 = v0 | ~ (vatcons(v3, v2) = v1) | ~ (vatcons(v3, v2) = v0)) & ! [v0: % 38.95/6.06 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! % 38.95/6.06 [v3: vGID] : (v1 = v0 | ~ (vqgroup(v3, v2) = v1) | ~ (vqgroup(v3, v2) = v0)) % 38.95/6.06 & ! [v0: vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] % 38.95/6.06 : ! [v3: vQuestionnaire] : (v1 = v0 | ~ (vqseq(v3, v2) = v1) | ~ (vqseq(v3, % 38.95/6.06 v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: % 38.95/6.06 vUnOpT] : (v1 = v0 | ~ (vunop(v3, v2) = v1) | ~ (vunop(v3, v2) = v0)) & ! % 38.95/6.06 [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = % 38.95/6.06 v0 | ~ (vMC(v3, v2) = v1) | ~ (vMC(v3, v2) = v0)) & ! [v0: vATMap] : ! % 38.95/6.06 [v1: vATMap] : ! [v2: vQMap] : (v1 = v0 | ~ (vtypeQM(v2) = v1) | ~ % 38.95/6.06 (vtypeQM(v2) = v0)) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vAnsMap] : % 38.95/6.06 (v1 = v0 | ~ (vtypeAM(v2) = v1) | ~ (vtypeAM(v2) = v0)) & ! [v0: % 38.95/6.06 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptMapConf] : (v1 % 38.95/6.06 = v0 | ~ (visSomeMapConf(v2) = v1) | ~ (visSomeMapConf(v2) = v0)) & ! % 38.95/6.06 [v0: vstring] : ! [v1: vstring] : ! [v2: vLabel] : (v1 = v0 | ~ % 38.95/6.06 (vaskText(v2) = v1) | ~ (vaskText(v2) = v0)) & ! [v0: vnat] : ! [v1: % 38.95/6.06 vnat] : ! [v2: vLabel] : (v1 = v0 | ~ (vaskNumber(v2) = v1) | ~ % 38.95/6.06 (vaskNumber(v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vLabel] : (v1 % 38.95/6.06 = v0 | ~ (vaskYesNo(v2) = v1) | ~ (vaskYesNo(v2) = v0)) & ! [v0: % 38.95/6.06 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] : (v1 = v0 | % 38.95/6.06 ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) & ! [v0: % 38.95/6.06 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptExp] : (v1 = % 38.95/6.06 v0 | ~ (visSomeExp(v2) = v1) | ~ (visSomeExp(v2) = v0)) & ! [v0: % 38.95/6.06 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQConf] : (v1 = % 38.95/6.06 v0 | ~ (visSomeQC(v2) = v1) | ~ (visSomeQC(v2) = v0)) & ! [v0: % 38.95/6.06 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuestionnaire] : % 38.95/6.06 (v1 = v0 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 38.95/6.06 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQConf] : (v1 = v0 | ~ % 38.95/6.06 (vgetQuest(v2) = v1) | ~ (vgetQuest(v2) = v0)) & ! [v0: vQMap] : ! [v1: % 38.95/6.06 vQMap] : ! [v2: vQConf] : (v1 = v0 | ~ (vgetQM(v2) = v1) | ~ (vgetQM(v2) % 38.95/6.06 = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vQConf] : (v1 = v0 % 38.95/6.06 | ~ (vgetAM(v2) = v1) | ~ (vgetAM(v2) = v0)) & ! [v0: MultipleValueBool] % 38.95/6.06 : ! [v1: MultipleValueBool] : ! [v2: vOptQuestion] : (v1 = v0 | ~ % 38.95/6.06 (visSomeQuestion(v2) = v1) | ~ (visSomeQuestion(v2) = v0)) & ! [v0: % 38.95/6.06 vAType] : ! [v1: vAType] : ! [v2: vAval] : (v1 = v0 | ~ (vtypeOf(v2) = % 38.95/6.06 v1) | ~ (vtypeOf(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 38.95/6.06 MultipleValueBool] : ! [v2: vOptAType] : (v1 = v0 | ~ (visSomeAType(v2) = % 38.95/6.06 v1) | ~ (visSomeAType(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 38.95/6.06 MultipleValueBool] : ! [v2: vOptAval] : (v1 = v0 | ~ (visSomeAval(v2) = % 38.95/6.06 v1) | ~ (visSomeAval(v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: % 38.95/6.06 vnat] : (v1 = v0 | ~ (vpred(v2) = v1) | ~ (vpred(v2) = v0)) & ! [v0: vYN] % 38.95/6.06 : ! [v1: vYN] : ! [v2: vYN] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) = % 38.95/6.06 v0)) & ! [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vOptMapConf] : (v1 % 38.95/6.06 = v0 | ~ (vgetMapConf(v2) = v1) | ~ (vgetMapConf(v2) = v0)) & ! [v0: % 38.95/6.06 vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ (vgetExpValue(v2) = % 38.95/6.06 v1) | ~ (vgetExpValue(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 38.95/6.06 [v2: vOptExp] : (v1 = v0 | ~ (vgetExp(v2) = v1) | ~ (vgetExp(v2) = v0)) & ! % 38.95/6.06 [v0: vQConf] : ! [v1: vQConf] : ! [v2: vOptQConf] : (v1 = v0 | ~ % 38.95/6.06 (vgetQC(v2) = v1) | ~ (vgetQC(v2) = v0)) & ! [v0: vAType] : ! [v1: % 38.95/6.06 vAType] : ! [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionAType(v2) = v1) % 38.95/6.06 | ~ (vgetQuestionAType(v2) = v0)) & ! [v0: vLabel] : ! [v1: vLabel] : ! % 38.95/6.06 [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionLabel(v2) = v1) | ~ % 38.95/6.06 (vgetQuestionLabel(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: % 38.95/6.06 vOptQuestion] : (v1 = v0 | ~ (vgetQuestionQID(v2) = v1) | ~ % 38.95/6.06 (vgetQuestionQID(v2) = v0)) & ! [v0: vAType] : ! [v1: vAType] : ! [v2: % 38.95/6.06 vOptAType] : (v1 = v0 | ~ (vgetAType(v2) = v1) | ~ (vgetAType(v2) = v0)) & % 38.95/6.06 ! [v0: vAval] : ! [v1: vAval] : ! [v2: vOptAval] : (v1 = v0 | ~ % 38.95/6.06 (vgetAval(v2) = v1) | ~ (vgetAval(v2) = v0)) & ! [v0: vOptAval] : ! [v1: % 38.95/6.06 vOptAval] : ! [v2: vAval] : (v1 = v0 | ~ (vsomeAval(v2) = v1) | ~ % 38.95/6.06 (vsomeAval(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: vQID] : (v1 % 38.95/6.06 = v0 | ~ (venumQID(v2) = v1) | ~ (venumQID(v2) = v0)) & ! [v0: % 38.95/6.06 vOptMapConf] : ! [v1: vOptMapConf] : ! [v2: vMapConf] : (v1 = v0 | ~ % 38.95/6.06 (vsomeMapConf(v2) = v1) | ~ (vsomeMapConf(v2) = v0)) & ! [v0: vGID] : ! % 38.95/6.06 [v1: vGID] : ! [v2: vGID] : (v1 = v0 | ~ (venumGID(v2) = v1) | ~ % 38.95/6.06 (venumGID(v2) = v0)) & ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vExp] : % 38.95/6.06 (v1 = v0 | ~ (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) & ! [v0: vAval] : % 38.95/6.06 ! [v1: vAval] : ! [v2: vstring] : (v1 = v0 | ~ (vT(v2) = v1) | ~ (vT(v2) = % 38.95/6.06 v0)) & ! [v0: vAval] : ! [v1: vAval] : ! [v2: vnat] : (v1 = v0 | ~ % 38.95/6.06 (vNum(v2) = v1) | ~ (vNum(v2) = v0)) & ! [v0: vAval] : ! [v1: vAval] : ! % 38.95/6.06 [v2: vYN] : (v1 = v0 | ~ (vB(v2) = v1) | ~ (vB(v2) = v0)) & ! [v0: % 38.95/6.06 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : (v1 = v0 | ~ % 38.95/6.06 (vsomeAType(v2) = v1) | ~ (vsomeAType(v2) = v0)) & ! [v0: vOptQConf] : ! % 38.95/6.06 [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | ~ (vsomeQConf(v2) = v1) | ~ % 38.95/6.06 (vsomeQConf(v2) = v0)) & ! [v0: vchar] : ! [v1: vchar] : ! [v2: vchar] : % 38.95/6.06 (v1 = v0 | ~ (venumchar(v2) = v1) | ~ (venumchar(v2) = v0)) & ! [v0: % 38.95/6.06 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vEntry] : (v1 = v0 | ~ % 38.95/6.06 (vqsingle(v2) = v1) | ~ (vqsingle(v2) = v0)) & ! [v0: vnat] : ! [v1: % 38.95/6.06 vnat] : ! [v2: vnat] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = % 38.95/6.06 v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vQID] : (v1 = v0 | ~ % 38.95/6.06 (vqvar(v2) = v1) | ~ (vqvar(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 38.95/6.06 [v2: vAval] : (v1 = v0 | ~ (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & % 38.95/6.06 ! [v0: vLabel] : ! [v1: vLabel] : ! [v2: vLabel] : (v1 = v0 | ~ % 38.95/6.06 (venumLabel(v2) = v1) | ~ (venumLabel(v2) = v0)) & ! [v0: vEntry] : ! % 38.95/6.06 [v1: vEntry] : ! [v2: vQID] : (v1 = v0 | ~ (vask(v2) = v1) | ~ (vask(v2) = % 38.95/6.06 v0)) % 38.95/6.06 % 38.95/6.06 Further assumptions not needed in the proof: % 38.95/6.06 -------------------------------------------- % 38.95/6.06 DIFF-B-Num, DIFF-B-T, DIFF-Num-T, DIFF-Number-Text, DIFF-YesNo-Number, % 38.95/6.06 DIFF-YesNo-Text, DIFF-addop-andop, DIFF-addop-divop, DIFF-addop-eqop, % 38.95/6.06 DIFF-addop-gtop, DIFF-addop-ltop, DIFF-addop-mulop, DIFF-addop-orop, % 38.95/6.06 DIFF-addop-subop, DIFF-aempty-abind, DIFF-andop-orop, DIFF-atempty-atcons, % 38.95/6.06 DIFF-atmempty-atmbind, DIFF-binop-unop, DIFF-constant-binop, DIFF-constant-qvar, % 38.95/6.06 DIFF-constant-unop, DIFF-defquestion-ask, DIFF-divop-andop, DIFF-divop-eqop, % 38.95/6.06 DIFF-divop-gtop, DIFF-divop-ltop, DIFF-divop-orop, DIFF-eqop-andop, % 38.95/6.06 DIFF-eqop-gtop, DIFF-eqop-ltop, DIFF-eqop-orop, DIFF-gtop-andop, DIFF-gtop-ltop, % 38.95/6.06 DIFF-gtop-orop, DIFF-initGID-enumGID, DIFF-initLabel-enumLabel, % 38.95/6.06 DIFF-initQID-enumQID, DIFF-initchar-enumchar, DIFF-ltop-andop, DIFF-ltop-orop, % 38.95/6.06 DIFF-mulop-andop, DIFF-mulop-divop, DIFF-mulop-eqop, DIFF-mulop-gtop, % 38.95/6.06 DIFF-mulop-ltop, DIFF-mulop-orop, DIFF-noAType-someAType, DIFF-noAval-someAval, % 38.95/6.06 DIFF-noExp-someExp, DIFF-noMapConf-someMapConf, DIFF-noQConf-someQConf, % 38.95/6.06 DIFF-noQuestion-someQuestion, DIFF-qcond-qgroup, DIFF-qempty-qcond, % 38.95/6.06 DIFF-qempty-qgroup, DIFF-qempty-qseq, DIFF-qempty-qsingle, DIFF-qmempty-qmbind, % 38.95/6.06 DIFF-qseq-qcond, DIFF-qseq-qgroup, DIFF-qsingle-qcond, DIFF-qsingle-qgroup, % 38.95/6.06 DIFF-qsingle-qseq, DIFF-question-ask, DIFF-question-defquestion, % 38.95/6.06 DIFF-question-value, DIFF-qvar-binop, DIFF-qvar-unop, DIFF-sempty-scons, % 38.95/6.06 DIFF-subop-andop, DIFF-subop-divop, DIFF-subop-eqop, DIFF-subop-gtop, % 38.95/6.06 DIFF-subop-ltop, DIFF-subop-mulop, DIFF-subop-orop, DIFF-value-ask, % 38.95/6.06 DIFF-value-defquestion, DIFF-yes-no, DIFF-zero-succ, EQ-B, EQ-MC, EQ-Num, EQ-QC, % 38.95/6.06 EQ-T, EQ-abind, EQ-ask, EQ-atcons, EQ-atmbind, EQ-binop, EQ-constant, % 38.95/6.06 EQ-defquestion, EQ-enumGID, EQ-enumLabel, EQ-enumQID, EQ-enumchar, EQ-qcond, % 38.95/6.06 EQ-qgroup, EQ-qmbind, EQ-qseq, EQ-qsingle, EQ-question, EQ-qvar, EQ-scons, % 38.95/6.06 EQ-someAType, EQ-someAval, EQ-someExp, EQ-someMapConf, EQ-someQConf, % 38.95/6.06 EQ-someQuestion, EQ-succ, EQ-unop, EQ-value, Task, Task_inv1, Task_inv2, % 38.95/6.06 Task_inv3, Task_inv4, Tdefquestion, Tdefquestion_inv1, Tdefquestion_inv2, % 38.95/6.06 Tdefquestion_inv3, Tqcond, Tqcond_inv1, Tqcond_inv2, Tqcond_inv3, Tqcond_inv4, % 38.95/6.06 Tqcond_inv5, Tqcond_inv6, Tqcond_inv7, Tqempty, Tqempty_inv1, Tqempty_inv2, % 38.95/6.06 Tqgroup, Tqgroup_inv, Tqseq, Tqseq_inv1, Tqseq_inv2, Tqseq_inv3, Tqseq_inv4, % 38.95/6.06 Tquestion, Tquestion_inv1, Tquestion_inv2, Tquestion_inv3, Tvalue, Tvalue_inv1, % 38.95/6.06 Tvalue_inv2, Tvalue_inv3, Tvalue_inv4, and-0, and-1, and-INV, append-0, % 38.95/6.06 append-1, append-INV, appendATMap-0, appendATMap-1, appendATMap-INV, % 38.95/6.06 appendAnsMap-0, appendAnsMap-1, appendAnsMap-INV, checkBinOp-0, checkBinOp-1, % 38.95/6.06 checkBinOp-2, checkBinOp-3, checkBinOp-4, checkBinOp-5, checkBinOp-6, % 38.95/6.06 checkBinOp-7, checkBinOp-8, checkBinOp-9, checkBinOp-INV, checkUnOp-0, % 38.95/6.06 checkUnOp-1, checkUnOp-INV, divide-0, divide-1, divide-INV, dom-ATList, % 38.95/6.06 dom-ATMap, dom-AType, dom-AnsMap, dom-Aval, dom-BinOpT, dom-Entry, dom-Exp, % 38.95/6.06 dom-MapConf, dom-OptAType, dom-OptAval, dom-OptExp, dom-OptMapConf, % 38.95/6.06 dom-OptQConf, dom-OptQuestion, dom-QConf, dom-QMap, dom-Questionnaire, % 38.95/6.06 dom-UnOpT, dom-YN, dom-nat, dom-string, echeck-0, echeck-1, echeck-2, echeck-3, % 38.95/6.06 echeck-4, echeck-5, echeck-6, echeck-7, echeck-INV, evalBinOp-0, evalBinOp-1, % 38.95/6.06 evalBinOp-10, evalBinOp-2, evalBinOp-3, evalBinOp-4, evalBinOp-5, evalBinOp-6, % 38.95/6.06 evalBinOp-7, evalBinOp-8, evalBinOp-9, evalBinOp-INV, evalUnOp-0, evalUnOp-1, % 38.95/6.06 evalUnOp-INV, expIsValue-0, expIsValue-1, expIsValue-false-INV, % 38.95/6.06 expIsValue-true-INV, getAM-0, getAM-INV, getAType-0, getAnswer-0, getAnswer-1, % 38.95/6.06 getAnswer-2, getAnswer-INV, getAval-0, getExp-0, getExpValue-0, getMapConf-0, % 38.95/6.06 getQC-0, getQM-0, getQM-INV, getQuest-0, getQuest-INV, getQuestionAType-0, % 38.95/6.06 getQuestionLabel-0, getQuestionQID-0, gt-0, gt-1, gt-2, gt-INV, intersectATM-0, % 38.95/6.06 intersectATM-1, intersectATM-2, intersectATM-INV, isSomeAType-0, isSomeAType-1, % 38.95/6.06 isSomeAType-false-INV, isSomeAType-true-INV, isSomeAval-0, isSomeAval-1, % 38.95/6.06 isSomeAval-false-INV, isSomeAval-true-INV, isSomeExp-0, isSomeExp-1, % 38.95/6.06 isSomeExp-false-INV, isSomeExp-true-INV, isSomeMapConf-0, isSomeMapConf-1, % 38.95/6.06 isSomeMapConf-false-INV, isSomeMapConf-true-INV, isSomeQC-false-INV, % 38.95/6.06 isSomeQC-true-INV, isSomeQuestion-0, isSomeQuestion-1, isSomeQuestion-false-INV, % 38.95/6.06 isSomeQuestion-true-INV, isValue-0, isValue-1, isValue-false-INV, % 38.95/6.06 isValue-true-INV, lookupATMap-0, lookupATMap-1, lookupATMap-2, lookupATMap-INV, % 38.95/6.06 lookupAnsMap-0, lookupAnsMap-1, lookupAnsMap-2, lookupAnsMap-INV, lookupQMap-0, % 38.95/6.06 lookupQMap-1, lookupQMap-2, lookupQMap-INV, lt-0, lt-1, lt-2, lt-INV, minus-0, % 38.95/6.06 minus-1, minus-INV, multiply-0, multiply-1, multiply-INV, not-0, not-1, not-INV, % 38.95/6.06 or-0, or-1, or-INV, plus-0, plus-1, plus-INV, pred-0, pred-1, pred-INV, % 38.95/6.06 qcappend-0, qcappend-INV, reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, % 38.95/6.06 reduce-14, reduce-15, reduce-2, reduce-3, reduce-4, reduce-5, reduce-6, % 38.95/6.06 reduce-7, reduce-8, reduce-9, reduce-INV, reduceExp-0, reduceExp-1, % 38.95/6.06 reduceExp-10, reduceExp-2, reduceExp-3, reduceExp-4, reduceExp-5, reduceExp-6, % 38.95/6.06 reduceExp-7, reduceExp-8, reduceExp-9, reduceExp-INV, typeAM-0, typeAM-1, % 38.95/6.06 typeAM-INV, typeOf-0, typeOf-1, typeOf-2, typeOf-INV, typeQM-0, typeQM-1, % 38.95/6.06 typeQM-INV % 38.95/6.06 % 38.95/6.06 Those formulas are unsatisfiable: % 38.95/6.06 --------------------------------- % 38.95/6.06 % 38.95/6.06 Begin of proof % 38.95/6.06 | % 38.95/6.06 | ALPHA: (isSomeQC-0) implies: % 38.95/6.06 | (1) ? [v0: int] : ( ~ (v0 = 0) & visSomeQC(vnoQConf) = v0) % 38.95/6.06 | % 38.95/6.06 | ALPHA: (reduce-0) implies: % 38.95/6.06 | (2) ! [v0: vAnsMap] : ! [v1: vQMap] : ! [v2: vOptQConf] : (v2 = vnoQConf % 38.95/6.06 | | ~ (vreduce(vqempty, v0, v1) = v2) | ~ vQMap(v1) | ~ vAnsMap(v0)) % 38.95/6.06 | % 38.95/6.06 | ALPHA: (Preservation-qempty) implies: % 38.95/6.06 | (3) ? [v0: vATMap] : ? [v1: vQuestionnaire] : ? [v2: vQMap] : ? [v3: % 38.95/6.06 | vAnsMap] : ? [v4: vATMap] : ? [v5: vAnsMap] : ? [v6: vQMap] : ? % 38.95/6.06 | [v7: vATMap] : ? [v8: vATMap] : ? [v9: vMapConf] : ? [v10: vMapConf] % 38.95/6.06 | : ? [v11: vOptQConf] : ? [v12: vQConf] : ? [v13: vATMap] : ? [v14: % 38.95/6.06 | vATMap] : ? [v15: vMapConf] : ? [v16: int] : ( ~ (v16 = 0) & % 38.95/6.06 | vptcheck(v15, v1, v10) = v16 & vptcheck(v9, vqempty, v10) = 0 & % 38.95/6.06 | vtypeQM(v6) = v14 & vtypeQM(v2) = v8 & vtypeAM(v5) = v7 & vtypeAM(v3) % 38.95/6.06 | = v13 & vreduce(vqempty, v5, v2) = v11 & vQC(v3, v6, v1) = v12 & % 38.95/6.06 | vsomeQConf(v12) = v11 & vMC(v13, v14) = v15 & vMC(v7, v8) = v9 & % 38.95/6.06 | vMC(v4, v0) = v10 & vQMap(v6) & vQMap(v2) & vAnsMap(v5) & vAnsMap(v3) % 38.95/6.06 | & vOptQConf(v11) & vQConf(v12) & vQuestionnaire(v1) & vATMap(v14) & % 38.95/6.06 | vATMap(v13) & vATMap(v8) & vATMap(v7) & vATMap(v4) & vATMap(v0) & % 38.95/6.06 | vMapConf(v15) & vMapConf(v10) & vMapConf(v9)) % 38.95/6.06 | % 38.95/6.06 | ALPHA: (function-axioms) implies: % 38.95/6.06 | (4) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 38.95/6.06 | vOptQConf] : (v1 = v0 | ~ (visSomeQC(v2) = v1) | ~ (visSomeQC(v2) = % 38.95/6.06 | v0)) % 38.95/6.07 | % 38.95/6.07 | DELTA: instantiating (1) with fresh symbol all_320_0 gives: % 38.95/6.07 | (5) ~ (all_320_0 = 0) & visSomeQC(vnoQConf) = all_320_0 % 38.95/6.07 | % 38.95/6.07 | ALPHA: (5) implies: % 38.95/6.07 | (6) ~ (all_320_0 = 0) % 38.95/6.07 | (7) visSomeQC(vnoQConf) = all_320_0 % 38.95/6.07 | % 38.95/6.07 | DELTA: instantiating (3) with fresh symbols all_404_0, all_404_1, all_404_2, % 38.95/6.07 | all_404_3, all_404_4, all_404_5, all_404_6, all_404_7, all_404_8, % 38.95/6.07 | all_404_9, all_404_10, all_404_11, all_404_12, all_404_13, all_404_14, % 38.95/6.07 | all_404_15, all_404_16 gives: % 38.95/6.07 | (8) ~ (all_404_0 = 0) & vptcheck(all_404_1, all_404_15, all_404_6) = % 38.95/6.07 | all_404_0 & vptcheck(all_404_7, vqempty, all_404_6) = 0 & % 38.95/6.07 | vtypeQM(all_404_10) = all_404_2 & vtypeQM(all_404_14) = all_404_8 & % 38.95/6.07 | vtypeAM(all_404_11) = all_404_9 & vtypeAM(all_404_13) = all_404_3 & % 38.95/6.07 | vreduce(vqempty, all_404_11, all_404_14) = all_404_5 & vQC(all_404_13, % 38.95/6.07 | all_404_10, all_404_15) = all_404_4 & vsomeQConf(all_404_4) = % 38.95/6.07 | all_404_5 & vMC(all_404_3, all_404_2) = all_404_1 & vMC(all_404_9, % 38.95/6.07 | all_404_8) = all_404_7 & vMC(all_404_12, all_404_16) = all_404_6 & % 38.95/6.07 | vQMap(all_404_10) & vQMap(all_404_14) & vAnsMap(all_404_11) & % 38.95/6.07 | vAnsMap(all_404_13) & vOptQConf(all_404_5) & vQConf(all_404_4) & % 38.95/6.07 | vQuestionnaire(all_404_15) & vATMap(all_404_2) & vATMap(all_404_3) & % 38.95/6.07 | vATMap(all_404_8) & vATMap(all_404_9) & vATMap(all_404_12) & % 38.95/6.07 | vATMap(all_404_16) & vMapConf(all_404_1) & vMapConf(all_404_6) & % 38.95/6.07 | vMapConf(all_404_7) % 38.95/6.07 | % 38.95/6.07 | ALPHA: (8) implies: % 38.95/6.07 | (9) vQConf(all_404_4) % 38.95/6.07 | (10) vAnsMap(all_404_11) % 38.95/6.07 | (11) vQMap(all_404_14) % 38.95/6.07 | (12) vsomeQConf(all_404_4) = all_404_5 % 38.95/6.07 | (13) vreduce(vqempty, all_404_11, all_404_14) = all_404_5 % 38.95/6.07 | % 38.95/6.07 | GROUND_INST: instantiating (isSomeQC-1) with all_404_4, all_404_5, simplifying % 38.95/6.07 | with (9), (12) gives: % 38.95/6.07 | (14) visSomeQC(all_404_5) = 0 % 38.95/6.07 | % 38.95/6.07 | GROUND_INST: instantiating (2) with all_404_11, all_404_14, all_404_5, % 38.95/6.07 | simplifying with (10), (11), (13) gives: % 38.95/6.07 | (15) all_404_5 = vnoQConf % 38.95/6.07 | % 38.95/6.07 | REDUCE: (14), (15) imply: % 38.95/6.07 | (16) visSomeQC(vnoQConf) = 0 % 38.95/6.07 | % 38.95/6.07 | GROUND_INST: instantiating (4) with all_320_0, 0, vnoQConf, simplifying with % 38.95/6.07 | (7), (16) gives: % 38.95/6.07 | (17) all_320_0 = 0 % 38.95/6.07 | % 38.95/6.07 | REDUCE: (6), (17) imply: % 38.95/6.07 | (18) $false % 38.95/6.07 | % 38.95/6.07 | CLOSE: (18) is inconsistent. % 38.95/6.07 | % 38.95/6.07 End of proof % 38.95/6.07 % SZS output end Proof for theBenchmark % 38.95/6.07 % 38.95/6.07 5466ms %------------------------------------------------------------------------------