%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM258_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 : n009.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 30.58s 4.79s % Output : Proof 42.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM258_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.33 % Computer : n009.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Mon May 4 19:51:55 EDT 2026 % 0.15/0.34 % CPUTime : % 0.50/0.60 ________ _____ % 0.50/0.60 ___ __ \_________(_)________________________________ % 0.50/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.50/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.50/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.50/0.60 % 0.50/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.50/0.60 (2023-06-19) % 0.50/0.60 % 0.50/0.60 (c) Philipp Rümmer, 2009-2023 % 0.50/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.50/0.60 Amanda Stjerna. % 0.50/0.60 Free software under BSD-3-Clause. % 0.50/0.60 % 0.50/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.50/0.60 % 0.50/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.50/0.61 Running up to 7 provers in parallel. % 0.71/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.71/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.71/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.71/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.71/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.71/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.71/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.96/2.03 Prover 4: Preprocessing ... % 9.96/2.03 Prover 1: Preprocessing ... % 9.96/2.05 Prover 0: Preprocessing ... % 9.96/2.05 Prover 2: Preprocessing ... % 9.96/2.05 Prover 3: Preprocessing ... % 9.96/2.05 Prover 5: Preprocessing ... % 9.96/2.05 Prover 6: Preprocessing ... % 24.45/3.91 Prover 1: Warning: ignoring some quantifiers % 24.45/3.97 Prover 3: Warning: ignoring some quantifiers % 25.29/4.04 Prover 1: Constructing countermodel ... % 25.29/4.05 Prover 3: Constructing countermodel ... % 25.29/4.11 Prover 6: Proving ... % 26.70/4.23 Prover 5: Proving ... % 29.05/4.56 Prover 4: Warning: ignoring some quantifiers % 29.83/4.65 Prover 4: Constructing countermodel ... % 29.83/4.68 Prover 0: Proving ... % 30.58/4.78 Prover 3: proved (4159ms) % 30.58/4.78 % 30.58/4.79 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.58/4.79 % 30.58/4.79 Prover 5: stopped % 30.58/4.79 Prover 6: stopped % 30.58/4.79 Prover 0: stopped % 31.35/4.80 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 31.35/4.80 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 31.35/4.80 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 31.35/4.81 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 33.77/5.12 Prover 2: Proving ... % 33.77/5.12 Prover 2: stopped % 33.77/5.12 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 36.72/5.52 Prover 11: Preprocessing ... % 36.72/5.54 Prover 7: Preprocessing ... % 36.72/5.59 Prover 10: Preprocessing ... % 36.72/5.60 Prover 8: Preprocessing ... % 37.53/5.68 Prover 1: Found proof (size 78) % 37.53/5.68 Prover 1: proved (5061ms) % 37.53/5.68 Prover 4: stopped % 37.53/5.69 Prover 13: Preprocessing ... % 39.89/5.91 Prover 7: stopped % 39.89/5.91 Prover 10: stopped % 39.89/5.92 Prover 11: stopped % 40.53/6.02 Prover 13: stopped % 40.95/6.18 Prover 8: Warning: ignoring some quantifiers % 41.31/6.22 Prover 8: Constructing countermodel ... % 41.31/6.23 Prover 8: stopped % 41.31/6.23 % 41.31/6.23 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.31/6.23 % 41.31/6.27 % SZS output start Proof for theBenchmark % 41.31/6.29 Assumptions after simplification: % 41.31/6.29 --------------------------------- % 41.31/6.29 % 41.31/6.29 (EQ-someQConf) % 41.74/6.33 ! [v0: vQConf] : ! [v1: vQConf] : ! [v2: vOptQConf] : (v1 = v0 | ~ % 41.74/6.34 (vsomeQConf(v1) = v2) | ~ (vsomeQConf(v0) = v2) | ~ vQConf(v1) | ~ % 41.74/6.34 vQConf(v0)) % 41.74/6.34 % 41.74/6.34 (Preservation-qseq-qempty) % 41.74/6.34 vQuestionnaire(vq2) & vQuestionnaire(vq1) & vQuestionnaire(vqempty) & ? [v0: % 41.74/6.34 vQuestionnaire] : (vqseq(vq1, vq2) = v0 & vQuestionnaire(v0) & ? [v1: % 41.74/6.34 vATMap] : ? [v2: vQuestionnaire] : ? [v3: vQMap] : ? [v4: vAnsMap] : ? % 41.74/6.34 [v5: vATMap] : ? [v6: vAnsMap] : ? [v7: vQMap] : ? [v8: vATMap] : ? [v9: % 41.74/6.34 vATMap] : ? [v10: vMapConf] : ? [v11: vMapConf] : ? [v12: vOptQConf] : % 41.74/6.34 ? [v13: vQConf] : ? [v14: vATMap] : ? [v15: vATMap] : ? [v16: vMapConf] : % 41.74/6.34 ? [v17: int] : (vq1 = vqempty & ~ (v17 = 0) & vptcheck(v16, v2, v11) = v17 % 41.74/6.34 & vptcheck(v10, v0, v11) = 0 & vtypeQM(v7) = v15 & vtypeQM(v3) = v9 & % 41.74/6.34 vtypeAM(v6) = v8 & vtypeAM(v4) = v14 & vreduce(v0, v6, v3) = v12 & vQC(v4, % 41.74/6.34 v7, v2) = v13 & vsomeQConf(v13) = v12 & vMC(v14, v15) = v16 & vMC(v8, % 41.74/6.34 v9) = v10 & vMC(v5, v1) = v11 & vQMap(v7) & vQMap(v3) & vAnsMap(v6) & % 41.74/6.34 vAnsMap(v4) & vOptQConf(v12) & vQConf(v13) & vQuestionnaire(v2) & % 41.74/6.34 vATMap(v15) & vATMap(v14) & vATMap(v9) & vATMap(v8) & vATMap(v5) & % 41.74/6.34 vATMap(v1) & vMapConf(v16) & vMapConf(v11) & vMapConf(v10))) % 41.74/6.34 % 41.74/6.34 (Tqempty_inv1) % 41.74/6.35 vQuestionnaire(vqempty) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vATMap] % 41.74/6.35 : ! [v3: vATMap] : ! [v4: vMapConf] : ! [v5: vMapConf] : (v2 = v0 | ~ % 41.74/6.35 (vptcheck(v4, vqempty, v5) = 0) | ~ (vMC(v2, v3) = v5) | ~ (vMC(v0, v1) = % 41.74/6.35 v4) | ~ vATMap(v3) | ~ vATMap(v2) | ~ vATMap(v1) | ~ vATMap(v0)) % 41.74/6.35 % 41.74/6.35 (Tqempty_inv2) % 41.74/6.35 vQuestionnaire(vqempty) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vATMap] % 41.74/6.35 : ! [v3: vATMap] : ! [v4: vMapConf] : ! [v5: vMapConf] : (v3 = v1 | ~ % 41.74/6.35 (vptcheck(v4, vqempty, v5) = 0) | ~ (vMC(v2, v3) = v5) | ~ (vMC(v0, v1) = % 41.74/6.35 v4) | ~ vATMap(v3) | ~ vATMap(v2) | ~ vATMap(v1) | ~ vATMap(v0)) % 41.74/6.35 % 41.74/6.35 (Tqseq_inv1) % 41.74/6.35 ! [v0: vATMap] : ! [v1: vQuestionnaire] : ! [v2: vATMap] : ! [v3: vATMap] % 41.74/6.35 : ! [v4: vATMap] : ! [v5: vQuestionnaire] : ! [v6: vMapConf] : ! [v7: % 41.74/6.35 vQuestionnaire] : ! [v8: vMapConf] : ( ~ (vptcheck(v6, v7, v8) = 0) | ~ % 41.74/6.35 (vqseq(v1, v5) = v7) | ~ (vMC(v3, v4) = v8) | ~ (vMC(v2, v0) = v6) | ~ % 41.74/6.35 vQuestionnaire(v5) | ~ vQuestionnaire(v1) | ~ vATMap(v4) | ~ vATMap(v3) | % 41.74/6.35 ~ vATMap(v2) | ~ vATMap(v0) | ? [v9: vATMap] : ? [v10: vATMap] : ? % 41.74/6.35 [v11: vMapConf] : (vptcheck(v6, v1, v11) = 0 & vMC(v9, v10) = v11 & % 41.74/6.35 vATMap(v10) & vATMap(v9) & vMapConf(v11))) % 41.74/6.35 % 41.74/6.35 (Tqseq_inv2) % 41.74/6.35 ! [v0: vATMap] : ! [v1: vQuestionnaire] : ! [v2: vATMap] : ! [v3: vATMap] % 41.74/6.35 : ! [v4: vATMap] : ! [v5: vATMap] : ! [v6: vATMap] : ! [v7: % 41.74/6.35 vQuestionnaire] : ! [v8: vMapConf] : ! [v9: vQuestionnaire] : ! [v10: % 41.74/6.35 vMapConf] : ! [v11: vMapConf] : ( ~ (vptcheck(v8, v9, v10) = 0) | ~ % 41.74/6.35 (vptcheck(v8, v1, v11) = 0) | ~ (vqseq(v1, v7) = v9) | ~ (vMC(v5, v3) = % 41.74/6.35 v11) | ~ (vMC(v4, v6) = v10) | ~ (vMC(v2, v0) = v8) | ~ % 41.74/6.35 vQuestionnaire(v7) | ~ vQuestionnaire(v1) | ~ vATMap(v6) | ~ vATMap(v5) | % 41.74/6.35 ~ vATMap(v4) | ~ vATMap(v3) | ~ vATMap(v2) | ~ vATMap(v0) | ? [v12: % 41.74/6.35 vATMap] : ? [v13: vATMap] : ? [v14: vMapConf] : (vptcheck(v11, v7, v14) % 41.74/6.35 = 0 & vMC(v12, v13) = v14 & vATMap(v13) & vATMap(v12) & vMapConf(v14))) % 41.74/6.35 % 41.74/6.35 (Tqseq_inv3) % 41.74/6.35 ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vQuestionnaire] % 41.74/6.35 : ! [v4: vATMap] : ! [v5: vATMap] : ! [v6: vATMap] : ! [v7: vATMap] : ! % 41.74/6.35 [v8: vATMap] : ! [v9: vQuestionnaire] : ! [v10: vMapConf] : ! [v11: % 41.74/6.35 vQuestionnaire] : ! [v12: vMapConf] : ! [v13: vMapConf] : ! [v14: % 41.74/6.35 vMapConf] : (v6 = v1 | ~ (vptcheck(v13, v9, v14) = 0) | ~ (vptcheck(v10, % 41.74/6.35 v11, v12) = 0) | ~ (vqseq(v3, v9) = v11) | ~ (vMC(v7, v5) = v13) | ~ % 41.74/6.35 (vMC(v6, v8) = v12) | ~ (vMC(v4, v0) = v10) | ~ (vMC(v1, v2) = v14) | ~ % 41.74/6.35 vQuestionnaire(v9) | ~ vQuestionnaire(v3) | ~ vATMap(v8) | ~ vATMap(v7) | % 41.74/6.35 ~ vATMap(v6) | ~ vATMap(v5) | ~ vATMap(v4) | ~ vATMap(v2) | ~ % 41.74/6.35 vATMap(v1) | ~ vATMap(v0) | ? [v15: int] : ( ~ (v15 = 0) & vptcheck(v10, % 41.74/6.35 v3, v13) = v15)) % 41.74/6.36 % 41.74/6.36 (Tqseq_inv4) % 41.74/6.36 ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vQuestionnaire] % 41.74/6.36 : ! [v4: vATMap] : ! [v5: vATMap] : ! [v6: vATMap] : ! [v7: vATMap] : ! % 41.74/6.36 [v8: vATMap] : ! [v9: vQuestionnaire] : ! [v10: vMapConf] : ! [v11: % 41.74/6.36 vQuestionnaire] : ! [v12: vMapConf] : ! [v13: vMapConf] : ! [v14: % 41.74/6.36 vMapConf] : (v8 = v2 | ~ (vptcheck(v13, v9, v14) = 0) | ~ (vptcheck(v10, % 41.74/6.36 v11, v12) = 0) | ~ (vqseq(v3, v9) = v11) | ~ (vMC(v7, v5) = v13) | ~ % 41.74/6.36 (vMC(v6, v8) = v12) | ~ (vMC(v4, v0) = v10) | ~ (vMC(v1, v2) = v14) | ~ % 41.74/6.36 vQuestionnaire(v9) | ~ vQuestionnaire(v3) | ~ vATMap(v8) | ~ vATMap(v7) | % 41.74/6.36 ~ vATMap(v6) | ~ vATMap(v5) | ~ vATMap(v4) | ~ vATMap(v2) | ~ % 41.74/6.36 vATMap(v1) | ~ vATMap(v0) | ? [v15: int] : ( ~ (v15 = 0) & vptcheck(v10, % 41.74/6.36 v3, v13) = v15)) % 41.74/6.36 % 41.74/6.36 (getAM-0) % 41.74/6.36 ! [v0: vAnsMap] : ! [v1: vQMap] : ! [v2: vQuestionnaire] : ! [v3: vQConf] % 41.74/6.36 : ( ~ (vQC(v0, v1, v2) = v3) | ~ vQMap(v1) | ~ vAnsMap(v0) | ~ % 41.74/6.36 vQuestionnaire(v2) | vgetAM(v3) = v0) % 41.74/6.36 % 41.74/6.36 (getQM-0) % 41.74/6.36 ! [v0: vAnsMap] : ! [v1: vQMap] : ! [v2: vQuestionnaire] : ! [v3: vQConf] % 41.74/6.36 : ( ~ (vQC(v0, v1, v2) = v3) | ~ vQMap(v1) | ~ vAnsMap(v0) | ~ % 41.74/6.36 vQuestionnaire(v2) | vgetQM(v3) = v1) % 41.74/6.36 % 41.74/6.36 (getQuest-0) % 41.74/6.36 ! [v0: vAnsMap] : ! [v1: vQMap] : ! [v2: vQuestionnaire] : ! [v3: vQConf] % 41.74/6.36 : ( ~ (vQC(v0, v1, v2) = v3) | ~ vQMap(v1) | ~ vAnsMap(v0) | ~ % 41.74/6.36 vQuestionnaire(v2) | vgetQuest(v3) = v2) % 41.74/6.36 % 41.74/6.36 (getQuest-INV) % 41.74/6.36 ! [v0: vQConf] : ! [v1: vQuestionnaire] : ( ~ (vgetQuest(v0) = v1) | ~ % 41.74/6.36 vQConf(v0) | ? [v2: vAnsMap] : ? [v3: vQMap] : (vQC(v2, v3, v1) = v0 & % 41.74/6.36 vQMap(v3) & vAnsMap(v2) & vQuestionnaire(v1))) % 41.74/6.36 % 41.74/6.36 (reduce-8) % 41.74/6.36 vQuestionnaire(vqempty) & ! [v0: vQuestionnaire] : ! [v1: vAnsMap] : ! [v2: % 41.74/6.36 vQMap] : ! [v3: vQuestionnaire] : ! [v4: vOptQConf] : ( ~ (vreduce(v3, v1, % 41.74/6.36 v2) = v4) | ~ (vqseq(vqempty, v0) = v3) | ~ vQMap(v2) | ~ vAnsMap(v1) % 41.74/6.36 | ~ vQuestionnaire(v0) | ? [v5: vQConf] : (vQC(v1, v2, v0) = v5 & % 41.74/6.36 vsomeQConf(v5) = v4 & vOptQConf(v4) & vQConf(v5))) % 41.74/6.36 % 41.74/6.36 (function-axioms) % 41.74/6.39 ! [v0: vQMap] : ! [v1: vQMap] : ! [v2: vQMap] : ! [v3: vAType] : ! [v4: % 41.74/6.39 vLabel] : ! [v5: vQID] : (v1 = v0 | ~ (vqmbind(v5, v4, v3, v2) = v1) | ~ % 41.74/6.39 (vqmbind(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.74/6.39 MultipleValueBool] : ! [v2: vMapConf] : ! [v3: vQuestionnaire] : ! [v4: % 41.74/6.39 vMapConf] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, % 41.74/6.39 v2) = v0)) & ! [v0: vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : % 41.74/6.39 ! [v3: vAType] : ! [v4: vBinOpT] : (v1 = v0 | ~ (vcheckBinOp(v4, v3, v2) = % 41.74/6.39 v1) | ~ (vcheckBinOp(v4, v3, v2) = v0)) & ! [v0: vOptQConf] : ! [v1: % 41.74/6.39 vOptQConf] : ! [v2: vQMap] : ! [v3: vAnsMap] : ! [v4: vQuestionnaire] : % 41.74/6.39 (v1 = v0 | ~ (vreduce(v4, v3, v2) = v1) | ~ (vreduce(v4, v3, v2) = v0)) & ! % 41.74/6.39 [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vAval] : ! [v4: % 41.74/6.39 vBinOpT] : (v1 = v0 | ~ (vevalBinOp(v4, v3, v2) = v1) | ~ (vevalBinOp(v4, % 41.74/6.39 v3, v2) = v0)) & ! [v0: vQConf] : ! [v1: vQConf] : ! [v2: % 41.74/6.39 vQuestionnaire] : ! [v3: vQMap] : ! [v4: vAnsMap] : (v1 = v0 | ~ (vQC(v4, % 41.74/6.39 v3, v2) = v1) | ~ (vQC(v4, v3, v2) = v0)) & ! [v0: vATMap] : ! [v1: % 41.74/6.39 vATMap] : ! [v2: vATMap] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ % 41.74/6.39 (vatmbind(v4, v3, v2) = v1) | ~ (vatmbind(v4, v3, v2) = v0)) & ! [v0: % 41.74/6.39 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vAType] : ! [v3: vLabel] : % 41.74/6.39 ! [v4: vQID] : (v1 = v0 | ~ (vsomeQuestion(v4, v3, v2) = v1) | ~ % 41.74/6.39 (vsomeQuestion(v4, v3, v2) = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! % 41.74/6.39 [v2: vAnsMap] : ! [v3: vAval] : ! [v4: vQID] : (v1 = v0 | ~ (vabind(v4, v3, % 41.74/6.39 v2) = v1) | ~ (vabind(v4, v3, v2) = v0)) & ! [v0: vQuestionnaire] : ! % 41.74/6.39 [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! [v3: vQuestionnaire] : ! % 41.74/6.39 [v4: vExp] : (v1 = v0 | ~ (vqcond(v4, v3, v2) = v1) | ~ (vqcond(v4, v3, v2) % 41.74/6.39 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: vBinOpT] % 41.74/6.39 : ! [v4: vExp] : (v1 = v0 | ~ (vbinop(v4, v3, v2) = v1) | ~ (vbinop(v4, v3, % 41.74/6.39 v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! [v2: vAType] : ! % 41.74/6.39 [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ (vdefquestion(v4, v3, v2) = v1) | % 41.74/6.39 ~ (vdefquestion(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! % 41.74/6.39 [v2: vExp] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ (vvalue(v4, v3, % 41.74/6.39 v2) = v1) | ~ (vvalue(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: % 41.74/6.39 vEntry] : ! [v2: vAType] : ! [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ % 41.74/6.39 (vquestion(v4, v3, v2) = v1) | ~ (vquestion(v4, v3, v2) = v0)) & ! [v0: % 41.74/6.39 vOptAType] : ! [v1: vOptAType] : ! [v2: vExp] : ! [v3: vATMap] : (v1 = v0 % 41.74/6.39 | ~ (vecheck(v3, v2) = v1) | ~ (vecheck(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : ! [v3: vUnOpT] : (v1 = % 41.74/6.39 v0 | ~ (vcheckUnOp(v3, v2) = v1) | ~ (vcheckUnOp(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 41.74/6.39 ~ (vintersectATM(v3, v2) = v1) | ~ (vintersectATM(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 41.74/6.39 ~ (vappendATMap(v3, v2) = v1) | ~ (vappendATMap(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vOptAType] : ! [v1: vOptAType] : ! [v2: vATMap] : ! [v3: vQID] : (v1 = v0 % 41.74/6.39 | ~ (vlookupATMap(v3, v2) = v1) | ~ (vlookupATMap(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vOptExp] : ! [v1: vOptExp] : ! [v2: vAnsMap] : ! [v3: vExp] : (v1 = v0 | % 41.74/6.39 ~ (vreduceExp(v3, v2) = v1) | ~ (vreduceExp(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vUnOpT] : (v1 = v0 | % 41.74/6.39 ~ (vevalUnOp(v3, v2) = v1) | ~ (vevalUnOp(v3, v2) = v0)) & ! [v0: vAval] : % 41.74/6.39 ! [v1: vAval] : ! [v2: vAType] : ! [v3: vLabel] : (v1 = v0 | ~ % 41.74/6.39 (vgetAnswer(v3, v2) = v1) | ~ (vgetAnswer(v3, v2) = v0)) & ! [v0: vQConf] % 41.74/6.39 : ! [v1: vQConf] : ! [v2: vQuestionnaire] : ! [v3: vQConf] : (v1 = v0 | ~ % 41.74/6.39 (vqcappend(v3, v2) = v1) | ~ (vqcappend(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vQMap] : ! [v3: vQID] : (v1 % 41.74/6.39 = v0 | ~ (vlookupQMap(v3, v2) = v1) | ~ (vlookupQMap(v3, v2) = v0)) & ! % 41.74/6.39 [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vAnsMap] : ! [v3: vAnsMap] : (v1 = % 41.74/6.39 v0 | ~ (vappendAnsMap(v3, v2) = v1) | ~ (vappendAnsMap(v3, v2) = v0)) & ! % 41.74/6.39 [v0: vOptAval] : ! [v1: vOptAval] : ! [v2: vAnsMap] : ! [v3: vQID] : (v1 = % 41.74/6.39 v0 | ~ (vlookupAnsMap(v3, v2) = v1) | ~ (vlookupAnsMap(v3, v2) = v0)) & ! % 41.74/6.39 [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vATList] : (v1 = % 41.74/6.39 v0 | ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vnat] % 41.74/6.39 : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vdivide(v3, % 41.74/6.39 v2) = v1) | ~ (vdivide(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : % 41.74/6.39 ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vmultiply(v3, v2) = v1) | ~ % 41.74/6.39 (vmultiply(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : % 41.74/6.39 ! [v3: vnat] : (v1 = v0 | ~ (vminus(v3, v2) = v1) | ~ (vminus(v3, v2) = v0)) % 41.74/6.39 & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | % 41.74/6.39 ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: % 41.74/6.39 vYN] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 41.74/6.39 (vlt(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vnat] : ! [v3: % 41.74/6.39 vnat] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vYN] : ! [v1: vYN] : ! [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vor(v3, % 41.74/6.39 v2) = v1) | ~ (vor(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! % 41.74/6.39 [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vand(v3, v2) = v1) | ~ (vand(v3, % 41.74/6.39 v2) = v0)) & ! [v0: vstring] : ! [v1: vstring] : ! [v2: vstring] : ! % 41.74/6.39 [v3: vchar] : (v1 = v0 | ~ (vscons(v3, v2) = v1) | ~ (vscons(v3, v2) = v0)) % 41.74/6.39 & ! [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vAType] : % 41.74/6.39 (v1 = v0 | ~ (vatcons(v3, v2) = v1) | ~ (vatcons(v3, v2) = v0)) & ! [v0: % 41.74/6.39 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! % 41.74/6.39 [v3: vGID] : (v1 = v0 | ~ (vqgroup(v3, v2) = v1) | ~ (vqgroup(v3, v2) = v0)) % 41.74/6.39 & ! [v0: vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] % 41.74/6.39 : ! [v3: vQuestionnaire] : (v1 = v0 | ~ (vqseq(v3, v2) = v1) | ~ (vqseq(v3, % 41.74/6.39 v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: % 41.74/6.39 vUnOpT] : (v1 = v0 | ~ (vunop(v3, v2) = v1) | ~ (vunop(v3, v2) = v0)) & ! % 41.74/6.39 [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = % 41.74/6.39 v0 | ~ (vMC(v3, v2) = v1) | ~ (vMC(v3, v2) = v0)) & ! [v0: vATMap] : ! % 41.74/6.39 [v1: vATMap] : ! [v2: vQMap] : (v1 = v0 | ~ (vtypeQM(v2) = v1) | ~ % 41.74/6.39 (vtypeQM(v2) = v0)) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vAnsMap] : % 41.74/6.39 (v1 = v0 | ~ (vtypeAM(v2) = v1) | ~ (vtypeAM(v2) = v0)) & ! [v0: % 41.74/6.39 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptMapConf] : (v1 % 41.74/6.39 = v0 | ~ (visSomeMapConf(v2) = v1) | ~ (visSomeMapConf(v2) = v0)) & ! % 41.74/6.39 [v0: vstring] : ! [v1: vstring] : ! [v2: vLabel] : (v1 = v0 | ~ % 41.74/6.39 (vaskText(v2) = v1) | ~ (vaskText(v2) = v0)) & ! [v0: vnat] : ! [v1: % 41.74/6.39 vnat] : ! [v2: vLabel] : (v1 = v0 | ~ (vaskNumber(v2) = v1) | ~ % 41.74/6.39 (vaskNumber(v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vLabel] : (v1 % 41.74/6.39 = v0 | ~ (vaskYesNo(v2) = v1) | ~ (vaskYesNo(v2) = v0)) & ! [v0: % 41.74/6.39 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] : (v1 = v0 | % 41.74/6.39 ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) & ! [v0: % 41.74/6.39 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptExp] : (v1 = % 41.74/6.39 v0 | ~ (visSomeExp(v2) = v1) | ~ (visSomeExp(v2) = v0)) & ! [v0: % 41.74/6.39 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQConf] : (v1 = % 41.74/6.39 v0 | ~ (visSomeQC(v2) = v1) | ~ (visSomeQC(v2) = v0)) & ! [v0: % 41.74/6.39 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuestionnaire] : % 41.74/6.39 (v1 = v0 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 41.74/6.39 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQConf] : (v1 = v0 | ~ % 41.74/6.39 (vgetQuest(v2) = v1) | ~ (vgetQuest(v2) = v0)) & ! [v0: vQMap] : ! [v1: % 41.74/6.39 vQMap] : ! [v2: vQConf] : (v1 = v0 | ~ (vgetQM(v2) = v1) | ~ (vgetQM(v2) % 41.74/6.39 = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vQConf] : (v1 = v0 % 41.74/6.39 | ~ (vgetAM(v2) = v1) | ~ (vgetAM(v2) = v0)) & ! [v0: MultipleValueBool] % 41.74/6.39 : ! [v1: MultipleValueBool] : ! [v2: vOptQuestion] : (v1 = v0 | ~ % 41.74/6.39 (visSomeQuestion(v2) = v1) | ~ (visSomeQuestion(v2) = v0)) & ! [v0: % 41.74/6.39 vAType] : ! [v1: vAType] : ! [v2: vAval] : (v1 = v0 | ~ (vtypeOf(v2) = % 41.74/6.39 v1) | ~ (vtypeOf(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.74/6.39 MultipleValueBool] : ! [v2: vOptAType] : (v1 = v0 | ~ (visSomeAType(v2) = % 41.74/6.39 v1) | ~ (visSomeAType(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 41.74/6.39 MultipleValueBool] : ! [v2: vOptAval] : (v1 = v0 | ~ (visSomeAval(v2) = % 41.74/6.39 v1) | ~ (visSomeAval(v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: % 41.74/6.39 vnat] : (v1 = v0 | ~ (vpred(v2) = v1) | ~ (vpred(v2) = v0)) & ! [v0: vYN] % 41.74/6.39 : ! [v1: vYN] : ! [v2: vYN] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) = % 41.74/6.39 v0)) & ! [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vOptMapConf] : (v1 % 41.74/6.39 = v0 | ~ (vgetMapConf(v2) = v1) | ~ (vgetMapConf(v2) = v0)) & ! [v0: % 41.74/6.39 vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ (vgetExpValue(v2) = % 41.74/6.39 v1) | ~ (vgetExpValue(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 41.74/6.39 [v2: vOptExp] : (v1 = v0 | ~ (vgetExp(v2) = v1) | ~ (vgetExp(v2) = v0)) & ! % 41.74/6.39 [v0: vQConf] : ! [v1: vQConf] : ! [v2: vOptQConf] : (v1 = v0 | ~ % 41.74/6.39 (vgetQC(v2) = v1) | ~ (vgetQC(v2) = v0)) & ! [v0: vAType] : ! [v1: % 41.74/6.39 vAType] : ! [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionAType(v2) = v1) % 41.74/6.39 | ~ (vgetQuestionAType(v2) = v0)) & ! [v0: vLabel] : ! [v1: vLabel] : ! % 41.74/6.39 [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionLabel(v2) = v1) | ~ % 41.74/6.39 (vgetQuestionLabel(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: % 41.74/6.39 vOptQuestion] : (v1 = v0 | ~ (vgetQuestionQID(v2) = v1) | ~ % 41.74/6.39 (vgetQuestionQID(v2) = v0)) & ! [v0: vAType] : ! [v1: vAType] : ! [v2: % 41.74/6.39 vOptAType] : (v1 = v0 | ~ (vgetAType(v2) = v1) | ~ (vgetAType(v2) = v0)) & % 41.74/6.39 ! [v0: vAval] : ! [v1: vAval] : ! [v2: vOptAval] : (v1 = v0 | ~ % 41.74/6.39 (vgetAval(v2) = v1) | ~ (vgetAval(v2) = v0)) & ! [v0: vOptAval] : ! [v1: % 41.74/6.39 vOptAval] : ! [v2: vAval] : (v1 = v0 | ~ (vsomeAval(v2) = v1) | ~ % 41.74/6.39 (vsomeAval(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: vQID] : (v1 % 41.74/6.39 = v0 | ~ (venumQID(v2) = v1) | ~ (venumQID(v2) = v0)) & ! [v0: % 41.74/6.39 vOptMapConf] : ! [v1: vOptMapConf] : ! [v2: vMapConf] : (v1 = v0 | ~ % 41.74/6.39 (vsomeMapConf(v2) = v1) | ~ (vsomeMapConf(v2) = v0)) & ! [v0: vGID] : ! % 41.74/6.39 [v1: vGID] : ! [v2: vGID] : (v1 = v0 | ~ (venumGID(v2) = v1) | ~ % 41.74/6.39 (venumGID(v2) = v0)) & ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vExp] : % 41.74/6.39 (v1 = v0 | ~ (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) & ! [v0: vAval] : % 41.74/6.39 ! [v1: vAval] : ! [v2: vstring] : (v1 = v0 | ~ (vT(v2) = v1) | ~ (vT(v2) = % 41.74/6.39 v0)) & ! [v0: vAval] : ! [v1: vAval] : ! [v2: vnat] : (v1 = v0 | ~ % 41.74/6.39 (vNum(v2) = v1) | ~ (vNum(v2) = v0)) & ! [v0: vAval] : ! [v1: vAval] : ! % 41.74/6.39 [v2: vYN] : (v1 = v0 | ~ (vB(v2) = v1) | ~ (vB(v2) = v0)) & ! [v0: % 41.74/6.39 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : (v1 = v0 | ~ % 41.74/6.39 (vsomeAType(v2) = v1) | ~ (vsomeAType(v2) = v0)) & ! [v0: vOptQConf] : ! % 41.74/6.39 [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | ~ (vsomeQConf(v2) = v1) | ~ % 41.74/6.39 (vsomeQConf(v2) = v0)) & ! [v0: vchar] : ! [v1: vchar] : ! [v2: vchar] : % 41.74/6.39 (v1 = v0 | ~ (venumchar(v2) = v1) | ~ (venumchar(v2) = v0)) & ! [v0: % 41.74/6.39 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vEntry] : (v1 = v0 | ~ % 41.74/6.39 (vqsingle(v2) = v1) | ~ (vqsingle(v2) = v0)) & ! [v0: vnat] : ! [v1: % 41.74/6.39 vnat] : ! [v2: vnat] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = % 41.74/6.39 v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vQID] : (v1 = v0 | ~ % 41.74/6.39 (vqvar(v2) = v1) | ~ (vqvar(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 41.74/6.39 [v2: vAval] : (v1 = v0 | ~ (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & % 41.74/6.39 ! [v0: vLabel] : ! [v1: vLabel] : ! [v2: vLabel] : (v1 = v0 | ~ % 41.74/6.39 (venumLabel(v2) = v1) | ~ (venumLabel(v2) = v0)) & ! [v0: vEntry] : ! % 41.74/6.39 [v1: vEntry] : ! [v2: vQID] : (v1 = v0 | ~ (vask(v2) = v1) | ~ (vask(v2) = % 41.74/6.39 v0)) % 41.74/6.39 % 41.74/6.39 Further assumptions not needed in the proof: % 41.74/6.39 -------------------------------------------- % 41.74/6.39 DIFF-B-Num, DIFF-B-T, DIFF-Num-T, DIFF-Number-Text, DIFF-YesNo-Number, % 41.74/6.39 DIFF-YesNo-Text, DIFF-addop-andop, DIFF-addop-divop, DIFF-addop-eqop, % 41.74/6.39 DIFF-addop-gtop, DIFF-addop-ltop, DIFF-addop-mulop, DIFF-addop-orop, % 41.74/6.39 DIFF-addop-subop, DIFF-aempty-abind, DIFF-andop-orop, DIFF-atempty-atcons, % 41.74/6.39 DIFF-atmempty-atmbind, DIFF-binop-unop, DIFF-constant-binop, DIFF-constant-qvar, % 41.74/6.39 DIFF-constant-unop, DIFF-defquestion-ask, DIFF-divop-andop, DIFF-divop-eqop, % 41.74/6.39 DIFF-divop-gtop, DIFF-divop-ltop, DIFF-divop-orop, DIFF-eqop-andop, % 41.74/6.39 DIFF-eqop-gtop, DIFF-eqop-ltop, DIFF-eqop-orop, DIFF-gtop-andop, DIFF-gtop-ltop, % 41.74/6.39 DIFF-gtop-orop, DIFF-initGID-enumGID, DIFF-initLabel-enumLabel, % 41.74/6.39 DIFF-initQID-enumQID, DIFF-initchar-enumchar, DIFF-ltop-andop, DIFF-ltop-orop, % 41.74/6.39 DIFF-mulop-andop, DIFF-mulop-divop, DIFF-mulop-eqop, DIFF-mulop-gtop, % 41.74/6.39 DIFF-mulop-ltop, DIFF-mulop-orop, DIFF-noAType-someAType, DIFF-noAval-someAval, % 41.74/6.39 DIFF-noExp-someExp, DIFF-noMapConf-someMapConf, DIFF-noQConf-someQConf, % 41.74/6.39 DIFF-noQuestion-someQuestion, DIFF-qcond-qgroup, DIFF-qempty-qcond, % 41.74/6.39 DIFF-qempty-qgroup, DIFF-qempty-qseq, DIFF-qempty-qsingle, DIFF-qmempty-qmbind, % 41.74/6.39 DIFF-qseq-qcond, DIFF-qseq-qgroup, DIFF-qsingle-qcond, DIFF-qsingle-qgroup, % 41.74/6.39 DIFF-qsingle-qseq, DIFF-question-ask, DIFF-question-defquestion, % 41.74/6.39 DIFF-question-value, DIFF-qvar-binop, DIFF-qvar-unop, DIFF-sempty-scons, % 41.74/6.39 DIFF-subop-andop, DIFF-subop-divop, DIFF-subop-eqop, DIFF-subop-gtop, % 41.74/6.39 DIFF-subop-ltop, DIFF-subop-mulop, DIFF-subop-orop, DIFF-value-ask, % 41.74/6.39 DIFF-value-defquestion, DIFF-yes-no, DIFF-zero-succ, EQ-B, EQ-MC, EQ-Num, EQ-QC, % 41.74/6.39 EQ-T, EQ-abind, EQ-ask, EQ-atcons, EQ-atmbind, EQ-binop, EQ-constant, % 41.74/6.39 EQ-defquestion, EQ-enumGID, EQ-enumLabel, EQ-enumQID, EQ-enumchar, EQ-qcond, % 41.74/6.39 EQ-qgroup, EQ-qmbind, EQ-qseq, EQ-qsingle, EQ-question, EQ-qvar, EQ-scons, % 41.74/6.39 EQ-someAType, EQ-someAval, EQ-someExp, EQ-someMapConf, EQ-someQuestion, EQ-succ, % 41.74/6.39 EQ-unop, EQ-value, Preservation-qseq-IH0, Preservation-qseq-IH1, Task, % 41.74/6.39 Task_inv1, Task_inv2, Task_inv3, Task_inv4, Tdefquestion, Tdefquestion_inv1, % 41.74/6.39 Tdefquestion_inv2, Tdefquestion_inv3, Tqcond, Tqcond_inv1, Tqcond_inv2, % 41.74/6.39 Tqcond_inv3, Tqcond_inv4, Tqcond_inv5, Tqcond_inv6, Tqcond_inv7, Tqempty, % 41.74/6.39 Tqgroup, Tqgroup_inv, Tqseq, Tquestion, Tquestion_inv1, Tquestion_inv2, % 41.74/6.39 Tquestion_inv3, Tvalue, Tvalue_inv1, Tvalue_inv2, Tvalue_inv3, Tvalue_inv4, % 41.74/6.39 and-0, and-1, and-INV, append-0, append-1, append-INV, appendATMap-0, % 41.74/6.39 appendATMap-1, appendATMap-INV, appendAnsMap-0, appendAnsMap-1, % 41.74/6.39 appendAnsMap-INV, checkBinOp-0, checkBinOp-1, checkBinOp-2, checkBinOp-3, % 41.74/6.39 checkBinOp-4, checkBinOp-5, checkBinOp-6, checkBinOp-7, checkBinOp-8, % 41.74/6.39 checkBinOp-9, checkBinOp-INV, checkUnOp-0, checkUnOp-1, checkUnOp-INV, divide-0, % 41.74/6.39 divide-1, divide-INV, dom-ATList, dom-ATMap, dom-AType, dom-AnsMap, dom-Aval, % 41.74/6.39 dom-BinOpT, dom-Entry, dom-Exp, dom-MapConf, dom-OptAType, dom-OptAval, % 41.74/6.39 dom-OptExp, dom-OptMapConf, dom-OptQConf, dom-OptQuestion, dom-QConf, dom-QMap, % 41.74/6.39 dom-Questionnaire, dom-UnOpT, dom-YN, dom-nat, dom-string, echeck-0, echeck-1, % 41.74/6.39 echeck-2, echeck-3, echeck-4, echeck-5, echeck-6, echeck-7, echeck-INV, % 41.74/6.39 evalBinOp-0, evalBinOp-1, evalBinOp-10, evalBinOp-2, evalBinOp-3, evalBinOp-4, % 41.74/6.39 evalBinOp-5, evalBinOp-6, evalBinOp-7, evalBinOp-8, evalBinOp-9, evalBinOp-INV, % 41.74/6.39 evalUnOp-0, evalUnOp-1, evalUnOp-INV, expIsValue-0, expIsValue-1, % 41.74/6.39 expIsValue-false-INV, expIsValue-true-INV, getAM-INV, getAType-0, getAnswer-0, % 41.74/6.39 getAnswer-1, getAnswer-2, getAnswer-INV, getAval-0, getExp-0, getExpValue-0, % 41.74/6.39 getMapConf-0, getQC-0, getQM-INV, getQuestionAType-0, getQuestionLabel-0, % 41.74/6.39 getQuestionQID-0, gt-0, gt-1, gt-2, gt-INV, intersectATM-0, intersectATM-1, % 41.74/6.39 intersectATM-2, intersectATM-INV, isSomeAType-0, isSomeAType-1, % 41.74/6.39 isSomeAType-false-INV, isSomeAType-true-INV, isSomeAval-0, isSomeAval-1, % 41.74/6.39 isSomeAval-false-INV, isSomeAval-true-INV, isSomeExp-0, isSomeExp-1, % 41.74/6.39 isSomeExp-false-INV, isSomeExp-true-INV, isSomeMapConf-0, isSomeMapConf-1, % 41.74/6.39 isSomeMapConf-false-INV, isSomeMapConf-true-INV, isSomeQC-0, isSomeQC-1, % 41.74/6.39 isSomeQC-false-INV, isSomeQC-true-INV, isSomeQuestion-0, isSomeQuestion-1, % 41.74/6.39 isSomeQuestion-false-INV, isSomeQuestion-true-INV, isValue-0, isValue-1, % 41.74/6.39 isValue-false-INV, isValue-true-INV, lookupATMap-0, lookupATMap-1, % 41.74/6.39 lookupATMap-2, lookupATMap-INV, lookupAnsMap-0, lookupAnsMap-1, lookupAnsMap-2, % 41.74/6.39 lookupAnsMap-INV, lookupQMap-0, lookupQMap-1, lookupQMap-2, lookupQMap-INV, % 41.74/6.39 lt-0, lt-1, lt-2, lt-INV, minus-0, minus-1, minus-INV, multiply-0, multiply-1, % 41.74/6.39 multiply-INV, not-0, not-1, not-INV, or-0, or-1, or-INV, plus-0, plus-1, % 41.74/6.39 plus-INV, pred-0, pred-1, pred-INV, qcappend-0, qcappend-INV, reduce-0, % 41.74/6.39 reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, % 41.74/6.39 reduce-2, reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, reduce-9, % 41.74/6.39 reduce-INV, reduceExp-0, reduceExp-1, reduceExp-10, reduceExp-2, reduceExp-3, % 41.74/6.39 reduceExp-4, reduceExp-5, reduceExp-6, reduceExp-7, reduceExp-8, reduceExp-9, % 41.74/6.39 reduceExp-INV, typeAM-0, typeAM-1, typeAM-INV, typeOf-0, typeOf-1, typeOf-2, % 41.74/6.39 typeOf-INV, typeQM-0, typeQM-1, typeQM-INV % 41.74/6.39 % 41.74/6.39 Those formulas are unsatisfiable: % 41.74/6.39 --------------------------------- % 41.74/6.39 % 41.74/6.39 Begin of proof % 41.74/6.39 | % 41.74/6.39 | ALPHA: (reduce-8) implies: % 41.74/6.39 | (1) ! [v0: vQuestionnaire] : ! [v1: vAnsMap] : ! [v2: vQMap] : ! [v3: % 41.74/6.39 | vQuestionnaire] : ! [v4: vOptQConf] : ( ~ (vreduce(v3, v1, v2) = v4) % 41.74/6.39 | | ~ (vqseq(vqempty, v0) = v3) | ~ vQMap(v2) | ~ vAnsMap(v1) | ~ % 41.74/6.39 | vQuestionnaire(v0) | ? [v5: vQConf] : (vQC(v1, v2, v0) = v5 & % 41.74/6.39 | vsomeQConf(v5) = v4 & vOptQConf(v4) & vQConf(v5))) % 41.74/6.39 | % 41.74/6.40 | ALPHA: (Tqempty_inv1) implies: % 41.74/6.40 | (2) ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : % 41.74/6.40 | ! [v4: vMapConf] : ! [v5: vMapConf] : (v2 = v0 | ~ (vptcheck(v4, % 41.74/6.40 | vqempty, v5) = 0) | ~ (vMC(v2, v3) = v5) | ~ (vMC(v0, v1) = v4) % 41.74/6.40 | | ~ vATMap(v3) | ~ vATMap(v2) | ~ vATMap(v1) | ~ vATMap(v0)) % 41.74/6.40 | % 41.74/6.40 | ALPHA: (Tqempty_inv2) implies: % 41.74/6.40 | (3) ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : % 41.74/6.40 | ! [v4: vMapConf] : ! [v5: vMapConf] : (v3 = v1 | ~ (vptcheck(v4, % 41.74/6.40 | vqempty, v5) = 0) | ~ (vMC(v2, v3) = v5) | ~ (vMC(v0, v1) = v4) % 41.74/6.40 | | ~ vATMap(v3) | ~ vATMap(v2) | ~ vATMap(v1) | ~ vATMap(v0)) % 41.74/6.40 | % 41.74/6.40 | ALPHA: (Preservation-qseq-qempty) implies: % 42.23/6.40 | (4) vQuestionnaire(vq1) % 42.23/6.40 | (5) vQuestionnaire(vq2) % 42.23/6.40 | (6) ? [v0: vQuestionnaire] : (vqseq(vq1, vq2) = v0 & vQuestionnaire(v0) & % 42.23/6.40 | ? [v1: vATMap] : ? [v2: vQuestionnaire] : ? [v3: vQMap] : ? [v4: % 42.23/6.40 | vAnsMap] : ? [v5: vATMap] : ? [v6: vAnsMap] : ? [v7: vQMap] : ? % 42.23/6.40 | [v8: vATMap] : ? [v9: vATMap] : ? [v10: vMapConf] : ? [v11: % 42.23/6.40 | vMapConf] : ? [v12: vOptQConf] : ? [v13: vQConf] : ? [v14: % 42.23/6.40 | vATMap] : ? [v15: vATMap] : ? [v16: vMapConf] : ? [v17: int] : % 42.23/6.40 | (vq1 = vqempty & ~ (v17 = 0) & vptcheck(v16, v2, v11) = v17 & % 42.23/6.40 | vptcheck(v10, v0, v11) = 0 & vtypeQM(v7) = v15 & vtypeQM(v3) = v9 & % 42.23/6.40 | vtypeAM(v6) = v8 & vtypeAM(v4) = v14 & vreduce(v0, v6, v3) = v12 & % 42.23/6.40 | vQC(v4, v7, v2) = v13 & vsomeQConf(v13) = v12 & vMC(v14, v15) = v16 % 42.23/6.40 | & vMC(v8, v9) = v10 & vMC(v5, v1) = v11 & vQMap(v7) & vQMap(v3) & % 42.23/6.40 | vAnsMap(v6) & vAnsMap(v4) & vOptQConf(v12) & vQConf(v13) & % 42.23/6.40 | vQuestionnaire(v2) & vATMap(v15) & vATMap(v14) & vATMap(v9) & % 42.23/6.40 | vATMap(v8) & vATMap(v5) & vATMap(v1) & vMapConf(v16) & % 42.23/6.40 | vMapConf(v11) & vMapConf(v10))) % 42.23/6.40 | % 42.23/6.40 | ALPHA: (function-axioms) implies: % 42.23/6.40 | (7) ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vQConf] : (v1 = v0 | ~ % 42.23/6.40 | (vgetAM(v2) = v1) | ~ (vgetAM(v2) = v0)) % 42.23/6.40 | (8) ! [v0: vQMap] : ! [v1: vQMap] : ! [v2: vQConf] : (v1 = v0 | ~ % 42.23/6.40 | (vgetQM(v2) = v1) | ~ (vgetQM(v2) = v0)) % 42.23/6.40 | (9) ! [v0: vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQConf] : % 42.23/6.40 | (v1 = v0 | ~ (vgetQuest(v2) = v1) | ~ (vgetQuest(v2) = v0)) % 42.23/6.40 | (10) ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vAnsMap] : (v1 = v0 | ~ % 42.23/6.40 | (vtypeAM(v2) = v1) | ~ (vtypeAM(v2) = v0)) % 42.23/6.40 | (11) ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vQMap] : (v1 = v0 | ~ % 42.23/6.40 | (vtypeQM(v2) = v1) | ~ (vtypeQM(v2) = v0)) % 42.23/6.40 | (12) ! [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vATMap] : ! [v3: % 42.23/6.40 | vATMap] : (v1 = v0 | ~ (vMC(v3, v2) = v1) | ~ (vMC(v3, v2) = v0)) % 42.23/6.40 | (13) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 42.23/6.40 | vMapConf] : ! [v3: vQuestionnaire] : ! [v4: vMapConf] : (v1 = v0 | % 42.23/6.40 | ~ (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, v2) = v0)) % 42.23/6.40 | % 42.23/6.41 | DELTA: instantiating (6) with fresh symbol all_406_0 gives: % 42.23/6.41 | (14) vqseq(vq1, vq2) = all_406_0 & vQuestionnaire(all_406_0) & ? [v0: % 42.23/6.41 | vATMap] : ? [v1: vQuestionnaire] : ? [v2: vQMap] : ? [v3: % 42.23/6.41 | vAnsMap] : ? [v4: vATMap] : ? [v5: vAnsMap] : ? [v6: vQMap] : ? % 42.23/6.41 | [v7: vATMap] : ? [v8: vATMap] : ? [v9: vMapConf] : ? [v10: % 42.23/6.41 | vMapConf] : ? [v11: vOptQConf] : ? [v12: vQConf] : ? [v13: % 42.23/6.41 | vATMap] : ? [v14: vATMap] : ? [v15: vMapConf] : ? [v16: int] : % 42.23/6.41 | (vq1 = vqempty & ~ (v16 = 0) & vptcheck(v15, v1, v10) = v16 & % 42.23/6.41 | vptcheck(v9, all_406_0, v10) = 0 & vtypeQM(v6) = v14 & vtypeQM(v2) = % 42.23/6.41 | v8 & vtypeAM(v5) = v7 & vtypeAM(v3) = v13 & vreduce(all_406_0, v5, % 42.23/6.41 | v2) = v11 & vQC(v3, v6, v1) = v12 & vsomeQConf(v12) = v11 & % 42.23/6.41 | vMC(v13, v14) = v15 & vMC(v7, v8) = v9 & vMC(v4, v0) = v10 & % 42.23/6.41 | vQMap(v6) & vQMap(v2) & vAnsMap(v5) & vAnsMap(v3) & vOptQConf(v11) & % 42.23/6.41 | vQConf(v12) & vQuestionnaire(v1) & vATMap(v14) & vATMap(v13) & % 42.23/6.41 | vATMap(v8) & vATMap(v7) & vATMap(v4) & vATMap(v0) & vMapConf(v15) & % 42.23/6.41 | vMapConf(v10) & vMapConf(v9)) % 42.23/6.41 | % 42.23/6.41 | ALPHA: (14) implies: % 42.23/6.41 | (15) vqseq(vq1, vq2) = all_406_0 % 42.23/6.41 | (16) ? [v0: vATMap] : ? [v1: vQuestionnaire] : ? [v2: vQMap] : ? [v3: % 42.23/6.41 | vAnsMap] : ? [v4: vATMap] : ? [v5: vAnsMap] : ? [v6: vQMap] : ? % 42.23/6.41 | [v7: vATMap] : ? [v8: vATMap] : ? [v9: vMapConf] : ? [v10: % 42.23/6.41 | vMapConf] : ? [v11: vOptQConf] : ? [v12: vQConf] : ? [v13: % 42.23/6.41 | vATMap] : ? [v14: vATMap] : ? [v15: vMapConf] : ? [v16: int] : % 42.23/6.41 | (vq1 = vqempty & ~ (v16 = 0) & vptcheck(v15, v1, v10) = v16 & % 42.23/6.41 | vptcheck(v9, all_406_0, v10) = 0 & vtypeQM(v6) = v14 & vtypeQM(v2) = % 42.23/6.41 | v8 & vtypeAM(v5) = v7 & vtypeAM(v3) = v13 & vreduce(all_406_0, v5, % 42.23/6.41 | v2) = v11 & vQC(v3, v6, v1) = v12 & vsomeQConf(v12) = v11 & % 42.23/6.41 | vMC(v13, v14) = v15 & vMC(v7, v8) = v9 & vMC(v4, v0) = v10 & % 42.23/6.41 | vQMap(v6) & vQMap(v2) & vAnsMap(v5) & vAnsMap(v3) & vOptQConf(v11) & % 42.23/6.41 | vQConf(v12) & vQuestionnaire(v1) & vATMap(v14) & vATMap(v13) & % 42.23/6.41 | vATMap(v8) & vATMap(v7) & vATMap(v4) & vATMap(v0) & vMapConf(v15) & % 42.23/6.41 | vMapConf(v10) & vMapConf(v9)) % 42.23/6.41 | % 42.23/6.41 | DELTA: instantiating (16) with fresh symbols all_420_0, all_420_1, all_420_2, % 42.23/6.41 | all_420_3, all_420_4, all_420_5, all_420_6, all_420_7, all_420_8, % 42.23/6.41 | all_420_9, all_420_10, all_420_11, all_420_12, all_420_13, all_420_14, % 42.23/6.41 | all_420_15, all_420_16 gives: % 42.23/6.41 | (17) vq1 = vqempty & ~ (all_420_0 = 0) & vptcheck(all_420_1, all_420_15, % 42.23/6.41 | all_420_6) = all_420_0 & vptcheck(all_420_7, all_406_0, all_420_6) = % 42.23/6.41 | 0 & vtypeQM(all_420_10) = all_420_2 & vtypeQM(all_420_14) = all_420_8 % 42.23/6.41 | & vtypeAM(all_420_11) = all_420_9 & vtypeAM(all_420_13) = all_420_3 & % 42.23/6.41 | vreduce(all_406_0, all_420_11, all_420_14) = all_420_5 & % 42.23/6.41 | vQC(all_420_13, all_420_10, all_420_15) = all_420_4 & % 42.23/6.41 | vsomeQConf(all_420_4) = all_420_5 & vMC(all_420_3, all_420_2) = % 42.23/6.41 | all_420_1 & vMC(all_420_9, all_420_8) = all_420_7 & vMC(all_420_12, % 42.23/6.41 | all_420_16) = all_420_6 & vQMap(all_420_10) & vQMap(all_420_14) & % 42.23/6.41 | vAnsMap(all_420_11) & vAnsMap(all_420_13) & vOptQConf(all_420_5) & % 42.23/6.41 | vQConf(all_420_4) & vQuestionnaire(all_420_15) & vATMap(all_420_2) & % 42.23/6.41 | vATMap(all_420_3) & vATMap(all_420_8) & vATMap(all_420_9) & % 42.23/6.41 | vATMap(all_420_12) & vATMap(all_420_16) & vMapConf(all_420_1) & % 42.23/6.41 | vMapConf(all_420_6) & vMapConf(all_420_7) % 42.23/6.41 | % 42.23/6.41 | ALPHA: (17) implies: % 42.23/6.41 | (18) vq1 = vqempty % 42.23/6.41 | (19) ~ (all_420_0 = 0) % 42.23/6.41 | (20) vATMap(all_420_16) % 42.23/6.41 | (21) vATMap(all_420_12) % 42.23/6.41 | (22) vATMap(all_420_9) % 42.23/6.41 | (23) vATMap(all_420_8) % 42.23/6.41 | (24) vATMap(all_420_3) % 42.23/6.41 | (25) vATMap(all_420_2) % 42.23/6.41 | (26) vQuestionnaire(all_420_15) % 42.23/6.41 | (27) vQConf(all_420_4) % 42.23/6.41 | (28) vAnsMap(all_420_13) % 42.23/6.41 | (29) vAnsMap(all_420_11) % 42.23/6.41 | (30) vQMap(all_420_14) % 42.23/6.41 | (31) vQMap(all_420_10) % 42.23/6.42 | (32) vMC(all_420_12, all_420_16) = all_420_6 % 42.23/6.42 | (33) vMC(all_420_9, all_420_8) = all_420_7 % 42.23/6.42 | (34) vMC(all_420_3, all_420_2) = all_420_1 % 42.23/6.42 | (35) vsomeQConf(all_420_4) = all_420_5 % 42.23/6.42 | (36) vQC(all_420_13, all_420_10, all_420_15) = all_420_4 % 42.23/6.42 | (37) vreduce(all_406_0, all_420_11, all_420_14) = all_420_5 % 42.23/6.42 | (38) vtypeAM(all_420_13) = all_420_3 % 42.23/6.42 | (39) vtypeAM(all_420_11) = all_420_9 % 42.23/6.42 | (40) vtypeQM(all_420_14) = all_420_8 % 42.23/6.42 | (41) vtypeQM(all_420_10) = all_420_2 % 42.23/6.42 | (42) vptcheck(all_420_7, all_406_0, all_420_6) = 0 % 42.23/6.42 | (43) vptcheck(all_420_1, all_420_15, all_420_6) = all_420_0 % 42.23/6.42 | % 42.23/6.42 | REDUCE: (15), (18) imply: % 42.23/6.42 | (44) vqseq(vqempty, vq2) = all_406_0 % 42.23/6.42 | % 42.23/6.42 | REDUCE: (4), (18) imply: % 42.23/6.42 | (45) vQuestionnaire(vqempty) % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (getQuest-0) with all_420_13, all_420_10, % 42.23/6.42 | all_420_15, all_420_4, simplifying with (26), (28), (31), (36) % 42.23/6.42 | gives: % 42.23/6.42 | (46) vgetQuest(all_420_4) = all_420_15 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (getQM-0) with all_420_13, all_420_10, all_420_15, % 42.23/6.42 | all_420_4, simplifying with (26), (28), (31), (36) gives: % 42.23/6.42 | (47) vgetQM(all_420_4) = all_420_10 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (getAM-0) with all_420_13, all_420_10, all_420_15, % 42.23/6.42 | all_420_4, simplifying with (26), (28), (31), (36) gives: % 42.23/6.42 | (48) vgetAM(all_420_4) = all_420_13 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (1) with vq2, all_420_11, all_420_14, all_406_0, % 42.23/6.42 | all_420_5, simplifying with (5), (29), (30), (37), (44) gives: % 42.23/6.42 | (49) ? [v0: vQConf] : (vQC(all_420_11, all_420_14, vq2) = v0 & % 42.23/6.42 | vsomeQConf(v0) = all_420_5 & vOptQConf(all_420_5) & vQConf(v0)) % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (Tqseq_inv1) with all_420_8, vqempty, all_420_9, % 42.23/6.42 | all_420_12, all_420_16, vq2, all_420_7, all_406_0, all_420_6, % 42.23/6.42 | simplifying with (5), (20), (21), (22), (23), (32), (33), (42), % 42.23/6.42 | (44), (45) gives: % 42.23/6.42 | (50) ? [v0: vATMap] : ? [v1: vATMap] : ? [v2: vMapConf] : % 42.23/6.42 | (vptcheck(all_420_7, vqempty, v2) = 0 & vMC(v0, v1) = v2 & vATMap(v1) % 42.23/6.42 | & vATMap(v0) & vMapConf(v2)) % 42.23/6.42 | % 42.23/6.42 | DELTA: instantiating (49) with fresh symbol all_440_0 gives: % 42.23/6.42 | (51) vQC(all_420_11, all_420_14, vq2) = all_440_0 & vsomeQConf(all_440_0) = % 42.23/6.42 | all_420_5 & vOptQConf(all_420_5) & vQConf(all_440_0) % 42.23/6.42 | % 42.23/6.42 | ALPHA: (51) implies: % 42.23/6.42 | (52) vQConf(all_440_0) % 42.23/6.42 | (53) vsomeQConf(all_440_0) = all_420_5 % 42.23/6.42 | (54) vQC(all_420_11, all_420_14, vq2) = all_440_0 % 42.23/6.42 | % 42.23/6.42 | DELTA: instantiating (50) with fresh symbols all_442_0, all_442_1, all_442_2 % 42.23/6.42 | gives: % 42.23/6.42 | (55) vptcheck(all_420_7, vqempty, all_442_0) = 0 & vMC(all_442_2, % 42.23/6.42 | all_442_1) = all_442_0 & vATMap(all_442_1) & vATMap(all_442_2) & % 42.23/6.42 | vMapConf(all_442_0) % 42.23/6.42 | % 42.23/6.42 | ALPHA: (55) implies: % 42.23/6.42 | (56) vATMap(all_442_2) % 42.23/6.42 | (57) vATMap(all_442_1) % 42.23/6.42 | (58) vMC(all_442_2, all_442_1) = all_442_0 % 42.23/6.42 | (59) vptcheck(all_420_7, vqempty, all_442_0) = 0 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (EQ-someQConf) with all_420_4, all_440_0, % 42.23/6.42 | all_420_5, simplifying with (27), (35), (52), (53) gives: % 42.23/6.42 | (60) all_440_0 = all_420_4 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (getQuest-0) with all_420_11, all_420_14, vq2, % 42.23/6.42 | all_440_0, simplifying with (5), (29), (30), (54) gives: % 42.23/6.42 | (61) vgetQuest(all_440_0) = vq2 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (getQM-0) with all_420_11, all_420_14, vq2, % 42.23/6.42 | all_440_0, simplifying with (5), (29), (30), (54) gives: % 42.23/6.42 | (62) vgetQM(all_440_0) = all_420_14 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (getAM-0) with all_420_11, all_420_14, vq2, % 42.23/6.42 | all_440_0, simplifying with (5), (29), (30), (54) gives: % 42.23/6.42 | (63) vgetAM(all_440_0) = all_420_11 % 42.23/6.42 | % 42.23/6.42 | GROUND_INST: instantiating (getQuest-INV) with all_420_4, all_420_15, % 42.23/6.42 | simplifying with (27), (46) gives: % 42.23/6.43 | (64) ? [v0: vAnsMap] : ? [v1: vQMap] : (vQC(v0, v1, all_420_15) = % 42.23/6.43 | all_420_4 & vQMap(v1) & vAnsMap(v0) & vQuestionnaire(all_420_15)) % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (Tqseq_inv2) with all_420_8, vqempty, all_420_9, % 42.23/6.43 | all_442_1, all_420_12, all_442_2, all_420_16, vq2, all_420_7, % 42.23/6.43 | all_406_0, all_420_6, all_442_0, simplifying with (5), (20), % 42.23/6.43 | (21), (22), (23), (32), (33), (42), (44), (45), (56), (57), (58), % 42.23/6.43 | (59) gives: % 42.23/6.43 | (65) ? [v0: vATMap] : ? [v1: vATMap] : ? [v2: vMapConf] : % 42.23/6.43 | (vptcheck(all_442_0, vq2, v2) = 0 & vMC(v0, v1) = v2 & vATMap(v1) & % 42.23/6.43 | vATMap(v0) & vMapConf(v2)) % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (3) with all_420_9, all_420_8, all_442_2, % 42.23/6.43 | all_442_1, all_420_7, all_442_0, simplifying with (22), (23), % 42.23/6.43 | (33), (56), (57), (58), (59) gives: % 42.23/6.43 | (66) all_442_1 = all_420_8 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (2) with all_420_9, all_420_8, all_442_2, % 42.23/6.43 | all_442_1, all_420_7, all_442_0, simplifying with (22), (23), % 42.23/6.43 | (33), (56), (57), (58), (59) gives: % 42.23/6.43 | (67) all_442_2 = all_420_9 % 42.23/6.43 | % 42.23/6.43 | DELTA: instantiating (64) with fresh symbols all_494_0, all_494_1 gives: % 42.23/6.43 | (68) vQC(all_494_1, all_494_0, all_420_15) = all_420_4 & vQMap(all_494_0) & % 42.23/6.43 | vAnsMap(all_494_1) & vQuestionnaire(all_420_15) % 42.23/6.43 | % 42.23/6.43 | DELTA: instantiating (65) with fresh symbols all_500_0, all_500_1, all_500_2 % 42.23/6.43 | gives: % 42.23/6.43 | (69) vptcheck(all_442_0, vq2, all_500_0) = 0 & vMC(all_500_2, all_500_1) = % 42.23/6.43 | all_500_0 & vATMap(all_500_1) & vATMap(all_500_2) & % 42.23/6.43 | vMapConf(all_500_0) % 42.23/6.43 | % 42.23/6.43 | ALPHA: (69) implies: % 42.23/6.43 | (70) vATMap(all_500_2) % 42.23/6.43 | (71) vATMap(all_500_1) % 42.23/6.43 | (72) vMC(all_500_2, all_500_1) = all_500_0 % 42.23/6.43 | (73) vptcheck(all_442_0, vq2, all_500_0) = 0 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (60), (61) imply: % 42.23/6.43 | (74) vgetQuest(all_420_4) = vq2 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (60), (62) imply: % 42.23/6.43 | (75) vgetQM(all_420_4) = all_420_14 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (60), (63) imply: % 42.23/6.43 | (76) vgetAM(all_420_4) = all_420_11 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (58), (66), (67) imply: % 42.23/6.43 | (77) vMC(all_420_9, all_420_8) = all_442_0 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (12) with all_420_7, all_442_0, all_420_8, % 42.23/6.43 | all_420_9, simplifying with (33), (77) gives: % 42.23/6.43 | (78) all_442_0 = all_420_7 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (7) with all_420_13, all_420_11, all_420_4, % 42.23/6.43 | simplifying with (48), (76) gives: % 42.23/6.43 | (79) all_420_11 = all_420_13 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (8) with all_420_10, all_420_14, all_420_4, % 42.23/6.43 | simplifying with (47), (75) gives: % 42.23/6.43 | (80) all_420_10 = all_420_14 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (9) with all_420_15, vq2, all_420_4, simplifying % 42.23/6.43 | with (46), (74) gives: % 42.23/6.43 | (81) all_420_15 = vq2 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (73), (78) imply: % 42.23/6.43 | (82) vptcheck(all_420_7, vq2, all_500_0) = 0 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (43), (81) imply: % 42.23/6.43 | (83) vptcheck(all_420_1, vq2, all_420_6) = all_420_0 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (59), (78) imply: % 42.23/6.43 | (84) vptcheck(all_420_7, vqempty, all_420_7) = 0 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (41), (80) imply: % 42.23/6.43 | (85) vtypeQM(all_420_14) = all_420_2 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (39), (79) imply: % 42.23/6.43 | (86) vtypeAM(all_420_13) = all_420_9 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (10) with all_420_3, all_420_9, all_420_13, % 42.23/6.43 | simplifying with (38), (86) gives: % 42.23/6.43 | (87) all_420_3 = all_420_9 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (11) with all_420_8, all_420_2, all_420_14, % 42.23/6.43 | simplifying with (40), (85) gives: % 42.23/6.43 | (88) all_420_2 = all_420_8 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (34), (87), (88) imply: % 42.23/6.43 | (89) vMC(all_420_9, all_420_8) = all_420_1 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (12) with all_420_7, all_420_1, all_420_8, % 42.23/6.43 | all_420_9, simplifying with (33), (89) gives: % 42.23/6.43 | (90) all_420_1 = all_420_7 % 42.23/6.43 | % 42.23/6.43 | REDUCE: (83), (90) imply: % 42.23/6.43 | (91) vptcheck(all_420_7, vq2, all_420_6) = all_420_0 % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (Tqseq_inv4) with all_420_8, all_500_2, all_500_1, % 42.23/6.43 | vqempty, all_420_9, all_420_8, all_420_12, all_420_9, all_420_16, % 42.23/6.43 | vq2, all_420_7, all_406_0, all_420_6, all_420_7, all_500_0, % 42.23/6.43 | simplifying with (5), (20), (21), (22), (23), (32), (33), (42), % 42.23/6.43 | (44), (45), (70), (71), (72), (82) gives: % 42.23/6.43 | (92) all_500_1 = all_420_16 | ? [v0: int] : ( ~ (v0 = 0) & % 42.23/6.43 | vptcheck(all_420_7, vqempty, all_420_7) = v0) % 42.23/6.43 | % 42.23/6.43 | GROUND_INST: instantiating (Tqseq_inv3) with all_420_8, all_500_2, all_500_1, % 42.23/6.43 | vqempty, all_420_9, all_420_8, all_420_12, all_420_9, all_420_16, % 42.23/6.43 | vq2, all_420_7, all_406_0, all_420_6, all_420_7, all_500_0, % 42.23/6.43 | simplifying with (5), (20), (21), (22), (23), (32), (33), (42), % 42.23/6.43 | (44), (45), (70), (71), (72), (82) gives: % 42.23/6.43 | (93) all_500_2 = all_420_12 | ? [v0: int] : ( ~ (v0 = 0) & % 42.23/6.43 | vptcheck(all_420_7, vqempty, all_420_7) = v0) % 42.23/6.43 | % 42.23/6.43 | BETA: splitting (93) gives: % 42.23/6.44 | % 42.23/6.44 | Case 1: % 42.23/6.44 | | % 42.23/6.44 | | (94) all_500_2 = all_420_12 % 42.23/6.44 | | % 42.23/6.44 | | REDUCE: (72), (94) imply: % 42.23/6.44 | | (95) vMC(all_420_12, all_500_1) = all_500_0 % 42.23/6.44 | | % 42.23/6.44 | | BETA: splitting (92) gives: % 42.23/6.44 | | % 42.23/6.44 | | Case 1: % 42.23/6.44 | | | % 42.23/6.44 | | | (96) all_500_1 = all_420_16 % 42.23/6.44 | | | % 42.23/6.44 | | | REDUCE: (95), (96) imply: % 42.23/6.44 | | | (97) vMC(all_420_12, all_420_16) = all_500_0 % 42.23/6.44 | | | % 42.23/6.44 | | | GROUND_INST: instantiating (12) with all_420_6, all_500_0, all_420_16, % 42.23/6.44 | | | all_420_12, simplifying with (32), (97) gives: % 42.23/6.44 | | | (98) all_500_0 = all_420_6 % 42.23/6.44 | | | % 42.23/6.44 | | | REDUCE: (82), (98) imply: % 42.23/6.44 | | | (99) vptcheck(all_420_7, vq2, all_420_6) = 0 % 42.23/6.44 | | | % 42.23/6.44 | | | GROUND_INST: instantiating (13) with all_420_0, 0, all_420_6, vq2, % 42.23/6.44 | | | all_420_7, simplifying with (91), (99) gives: % 42.23/6.44 | | | (100) all_420_0 = 0 % 42.23/6.44 | | | % 42.23/6.44 | | | REDUCE: (19), (100) imply: % 42.23/6.44 | | | (101) $false % 42.23/6.44 | | | % 42.23/6.44 | | | CLOSE: (101) is inconsistent. % 42.23/6.44 | | | % 42.23/6.44 | | Case 2: % 42.23/6.44 | | | % 42.23/6.44 | | | (102) ? [v0: int] : ( ~ (v0 = 0) & vptcheck(all_420_7, vqempty, % 42.23/6.44 | | | all_420_7) = v0) % 42.23/6.44 | | | % 42.23/6.44 | | | DELTA: instantiating (102) with fresh symbol all_633_0 gives: % 42.23/6.44 | | | (103) ~ (all_633_0 = 0) & vptcheck(all_420_7, vqempty, all_420_7) = % 42.23/6.44 | | | all_633_0 % 42.23/6.44 | | | % 42.23/6.44 | | | REF_CLOSE: (13), (84), (103) are inconsistent by sub-proof #1. % 42.23/6.44 | | | % 42.23/6.44 | | End of split % 42.23/6.44 | | % 42.23/6.44 | Case 2: % 42.23/6.44 | | % 42.23/6.44 | | (104) ? [v0: int] : ( ~ (v0 = 0) & vptcheck(all_420_7, vqempty, % 42.23/6.44 | | all_420_7) = v0) % 42.23/6.44 | | % 42.23/6.44 | | DELTA: instantiating (104) with fresh symbol all_633_0 gives: % 42.23/6.44 | | (105) ~ (all_633_0 = 0) & vptcheck(all_420_7, vqempty, all_420_7) = % 42.23/6.44 | | all_633_0 % 42.23/6.44 | | % 42.23/6.44 | | REF_CLOSE: (13), (84), (105) are inconsistent by sub-proof #1. % 42.23/6.44 | | % 42.23/6.44 | End of split % 42.23/6.44 | % 42.23/6.44 End of proof % 42.23/6.44 % 42.23/6.44 Sub-proof #1 shows that the following formulas are inconsistent: % 42.23/6.44 ---------------------------------------------------------------- % 42.23/6.44 (1) ~ (all_633_0 = 0) & vptcheck(all_420_7, vqempty, all_420_7) = all_633_0 % 42.23/6.44 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 42.23/6.44 vMapConf] : ! [v3: vQuestionnaire] : ! [v4: vMapConf] : (v1 = v0 | ~ % 42.23/6.44 (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, v2) = v0)) % 42.23/6.44 (3) vptcheck(all_420_7, vqempty, all_420_7) = 0 % 42.23/6.44 % 42.23/6.44 Begin of proof % 42.23/6.44 | % 42.23/6.44 | ALPHA: (1) implies: % 42.23/6.44 | (4) ~ (all_633_0 = 0) % 42.23/6.44 | (5) vptcheck(all_420_7, vqempty, all_420_7) = all_633_0 % 42.23/6.44 | % 42.23/6.44 | GROUND_INST: instantiating (2) with 0, all_633_0, all_420_7, vqempty, % 42.23/6.44 | all_420_7, simplifying with (3), (5) gives: % 42.23/6.44 | (6) all_633_0 = 0 % 42.23/6.44 | % 42.23/6.44 | REDUCE: (4), (6) imply: % 42.23/6.44 | (7) $false % 42.23/6.44 | % 42.23/6.44 | CLOSE: (7) is inconsistent. % 42.23/6.44 | % 42.23/6.44 End of proof % 42.23/6.44 % SZS output end Proof for theBenchmark % 42.23/6.44 % 42.23/6.44 5839ms %------------------------------------------------------------------------------