%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM306_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 : n013.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:43 PM UTC 2026 % Result : Theorem 28.62s 4.58s % Output : Proof 38.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM306_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.33 % Computer : n013.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:40:40 EDT 2026 % 0.16/0.34 % CPUTime : % 0.51/0.60 ________ _____ % 0.51/0.60 ___ __ \_________(_)________________________________ % 0.51/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.51/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.51/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.51/0.60 % 0.51/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.51/0.60 (2023-06-19) % 0.51/0.60 % 0.51/0.60 (c) Philipp Rümmer, 2009-2023 % 0.51/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.51/0.60 Amanda Stjerna. % 0.51/0.60 Free software under BSD-3-Clause. % 0.51/0.60 % 0.51/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.51/0.60 % 0.51/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.51/0.62 Running up to 7 provers in parallel. % 0.72/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.72/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.72/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.72/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.72/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.72/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.72/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.62/2.04 Prover 5: Preprocessing ... % 10.40/2.13 Prover 2: Preprocessing ... % 11.02/2.22 Prover 1: Preprocessing ... % 11.02/2.23 Prover 3: Preprocessing ... % 11.02/2.24 Prover 6: Preprocessing ... % 11.02/2.26 Prover 0: Preprocessing ... % 11.76/2.30 Prover 4: Preprocessing ... % 23.99/3.93 Prover 1: Warning: ignoring some quantifiers % 24.85/4.02 Prover 3: Warning: ignoring some quantifiers % 24.85/4.04 Prover 1: Constructing countermodel ... % 24.85/4.10 Prover 6: Proving ... % 24.85/4.11 Prover 3: Constructing countermodel ... % 26.28/4.21 Prover 4: Warning: ignoring some quantifiers % 26.28/4.28 Prover 0: Proving ... % 27.07/4.34 Prover 4: Constructing countermodel ... % 28.62/4.50 Prover 5: Proving ... % 28.62/4.57 Prover 3: proved (3946ms) % 28.62/4.58 % 28.62/4.58 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 28.62/4.58 % 28.62/4.59 Prover 6: stopped % 28.62/4.60 Prover 5: stopped % 29.38/4.63 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.38/4.63 Prover 0: stopped % 29.38/4.63 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.38/4.63 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 29.38/4.63 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 31.00/4.83 Prover 2: Proving ... % 31.00/4.83 Prover 2: stopped % 31.00/4.84 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 32.56/5.10 Prover 1: Found proof (size 40) % 32.56/5.10 Prover 1: proved (4474ms) % 32.56/5.10 Prover 4: stopped % 33.95/5.27 Prover 11: Preprocessing ... % 33.95/5.28 Prover 7: Preprocessing ... % 34.71/5.31 Prover 10: Preprocessing ... % 34.71/5.33 Prover 8: Preprocessing ... % 34.71/5.36 Prover 13: Preprocessing ... % 36.24/5.55 Prover 10: stopped % 36.24/5.55 Prover 7: stopped % 36.96/5.60 Prover 11: stopped % 36.96/5.66 Prover 13: stopped % 37.83/5.84 Prover 8: Warning: ignoring some quantifiers % 37.83/5.87 Prover 8: Constructing countermodel ... % 37.83/5.89 Prover 8: stopped % 37.83/5.89 % 37.83/5.89 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 37.83/5.89 % 38.28/5.90 % SZS output start Proof for theBenchmark % 38.28/5.92 Assumptions after simplification: % 38.28/5.92 --------------------------------- % 38.28/5.92 % 38.28/5.92 (DIFF-noRawTable-someRawTable) % 38.28/5.95 vOptRawTable(vnoRawTable) & ! [v0: vRawTable] : ( ~ (vsomeRawTable(v0) = % 38.28/5.95 vnoRawTable) | ~ vRawTable(v0)) % 38.28/5.95 % 38.28/5.95 (EQ-table) % 38.28/5.95 ! [v0: vAttrL] : ! [v1: vRawTable] : ! [v2: vAttrL] : ! [v3: vRawTable] : % 38.28/5.95 ! [v4: vTable] : ( ~ (vtable(v2, v3) = v4) | ~ (vtable(v0, v1) = v4) | ~ % 38.28/5.95 vRawTable(v3) | ~ vRawTable(v1) | ~ vAttrL(v2) | ~ vAttrL(v0) | (v3 = v1 % 38.28/5.96 & v2 = v0)) % 38.28/5.96 % 38.28/5.96 (getAttrL-INV) % 38.28/5.96 ! [v0: vTable] : ! [v1: vAttrL] : ( ~ (vgetAttrL(v0) = v1) | ~ vTable(v0) | % 38.28/5.96 ? [v2: vRawTable] : (vtable(v1, v2) = v0 & vRawTable(v2) & vAttrL(v1))) % 38.28/5.96 % 38.28/5.96 (getRaw-INV) % 38.28/5.96 ! [v0: vTable] : ! [v1: vRawTable] : ( ~ (vgetRaw(v0) = v1) | ~ vTable(v0) % 38.28/5.96 | ? [v2: vAttrL] : (vtable(v2, v1) = v0 & vRawTable(v1) & vAttrL(v2))) % 38.28/5.96 % 38.28/5.96 (isSomeRawTable-false-INV) % 38.28/5.96 vOptRawTable(vnoRawTable) & ! [v0: vOptRawTable] : ! [v1: int] : (v1 = 0 | % 38.28/5.96 v0 = vnoRawTable | ~ (visSomeRawTable(v0) = v1) | ~ vOptRawTable(v0)) % 38.28/5.96 % 38.28/5.96 (projectColsProgress) % 38.28/5.96 ! [v0: vAttrL] : ! [v1: vRawTable] : ! [v2: vTType] : ! [v3: vAttrL] : ! % 38.28/5.96 [v4: vTType] : ! [v5: vOptTType] : ( ~ (vprojectTypeAttrL(v3, v4) = v5) | ~ % 38.28/5.96 (vwelltypedRawtable(v4, v1) = 0) | ~ (vmatchingAttrL(v4, v0) = 0) | ~ % 38.28/5.96 (vsomeTType(v2) = v5) | ~ vTType(v4) | ~ vTType(v2) | ~ vRawTable(v1) | % 38.28/5.96 ~ vAttrL(v3) | ~ vAttrL(v0) | ? [v6: vOptRawTable] : (vprojectCols(v3, v0, % 38.28/5.96 v1) = v6 & vOptRawTable(v6) & ? [v7: vRawTable] : (vsomeRawTable(v7) = % 38.28/5.96 v6 & vRawTable(v7)))) % 38.28/5.96 % 38.28/5.96 (projectTableProgress-list-isSomeRawTable-False) % 38.28/5.96 ? [v0: vAttrL] : ? [v1: vTable] : ? [v2: vTType] : ? [v3: vTType] : ? % 38.28/5.96 [v4: vAttrL] : ? [v5: vRawTable] : ? [v6: vOptRawTable] : ? [v7: int] : ? % 38.28/5.96 [v8: vSelect] : ? [v9: vOptTType] : ? [v10: vOptTable] : ( ~ (v7 = 0) & % 38.28/5.96 vprojectType(v8, v2) = v9 & vprojectTable(v8, v1) = v10 & vprojectCols(v0, % 38.28/5.96 v4, v5) = v6 & visSomeRawTable(v6) = v7 & vwelltypedtable(v2, v1) = 0 & % 38.28/5.96 vgetAttrL(v1) = v4 & vgetRaw(v1) = v5 & vsomeTType(v3) = v9 & vlist(v0) = v8 % 38.28/5.96 & vSelect(v8) & vTType(v3) & vTType(v2) & vTable(v1) & vOptTable(v10) & % 38.28/5.96 vOptTType(v9) & vOptRawTable(v6) & vRawTable(v5) & vAttrL(v4) & vAttrL(v0) & % 38.28/5.96 ! [v11: vTable] : ( ~ (vsomeTable(v11) = v10) | ~ vTable(v11))) % 38.28/5.96 % 38.28/5.96 (projectType-1) % 38.28/5.96 ! [v0: vAttrL] : ! [v1: vTType] : ! [v2: vSelect] : ! [v3: vOptTType] : ( % 38.28/5.96 ~ (vprojectType(v2, v1) = v3) | ~ (vlist(v0) = v2) | ~ vTType(v1) | ~ % 38.28/5.96 vAttrL(v0) | (vprojectTypeAttrL(v0, v1) = v3 & vOptTType(v3))) % 38.28/5.96 % 38.28/5.96 (welltypedtable-true-INV) % 38.28/5.97 ! [v0: vTType] : ! [v1: vTable] : ( ~ (vwelltypedtable(v0, v1) = 0) | ~ % 38.28/5.97 vTType(v0) | ~ vTable(v1) | ? [v2: vAttrL] : ? [v3: vRawTable] : % 38.28/5.97 (vwelltypedRawtable(v0, v3) = 0 & vmatchingAttrL(v0, v2) = 0 & vtable(v2, % 38.28/5.97 v3) = v1 & vRawTable(v3) & vAttrL(v2))) % 38.28/5.97 % 38.28/5.97 (function-axioms) % 38.28/5.99 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTType] : ! % 38.28/5.99 [v3: vQuery] : ! [v4: vTTContext] : (v1 = v0 | ~ (vptcheck(v4, v3, v2) = v1) % 38.28/5.99 | ~ (vptcheck(v4, v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] % 38.28/5.99 : ! [v2: vPred] : ! [v3: vAttrL] : ! [v4: vRawTable] : (v1 = v0 | ~ % 38.28/5.99 (vfilterRows(v4, v3, v2) = v1) | ~ (vfilterRows(v4, v3, v2) = v0)) & ! % 38.28/5.99 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! [v3: % 38.28/5.99 vAttrL] : ! [v4: vPred] : (v1 = v0 | ~ (vfilterSingleRow(v4, v3, v2) = v1) % 38.28/5.99 | ~ (vfilterSingleRow(v4, v3, v2) = v0)) & ! [v0: vOptVal] : ! [v1: % 38.28/5.99 vOptVal] : ! [v2: vRow] : ! [v3: vAttrL] : ! [v4: vExp] : (v1 = v0 | ~ % 38.28/5.99 (vevalExpRow(v4, v3, v2) = v1) | ~ (vevalExpRow(v4, v3, v2) = v0)) & ! % 38.28/5.99 [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! [v2: vRawTable] : ! [v3: % 38.28/5.99 vAttrL] : ! [v4: vAttrL] : (v1 = v0 | ~ (vprojectCols(v4, v3, v2) = v1) | % 38.28/5.99 ~ (vprojectCols(v4, v3, v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: % 38.28/5.99 vOptRawTable] : ! [v2: vRawTable] : ! [v3: vAttrL] : ! [v4: vName] : (v1 % 38.28/5.99 = v0 | ~ (vfindCol(v4, v3, v2) = v1) | ~ (vfindCol(v4, v3, v2) = v0)) & ! % 38.28/5.99 [v0: vTStore] : ! [v1: vTStore] : ! [v2: vTStore] : ! [v3: vTable] : ! % 38.28/5.99 [v4: vName] : (v1 = v0 | ~ (vbindStore(v4, v3, v2) = v1) | ~ (vbindStore(v4, % 38.28/5.99 v3, v2) = v0)) & ! [v0: vTTContext] : ! [v1: vTTContext] : ! [v2: % 38.28/5.99 vTTContext] : ! [v3: vTType] : ! [v4: vName] : (v1 = v0 | ~ % 38.28/5.99 (vbindContext(v4, v3, v2) = v1) | ~ (vbindContext(v4, v3, v2) = v0)) & ! % 38.28/5.99 [v0: vTType] : ! [v1: vTType] : ! [v2: vTType] : ! [v3: vFType] : ! [v4: % 38.28/5.99 vName] : (v1 = v0 | ~ (vttcons(v4, v3, v2) = v1) | ~ (vttcons(v4, v3, v2) % 38.28/5.99 = v0)) & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vPred] : ! [v3: % 38.28/5.99 vName] : ! [v4: vSelect] : (v1 = v0 | ~ (vselectFromWhere(v4, v3, v2) = % 38.28/5.99 v1) | ~ (vselectFromWhere(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 38.28/5.99 : ! [v1: MultipleValueBool] : ! [v2: vTTContext] : ! [v3: vTStore] : (v1 = % 38.28/5.99 v0 | ~ (vstoreContextConsistent(v3, v2) = v1) | ~ % 38.28/5.99 (vstoreContextConsistent(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 38.28/5.99 [v1: MultipleValueBool] : ! [v2: vTType] : ! [v3: vPred] : (v1 = v0 | ~ % 38.28/5.99 (vtcheckPred(v3, v2) = v1) | ~ (vtcheckPred(v3, v2) = v0)) & ! [v0: % 38.28/5.99 vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: vExp] : (v1 = v0 % 38.28/5.99 | ~ (vtypeOfExp(v3, v2) = v1) | ~ (vtypeOfExp(v3, v2) = v0)) & ! [v0: % 38.28/5.99 vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vSelect] : (v1 = % 38.28/5.99 v0 | ~ (vprojectType(v3, v2) = v1) | ~ (vprojectType(v3, v2) = v0)) & ! % 38.28/5.99 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vAttrL] : (v1 % 38.28/5.99 = v0 | ~ (vprojectTypeAttrL(v3, v2) = v1) | ~ (vprojectTypeAttrL(v3, v2) = % 38.28/5.99 v0)) & ! [v0: vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: % 38.28/5.99 vName] : (v1 = v0 | ~ (vfindColType(v3, v2) = v1) | ~ (vfindColType(v3, % 38.28/5.99 v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: vTStore] % 38.28/5.99 : ! [v3: vQuery] : (v1 = v0 | ~ (vreduce(v3, v2) = v1) | ~ (vreduce(v3, v2) % 38.28/5.99 = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: vPred] : ! [v3: % 38.28/5.99 vTable] : (v1 = v0 | ~ (vfilterTable(v3, v2) = v1) | ~ (vfilterTable(v3, % 38.28/5.99 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 38.28/5.99 ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ (vlessThan(v3, v2) = v1) | ~ % 38.28/5.99 (vlessThan(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 38.28/5.99 MultipleValueBool] : ! [v2: vVal] : ! [v3: vVal] : (v1 = v0 | ~ % 38.28/5.99 (vgreaterThan(v3, v2) = v1) | ~ (vgreaterThan(v3, v2) = v0)) & ! [v0: % 38.28/5.99 vOptTable] : ! [v1: vOptTable] : ! [v2: vTable] : ! [v3: vSelect] : (v1 = % 38.28/5.99 v0 | ~ (vprojectTable(v3, v2) = v1) | ~ (vprojectTable(v3, v2) = v0)) & ! % 38.28/5.99 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTTContext] : ! [v3: vName] : % 38.28/5.99 (v1 = v0 | ~ (vlookupContext(v3, v2) = v1) | ~ (vlookupContext(v3, v2) = % 38.28/5.99 v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! [v2: vTStore] : ! % 38.28/5.99 [v3: vName] : (v1 = v0 | ~ (vlookupStore(v3, v2) = v1) | ~ (vlookupStore(v3, % 38.28/5.99 v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 38.28/5.99 vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ (vrawDifference(v3, v2) = % 38.28/5.99 v1) | ~ (vrawDifference(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: % 38.28/5.99 vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 38.28/5.99 (vrawIntersection(v3, v2) = v1) | ~ (vrawIntersection(v3, v2) = v0)) & ! % 38.28/5.99 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 38.28/5.99 : (v1 = v0 | ~ (vrawUnion(v3, v2) = v1) | ~ (vrawUnion(v3, v2) = v0)) & ! % 38.28/5.99 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] % 38.28/5.99 : (v1 = v0 | ~ (vattachColToFrontRaw(v3, v2) = v1) | ~ % 38.28/5.99 (vattachColToFrontRaw(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 38.28/5.99 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 38.28/5.99 (vsameLength(v3, v2) = v1) | ~ (vsameLength(v3, v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRawTable] : ! % 38.28/5.99 [v3: vRow] : (v1 = v0 | ~ (vrowIn(v3, v2) = v1) | ~ (vrowIn(v3, v2) = v0)) & % 38.28/5.99 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vTable] : ! % 38.28/5.99 [v3: vTType] : (v1 = v0 | ~ (vwelltypedtable(v3, v2) = v1) | ~ % 38.28/5.99 (vwelltypedtable(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 38.28/5.99 MultipleValueBool] : ! [v2: vRawTable] : ! [v3: vTType] : (v1 = v0 | ~ % 38.28/5.99 (vwelltypedRawtable(v3, v2) = v1) | ~ (vwelltypedRawtable(v3, v2) = v0)) & % 38.28/5.99 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vRow] : ! % 38.28/5.99 [v3: vTType] : (v1 = v0 | ~ (vwelltypedRow(v3, v2) = v1) | ~ % 38.28/5.99 (vwelltypedRow(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 38.28/5.99 MultipleValueBool] : ! [v2: vAttrL] : ! [v3: vTType] : (v1 = v0 | ~ % 38.28/5.99 (vmatchingAttrL(v3, v2) = v1) | ~ (vmatchingAttrL(v3, v2) = v0)) & ! [v0: % 38.28/5.99 vAttrL] : ! [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vAttrL] : (v1 = v0 | % 38.28/5.99 ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) & ! [v0: vAttrL] : ! % 38.28/5.99 [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vName] : (v1 = v0 | ~ (vacons(v3, % 38.28/5.99 v2) = v1) | ~ (vacons(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] % 38.28/5.99 : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ (vlt(v3, v2) = v1) | ~ % 38.28/5.99 (vlt(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! % 38.28/5.99 [v3: vExp] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = v0)) & ! % 38.28/5.99 [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ % 38.28/5.99 (veq(v3, v2) = v1) | ~ (veq(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: % 38.28/5.99 vPred] : ! [v2: vPred] : ! [v3: vPred] : (v1 = v0 | ~ (vand(v3, v2) = v1) % 38.28/5.99 | ~ (vand(v3, v2) = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: % 38.28/5.99 vRawTable] : ! [v3: vAttrL] : (v1 = v0 | ~ (vtable(v3, v2) = v1) | ~ % 38.28/5.99 (vtable(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 38.28/5.99 vRawTable] : ! [v3: vRow] : (v1 = v0 | ~ (vtcons(v3, v2) = v1) | ~ % 38.28/5.99 (vtcons(v3, v2) = v0)) & ! [v0: vRow] : ! [v1: vRow] : ! [v2: vRow] : ! % 38.28/5.99 [v3: vVal] : (v1 = v0 | ~ (vrcons(v3, v2) = v1) | ~ (vrcons(v3, v2) = v0)) & % 38.28/5.99 ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = % 38.28/5.99 v0 | ~ (vDifference(v3, v2) = v1) | ~ (vDifference(v3, v2) = v0)) & ! % 38.28/5.99 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 38.28/5.99 | ~ (vIntersection(v3, v2) = v1) | ~ (vIntersection(v3, v2) = v0)) & ! % 38.28/5.99 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 38.28/5.99 | ~ (vUnion(v3, v2) = v1) | ~ (vUnion(v3, v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptFType] : (v1 = % 38.28/5.99 v0 | ~ (visSomeFType(v2) = v1) | ~ (visSomeFType(v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptVal] : (v1 = % 38.28/5.99 v0 | ~ (visSomeVal(v2) = v1) | ~ (visSomeVal(v2) = v0)) & ! [v0: % 38.28/5.99 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 38.28/5.99 (vprojectEmptyCol(v2) = v1) | ~ (vprojectEmptyCol(v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptQuery] : (v1 = % 38.28/5.99 v0 | ~ (visSomeQuery(v2) = v1) | ~ (visSomeQuery(v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vQuery] : (v1 = v0 % 38.28/5.99 | ~ (visValue(v2) = v1) | ~ (visValue(v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTType] : (v1 = % 38.28/5.99 v0 | ~ (visSomeTType(v2) = v1) | ~ (visSomeTType(v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptTable] : (v1 = % 38.28/5.99 v0 | ~ (visSomeTable(v2) = v1) | ~ (visSomeTable(v2) = v0)) & ! [v0: % 38.28/5.99 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: vOptRawTable] : % 38.28/5.99 (v1 = v0 | ~ (visSomeRawTable(v2) = v1) | ~ (visSomeRawTable(v2) = v0)) & ! % 38.28/5.99 [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 38.28/5.99 (vdropFirstColRaw(v2) = v1) | ~ (vdropFirstColRaw(v2) = v0)) & ! [v0: % 38.28/5.99 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 38.28/5.99 (vprojectFirstRaw(v2) = v1) | ~ (vprojectFirstRaw(v2) = v0)) & ! [v0: % 38.28/5.99 vFType] : ! [v1: vFType] : ! [v2: vVal] : (v1 = v0 | ~ (vfieldType(v2) = % 38.28/5.99 v1) | ~ (vfieldType(v2) = v0)) & ! [v0: vAttrL] : ! [v1: vAttrL] : ! % 38.28/5.99 [v2: vTable] : (v1 = v0 | ~ (vgetAttrL(v2) = v1) | ~ (vgetAttrL(v2) = v0)) & % 38.28/5.99 ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vTable] : (v1 = v0 | ~ % 38.28/5.99 (vgetRaw(v2) = v1) | ~ (vgetRaw(v2) = v0)) & ! [v0: vFType] : ! [v1: % 38.28/5.99 vFType] : ! [v2: vOptFType] : (v1 = v0 | ~ (vgetFType(v2) = v1) | ~ % 38.28/5.99 (vgetFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vOptVal] : % 38.28/5.99 (v1 = v0 | ~ (vgetVal(v2) = v1) | ~ (vgetVal(v2) = v0)) & ! [v0: vQuery] : % 38.28/5.99 ! [v1: vQuery] : ! [v2: vOptQuery] : (v1 = v0 | ~ (vgetQuery(v2) = v1) | ~ % 38.28/5.99 (vgetQuery(v2) = v0)) & ! [v0: vTType] : ! [v1: vTType] : ! [v2: % 38.28/5.99 vOptTType] : (v1 = v0 | ~ (vgetTType(v2) = v1) | ~ (vgetTType(v2) = v0)) & % 38.28/5.99 ! [v0: vTable] : ! [v1: vTable] : ! [v2: vOptTable] : (v1 = v0 | ~ % 38.28/5.99 (vgetTable(v2) = v1) | ~ (vgetTable(v2) = v0)) & ! [v0: vRawTable] : ! % 38.28/5.99 [v1: vRawTable] : ! [v2: vOptRawTable] : (v1 = v0 | ~ (vgetRawTable(v2) = % 38.28/5.99 v1) | ~ (vgetRawTable(v2) = v0)) & ! [v0: vOptFType] : ! [v1: % 38.28/5.99 vOptFType] : ! [v2: vFType] : (v1 = v0 | ~ (vsomeFType(v2) = v1) | ~ % 38.28/5.99 (vsomeFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vVal] : (v1 % 38.28/5.99 = v0 | ~ (venumVal(v2) = v1) | ~ (venumVal(v2) = v0)) & ! [v0: vPred] : % 38.28/5.99 ! [v1: vPred] : ! [v2: vPred] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) % 38.28/5.99 = v0)) & ! [v0: vOptVal] : ! [v1: vOptVal] : ! [v2: vVal] : (v1 = v0 | % 38.28/5.99 ~ (vsomeVal(v2) = v1) | ~ (vsomeVal(v2) = v0)) & ! [v0: vExp] : ! [v1: % 38.28/5.99 vExp] : ! [v2: vName] : (v1 = v0 | ~ (vlookup(v2) = v1) | ~ (vlookup(v2) % 38.28/5.99 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vVal] : (v1 = v0 | ~ % 38.28/5.99 (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & ! [v0: vName] : ! [v1: % 38.28/5.99 vName] : ! [v2: vName] : (v1 = v0 | ~ (venumName(v2) = v1) | ~ % 38.28/5.99 (venumName(v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: % 38.28/5.99 vQuery] : (v1 = v0 | ~ (vsomeQuery(v2) = v1) | ~ (vsomeQuery(v2) = v0)) & % 38.28/5.99 ! [v0: vFType] : ! [v1: vFType] : ! [v2: vFType] : (v1 = v0 | ~ % 38.28/5.99 (venumFType(v2) = v1) | ~ (venumFType(v2) = v0)) & ! [v0: vOptTType] : ! % 38.28/5.99 [v1: vOptTType] : ! [v2: vTType] : (v1 = v0 | ~ (vsomeTType(v2) = v1) | ~ % 38.28/5.99 (vsomeTType(v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! % 38.28/5.99 [v2: vRawTable] : (v1 = v0 | ~ (vsomeRawTable(v2) = v1) | ~ % 38.28/5.99 (vsomeRawTable(v2) = v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! % 38.28/5.99 [v2: vTable] : (v1 = v0 | ~ (vsomeTable(v2) = v1) | ~ (vsomeTable(v2) = v0)) % 38.28/5.99 & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vTable] : (v1 = v0 | ~ % 38.28/5.99 (vtvalue(v2) = v1) | ~ (vtvalue(v2) = v0)) & ! [v0: vSelect] : ! [v1: % 38.28/5.99 vSelect] : ! [v2: vAttrL] : (v1 = v0 | ~ (vlist(v2) = v1) | ~ (vlist(v2) % 38.28/5.99 = v0)) % 38.28/5.99 % 38.28/5.99 Further assumptions not needed in the proof: % 38.28/5.99 -------------------------------------------- % 38.28/5.99 DIFF-Intersection-Difference, DIFF-Union-Difference, DIFF-Union-Intersection, % 38.28/5.99 DIFF-aempty-acons, DIFF-all-list, DIFF-and-eq, DIFF-and-gt, DIFF-and-lt, % 38.28/5.99 DIFF-and-not, DIFF-constant-lookup, DIFF-emptyContext-bindContext, % 38.28/5.99 DIFF-emptyStore-bindStore, DIFF-eq-gt, DIFF-eq-lt, DIFF-gt-lt, % 38.28/5.99 DIFF-initFType-enumFType, DIFF-initName-enumName, DIFF-initVal-enumVal, % 38.28/5.99 DIFF-noFType-someFType, DIFF-noQuery-someQuery, DIFF-noTType-someTType, % 38.28/5.99 DIFF-noTable-someTable, DIFF-noVal-someVal, DIFF-not-eq, DIFF-not-gt, % 38.28/5.99 DIFF-not-lt, DIFF-ptrue-and, DIFF-ptrue-eq, DIFF-ptrue-gt, DIFF-ptrue-lt, % 38.28/5.99 DIFF-ptrue-not, DIFF-rempty-rcons, DIFF-selectFromWhere-Difference, % 38.28/5.99 DIFF-selectFromWhere-Intersection, DIFF-selectFromWhere-Union, % 38.28/5.99 DIFF-tempty-tcons, DIFF-ttempty-ttcons, DIFF-tvalue-Difference, % 38.28/5.99 DIFF-tvalue-Intersection, DIFF-tvalue-Union, DIFF-tvalue-selectFromWhere, % 38.28/5.99 EQ-Difference, EQ-Intersection, EQ-Union, EQ-acons, EQ-and, EQ-bindContext, % 38.28/5.99 EQ-bindStore, EQ-constant, EQ-enumFType, EQ-enumName, EQ-enumVal, EQ-eq, EQ-gt, % 38.28/5.99 EQ-list, EQ-lookup, EQ-lt, EQ-not, EQ-rcons, EQ-selectFromWhere, EQ-someFType, % 38.28/5.99 EQ-someQuery, EQ-someRawTable, EQ-someTType, EQ-someTable, EQ-someVal, EQ-tcons, % 38.28/5.99 EQ-ttcons, EQ-tvalue, TDifference, TDifference_inv1, TDifference_inv2, % 38.28/5.99 TIntersection, TIntersection_inv1, TIntersection_inv2, TSelectFromWhere, % 38.28/5.99 TSelectFromWhere_inv, TTTContextDuplicate, TTTContextSwap, TUnion, TUnion_inv1, % 38.28/5.99 TUnion_inv2, Ttvalue, Ttvalue_inv, append-0, append-1, append-INV, % 38.28/5.99 attachColToFrontRaw-0, attachColToFrontRaw-1, attachColToFrontRaw-2, % 38.28/5.99 attachColToFrontRaw-INV, dom-AttrL, dom-Exp, dom-OptFType, dom-OptQuery, % 38.28/5.99 dom-OptRawTable, dom-OptTType, dom-OptTable, dom-OptVal, dom-Pred, dom-Query, % 38.28/5.99 dom-RawTable, dom-Row, dom-Select, dom-TStore, dom-TTContext, dom-TType, % 38.28/5.99 dom-Table, dropFirstColRaw-0, dropFirstColRaw-1, dropFirstColRaw-2, % 38.28/5.99 dropFirstColRaw-INV, evalExpRow-0, evalExpRow-1, evalExpRow-2, evalExpRow-3, % 38.28/5.99 evalExpRow-INV, filterRows-0, filterRows-1, filterRows-2, filterRows-INV, % 38.28/5.99 filterSingleRow-0, filterSingleRow-1, filterSingleRow-2, filterSingleRow-3, % 38.28/5.99 filterSingleRow-4, filterSingleRow-5, filterSingleRow-false-INV, % 38.28/5.99 filterSingleRow-true-INV, filterTable-0, filterTable-INV, findCol-0, findCol-1, % 38.28/5.99 findCol-2, findCol-INV, findColType-0, findColType-1, findColType-2, % 38.28/5.99 findColType-INV, getAttrL-0, getFType-0, getQuery-0, getRaw-0, getRawTable-0, % 38.28/5.99 getTType-0, getTable-0, getVal-0, isSomeFType-0, isSomeFType-1, % 38.28/5.99 isSomeFType-false-INV, isSomeFType-true-INV, isSomeQuery-0, isSomeQuery-1, % 38.28/5.99 isSomeQuery-false-INV, isSomeQuery-true-INV, isSomeRawTable-0, isSomeRawTable-1, % 38.28/5.99 isSomeRawTable-true-INV, isSomeTType-0, isSomeTType-1, isSomeTType-false-INV, % 38.28/5.99 isSomeTType-true-INV, isSomeTable-0, isSomeTable-1, isSomeTable-false-INV, % 38.28/5.99 isSomeTable-true-INV, isSomeVal-0, isSomeVal-1, isSomeVal-false-INV, % 38.28/5.99 isSomeVal-true-INV, isValue-0, isValue-1, isValue-2, isValue-3, isValue-4, % 38.28/5.99 isValue-false-INV, isValue-true-INV, lookupContext-0, lookupContext-1, % 38.28/5.99 lookupContext-2, lookupContext-INV, lookupStore-0, lookupStore-1, lookupStore-2, % 38.28/5.99 lookupStore-INV, matchingAttrL-0, matchingAttrL-1, matchingAttrL-2, % 38.28/5.99 matchingAttrL-false-INV, matchingAttrL-true-INV, projectCols-0, projectCols-1, % 38.28/5.99 projectCols-2, projectCols-INV, projectColsPreservesRowCount, % 38.28/5.99 projectColsWelltypedWithSelectType, projectEmptyCol-0, projectEmptyCol-1, % 38.28/5.99 projectEmptyCol-INV, projectFirstRaw-0, projectFirstRaw-1, projectFirstRaw-2, % 38.28/5.99 projectFirstRaw-INV, projectTable-0, projectTable-1, projectTable-2, % 38.28/5.99 projectTable-INV, projectType-0, projectType-INV, projectTypeAttrL-0, % 38.28/5.99 projectTypeAttrL-1, projectTypeAttrL-2, projectTypeAttrL-INV, rawDifference-0, % 38.28/5.99 rawDifference-1, rawDifference-2, rawDifference-3, rawDifference-4, % 38.28/5.99 rawDifference-INV, rawIntersection-0, rawIntersection-1, rawIntersection-2, % 38.28/5.99 rawIntersection-3, rawIntersection-4, rawIntersection-INV, rawUnion-0, % 38.28/5.99 rawUnion-1, rawUnion-2, rawUnion-INV, reduce-0, reduce-1, reduce-10, reduce-11, % 38.28/5.99 reduce-12, reduce-13, reduce-14, reduce-15, reduce-16, reduce-17, reduce-18, % 38.28/5.99 reduce-2, reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, reduce-8, reduce-9, % 38.28/5.99 reduce-INV, rowIn-0, rowIn-1, rowIn-false-INV, rowIn-true-INV, sameLength-0, % 38.28/5.99 sameLength-1, sameLength-2, sameLength-false-INV, sameLength-true-INV, % 38.28/5.99 storeContextConsistent-0, storeContextConsistent-1, storeContextConsistent-2, % 38.28/5.99 storeContextConsistent-false-INV, storeContextConsistent-true-INV, tcheckPred-0, % 38.28/5.99 tcheckPred-1, tcheckPred-2, tcheckPred-3, tcheckPred-4, tcheckPred-5, % 38.28/5.99 tcheckPred-false-INV, tcheckPred-true-INV, typeOfExp-0, typeOfExp-1, % 38.28/5.99 typeOfExp-2, typeOfExp-3, typeOfExp-INV, welltypedRawtable-0, % 38.28/5.99 welltypedRawtable-1, welltypedRawtable-false-INV, welltypedRawtable-true-INV, % 38.28/5.99 welltypedRow-0, welltypedRow-1, welltypedRow-2, welltypedRow-false-INV, % 38.28/5.99 welltypedRow-true-INV, welltypedtable-0, welltypedtable-false-INV % 38.28/5.99 % 38.28/5.99 Those formulas are unsatisfiable: % 38.28/5.99 --------------------------------- % 38.28/5.99 % 38.28/5.99 Begin of proof % 38.28/5.99 | % 38.28/6.00 | ALPHA: (DIFF-noRawTable-someRawTable) implies: % 38.28/6.00 | (1) ! [v0: vRawTable] : ( ~ (vsomeRawTable(v0) = vnoRawTable) | ~ % 38.28/6.00 | vRawTable(v0)) % 38.28/6.00 | % 38.28/6.00 | ALPHA: (isSomeRawTable-false-INV) implies: % 38.28/6.00 | (2) ! [v0: vOptRawTable] : ! [v1: int] : (v1 = 0 | v0 = vnoRawTable | ~ % 38.28/6.00 | (visSomeRawTable(v0) = v1) | ~ vOptRawTable(v0)) % 38.28/6.00 | % 38.28/6.00 | ALPHA: (function-axioms) implies: % 38.28/6.00 | (3) ! [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! [v2: vRawTable] : ! % 38.28/6.00 | [v3: vAttrL] : ! [v4: vAttrL] : (v1 = v0 | ~ (vprojectCols(v4, v3, % 38.28/6.00 | v2) = v1) | ~ (vprojectCols(v4, v3, v2) = v0)) % 38.28/6.00 | % 38.28/6.00 | DELTA: instantiating (projectTableProgress-list-isSomeRawTable-False) with % 38.28/6.00 | fresh symbols all_339_0, all_339_1, all_339_2, all_339_3, all_339_4, % 38.28/6.00 | all_339_5, all_339_6, all_339_7, all_339_8, all_339_9, all_339_10 % 38.28/6.00 | gives: % 38.28/6.00 | (4) ~ (all_339_3 = 0) & vprojectType(all_339_2, all_339_8) = all_339_1 & % 38.28/6.00 | vprojectTable(all_339_2, all_339_9) = all_339_0 & % 38.28/6.00 | vprojectCols(all_339_10, all_339_6, all_339_5) = all_339_4 & % 38.28/6.00 | visSomeRawTable(all_339_4) = all_339_3 & vwelltypedtable(all_339_8, % 38.28/6.00 | all_339_9) = 0 & vgetAttrL(all_339_9) = all_339_6 & % 38.28/6.00 | vgetRaw(all_339_9) = all_339_5 & vsomeTType(all_339_7) = all_339_1 & % 38.28/6.00 | vlist(all_339_10) = all_339_2 & vSelect(all_339_2) & vTType(all_339_7) % 38.28/6.00 | & vTType(all_339_8) & vTable(all_339_9) & vOptTable(all_339_0) & % 38.28/6.00 | vOptTType(all_339_1) & vOptRawTable(all_339_4) & vRawTable(all_339_5) & % 38.28/6.00 | vAttrL(all_339_6) & vAttrL(all_339_10) & ! [v0: vTable] : ( ~ % 38.28/6.00 | (vsomeTable(v0) = all_339_0) | ~ vTable(v0)) % 38.28/6.00 | % 38.28/6.00 | ALPHA: (4) implies: % 38.28/6.00 | (5) ~ (all_339_3 = 0) % 38.28/6.00 | (6) vAttrL(all_339_10) % 38.28/6.00 | (7) vOptRawTable(all_339_4) % 38.28/6.00 | (8) vTable(all_339_9) % 38.28/6.00 | (9) vTType(all_339_8) % 38.28/6.00 | (10) vTType(all_339_7) % 38.28/6.00 | (11) vlist(all_339_10) = all_339_2 % 38.28/6.00 | (12) vsomeTType(all_339_7) = all_339_1 % 38.28/6.00 | (13) vgetRaw(all_339_9) = all_339_5 % 38.28/6.00 | (14) vgetAttrL(all_339_9) = all_339_6 % 38.28/6.00 | (15) vwelltypedtable(all_339_8, all_339_9) = 0 % 38.28/6.00 | (16) visSomeRawTable(all_339_4) = all_339_3 % 38.28/6.00 | (17) vprojectCols(all_339_10, all_339_6, all_339_5) = all_339_4 % 38.28/6.00 | (18) vprojectType(all_339_2, all_339_8) = all_339_1 % 38.28/6.00 | % 38.28/6.00 | GROUND_INST: instantiating (getRaw-INV) with all_339_9, all_339_5, simplifying % 38.28/6.00 | with (8), (13) gives: % 38.28/6.00 | (19) ? [v0: vAttrL] : (vtable(v0, all_339_5) = all_339_9 & % 38.28/6.00 | vRawTable(all_339_5) & vAttrL(v0)) % 38.28/6.00 | % 38.28/6.00 | GROUND_INST: instantiating (getAttrL-INV) with all_339_9, all_339_6, % 38.28/6.00 | simplifying with (8), (14) gives: % 38.28/6.00 | (20) ? [v0: vRawTable] : (vtable(all_339_6, v0) = all_339_9 & % 38.28/6.00 | vRawTable(v0) & vAttrL(all_339_6)) % 38.28/6.00 | % 38.28/6.00 | GROUND_INST: instantiating (welltypedtable-true-INV) with all_339_8, % 38.28/6.00 | all_339_9, simplifying with (8), (9), (15) gives: % 38.28/6.01 | (21) ? [v0: vAttrL] : ? [v1: vRawTable] : (vwelltypedRawtable(all_339_8, % 38.28/6.01 | v1) = 0 & vmatchingAttrL(all_339_8, v0) = 0 & vtable(v0, v1) = % 38.28/6.01 | all_339_9 & vRawTable(v1) & vAttrL(v0)) % 38.28/6.01 | % 38.28/6.01 | GROUND_INST: instantiating (2) with all_339_4, all_339_3, simplifying with % 38.28/6.01 | (7), (16) gives: % 38.28/6.01 | (22) all_339_3 = 0 | all_339_4 = vnoRawTable % 38.28/6.01 | % 38.28/6.01 | GROUND_INST: instantiating (projectType-1) with all_339_10, all_339_8, % 38.28/6.01 | all_339_2, all_339_1, simplifying with (6), (9), (11), (18) % 38.28/6.01 | gives: % 38.28/6.01 | (23) vprojectTypeAttrL(all_339_10, all_339_8) = all_339_1 & % 38.28/6.01 | vOptTType(all_339_1) % 38.28/6.01 | % 38.28/6.01 | ALPHA: (23) implies: % 38.28/6.01 | (24) vprojectTypeAttrL(all_339_10, all_339_8) = all_339_1 % 38.28/6.01 | % 38.28/6.01 | DELTA: instantiating (20) with fresh symbol all_358_0 gives: % 38.28/6.01 | (25) vtable(all_339_6, all_358_0) = all_339_9 & vRawTable(all_358_0) & % 38.28/6.01 | vAttrL(all_339_6) % 38.28/6.01 | % 38.28/6.01 | ALPHA: (25) implies: % 38.28/6.01 | (26) vAttrL(all_339_6) % 38.28/6.01 | (27) vRawTable(all_358_0) % 38.28/6.01 | (28) vtable(all_339_6, all_358_0) = all_339_9 % 38.28/6.01 | % 38.28/6.01 | DELTA: instantiating (19) with fresh symbol all_360_0 gives: % 38.28/6.01 | (29) vtable(all_360_0, all_339_5) = all_339_9 & vRawTable(all_339_5) & % 38.28/6.01 | vAttrL(all_360_0) % 38.28/6.01 | % 38.28/6.01 | ALPHA: (29) implies: % 38.28/6.01 | (30) vAttrL(all_360_0) % 38.28/6.01 | (31) vRawTable(all_339_5) % 38.28/6.01 | (32) vtable(all_360_0, all_339_5) = all_339_9 % 38.28/6.01 | % 38.28/6.01 | DELTA: instantiating (21) with fresh symbols all_362_0, all_362_1 gives: % 38.28/6.01 | (33) vwelltypedRawtable(all_339_8, all_362_0) = 0 & % 38.28/6.01 | vmatchingAttrL(all_339_8, all_362_1) = 0 & vtable(all_362_1, % 38.28/6.01 | all_362_0) = all_339_9 & vRawTable(all_362_0) & vAttrL(all_362_1) % 38.28/6.01 | % 38.28/6.01 | ALPHA: (33) implies: % 38.28/6.01 | (34) vAttrL(all_362_1) % 38.28/6.01 | (35) vRawTable(all_362_0) % 38.28/6.01 | (36) vtable(all_362_1, all_362_0) = all_339_9 % 38.28/6.01 | (37) vmatchingAttrL(all_339_8, all_362_1) = 0 % 38.28/6.01 | (38) vwelltypedRawtable(all_339_8, all_362_0) = 0 % 38.28/6.01 | % 38.28/6.01 | BETA: splitting (22) gives: % 38.28/6.01 | % 38.28/6.01 | Case 1: % 38.28/6.01 | | % 38.28/6.01 | | (39) all_339_3 = 0 % 38.28/6.01 | | % 38.28/6.01 | | REDUCE: (5), (39) imply: % 38.28/6.01 | | (40) $false % 38.28/6.01 | | % 38.28/6.01 | | CLOSE: (40) is inconsistent. % 38.28/6.01 | | % 38.28/6.01 | Case 2: % 38.28/6.01 | | % 38.28/6.01 | | (41) all_339_4 = vnoRawTable % 38.28/6.01 | | % 38.28/6.01 | | REDUCE: (17), (41) imply: % 38.28/6.01 | | (42) vprojectCols(all_339_10, all_339_6, all_339_5) = vnoRawTable % 38.28/6.01 | | % 38.28/6.01 | | GROUND_INST: instantiating (EQ-table) with all_360_0, all_339_5, all_362_1, % 38.28/6.01 | | all_362_0, all_339_9, simplifying with (30), (31), (32), (34), % 38.28/6.01 | | (35), (36) gives: % 38.28/6.01 | | (43) all_362_0 = all_339_5 & all_362_1 = all_360_0 % 38.28/6.01 | | % 38.28/6.01 | | ALPHA: (43) implies: % 38.79/6.01 | | (44) all_362_1 = all_360_0 % 38.79/6.01 | | (45) all_362_0 = all_339_5 % 38.79/6.01 | | % 38.79/6.01 | | GROUND_INST: instantiating (EQ-table) with all_339_6, all_358_0, all_362_1, % 38.79/6.01 | | all_362_0, all_339_9, simplifying with (26), (27), (28), (34), % 38.79/6.01 | | (35), (36) gives: % 38.79/6.01 | | (46) all_362_0 = all_358_0 & all_362_1 = all_339_6 % 38.79/6.01 | | % 38.79/6.01 | | ALPHA: (46) implies: % 38.79/6.01 | | (47) all_362_1 = all_339_6 % 38.79/6.01 | | (48) all_362_0 = all_358_0 % 38.79/6.01 | | % 38.79/6.02 | | GROUND_INST: instantiating (projectColsProgress) with all_362_1, all_362_0, % 38.79/6.02 | | all_339_7, all_339_10, all_339_8, all_339_1, simplifying with % 38.79/6.02 | | (6), (9), (10), (12), (24), (34), (35), (37), (38) gives: % 38.79/6.02 | | (49) ? [v0: vOptRawTable] : (vprojectCols(all_339_10, all_362_1, % 38.79/6.02 | | all_362_0) = v0 & vOptRawTable(v0) & ? [v1: vRawTable] : % 38.79/6.02 | | (vsomeRawTable(v1) = v0 & vRawTable(v1))) % 38.79/6.02 | | % 38.79/6.02 | | COMBINE_EQS: (45), (48) imply: % 38.79/6.02 | | (50) all_358_0 = all_339_5 % 38.79/6.02 | | % 38.79/6.02 | | COMBINE_EQS: (44), (47) imply: % 38.79/6.02 | | (51) all_360_0 = all_339_6 % 38.79/6.02 | | % 38.79/6.02 | | DELTA: instantiating (49) with fresh symbol all_398_0 gives: % 38.79/6.02 | | (52) vprojectCols(all_339_10, all_362_1, all_362_0) = all_398_0 & % 38.79/6.02 | | vOptRawTable(all_398_0) & ? [v0: vRawTable] : (vsomeRawTable(v0) = % 38.79/6.02 | | all_398_0 & vRawTable(v0)) % 38.79/6.02 | | % 38.79/6.02 | | ALPHA: (52) implies: % 38.79/6.02 | | (53) vprojectCols(all_339_10, all_362_1, all_362_0) = all_398_0 % 38.79/6.02 | | (54) ? [v0: vRawTable] : (vsomeRawTable(v0) = all_398_0 & vRawTable(v0)) % 38.79/6.02 | | % 38.79/6.02 | | DELTA: instantiating (54) with fresh symbol all_400_0 gives: % 38.79/6.02 | | (55) vsomeRawTable(all_400_0) = all_398_0 & vRawTable(all_400_0) % 38.79/6.02 | | % 38.79/6.02 | | ALPHA: (55) implies: % 38.79/6.02 | | (56) vRawTable(all_400_0) % 38.79/6.02 | | (57) vsomeRawTable(all_400_0) = all_398_0 % 38.79/6.02 | | % 38.79/6.02 | | REDUCE: (45), (47), (53) imply: % 38.79/6.02 | | (58) vprojectCols(all_339_10, all_339_6, all_339_5) = all_398_0 % 38.79/6.02 | | % 38.79/6.02 | | GROUND_INST: instantiating (3) with vnoRawTable, all_398_0, all_339_5, % 38.79/6.02 | | all_339_6, all_339_10, simplifying with (42), (58) gives: % 38.79/6.02 | | (59) all_398_0 = vnoRawTable % 38.79/6.02 | | % 38.79/6.02 | | REDUCE: (57), (59) imply: % 38.79/6.02 | | (60) vsomeRawTable(all_400_0) = vnoRawTable % 38.79/6.02 | | % 38.79/6.02 | | GROUND_INST: instantiating (1) with all_400_0, simplifying with (56), (60) % 38.79/6.02 | | gives: % 38.79/6.02 | | (61) $false % 38.79/6.02 | | % 38.79/6.02 | | CLOSE: (61) is inconsistent. % 38.79/6.02 | | % 38.79/6.02 | End of split % 38.79/6.02 | % 38.79/6.02 End of proof % 38.79/6.02 % SZS output end Proof for theBenchmark % 38.79/6.02 % 38.79/6.02 5416ms %------------------------------------------------------------------------------