%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM269_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 : n010.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:40 PM UTC 2026 % Result : Theorem 41.93s 6.22s % Output : Proof 50.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.16 % Problem : COM269_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.17 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.39 % Computer : n010.cluster.edu % 0.15/0.39 % Model : x86_64 x86_64 % 0.15/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.39 % Memory : 8042.1875MB % 0.15/0.39 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.39 % CPULimit : 300 % 0.15/0.39 % WCLimit : 300 % 0.15/0.39 % DateTime : Mon May 4 20:03:36 EDT 2026 % 0.15/0.39 % CPUTime : % 0.60/0.66 ________ _____ % 0.60/0.66 ___ __ \_________(_)________________________________ % 0.60/0.66 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.60/0.66 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.60/0.66 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.60/0.66 % 0.60/0.66 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.60/0.66 (2023-06-19) % 0.60/0.66 % 0.60/0.66 (c) Philipp Rümmer, 2009-2023 % 0.60/0.66 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.60/0.66 Amanda Stjerna. % 0.60/0.66 Free software under BSD-3-Clause. % 0.60/0.66 % 0.60/0.66 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.60/0.66 % 0.60/0.66 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.60/0.68 Running up to 7 provers in parallel. % 0.60/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.60/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.60/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.60/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.60/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.60/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.60/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.31/2.07 Prover 1: Preprocessing ... % 10.09/2.13 Prover 4: Preprocessing ... % 10.74/2.23 Prover 5: Preprocessing ... % 10.74/2.23 Prover 2: Preprocessing ... % 10.74/2.23 Prover 3: Preprocessing ... % 10.74/2.23 Prover 0: Preprocessing ... % 10.74/2.26 Prover 6: Preprocessing ... % 24.75/4.09 Prover 1: Warning: ignoring some quantifiers % 24.75/4.09 Prover 3: Warning: ignoring some quantifiers % 25.53/4.14 Prover 3: Constructing countermodel ... % 25.53/4.18 Prover 6: Proving ... % 25.53/4.19 Prover 1: Constructing countermodel ... % 28.53/4.52 Prover 5: Proving ... % 29.32/4.67 Prover 4: Warning: ignoring some quantifiers % 30.11/4.77 Prover 4: Constructing countermodel ... % 30.91/4.89 Prover 0: Proving ... % 35.61/5.45 Prover 2: Proving ... % 41.93/6.22 Prover 5: proved (5529ms) % 41.93/6.22 % 41.93/6.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 41.93/6.22 % 41.93/6.23 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 41.93/6.23 Prover 3: stopped % 41.93/6.23 Prover 6: stopped % 41.93/6.23 Prover 0: stopped % 41.93/6.24 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 41.93/6.24 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 41.93/6.24 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 41.93/6.25 Prover 2: stopped % 41.93/6.28 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 45.87/6.75 Prover 4: Found proof (size 34) % 45.87/6.75 Prover 4: proved (6065ms) % 45.87/6.76 Prover 1: stopped % 46.65/6.86 Prover 10: Preprocessing ... % 46.65/6.86 Prover 7: Preprocessing ... % 46.65/6.86 Prover 8: Preprocessing ... % 47.52/6.93 Prover 11: Preprocessing ... % 47.52/6.93 Prover 13: Preprocessing ... % 48.34/7.03 Prover 7: stopped % 48.34/7.03 Prover 10: stopped % 48.34/7.05 Prover 11: stopped % 48.94/7.13 Prover 13: stopped % 49.28/7.28 Prover 8: Warning: ignoring some quantifiers % 49.69/7.31 Prover 8: Constructing countermodel ... % 49.69/7.32 Prover 8: stopped % 49.69/7.32 % 49.69/7.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 49.69/7.33 % 49.69/7.34 % SZS output start Proof for theBenchmark % 49.69/7.36 Assumptions after simplification: % 49.69/7.36 --------------------------------- % 49.69/7.36 % 49.69/7.36 (Progress-qsingle-value-expIsValue-False-isSomeExp-True) % 50.13/7.41 ? [v0: vQMap] : ? [v1: vAType] : ? [v2: vATMap] : ? [v3: vATMap] : ? [v4: % 50.13/7.41 vAnsMap] : ? [v5: vQID] : ? [v6: vExp] : ? [v7: vOptExp] : ? [v8: int] : % 50.13/7.41 ? [v9: vEntry] : ? [v10: vQuestionnaire] : ? [v11: int] : ? [v12: vATMap] % 50.13/7.41 : ? [v13: vATMap] : ? [v14: vMapConf] : ? [v15: vMapConf] : ? [v16: % 50.13/7.41 vOptQConf] : ( ~ (v11 = 0) & ~ (v8 = 0) & vptcheck(v14, v10, v15) = 0 & % 50.13/7.41 vtypeQM(v0) = v13 & vtypeAM(v4) = v12 & vreduce(v10, v4, v0) = v16 & % 50.13/7.41 vreduceExp(v6, v4) = v7 & vexpIsValue(v6) = v8 & visSomeExp(v7) = 0 & % 50.13/7.41 visValue(v10) = v11 & vqsingle(v9) = v10 & vMC(v12, v13) = v14 & vMC(v2, v3) % 50.13/7.41 = v15 & vvalue(v5, v1, v6) = v9 & vAType(v1) & vOptExp(v7) & vQID(v5) & % 50.13/7.41 vQMap(v0) & vExp(v6) & vAnsMap(v4) & vOptQConf(v16) & vQuestionnaire(v10) & % 50.13/7.41 vATMap(v13) & vATMap(v12) & vATMap(v3) & vATMap(v2) & vMapConf(v15) & % 50.13/7.41 vMapConf(v14) & vEntry(v9) & ! [v17: vAnsMap] : ! [v18: vQMap] : ! [v19: % 50.13/7.41 vQuestionnaire] : ! [v20: vQConf] : ( ~ (vQC(v17, v18, v19) = v20) | ~ % 50.13/7.41 vQMap(v18) | ~ vAnsMap(v17) | ~ vQuestionnaire(v19) | ? [v21: % 50.13/7.41 vOptQConf] : ( ~ (v21 = v16) & vsomeQConf(v20) = v21 & vOptQConf(v21)))) % 50.13/7.41 % 50.13/7.41 (reduce-3) % 50.13/7.42 ! [v0: vQMap] : ! [v1: vAType] : ! [v2: vAnsMap] : ! [v3: vQID] : ! [v4: % 50.13/7.42 vExp] : ! [v5: vOptExp] : ! [v6: vExp] : ! [v7: vEntry] : ! [v8: % 50.13/7.42 vQuestionnaire] : ! [v9: vQConf] : ( ~ (vreduceExp(v4, v2) = v5) | ~ % 50.13/7.42 (vgetExp(v5) = v6) | ~ (vQC(v2, v0, v8) = v9) | ~ (vqsingle(v7) = v8) | ~ % 50.13/7.42 (vvalue(v3, v1, v6) = v7) | ~ vAType(v1) | ~ vQID(v3) | ~ vQMap(v0) | ~ % 50.13/7.42 vExp(v4) | ~ vAnsMap(v2) | ? [v10: any] : ? [v11: any] : ? [v12: vEntry] % 50.13/7.42 : ? [v13: vQuestionnaire] : ? [v14: vOptQConf] : ? [v15: vOptQConf] : % 50.13/7.42 (vreduce(v13, v2, v0) = v14 & vexpIsValue(v4) = v10 & visSomeExp(v5) = v11 & % 50.13/7.42 vsomeQConf(v9) = v15 & vqsingle(v12) = v13 & vvalue(v3, v1, v4) = v12 & % 50.13/7.42 vOptQConf(v15) & vOptQConf(v14) & vQuestionnaire(v13) & vEntry(v12) & ( ~ % 50.13/7.42 (v11 = 0) | v15 = v14 | v10 = 0))) & ! [v0: vQMap] : ! [v1: vAType] : % 50.13/7.42 ! [v2: vAnsMap] : ! [v3: vQID] : ! [v4: vExp] : ! [v5: vEntry] : ! [v6: % 50.13/7.42 vQuestionnaire] : ! [v7: vOptQConf] : ( ~ (vreduce(v6, v2, v0) = v7) | ~ % 50.13/7.42 (vqsingle(v5) = v6) | ~ (vvalue(v3, v1, v4) = v5) | ~ vAType(v1) | ~ % 50.13/7.42 vQID(v3) | ~ vQMap(v0) | ~ vExp(v4) | ~ vAnsMap(v2) | ? [v8: any] : ? % 50.13/7.42 [v9: vOptExp] : ? [v10: any] : ? [v11: vExp] : ? [v12: vEntry] : ? [v13: % 50.13/7.42 vQuestionnaire] : ? [v14: vQConf] : ? [v15: vOptQConf] : (vreduceExp(v4, % 50.13/7.42 v2) = v9 & vexpIsValue(v4) = v8 & visSomeExp(v9) = v10 & vgetExp(v9) = % 50.13/7.42 v11 & vQC(v2, v0, v13) = v14 & vsomeQConf(v14) = v15 & vqsingle(v12) = v13 % 50.13/7.42 & vvalue(v3, v1, v11) = v12 & vOptExp(v9) & vExp(v11) & vOptQConf(v15) & % 50.13/7.42 vQConf(v14) & vQuestionnaire(v13) & vEntry(v12) & ( ~ (v10 = 0) | v15 = v7 % 50.13/7.42 | v8 = 0))) % 50.13/7.42 % 50.13/7.42 (reduce-8) % 50.13/7.42 vQuestionnaire(vqempty) & ! [v0: vQuestionnaire] : ! [v1: vAnsMap] : ! [v2: % 50.13/7.42 vQMap] : ! [v3: vQuestionnaire] : ! [v4: vOptQConf] : ( ~ (vreduce(v3, v1, % 50.13/7.42 v2) = v4) | ~ (vqseq(vqempty, v0) = v3) | ~ vQMap(v2) | ~ vAnsMap(v1) % 50.13/7.42 | ~ vQuestionnaire(v0) | ? [v5: vQConf] : (vQC(v1, v2, v0) = v5 & % 50.13/7.42 vsomeQConf(v5) = v4 & vOptQConf(v4) & vQConf(v5))) & ! [v0: % 50.13/7.42 vQuestionnaire] : ! [v1: vAnsMap] : ! [v2: vQMap] : ! [v3: vQConf] : ( ~ % 50.13/7.42 (vQC(v1, v2, v0) = v3) | ~ vQMap(v2) | ~ vAnsMap(v1) | ~ % 50.13/7.42 vQuestionnaire(v0) | ? [v4: vQuestionnaire] : ? [v5: vOptQConf] : % 50.13/7.42 (vreduce(v4, v1, v2) = v5 & vsomeQConf(v3) = v5 & vqseq(vqempty, v0) = v4 & % 50.13/7.43 vOptQConf(v5) & vQuestionnaire(v4))) % 50.13/7.43 % 50.13/7.43 (function-axioms) % 50.13/7.45 ! [v0: vQMap] : ! [v1: vQMap] : ! [v2: vQMap] : ! [v3: vAType] : ! [v4: % 50.13/7.45 vLabel] : ! [v5: vQID] : (v1 = v0 | ~ (vqmbind(v5, v4, v3, v2) = v1) | ~ % 50.13/7.45 (vqmbind(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 50.13/7.45 MultipleValueBool] : ! [v2: vMapConf] : ! [v3: vQuestionnaire] : ! [v4: % 50.13/7.45 vMapConf] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, % 50.13/7.45 v2) = v0)) & ! [v0: vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : % 50.13/7.45 ! [v3: vAType] : ! [v4: vBinOpT] : (v1 = v0 | ~ (vcheckBinOp(v4, v3, v2) = % 50.13/7.45 v1) | ~ (vcheckBinOp(v4, v3, v2) = v0)) & ! [v0: vOptQConf] : ! [v1: % 50.13/7.45 vOptQConf] : ! [v2: vQMap] : ! [v3: vAnsMap] : ! [v4: vQuestionnaire] : % 50.13/7.45 (v1 = v0 | ~ (vreduce(v4, v3, v2) = v1) | ~ (vreduce(v4, v3, v2) = v0)) & ! % 50.13/7.45 [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vAval] : ! [v4: % 50.13/7.45 vBinOpT] : (v1 = v0 | ~ (vevalBinOp(v4, v3, v2) = v1) | ~ (vevalBinOp(v4, % 50.13/7.45 v3, v2) = v0)) & ! [v0: vQConf] : ! [v1: vQConf] : ! [v2: % 50.13/7.45 vQuestionnaire] : ! [v3: vQMap] : ! [v4: vAnsMap] : (v1 = v0 | ~ (vQC(v4, % 50.13/7.45 v3, v2) = v1) | ~ (vQC(v4, v3, v2) = v0)) & ! [v0: vATMap] : ! [v1: % 50.13/7.45 vATMap] : ! [v2: vATMap] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ % 50.13/7.45 (vatmbind(v4, v3, v2) = v1) | ~ (vatmbind(v4, v3, v2) = v0)) & ! [v0: % 50.13/7.45 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vAType] : ! [v3: vLabel] : % 50.13/7.45 ! [v4: vQID] : (v1 = v0 | ~ (vsomeQuestion(v4, v3, v2) = v1) | ~ % 50.13/7.45 (vsomeQuestion(v4, v3, v2) = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! % 50.13/7.45 [v2: vAnsMap] : ! [v3: vAval] : ! [v4: vQID] : (v1 = v0 | ~ (vabind(v4, v3, % 50.13/7.45 v2) = v1) | ~ (vabind(v4, v3, v2) = v0)) & ! [v0: vQuestionnaire] : ! % 50.13/7.45 [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! [v3: vQuestionnaire] : ! % 50.13/7.45 [v4: vExp] : (v1 = v0 | ~ (vqcond(v4, v3, v2) = v1) | ~ (vqcond(v4, v3, v2) % 50.13/7.45 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: vBinOpT] % 50.13/7.45 : ! [v4: vExp] : (v1 = v0 | ~ (vbinop(v4, v3, v2) = v1) | ~ (vbinop(v4, v3, % 50.13/7.45 v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! [v2: vAType] : ! % 50.13/7.45 [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ (vdefquestion(v4, v3, v2) = v1) | % 50.13/7.45 ~ (vdefquestion(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! % 50.13/7.45 [v2: vExp] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ (vvalue(v4, v3, % 50.13/7.45 v2) = v1) | ~ (vvalue(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: % 50.13/7.45 vEntry] : ! [v2: vAType] : ! [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ % 50.13/7.45 (vquestion(v4, v3, v2) = v1) | ~ (vquestion(v4, v3, v2) = v0)) & ! [v0: % 50.13/7.45 vOptAType] : ! [v1: vOptAType] : ! [v2: vExp] : ! [v3: vATMap] : (v1 = v0 % 50.13/7.45 | ~ (vecheck(v3, v2) = v1) | ~ (vecheck(v3, v2) = v0)) & ! [v0: % 50.13/7.45 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : ! [v3: vUnOpT] : (v1 = % 50.13/7.45 v0 | ~ (vcheckUnOp(v3, v2) = v1) | ~ (vcheckUnOp(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 50.13/7.46 ~ (vintersectATM(v3, v2) = v1) | ~ (vintersectATM(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 50.13/7.46 ~ (vappendATMap(v3, v2) = v1) | ~ (vappendATMap(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vOptAType] : ! [v1: vOptAType] : ! [v2: vATMap] : ! [v3: vQID] : (v1 = v0 % 50.13/7.46 | ~ (vlookupATMap(v3, v2) = v1) | ~ (vlookupATMap(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vOptExp] : ! [v1: vOptExp] : ! [v2: vAnsMap] : ! [v3: vExp] : (v1 = v0 | % 50.13/7.46 ~ (vreduceExp(v3, v2) = v1) | ~ (vreduceExp(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vUnOpT] : (v1 = v0 | % 50.13/7.46 ~ (vevalUnOp(v3, v2) = v1) | ~ (vevalUnOp(v3, v2) = v0)) & ! [v0: vAval] : % 50.13/7.46 ! [v1: vAval] : ! [v2: vAType] : ! [v3: vLabel] : (v1 = v0 | ~ % 50.13/7.46 (vgetAnswer(v3, v2) = v1) | ~ (vgetAnswer(v3, v2) = v0)) & ! [v0: vQConf] % 50.13/7.46 : ! [v1: vQConf] : ! [v2: vQuestionnaire] : ! [v3: vQConf] : (v1 = v0 | ~ % 50.13/7.46 (vqcappend(v3, v2) = v1) | ~ (vqcappend(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vQMap] : ! [v3: vQID] : (v1 % 50.13/7.46 = v0 | ~ (vlookupQMap(v3, v2) = v1) | ~ (vlookupQMap(v3, v2) = v0)) & ! % 50.13/7.46 [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vAnsMap] : ! [v3: vAnsMap] : (v1 = % 50.13/7.46 v0 | ~ (vappendAnsMap(v3, v2) = v1) | ~ (vappendAnsMap(v3, v2) = v0)) & ! % 50.13/7.46 [v0: vOptAval] : ! [v1: vOptAval] : ! [v2: vAnsMap] : ! [v3: vQID] : (v1 = % 50.13/7.46 v0 | ~ (vlookupAnsMap(v3, v2) = v1) | ~ (vlookupAnsMap(v3, v2) = v0)) & ! % 50.13/7.46 [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vATList] : (v1 = % 50.13/7.46 v0 | ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vnat] % 50.13/7.46 : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vdivide(v3, % 50.13/7.46 v2) = v1) | ~ (vdivide(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : % 50.13/7.46 ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vmultiply(v3, v2) = v1) | ~ % 50.13/7.46 (vmultiply(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : % 50.13/7.46 ! [v3: vnat] : (v1 = v0 | ~ (vminus(v3, v2) = v1) | ~ (vminus(v3, v2) = v0)) % 50.13/7.46 & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | % 50.13/7.46 ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: % 50.13/7.46 vYN] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 50.13/7.46 (vlt(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vnat] : ! [v3: % 50.13/7.46 vnat] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vYN] : ! [v1: vYN] : ! [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vor(v3, % 50.13/7.46 v2) = v1) | ~ (vor(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! % 50.13/7.46 [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vand(v3, v2) = v1) | ~ (vand(v3, % 50.13/7.46 v2) = v0)) & ! [v0: vstring] : ! [v1: vstring] : ! [v2: vstring] : ! % 50.13/7.46 [v3: vchar] : (v1 = v0 | ~ (vscons(v3, v2) = v1) | ~ (vscons(v3, v2) = v0)) % 50.13/7.46 & ! [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vAType] : % 50.13/7.46 (v1 = v0 | ~ (vatcons(v3, v2) = v1) | ~ (vatcons(v3, v2) = v0)) & ! [v0: % 50.13/7.46 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! % 50.13/7.46 [v3: vGID] : (v1 = v0 | ~ (vqgroup(v3, v2) = v1) | ~ (vqgroup(v3, v2) = v0)) % 50.13/7.46 & ! [v0: vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] % 50.13/7.46 : ! [v3: vQuestionnaire] : (v1 = v0 | ~ (vqseq(v3, v2) = v1) | ~ (vqseq(v3, % 50.13/7.46 v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: % 50.13/7.46 vUnOpT] : (v1 = v0 | ~ (vunop(v3, v2) = v1) | ~ (vunop(v3, v2) = v0)) & ! % 50.13/7.46 [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = % 50.13/7.46 v0 | ~ (vMC(v3, v2) = v1) | ~ (vMC(v3, v2) = v0)) & ! [v0: vATMap] : ! % 50.13/7.46 [v1: vATMap] : ! [v2: vQMap] : (v1 = v0 | ~ (vtypeQM(v2) = v1) | ~ % 50.13/7.46 (vtypeQM(v2) = v0)) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vAnsMap] : % 50.13/7.46 (v1 = v0 | ~ (vtypeAM(v2) = v1) | ~ (vtypeAM(v2) = v0)) & ! [v0: % 50.13/7.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptMapConf] : (v1 % 50.13/7.46 = v0 | ~ (visSomeMapConf(v2) = v1) | ~ (visSomeMapConf(v2) = v0)) & ! % 50.13/7.46 [v0: vstring] : ! [v1: vstring] : ! [v2: vLabel] : (v1 = v0 | ~ % 50.13/7.46 (vaskText(v2) = v1) | ~ (vaskText(v2) = v0)) & ! [v0: vnat] : ! [v1: % 50.13/7.46 vnat] : ! [v2: vLabel] : (v1 = v0 | ~ (vaskNumber(v2) = v1) | ~ % 50.13/7.46 (vaskNumber(v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vLabel] : (v1 % 50.13/7.46 = v0 | ~ (vaskYesNo(v2) = v1) | ~ (vaskYesNo(v2) = v0)) & ! [v0: % 50.13/7.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] : (v1 = v0 | % 50.13/7.46 ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) & ! [v0: % 50.13/7.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptExp] : (v1 = % 50.13/7.46 v0 | ~ (visSomeExp(v2) = v1) | ~ (visSomeExp(v2) = v0)) & ! [v0: % 50.13/7.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQConf] : (v1 = % 50.13/7.46 v0 | ~ (visSomeQC(v2) = v1) | ~ (visSomeQC(v2) = v0)) & ! [v0: % 50.13/7.46 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuestionnaire] : % 50.13/7.46 (v1 = v0 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 50.13/7.46 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQConf] : (v1 = v0 | ~ % 50.13/7.46 (vgetQuest(v2) = v1) | ~ (vgetQuest(v2) = v0)) & ! [v0: vQMap] : ! [v1: % 50.13/7.46 vQMap] : ! [v2: vQConf] : (v1 = v0 | ~ (vgetQM(v2) = v1) | ~ (vgetQM(v2) % 50.13/7.46 = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vQConf] : (v1 = v0 % 50.13/7.46 | ~ (vgetAM(v2) = v1) | ~ (vgetAM(v2) = v0)) & ! [v0: MultipleValueBool] % 50.13/7.46 : ! [v1: MultipleValueBool] : ! [v2: vOptQuestion] : (v1 = v0 | ~ % 50.13/7.46 (visSomeQuestion(v2) = v1) | ~ (visSomeQuestion(v2) = v0)) & ! [v0: % 50.13/7.46 vAType] : ! [v1: vAType] : ! [v2: vAval] : (v1 = v0 | ~ (vtypeOf(v2) = % 50.13/7.46 v1) | ~ (vtypeOf(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 50.13/7.46 MultipleValueBool] : ! [v2: vOptAType] : (v1 = v0 | ~ (visSomeAType(v2) = % 50.13/7.46 v1) | ~ (visSomeAType(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 50.13/7.46 MultipleValueBool] : ! [v2: vOptAval] : (v1 = v0 | ~ (visSomeAval(v2) = % 50.13/7.46 v1) | ~ (visSomeAval(v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: % 50.13/7.46 vnat] : (v1 = v0 | ~ (vpred(v2) = v1) | ~ (vpred(v2) = v0)) & ! [v0: vYN] % 50.13/7.46 : ! [v1: vYN] : ! [v2: vYN] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) = % 50.13/7.46 v0)) & ! [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vOptMapConf] : (v1 % 50.13/7.46 = v0 | ~ (vgetMapConf(v2) = v1) | ~ (vgetMapConf(v2) = v0)) & ! [v0: % 50.13/7.46 vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ (vgetExpValue(v2) = % 50.13/7.46 v1) | ~ (vgetExpValue(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 50.13/7.46 [v2: vOptExp] : (v1 = v0 | ~ (vgetExp(v2) = v1) | ~ (vgetExp(v2) = v0)) & ! % 50.13/7.46 [v0: vQConf] : ! [v1: vQConf] : ! [v2: vOptQConf] : (v1 = v0 | ~ % 50.13/7.46 (vgetQC(v2) = v1) | ~ (vgetQC(v2) = v0)) & ! [v0: vAType] : ! [v1: % 50.13/7.46 vAType] : ! [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionAType(v2) = v1) % 50.13/7.46 | ~ (vgetQuestionAType(v2) = v0)) & ! [v0: vLabel] : ! [v1: vLabel] : ! % 50.13/7.46 [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionLabel(v2) = v1) | ~ % 50.13/7.46 (vgetQuestionLabel(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: % 50.13/7.46 vOptQuestion] : (v1 = v0 | ~ (vgetQuestionQID(v2) = v1) | ~ % 50.13/7.46 (vgetQuestionQID(v2) = v0)) & ! [v0: vAType] : ! [v1: vAType] : ! [v2: % 50.13/7.46 vOptAType] : (v1 = v0 | ~ (vgetAType(v2) = v1) | ~ (vgetAType(v2) = v0)) & % 50.13/7.46 ! [v0: vAval] : ! [v1: vAval] : ! [v2: vOptAval] : (v1 = v0 | ~ % 50.13/7.46 (vgetAval(v2) = v1) | ~ (vgetAval(v2) = v0)) & ! [v0: vOptAval] : ! [v1: % 50.13/7.46 vOptAval] : ! [v2: vAval] : (v1 = v0 | ~ (vsomeAval(v2) = v1) | ~ % 50.13/7.46 (vsomeAval(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: vQID] : (v1 % 50.13/7.46 = v0 | ~ (venumQID(v2) = v1) | ~ (venumQID(v2) = v0)) & ! [v0: % 50.13/7.46 vOptMapConf] : ! [v1: vOptMapConf] : ! [v2: vMapConf] : (v1 = v0 | ~ % 50.13/7.46 (vsomeMapConf(v2) = v1) | ~ (vsomeMapConf(v2) = v0)) & ! [v0: vGID] : ! % 50.13/7.46 [v1: vGID] : ! [v2: vGID] : (v1 = v0 | ~ (venumGID(v2) = v1) | ~ % 50.13/7.46 (venumGID(v2) = v0)) & ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vExp] : % 50.13/7.46 (v1 = v0 | ~ (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) & ! [v0: vAval] : % 50.13/7.46 ! [v1: vAval] : ! [v2: vstring] : (v1 = v0 | ~ (vT(v2) = v1) | ~ (vT(v2) = % 50.13/7.46 v0)) & ! [v0: vAval] : ! [v1: vAval] : ! [v2: vnat] : (v1 = v0 | ~ % 50.13/7.46 (vNum(v2) = v1) | ~ (vNum(v2) = v0)) & ! [v0: vAval] : ! [v1: vAval] : ! % 50.13/7.46 [v2: vYN] : (v1 = v0 | ~ (vB(v2) = v1) | ~ (vB(v2) = v0)) & ! [v0: % 50.13/7.46 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : (v1 = v0 | ~ % 50.13/7.46 (vsomeAType(v2) = v1) | ~ (vsomeAType(v2) = v0)) & ! [v0: vOptQConf] : ! % 50.13/7.46 [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | ~ (vsomeQConf(v2) = v1) | ~ % 50.13/7.46 (vsomeQConf(v2) = v0)) & ! [v0: vchar] : ! [v1: vchar] : ! [v2: vchar] : % 50.13/7.46 (v1 = v0 | ~ (venumchar(v2) = v1) | ~ (venumchar(v2) = v0)) & ! [v0: % 50.13/7.46 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vEntry] : (v1 = v0 | ~ % 50.13/7.46 (vqsingle(v2) = v1) | ~ (vqsingle(v2) = v0)) & ! [v0: vnat] : ! [v1: % 50.13/7.46 vnat] : ! [v2: vnat] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = % 50.13/7.46 v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vQID] : (v1 = v0 | ~ % 50.13/7.46 (vqvar(v2) = v1) | ~ (vqvar(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 50.13/7.46 [v2: vAval] : (v1 = v0 | ~ (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & % 50.13/7.46 ! [v0: vLabel] : ! [v1: vLabel] : ! [v2: vLabel] : (v1 = v0 | ~ % 50.13/7.46 (venumLabel(v2) = v1) | ~ (venumLabel(v2) = v0)) & ! [v0: vEntry] : ! % 50.13/7.46 [v1: vEntry] : ! [v2: vQID] : (v1 = v0 | ~ (vask(v2) = v1) | ~ (vask(v2) = % 50.13/7.46 v0)) % 50.13/7.46 % 50.13/7.46 Further assumptions not needed in the proof: % 50.13/7.46 -------------------------------------------- % 50.13/7.46 DIFF-B-Num, DIFF-B-T, DIFF-Num-T, DIFF-Number-Text, DIFF-YesNo-Number, % 50.13/7.46 DIFF-YesNo-Text, DIFF-addop-andop, DIFF-addop-divop, DIFF-addop-eqop, % 50.13/7.46 DIFF-addop-gtop, DIFF-addop-ltop, DIFF-addop-mulop, DIFF-addop-orop, % 50.13/7.46 DIFF-addop-subop, DIFF-aempty-abind, DIFF-andop-orop, DIFF-atempty-atcons, % 50.13/7.46 DIFF-atmempty-atmbind, DIFF-binop-unop, DIFF-constant-binop, DIFF-constant-qvar, % 50.13/7.46 DIFF-constant-unop, DIFF-defquestion-ask, DIFF-divop-andop, DIFF-divop-eqop, % 50.13/7.46 DIFF-divop-gtop, DIFF-divop-ltop, DIFF-divop-orop, DIFF-eqop-andop, % 50.13/7.46 DIFF-eqop-gtop, DIFF-eqop-ltop, DIFF-eqop-orop, DIFF-gtop-andop, DIFF-gtop-ltop, % 50.13/7.46 DIFF-gtop-orop, DIFF-initGID-enumGID, DIFF-initLabel-enumLabel, % 50.13/7.46 DIFF-initQID-enumQID, DIFF-initchar-enumchar, DIFF-ltop-andop, DIFF-ltop-orop, % 50.13/7.46 DIFF-mulop-andop, DIFF-mulop-divop, DIFF-mulop-eqop, DIFF-mulop-gtop, % 50.13/7.46 DIFF-mulop-ltop, DIFF-mulop-orop, DIFF-noAType-someAType, DIFF-noAval-someAval, % 50.13/7.46 DIFF-noExp-someExp, DIFF-noMapConf-someMapConf, DIFF-noQConf-someQConf, % 50.13/7.46 DIFF-noQuestion-someQuestion, DIFF-qcond-qgroup, DIFF-qempty-qcond, % 50.13/7.46 DIFF-qempty-qgroup, DIFF-qempty-qseq, DIFF-qempty-qsingle, DIFF-qmempty-qmbind, % 50.13/7.46 DIFF-qseq-qcond, DIFF-qseq-qgroup, DIFF-qsingle-qcond, DIFF-qsingle-qgroup, % 50.13/7.46 DIFF-qsingle-qseq, DIFF-question-ask, DIFF-question-defquestion, % 50.13/7.46 DIFF-question-value, DIFF-qvar-binop, DIFF-qvar-unop, DIFF-sempty-scons, % 50.13/7.46 DIFF-subop-andop, DIFF-subop-divop, DIFF-subop-eqop, DIFF-subop-gtop, % 50.13/7.46 DIFF-subop-ltop, DIFF-subop-mulop, DIFF-subop-orop, DIFF-value-ask, % 50.13/7.46 DIFF-value-defquestion, DIFF-yes-no, DIFF-zero-succ, EQ-B, EQ-MC, EQ-Num, EQ-QC, % 50.13/7.46 EQ-T, EQ-abind, EQ-ask, EQ-atcons, EQ-atmbind, EQ-binop, EQ-constant, % 50.13/7.46 EQ-defquestion, EQ-enumGID, EQ-enumLabel, EQ-enumQID, EQ-enumchar, EQ-qcond, % 50.13/7.46 EQ-qgroup, EQ-qmbind, EQ-qseq, EQ-qsingle, EQ-question, EQ-qvar, EQ-scons, % 50.13/7.46 EQ-someAType, EQ-someAval, EQ-someExp, EQ-someMapConf, EQ-someQConf, % 50.13/7.46 EQ-someQuestion, EQ-succ, EQ-unop, EQ-value, Task, Task_inv1, Task_inv2, % 50.13/7.46 Task_inv3, Task_inv4, Tdefquestion, Tdefquestion_inv1, Tdefquestion_inv2, % 50.13/7.46 Tdefquestion_inv3, Tqcond, Tqcond_inv1, Tqcond_inv2, Tqcond_inv3, Tqcond_inv4, % 50.13/7.46 Tqcond_inv5, Tqcond_inv6, Tqcond_inv7, Tqempty, Tqempty_inv1, Tqempty_inv2, % 50.13/7.46 Tqgroup, Tqgroup_inv, Tqseq, Tqseq_inv1, Tqseq_inv2, Tqseq_inv3, Tqseq_inv4, % 50.13/7.46 Tquestion, Tquestion_inv1, Tquestion_inv2, Tquestion_inv3, Tvalue, Tvalue_inv1, % 50.13/7.46 Tvalue_inv2, Tvalue_inv3, Tvalue_inv4, and-0, and-1, and-INV, append-0, % 50.13/7.46 append-1, append-INV, appendATMap-0, appendATMap-1, appendATMap-INV, % 50.13/7.46 appendAnsMap-0, appendAnsMap-1, appendAnsMap-INV, checkBinOp-0, checkBinOp-1, % 50.13/7.46 checkBinOp-2, checkBinOp-3, checkBinOp-4, checkBinOp-5, checkBinOp-6, % 50.13/7.46 checkBinOp-7, checkBinOp-8, checkBinOp-9, checkBinOp-INV, checkUnOp-0, % 50.13/7.46 checkUnOp-1, checkUnOp-INV, divide-0, divide-1, divide-INV, dom-ATList, % 50.13/7.46 dom-ATMap, dom-AType, dom-AnsMap, dom-Aval, dom-BinOpT, dom-Entry, dom-Exp, % 50.13/7.46 dom-MapConf, dom-OptAType, dom-OptAval, dom-OptExp, dom-OptMapConf, % 50.13/7.46 dom-OptQConf, dom-OptQuestion, dom-QConf, dom-QMap, dom-Questionnaire, % 50.13/7.46 dom-UnOpT, dom-YN, dom-nat, dom-string, echeck-0, echeck-1, echeck-2, echeck-3, % 50.13/7.46 echeck-4, echeck-5, echeck-6, echeck-7, echeck-INV, evalBinOp-0, evalBinOp-1, % 50.13/7.46 evalBinOp-10, evalBinOp-2, evalBinOp-3, evalBinOp-4, evalBinOp-5, evalBinOp-6, % 50.13/7.46 evalBinOp-7, evalBinOp-8, evalBinOp-9, evalBinOp-INV, evalUnOp-0, evalUnOp-1, % 50.13/7.46 evalUnOp-INV, expIsValue-0, expIsValue-1, expIsValue-false-INV, % 50.13/7.46 expIsValue-true-INV, getAM-0, getAM-INV, getAType-0, getAnswer-0, getAnswer-1, % 50.13/7.46 getAnswer-2, getAnswer-INV, getAval-0, getExp-0, getExpValue-0, getMapConf-0, % 50.13/7.46 getQC-0, getQM-0, getQM-INV, getQuest-0, getQuest-INV, getQuestionAType-0, % 50.13/7.46 getQuestionLabel-0, getQuestionQID-0, gt-0, gt-1, gt-2, gt-INV, intersectATM-0, % 50.13/7.46 intersectATM-1, intersectATM-2, intersectATM-INV, isSomeAType-0, isSomeAType-1, % 50.13/7.46 isSomeAType-false-INV, isSomeAType-true-INV, isSomeAval-0, isSomeAval-1, % 50.13/7.46 isSomeAval-false-INV, isSomeAval-true-INV, isSomeExp-0, isSomeExp-1, % 50.13/7.46 isSomeExp-false-INV, isSomeExp-true-INV, isSomeMapConf-0, isSomeMapConf-1, % 50.13/7.46 isSomeMapConf-false-INV, isSomeMapConf-true-INV, isSomeQC-0, isSomeQC-1, % 50.13/7.46 isSomeQC-false-INV, isSomeQC-true-INV, isSomeQuestion-0, isSomeQuestion-1, % 50.13/7.46 isSomeQuestion-false-INV, isSomeQuestion-true-INV, isValue-0, isValue-1, % 50.13/7.46 isValue-false-INV, isValue-true-INV, lookupATMap-0, lookupATMap-1, % 50.13/7.46 lookupATMap-2, lookupATMap-INV, lookupAnsMap-0, lookupAnsMap-1, lookupAnsMap-2, % 50.13/7.46 lookupAnsMap-INV, lookupQMap-0, lookupQMap-1, lookupQMap-2, lookupQMap-INV, % 50.13/7.46 lt-0, lt-1, lt-2, lt-INV, minus-0, minus-1, minus-INV, multiply-0, multiply-1, % 50.13/7.46 multiply-INV, not-0, not-1, not-INV, or-0, or-1, or-INV, plus-0, plus-1, % 50.13/7.46 plus-INV, pred-0, pred-1, pred-INV, qcappend-0, qcappend-INV, reduce-0, % 50.13/7.46 reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, % 50.13/7.46 reduce-2, reduce-4, reduce-5, reduce-6, reduce-7, reduce-9, reduce-INV, % 50.13/7.46 reduceExp-0, reduceExp-1, reduceExp-10, reduceExp-2, reduceExp-3, reduceExp-4, % 50.13/7.46 reduceExp-5, reduceExp-6, reduceExp-7, reduceExp-8, reduceExp-9, reduceExp-INV, % 50.13/7.46 reduceExpPreservation, reduceExpProgress, typeAM-0, typeAM-1, typeAM-INV, % 50.13/7.46 typeOf-0, typeOf-1, typeOf-2, typeOf-INV, typeQM-0, typeQM-1, typeQM-INV % 50.13/7.46 % 50.13/7.46 Those formulas are unsatisfiable: % 50.13/7.46 --------------------------------- % 50.13/7.46 % 50.13/7.46 Begin of proof % 50.13/7.46 | % 50.13/7.46 | ALPHA: (reduce-3) implies: % 50.13/7.46 | (1) ! [v0: vQMap] : ! [v1: vAType] : ! [v2: vAnsMap] : ! [v3: vQID] : % 50.13/7.46 | ! [v4: vExp] : ! [v5: vEntry] : ! [v6: vQuestionnaire] : ! [v7: % 50.13/7.46 | vOptQConf] : ( ~ (vreduce(v6, v2, v0) = v7) | ~ (vqsingle(v5) = v6) % 50.13/7.46 | | ~ (vvalue(v3, v1, v4) = v5) | ~ vAType(v1) | ~ vQID(v3) | ~ % 50.13/7.46 | vQMap(v0) | ~ vExp(v4) | ~ vAnsMap(v2) | ? [v8: any] : ? [v9: % 50.13/7.46 | vOptExp] : ? [v10: any] : ? [v11: vExp] : ? [v12: vEntry] : ? % 50.13/7.46 | [v13: vQuestionnaire] : ? [v14: vQConf] : ? [v15: vOptQConf] : % 50.13/7.46 | (vreduceExp(v4, v2) = v9 & vexpIsValue(v4) = v8 & visSomeExp(v9) = % 50.13/7.46 | v10 & vgetExp(v9) = v11 & vQC(v2, v0, v13) = v14 & vsomeQConf(v14) % 50.13/7.46 | = v15 & vqsingle(v12) = v13 & vvalue(v3, v1, v11) = v12 & % 50.13/7.46 | vOptExp(v9) & vExp(v11) & vOptQConf(v15) & vQConf(v14) & % 50.13/7.46 | vQuestionnaire(v13) & vEntry(v12) & ( ~ (v10 = 0) | v15 = v7 | v8 = % 50.13/7.46 | 0))) % 50.13/7.46 | % 50.13/7.46 | ALPHA: (reduce-8) implies: % 50.13/7.46 | (2) ! [v0: vQuestionnaire] : ! [v1: vAnsMap] : ! [v2: vQMap] : ! [v3: % 50.13/7.46 | vQConf] : ( ~ (vQC(v1, v2, v0) = v3) | ~ vQMap(v2) | ~ vAnsMap(v1) % 50.13/7.46 | | ~ vQuestionnaire(v0) | ? [v4: vQuestionnaire] : ? [v5: % 50.13/7.46 | vOptQConf] : (vreduce(v4, v1, v2) = v5 & vsomeQConf(v3) = v5 & % 50.13/7.46 | vqseq(vqempty, v0) = v4 & vOptQConf(v5) & vQuestionnaire(v4))) % 50.13/7.46 | % 50.13/7.46 | ALPHA: (function-axioms) implies: % 50.13/7.47 | (3) ! [v0: vOptQConf] : ! [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | % 50.13/7.47 | ~ (vsomeQConf(v2) = v1) | ~ (vsomeQConf(v2) = v0)) % 50.13/7.47 | (4) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 50.13/7.47 | vOptExp] : (v1 = v0 | ~ (visSomeExp(v2) = v1) | ~ (visSomeExp(v2) = % 50.13/7.47 | v0)) % 50.13/7.47 | (5) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] % 50.13/7.47 | : (v1 = v0 | ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) % 50.13/7.47 | (6) ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAnsMap] : ! [v3: vExp] % 50.13/7.47 | : (v1 = v0 | ~ (vreduceExp(v3, v2) = v1) | ~ (vreduceExp(v3, v2) = % 50.13/7.47 | v0)) % 50.13/7.47 | % 50.13/7.47 | DELTA: instantiating (Progress-qsingle-value-expIsValue-False-isSomeExp-True) % 50.13/7.47 | with fresh symbols all_403_0, all_403_1, all_403_2, all_403_3, % 50.13/7.47 | all_403_4, all_403_5, all_403_6, all_403_7, all_403_8, all_403_9, % 50.13/7.47 | all_403_10, all_403_11, all_403_12, all_403_13, all_403_14, all_403_15, % 50.13/7.47 | all_403_16 gives: % 50.13/7.47 | (7) ~ (all_403_5 = 0) & ~ (all_403_8 = 0) & vptcheck(all_403_2, % 50.13/7.47 | all_403_6, all_403_1) = 0 & vtypeQM(all_403_16) = all_403_3 & % 50.13/7.47 | vtypeAM(all_403_12) = all_403_4 & vreduce(all_403_6, all_403_12, % 50.13/7.47 | all_403_16) = all_403_0 & vreduceExp(all_403_10, all_403_12) = % 50.13/7.47 | all_403_9 & vexpIsValue(all_403_10) = all_403_8 & visSomeExp(all_403_9) % 50.13/7.47 | = 0 & visValue(all_403_6) = all_403_5 & vqsingle(all_403_7) = all_403_6 % 50.13/7.47 | & vMC(all_403_4, all_403_3) = all_403_2 & vMC(all_403_14, all_403_13) = % 50.13/7.47 | all_403_1 & vvalue(all_403_11, all_403_15, all_403_10) = all_403_7 & % 50.13/7.47 | vAType(all_403_15) & vOptExp(all_403_9) & vQID(all_403_11) & % 50.13/7.47 | vQMap(all_403_16) & vExp(all_403_10) & vAnsMap(all_403_12) & % 50.13/7.47 | vOptQConf(all_403_0) & vQuestionnaire(all_403_6) & vATMap(all_403_3) & % 50.13/7.47 | vATMap(all_403_4) & vATMap(all_403_13) & vATMap(all_403_14) & % 50.13/7.47 | vMapConf(all_403_1) & vMapConf(all_403_2) & vEntry(all_403_7) & ! [v0: % 50.13/7.47 | vAnsMap] : ! [v1: vQMap] : ! [v2: vQuestionnaire] : ! [v3: vQConf] % 50.13/7.47 | : ( ~ (vQC(v0, v1, v2) = v3) | ~ vQMap(v1) | ~ vAnsMap(v0) | ~ % 50.13/7.47 | vQuestionnaire(v2) | ? [v4: any] : ( ~ (v4 = all_403_0) & % 50.13/7.47 | vsomeQConf(v3) = v4 & vOptQConf(v4))) % 50.13/7.47 | % 50.13/7.47 | ALPHA: (7) implies: % 50.13/7.47 | (8) ~ (all_403_8 = 0) % 50.13/7.47 | (9) vAnsMap(all_403_12) % 50.13/7.47 | (10) vExp(all_403_10) % 50.13/7.47 | (11) vQMap(all_403_16) % 50.13/7.47 | (12) vQID(all_403_11) % 50.13/7.47 | (13) vAType(all_403_15) % 50.13/7.47 | (14) vvalue(all_403_11, all_403_15, all_403_10) = all_403_7 % 50.13/7.47 | (15) vqsingle(all_403_7) = all_403_6 % 50.13/7.47 | (16) visSomeExp(all_403_9) = 0 % 50.13/7.47 | (17) vexpIsValue(all_403_10) = all_403_8 % 50.13/7.47 | (18) vreduceExp(all_403_10, all_403_12) = all_403_9 % 50.13/7.47 | (19) vreduce(all_403_6, all_403_12, all_403_16) = all_403_0 % 50.13/7.47 | (20) ! [v0: vAnsMap] : ! [v1: vQMap] : ! [v2: vQuestionnaire] : ! [v3: % 50.13/7.47 | vQConf] : ( ~ (vQC(v0, v1, v2) = v3) | ~ vQMap(v1) | ~ vAnsMap(v0) % 50.13/7.47 | | ~ vQuestionnaire(v2) | ? [v4: any] : ( ~ (v4 = all_403_0) & % 50.13/7.47 | vsomeQConf(v3) = v4 & vOptQConf(v4))) % 50.13/7.47 | % 50.13/7.47 | GROUND_INST: instantiating (1) with all_403_16, all_403_15, all_403_12, % 50.13/7.47 | all_403_11, all_403_10, all_403_7, all_403_6, all_403_0, % 50.13/7.47 | simplifying with (9), (10), (11), (12), (13), (14), (15), (19) % 50.13/7.47 | gives: % 50.13/7.47 | (21) ? [v0: any] : ? [v1: vOptExp] : ? [v2: any] : ? [v3: vExp] : ? % 50.13/7.47 | [v4: vEntry] : ? [v5: vQuestionnaire] : ? [v6: vQConf] : ? [v7: % 50.13/7.47 | vOptQConf] : (vreduceExp(all_403_10, all_403_12) = v1 & % 50.13/7.47 | vexpIsValue(all_403_10) = v0 & visSomeExp(v1) = v2 & vgetExp(v1) = % 50.13/7.47 | v3 & vQC(all_403_12, all_403_16, v5) = v6 & vsomeQConf(v6) = v7 & % 50.13/7.47 | vqsingle(v4) = v5 & vvalue(all_403_11, all_403_15, v3) = v4 & % 50.13/7.47 | vOptExp(v1) & vExp(v3) & vOptQConf(v7) & vQConf(v6) & % 50.13/7.47 | vQuestionnaire(v5) & vEntry(v4) & ( ~ (v2 = 0) | v7 = all_403_0 | v0 % 50.13/7.47 | = 0)) % 50.13/7.48 | % 50.13/7.48 | DELTA: instantiating (21) with fresh symbols all_463_0, all_463_1, all_463_2, % 50.13/7.48 | all_463_3, all_463_4, all_463_5, all_463_6, all_463_7 gives: % 50.13/7.48 | (22) vreduceExp(all_403_10, all_403_12) = all_463_6 & % 50.13/7.48 | vexpIsValue(all_403_10) = all_463_7 & visSomeExp(all_463_6) = % 50.13/7.48 | all_463_5 & vgetExp(all_463_6) = all_463_4 & vQC(all_403_12, % 50.13/7.48 | all_403_16, all_463_2) = all_463_1 & vsomeQConf(all_463_1) = % 50.13/7.48 | all_463_0 & vqsingle(all_463_3) = all_463_2 & vvalue(all_403_11, % 50.13/7.48 | all_403_15, all_463_4) = all_463_3 & vOptExp(all_463_6) & % 50.13/7.48 | vExp(all_463_4) & vOptQConf(all_463_0) & vQConf(all_463_1) & % 50.13/7.48 | vQuestionnaire(all_463_2) & vEntry(all_463_3) & ( ~ (all_463_5 = 0) | % 50.13/7.48 | all_463_0 = all_403_0 | all_463_7 = 0) % 50.13/7.48 | % 50.13/7.48 | ALPHA: (22) implies: % 50.13/7.48 | (23) vQuestionnaire(all_463_2) % 50.13/7.48 | (24) vsomeQConf(all_463_1) = all_463_0 % 50.13/7.48 | (25) vQC(all_403_12, all_403_16, all_463_2) = all_463_1 % 50.13/7.48 | (26) visSomeExp(all_463_6) = all_463_5 % 50.13/7.48 | (27) vexpIsValue(all_403_10) = all_463_7 % 50.13/7.48 | (28) vreduceExp(all_403_10, all_403_12) = all_463_6 % 50.13/7.48 | (29) ~ (all_463_5 = 0) | all_463_0 = all_403_0 | all_463_7 = 0 % 50.13/7.48 | % 50.13/7.48 | GROUND_INST: instantiating (5) with all_403_8, all_463_7, all_403_10, % 50.13/7.48 | simplifying with (17), (27) gives: % 50.13/7.48 | (30) all_463_7 = all_403_8 % 50.13/7.48 | % 50.13/7.48 | GROUND_INST: instantiating (6) with all_403_9, all_463_6, all_403_12, % 50.13/7.48 | all_403_10, simplifying with (18), (28) gives: % 50.13/7.48 | (31) all_463_6 = all_403_9 % 50.13/7.48 | % 50.13/7.48 | REDUCE: (26), (31) imply: % 50.13/7.48 | (32) visSomeExp(all_403_9) = all_463_5 % 50.13/7.48 | % 50.13/7.48 | GROUND_INST: instantiating (4) with 0, all_463_5, all_403_9, simplifying with % 50.13/7.48 | (16), (32) gives: % 50.13/7.48 | (33) all_463_5 = 0 % 50.13/7.48 | % 50.13/7.48 | BETA: splitting (29) gives: % 50.13/7.48 | % 50.13/7.48 | Case 1: % 50.13/7.48 | | % 50.13/7.48 | | (34) ~ (all_463_5 = 0) % 50.13/7.48 | | % 50.13/7.48 | | REDUCE: (33), (34) imply: % 50.13/7.48 | | (35) $false % 50.13/7.48 | | % 50.13/7.48 | | CLOSE: (35) is inconsistent. % 50.13/7.48 | | % 50.13/7.48 | Case 2: % 50.13/7.48 | | % 50.13/7.48 | | (36) all_463_0 = all_403_0 | all_463_7 = 0 % 50.13/7.48 | | % 50.13/7.48 | | BETA: splitting (36) gives: % 50.13/7.48 | | % 50.13/7.48 | | Case 1: % 50.13/7.48 | | | % 50.13/7.48 | | | (37) all_463_7 = 0 % 50.13/7.48 | | | % 50.13/7.48 | | | COMBINE_EQS: (30), (37) imply: % 50.13/7.48 | | | (38) all_403_8 = 0 % 50.13/7.48 | | | % 50.13/7.48 | | | SIMP: (38) implies: % 50.13/7.48 | | | (39) all_403_8 = 0 % 50.13/7.48 | | | % 50.13/7.48 | | | REDUCE: (8), (39) imply: % 50.13/7.48 | | | (40) $false % 50.13/7.48 | | | % 50.13/7.48 | | | CLOSE: (40) is inconsistent. % 50.13/7.48 | | | % 50.13/7.48 | | Case 2: % 50.13/7.48 | | | % 50.13/7.48 | | | (41) all_463_0 = all_403_0 % 50.13/7.48 | | | % 50.13/7.48 | | | REDUCE: (24), (41) imply: % 50.13/7.48 | | | (42) vsomeQConf(all_463_1) = all_403_0 % 50.13/7.48 | | | % 50.13/7.48 | | | GROUND_INST: instantiating (2) with all_463_2, all_403_12, all_403_16, % 50.13/7.48 | | | all_463_1, simplifying with (9), (11), (23), (25) gives: % 50.13/7.48 | | | (43) ? [v0: vQuestionnaire] : ? [v1: vOptQConf] : (vreduce(v0, % 50.13/7.48 | | | all_403_12, all_403_16) = v1 & vsomeQConf(all_463_1) = v1 & % 50.13/7.48 | | | vqseq(vqempty, all_463_2) = v0 & vOptQConf(v1) & % 50.13/7.48 | | | vQuestionnaire(v0)) % 50.13/7.48 | | | % 50.13/7.48 | | | GROUND_INST: instantiating (20) with all_403_12, all_403_16, all_463_2, % 50.13/7.48 | | | all_463_1, simplifying with (9), (11), (23), (25) gives: % 50.13/7.48 | | | (44) ? [v0: any] : ( ~ (v0 = all_403_0) & vsomeQConf(all_463_1) = v0 & % 50.13/7.48 | | | vOptQConf(v0)) % 50.13/7.48 | | | % 50.13/7.48 | | | DELTA: instantiating (44) with fresh symbol all_540_0 gives: % 50.13/7.48 | | | (45) ~ (all_540_0 = all_403_0) & vsomeQConf(all_463_1) = all_540_0 & % 50.13/7.48 | | | vOptQConf(all_540_0) % 50.13/7.48 | | | % 50.13/7.48 | | | ALPHA: (45) implies: % 50.13/7.48 | | | (46) ~ (all_540_0 = all_403_0) % 50.13/7.48 | | | (47) vsomeQConf(all_463_1) = all_540_0 % 50.13/7.48 | | | % 50.13/7.48 | | | DELTA: instantiating (43) with fresh symbols all_544_0, all_544_1 gives: % 50.13/7.48 | | | (48) vreduce(all_544_1, all_403_12, all_403_16) = all_544_0 & % 50.13/7.48 | | | vsomeQConf(all_463_1) = all_544_0 & vqseq(vqempty, all_463_2) = % 50.13/7.48 | | | all_544_1 & vOptQConf(all_544_0) & vQuestionnaire(all_544_1) % 50.13/7.48 | | | % 50.13/7.48 | | | ALPHA: (48) implies: % 50.13/7.48 | | | (49) vsomeQConf(all_463_1) = all_544_0 % 50.13/7.48 | | | % 50.13/7.48 | | | GROUND_INST: instantiating (3) with all_403_0, all_544_0, all_463_1, % 50.13/7.48 | | | simplifying with (42), (49) gives: % 50.13/7.48 | | | (50) all_544_0 = all_403_0 % 50.13/7.48 | | | % 50.13/7.48 | | | GROUND_INST: instantiating (3) with all_540_0, all_544_0, all_463_1, % 50.13/7.49 | | | simplifying with (47), (49) gives: % 50.13/7.49 | | | (51) all_544_0 = all_540_0 % 50.13/7.49 | | | % 50.13/7.49 | | | COMBINE_EQS: (50), (51) imply: % 50.13/7.49 | | | (52) all_540_0 = all_403_0 % 50.13/7.49 | | | % 50.13/7.49 | | | REDUCE: (46), (52) imply: % 50.13/7.49 | | | (53) $false % 50.13/7.49 | | | % 50.13/7.49 | | | CLOSE: (53) is inconsistent. % 50.13/7.49 | | | % 50.13/7.49 | | End of split % 50.13/7.49 | | % 50.13/7.49 | End of split % 50.13/7.49 | % 50.13/7.49 End of proof % 50.13/7.49 % SZS output end Proof for theBenchmark % 50.13/7.49 % 50.13/7.49 6822ms %------------------------------------------------------------------------------