%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM268_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 : n011.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 31.14s 4.99s % Output : Proof 44.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM268_1 : TPTP v9.3.0. Released v9.3.0. % 0.10/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.17/0.34 % Computer : n011.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon May 4 20:02:02 EDT 2026 % 0.17/0.34 % CPUTime : % 0.48/0.60 ________ _____ % 0.48/0.60 ___ __ \_________(_)________________________________ % 0.48/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.48/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.48/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.48/0.60 % 0.48/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.48/0.60 (2023-06-19) % 0.48/0.60 % 0.48/0.60 (c) Philipp Rümmer, 2009-2023 % 0.48/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.48/0.60 Amanda Stjerna. % 0.48/0.60 Free software under BSD-3-Clause. % 0.48/0.60 % 0.48/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.48/0.60 % 0.48/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.48/0.62 Running up to 7 provers in parallel. % 0.72/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.72/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.72/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.72/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.72/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.72/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.72/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 10.35/2.12 Prover 4: Preprocessing ... % 10.35/2.13 Prover 1: Preprocessing ... % 10.35/2.16 Prover 0: Preprocessing ... % 10.35/2.16 Prover 3: Preprocessing ... % 10.35/2.16 Prover 2: Preprocessing ... % 10.35/2.16 Prover 5: Preprocessing ... % 10.35/2.16 Prover 6: Preprocessing ... % 25.87/4.23 Prover 1: Warning: ignoring some quantifiers % 25.87/4.30 Prover 3: Warning: ignoring some quantifiers % 26.68/4.35 Prover 6: Proving ... % 26.68/4.36 Prover 3: Constructing countermodel ... % 26.68/4.36 Prover 1: Constructing countermodel ... % 28.11/4.56 Prover 5: Proving ... % 29.57/4.74 Prover 4: Warning: ignoring some quantifiers % 30.36/4.83 Prover 4: Constructing countermodel ... % 31.14/4.99 Prover 3: proved (4363ms) % 31.14/4.99 % 31.14/4.99 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.14/4.99 % 31.14/5.00 Prover 5: stopped % 31.14/5.00 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 31.14/5.00 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 31.14/5.01 Prover 6: stopped % 31.14/5.01 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 31.97/5.08 Prover 0: Proving ... % 31.97/5.08 Prover 0: stopped % 31.97/5.09 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 35.70/5.61 Prover 2: Proving ... % 35.70/5.61 Prover 2: stopped % 36.55/5.62 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 37.30/5.72 Prover 8: Preprocessing ... % 37.30/5.72 Prover 7: Preprocessing ... % 37.30/5.74 Prover 10: Preprocessing ... % 37.30/5.77 Prover 11: Preprocessing ... % 38.75/6.02 Prover 13: Preprocessing ... % 39.67/6.05 Prover 1: Found proof (size 54) % 39.67/6.06 Prover 1: proved (5433ms) % 39.67/6.06 Prover 4: stopped % 39.67/6.07 Prover 11: stopped % 41.01/6.23 Prover 13: stopped % 41.64/6.35 Prover 8: Warning: ignoring some quantifiers % 41.64/6.39 Prover 8: Constructing countermodel ... % 42.25/6.41 Prover 8: stopped % 42.77/6.53 Prover 10: Warning: ignoring some quantifiers % 42.77/6.58 Prover 10: Constructing countermodel ... % 42.77/6.59 Prover 7: Warning: ignoring some quantifiers % 43.27/6.60 Prover 10: stopped % 43.27/6.66 Prover 7: Constructing countermodel ... % 43.27/6.68 Prover 7: stopped % 43.27/6.68 % 43.27/6.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 43.27/6.68 % 43.78/6.70 % SZS output start Proof for theBenchmark % 43.78/6.72 Assumptions after simplification: % 43.78/6.72 --------------------------------- % 43.78/6.72 % 43.78/6.72 (Progress-qsingle-value) % 43.78/6.76 ? [v0: vQMap] : ? [v1: vAType] : ? [v2: vATMap] : ? [v3: vATMap] : ? [v4: % 43.78/6.76 vAnsMap] : ? [v5: vQID] : ? [v6: vExp] : ? [v7: vEntry] : ? [v8: % 43.78/6.76 vQuestionnaire] : ? [v9: int] : ? [v10: vATMap] : ? [v11: vATMap] : ? % 43.78/6.76 [v12: vMapConf] : ? [v13: vMapConf] : ? [v14: vOptQConf] : ( ~ (v9 = 0) & % 43.78/6.76 vptcheck(v12, v8, v13) = 0 & vtypeQM(v0) = v11 & vtypeAM(v4) = v10 & % 43.78/6.76 vreduce(v8, v4, v0) = v14 & visValue(v8) = v9 & vqsingle(v7) = v8 & vMC(v10, % 43.78/6.76 v11) = v12 & vMC(v2, v3) = v13 & vvalue(v5, v1, v6) = v7 & vAType(v1) & % 43.78/6.76 vQID(v5) & vQMap(v0) & vExp(v6) & vAnsMap(v4) & vOptQConf(v14) & % 43.78/6.76 vQuestionnaire(v8) & vATMap(v11) & vATMap(v10) & vATMap(v3) & vATMap(v2) & % 43.78/6.76 vMapConf(v13) & vMapConf(v12) & vEntry(v7) & ! [v15: vAnsMap] : ! [v16: % 43.78/6.76 vQMap] : ! [v17: vQuestionnaire] : ! [v18: vQConf] : ( ~ (vQC(v15, v16, % 43.78/6.76 v17) = v18) | ~ vQMap(v16) | ~ vAnsMap(v15) | ~ vQuestionnaire(v17) % 43.78/6.76 | ? [v19: vOptQConf] : ( ~ (v19 = v14) & vsomeQConf(v18) = v19 & % 43.78/6.76 vOptQConf(v19)))) % 43.78/6.76 % 43.78/6.76 (Progress-qsingle-value-expIsValue-False) % 43.78/6.77 ! [v0: vQMap] : ! [v1: vAType] : ! [v2: vATMap] : ! [v3: vATMap] : ! [v4: % 43.78/6.77 vAnsMap] : ! [v5: vQID] : ! [v6: vExp] : ! [v7: vEntry] : ! [v8: % 43.78/6.77 vQuestionnaire] : ! [v9: vATMap] : ! [v10: vATMap] : ! [v11: vMapConf] : % 43.78/6.77 ! [v12: vMapConf] : ( ~ (vptcheck(v11, v8, v12) = 0) | ~ (vtypeQM(v0) = v10) % 43.78/6.77 | ~ (vtypeAM(v4) = v9) | ~ (vqsingle(v7) = v8) | ~ (vMC(v9, v10) = v11) | % 43.78/6.77 ~ (vMC(v2, v3) = v12) | ~ (vvalue(v5, v1, v6) = v7) | ~ vAType(v1) | ~ % 43.78/6.77 vQID(v5) | ~ vQMap(v0) | ~ vExp(v6) | ~ vAnsMap(v4) | ~ vATMap(v3) | ~ % 43.78/6.77 vATMap(v2) | ? [v13: any] : ? [v14: any] : ? [v15: vOptQConf] : % 43.78/6.77 (vreduce(v8, v4, v0) = v15 & vexpIsValue(v6) = v13 & visValue(v8) = v14 & % 43.78/6.77 vOptQConf(v15) & (v14 = 0 | v13 = 0 | ? [v16: vAnsMap] : ? [v17: vQMap] % 43.78/6.77 : ? [v18: vQuestionnaire] : ? [v19: vQConf] : (vQC(v16, v17, v18) = % 43.78/6.77 v19 & vsomeQConf(v19) = v15 & vQMap(v17) & vAnsMap(v16) & vQConf(v19) % 43.78/6.77 & vQuestionnaire(v18))))) % 43.78/6.77 % 43.78/6.77 (Progress-qsingle-value-expIsValue-True) % 43.78/6.77 ! [v0: vQMap] : ! [v1: vAType] : ! [v2: vATMap] : ! [v3: vATMap] : ! [v4: % 43.78/6.77 vAnsMap] : ! [v5: vQID] : ! [v6: vExp] : ! [v7: vEntry] : ! [v8: % 43.78/6.77 vQuestionnaire] : ! [v9: vATMap] : ! [v10: vATMap] : ! [v11: vMapConf] : % 43.78/6.77 ! [v12: vMapConf] : ( ~ (vptcheck(v11, v8, v12) = 0) | ~ (vtypeQM(v0) = v10) % 43.78/6.77 | ~ (vtypeAM(v4) = v9) | ~ (vqsingle(v7) = v8) | ~ (vMC(v9, v10) = v11) | % 43.78/6.77 ~ (vMC(v2, v3) = v12) | ~ (vvalue(v5, v1, v6) = v7) | ~ vAType(v1) | ~ % 43.78/6.77 vQID(v5) | ~ vQMap(v0) | ~ vExp(v6) | ~ vAnsMap(v4) | ~ vATMap(v3) | ~ % 43.78/6.77 vATMap(v2) | ? [v13: any] : ? [v14: any] : ? [v15: vOptQConf] : % 43.78/6.77 (vreduce(v8, v4, v0) = v15 & vexpIsValue(v6) = v13 & visValue(v8) = v14 & % 43.78/6.77 vOptQConf(v15) & ( ~ (v13 = 0) | v14 = 0 | ? [v16: vAnsMap] : ? [v17: % 43.78/6.77 vQMap] : ? [v18: vQuestionnaire] : ? [v19: vQConf] : (vQC(v16, v17, % 43.78/6.77 v18) = v19 & vsomeQConf(v19) = v15 & vQMap(v17) & vAnsMap(v16) & % 43.78/6.77 vQConf(v19) & vQuestionnaire(v18))))) % 43.78/6.77 % 43.78/6.77 (Tqempty_inv2) % 43.78/6.78 vQuestionnaire(vqempty) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vATMap] % 43.78/6.78 : ! [v3: vATMap] : ! [v4: vMapConf] : ! [v5: vMapConf] : (v3 = v1 | ~ % 43.78/6.78 (vptcheck(v4, vqempty, v5) = 0) | ~ (vMC(v2, v3) = v5) | ~ (vMC(v0, v1) = % 43.78/6.78 v4) | ~ vATMap(v3) | ~ vATMap(v2) | ~ vATMap(v1) | ~ vATMap(v0)) % 43.78/6.78 % 43.78/6.78 (reduce-2) % 43.78/6.78 vQuestionnaire(vqempty) & ! [v0: vQMap] : ! [v1: vAType] : ! [v2: vAnsMap] % 43.78/6.78 : ! [v3: vQID] : ! [v4: vExp] : ! [v5: vEntry] : ! [v6: vQuestionnaire] : % 43.78/6.78 ! [v7: vOptQConf] : ( ~ (vreduce(v6, v2, v0) = v7) | ~ (vqsingle(v5) = v6) | % 43.78/6.78 ~ (vvalue(v3, v1, v4) = v5) | ~ vAType(v1) | ~ vQID(v3) | ~ vQMap(v0) | % 43.78/6.78 ~ vExp(v4) | ~ vAnsMap(v2) | ? [v8: any] : ? [v9: vAval] : ? [v10: % 43.78/6.78 vAnsMap] : ? [v11: vQConf] : ? [v12: vOptQConf] : (vexpIsValue(v4) = v8 % 43.78/6.78 & vgetExpValue(v4) = v9 & vQC(v10, v0, vqempty) = v11 & vabind(v3, v9, v2) % 43.78/6.78 = v10 & vsomeQConf(v11) = v12 & vAnsMap(v10) & vOptQConf(v12) & vAval(v9) % 43.78/6.78 & vQConf(v11) & ( ~ (v8 = 0) | v12 = v7))) % 43.78/6.78 % 43.78/6.78 (function-axioms) % 44.24/6.82 ! [v0: vQMap] : ! [v1: vQMap] : ! [v2: vQMap] : ! [v3: vAType] : ! [v4: % 44.24/6.82 vLabel] : ! [v5: vQID] : (v1 = v0 | ~ (vqmbind(v5, v4, v3, v2) = v1) | ~ % 44.24/6.82 (vqmbind(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 44.24/6.82 MultipleValueBool] : ! [v2: vMapConf] : ! [v3: vQuestionnaire] : ! [v4: % 44.24/6.82 vMapConf] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) | ~ (vptcheck(v4, v3, % 44.24/6.82 v2) = v0)) & ! [v0: vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : % 44.24/6.82 ! [v3: vAType] : ! [v4: vBinOpT] : (v1 = v0 | ~ (vcheckBinOp(v4, v3, v2) = % 44.24/6.82 v1) | ~ (vcheckBinOp(v4, v3, v2) = v0)) & ! [v0: vOptQConf] : ! [v1: % 44.24/6.82 vOptQConf] : ! [v2: vQMap] : ! [v3: vAnsMap] : ! [v4: vQuestionnaire] : % 44.24/6.82 (v1 = v0 | ~ (vreduce(v4, v3, v2) = v1) | ~ (vreduce(v4, v3, v2) = v0)) & ! % 44.24/6.82 [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vAval] : ! [v4: % 44.24/6.82 vBinOpT] : (v1 = v0 | ~ (vevalBinOp(v4, v3, v2) = v1) | ~ (vevalBinOp(v4, % 44.24/6.82 v3, v2) = v0)) & ! [v0: vQConf] : ! [v1: vQConf] : ! [v2: % 44.24/6.82 vQuestionnaire] : ! [v3: vQMap] : ! [v4: vAnsMap] : (v1 = v0 | ~ (vQC(v4, % 44.24/6.82 v3, v2) = v1) | ~ (vQC(v4, v3, v2) = v0)) & ! [v0: vATMap] : ! [v1: % 44.24/6.82 vATMap] : ! [v2: vATMap] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ % 44.24/6.82 (vatmbind(v4, v3, v2) = v1) | ~ (vatmbind(v4, v3, v2) = v0)) & ! [v0: % 44.24/6.82 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vAType] : ! [v3: vLabel] : % 44.24/6.82 ! [v4: vQID] : (v1 = v0 | ~ (vsomeQuestion(v4, v3, v2) = v1) | ~ % 44.24/6.82 (vsomeQuestion(v4, v3, v2) = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! % 44.24/6.82 [v2: vAnsMap] : ! [v3: vAval] : ! [v4: vQID] : (v1 = v0 | ~ (vabind(v4, v3, % 44.24/6.82 v2) = v1) | ~ (vabind(v4, v3, v2) = v0)) & ! [v0: vQuestionnaire] : ! % 44.24/6.82 [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! [v3: vQuestionnaire] : ! % 44.24/6.82 [v4: vExp] : (v1 = v0 | ~ (vqcond(v4, v3, v2) = v1) | ~ (vqcond(v4, v3, v2) % 44.24/6.82 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: vBinOpT] % 44.24/6.82 : ! [v4: vExp] : (v1 = v0 | ~ (vbinop(v4, v3, v2) = v1) | ~ (vbinop(v4, v3, % 44.24/6.82 v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! [v2: vAType] : ! % 44.24/6.82 [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ (vdefquestion(v4, v3, v2) = v1) | % 44.24/6.82 ~ (vdefquestion(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: vEntry] : ! % 44.24/6.82 [v2: vExp] : ! [v3: vAType] : ! [v4: vQID] : (v1 = v0 | ~ (vvalue(v4, v3, % 44.24/6.82 v2) = v1) | ~ (vvalue(v4, v3, v2) = v0)) & ! [v0: vEntry] : ! [v1: % 44.24/6.82 vEntry] : ! [v2: vAType] : ! [v3: vLabel] : ! [v4: vQID] : (v1 = v0 | ~ % 44.24/6.82 (vquestion(v4, v3, v2) = v1) | ~ (vquestion(v4, v3, v2) = v0)) & ! [v0: % 44.24/6.82 vOptAType] : ! [v1: vOptAType] : ! [v2: vExp] : ! [v3: vATMap] : (v1 = v0 % 44.24/6.82 | ~ (vecheck(v3, v2) = v1) | ~ (vecheck(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : ! [v3: vUnOpT] : (v1 = % 44.24/6.82 v0 | ~ (vcheckUnOp(v3, v2) = v1) | ~ (vcheckUnOp(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 44.24/6.82 ~ (vintersectATM(v3, v2) = v1) | ~ (vintersectATM(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vATMap] : ! [v1: vATMap] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = v0 | % 44.24/6.82 ~ (vappendATMap(v3, v2) = v1) | ~ (vappendATMap(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vOptAType] : ! [v1: vOptAType] : ! [v2: vATMap] : ! [v3: vQID] : (v1 = v0 % 44.24/6.82 | ~ (vlookupATMap(v3, v2) = v1) | ~ (vlookupATMap(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vOptExp] : ! [v1: vOptExp] : ! [v2: vAnsMap] : ! [v3: vExp] : (v1 = v0 | % 44.24/6.82 ~ (vreduceExp(v3, v2) = v1) | ~ (vreduceExp(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vOptExp] : ! [v1: vOptExp] : ! [v2: vAval] : ! [v3: vUnOpT] : (v1 = v0 | % 44.24/6.82 ~ (vevalUnOp(v3, v2) = v1) | ~ (vevalUnOp(v3, v2) = v0)) & ! [v0: vAval] : % 44.24/6.82 ! [v1: vAval] : ! [v2: vAType] : ! [v3: vLabel] : (v1 = v0 | ~ % 44.24/6.82 (vgetAnswer(v3, v2) = v1) | ~ (vgetAnswer(v3, v2) = v0)) & ! [v0: vQConf] % 44.24/6.82 : ! [v1: vQConf] : ! [v2: vQuestionnaire] : ! [v3: vQConf] : (v1 = v0 | ~ % 44.24/6.82 (vqcappend(v3, v2) = v1) | ~ (vqcappend(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vOptQuestion] : ! [v1: vOptQuestion] : ! [v2: vQMap] : ! [v3: vQID] : (v1 % 44.24/6.82 = v0 | ~ (vlookupQMap(v3, v2) = v1) | ~ (vlookupQMap(v3, v2) = v0)) & ! % 44.24/6.82 [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vAnsMap] : ! [v3: vAnsMap] : (v1 = % 44.24/6.82 v0 | ~ (vappendAnsMap(v3, v2) = v1) | ~ (vappendAnsMap(v3, v2) = v0)) & ! % 44.24/6.82 [v0: vOptAval] : ! [v1: vOptAval] : ! [v2: vAnsMap] : ! [v3: vQID] : (v1 = % 44.24/6.82 v0 | ~ (vlookupAnsMap(v3, v2) = v1) | ~ (vlookupAnsMap(v3, v2) = v0)) & ! % 44.24/6.82 [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vATList] : (v1 = % 44.24/6.82 v0 | ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vnat] % 44.24/6.82 : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vdivide(v3, % 44.24/6.82 v2) = v1) | ~ (vdivide(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : % 44.24/6.82 ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vmultiply(v3, v2) = v1) | ~ % 44.24/6.82 (vmultiply(v3, v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : % 44.24/6.82 ! [v3: vnat] : (v1 = v0 | ~ (vminus(v3, v2) = v1) | ~ (vminus(v3, v2) = v0)) % 44.24/6.82 & ! [v0: vnat] : ! [v1: vnat] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | % 44.24/6.82 ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: % 44.24/6.82 vYN] : ! [v2: vnat] : ! [v3: vnat] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 44.24/6.82 (vlt(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vnat] : ! [v3: % 44.24/6.82 vnat] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vYN] : ! [v1: vYN] : ! [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vor(v3, % 44.24/6.82 v2) = v1) | ~ (vor(v3, v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! % 44.24/6.82 [v2: vYN] : ! [v3: vYN] : (v1 = v0 | ~ (vand(v3, v2) = v1) | ~ (vand(v3, % 44.24/6.82 v2) = v0)) & ! [v0: vstring] : ! [v1: vstring] : ! [v2: vstring] : ! % 44.24/6.82 [v3: vchar] : (v1 = v0 | ~ (vscons(v3, v2) = v1) | ~ (vscons(v3, v2) = v0)) % 44.24/6.82 & ! [v0: vATList] : ! [v1: vATList] : ! [v2: vATList] : ! [v3: vAType] : % 44.24/6.82 (v1 = v0 | ~ (vatcons(v3, v2) = v1) | ~ (vatcons(v3, v2) = v0)) & ! [v0: % 44.24/6.82 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] : ! % 44.24/6.82 [v3: vGID] : (v1 = v0 | ~ (vqgroup(v3, v2) = v1) | ~ (vqgroup(v3, v2) = v0)) % 44.24/6.82 & ! [v0: vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQuestionnaire] % 44.24/6.82 : ! [v3: vQuestionnaire] : (v1 = v0 | ~ (vqseq(v3, v2) = v1) | ~ (vqseq(v3, % 44.24/6.82 v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vExp] : ! [v3: % 44.24/6.82 vUnOpT] : (v1 = v0 | ~ (vunop(v3, v2) = v1) | ~ (vunop(v3, v2) = v0)) & ! % 44.24/6.82 [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vATMap] : ! [v3: vATMap] : (v1 = % 44.24/6.82 v0 | ~ (vMC(v3, v2) = v1) | ~ (vMC(v3, v2) = v0)) & ! [v0: vATMap] : ! % 44.24/6.82 [v1: vATMap] : ! [v2: vQMap] : (v1 = v0 | ~ (vtypeQM(v2) = v1) | ~ % 44.24/6.82 (vtypeQM(v2) = v0)) & ! [v0: vATMap] : ! [v1: vATMap] : ! [v2: vAnsMap] : % 44.24/6.82 (v1 = v0 | ~ (vtypeAM(v2) = v1) | ~ (vtypeAM(v2) = v0)) & ! [v0: % 44.24/6.82 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptMapConf] : (v1 % 44.24/6.82 = v0 | ~ (visSomeMapConf(v2) = v1) | ~ (visSomeMapConf(v2) = v0)) & ! % 44.24/6.82 [v0: vstring] : ! [v1: vstring] : ! [v2: vLabel] : (v1 = v0 | ~ % 44.24/6.82 (vaskText(v2) = v1) | ~ (vaskText(v2) = v0)) & ! [v0: vnat] : ! [v1: % 44.24/6.82 vnat] : ! [v2: vLabel] : (v1 = v0 | ~ (vaskNumber(v2) = v1) | ~ % 44.24/6.82 (vaskNumber(v2) = v0)) & ! [v0: vYN] : ! [v1: vYN] : ! [v2: vLabel] : (v1 % 44.24/6.82 = v0 | ~ (vaskYesNo(v2) = v1) | ~ (vaskYesNo(v2) = v0)) & ! [v0: % 44.24/6.82 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] : (v1 = v0 | % 44.24/6.82 ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) & ! [v0: % 44.24/6.82 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptExp] : (v1 = % 44.24/6.82 v0 | ~ (visSomeExp(v2) = v1) | ~ (visSomeExp(v2) = v0)) & ! [v0: % 44.24/6.82 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQConf] : (v1 = % 44.24/6.82 v0 | ~ (visSomeQC(v2) = v1) | ~ (visSomeQC(v2) = v0)) & ! [v0: % 44.24/6.82 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuestionnaire] : % 44.24/6.82 (v1 = v0 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 44.24/6.82 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vQConf] : (v1 = v0 | ~ % 44.24/6.82 (vgetQuest(v2) = v1) | ~ (vgetQuest(v2) = v0)) & ! [v0: vQMap] : ! [v1: % 44.24/6.82 vQMap] : ! [v2: vQConf] : (v1 = v0 | ~ (vgetQM(v2) = v1) | ~ (vgetQM(v2) % 44.24/6.82 = v0)) & ! [v0: vAnsMap] : ! [v1: vAnsMap] : ! [v2: vQConf] : (v1 = v0 % 44.24/6.82 | ~ (vgetAM(v2) = v1) | ~ (vgetAM(v2) = v0)) & ! [v0: MultipleValueBool] % 44.24/6.82 : ! [v1: MultipleValueBool] : ! [v2: vOptQuestion] : (v1 = v0 | ~ % 44.24/6.82 (visSomeQuestion(v2) = v1) | ~ (visSomeQuestion(v2) = v0)) & ! [v0: % 44.24/6.82 vAType] : ! [v1: vAType] : ! [v2: vAval] : (v1 = v0 | ~ (vtypeOf(v2) = % 44.24/6.82 v1) | ~ (vtypeOf(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 44.24/6.82 MultipleValueBool] : ! [v2: vOptAType] : (v1 = v0 | ~ (visSomeAType(v2) = % 44.24/6.82 v1) | ~ (visSomeAType(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 44.24/6.82 MultipleValueBool] : ! [v2: vOptAval] : (v1 = v0 | ~ (visSomeAval(v2) = % 44.24/6.82 v1) | ~ (visSomeAval(v2) = v0)) & ! [v0: vnat] : ! [v1: vnat] : ! [v2: % 44.24/6.82 vnat] : (v1 = v0 | ~ (vpred(v2) = v1) | ~ (vpred(v2) = v0)) & ! [v0: vYN] % 44.24/6.82 : ! [v1: vYN] : ! [v2: vYN] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) = % 44.24/6.82 v0)) & ! [v0: vMapConf] : ! [v1: vMapConf] : ! [v2: vOptMapConf] : (v1 % 44.24/6.82 = v0 | ~ (vgetMapConf(v2) = v1) | ~ (vgetMapConf(v2) = v0)) & ! [v0: % 44.24/6.82 vAval] : ! [v1: vAval] : ! [v2: vExp] : (v1 = v0 | ~ (vgetExpValue(v2) = % 44.24/6.82 v1) | ~ (vgetExpValue(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 44.24/6.82 [v2: vOptExp] : (v1 = v0 | ~ (vgetExp(v2) = v1) | ~ (vgetExp(v2) = v0)) & ! % 44.24/6.82 [v0: vQConf] : ! [v1: vQConf] : ! [v2: vOptQConf] : (v1 = v0 | ~ % 44.24/6.82 (vgetQC(v2) = v1) | ~ (vgetQC(v2) = v0)) & ! [v0: vAType] : ! [v1: % 44.24/6.82 vAType] : ! [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionAType(v2) = v1) % 44.24/6.82 | ~ (vgetQuestionAType(v2) = v0)) & ! [v0: vLabel] : ! [v1: vLabel] : ! % 44.24/6.82 [v2: vOptQuestion] : (v1 = v0 | ~ (vgetQuestionLabel(v2) = v1) | ~ % 44.24/6.82 (vgetQuestionLabel(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: % 44.24/6.82 vOptQuestion] : (v1 = v0 | ~ (vgetQuestionQID(v2) = v1) | ~ % 44.24/6.82 (vgetQuestionQID(v2) = v0)) & ! [v0: vAType] : ! [v1: vAType] : ! [v2: % 44.24/6.82 vOptAType] : (v1 = v0 | ~ (vgetAType(v2) = v1) | ~ (vgetAType(v2) = v0)) & % 44.24/6.82 ! [v0: vAval] : ! [v1: vAval] : ! [v2: vOptAval] : (v1 = v0 | ~ % 44.24/6.82 (vgetAval(v2) = v1) | ~ (vgetAval(v2) = v0)) & ! [v0: vOptAval] : ! [v1: % 44.24/6.82 vOptAval] : ! [v2: vAval] : (v1 = v0 | ~ (vsomeAval(v2) = v1) | ~ % 44.24/6.82 (vsomeAval(v2) = v0)) & ! [v0: vQID] : ! [v1: vQID] : ! [v2: vQID] : (v1 % 44.24/6.82 = v0 | ~ (venumQID(v2) = v1) | ~ (venumQID(v2) = v0)) & ! [v0: % 44.24/6.82 vOptMapConf] : ! [v1: vOptMapConf] : ! [v2: vMapConf] : (v1 = v0 | ~ % 44.24/6.82 (vsomeMapConf(v2) = v1) | ~ (vsomeMapConf(v2) = v0)) & ! [v0: vGID] : ! % 44.24/6.82 [v1: vGID] : ! [v2: vGID] : (v1 = v0 | ~ (venumGID(v2) = v1) | ~ % 44.24/6.82 (venumGID(v2) = v0)) & ! [v0: vOptExp] : ! [v1: vOptExp] : ! [v2: vExp] : % 44.24/6.82 (v1 = v0 | ~ (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) & ! [v0: vAval] : % 44.24/6.82 ! [v1: vAval] : ! [v2: vstring] : (v1 = v0 | ~ (vT(v2) = v1) | ~ (vT(v2) = % 44.24/6.82 v0)) & ! [v0: vAval] : ! [v1: vAval] : ! [v2: vnat] : (v1 = v0 | ~ % 44.24/6.82 (vNum(v2) = v1) | ~ (vNum(v2) = v0)) & ! [v0: vAval] : ! [v1: vAval] : ! % 44.24/6.82 [v2: vYN] : (v1 = v0 | ~ (vB(v2) = v1) | ~ (vB(v2) = v0)) & ! [v0: % 44.24/6.82 vOptAType] : ! [v1: vOptAType] : ! [v2: vAType] : (v1 = v0 | ~ % 44.24/6.82 (vsomeAType(v2) = v1) | ~ (vsomeAType(v2) = v0)) & ! [v0: vOptQConf] : ! % 44.24/6.82 [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | ~ (vsomeQConf(v2) = v1) | ~ % 44.24/6.82 (vsomeQConf(v2) = v0)) & ! [v0: vchar] : ! [v1: vchar] : ! [v2: vchar] : % 44.24/6.82 (v1 = v0 | ~ (venumchar(v2) = v1) | ~ (venumchar(v2) = v0)) & ! [v0: % 44.24/6.82 vQuestionnaire] : ! [v1: vQuestionnaire] : ! [v2: vEntry] : (v1 = v0 | ~ % 44.24/6.82 (vqsingle(v2) = v1) | ~ (vqsingle(v2) = v0)) & ! [v0: vnat] : ! [v1: % 44.24/6.83 vnat] : ! [v2: vnat] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = % 44.24/6.83 v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vQID] : (v1 = v0 | ~ % 44.24/6.83 (vqvar(v2) = v1) | ~ (vqvar(v2) = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! % 44.24/6.83 [v2: vAval] : (v1 = v0 | ~ (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & % 44.24/6.83 ! [v0: vLabel] : ! [v1: vLabel] : ! [v2: vLabel] : (v1 = v0 | ~ % 44.24/6.83 (venumLabel(v2) = v1) | ~ (venumLabel(v2) = v0)) & ! [v0: vEntry] : ! % 44.24/6.83 [v1: vEntry] : ! [v2: vQID] : (v1 = v0 | ~ (vask(v2) = v1) | ~ (vask(v2) = % 44.24/6.83 v0)) % 44.24/6.83 % 44.24/6.83 Further assumptions not needed in the proof: % 44.24/6.83 -------------------------------------------- % 44.24/6.83 DIFF-B-Num, DIFF-B-T, DIFF-Num-T, DIFF-Number-Text, DIFF-YesNo-Number, % 44.24/6.83 DIFF-YesNo-Text, DIFF-addop-andop, DIFF-addop-divop, DIFF-addop-eqop, % 44.24/6.83 DIFF-addop-gtop, DIFF-addop-ltop, DIFF-addop-mulop, DIFF-addop-orop, % 44.24/6.83 DIFF-addop-subop, DIFF-aempty-abind, DIFF-andop-orop, DIFF-atempty-atcons, % 44.24/6.83 DIFF-atmempty-atmbind, DIFF-binop-unop, DIFF-constant-binop, DIFF-constant-qvar, % 44.24/6.83 DIFF-constant-unop, DIFF-defquestion-ask, DIFF-divop-andop, DIFF-divop-eqop, % 44.24/6.83 DIFF-divop-gtop, DIFF-divop-ltop, DIFF-divop-orop, DIFF-eqop-andop, % 44.24/6.83 DIFF-eqop-gtop, DIFF-eqop-ltop, DIFF-eqop-orop, DIFF-gtop-andop, DIFF-gtop-ltop, % 44.24/6.83 DIFF-gtop-orop, DIFF-initGID-enumGID, DIFF-initLabel-enumLabel, % 44.24/6.83 DIFF-initQID-enumQID, DIFF-initchar-enumchar, DIFF-ltop-andop, DIFF-ltop-orop, % 44.24/6.83 DIFF-mulop-andop, DIFF-mulop-divop, DIFF-mulop-eqop, DIFF-mulop-gtop, % 44.24/6.83 DIFF-mulop-ltop, DIFF-mulop-orop, DIFF-noAType-someAType, DIFF-noAval-someAval, % 44.24/6.83 DIFF-noExp-someExp, DIFF-noMapConf-someMapConf, DIFF-noQConf-someQConf, % 44.24/6.83 DIFF-noQuestion-someQuestion, DIFF-qcond-qgroup, DIFF-qempty-qcond, % 44.24/6.83 DIFF-qempty-qgroup, DIFF-qempty-qseq, DIFF-qempty-qsingle, DIFF-qmempty-qmbind, % 44.24/6.83 DIFF-qseq-qcond, DIFF-qseq-qgroup, DIFF-qsingle-qcond, DIFF-qsingle-qgroup, % 44.24/6.83 DIFF-qsingle-qseq, DIFF-question-ask, DIFF-question-defquestion, % 44.24/6.83 DIFF-question-value, DIFF-qvar-binop, DIFF-qvar-unop, DIFF-sempty-scons, % 44.24/6.83 DIFF-subop-andop, DIFF-subop-divop, DIFF-subop-eqop, DIFF-subop-gtop, % 44.24/6.83 DIFF-subop-ltop, DIFF-subop-mulop, DIFF-subop-orop, DIFF-value-ask, % 44.24/6.83 DIFF-value-defquestion, DIFF-yes-no, DIFF-zero-succ, EQ-B, EQ-MC, EQ-Num, EQ-QC, % 44.24/6.83 EQ-T, EQ-abind, EQ-ask, EQ-atcons, EQ-atmbind, EQ-binop, EQ-constant, % 44.24/6.83 EQ-defquestion, EQ-enumGID, EQ-enumLabel, EQ-enumQID, EQ-enumchar, EQ-qcond, % 44.24/6.83 EQ-qgroup, EQ-qmbind, EQ-qseq, EQ-qsingle, EQ-question, EQ-qvar, EQ-scons, % 44.24/6.83 EQ-someAType, EQ-someAval, EQ-someExp, EQ-someMapConf, EQ-someQConf, % 44.24/6.83 EQ-someQuestion, EQ-succ, EQ-unop, EQ-value, Task, Task_inv1, Task_inv2, % 44.24/6.83 Task_inv3, Task_inv4, Tdefquestion, Tdefquestion_inv1, Tdefquestion_inv2, % 44.24/6.83 Tdefquestion_inv3, Tqcond, Tqcond_inv1, Tqcond_inv2, Tqcond_inv3, Tqcond_inv4, % 44.24/6.83 Tqcond_inv5, Tqcond_inv6, Tqcond_inv7, Tqempty, Tqempty_inv1, Tqgroup, % 44.24/6.83 Tqgroup_inv, Tqseq, Tqseq_inv1, Tqseq_inv2, Tqseq_inv3, Tqseq_inv4, Tquestion, % 44.24/6.83 Tquestion_inv1, Tquestion_inv2, Tquestion_inv3, Tvalue, Tvalue_inv1, % 44.24/6.83 Tvalue_inv2, Tvalue_inv3, Tvalue_inv4, and-0, and-1, and-INV, append-0, % 44.24/6.83 append-1, append-INV, appendATMap-0, appendATMap-1, appendATMap-INV, % 44.24/6.83 appendAnsMap-0, appendAnsMap-1, appendAnsMap-INV, checkBinOp-0, checkBinOp-1, % 44.24/6.83 checkBinOp-2, checkBinOp-3, checkBinOp-4, checkBinOp-5, checkBinOp-6, % 44.24/6.83 checkBinOp-7, checkBinOp-8, checkBinOp-9, checkBinOp-INV, checkUnOp-0, % 44.24/6.83 checkUnOp-1, checkUnOp-INV, divide-0, divide-1, divide-INV, dom-ATList, % 44.24/6.83 dom-ATMap, dom-AType, dom-AnsMap, dom-Aval, dom-BinOpT, dom-Entry, dom-Exp, % 44.24/6.83 dom-MapConf, dom-OptAType, dom-OptAval, dom-OptExp, dom-OptMapConf, % 44.24/6.83 dom-OptQConf, dom-OptQuestion, dom-QConf, dom-QMap, dom-Questionnaire, % 44.24/6.83 dom-UnOpT, dom-YN, dom-nat, dom-string, echeck-0, echeck-1, echeck-2, echeck-3, % 44.24/6.83 echeck-4, echeck-5, echeck-6, echeck-7, echeck-INV, evalBinOp-0, evalBinOp-1, % 44.24/6.83 evalBinOp-10, evalBinOp-2, evalBinOp-3, evalBinOp-4, evalBinOp-5, evalBinOp-6, % 44.24/6.83 evalBinOp-7, evalBinOp-8, evalBinOp-9, evalBinOp-INV, evalUnOp-0, evalUnOp-1, % 44.24/6.83 evalUnOp-INV, expIsValue-0, expIsValue-1, expIsValue-false-INV, % 44.24/6.83 expIsValue-true-INV, getAM-0, getAM-INV, getAType-0, getAnswer-0, getAnswer-1, % 44.24/6.83 getAnswer-2, getAnswer-INV, getAval-0, getExp-0, getExpValue-0, getMapConf-0, % 44.24/6.83 getQC-0, getQM-0, getQM-INV, getQuest-0, getQuest-INV, getQuestionAType-0, % 44.24/6.83 getQuestionLabel-0, getQuestionQID-0, gt-0, gt-1, gt-2, gt-INV, intersectATM-0, % 44.24/6.83 intersectATM-1, intersectATM-2, intersectATM-INV, isSomeAType-0, isSomeAType-1, % 44.24/6.83 isSomeAType-false-INV, isSomeAType-true-INV, isSomeAval-0, isSomeAval-1, % 44.24/6.83 isSomeAval-false-INV, isSomeAval-true-INV, isSomeExp-0, isSomeExp-1, % 44.24/6.83 isSomeExp-false-INV, isSomeExp-true-INV, isSomeMapConf-0, isSomeMapConf-1, % 44.24/6.83 isSomeMapConf-false-INV, isSomeMapConf-true-INV, isSomeQC-0, isSomeQC-1, % 44.24/6.83 isSomeQC-false-INV, isSomeQC-true-INV, isSomeQuestion-0, isSomeQuestion-1, % 44.24/6.83 isSomeQuestion-false-INV, isSomeQuestion-true-INV, isValue-0, isValue-1, % 44.24/6.83 isValue-false-INV, isValue-true-INV, lookupATMap-0, lookupATMap-1, % 44.24/6.83 lookupATMap-2, lookupATMap-INV, lookupAnsMap-0, lookupAnsMap-1, lookupAnsMap-2, % 44.24/6.83 lookupAnsMap-INV, lookupQMap-0, lookupQMap-1, lookupQMap-2, lookupQMap-INV, % 44.24/6.83 lt-0, lt-1, lt-2, lt-INV, minus-0, minus-1, minus-INV, multiply-0, multiply-1, % 44.24/6.83 multiply-INV, not-0, not-1, not-INV, or-0, or-1, or-INV, plus-0, plus-1, % 44.24/6.83 plus-INV, pred-0, pred-1, pred-INV, qcappend-0, qcappend-INV, reduce-0, % 44.24/6.83 reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, % 44.24/6.83 reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, reduce-8, reduce-9, % 44.24/6.83 reduce-INV, reduceExp-0, reduceExp-1, reduceExp-10, reduceExp-2, reduceExp-3, % 44.24/6.83 reduceExp-4, reduceExp-5, reduceExp-6, reduceExp-7, reduceExp-8, reduceExp-9, % 44.24/6.83 reduceExp-INV, typeAM-0, typeAM-1, typeAM-INV, typeOf-0, typeOf-1, typeOf-2, % 44.24/6.83 typeOf-INV, typeQM-0, typeQM-1, typeQM-INV % 44.24/6.83 % 44.24/6.83 Those formulas are unsatisfiable: % 44.24/6.83 --------------------------------- % 44.24/6.83 % 44.24/6.83 Begin of proof % 44.24/6.83 | % 44.24/6.83 | ALPHA: (reduce-2) implies: % 44.24/6.83 | (1) ! [v0: vQMap] : ! [v1: vAType] : ! [v2: vAnsMap] : ! [v3: vQID] : % 44.24/6.83 | ! [v4: vExp] : ! [v5: vEntry] : ! [v6: vQuestionnaire] : ! [v7: % 44.24/6.83 | vOptQConf] : ( ~ (vreduce(v6, v2, v0) = v7) | ~ (vqsingle(v5) = v6) % 44.24/6.83 | | ~ (vvalue(v3, v1, v4) = v5) | ~ vAType(v1) | ~ vQID(v3) | ~ % 44.24/6.83 | vQMap(v0) | ~ vExp(v4) | ~ vAnsMap(v2) | ? [v8: any] : ? [v9: % 44.24/6.83 | vAval] : ? [v10: vAnsMap] : ? [v11: vQConf] : ? [v12: vOptQConf] % 44.24/6.83 | : (vexpIsValue(v4) = v8 & vgetExpValue(v4) = v9 & vQC(v10, v0, % 44.24/6.83 | vqempty) = v11 & vabind(v3, v9, v2) = v10 & vsomeQConf(v11) = v12 % 44.24/6.83 | & vAnsMap(v10) & vOptQConf(v12) & vAval(v9) & vQConf(v11) & ( ~ (v8 % 44.24/6.83 | = 0) | v12 = v7))) % 44.24/6.83 | % 44.24/6.83 | ALPHA: (Tqempty_inv2) implies: % 44.24/6.83 | (2) vQuestionnaire(vqempty) % 44.24/6.83 | % 44.24/6.83 | ALPHA: (function-axioms) implies: % 44.24/6.84 | (3) ! [v0: vOptQConf] : ! [v1: vOptQConf] : ! [v2: vQConf] : (v1 = v0 | % 44.24/6.84 | ~ (vsomeQConf(v2) = v1) | ~ (vsomeQConf(v2) = v0)) % 44.24/6.84 | (4) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 44.24/6.84 | vQuestionnaire] : (v1 = v0 | ~ (visValue(v2) = v1) | ~ % 44.24/6.84 | (visValue(v2) = v0)) % 44.24/6.84 | (5) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vExp] % 44.24/6.84 | : (v1 = v0 | ~ (vexpIsValue(v2) = v1) | ~ (vexpIsValue(v2) = v0)) % 44.24/6.84 | (6) ! [v0: vOptQConf] : ! [v1: vOptQConf] : ! [v2: vQMap] : ! [v3: % 44.24/6.84 | vAnsMap] : ! [v4: vQuestionnaire] : (v1 = v0 | ~ (vreduce(v4, v3, % 44.24/6.84 | v2) = v1) | ~ (vreduce(v4, v3, v2) = v0)) % 44.24/6.84 | % 44.24/6.84 | DELTA: instantiating (Progress-qsingle-value) with fresh symbols all_406_0, % 44.24/6.84 | all_406_1, all_406_2, all_406_3, all_406_4, all_406_5, all_406_6, % 44.24/6.84 | all_406_7, all_406_8, all_406_9, all_406_10, all_406_11, all_406_12, % 44.24/6.84 | all_406_13, all_406_14 gives: % 44.24/6.84 | (7) ~ (all_406_5 = 0) & vptcheck(all_406_2, all_406_6, all_406_1) = 0 & % 44.24/6.84 | vtypeQM(all_406_14) = all_406_3 & vtypeAM(all_406_10) = all_406_4 & % 44.24/6.84 | vreduce(all_406_6, all_406_10, all_406_14) = all_406_0 & % 44.24/6.84 | visValue(all_406_6) = all_406_5 & vqsingle(all_406_7) = all_406_6 & % 44.24/6.84 | vMC(all_406_4, all_406_3) = all_406_2 & vMC(all_406_12, all_406_11) = % 44.24/6.84 | all_406_1 & vvalue(all_406_9, all_406_13, all_406_8) = all_406_7 & % 44.24/6.84 | vAType(all_406_13) & vQID(all_406_9) & vQMap(all_406_14) & % 44.24/6.84 | vExp(all_406_8) & vAnsMap(all_406_10) & vOptQConf(all_406_0) & % 44.24/6.84 | vQuestionnaire(all_406_6) & vATMap(all_406_3) & vATMap(all_406_4) & % 44.24/6.84 | vATMap(all_406_11) & vATMap(all_406_12) & vMapConf(all_406_1) & % 44.24/6.84 | vMapConf(all_406_2) & vEntry(all_406_7) & ! [v0: vAnsMap] : ! [v1: % 44.24/6.84 | vQMap] : ! [v2: vQuestionnaire] : ! [v3: vQConf] : ( ~ (vQC(v0, v1, % 44.24/6.84 | v2) = v3) | ~ vQMap(v1) | ~ vAnsMap(v0) | ~ vQuestionnaire(v2) % 44.24/6.84 | | ? [v4: any] : ( ~ (v4 = all_406_0) & vsomeQConf(v3) = v4 & % 44.24/6.84 | vOptQConf(v4))) % 44.24/6.84 | % 44.24/6.84 | ALPHA: (7) implies: % 44.24/6.84 | (8) ~ (all_406_5 = 0) % 44.24/6.84 | (9) vATMap(all_406_12) % 44.24/6.85 | (10) vATMap(all_406_11) % 44.24/6.85 | (11) vAnsMap(all_406_10) % 44.24/6.85 | (12) vExp(all_406_8) % 44.24/6.85 | (13) vQMap(all_406_14) % 44.24/6.85 | (14) vQID(all_406_9) % 44.24/6.85 | (15) vAType(all_406_13) % 44.24/6.85 | (16) vvalue(all_406_9, all_406_13, all_406_8) = all_406_7 % 44.24/6.85 | (17) vMC(all_406_12, all_406_11) = all_406_1 % 44.24/6.85 | (18) vMC(all_406_4, all_406_3) = all_406_2 % 44.24/6.85 | (19) vqsingle(all_406_7) = all_406_6 % 44.24/6.85 | (20) visValue(all_406_6) = all_406_5 % 44.24/6.85 | (21) vreduce(all_406_6, all_406_10, all_406_14) = all_406_0 % 44.24/6.85 | (22) vtypeAM(all_406_10) = all_406_4 % 44.24/6.85 | (23) vtypeQM(all_406_14) = all_406_3 % 44.24/6.85 | (24) vptcheck(all_406_2, all_406_6, all_406_1) = 0 % 44.24/6.85 | (25) ! [v0: vAnsMap] : ! [v1: vQMap] : ! [v2: vQuestionnaire] : ! [v3: % 44.24/6.85 | vQConf] : ( ~ (vQC(v0, v1, v2) = v3) | ~ vQMap(v1) | ~ vAnsMap(v0) % 44.24/6.85 | | ~ vQuestionnaire(v2) | ? [v4: any] : ( ~ (v4 = all_406_0) & % 44.24/6.85 | vsomeQConf(v3) = v4 & vOptQConf(v4))) % 44.24/6.85 | % 44.24/6.85 | GROUND_INST: instantiating (1) with all_406_14, all_406_13, all_406_10, % 44.24/6.85 | all_406_9, all_406_8, all_406_7, all_406_6, all_406_0, % 44.24/6.85 | simplifying with (11), (12), (13), (14), (15), (16), (19), (21) % 44.24/6.85 | gives: % 44.24/6.85 | (26) ? [v0: any] : ? [v1: vAval] : ? [v2: vAnsMap] : ? [v3: vQConf] : % 44.24/6.85 | ? [v4: vOptQConf] : (vexpIsValue(all_406_8) = v0 & % 44.24/6.85 | vgetExpValue(all_406_8) = v1 & vQC(v2, all_406_14, vqempty) = v3 & % 44.24/6.85 | vabind(all_406_9, v1, all_406_10) = v2 & vsomeQConf(v3) = v4 & % 44.24/6.85 | vAnsMap(v2) & vOptQConf(v4) & vAval(v1) & vQConf(v3) & ( ~ (v0 = 0) % 44.24/6.85 | | v4 = all_406_0)) % 44.24/6.85 | % 44.24/6.85 | GROUND_INST: instantiating (Progress-qsingle-value-expIsValue-True) with % 44.24/6.85 | all_406_14, all_406_13, all_406_12, all_406_11, all_406_10, % 44.24/6.85 | all_406_9, all_406_8, all_406_7, all_406_6, all_406_4, all_406_3, % 44.24/6.85 | all_406_2, all_406_1, simplifying with (9), (10), (11), (12), % 44.24/6.85 | (13), (14), (15), (16), (17), (18), (19), (22), (23), (24) gives: % 44.24/6.85 | (27) ? [v0: any] : ? [v1: any] : ? [v2: vOptQConf] : (vreduce(all_406_6, % 44.24/6.85 | all_406_10, all_406_14) = v2 & vexpIsValue(all_406_8) = v0 & % 44.24/6.85 | visValue(all_406_6) = v1 & vOptQConf(v2) & ( ~ (v0 = 0) | v1 = 0 | % 44.24/6.85 | ? [v3: vAnsMap] : ? [v4: vQMap] : ? [v5: vQuestionnaire] : ? % 44.24/6.85 | [v6: vQConf] : (vQC(v3, v4, v5) = v6 & vsomeQConf(v6) = v2 & % 44.24/6.85 | vQMap(v4) & vAnsMap(v3) & vQConf(v6) & vQuestionnaire(v5)))) % 44.24/6.85 | % 44.24/6.85 | GROUND_INST: instantiating (Progress-qsingle-value-expIsValue-False) with % 44.24/6.85 | all_406_14, all_406_13, all_406_12, all_406_11, all_406_10, % 44.24/6.85 | all_406_9, all_406_8, all_406_7, all_406_6, all_406_4, all_406_3, % 44.24/6.85 | all_406_2, all_406_1, simplifying with (9), (10), (11), (12), % 44.24/6.85 | (13), (14), (15), (16), (17), (18), (19), (22), (23), (24) gives: % 44.24/6.86 | (28) ? [v0: any] : ? [v1: any] : ? [v2: vOptQConf] : (vreduce(all_406_6, % 44.24/6.86 | all_406_10, all_406_14) = v2 & vexpIsValue(all_406_8) = v0 & % 44.24/6.86 | visValue(all_406_6) = v1 & vOptQConf(v2) & (v1 = 0 | v0 = 0 | ? % 44.24/6.86 | [v3: vAnsMap] : ? [v4: vQMap] : ? [v5: vQuestionnaire] : ? [v6: % 44.24/6.86 | vQConf] : (vQC(v3, v4, v5) = v6 & vsomeQConf(v6) = v2 & % 44.24/6.86 | vQMap(v4) & vAnsMap(v3) & vQConf(v6) & vQuestionnaire(v5)))) % 44.24/6.86 | % 44.24/6.86 | DELTA: instantiating (26) with fresh symbols all_445_0, all_445_1, all_445_2, % 44.24/6.86 | all_445_3, all_445_4 gives: % 44.24/6.86 | (29) vexpIsValue(all_406_8) = all_445_4 & vgetExpValue(all_406_8) = % 44.24/6.86 | all_445_3 & vQC(all_445_2, all_406_14, vqempty) = all_445_1 & % 44.24/6.86 | vabind(all_406_9, all_445_3, all_406_10) = all_445_2 & % 44.24/6.86 | vsomeQConf(all_445_1) = all_445_0 & vAnsMap(all_445_2) & % 44.24/6.86 | vOptQConf(all_445_0) & vAval(all_445_3) & vQConf(all_445_1) & ( ~ % 44.24/6.86 | (all_445_4 = 0) | all_445_0 = all_406_0) % 44.24/6.86 | % 44.24/6.86 | ALPHA: (29) implies: % 44.24/6.86 | (30) vAnsMap(all_445_2) % 44.24/6.86 | (31) vsomeQConf(all_445_1) = all_445_0 % 44.24/6.86 | (32) vQC(all_445_2, all_406_14, vqempty) = all_445_1 % 44.24/6.86 | (33) vexpIsValue(all_406_8) = all_445_4 % 44.24/6.86 | (34) ~ (all_445_4 = 0) | all_445_0 = all_406_0 % 44.24/6.86 | % 44.24/6.86 | DELTA: instantiating (27) with fresh symbols all_447_0, all_447_1, all_447_2 % 44.24/6.86 | gives: % 44.24/6.86 | (35) vreduce(all_406_6, all_406_10, all_406_14) = all_447_0 & % 44.24/6.86 | vexpIsValue(all_406_8) = all_447_2 & visValue(all_406_6) = all_447_1 & % 44.24/6.86 | vOptQConf(all_447_0) & ( ~ (all_447_2 = 0) | all_447_1 = 0 | ? [v0: % 44.24/6.86 | vAnsMap] : ? [v1: vQMap] : ? [v2: vQuestionnaire] : ? [v3: % 44.24/6.86 | vQConf] : (vQC(v0, v1, v2) = v3 & vsomeQConf(v3) = all_447_0 & % 44.24/6.86 | vQMap(v1) & vAnsMap(v0) & vQConf(v3) & vQuestionnaire(v2))) % 44.24/6.86 | % 44.24/6.86 | ALPHA: (35) implies: % 44.24/6.86 | (36) visValue(all_406_6) = all_447_1 % 44.24/6.86 | (37) vexpIsValue(all_406_8) = all_447_2 % 44.24/6.86 | (38) vreduce(all_406_6, all_406_10, all_406_14) = all_447_0 % 44.24/6.86 | % 44.24/6.86 | DELTA: instantiating (28) with fresh symbols all_449_0, all_449_1, all_449_2 % 44.24/6.86 | gives: % 44.24/6.86 | (39) vreduce(all_406_6, all_406_10, all_406_14) = all_449_0 & % 44.24/6.86 | vexpIsValue(all_406_8) = all_449_2 & visValue(all_406_6) = all_449_1 & % 44.24/6.86 | vOptQConf(all_449_0) & (all_449_1 = 0 | all_449_2 = 0 | ? [v0: % 44.24/6.86 | vAnsMap] : ? [v1: vQMap] : ? [v2: vQuestionnaire] : ? [v3: % 44.24/6.86 | vQConf] : (vQC(v0, v1, v2) = v3 & vsomeQConf(v3) = all_449_0 & % 44.24/6.86 | vQMap(v1) & vAnsMap(v0) & vQConf(v3) & vQuestionnaire(v2))) % 44.24/6.86 | % 44.24/6.86 | ALPHA: (39) implies: % 44.24/6.86 | (40) visValue(all_406_6) = all_449_1 % 44.24/6.86 | (41) vexpIsValue(all_406_8) = all_449_2 % 44.24/6.86 | (42) vreduce(all_406_6, all_406_10, all_406_14) = all_449_0 % 44.24/6.86 | (43) all_449_1 = 0 | all_449_2 = 0 | ? [v0: vAnsMap] : ? [v1: vQMap] : ? % 44.24/6.86 | [v2: vQuestionnaire] : ? [v3: vQConf] : (vQC(v0, v1, v2) = v3 & % 44.24/6.86 | vsomeQConf(v3) = all_449_0 & vQMap(v1) & vAnsMap(v0) & vQConf(v3) & % 44.24/6.86 | vQuestionnaire(v2)) % 44.24/6.86 | % 44.24/6.86 | GROUND_INST: instantiating (4) with all_406_5, all_449_1, all_406_6, % 44.24/6.86 | simplifying with (20), (40) gives: % 44.24/6.86 | (44) all_449_1 = all_406_5 % 44.24/6.86 | % 44.24/6.86 | GROUND_INST: instantiating (4) with all_447_1, all_449_1, all_406_6, % 44.24/6.86 | simplifying with (36), (40) gives: % 44.24/6.86 | (45) all_449_1 = all_447_1 % 44.24/6.86 | % 44.24/6.86 | GROUND_INST: instantiating (5) with all_447_2, all_449_2, all_406_8, % 44.24/6.86 | simplifying with (37), (41) gives: % 44.24/6.86 | (46) all_449_2 = all_447_2 % 44.24/6.86 | % 44.24/6.86 | GROUND_INST: instantiating (5) with all_445_4, all_449_2, all_406_8, % 44.24/6.86 | simplifying with (33), (41) gives: % 44.24/6.86 | (47) all_449_2 = all_445_4 % 44.24/6.86 | % 44.24/6.87 | GROUND_INST: instantiating (6) with all_406_0, all_449_0, all_406_14, % 44.24/6.87 | all_406_10, all_406_6, simplifying with (21), (42) gives: % 44.24/6.87 | (48) all_449_0 = all_406_0 % 44.24/6.87 | % 44.24/6.87 | GROUND_INST: instantiating (6) with all_447_0, all_449_0, all_406_14, % 44.24/6.87 | all_406_10, all_406_6, simplifying with (38), (42) gives: % 44.24/6.87 | (49) all_449_0 = all_447_0 % 44.24/6.87 | % 44.24/6.87 | COMBINE_EQS: (48), (49) imply: % 44.24/6.87 | (50) all_447_0 = all_406_0 % 44.24/6.87 | % 44.24/6.87 | COMBINE_EQS: (44), (45) imply: % 44.24/6.87 | (51) all_447_1 = all_406_5 % 44.24/6.87 | % 44.24/6.87 | COMBINE_EQS: (46), (47) imply: % 44.24/6.87 | (52) all_447_2 = all_445_4 % 44.24/6.87 | % 44.24/6.87 | GROUND_INST: instantiating (25) with all_445_2, all_406_14, vqempty, % 44.24/6.87 | all_445_1, simplifying with (2), (13), (30), (32) gives: % 44.24/6.87 | (53) ? [v0: any] : ( ~ (v0 = all_406_0) & vsomeQConf(all_445_1) = v0 & % 44.24/6.87 | vOptQConf(v0)) % 44.24/6.87 | % 44.24/6.87 | DELTA: instantiating (53) with fresh symbol all_495_0 gives: % 44.24/6.87 | (54) ~ (all_495_0 = all_406_0) & vsomeQConf(all_445_1) = all_495_0 & % 44.24/6.87 | vOptQConf(all_495_0) % 44.24/6.87 | % 44.24/6.87 | ALPHA: (54) implies: % 44.24/6.87 | (55) ~ (all_495_0 = all_406_0) % 44.24/6.87 | (56) vsomeQConf(all_445_1) = all_495_0 % 44.24/6.87 | % 44.24/6.87 | GROUND_INST: instantiating (3) with all_445_0, all_495_0, all_445_1, % 44.24/6.87 | simplifying with (31), (56) gives: % 44.24/6.87 | (57) all_495_0 = all_445_0 % 44.24/6.87 | % 44.24/6.87 | REDUCE: (55), (57) imply: % 44.24/6.87 | (58) ~ (all_445_0 = all_406_0) % 44.24/6.87 | % 44.24/6.87 | BETA: splitting (34) gives: % 44.24/6.87 | % 44.24/6.87 | Case 1: % 44.24/6.87 | | % 44.24/6.87 | | (59) ~ (all_445_4 = 0) % 44.24/6.87 | | % 44.24/6.87 | | BETA: splitting (43) gives: % 44.24/6.87 | | % 44.24/6.87 | | Case 1: % 44.24/6.87 | | | % 44.24/6.87 | | | (60) all_449_1 = 0 % 44.24/6.87 | | | % 44.24/6.87 | | | COMBINE_EQS: (44), (60) imply: % 44.24/6.87 | | | (61) all_406_5 = 0 % 44.24/6.87 | | | % 44.24/6.87 | | | REDUCE: (8), (61) imply: % 44.24/6.87 | | | (62) $false % 44.24/6.87 | | | % 44.24/6.87 | | | CLOSE: (62) is inconsistent. % 44.24/6.87 | | | % 44.24/6.87 | | Case 2: % 44.24/6.87 | | | % 44.24/6.87 | | | (63) all_449_2 = 0 | ? [v0: vAnsMap] : ? [v1: vQMap] : ? [v2: % 44.24/6.87 | | | vQuestionnaire] : ? [v3: vQConf] : (vQC(v0, v1, v2) = v3 & % 44.24/6.87 | | | vsomeQConf(v3) = all_449_0 & vQMap(v1) & vAnsMap(v0) & % 44.24/6.87 | | | vQConf(v3) & vQuestionnaire(v2)) % 44.24/6.87 | | | % 44.24/6.87 | | | BETA: splitting (63) gives: % 44.24/6.87 | | | % 44.24/6.87 | | | Case 1: % 44.24/6.87 | | | | % 44.24/6.87 | | | | (64) all_449_2 = 0 % 44.24/6.87 | | | | % 44.24/6.87 | | | | COMBINE_EQS: (47), (64) imply: % 44.24/6.87 | | | | (65) all_445_4 = 0 % 44.24/6.87 | | | | % 44.24/6.87 | | | | REDUCE: (59), (65) imply: % 44.24/6.87 | | | | (66) $false % 44.24/6.87 | | | | % 44.24/6.87 | | | | CLOSE: (66) is inconsistent. % 44.24/6.87 | | | | % 44.24/6.87 | | | Case 2: % 44.24/6.87 | | | | % 44.24/6.87 | | | | (67) ? [v0: vAnsMap] : ? [v1: vQMap] : ? [v2: vQuestionnaire] : ? % 44.24/6.87 | | | | [v3: vQConf] : (vQC(v0, v1, v2) = v3 & vsomeQConf(v3) = % 44.24/6.87 | | | | all_449_0 & vQMap(v1) & vAnsMap(v0) & vQConf(v3) & % 44.24/6.87 | | | | vQuestionnaire(v2)) % 44.24/6.87 | | | | % 44.24/6.87 | | | | DELTA: instantiating (67) with fresh symbols all_526_0, all_526_1, % 44.24/6.87 | | | | all_526_2, all_526_3 gives: % 44.24/6.87 | | | | (68) vQC(all_526_3, all_526_2, all_526_1) = all_526_0 & % 44.24/6.87 | | | | vsomeQConf(all_526_0) = all_449_0 & vQMap(all_526_2) & % 44.24/6.87 | | | | vAnsMap(all_526_3) & vQConf(all_526_0) & % 44.24/6.87 | | | | vQuestionnaire(all_526_1) % 44.24/6.87 | | | | % 44.24/6.87 | | | | ALPHA: (68) implies: % 44.24/6.87 | | | | (69) vQuestionnaire(all_526_1) % 44.24/6.87 | | | | (70) vAnsMap(all_526_3) % 44.24/6.87 | | | | (71) vQMap(all_526_2) % 44.24/6.88 | | | | (72) vsomeQConf(all_526_0) = all_449_0 % 44.24/6.88 | | | | (73) vQC(all_526_3, all_526_2, all_526_1) = all_526_0 % 44.24/6.88 | | | | % 44.24/6.88 | | | | REDUCE: (48), (72) imply: % 44.24/6.88 | | | | (74) vsomeQConf(all_526_0) = all_406_0 % 44.24/6.88 | | | | % 44.24/6.88 | | | | GROUND_INST: instantiating (25) with all_526_3, all_526_2, all_526_1, % 44.24/6.88 | | | | all_526_0, simplifying with (69), (70), (71), (73) gives: % 44.24/6.88 | | | | (75) ? [v0: any] : ( ~ (v0 = all_406_0) & vsomeQConf(all_526_0) = v0 % 44.24/6.88 | | | | & vOptQConf(v0)) % 44.24/6.88 | | | | % 44.24/6.88 | | | | DELTA: instantiating (75) with fresh symbol all_636_0 gives: % 44.24/6.88 | | | | (76) ~ (all_636_0 = all_406_0) & vsomeQConf(all_526_0) = all_636_0 & % 44.24/6.88 | | | | vOptQConf(all_636_0) % 44.24/6.88 | | | | % 44.24/6.88 | | | | ALPHA: (76) implies: % 44.24/6.88 | | | | (77) ~ (all_636_0 = all_406_0) % 44.24/6.88 | | | | (78) vsomeQConf(all_526_0) = all_636_0 % 44.24/6.88 | | | | % 44.24/6.88 | | | | GROUND_INST: instantiating (3) with all_406_0, all_636_0, all_526_0, % 44.24/6.88 | | | | simplifying with (74), (78) gives: % 44.24/6.88 | | | | (79) all_636_0 = all_406_0 % 44.24/6.88 | | | | % 44.24/6.88 | | | | REDUCE: (77), (79) imply: % 44.24/6.88 | | | | (80) $false % 44.24/6.88 | | | | % 44.24/6.88 | | | | CLOSE: (80) is inconsistent. % 44.24/6.88 | | | | % 44.24/6.88 | | | End of split % 44.24/6.88 | | | % 44.24/6.88 | | End of split % 44.24/6.88 | | % 44.24/6.88 | Case 2: % 44.24/6.88 | | % 44.24/6.88 | | (81) all_445_0 = all_406_0 % 44.24/6.88 | | % 44.24/6.88 | | REDUCE: (58), (81) imply: % 44.24/6.88 | | (82) $false % 44.24/6.88 | | % 44.24/6.88 | | CLOSE: (82) is inconsistent. % 44.24/6.88 | | % 44.24/6.88 | End of split % 44.24/6.88 | % 44.24/6.88 End of proof % 44.24/6.88 % SZS output end Proof for theBenchmark % 44.24/6.88 % 44.24/6.88 6273ms %------------------------------------------------------------------------------