%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM308_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 : n023.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:44 PM UTC 2026 % Result : Theorem 73.50s 10.32s % Output : Proof 74.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM308_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.33 % Computer : n023.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Mon May 4 20:44:53 EDT 2026 % 0.16/0.33 % CPUTime : % 0.52/0.59 ________ _____ % 0.52/0.59 ___ __ \_________(_)________________________________ % 0.52/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.52/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.52/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.52/0.59 % 0.52/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.52/0.59 (2023-06-19) % 0.52/0.59 % 0.52/0.59 (c) Philipp Rümmer, 2009-2023 % 0.52/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.52/0.59 Amanda Stjerna. % 0.52/0.59 Free software under BSD-3-Clause. % 0.52/0.59 % 0.52/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.52/0.59 % 0.52/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.52/0.61 Running up to 7 provers in parallel. % 0.52/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.52/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.52/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.52/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.52/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.52/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.52/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.91/2.07 Prover 1: Preprocessing ... % 9.91/2.07 Prover 4: Preprocessing ... % 9.91/2.11 Prover 3: Preprocessing ... % 9.91/2.11 Prover 2: Preprocessing ... % 10.66/2.13 Prover 5: Preprocessing ... % 10.66/2.13 Prover 6: Preprocessing ... % 10.66/2.13 Prover 0: Preprocessing ... % 24.19/3.99 Prover 1: Warning: ignoring some quantifiers % 25.05/4.02 Prover 4: Warning: ignoring some quantifiers % 25.05/4.07 Prover 3: Warning: ignoring some quantifiers % 25.85/4.14 Prover 1: Constructing countermodel ... % 25.85/4.14 Prover 3: Constructing countermodel ... % 25.85/4.18 Prover 4: Constructing countermodel ... % 26.48/4.20 Prover 6: Proving ... % 26.48/4.21 Prover 5: Proving ... % 26.48/4.25 Prover 0: Proving ... % 29.61/4.66 Prover 2: Proving ... % 72.92/10.23 Prover 4: Found proof (size 188) % 72.92/10.24 Prover 4: proved (9617ms) % 72.92/10.24 Prover 1: stopped % 72.92/10.24 Prover 3: stopped % 72.92/10.24 Prover 5: stopped % 72.92/10.24 Prover 6: stopped % 72.92/10.26 Prover 2: stopped % 73.50/10.32 Prover 0: stopped % 73.50/10.32 % 73.50/10.32 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 73.50/10.32 % 73.50/10.34 % SZS output start Proof for theBenchmark % 73.50/10.35 Assumptions after simplification: % 73.50/10.35 --------------------------------- % 73.50/10.35 % 73.50/10.35 (DIFF-tempty-tcons) % 73.50/10.37 vRawTable(vtempty) & ! [v0: vRow] : ! [v1: vRawTable] : ( ~ (vtcons(v0, v1) % 73.50/10.37 = vtempty) | ~ vRawTable(v1) | ~ vRow(v0)) % 73.50/10.37 % 73.50/10.37 (EQ-tcons) % 73.50/10.38 ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRow] : ! [v3: vRawTable] : ! % 73.50/10.38 [v4: vRawTable] : (v3 = v1 | ~ (vtcons(v2, v3) = v4) | ~ (vtcons(v0, v1) = % 73.50/10.38 v4) | ~ vRawTable(v3) | ~ vRawTable(v1) | ~ vRow(v2) | ~ vRow(v0)) & % 73.50/10.38 ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRow] : ! [v3: vRawTable] : ! % 73.50/10.38 [v4: vRawTable] : (v2 = v0 | ~ (vtcons(v2, v3) = v4) | ~ (vtcons(v0, v1) = % 73.50/10.38 v4) | ~ vRawTable(v3) | ~ vRawTable(v1) | ~ vRow(v2) | ~ vRow(v0)) % 73.50/10.38 % 73.50/10.38 (rawDifference-3) % 73.50/10.38 vRawTable(vtempty) & ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRawTable] : % 73.50/10.38 ! [v3: vRawTable] : ! [v4: vRawTable] : ( ~ (vrawDifference(v3, v2) = v4) | % 73.50/10.38 ~ (vtcons(v0, v1) = v3) | ~ vRawTable(v2) | ~ vRawTable(v1) | ~ vRow(v0) % 73.50/10.38 | ? [v5: any] : ? [v6: vRawTable] : ? [v7: vRawTable] : ? [v8: vRow] : % 73.50/10.38 (vRow(v8) & ((v8 = v0 & v1 = vtempty) | (vrawDifference(v1, v2) = v6 & % 73.50/10.38 vrowIn(v0, v2) = v5 & vtcons(v0, v6) = v7 & vRawTable(v7) & % 73.50/10.38 vRawTable(v6) & (v7 = v4 | v5 = 0))))) & ! [v0: vRow] : ! [v1: % 73.50/10.38 vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : ! [v4: vRawTable] : % 73.50/10.38 ( ~ (vrawDifference(v1, v2) = v3) | ~ (vtcons(v0, v3) = v4) | ~ % 73.50/10.38 vRawTable(v2) | ~ vRawTable(v1) | ~ vRow(v0) | ? [v5: any] : ? [v6: % 73.50/10.38 vRawTable] : ? [v7: vRawTable] : ? [v8: vRow] : (vRow(v8) & ((v8 = v0 & % 73.50/10.38 v1 = vtempty) | (vrawDifference(v6, v2) = v7 & vrowIn(v0, v2) = v5 & % 73.50/10.38 vtcons(v0, v1) = v6 & vRawTable(v7) & vRawTable(v6) & (v7 = v4 | v5 = % 73.50/10.38 0))))) % 73.50/10.38 % 73.50/10.38 (rawDifference-4) % 73.50/10.38 vRawTable(vtempty) & ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRawTable] : % 73.50/10.38 ! [v3: vRawTable] : ! [v4: vRawTable] : ( ~ (vrawDifference(v3, v2) = v4) | % 73.50/10.38 ~ (vtcons(v0, v1) = v3) | ~ vRawTable(v2) | ~ vRawTable(v1) | ~ vRow(v0) % 73.50/10.38 | ? [v5: any] : ? [v6: vRawTable] : ? [v7: vRow] : (vRow(v7) & ((v7 = v0 % 73.50/10.38 & v1 = vtempty) | (vrawDifference(v1, v2) = v6 & vrowIn(v0, v2) = v5 & % 73.50/10.38 vRawTable(v6) & ( ~ (v5 = 0) | v6 = v4))))) % 73.50/10.38 % 73.50/10.38 (rawDifference-INV) % 73.50/10.39 vRawTable(vtempty) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 73.50/10.39 vRawTable] : ( ~ (vrawDifference(v0, v1) = v2) | ~ vRawTable(v1) | ~ % 73.50/10.39 vRawTable(v0) | ? [v3: vRow] : ? [v4: vRawTable] : ? [v5: vRawTable] : ? % 73.50/10.39 [v6: vRawTable] : ? [v7: vRawTable] : ? [v8: int] : ? [v9: vRawTable] : % 73.50/10.39 ? [v10: vRow] : ? [v11: vRawTable] : ? [v12: vRawTable] : ? [v13: % 73.50/10.39 vRawTable] : ? [v14: vRawTable] : ? [v15: int] : ? [v16: vRawTable] : % 73.50/10.39 ? [v17: vRawTable] : ? [v18: vRow] : ? [v19: vRawTable] : ? [v20: int] : % 73.50/10.39 ? [v21: vRawTable] : ? [v22: vRow] : ? [v23: vRawTable] : ? [v24: int] : % 73.50/10.39 ? [v25: vRawTable] : ? [v26: vRawTable] : (vRawTable(v26) & vRawTable(v23) % 73.50/10.39 & vRawTable(v19) & vRawTable(v13) & vRawTable(v12) & vRawTable(v11) & % 73.50/10.39 vRawTable(v6) & vRawTable(v5) & vRawTable(v4) & vRow(v22) & vRow(v18) & % 73.50/10.39 vRow(v10) & vRow(v3) & ((v26 = v1 & v2 = vtempty & v0 = vtempty) | (v25 = % 73.50/10.39 v0 & v23 = v1 & v2 = v0 & ~ (v24 = 0) & vrowIn(v22, v1) = v24 & % 73.50/10.39 vtcons(v22, vtempty) = v0) | (v21 = v0 & v20 = 0 & v19 = v1 & v2 = % 73.50/10.39 vtempty & vrowIn(v18, v1) = 0 & vtcons(v18, vtempty) = v0) | (v17 = v2 % 73.50/10.39 & v16 = v0 & v14 = v12 & v13 = v1 & ~ (v15 = 0) & ~ (v11 = vtempty) % 73.50/10.39 & vrawDifference(v11, v1) = v12 & vrowIn(v10, v1) = v15 & vtcons(v10, % 73.50/10.39 v12) = v2 & vtcons(v10, v11) = v0 & vRawTable(v2)) | (v9 = v0 & v8 = % 73.50/10.39 0 & v7 = v2 & v6 = v1 & v5 = v2 & ~ (v4 = vtempty) & % 73.50/10.39 vrawDifference(v4, v1) = v2 & vrowIn(v3, v1) = 0 & vtcons(v3, v4) = v0 % 73.50/10.39 & vRawTable(v2))))) % 73.50/10.39 % 73.50/10.39 (rawDifferencePreservesWellTypedRaw-tcons-IH0) % 73.50/10.39 vRawTable(vrt2) & ! [v0: vTType] : ! [v1: vRawTable] : ! [v2: vRawTable] : % 73.50/10.39 ! [v3: int] : (v3 = 0 | ~ (vrawDifference(vrt2, v1) = v2) | ~ % 73.50/10.39 (vwelltypedRawtable(v0, v2) = v3) | ~ vTType(v0) | ~ vRawTable(v1) | ? % 73.50/10.39 [v4: any] : ? [v5: any] : (vwelltypedRawtable(v0, v1) = v5 & % 73.50/10.39 vwelltypedRawtable(v0, vrt2) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0)))) & ! % 73.50/10.39 [v0: vTType] : ! [v1: vRawTable] : ( ~ (vwelltypedRawtable(v0, v1) = 0) | ~ % 73.50/10.39 vTType(v0) | ~ vRawTable(v1) | ? [v2: any] : ? [v3: vRawTable] : ? [v4: % 73.50/10.39 any] : (vrawDifference(vrt2, v1) = v3 & vwelltypedRawtable(v0, v3) = v4 & % 73.50/10.39 vwelltypedRawtable(v0, vrt2) = v2 & vRawTable(v3) & ( ~ (v2 = 0) | v4 = % 73.50/10.39 0))) % 73.50/10.39 % 73.50/10.39 (rawDifferencePreservesWellTypedRaw-tcons-tempty-rowIn-False) % 73.50/10.39 vRawTable(vrt2) & vRawTable(vtempty) & ? [v0: vRow] : ? [v1: vTType] : ? % 73.50/10.39 [v2: vRawTable] : ? [v3: vRawTable] : ? [v4: int] : ( ~ (v4 = 0) & % 73.50/10.39 vrawDifference(v2, vtempty) = v3 & vrowIn(v0, vrt2) = 0 & % 73.50/10.39 vwelltypedRawtable(v1, v3) = v4 & vwelltypedRawtable(v1, v2) = 0 & % 73.50/10.39 vwelltypedRawtable(v1, vtempty) = 0 & vtcons(v0, vrt2) = v2 & vTType(v1) & % 73.50/10.39 vRawTable(v3) & vRawTable(v2) & vRow(v0)) % 73.50/10.39 % 73.50/10.39 (rowIn-0) % 73.50/10.39 vRawTable(vtempty) & ! [v0: vRow] : ( ~ (vrowIn(v0, vtempty) = 0) | ~ % 73.50/10.39 vRow(v0)) % 73.50/10.39 % 73.50/10.39 (welltypedRawtable-1) % 73.50/10.40 ! [v0: vTType] : ! [v1: vRow] : ! [v2: vRawTable] : ! [v3: vRawTable] : ! % 73.94/10.40 [v4: int] : (v4 = 0 | ~ (vwelltypedRawtable(v0, v3) = v4) | ~ (vtcons(v1, % 73.94/10.40 v2) = v3) | ~ vTType(v0) | ~ vRawTable(v2) | ~ vRow(v1) | ? [v5: % 73.94/10.40 any] : ? [v6: any] : (vwelltypedRawtable(v0, v2) = v6 & vwelltypedRow(v0, % 73.94/10.40 v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0)))) & ! [v0: vTType] : ! [v1: % 73.94/10.40 vRow] : ! [v2: vRawTable] : ! [v3: vRawTable] : ( ~ % 73.94/10.40 (vwelltypedRawtable(v0, v3) = 0) | ~ (vtcons(v1, v2) = v3) | ~ vTType(v0) % 73.94/10.40 | ~ vRawTable(v2) | ~ vRow(v1) | (vwelltypedRawtable(v0, v2) = 0 & % 73.94/10.40 vwelltypedRow(v0, v1) = 0)) % 73.94/10.40 % 73.94/10.40 (welltypedRawtable-false-INV) % 73.94/10.40 ! [v0: vTType] : ! [v1: vRawTable] : ! [v2: int] : (v2 = 0 | ~ % 73.94/10.40 (vwelltypedRawtable(v0, v1) = v2) | ~ vTType(v0) | ~ vRawTable(v1) | ? % 73.94/10.40 [v3: vRow] : ? [v4: vRawTable] : ? [v5: any] : ? [v6: any] : % 73.94/10.40 (vwelltypedRawtable(v0, v4) = v6 & vwelltypedRow(v0, v3) = v5 & vtcons(v3, % 73.94/10.40 v4) = v1 & vRawTable(v4) & vRow(v3) & ( ~ (v6 = 0) | ~ (v5 = 0)))) % 73.94/10.40 % 73.94/10.40 (welltypedRawtable-true-INV) % 73.94/10.40 vRawTable(vtempty) & ! [v0: vTType] : ! [v1: vRawTable] : ( ~ % 73.94/10.40 (vwelltypedRawtable(v0, v1) = 0) | ~ vTType(v0) | ~ vRawTable(v1) | ? % 73.94/10.40 [v2: vRow] : ? [v3: vRawTable] : ? [v4: vTType] : ? [v5: vRawTable] : ? % 73.94/10.40 [v6: int] : ? [v7: int] : ? [v8: vTType] : (vTType(v8) & vTType(v4) & % 73.94/10.40 vRawTable(v3) & vRow(v2) & ((v8 = v0 & v1 = vtempty) | (v7 = 0 & v6 = 0 & % 73.94/10.40 v5 = v1 & v4 = v0 & vwelltypedRawtable(v0, v3) = 0 & vwelltypedRow(v0, % 73.94/10.40 v2) = 0 & vtcons(v2, v3) = v1)))) % 73.94/10.40 % 73.94/10.40 (function-axioms) % 73.94/10.42 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTType] : ! % 73.94/10.42 [v3: vQuery] : ! [v4: vTTContext] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) % 73.94/10.42 | ~ (vptcheck(v4, v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] % 73.94/10.42 : ! [v2: vPred] : ! [v3: vAttrL] : ! [v4: vRawTable] : (v1 = v0 | ~ % 73.94/10.42 (vfilterRows(v4, v3, v2) = v1) | ~ (vfilterRows(v4, v3, v2) = v0)) & ! % 73.94/10.42 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! [v3: % 73.94/10.42 vAttrL] : ! [v4: vPred] : (v1 = v0 | ~ (vfilterSingleRow(v4, v3, v2) = v1) % 73.94/10.42 | ~ (vfilterSingleRow(v4, v3, v2) = v0)) & ! [v0: vOptVal] : ! [v1: % 73.94/10.42 vOptVal] : ! [v2: vRow] : ! [v3: vAttrL] : ! [v4: vExp] : (v1 = v0 | ~ % 73.94/10.42 (vevalExpRow(v4, v3, v2) = v1) | ~ (vevalExpRow(v4, v3, v2) = v0)) & ! % 73.94/10.42 [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! [v2: vRawTable] : ! [v3: % 73.94/10.42 vAttrL] : ! [v4: vAttrL] : (v1 = v0 | ~ (vprojectCols(v4, v3, v2) = v1) | % 73.94/10.42 ~ (vprojectCols(v4, v3, v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: % 73.94/10.42 vOptRawTable] : ! [v2: vRawTable] : ! [v3: vAttrL] : ! [v4: vName] : (v1 % 73.94/10.42 = v0 | ~ (vfindCol(v4, v3, v2) = v1) | ~ (vfindCol(v4, v3, v2) = v0)) & ! % 73.94/10.42 [v0: vTStore] : ! [v1: vTStore] : ! [v2: vTStore] : ! [v3: vTable] : ! % 73.94/10.42 [v4: vName] : (v1 = v0 | ~ (vbindStore(v4, v3, v2) = v1) | ~ (vbindStore(v4, % 73.94/10.42 v3, v2) = v0)) & ! [v0: vTTContext] : ! [v1: vTTContext] : ! [v2: % 73.94/10.42 vTTContext] : ! [v3: vTType] : ! [v4: vName] : (v1 = v0 | ~ % 73.94/10.42 (vbindContext(v4, v3, v2) = v1) | ~ (vbindContext(v4, v3, v2) = v0)) & ! % 73.94/10.42 [v0: vTType] : ! [v1: vTType] : ! [v2: vTType] : ! [v3: vFType] : ! [v4: % 73.94/10.42 vName] : (v1 = v0 | ~ (vttcons(v4, v3, v2) = v1) | ~ (vttcons(v4, v3, v2) % 73.94/10.42 = v0)) & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vPred] : ! [v3: % 73.94/10.42 vName] : ! [v4: vSelect] : (v1 = v0 | ~ (vselectFromWhere(v4, v3, v2) = % 73.94/10.42 v1) | ~ (vselectFromWhere(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 73.94/10.42 : ! [v1: MultipleValueBool] : ! [v2: vTTContext] : ! [v3: vTStore] : (v1 = % 73.94/10.42 v0 | ~ (vstoreContextConsistent(v3, v2) = v1) | ~ % 73.94/10.42 (vstoreContextConsistent(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 73.94/10.42 [v1: MultipleValueBool] : ! [v2: vTType] : ! [v3: vPred] : (v1 = v0 | ~ % 73.94/10.42 (vtcheckPred(v3, v2) = v1) | ~ (vtcheckPred(v3, v2) = v0)) & ! [v0: % 73.94/10.42 vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: vExp] : (v1 = v0 % 73.94/10.42 | ~ (vtypeOfExp(v3, v2) = v1) | ~ (vtypeOfExp(v3, v2) = v0)) & ! [v0: % 73.94/10.42 vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vSelect] : (v1 = % 73.94/10.42 v0 | ~ (vprojectType(v3, v2) = v1) | ~ (vprojectType(v3, v2) = v0)) & ! % 73.94/10.43 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vAttrL] : (v1 % 73.94/10.43 = v0 | ~ (vprojectTypeAttrL(v3, v2) = v1) | ~ (vprojectTypeAttrL(v3, v2) = % 73.94/10.43 v0)) & ! [v0: vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: % 73.94/10.43 vName] : (v1 = v0 | ~ (vfindColType(v3, v2) = v1) | ~ (vfindColType(v3, % 73.94/10.43 v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: vTStore] % 73.94/10.43 : ! [v3: vQuery] : (v1 = v0 | ~ (vreduce(v3, v2) = v1) | ~ (vreduce(v3, v2) % 73.94/10.43 = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: vPred] : ! [v3: % 73.94/10.43 vTable] : (v1 = v0 | ~ (vfilterTable(v3, v2) = v1) | ~ (vfilterTable(v3, % 73.94/10.43 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 73.94/10.43 ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ (vlessThan(v3, v2) = v1) | ~ % 73.94/10.43 (vlessThan(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 73.94/10.43 MultipleValueBool] : ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ % 73.94/10.43 (vgreaterThan(v3, v2) = v1) | ~ (vgreaterThan(v3, v2) = v0)) & ! [v0: % 73.94/10.43 vOptTable] : ! [v1: vOptTable] : ! [v2: vTable] : ! [v3: vSelect] : (v1 = % 73.94/10.43 v0 | ~ (vprojectTable(v3, v2) = v1) | ~ (vprojectTable(v3, v2) = v0)) & ! % 73.94/10.43 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTTContext] : ! [v3: vName] : % 73.94/10.43 (v1 = v0 | ~ (vlookupContext(v3, v2) = v1) | ~ (vlookupContext(v3, v2) = % 73.94/10.43 v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! [v2: vTStore] : ! % 73.94/10.43 [v3: vName] : (v1 = v0 | ~ (vlookupStore(v3, v2) = v1) | ~ (vlookupStore(v3, % 73.94/10.43 v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 73.94/10.43 vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ (vrawDifference(v3, v2) = % 73.94/10.43 v1) | ~ (vrawDifference(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: % 73.94/10.43 vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 73.94/10.43 (vrawIntersection(v3, v2) = v1) | ~ (vrawIntersection(v3, v2) = v0)) & ! % 73.94/10.43 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 73.94/10.43 : (v1 = v0 | ~ (vrawUnion(v3, v2) = v1) | ~ (vrawUnion(v3, v2) = v0)) & ! % 73.94/10.43 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 73.94/10.43 : (v1 = v0 | ~ (vattachColToFrontRaw(v3, v2) = v1) | ~ % 73.94/10.43 (vattachColToFrontRaw(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 73.94/10.43 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 73.94/10.43 (vsameLength(v3, v2) = v1) | ~ (vsameLength(v3, v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRawTable] : ! % 73.94/10.43 [v3: vRow] : (v1 = v0 | ~ (vrowIn(v3, v2) = v1) | ~ (vrowIn(v3, v2) = v0)) & % 73.94/10.43 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTable] : ! % 73.94/10.43 [v3: vTType] : (v1 = v0 | ~ (vwelltypedtable(v3, v2) = v1) | ~ % 73.94/10.43 (vwelltypedtable(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 73.94/10.43 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ % 73.94/10.43 (vwelltypedRawtable(v3, v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) & % 73.94/10.43 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! % 73.94/10.43 [v3: vTType] : (v1 = v0 | ~ (vwelltypedRow(v3, v2) = v1) | ~ % 73.94/10.43 (vwelltypedRow(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 73.94/10.43 MultipleValueBool] : ! [v2: vAttrL] : ! [v3: vTType] : (v1 = v0 | ~ % 73.94/10.43 (vmatchingAttrL(v3, v2) = v1) | ~ (vmatchingAttrL(v3, v2) = v0)) & ! [v0: % 73.94/10.43 vAttrL] : ! [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vAttrL] : (v1 = v0 | % 73.94/10.43 ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vAttrL] : ! % 73.94/10.43 [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vName] : (v1 = v0 | ~ (vacons(v3, % 73.94/10.43 v2) = v1) | ~ (vacons(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] % 73.94/10.43 : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 73.94/10.43 (vlt(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! % 73.94/10.43 [v3: vExp] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! % 73.94/10.43 [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ % 73.94/10.43 (veq(v3, v2) = v1) | ~ (veq(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: % 73.94/10.43 vPred] : ! [v2: vPred] : ! [v3: vPred] : (v1 = v0 | ~ (vand(v3, v2) = v1) % 73.94/10.43 | ~ (vand(v3, v2) = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: % 73.94/10.43 vRawTable] : ! [v3: vAttrL] : (v1 = v0 | ~ (vtable(v3, v2) = v1) | ~ % 73.94/10.43 (vtable(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 73.94/10.43 vRawTable] : ! [v3: vRow] : (v1 = v0 | ~ (vtcons(v3, v2) = v1) | ~ % 73.94/10.43 (vtcons(v3, v2) = v0)) & ! [v0: vRow] : ! [v1: vRow] : ! [v2: vRow] : ! % 73.94/10.43 [v3: vVal] : (v1 = v0 | ~ (vrcons(v3, v2) = v1) | ~ (vrcons(v3, v2) = v0)) & % 73.94/10.43 ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = % 73.94/10.43 v0 | ~ (vDifference(v3, v2) = v1) | ~ (vDifference(v3, v2) = v0)) & ! % 73.94/10.43 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 73.94/10.43 | ~ (vIntersection(v3, v2) = v1) | ~ (vIntersection(v3, v2) = v0)) & ! % 73.94/10.43 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 73.94/10.43 | ~ (vUnion(v3, v2) = v1) | ~ (vUnion(v3, v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptFType] : (v1 = % 73.94/10.43 v0 | ~ (visSomeFType(v2) = v1) | ~ (visSomeFType(v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptVal] : (v1 = % 73.94/10.43 v0 | ~ (visSomeVal(v2) = v1) | ~ (visSomeVal(v2) = v0)) & ! [v0: % 73.94/10.43 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 73.94/10.43 (vprojectEmptyCol(v2) = v1) | ~ (vprojectEmptyCol(v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQuery] : (v1 = % 73.94/10.43 v0 | ~ (visSomeQuery(v2) = v1) | ~ (visSomeQuery(v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuery] : (v1 = v0 % 73.94/10.43 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTType] : (v1 = % 73.94/10.43 v0 | ~ (visSomeTType(v2) = v1) | ~ (visSomeTType(v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTable] : (v1 = % 73.94/10.43 v0 | ~ (visSomeTable(v2) = v1) | ~ (visSomeTable(v2) = v0)) & ! [v0: % 73.94/10.43 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptRawTable] : % 73.94/10.43 (v1 = v0 | ~ (visSomeRawTable(v2) = v1) | ~ (visSomeRawTable(v2) = v0)) & ! % 73.94/10.43 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 73.94/10.43 (vdropFirstColRaw(v2) = v1) | ~ (vdropFirstColRaw(v2) = v0)) & ! [v0: % 73.94/10.43 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 73.94/10.43 (vprojectFirstRaw(v2) = v1) | ~ (vprojectFirstRaw(v2) = v0)) & ! [v0: % 73.94/10.43 vFType] : ! [v1: vFType] : ! [v2: vVal] : (v1 = v0 | ~ (vfieldType(v2) = % 73.94/10.43 v1) | ~ (vfieldType(v2) = v0)) & ! [v0: vAttrL] : ! [v1: vAttrL] : ! % 73.94/10.43 [v2: vTable] : (v1 = v0 | ~ (vgetAttrL(v2) = v1) | ~ (vgetAttrL(v2) = v0)) & % 73.94/10.43 ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vTable] : (v1 = v0 | ~ % 73.94/10.43 (vgetRaw(v2) = v1) | ~ (vgetRaw(v2) = v0)) & ! [v0: vFType] : ! [v1: % 73.94/10.43 vFType] : ! [v2: vOptFType] : (v1 = v0 | ~ (vgetFType(v2) = v1) | ~ % 73.94/10.43 (vgetFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vOptVal] : % 73.94/10.43 (v1 = v0 | ~ (vgetVal(v2) = v1) | ~ (vgetVal(v2) = v0)) & ! [v0: vQuery] : % 73.94/10.43 ! [v1: vQuery] : ! [v2: vOptQuery] : (v1 = v0 | ~ (vgetQuery(v2) = v1) | ~ % 73.94/10.43 (vgetQuery(v2) = v0)) & ! [v0: vTType] : ! [v1: vTType] : ! [v2: % 73.94/10.43 vOptTType] : (v1 = v0 | ~ (vgetTType(v2) = v1) | ~ (vgetTType(v2) = v0)) & % 73.94/10.43 ! [v0: vTable] : ! [v1: vTable] : ! [v2: vOptTable] : (v1 = v0 | ~ % 73.94/10.43 (vgetTable(v2) = v1) | ~ (vgetTable(v2) = v0)) & ! [v0: vRawTable] : ! % 73.94/10.43 [v1: vRawTable] : ! [v2: vOptRawTable] : (v1 = v0 | ~ (vgetRawTable(v2) = % 73.94/10.43 v1) | ~ (vgetRawTable(v2) = v0)) & ! [v0: vOptFType] : ! [v1: % 73.94/10.43 vOptFType] : ! [v2: vFType] : (v1 = v0 | ~ (vsomeFType(v2) = v1) | ~ % 73.94/10.43 (vsomeFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vVal] : (v1 % 73.94/10.43 = v0 | ~ (venumVal(v2) = v1) | ~ (venumVal(v2) = v0)) & ! [v0: vPred] : % 73.94/10.43 ! [v1: vPred] : ! [v2: vPred] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) % 73.94/10.43 = v0)) & ! [v0: vOptVal] : ! [v1: vOptVal] : ! [v2: vVal] : (v1 = v0 | % 73.94/10.43 ~ (vsomeVal(v2) = v1) | ~ (vsomeVal(v2) = v0)) & ! [v0: vExp] : ! [v1: % 73.94/10.43 vExp] : ! [v2: vName] : (v1 = v0 | ~ (vlookup(v2) = v1) | ~ (vlookup(v2) % 73.94/10.43 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vVal] : (v1 = v0 | ~ % 73.94/10.43 (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & ! [v0: vName] : ! [v1: % 73.94/10.43 vName] : ! [v2: vName] : (v1 = v0 | ~ (venumName(v2) = v1) | ~ % 73.94/10.43 (venumName(v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: % 73.94/10.43 vQuery] : (v1 = v0 | ~ (vsomeQuery(v2) = v1) | ~ (vsomeQuery(v2) = v0)) & % 73.94/10.43 ! [v0: vFType] : ! [v1: vFType] : ! [v2: vFType] : (v1 = v0 | ~ % 73.94/10.43 (venumFType(v2) = v1) | ~ (venumFType(v2) = v0)) & ! [v0: vOptTType] : ! % 73.94/10.43 [v1: vOptTType] : ! [v2: vTType] : (v1 = v0 | ~ (vsomeTType(v2) = v1) | ~ % 73.94/10.43 (vsomeTType(v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! % 73.94/10.43 [v2: vRawTable] : (v1 = v0 | ~ (vsomeRawTable(v2) = v1) | ~ % 73.94/10.43 (vsomeRawTable(v2) = v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! % 73.94/10.43 [v2: vTable] : (v1 = v0 | ~ (vsomeTable(v2) = v1) | ~ (vsomeTable(v2) = v0)) % 73.94/10.43 & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vTable] : (v1 = v0 | ~ % 73.94/10.43 (vtvalue(v2) = v1) | ~ (vtvalue(v2) = v0)) & ! [v0: vSelect] : ! [v1: % 73.94/10.43 vSelect] : ! [v2: vAttrL] : (v1 = v0 | ~ (vlist(v2) = v1) | ~ (vlist(v2) % 73.94/10.43 = v0)) % 73.94/10.43 % 73.94/10.43 Further assumptions not needed in the proof: % 73.94/10.43 -------------------------------------------- % 73.94/10.43 DIFF-Intersection-Difference, DIFF-Union-Difference, DIFF-Union-Intersection, % 73.94/10.43 DIFF-aempty-acons, DIFF-all-list, DIFF-and-eq, DIFF-and-gt, DIFF-and-lt, % 73.94/10.43 DIFF-and-not, DIFF-constant-lookup, DIFF-emptyContext-bindContext, % 73.94/10.43 DIFF-emptyStore-bindStore, DIFF-eq-gt, DIFF-eq-lt, DIFF-gt-lt, % 73.94/10.43 DIFF-initFType-enumFType, DIFF-initName-enumName, DIFF-initVal-enumVal, % 73.94/10.43 DIFF-noFType-someFType, DIFF-noQuery-someQuery, DIFF-noRawTable-someRawTable, % 73.94/10.43 DIFF-noTType-someTType, DIFF-noTable-someTable, DIFF-noVal-someVal, DIFF-not-eq, % 73.94/10.43 DIFF-not-gt, DIFF-not-lt, DIFF-ptrue-and, DIFF-ptrue-eq, DIFF-ptrue-gt, % 73.94/10.43 DIFF-ptrue-lt, DIFF-ptrue-not, DIFF-rempty-rcons, % 73.94/10.43 DIFF-selectFromWhere-Difference, DIFF-selectFromWhere-Intersection, % 73.94/10.43 DIFF-selectFromWhere-Union, DIFF-ttempty-ttcons, DIFF-tvalue-Difference, % 73.94/10.43 DIFF-tvalue-Intersection, DIFF-tvalue-Union, DIFF-tvalue-selectFromWhere, % 73.94/10.43 EQ-Difference, EQ-Intersection, EQ-Union, EQ-acons, EQ-and, EQ-bindContext, % 73.94/10.43 EQ-bindStore, EQ-constant, EQ-enumFType, EQ-enumName, EQ-enumVal, EQ-eq, EQ-gt, % 73.94/10.43 EQ-list, EQ-lookup, EQ-lt, EQ-not, EQ-rcons, EQ-selectFromWhere, EQ-someFType, % 73.94/10.43 EQ-someQuery, EQ-someRawTable, EQ-someTType, EQ-someTable, EQ-someVal, EQ-table, % 73.94/10.43 EQ-ttcons, EQ-tvalue, TDifference, TDifference_inv1, TDifference_inv2, % 73.94/10.43 TIntersection, TIntersection_inv1, TIntersection_inv2, TSelectFromWhere, % 73.94/10.43 TSelectFromWhere_inv, TTTContextDuplicate, TTTContextSwap, TUnion, TUnion_inv1, % 73.94/10.43 TUnion_inv2, Ttvalue, Ttvalue_inv, append-0, append-1, append-INV, % 73.94/10.43 attachColToFrontRaw-0, attachColToFrontRaw-1, attachColToFrontRaw-2, % 73.94/10.43 attachColToFrontRaw-INV, dom-AttrL, dom-Exp, dom-OptFType, dom-OptQuery, % 73.94/10.43 dom-OptRawTable, dom-OptTType, dom-OptTable, dom-OptVal, dom-Pred, dom-Query, % 73.94/10.43 dom-RawTable, dom-Row, dom-Select, dom-TStore, dom-TTContext, dom-TType, % 73.94/10.43 dom-Table, dropFirstColRaw-0, dropFirstColRaw-1, dropFirstColRaw-2, % 73.94/10.43 dropFirstColRaw-INV, evalExpRow-0, evalExpRow-1, evalExpRow-2, evalExpRow-3, % 73.94/10.43 evalExpRow-INV, filterRows-0, filterRows-1, filterRows-2, filterRows-INV, % 73.94/10.43 filterSingleRow-0, filterSingleRow-1, filterSingleRow-2, filterSingleRow-3, % 73.94/10.43 filterSingleRow-4, filterSingleRow-5, filterSingleRow-false-INV, % 73.94/10.43 filterSingleRow-true-INV, filterTable-0, filterTable-INV, findCol-0, findCol-1, % 73.94/10.43 findCol-2, findCol-INV, findColType-0, findColType-1, findColType-2, % 73.94/10.43 findColType-INV, getAttrL-0, getAttrL-INV, getFType-0, getQuery-0, getRaw-0, % 73.94/10.43 getRaw-INV, getRawTable-0, getTType-0, getTable-0, getVal-0, isSomeFType-0, % 73.94/10.43 isSomeFType-1, isSomeFType-false-INV, isSomeFType-true-INV, isSomeQuery-0, % 73.94/10.43 isSomeQuery-1, isSomeQuery-false-INV, isSomeQuery-true-INV, isSomeRawTable-0, % 73.94/10.43 isSomeRawTable-1, isSomeRawTable-false-INV, isSomeRawTable-true-INV, % 73.94/10.43 isSomeTType-0, isSomeTType-1, isSomeTType-false-INV, isSomeTType-true-INV, % 73.94/10.43 isSomeTable-0, isSomeTable-1, isSomeTable-false-INV, isSomeTable-true-INV, % 73.94/10.43 isSomeVal-0, isSomeVal-1, isSomeVal-false-INV, isSomeVal-true-INV, isValue-0, % 73.94/10.43 isValue-1, isValue-2, isValue-3, isValue-4, isValue-false-INV, isValue-true-INV, % 73.94/10.43 lookupContext-0, lookupContext-1, lookupContext-2, lookupContext-INV, % 73.94/10.43 lookupStore-0, lookupStore-1, lookupStore-2, lookupStore-INV, matchingAttrL-0, % 73.94/10.43 matchingAttrL-1, matchingAttrL-2, matchingAttrL-false-INV, % 73.94/10.43 matchingAttrL-true-INV, projectCols-0, projectCols-1, projectCols-2, % 73.94/10.43 projectCols-INV, projectEmptyCol-0, projectEmptyCol-1, projectEmptyCol-INV, % 73.94/10.43 projectFirstRaw-0, projectFirstRaw-1, projectFirstRaw-2, projectFirstRaw-INV, % 73.94/10.43 projectTable-0, projectTable-1, projectTable-2, projectTable-INV, projectType-0, % 73.94/10.43 projectType-1, projectType-INV, projectTypeAttrL-0, projectTypeAttrL-1, % 73.94/10.43 projectTypeAttrL-2, projectTypeAttrL-INV, rawDifference-0, rawDifference-1, % 73.94/10.43 rawDifference-2, rawIntersection-0, rawIntersection-1, rawIntersection-2, % 73.94/10.43 rawIntersection-3, rawIntersection-4, rawIntersection-INV, rawUnion-0, % 73.94/10.43 rawUnion-1, rawUnion-2, rawUnion-INV, reduce-0, reduce-1, reduce-10, reduce-11, % 73.94/10.43 reduce-12, reduce-13, reduce-14, reduce-15, reduce-16, reduce-17, reduce-18, % 73.94/10.43 reduce-2, reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, reduce-8, reduce-9, % 73.94/10.43 reduce-INV, rowIn-1, rowIn-false-INV, rowIn-true-INV, sameLength-0, % 73.94/10.43 sameLength-1, sameLength-2, sameLength-false-INV, sameLength-true-INV, % 73.94/10.43 storeContextConsistent-0, storeContextConsistent-1, storeContextConsistent-2, % 73.94/10.43 storeContextConsistent-false-INV, storeContextConsistent-true-INV, tcheckPred-0, % 73.94/10.43 tcheckPred-1, tcheckPred-2, tcheckPred-3, tcheckPred-4, tcheckPred-5, % 73.94/10.43 tcheckPred-false-INV, tcheckPred-true-INV, typeOfExp-0, typeOfExp-1, % 73.94/10.43 typeOfExp-2, typeOfExp-3, typeOfExp-INV, welltypedRawtable-0, welltypedRow-0, % 73.94/10.43 welltypedRow-1, welltypedRow-2, welltypedRow-false-INV, welltypedRow-true-INV, % 73.94/10.43 welltypedtable-0, welltypedtable-false-INV, welltypedtable-true-INV % 73.94/10.43 % 73.94/10.43 Those formulas are unsatisfiable: % 73.94/10.43 --------------------------------- % 73.94/10.43 % 73.94/10.43 Begin of proof % 73.94/10.43 | % 73.94/10.43 | ALPHA: (EQ-tcons) implies: % 73.94/10.43 | (1) ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRow] : ! [v3: vRawTable] % 73.94/10.43 | : ! [v4: vRawTable] : (v2 = v0 | ~ (vtcons(v2, v3) = v4) | ~ % 73.94/10.43 | (vtcons(v0, v1) = v4) | ~ vRawTable(v3) | ~ vRawTable(v1) | ~ % 73.94/10.43 | vRow(v2) | ~ vRow(v0)) % 73.94/10.44 | (2) ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRow] : ! [v3: vRawTable] % 73.94/10.44 | : ! [v4: vRawTable] : (v3 = v1 | ~ (vtcons(v2, v3) = v4) | ~ % 73.94/10.44 | (vtcons(v0, v1) = v4) | ~ vRawTable(v3) | ~ vRawTable(v1) | ~ % 73.94/10.44 | vRow(v2) | ~ vRow(v0)) % 73.94/10.44 | % 73.94/10.44 | ALPHA: (DIFF-tempty-tcons) implies: % 73.94/10.44 | (3) ! [v0: vRow] : ! [v1: vRawTable] : ( ~ (vtcons(v0, v1) = vtempty) | % 73.94/10.44 | ~ vRawTable(v1) | ~ vRow(v0)) % 73.94/10.44 | % 73.94/10.44 | ALPHA: (welltypedRawtable-1) implies: % 73.94/10.44 | (4) ! [v0: vTType] : ! [v1: vRow] : ! [v2: vRawTable] : ! [v3: % 73.94/10.44 | vRawTable] : ( ~ (vwelltypedRawtable(v0, v3) = 0) | ~ (vtcons(v1, % 73.94/10.44 | v2) = v3) | ~ vTType(v0) | ~ vRawTable(v2) | ~ vRow(v1) | % 73.94/10.44 | (vwelltypedRawtable(v0, v2) = 0 & vwelltypedRow(v0, v1) = 0)) % 73.94/10.44 | % 73.94/10.44 | ALPHA: (welltypedRawtable-true-INV) implies: % 73.94/10.44 | (5) ! [v0: vTType] : ! [v1: vRawTable] : ( ~ (vwelltypedRawtable(v0, v1) % 73.94/10.44 | = 0) | ~ vTType(v0) | ~ vRawTable(v1) | ? [v2: vRow] : ? [v3: % 73.94/10.44 | vRawTable] : ? [v4: vTType] : ? [v5: vRawTable] : ? [v6: int] : % 73.94/10.44 | ? [v7: int] : ? [v8: vTType] : (vTType(v8) & vTType(v4) & % 73.94/10.44 | vRawTable(v3) & vRow(v2) & ((v8 = v0 & v1 = vtempty) | (v7 = 0 & v6 % 73.94/10.44 | = 0 & v5 = v1 & v4 = v0 & vwelltypedRawtable(v0, v3) = 0 & % 73.94/10.44 | vwelltypedRow(v0, v2) = 0 & vtcons(v2, v3) = v1)))) % 73.94/10.44 | % 73.94/10.44 | ALPHA: (rowIn-0) implies: % 73.94/10.44 | (6) ! [v0: vRow] : ( ~ (vrowIn(v0, vtempty) = 0) | ~ vRow(v0)) % 73.94/10.44 | % 73.94/10.44 | ALPHA: (rawDifference-3) implies: % 73.94/10.44 | (7) ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: % 73.94/10.44 | vRawTable] : ! [v4: vRawTable] : ( ~ (vrawDifference(v3, v2) = v4) | % 73.94/10.44 | ~ (vtcons(v0, v1) = v3) | ~ vRawTable(v2) | ~ vRawTable(v1) | ~ % 73.94/10.44 | vRow(v0) | ? [v5: any] : ? [v6: vRawTable] : ? [v7: vRawTable] : % 73.94/10.44 | ? [v8: vRow] : (vRow(v8) & ((v8 = v0 & v1 = vtempty) | % 73.94/10.44 | (vrawDifference(v1, v2) = v6 & vrowIn(v0, v2) = v5 & vtcons(v0, % 73.94/10.44 | v6) = v7 & vRawTable(v7) & vRawTable(v6) & (v7 = v4 | v5 = % 73.94/10.44 | 0))))) % 73.94/10.44 | % 73.94/10.44 | ALPHA: (rawDifference-4) implies: % 73.94/10.44 | (8) ! [v0: vRow] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: % 73.94/10.44 | vRawTable] : ! [v4: vRawTable] : ( ~ (vrawDifference(v3, v2) = v4) | % 73.94/10.44 | ~ (vtcons(v0, v1) = v3) | ~ vRawTable(v2) | ~ vRawTable(v1) | ~ % 73.94/10.44 | vRow(v0) | ? [v5: any] : ? [v6: vRawTable] : ? [v7: vRow] : % 73.94/10.44 | (vRow(v7) & ((v7 = v0 & v1 = vtempty) | (vrawDifference(v1, v2) = v6 % 73.94/10.44 | & vrowIn(v0, v2) = v5 & vRawTable(v6) & ( ~ (v5 = 0) | v6 = % 73.94/10.44 | v4))))) % 73.94/10.44 | % 73.94/10.44 | ALPHA: (rawDifference-INV) implies: % 73.94/10.44 | (9) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ( ~ % 73.94/10.45 | (vrawDifference(v0, v1) = v2) | ~ vRawTable(v1) | ~ vRawTable(v0) | % 73.94/10.45 | ? [v3: vRow] : ? [v4: vRawTable] : ? [v5: vRawTable] : ? [v6: % 73.94/10.45 | vRawTable] : ? [v7: vRawTable] : ? [v8: int] : ? [v9: vRawTable] % 73.94/10.45 | : ? [v10: vRow] : ? [v11: vRawTable] : ? [v12: vRawTable] : ? % 73.94/10.45 | [v13: vRawTable] : ? [v14: vRawTable] : ? [v15: int] : ? [v16: % 73.94/10.45 | vRawTable] : ? [v17: vRawTable] : ? [v18: vRow] : ? [v19: % 73.94/10.45 | vRawTable] : ? [v20: int] : ? [v21: vRawTable] : ? [v22: vRow] : % 73.94/10.45 | ? [v23: vRawTable] : ? [v24: int] : ? [v25: vRawTable] : ? [v26: % 73.94/10.45 | vRawTable] : (vRawTable(v26) & vRawTable(v23) & vRawTable(v19) & % 73.94/10.45 | vRawTable(v13) & vRawTable(v12) & vRawTable(v11) & vRawTable(v6) & % 73.94/10.45 | vRawTable(v5) & vRawTable(v4) & vRow(v22) & vRow(v18) & vRow(v10) & % 73.94/10.45 | vRow(v3) & ((v26 = v1 & v2 = vtempty & v0 = vtempty) | (v25 = v0 & % 73.94/10.45 | v23 = v1 & v2 = v0 & ~ (v24 = 0) & vrowIn(v22, v1) = v24 & % 73.94/10.45 | vtcons(v22, vtempty) = v0) | (v21 = v0 & v20 = 0 & v19 = v1 & % 73.94/10.45 | v2 = vtempty & vrowIn(v18, v1) = 0 & vtcons(v18, vtempty) = v0) % 73.94/10.45 | | (v17 = v2 & v16 = v0 & v14 = v12 & v13 = v1 & ~ (v15 = 0) & ~ % 73.94/10.45 | (v11 = vtempty) & vrawDifference(v11, v1) = v12 & vrowIn(v10, % 73.94/10.45 | v1) = v15 & vtcons(v10, v12) = v2 & vtcons(v10, v11) = v0 & % 73.94/10.45 | vRawTable(v2)) | (v9 = v0 & v8 = 0 & v7 = v2 & v6 = v1 & v5 = % 73.94/10.45 | v2 & ~ (v4 = vtempty) & vrawDifference(v4, v1) = v2 & % 73.94/10.45 | vrowIn(v3, v1) = 0 & vtcons(v3, v4) = v0 & vRawTable(v2))))) % 73.94/10.45 | % 73.94/10.45 | ALPHA: (rawDifferencePreservesWellTypedRaw-tcons-IH0) implies: % 73.94/10.45 | (10) ! [v0: vTType] : ! [v1: vRawTable] : ( ~ (vwelltypedRawtable(v0, v1) % 73.94/10.45 | = 0) | ~ vTType(v0) | ~ vRawTable(v1) | ? [v2: any] : ? [v3: % 73.94/10.45 | vRawTable] : ? [v4: any] : (vrawDifference(vrt2, v1) = v3 & % 73.94/10.45 | vwelltypedRawtable(v0, v3) = v4 & vwelltypedRawtable(v0, vrt2) = % 73.94/10.45 | v2 & vRawTable(v3) & ( ~ (v2 = 0) | v4 = 0))) % 73.94/10.45 | % 73.94/10.45 | ALPHA: (rawDifferencePreservesWellTypedRaw-tcons-tempty-rowIn-False) implies: % 73.94/10.45 | (11) vRawTable(vtempty) % 73.94/10.45 | (12) vRawTable(vrt2) % 73.94/10.45 | (13) ? [v0: vRow] : ? [v1: vTType] : ? [v2: vRawTable] : ? [v3: % 73.94/10.45 | vRawTable] : ? [v4: int] : ( ~ (v4 = 0) & vrawDifference(v2, % 73.94/10.45 | vtempty) = v3 & vrowIn(v0, vrt2) = 0 & vwelltypedRawtable(v1, v3) % 73.94/10.45 | = v4 & vwelltypedRawtable(v1, v2) = 0 & vwelltypedRawtable(v1, % 73.94/10.45 | vtempty) = 0 & vtcons(v0, vrt2) = v2 & vTType(v1) & vRawTable(v3) % 73.94/10.45 | & vRawTable(v2) & vRow(v0)) % 73.94/10.45 | % 73.94/10.45 | ALPHA: (function-axioms) implies: % 73.94/10.45 | (14) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 73.94/10.45 | vRow] : ! [v3: vTType] : (v1 = v0 | ~ (vwelltypedRow(v3, v2) = v1) % 73.94/10.45 | | ~ (vwelltypedRow(v3, v2) = v0)) % 73.94/10.45 | (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 73.94/10.45 | vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ (vwelltypedRawtable(v3, % 73.94/10.45 | v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) % 73.94/10.45 | (16) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: % 73.94/10.45 | vRawTable] : (v1 = v0 | ~ (vrawDifference(v3, v2) = v1) | ~ % 73.94/10.45 | (vrawDifference(v3, v2) = v0)) % 73.94/10.45 | % 73.94/10.45 | DELTA: instantiating (13) with fresh symbols all_332_0, all_332_1, all_332_2, % 73.94/10.45 | all_332_3, all_332_4 gives: % 73.94/10.45 | (17) ~ (all_332_0 = 0) & vrawDifference(all_332_2, vtempty) = all_332_1 & % 73.94/10.45 | vrowIn(all_332_4, vrt2) = 0 & vwelltypedRawtable(all_332_3, all_332_1) % 73.94/10.45 | = all_332_0 & vwelltypedRawtable(all_332_3, all_332_2) = 0 & % 73.94/10.45 | vwelltypedRawtable(all_332_3, vtempty) = 0 & vtcons(all_332_4, vrt2) = % 73.94/10.45 | all_332_2 & vTType(all_332_3) & vRawTable(all_332_1) & % 73.94/10.45 | vRawTable(all_332_2) & vRow(all_332_4) % 73.94/10.45 | % 73.94/10.45 | ALPHA: (17) implies: % 73.94/10.45 | (18) ~ (all_332_0 = 0) % 73.94/10.45 | (19) vRow(all_332_4) % 73.94/10.45 | (20) vRawTable(all_332_2) % 73.94/10.45 | (21) vRawTable(all_332_1) % 73.94/10.45 | (22) vTType(all_332_3) % 73.94/10.45 | (23) vtcons(all_332_4, vrt2) = all_332_2 % 73.94/10.45 | (24) vwelltypedRawtable(all_332_3, vtempty) = 0 % 73.94/10.45 | (25) vwelltypedRawtable(all_332_3, all_332_2) = 0 % 73.94/10.45 | (26) vwelltypedRawtable(all_332_3, all_332_1) = all_332_0 % 73.94/10.45 | (27) vrawDifference(all_332_2, vtempty) = all_332_1 % 73.94/10.45 | % 73.94/10.45 | GROUND_INST: instantiating (10) with all_332_3, vtempty, simplifying with % 73.94/10.45 | (11), (22), (24) gives: % 73.94/10.46 | (28) ? [v0: any] : ? [v1: vRawTable] : ? [v2: any] : % 73.94/10.46 | (vrawDifference(vrt2, vtempty) = v1 & vwelltypedRawtable(all_332_3, % 73.94/10.46 | v1) = v2 & vwelltypedRawtable(all_332_3, vrt2) = v0 & % 73.94/10.46 | vRawTable(v1) & ( ~ (v0 = 0) | v2 = 0)) % 73.94/10.46 | % 73.94/10.46 | GROUND_INST: instantiating (4) with all_332_3, all_332_4, vrt2, all_332_2, % 73.94/10.46 | simplifying with (12), (19), (22), (23), (25) gives: % 73.94/10.46 | (29) vwelltypedRawtable(all_332_3, vrt2) = 0 & vwelltypedRow(all_332_3, % 73.94/10.46 | all_332_4) = 0 % 73.94/10.46 | % 73.94/10.46 | ALPHA: (29) implies: % 73.94/10.46 | (30) vwelltypedRawtable(all_332_3, vrt2) = 0 % 73.94/10.46 | % 73.94/10.46 | GROUND_INST: instantiating (5) with all_332_3, all_332_2, simplifying with % 73.94/10.46 | (20), (22), (25) gives: % 73.94/10.46 | (31) ? [v0: vRow] : ? [v1: vRawTable] : ? [v2: vTType] : ? [v3: int] : % 73.94/10.46 | ? [v4: int] : ? [v5: int] : ? [v6: vTType] : (vTType(v6) & % 73.94/10.46 | vTType(v2) & vRawTable(v1) & vRow(v0) & ((v6 = all_332_3 & all_332_2 % 73.94/10.46 | = vtempty) | (v5 = 0 & v4 = 0 & v3 = all_332_2 & v2 = all_332_3 % 73.94/10.46 | & vwelltypedRawtable(all_332_3, v1) = 0 & % 73.94/10.46 | vwelltypedRow(all_332_3, v0) = 0 & vtcons(v0, v1) = all_332_2))) % 73.94/10.46 | % 73.94/10.46 | GROUND_INST: instantiating (10) with all_332_3, all_332_2, simplifying with % 73.94/10.46 | (20), (22), (25) gives: % 73.94/10.46 | (32) ? [v0: any] : ? [v1: vRawTable] : ? [v2: any] : % 73.94/10.46 | (vrawDifference(vrt2, all_332_2) = v1 & vwelltypedRawtable(all_332_3, % 73.94/10.46 | v1) = v2 & vwelltypedRawtable(all_332_3, vrt2) = v0 & % 73.94/10.46 | vRawTable(v1) & ( ~ (v0 = 0) | v2 = 0)) % 73.94/10.46 | % 73.94/10.46 | GROUND_INST: instantiating (welltypedRawtable-false-INV) with all_332_3, % 73.94/10.46 | all_332_1, all_332_0, simplifying with (21), (22), (26) gives: % 73.94/10.46 | (33) all_332_0 = 0 | ? [v0: vRow] : ? [v1: vRawTable] : ? [v2: any] : ? % 73.94/10.46 | [v3: any] : (vwelltypedRawtable(all_332_3, v1) = v3 & % 73.94/10.46 | vwelltypedRow(all_332_3, v0) = v2 & vtcons(v0, v1) = all_332_1 & % 73.94/10.46 | vRawTable(v1) & vRow(v0) & ( ~ (v3 = 0) | ~ (v2 = 0))) % 73.94/10.46 | % 73.94/10.46 | GROUND_INST: instantiating (9) with all_332_2, vtempty, all_332_1, simplifying % 73.94/10.46 | with (11), (20), (27) gives: % 73.94/10.46 | (34) ? [v0: vRow] : ? [v1: vRawTable] : ? [v2: vRawTable] : ? [v3: % 73.94/10.46 | vRawTable] : ? [v4: int] : ? [v5: int] : ? [v6: int] : ? [v7: % 73.94/10.46 | vRow] : ? [v8: vRawTable] : ? [v9: vRawTable] : ? [v10: % 73.94/10.46 | vRawTable] : ? [v11: vRawTable] : ? [v12: int] : ? [v13: int] : % 73.94/10.46 | ? [v14: int] : ? [v15: vRow] : ? [v16: vRawTable] : ? [v17: int] : % 73.94/10.46 | ? [v18: int] : ? [v19: vRow] : ? [v20: vRawTable] : ? [v21: int] : % 73.94/10.46 | ? [v22: int] : ? [v23: vRawTable] : (vRawTable(v23) & vRawTable(v20) % 73.94/10.46 | & vRawTable(v16) & vRawTable(v10) & vRawTable(v9) & vRawTable(v8) & % 73.94/10.46 | vRawTable(v3) & vRawTable(v2) & vRawTable(v1) & vRow(v19) & % 73.94/10.46 | vRow(v15) & vRow(v7) & vRow(v0) & ((v23 = vtempty & all_332_1 = % 73.94/10.46 | vtempty & all_332_2 = vtempty) | (v22 = all_332_2 & v20 = % 73.94/10.46 | vtempty & all_332_1 = all_332_2 & ~ (v21 = 0) & vrowIn(v19, % 73.94/10.46 | vtempty) = v21 & vtcons(v19, vtempty) = all_332_2) | (v18 = % 73.94/10.46 | all_332_2 & v17 = 0 & v16 = vtempty & all_332_1 = vtempty & % 73.94/10.46 | vrowIn(v15, vtempty) = 0 & vtcons(v15, vtempty) = all_332_2) | % 73.94/10.46 | (v14 = all_332_1 & v13 = all_332_2 & v11 = v9 & v10 = vtempty & ~ % 73.94/10.46 | (v12 = 0) & ~ (v8 = vtempty) & vrawDifference(v8, vtempty) = v9 % 73.94/10.46 | & vrowIn(v7, vtempty) = v12 & vtcons(v7, v9) = all_332_1 & % 73.94/10.46 | vtcons(v7, v8) = all_332_2 & vRawTable(all_332_1)) | (v6 = % 73.94/10.46 | all_332_2 & v5 = 0 & v4 = all_332_1 & v3 = vtempty & v2 = % 73.94/10.46 | all_332_1 & ~ (v1 = vtempty) & vrawDifference(v1, vtempty) = % 73.94/10.46 | all_332_1 & vrowIn(v0, vtempty) = 0 & vtcons(v0, v1) = all_332_2 % 73.94/10.46 | & vRawTable(all_332_1)))) % 73.94/10.46 | % 73.94/10.46 | DELTA: instantiating (28) with fresh symbols all_371_0, all_371_1, all_371_2 % 73.94/10.46 | gives: % 73.94/10.46 | (35) vrawDifference(vrt2, vtempty) = all_371_1 & % 73.94/10.46 | vwelltypedRawtable(all_332_3, all_371_1) = all_371_0 & % 73.94/10.46 | vwelltypedRawtable(all_332_3, vrt2) = all_371_2 & vRawTable(all_371_1) % 73.94/10.46 | & ( ~ (all_371_2 = 0) | all_371_0 = 0) % 73.94/10.46 | % 73.94/10.46 | ALPHA: (35) implies: % 73.94/10.46 | (36) vwelltypedRawtable(all_332_3, vrt2) = all_371_2 % 73.94/10.46 | (37) vwelltypedRawtable(all_332_3, all_371_1) = all_371_0 % 73.94/10.46 | (38) vrawDifference(vrt2, vtempty) = all_371_1 % 73.94/10.46 | (39) ~ (all_371_2 = 0) | all_371_0 = 0 % 73.94/10.46 | % 73.94/10.46 | DELTA: instantiating (32) with fresh symbols all_373_0, all_373_1, all_373_2 % 73.94/10.46 | gives: % 73.94/10.46 | (40) vrawDifference(vrt2, all_332_2) = all_373_1 & % 73.94/10.46 | vwelltypedRawtable(all_332_3, all_373_1) = all_373_0 & % 73.94/10.46 | vwelltypedRawtable(all_332_3, vrt2) = all_373_2 & vRawTable(all_373_1) % 73.94/10.46 | & ( ~ (all_373_2 = 0) | all_373_0 = 0) % 73.94/10.46 | % 73.94/10.46 | ALPHA: (40) implies: % 73.94/10.46 | (41) vwelltypedRawtable(all_332_3, vrt2) = all_373_2 % 73.94/10.46 | % 73.94/10.46 | DELTA: instantiating (31) with fresh symbols all_383_0, all_383_1, all_383_2, % 73.94/10.46 | all_383_3, all_383_4, all_383_5, all_383_6 gives: % 73.94/10.46 | (42) vTType(all_383_0) & vTType(all_383_4) & vRawTable(all_383_5) & % 73.94/10.46 | vRow(all_383_6) & ((all_383_0 = all_332_3 & all_332_2 = vtempty) | % 73.94/10.46 | (all_383_1 = 0 & all_383_2 = 0 & all_383_3 = all_332_2 & all_383_4 = % 73.94/10.46 | all_332_3 & vwelltypedRawtable(all_332_3, all_383_5) = 0 & % 73.94/10.46 | vwelltypedRow(all_332_3, all_383_6) = 0 & vtcons(all_383_6, % 73.94/10.46 | all_383_5) = all_332_2)) % 73.94/10.46 | % 73.94/10.46 | ALPHA: (42) implies: % 73.94/10.46 | (43) vRow(all_383_6) % 73.94/10.47 | (44) vRawTable(all_383_5) % 73.94/10.47 | (45) (all_383_0 = all_332_3 & all_332_2 = vtempty) | (all_383_1 = 0 & % 73.94/10.47 | all_383_2 = 0 & all_383_3 = all_332_2 & all_383_4 = all_332_3 & % 73.94/10.47 | vwelltypedRawtable(all_332_3, all_383_5) = 0 & % 73.94/10.47 | vwelltypedRow(all_332_3, all_383_6) = 0 & vtcons(all_383_6, % 73.94/10.47 | all_383_5) = all_332_2) % 73.94/10.47 | % 73.94/10.47 | DELTA: instantiating (34) with fresh symbols all_385_0, all_385_1, all_385_2, % 73.94/10.47 | all_385_3, all_385_4, all_385_5, all_385_6, all_385_7, all_385_8, % 73.94/10.47 | all_385_9, all_385_10, all_385_11, all_385_12, all_385_13, all_385_14, % 73.94/10.47 | all_385_15, all_385_16, all_385_17, all_385_18, all_385_19, all_385_20, % 73.94/10.47 | all_385_21, all_385_22, all_385_23 gives: % 73.94/10.47 | (46) vRawTable(all_385_0) & vRawTable(all_385_3) & vRawTable(all_385_7) & % 73.94/10.47 | vRawTable(all_385_13) & vRawTable(all_385_14) & vRawTable(all_385_15) % 73.94/10.47 | & vRawTable(all_385_20) & vRawTable(all_385_21) & % 73.94/10.47 | vRawTable(all_385_22) & vRow(all_385_4) & vRow(all_385_8) & % 73.94/10.47 | vRow(all_385_16) & vRow(all_385_23) & ((all_385_0 = vtempty & % 73.94/10.47 | all_332_1 = vtempty & all_332_2 = vtempty) | (all_385_1 = % 73.94/10.47 | all_332_2 & all_385_3 = vtempty & all_332_1 = all_332_2 & ~ % 73.94/10.47 | (all_385_2 = 0) & vrowIn(all_385_4, vtempty) = all_385_2 & % 73.94/10.47 | vtcons(all_385_4, vtempty) = all_332_2) | (all_385_5 = all_332_2 & % 73.94/10.47 | all_385_6 = 0 & all_385_7 = vtempty & all_332_1 = vtempty & % 73.94/10.47 | vrowIn(all_385_8, vtempty) = 0 & vtcons(all_385_8, vtempty) = % 73.94/10.47 | all_332_2) | (all_385_9 = all_332_1 & all_385_10 = all_332_2 & % 73.94/10.47 | all_385_12 = all_385_14 & all_385_13 = vtempty & ~ (all_385_11 = % 73.94/10.47 | 0) & ~ (all_385_15 = vtempty) & vrawDifference(all_385_15, % 73.94/10.47 | vtempty) = all_385_14 & vrowIn(all_385_16, vtempty) = all_385_11 % 73.94/10.47 | & vtcons(all_385_16, all_385_14) = all_332_1 & vtcons(all_385_16, % 73.94/10.47 | all_385_15) = all_332_2 & vRawTable(all_332_1)) | (all_385_17 = % 73.94/10.47 | all_332_2 & all_385_18 = 0 & all_385_19 = all_332_1 & all_385_20 = % 73.94/10.47 | vtempty & all_385_21 = all_332_1 & ~ (all_385_22 = vtempty) & % 73.94/10.47 | vrawDifference(all_385_22, vtempty) = all_332_1 & % 73.94/10.47 | vrowIn(all_385_23, vtempty) = 0 & vtcons(all_385_23, all_385_22) = % 73.94/10.47 | all_332_2 & vRawTable(all_332_1))) % 73.94/10.47 | % 73.94/10.47 | ALPHA: (46) implies: % 73.94/10.47 | (47) vRow(all_385_23) % 73.94/10.47 | (48) vRow(all_385_16) % 73.94/10.47 | (49) vRawTable(all_385_15) % 73.94/10.47 | (50) vRawTable(all_385_14) % 73.94/10.47 | (51) vRawTable(all_385_13) % 73.94/10.47 | (52) (all_385_0 = vtempty & all_332_1 = vtempty & all_332_2 = vtempty) | % 73.94/10.47 | (all_385_1 = all_332_2 & all_385_3 = vtempty & all_332_1 = all_332_2 & % 73.94/10.47 | ~ (all_385_2 = 0) & vrowIn(all_385_4, vtempty) = all_385_2 & % 73.94/10.47 | vtcons(all_385_4, vtempty) = all_332_2) | (all_385_5 = all_332_2 & % 73.94/10.47 | all_385_6 = 0 & all_385_7 = vtempty & all_332_1 = vtempty & % 73.94/10.47 | vrowIn(all_385_8, vtempty) = 0 & vtcons(all_385_8, vtempty) = % 73.94/10.47 | all_332_2) | (all_385_9 = all_332_1 & all_385_10 = all_332_2 & % 73.94/10.47 | all_385_12 = all_385_14 & all_385_13 = vtempty & ~ (all_385_11 = 0) % 73.94/10.47 | & ~ (all_385_15 = vtempty) & vrawDifference(all_385_15, vtempty) = % 73.94/10.47 | all_385_14 & vrowIn(all_385_16, vtempty) = all_385_11 & % 73.94/10.47 | vtcons(all_385_16, all_385_14) = all_332_1 & vtcons(all_385_16, % 73.94/10.47 | all_385_15) = all_332_2 & vRawTable(all_332_1)) | (all_385_17 = % 73.94/10.47 | all_332_2 & all_385_18 = 0 & all_385_19 = all_332_1 & all_385_20 = % 73.94/10.47 | vtempty & all_385_21 = all_332_1 & ~ (all_385_22 = vtempty) & % 73.94/10.47 | vrawDifference(all_385_22, vtempty) = all_332_1 & vrowIn(all_385_23, % 73.94/10.47 | vtempty) = 0 & vtcons(all_385_23, all_385_22) = all_332_2 & % 73.94/10.47 | vRawTable(all_332_1)) % 73.94/10.47 | % 73.94/10.47 | BETA: splitting (33) gives: % 73.94/10.47 | % 73.94/10.47 | Case 1: % 73.94/10.47 | | % 73.94/10.47 | | (53) all_332_0 = 0 % 73.94/10.47 | | % 73.94/10.47 | | REDUCE: (18), (53) imply: % 73.94/10.47 | | (54) $false % 73.94/10.47 | | % 73.94/10.47 | | CLOSE: (54) is inconsistent. % 73.94/10.47 | | % 73.94/10.47 | Case 2: % 73.94/10.47 | | % 73.94/10.47 | | (55) ? [v0: vRow] : ? [v1: vRawTable] : ? [v2: any] : ? [v3: any] : % 73.94/10.47 | | (vwelltypedRawtable(all_332_3, v1) = v3 & vwelltypedRow(all_332_3, % 73.94/10.47 | | v0) = v2 & vtcons(v0, v1) = all_332_1 & vRawTable(v1) & vRow(v0) % 73.94/10.47 | | & ( ~ (v3 = 0) | ~ (v2 = 0))) % 73.94/10.47 | | % 73.94/10.47 | | DELTA: instantiating (55) with fresh symbols all_391_0, all_391_1, % 73.94/10.47 | | all_391_2, all_391_3 gives: % 73.94/10.47 | | (56) vwelltypedRawtable(all_332_3, all_391_2) = all_391_0 & % 73.94/10.47 | | vwelltypedRow(all_332_3, all_391_3) = all_391_1 & vtcons(all_391_3, % 73.94/10.47 | | all_391_2) = all_332_1 & vRawTable(all_391_2) & vRow(all_391_3) & % 73.94/10.47 | | ( ~ (all_391_0 = 0) | ~ (all_391_1 = 0)) % 73.94/10.47 | | % 73.94/10.47 | | ALPHA: (56) implies: % 73.94/10.47 | | (57) vRow(all_391_3) % 73.94/10.47 | | (58) vRawTable(all_391_2) % 73.94/10.47 | | (59) vtcons(all_391_3, all_391_2) = all_332_1 % 73.94/10.47 | | (60) vwelltypedRow(all_332_3, all_391_3) = all_391_1 % 73.94/10.47 | | (61) vwelltypedRawtable(all_332_3, all_391_2) = all_391_0 % 73.94/10.47 | | (62) ~ (all_391_0 = 0) | ~ (all_391_1 = 0) % 73.94/10.47 | | % 73.94/10.47 | | GROUND_INST: instantiating (15) with all_371_2, all_373_2, vrt2, all_332_3, % 73.94/10.47 | | simplifying with (36), (41) gives: % 73.94/10.47 | | (63) all_373_2 = all_371_2 % 73.94/10.47 | | % 73.94/10.47 | | GROUND_INST: instantiating (15) with 0, all_373_2, vrt2, all_332_3, % 73.94/10.47 | | simplifying with (30), (41) gives: % 73.94/10.47 | | (64) all_373_2 = 0 % 73.94/10.47 | | % 73.94/10.47 | | COMBINE_EQS: (63), (64) imply: % 73.94/10.47 | | (65) all_371_2 = 0 % 73.94/10.47 | | % 73.94/10.47 | | SIMP: (65) implies: % 73.94/10.47 | | (66) all_371_2 = 0 % 73.94/10.47 | | % 73.94/10.47 | | BETA: splitting (39) gives: % 73.94/10.47 | | % 73.94/10.47 | | Case 1: % 73.94/10.47 | | | % 73.94/10.47 | | | (67) ~ (all_371_2 = 0) % 73.94/10.47 | | | % 73.94/10.47 | | | REDUCE: (66), (67) imply: % 73.94/10.47 | | | (68) $false % 73.94/10.47 | | | % 73.94/10.47 | | | CLOSE: (68) is inconsistent. % 73.94/10.47 | | | % 73.94/10.47 | | Case 2: % 73.94/10.47 | | | % 73.94/10.47 | | | (69) all_371_0 = 0 % 73.94/10.47 | | | % 73.94/10.47 | | | REDUCE: (37), (69) imply: % 73.94/10.47 | | | (70) vwelltypedRawtable(all_332_3, all_371_1) = 0 % 73.94/10.48 | | | % 73.94/10.48 | | | BETA: splitting (45) gives: % 73.94/10.48 | | | % 73.94/10.48 | | | Case 1: % 73.94/10.48 | | | | % 73.94/10.48 | | | | (71) all_383_0 = all_332_3 & all_332_2 = vtempty % 73.94/10.48 | | | | % 73.94/10.48 | | | | ALPHA: (71) implies: % 73.94/10.48 | | | | (72) all_332_2 = vtempty % 73.94/10.48 | | | | % 73.94/10.48 | | | | REDUCE: (23), (72) imply: % 73.94/10.48 | | | | (73) vtcons(all_332_4, vrt2) = vtempty % 73.94/10.48 | | | | % 73.94/10.48 | | | | GROUND_INST: instantiating (3) with all_332_4, vrt2, simplifying with % 73.94/10.48 | | | | (12), (19), (73) gives: % 73.94/10.48 | | | | (74) $false % 73.94/10.48 | | | | % 73.94/10.48 | | | | CLOSE: (74) is inconsistent. % 73.94/10.48 | | | | % 73.94/10.48 | | | Case 2: % 73.94/10.48 | | | | % 73.94/10.48 | | | | (75) all_383_1 = 0 & all_383_2 = 0 & all_383_3 = all_332_2 & % 73.94/10.48 | | | | all_383_4 = all_332_3 & vwelltypedRawtable(all_332_3, all_383_5) % 73.94/10.48 | | | | = 0 & vwelltypedRow(all_332_3, all_383_6) = 0 & % 73.94/10.48 | | | | vtcons(all_383_6, all_383_5) = all_332_2 % 73.94/10.48 | | | | % 73.94/10.48 | | | | ALPHA: (75) implies: % 73.94/10.48 | | | | (76) vtcons(all_383_6, all_383_5) = all_332_2 % 73.94/10.48 | | | | (77) vwelltypedRow(all_332_3, all_383_6) = 0 % 73.94/10.48 | | | | % 73.94/10.48 | | | | BETA: splitting (62) gives: % 73.94/10.48 | | | | % 73.94/10.48 | | | | Case 1: % 73.94/10.48 | | | | | % 73.94/10.48 | | | | | (78) ~ (all_391_0 = 0) % 73.94/10.48 | | | | | % 73.94/10.48 | | | | | BETA: splitting (52) gives: % 73.94/10.48 | | | | | % 73.94/10.48 | | | | | Case 1: % 73.94/10.48 | | | | | | % 73.94/10.48 | | | | | | (79) (all_385_0 = vtempty & all_332_1 = vtempty & all_332_2 = % 73.94/10.48 | | | | | | vtempty) | (all_385_1 = all_332_2 & all_385_3 = vtempty & % 73.94/10.48 | | | | | | all_332_1 = all_332_2 & ~ (all_385_2 = 0) & % 73.94/10.48 | | | | | | vrowIn(all_385_4, vtempty) = all_385_2 & vtcons(all_385_4, % 73.94/10.48 | | | | | | vtempty) = all_332_2) % 73.94/10.48 | | | | | | % 73.94/10.48 | | | | | | BETA: splitting (79) gives: % 73.94/10.48 | | | | | | % 73.94/10.48 | | | | | | Case 1: % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | (80) all_385_0 = vtempty & all_332_1 = vtempty & all_332_2 = % 73.94/10.48 | | | | | | | vtempty % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | ALPHA: (80) implies: % 73.94/10.48 | | | | | | | (81) all_332_2 = vtempty % 73.94/10.48 | | | | | | | (82) all_332_1 = vtempty % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | REDUCE: (26), (82) imply: % 73.94/10.48 | | | | | | | (83) vwelltypedRawtable(all_332_3, vtempty) = all_332_0 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | GROUND_INST: instantiating (15) with 0, all_332_0, vtempty, % 73.94/10.48 | | | | | | | all_332_3, simplifying with (24), (83) gives: % 73.94/10.48 | | | | | | | (84) all_332_0 = 0 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | REDUCE: (18), (84) imply: % 73.94/10.48 | | | | | | | (85) $false % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | CLOSE: (85) is inconsistent. % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | Case 2: % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | (86) all_385_1 = all_332_2 & all_385_3 = vtempty & all_332_1 = % 73.94/10.48 | | | | | | | all_332_2 & ~ (all_385_2 = 0) & vrowIn(all_385_4, % 73.94/10.48 | | | | | | | vtempty) = all_385_2 & vtcons(all_385_4, vtempty) = % 73.94/10.48 | | | | | | | all_332_2 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | ALPHA: (86) implies: % 73.94/10.48 | | | | | | | (87) all_332_1 = all_332_2 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | REDUCE: (26), (87) imply: % 73.94/10.48 | | | | | | | (88) vwelltypedRawtable(all_332_3, all_332_2) = all_332_0 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | GROUND_INST: instantiating (15) with 0, all_332_0, all_332_2, % 73.94/10.48 | | | | | | | all_332_3, simplifying with (25), (88) gives: % 73.94/10.48 | | | | | | | (89) all_332_0 = 0 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | REDUCE: (18), (89) imply: % 73.94/10.48 | | | | | | | (90) $false % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | CLOSE: (90) is inconsistent. % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | End of split % 73.94/10.48 | | | | | | % 73.94/10.48 | | | | | Case 2: % 73.94/10.48 | | | | | | % 73.94/10.48 | | | | | | (91) (all_385_5 = all_332_2 & all_385_6 = 0 & all_385_7 = vtempty % 73.94/10.48 | | | | | | & all_332_1 = vtempty & vrowIn(all_385_8, vtempty) = 0 & % 73.94/10.48 | | | | | | vtcons(all_385_8, vtempty) = all_332_2) | (all_385_9 = % 73.94/10.48 | | | | | | all_332_1 & all_385_10 = all_332_2 & all_385_12 = % 73.94/10.48 | | | | | | all_385_14 & all_385_13 = vtempty & ~ (all_385_11 = 0) & % 73.94/10.48 | | | | | | ~ (all_385_15 = vtempty) & vrawDifference(all_385_15, % 73.94/10.48 | | | | | | vtempty) = all_385_14 & vrowIn(all_385_16, vtempty) = % 73.94/10.48 | | | | | | all_385_11 & vtcons(all_385_16, all_385_14) = all_332_1 & % 73.94/10.48 | | | | | | vtcons(all_385_16, all_385_15) = all_332_2 & % 73.94/10.48 | | | | | | vRawTable(all_332_1)) | (all_385_17 = all_332_2 & % 73.94/10.48 | | | | | | all_385_18 = 0 & all_385_19 = all_332_1 & all_385_20 = % 73.94/10.48 | | | | | | vtempty & all_385_21 = all_332_1 & ~ (all_385_22 = % 73.94/10.48 | | | | | | vtempty) & vrawDifference(all_385_22, vtempty) = % 73.94/10.48 | | | | | | all_332_1 & vrowIn(all_385_23, vtempty) = 0 & % 73.94/10.48 | | | | | | vtcons(all_385_23, all_385_22) = all_332_2 & % 73.94/10.48 | | | | | | vRawTable(all_332_1)) % 73.94/10.48 | | | | | | % 73.94/10.48 | | | | | | BETA: splitting (91) gives: % 73.94/10.48 | | | | | | % 73.94/10.48 | | | | | | Case 1: % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | (92) all_385_5 = all_332_2 & all_385_6 = 0 & all_385_7 = % 73.94/10.48 | | | | | | | vtempty & all_332_1 = vtempty & vrowIn(all_385_8, vtempty) % 73.94/10.48 | | | | | | | = 0 & vtcons(all_385_8, vtempty) = all_332_2 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | ALPHA: (92) implies: % 73.94/10.48 | | | | | | | (93) all_332_1 = vtempty % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | REDUCE: (26), (93) imply: % 73.94/10.48 | | | | | | | (94) vwelltypedRawtable(all_332_3, vtempty) = all_332_0 % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | REF_CLOSE: (15), (18), (24), (94) are inconsistent by sub-proof % 73.94/10.48 | | | | | | | #1. % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | Case 2: % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | (95) (all_385_9 = all_332_1 & all_385_10 = all_332_2 & % 73.94/10.48 | | | | | | | all_385_12 = all_385_14 & all_385_13 = vtempty & ~ % 73.94/10.48 | | | | | | | (all_385_11 = 0) & ~ (all_385_15 = vtempty) & % 73.94/10.48 | | | | | | | vrawDifference(all_385_15, vtempty) = all_385_14 & % 73.94/10.48 | | | | | | | vrowIn(all_385_16, vtempty) = all_385_11 & % 73.94/10.48 | | | | | | | vtcons(all_385_16, all_385_14) = all_332_1 & % 73.94/10.48 | | | | | | | vtcons(all_385_16, all_385_15) = all_332_2 & % 73.94/10.48 | | | | | | | vRawTable(all_332_1)) | (all_385_17 = all_332_2 & % 73.94/10.48 | | | | | | | all_385_18 = 0 & all_385_19 = all_332_1 & all_385_20 = % 73.94/10.48 | | | | | | | vtempty & all_385_21 = all_332_1 & ~ (all_385_22 = % 73.94/10.48 | | | | | | | vtempty) & vrawDifference(all_385_22, vtempty) = % 73.94/10.48 | | | | | | | all_332_1 & vrowIn(all_385_23, vtempty) = 0 & % 73.94/10.48 | | | | | | | vtcons(all_385_23, all_385_22) = all_332_2 & % 73.94/10.48 | | | | | | | vRawTable(all_332_1)) % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | BETA: splitting (95) gives: % 73.94/10.48 | | | | | | | % 73.94/10.48 | | | | | | | Case 1: % 73.94/10.48 | | | | | | | | % 73.94/10.48 | | | | | | | | (96) all_385_9 = all_332_1 & all_385_10 = all_332_2 & % 73.94/10.48 | | | | | | | | all_385_12 = all_385_14 & all_385_13 = vtempty & ~ % 73.94/10.48 | | | | | | | | (all_385_11 = 0) & ~ (all_385_15 = vtempty) & % 73.94/10.48 | | | | | | | | vrawDifference(all_385_15, vtempty) = all_385_14 & % 73.94/10.48 | | | | | | | | vrowIn(all_385_16, vtempty) = all_385_11 & % 73.94/10.48 | | | | | | | | vtcons(all_385_16, all_385_14) = all_332_1 & % 73.94/10.48 | | | | | | | | vtcons(all_385_16, all_385_15) = all_332_2 & % 73.94/10.48 | | | | | | | | vRawTable(all_332_1) % 73.94/10.48 | | | | | | | | % 73.94/10.48 | | | | | | | | ALPHA: (96) implies: % 73.94/10.48 | | | | | | | | (97) all_385_13 = vtempty % 73.94/10.48 | | | | | | | | (98) ~ (all_385_15 = vtempty) % 73.94/10.48 | | | | | | | | (99) vtcons(all_385_16, all_385_15) = all_332_2 % 73.94/10.48 | | | | | | | | (100) vtcons(all_385_16, all_385_14) = all_332_1 % 73.94/10.48 | | | | | | | | (101) vrawDifference(all_385_15, vtempty) = all_385_14 % 73.94/10.48 | | | | | | | | % 73.94/10.48 | | | | | | | | GROUND_INST: instantiating (7) with all_383_6, all_383_5, % 73.94/10.48 | | | | | | | | vtempty, all_332_2, all_332_1, simplifying with % 73.94/10.48 | | | | | | | | (11), (27), (43), (44), (76) gives: % 73.94/10.49 | | | | | | | | (102) ? [v0: any] : ? [v1: vRawTable] : ? [v2: vRawTable] % 73.94/10.49 | | | | | | | | : ? [v3: vRow] : (vRow(v3) & ((v3 = all_383_6 & % 73.94/10.49 | | | | | | | | all_383_5 = vtempty) | (vrawDifference(all_383_5, % 73.94/10.49 | | | | | | | | vtempty) = v1 & vrowIn(all_383_6, vtempty) = v0 % 73.94/10.49 | | | | | | | | & vtcons(all_383_6, v1) = v2 & vRawTable(v2) & % 73.94/10.49 | | | | | | | | vRawTable(v1) & (v2 = all_332_1 | v0 = 0)))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | GROUND_INST: instantiating (8) with all_383_6, all_383_5, % 73.94/10.49 | | | | | | | | vtempty, all_332_2, all_332_1, simplifying with % 73.94/10.49 | | | | | | | | (11), (27), (43), (44), (76) gives: % 73.94/10.49 | | | | | | | | (103) ? [v0: any] : ? [v1: vRawTable] : ? [v2: vRow] : % 73.94/10.49 | | | | | | | | (vRow(v2) & ((v2 = all_383_6 & all_383_5 = vtempty) | % 73.94/10.49 | | | | | | | | (vrawDifference(all_383_5, vtempty) = v1 & % 73.94/10.49 | | | | | | | | vrowIn(all_383_6, vtempty) = v0 & vRawTable(v1) & % 73.94/10.49 | | | | | | | | ( ~ (v0 = 0) | v1 = all_332_1)))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | GROUND_INST: instantiating (2) with all_332_4, vrt2, all_385_16, % 73.94/10.49 | | | | | | | | all_385_15, all_332_2, simplifying with (12), (19), % 73.94/10.49 | | | | | | | | (23), (48), (49), (99) gives: % 73.94/10.49 | | | | | | | | (104) all_385_15 = vrt2 % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | GROUND_INST: instantiating (2) with all_383_6, all_383_5, % 73.94/10.49 | | | | | | | | all_385_16, all_385_15, all_332_2, simplifying with % 73.94/10.49 | | | | | | | | (43), (44), (48), (49), (76), (99) gives: % 73.94/10.49 | | | | | | | | (105) all_385_15 = all_383_5 % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | GROUND_INST: instantiating (7) with all_385_16, all_385_15, % 73.94/10.49 | | | | | | | | vtempty, all_332_2, all_332_1, simplifying with % 73.94/10.49 | | | | | | | | (11), (27), (48), (49), (99) gives: % 73.94/10.49 | | | | | | | | (106) ? [v0: any] : ? [v1: vRawTable] : ? [v2: vRawTable] % 73.94/10.49 | | | | | | | | : ? [v3: vRow] : (vRow(v3) & ((v3 = all_385_16 & % 73.94/10.49 | | | | | | | | all_385_15 = vtempty) | % 73.94/10.49 | | | | | | | | (vrawDifference(all_385_15, vtempty) = v1 & % 73.94/10.49 | | | | | | | | vrowIn(all_385_16, vtempty) = v0 & % 73.94/10.49 | | | | | | | | vtcons(all_385_16, v1) = v2 & vRawTable(v2) & % 73.94/10.49 | | | | | | | | vRawTable(v1) & (v2 = all_332_1 | v0 = 0)))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | GROUND_INST: instantiating (8) with all_385_16, all_385_15, % 73.94/10.49 | | | | | | | | vtempty, all_332_2, all_332_1, simplifying with % 73.94/10.49 | | | | | | | | (11), (27), (48), (49), (99) gives: % 73.94/10.49 | | | | | | | | (107) ? [v0: any] : ? [v1: vRawTable] : ? [v2: vRow] : % 73.94/10.49 | | | | | | | | (vRow(v2) & ((v2 = all_385_16 & all_385_15 = vtempty) | % 73.94/10.49 | | | | | | | | (vrawDifference(all_385_15, vtempty) = v1 & % 73.94/10.49 | | | | | | | | vrowIn(all_385_16, vtempty) = v0 & vRawTable(v1) % 73.94/10.49 | | | | | | | | & ( ~ (v0 = 0) | v1 = all_332_1)))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | GROUND_INST: instantiating (2) with all_391_3, all_391_2, % 73.94/10.49 | | | | | | | | all_385_16, all_385_14, all_332_1, simplifying with % 73.94/10.49 | | | | | | | | (48), (50), (57), (58), (59), (100) gives: % 73.94/10.49 | | | | | | | | (108) all_391_2 = all_385_14 % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | COMBINE_EQS: (104), (105) imply: % 73.94/10.49 | | | | | | | | (109) all_383_5 = vrt2 % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | SIMP: (109) implies: % 73.94/10.49 | | | | | | | | (110) all_383_5 = vrt2 % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | DELTA: instantiating (107) with fresh symbols all_925_0, % 73.94/10.49 | | | | | | | | all_925_1, all_925_2 gives: % 73.94/10.49 | | | | | | | | (111) vRow(all_925_0) & ((all_925_0 = all_385_16 & all_385_15 % 73.94/10.49 | | | | | | | | = vtempty) | (vrawDifference(all_385_15, vtempty) = % 73.94/10.49 | | | | | | | | all_925_1 & vrowIn(all_385_16, vtempty) = all_925_2 % 73.94/10.49 | | | | | | | | & vRawTable(all_925_1) & ( ~ (all_925_2 = 0) | % 73.94/10.49 | | | | | | | | all_925_1 = all_332_1))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | ALPHA: (111) implies: % 73.94/10.49 | | | | | | | | (112) (all_925_0 = all_385_16 & all_385_15 = vtempty) | % 73.94/10.49 | | | | | | | | (vrawDifference(all_385_15, vtempty) = all_925_1 & % 73.94/10.49 | | | | | | | | vrowIn(all_385_16, vtempty) = all_925_2 & % 73.94/10.49 | | | | | | | | vRawTable(all_925_1) & ( ~ (all_925_2 = 0) | % 73.94/10.49 | | | | | | | | all_925_1 = all_332_1)) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | DELTA: instantiating (103) with fresh symbols all_927_0, % 73.94/10.49 | | | | | | | | all_927_1, all_927_2 gives: % 73.94/10.49 | | | | | | | | (113) vRow(all_927_0) & ((all_927_0 = all_383_6 & all_383_5 = % 73.94/10.49 | | | | | | | | vtempty) | (vrawDifference(all_383_5, vtempty) = % 73.94/10.49 | | | | | | | | all_927_1 & vrowIn(all_383_6, vtempty) = all_927_2 % 73.94/10.49 | | | | | | | | & vRawTable(all_927_1) & ( ~ (all_927_2 = 0) | % 73.94/10.49 | | | | | | | | all_927_1 = all_332_1))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | ALPHA: (113) implies: % 73.94/10.49 | | | | | | | | (114) (all_927_0 = all_383_6 & all_383_5 = vtempty) | % 73.94/10.49 | | | | | | | | (vrawDifference(all_383_5, vtempty) = all_927_1 & % 73.94/10.49 | | | | | | | | vrowIn(all_383_6, vtempty) = all_927_2 & % 73.94/10.49 | | | | | | | | vRawTable(all_927_1) & ( ~ (all_927_2 = 0) | % 73.94/10.49 | | | | | | | | all_927_1 = all_332_1)) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | DELTA: instantiating (106) with fresh symbols all_933_0, % 73.94/10.49 | | | | | | | | all_933_1, all_933_2, all_933_3 gives: % 73.94/10.49 | | | | | | | | (115) vRow(all_933_0) & ((all_933_0 = all_385_16 & all_385_15 % 73.94/10.49 | | | | | | | | = vtempty) | (vrawDifference(all_385_15, vtempty) = % 73.94/10.49 | | | | | | | | all_933_2 & vrowIn(all_385_16, vtempty) = all_933_3 % 73.94/10.49 | | | | | | | | & vtcons(all_385_16, all_933_2) = all_933_1 & % 73.94/10.49 | | | | | | | | vRawTable(all_933_1) & vRawTable(all_933_2) & % 73.94/10.49 | | | | | | | | (all_933_1 = all_332_1 | all_933_3 = 0))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | ALPHA: (115) implies: % 73.94/10.49 | | | | | | | | (116) (all_933_0 = all_385_16 & all_385_15 = vtempty) | % 73.94/10.49 | | | | | | | | (vrawDifference(all_385_15, vtempty) = all_933_2 & % 73.94/10.49 | | | | | | | | vrowIn(all_385_16, vtempty) = all_933_3 & % 73.94/10.49 | | | | | | | | vtcons(all_385_16, all_933_2) = all_933_1 & % 73.94/10.49 | | | | | | | | vRawTable(all_933_1) & vRawTable(all_933_2) & % 73.94/10.49 | | | | | | | | (all_933_1 = all_332_1 | all_933_3 = 0)) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | DELTA: instantiating (102) with fresh symbols all_947_0, % 73.94/10.49 | | | | | | | | all_947_1, all_947_2, all_947_3 gives: % 73.94/10.49 | | | | | | | | (117) vRow(all_947_0) & ((all_947_0 = all_383_6 & all_383_5 = % 73.94/10.49 | | | | | | | | vtempty) | (vrawDifference(all_383_5, vtempty) = % 73.94/10.49 | | | | | | | | all_947_2 & vrowIn(all_383_6, vtempty) = all_947_3 % 73.94/10.49 | | | | | | | | & vtcons(all_383_6, all_947_2) = all_947_1 & % 73.94/10.49 | | | | | | | | vRawTable(all_947_1) & vRawTable(all_947_2) & % 73.94/10.49 | | | | | | | | (all_947_1 = all_332_1 | all_947_3 = 0))) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | ALPHA: (117) implies: % 73.94/10.49 | | | | | | | | (118) (all_947_0 = all_383_6 & all_383_5 = vtempty) | % 73.94/10.49 | | | | | | | | (vrawDifference(all_383_5, vtempty) = all_947_2 & % 73.94/10.49 | | | | | | | | vrowIn(all_383_6, vtempty) = all_947_3 & % 73.94/10.49 | | | | | | | | vtcons(all_383_6, all_947_2) = all_947_1 & % 73.94/10.49 | | | | | | | | vRawTable(all_947_1) & vRawTable(all_947_2) & % 73.94/10.49 | | | | | | | | (all_947_1 = all_332_1 | all_947_3 = 0)) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | REDUCE: (98), (104) imply: % 73.94/10.49 | | | | | | | | (119) ~ (vrt2 = vtempty) % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | REDUCE: (101), (104) imply: % 73.94/10.49 | | | | | | | | (120) vrawDifference(vrt2, vtempty) = all_385_14 % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | REDUCE: (61), (108) imply: % 73.94/10.49 | | | | | | | | (121) vwelltypedRawtable(all_332_3, all_385_14) = all_391_0 % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | BETA: splitting (116) gives: % 73.94/10.49 | | | | | | | | % 73.94/10.49 | | | | | | | | Case 1: % 73.94/10.49 | | | | | | | | | % 73.94/10.49 | | | | | | | | | (122) all_933_0 = all_385_16 & all_385_15 = vtempty % 73.94/10.49 | | | | | | | | | % 73.94/10.49 | | | | | | | | | ALPHA: (122) implies: % 73.94/10.49 | | | | | | | | | (123) all_385_15 = vtempty % 73.94/10.49 | | | | | | | | | % 73.94/10.49 | | | | | | | | | COMBINE_EQS: (104), (123) imply: % 73.94/10.49 | | | | | | | | | (124) vrt2 = vtempty % 73.94/10.49 | | | | | | | | | % 73.94/10.49 | | | | | | | | | REDUCE: (119), (124) imply: % 73.94/10.49 | | | | | | | | | (125) $false % 73.94/10.49 | | | | | | | | | % 73.94/10.49 | | | | | | | | | CLOSE: (125) is inconsistent. % 73.94/10.49 | | | | | | | | | % 73.94/10.49 | | | | | | | | Case 2: % 73.94/10.49 | | | | | | | | | % 73.94/10.49 | | | | | | | | | (126) vrawDifference(all_385_15, vtempty) = all_933_2 & % 73.94/10.49 | | | | | | | | | vrowIn(all_385_16, vtempty) = all_933_3 & % 73.94/10.49 | | | | | | | | | vtcons(all_385_16, all_933_2) = all_933_1 & % 73.94/10.49 | | | | | | | | | vRawTable(all_933_1) & vRawTable(all_933_2) & % 73.94/10.49 | | | | | | | | | (all_933_1 = all_332_1 | all_933_3 = 0) % 73.94/10.49 | | | | | | | | | % 73.94/10.50 | | | | | | | | | ALPHA: (126) implies: % 73.94/10.50 | | | | | | | | | (127) vrawDifference(all_385_15, vtempty) = all_933_2 % 73.94/10.50 | | | | | | | | | % 73.94/10.50 | | | | | | | | | REDUCE: (104), (127) imply: % 73.94/10.50 | | | | | | | | | (128) vrawDifference(vrt2, vtempty) = all_933_2 % 73.94/10.50 | | | | | | | | | % 73.94/10.50 | | | | | | | | | BETA: splitting (114) gives: % 73.94/10.50 | | | | | | | | | % 73.94/10.50 | | | | | | | | | Case 1: % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | (129) all_927_0 = all_383_6 & all_383_5 = vtempty % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | ALPHA: (129) implies: % 73.94/10.50 | | | | | | | | | | (130) all_383_5 = vtempty % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | COMBINE_EQS: (110), (130) imply: % 73.94/10.50 | | | | | | | | | | (131) vrt2 = vtempty % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | REDUCE: (119), (131) imply: % 73.94/10.50 | | | | | | | | | | (132) $false % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | CLOSE: (132) is inconsistent. % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | Case 2: % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | (133) vrawDifference(all_383_5, vtempty) = all_927_1 & % 73.94/10.50 | | | | | | | | | | vrowIn(all_383_6, vtempty) = all_927_2 & % 73.94/10.50 | | | | | | | | | | vRawTable(all_927_1) & ( ~ (all_927_2 = 0) | % 73.94/10.50 | | | | | | | | | | all_927_1 = all_332_1) % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | ALPHA: (133) implies: % 73.94/10.50 | | | | | | | | | | (134) vrawDifference(all_383_5, vtempty) = all_927_1 % 73.94/10.50 | | | | | | | | | | % 73.94/10.50 | | | | | | | | | | REDUCE: (110), (134) imply: % 74.43/10.50 | | | | | | | | | | (135) vrawDifference(vrt2, vtempty) = all_927_1 % 74.43/10.50 | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | BETA: splitting (112) gives: % 74.43/10.50 | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | Case 1: % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | (136) all_925_0 = all_385_16 & all_385_15 = vtempty % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | ALPHA: (136) implies: % 74.43/10.50 | | | | | | | | | | | (137) all_385_15 = vtempty % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | COMBINE_EQS: (104), (137) imply: % 74.43/10.50 | | | | | | | | | | | (138) vrt2 = vtempty % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | SIMP: (138) implies: % 74.43/10.50 | | | | | | | | | | | (139) vrt2 = vtempty % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | REDUCE: (119), (139) imply: % 74.43/10.50 | | | | | | | | | | | (140) $false % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | CLOSE: (140) is inconsistent. % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | Case 2: % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | (141) vrawDifference(all_385_15, vtempty) = all_925_1 & % 74.43/10.50 | | | | | | | | | | | vrowIn(all_385_16, vtempty) = all_925_2 & % 74.43/10.50 | | | | | | | | | | | vRawTable(all_925_1) & ( ~ (all_925_2 = 0) | % 74.43/10.50 | | | | | | | | | | | all_925_1 = all_332_1) % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | ALPHA: (141) implies: % 74.43/10.50 | | | | | | | | | | | (142) vrawDifference(all_385_15, vtempty) = all_925_1 % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | REDUCE: (104), (142) imply: % 74.43/10.50 | | | | | | | | | | | (143) vrawDifference(vrt2, vtempty) = all_925_1 % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | BETA: splitting (118) gives: % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | Case 1: % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | (144) all_947_0 = all_383_6 & all_383_5 = vtempty % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | ALPHA: (144) implies: % 74.43/10.50 | | | | | | | | | | | | (145) all_383_5 = vtempty % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | COMBINE_EQS: (110), (145) imply: % 74.43/10.50 | | | | | | | | | | | | (146) vrt2 = vtempty % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | REDUCE: (119), (146) imply: % 74.43/10.50 | | | | | | | | | | | | (147) $false % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | CLOSE: (147) is inconsistent. % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | Case 2: % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | (148) vrawDifference(all_383_5, vtempty) = all_947_2 & % 74.43/10.50 | | | | | | | | | | | | vrowIn(all_383_6, vtempty) = all_947_3 & % 74.43/10.50 | | | | | | | | | | | | vtcons(all_383_6, all_947_2) = all_947_1 & % 74.43/10.50 | | | | | | | | | | | | vRawTable(all_947_1) & vRawTable(all_947_2) & % 74.43/10.50 | | | | | | | | | | | | (all_947_1 = all_332_1 | all_947_3 = 0) % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | ALPHA: (148) implies: % 74.43/10.50 | | | | | | | | | | | | (149) vrawDifference(all_383_5, vtempty) = all_947_2 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | REDUCE: (110), (149) imply: % 74.43/10.50 | | | | | | | | | | | | (150) vrawDifference(vrt2, vtempty) = all_947_2 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_371_1, all_927_1, % 74.43/10.50 | | | | | | | | | | | | vtempty, vrt2, simplifying with (38), (135) gives: % 74.43/10.50 | | | | | | | | | | | | (151) all_927_1 = all_371_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_385_14, all_927_1, % 74.43/10.50 | | | | | | | | | | | | vtempty, vrt2, simplifying with (120), (135) % 74.43/10.50 | | | | | | | | | | | | gives: % 74.43/10.50 | | | | | | | | | | | | (152) all_927_1 = all_385_14 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_927_1, all_933_2, % 74.43/10.50 | | | | | | | | | | | | vtempty, vrt2, simplifying with (128), (135) % 74.43/10.50 | | | | | | | | | | | | gives: % 74.43/10.50 | | | | | | | | | | | | (153) all_933_2 = all_927_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_933_2, all_947_2, % 74.43/10.50 | | | | | | | | | | | | vtempty, vrt2, simplifying with (128), (150) % 74.43/10.50 | | | | | | | | | | | | gives: % 74.43/10.50 | | | | | | | | | | | | (154) all_947_2 = all_933_2 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_925_1, all_947_2, % 74.43/10.50 | | | | | | | | | | | | vtempty, vrt2, simplifying with (143), (150) % 74.43/10.50 | | | | | | | | | | | | gives: % 74.43/10.50 | | | | | | | | | | | | (155) all_947_2 = all_925_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | COMBINE_EQS: (154), (155) imply: % 74.43/10.50 | | | | | | | | | | | | (156) all_933_2 = all_925_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | SIMP: (156) implies: % 74.43/10.50 | | | | | | | | | | | | (157) all_933_2 = all_925_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | COMBINE_EQS: (153), (157) imply: % 74.43/10.50 | | | | | | | | | | | | (158) all_927_1 = all_925_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | SIMP: (158) implies: % 74.43/10.50 | | | | | | | | | | | | (159) all_927_1 = all_925_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | COMBINE_EQS: (152), (159) imply: % 74.43/10.50 | | | | | | | | | | | | (160) all_925_1 = all_385_14 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | COMBINE_EQS: (151), (159) imply: % 74.43/10.50 | | | | | | | | | | | | (161) all_925_1 = all_371_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | COMBINE_EQS: (160), (161) imply: % 74.43/10.50 | | | | | | | | | | | | (162) all_385_14 = all_371_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | SIMP: (162) implies: % 74.43/10.50 | | | | | | | | | | | | (163) all_385_14 = all_371_1 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | REDUCE: (121), (163) imply: % 74.43/10.50 | | | | | | | | | | | | (164) vwelltypedRawtable(all_332_3, all_371_1) = % 74.43/10.50 | | | | | | | | | | | | all_391_0 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | GROUND_INST: instantiating (15) with 0, all_391_0, all_371_1, % 74.43/10.50 | | | | | | | | | | | | all_332_3, simplifying with (70), (164) gives: % 74.43/10.50 | | | | | | | | | | | | (165) all_391_0 = 0 % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | REDUCE: (78), (165) imply: % 74.43/10.50 | | | | | | | | | | | | (166) $false % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | | CLOSE: (166) is inconsistent. % 74.43/10.50 | | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | | End of split % 74.43/10.50 | | | | | | | | | | | % 74.43/10.50 | | | | | | | | | | End of split % 74.43/10.50 | | | | | | | | | | % 74.43/10.50 | | | | | | | | | End of split % 74.43/10.50 | | | | | | | | | % 74.43/10.50 | | | | | | | | End of split % 74.43/10.50 | | | | | | | | % 74.43/10.50 | | | | | | | Case 2: % 74.43/10.50 | | | | | | | | % 74.43/10.50 | | | | | | | | (167) all_385_17 = all_332_2 & all_385_18 = 0 & all_385_19 = % 74.43/10.50 | | | | | | | | all_332_1 & all_385_20 = vtempty & all_385_21 = % 74.43/10.50 | | | | | | | | all_332_1 & ~ (all_385_22 = vtempty) & % 74.43/10.50 | | | | | | | | vrawDifference(all_385_22, vtempty) = all_332_1 & % 74.43/10.50 | | | | | | | | vrowIn(all_385_23, vtempty) = 0 & vtcons(all_385_23, % 74.43/10.50 | | | | | | | | all_385_22) = all_332_2 & vRawTable(all_332_1) % 74.43/10.50 | | | | | | | | % 74.43/10.50 | | | | | | | | ALPHA: (167) implies: % 74.43/10.50 | | | | | | | | (168) vrowIn(all_385_23, vtempty) = 0 % 74.43/10.50 | | | | | | | | % 74.43/10.50 | | | | | | | | GROUND_INST: instantiating (6) with all_385_23, simplifying with % 74.43/10.50 | | | | | | | | (47), (168) gives: % 74.43/10.50 | | | | | | | | (169) $false % 74.43/10.50 | | | | | | | | % 74.43/10.50 | | | | | | | | CLOSE: (169) is inconsistent. % 74.43/10.50 | | | | | | | | % 74.43/10.50 | | | | | | | End of split % 74.43/10.50 | | | | | | | % 74.43/10.50 | | | | | | End of split % 74.43/10.50 | | | | | | % 74.43/10.50 | | | | | End of split % 74.43/10.50 | | | | | % 74.43/10.50 | | | | Case 2: % 74.43/10.50 | | | | | % 74.43/10.50 | | | | | (170) ~ (all_391_1 = 0) % 74.43/10.50 | | | | | % 74.43/10.50 | | | | | BETA: splitting (52) gives: % 74.43/10.50 | | | | | % 74.43/10.50 | | | | | Case 1: % 74.43/10.50 | | | | | | % 74.43/10.50 | | | | | | (171) (all_385_0 = vtempty & all_332_1 = vtempty & all_332_2 = % 74.43/10.50 | | | | | | vtempty) | (all_385_1 = all_332_2 & all_385_3 = vtempty & % 74.43/10.50 | | | | | | all_332_1 = all_332_2 & ~ (all_385_2 = 0) & % 74.43/10.50 | | | | | | vrowIn(all_385_4, vtempty) = all_385_2 & % 74.43/10.50 | | | | | | vtcons(all_385_4, vtempty) = all_332_2) % 74.43/10.50 | | | | | | % 74.43/10.50 | | | | | | BETA: splitting (171) gives: % 74.43/10.50 | | | | | | % 74.43/10.50 | | | | | | Case 1: % 74.43/10.50 | | | | | | | % 74.43/10.50 | | | | | | | (172) all_385_0 = vtempty & all_332_1 = vtempty & all_332_2 = % 74.43/10.50 | | | | | | | vtempty % 74.43/10.50 | | | | | | | % 74.43/10.50 | | | | | | | ALPHA: (172) implies: % 74.43/10.50 | | | | | | | (173) all_332_2 = vtempty % 74.43/10.50 | | | | | | | (174) all_332_1 = vtempty % 74.43/10.50 | | | | | | | % 74.43/10.50 | | | | | | | REDUCE: (26), (174) imply: % 74.43/10.50 | | | | | | | (175) vwelltypedRawtable(all_332_3, vtempty) = all_332_0 % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | REF_CLOSE: (15), (18), (24), (175) are inconsistent by sub-proof % 74.43/10.51 | | | | | | | #1. % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | Case 2: % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | (176) all_385_1 = all_332_2 & all_385_3 = vtempty & all_332_1 = % 74.43/10.51 | | | | | | | all_332_2 & ~ (all_385_2 = 0) & vrowIn(all_385_4, % 74.43/10.51 | | | | | | | vtempty) = all_385_2 & vtcons(all_385_4, vtempty) = % 74.43/10.51 | | | | | | | all_332_2 % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | ALPHA: (176) implies: % 74.43/10.51 | | | | | | | (177) all_332_1 = all_332_2 % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | REDUCE: (26), (177) imply: % 74.43/10.51 | | | | | | | (178) vwelltypedRawtable(all_332_3, all_332_2) = all_332_0 % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | GROUND_INST: instantiating (15) with 0, all_332_0, all_332_2, % 74.43/10.51 | | | | | | | all_332_3, simplifying with (25), (178) gives: % 74.43/10.51 | | | | | | | (179) all_332_0 = 0 % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | REDUCE: (18), (179) imply: % 74.43/10.51 | | | | | | | (180) $false % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | CLOSE: (180) is inconsistent. % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | End of split % 74.43/10.51 | | | | | | % 74.43/10.51 | | | | | Case 2: % 74.43/10.51 | | | | | | % 74.43/10.51 | | | | | | (181) (all_385_5 = all_332_2 & all_385_6 = 0 & all_385_7 = % 74.43/10.51 | | | | | | vtempty & all_332_1 = vtempty & vrowIn(all_385_8, % 74.43/10.51 | | | | | | vtempty) = 0 & vtcons(all_385_8, vtempty) = all_332_2) % 74.43/10.51 | | | | | | | (all_385_9 = all_332_1 & all_385_10 = all_332_2 & % 74.43/10.51 | | | | | | all_385_12 = all_385_14 & all_385_13 = vtempty & ~ % 74.43/10.51 | | | | | | (all_385_11 = 0) & ~ (all_385_15 = vtempty) & % 74.43/10.51 | | | | | | vrawDifference(all_385_15, vtempty) = all_385_14 & % 74.43/10.51 | | | | | | vrowIn(all_385_16, vtempty) = all_385_11 & % 74.43/10.51 | | | | | | vtcons(all_385_16, all_385_14) = all_332_1 & % 74.43/10.51 | | | | | | vtcons(all_385_16, all_385_15) = all_332_2 & % 74.43/10.51 | | | | | | vRawTable(all_332_1)) | (all_385_17 = all_332_2 & % 74.43/10.51 | | | | | | all_385_18 = 0 & all_385_19 = all_332_1 & all_385_20 = % 74.43/10.51 | | | | | | vtempty & all_385_21 = all_332_1 & ~ (all_385_22 = % 74.43/10.51 | | | | | | vtempty) & vrawDifference(all_385_22, vtempty) = % 74.43/10.51 | | | | | | all_332_1 & vrowIn(all_385_23, vtempty) = 0 & % 74.43/10.51 | | | | | | vtcons(all_385_23, all_385_22) = all_332_2 & % 74.43/10.51 | | | | | | vRawTable(all_332_1)) % 74.43/10.51 | | | | | | % 74.43/10.51 | | | | | | BETA: splitting (181) gives: % 74.43/10.51 | | | | | | % 74.43/10.51 | | | | | | Case 1: % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | (182) all_385_5 = all_332_2 & all_385_6 = 0 & all_385_7 = % 74.43/10.51 | | | | | | | vtempty & all_332_1 = vtempty & vrowIn(all_385_8, % 74.43/10.51 | | | | | | | vtempty) = 0 & vtcons(all_385_8, vtempty) = all_332_2 % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | ALPHA: (182) implies: % 74.43/10.51 | | | | | | | (183) all_332_1 = vtempty % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | REDUCE: (26), (183) imply: % 74.43/10.51 | | | | | | | (184) vwelltypedRawtable(all_332_3, vtempty) = all_332_0 % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | REF_CLOSE: (15), (18), (24), (184) are inconsistent by sub-proof % 74.43/10.51 | | | | | | | #1. % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | Case 2: % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | (185) (all_385_9 = all_332_1 & all_385_10 = all_332_2 & % 74.43/10.51 | | | | | | | all_385_12 = all_385_14 & all_385_13 = vtempty & ~ % 74.43/10.51 | | | | | | | (all_385_11 = 0) & ~ (all_385_15 = vtempty) & % 74.43/10.51 | | | | | | | vrawDifference(all_385_15, vtempty) = all_385_14 & % 74.43/10.51 | | | | | | | vrowIn(all_385_16, vtempty) = all_385_11 & % 74.43/10.51 | | | | | | | vtcons(all_385_16, all_385_14) = all_332_1 & % 74.43/10.51 | | | | | | | vtcons(all_385_16, all_385_15) = all_332_2 & % 74.43/10.51 | | | | | | | vRawTable(all_332_1)) | (all_385_17 = all_332_2 & % 74.43/10.51 | | | | | | | all_385_18 = 0 & all_385_19 = all_332_1 & all_385_20 = % 74.43/10.51 | | | | | | | vtempty & all_385_21 = all_332_1 & ~ (all_385_22 = % 74.43/10.51 | | | | | | | vtempty) & vrawDifference(all_385_22, vtempty) = % 74.43/10.51 | | | | | | | all_332_1 & vrowIn(all_385_23, vtempty) = 0 & % 74.43/10.51 | | | | | | | vtcons(all_385_23, all_385_22) = all_332_2 & % 74.43/10.51 | | | | | | | vRawTable(all_332_1)) % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | BETA: splitting (185) gives: % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | | Case 1: % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | (186) all_385_9 = all_332_1 & all_385_10 = all_332_2 & % 74.43/10.51 | | | | | | | | all_385_12 = all_385_14 & all_385_13 = vtempty & ~ % 74.43/10.51 | | | | | | | | (all_385_11 = 0) & ~ (all_385_15 = vtempty) & % 74.43/10.51 | | | | | | | | vrawDifference(all_385_15, vtempty) = all_385_14 & % 74.43/10.51 | | | | | | | | vrowIn(all_385_16, vtempty) = all_385_11 & % 74.43/10.51 | | | | | | | | vtcons(all_385_16, all_385_14) = all_332_1 & % 74.43/10.51 | | | | | | | | vtcons(all_385_16, all_385_15) = all_332_2 & % 74.43/10.51 | | | | | | | | vRawTable(all_332_1) % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | ALPHA: (186) implies: % 74.43/10.51 | | | | | | | | (187) vtcons(all_385_16, all_385_15) = all_332_2 % 74.43/10.51 | | | | | | | | (188) vtcons(all_385_16, all_385_14) = all_332_1 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | GROUND_INST: instantiating (1) with all_332_4, vrt2, all_385_16, % 74.43/10.51 | | | | | | | | all_385_15, all_332_2, simplifying with (12), (19), % 74.43/10.51 | | | | | | | | (23), (48), (49), (187) gives: % 74.43/10.51 | | | | | | | | (189) all_385_16 = all_332_4 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | GROUND_INST: instantiating (1) with all_383_6, all_383_5, % 74.43/10.51 | | | | | | | | all_385_16, all_385_15, all_332_2, simplifying with % 74.43/10.51 | | | | | | | | (43), (44), (48), (49), (76), (187) gives: % 74.43/10.51 | | | | | | | | (190) all_385_16 = all_383_6 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | GROUND_INST: instantiating (1) with all_391_3, all_391_2, % 74.43/10.51 | | | | | | | | all_385_16, all_385_14, all_332_1, simplifying with % 74.43/10.51 | | | | | | | | (48), (50), (57), (58), (59), (188) gives: % 74.43/10.51 | | | | | | | | (191) all_391_3 = all_385_16 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | COMBINE_EQS: (189), (190) imply: % 74.43/10.51 | | | | | | | | (192) all_383_6 = all_332_4 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | SIMP: (192) implies: % 74.43/10.51 | | | | | | | | (193) all_383_6 = all_332_4 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | COMBINE_EQS: (189), (191) imply: % 74.43/10.51 | | | | | | | | (194) all_391_3 = all_332_4 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | REDUCE: (60), (194) imply: % 74.43/10.51 | | | | | | | | (195) vwelltypedRow(all_332_3, all_332_4) = all_391_1 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | REDUCE: (77), (193) imply: % 74.43/10.51 | | | | | | | | (196) vwelltypedRow(all_332_3, all_332_4) = 0 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | GROUND_INST: instantiating (14) with 0, all_391_1, all_332_4, % 74.43/10.51 | | | | | | | | all_332_3, simplifying with (195), (196) gives: % 74.43/10.51 | | | | | | | | (197) all_391_1 = 0 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | REDUCE: (170), (197) imply: % 74.43/10.51 | | | | | | | | (198) $false % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | CLOSE: (198) is inconsistent. % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | Case 2: % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | (199) all_385_17 = all_332_2 & all_385_18 = 0 & all_385_19 = % 74.43/10.51 | | | | | | | | all_332_1 & all_385_20 = vtempty & all_385_21 = % 74.43/10.51 | | | | | | | | all_332_1 & ~ (all_385_22 = vtempty) & % 74.43/10.51 | | | | | | | | vrawDifference(all_385_22, vtempty) = all_332_1 & % 74.43/10.51 | | | | | | | | vrowIn(all_385_23, vtempty) = 0 & vtcons(all_385_23, % 74.43/10.51 | | | | | | | | all_385_22) = all_332_2 & vRawTable(all_332_1) % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | ALPHA: (199) implies: % 74.43/10.51 | | | | | | | | (200) vrowIn(all_385_23, vtempty) = 0 % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | GROUND_INST: instantiating (6) with all_385_23, simplifying with % 74.43/10.51 | | | | | | | | (47), (200) gives: % 74.43/10.51 | | | | | | | | (201) $false % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | | CLOSE: (201) is inconsistent. % 74.43/10.51 | | | | | | | | % 74.43/10.51 | | | | | | | End of split % 74.43/10.51 | | | | | | | % 74.43/10.51 | | | | | | End of split % 74.43/10.51 | | | | | | % 74.43/10.51 | | | | | End of split % 74.43/10.51 | | | | | % 74.43/10.51 | | | | End of split % 74.43/10.51 | | | | % 74.43/10.51 | | | End of split % 74.43/10.51 | | | % 74.43/10.51 | | End of split % 74.43/10.51 | | % 74.43/10.51 | End of split % 74.43/10.51 | % 74.43/10.51 End of proof % 74.43/10.51 % 74.43/10.51 Sub-proof #1 shows that the following formulas are inconsistent: % 74.43/10.51 ---------------------------------------------------------------- % 74.43/10.51 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 74.43/10.51 vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ (vwelltypedRawtable(v3, % 74.43/10.51 v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) % 74.43/10.51 (2) vwelltypedRawtable(all_332_3, vtempty) = all_332_0 % 74.43/10.51 (3) vwelltypedRawtable(all_332_3, vtempty) = 0 % 74.43/10.51 (4) ~ (all_332_0 = 0) % 74.43/10.51 % 74.43/10.51 Begin of proof % 74.43/10.51 | % 74.43/10.51 | GROUND_INST: instantiating (1) with 0, all_332_0, vtempty, all_332_3, % 74.43/10.51 | simplifying with (2), (3) gives: % 74.43/10.51 | (5) all_332_0 = 0 % 74.43/10.51 | % 74.43/10.51 | REDUCE: (4), (5) imply: % 74.43/10.51 | (6) $false % 74.43/10.51 | % 74.43/10.51 | CLOSE: (6) is inconsistent. % 74.43/10.51 | % 74.43/10.51 End of proof % 74.43/10.51 % SZS output end Proof for theBenchmark % 74.43/10.51 % 74.43/10.51 9920ms %------------------------------------------------------------------------------