%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM280_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 : n022.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:41 PM UTC 2026 % Result : Theorem 33.47s 5.10s % Output : Proof 108.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.14 % Problem : COM280_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.15 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.36 % Computer : n022.cluster.edu % 0.16/0.36 % Model : x86_64 x86_64 % 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.36 % Memory : 8042.1875MB % 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.36 % CPULimit : 300 % 0.16/0.36 % WCLimit : 300 % 0.16/0.36 % DateTime : Mon May 4 20:13:36 EDT 2026 % 0.16/0.36 % CPUTime : % 0.63/0.63 ________ _____ % 0.63/0.63 ___ __ \_________(_)________________________________ % 0.63/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.63/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.63/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.63/0.63 % 0.63/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.63/0.63 (2023-06-19) % 0.63/0.63 % 0.63/0.63 (c) Philipp Rümmer, 2009-2023 % 0.63/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.63/0.63 Amanda Stjerna. % 0.63/0.63 Free software under BSD-3-Clause. % 0.63/0.63 % 0.63/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.63/0.63 % 0.63/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.63/0.64 Running up to 7 provers in parallel. % 0.63/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.63/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.63/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.63/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.63/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.63/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.63/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 9.19/1.97 Prover 1: Preprocessing ... % 10.88/2.13 Prover 2: Preprocessing ... % 10.88/2.13 Prover 6: Preprocessing ... % 10.88/2.13 Prover 5: Preprocessing ... % 11.53/2.21 Prover 4: Preprocessing ... % 11.53/2.21 Prover 0: Preprocessing ... % 11.53/2.23 Prover 3: Preprocessing ... % 24.77/4.00 Prover 1: Warning: ignoring some quantifiers % 25.62/4.05 Prover 3: Warning: ignoring some quantifiers % 25.62/4.07 Prover 4: Warning: ignoring some quantifiers % 25.62/4.09 Prover 3: Constructing countermodel ... % 25.62/4.10 Prover 1: Constructing countermodel ... % 26.44/4.12 Prover 6: Proving ... % 26.44/4.17 Prover 0: Proving ... % 26.44/4.17 Prover 4: Constructing countermodel ... % 27.03/4.26 Prover 5: Proving ... % 30.16/4.65 Prover 2: Proving ... % 33.47/5.09 Prover 6: proved (4439ms) % 33.47/5.09 % 33.47/5.10 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.47/5.10 % 33.47/5.11 Prover 0: stopped % 33.47/5.11 Prover 5: stopped % 33.47/5.12 Prover 3: stopped % 34.26/5.12 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 34.26/5.12 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 34.26/5.12 Prover 2: stopped % 34.26/5.13 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 34.26/5.13 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 34.26/5.13 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 40.30/5.91 Prover 7: Preprocessing ... % 40.30/5.92 Prover 13: Preprocessing ... % 40.30/5.92 Prover 8: Preprocessing ... % 40.30/5.94 Prover 11: Preprocessing ... % 40.30/5.96 Prover 10: Preprocessing ... % 45.83/6.61 Prover 8: Warning: ignoring some quantifiers % 45.83/6.67 Prover 8: Constructing countermodel ... % 46.59/6.72 Prover 7: Warning: ignoring some quantifiers % 46.59/6.76 Prover 10: Warning: ignoring some quantifiers % 46.59/6.77 Prover 7: Constructing countermodel ... % 47.39/6.80 Prover 10: Constructing countermodel ... % 48.18/6.93 Prover 11: Warning: ignoring some quantifiers % 48.18/6.96 Prover 11: Constructing countermodel ... % 49.07/7.03 Prover 13: Warning: ignoring some quantifiers % 49.86/7.12 Prover 13: Constructing countermodel ... % 73.53/10.18 Prover 13: stopped % 73.53/10.20 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 76.55/10.51 Prover 16: Preprocessing ... % 81.43/11.15 Prover 16: Warning: ignoring some quantifiers % 82.10/11.22 Prover 16: Constructing countermodel ... % 107.37/14.46 Prover 7: Found proof (size 44) % 107.37/14.46 Prover 7: proved (9266ms) % 107.37/14.46 Prover 1: stopped % 107.37/14.46 Prover 10: stopped % 107.37/14.46 Prover 16: stopped % 107.37/14.46 Prover 4: stopped % 107.37/14.46 Prover 8: stopped % 107.37/14.46 Prover 11: stopped % 107.37/14.46 % 107.37/14.46 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 107.37/14.46 % 107.37/14.47 % SZS output start Proof for theBenchmark % 107.37/14.48 Assumptions after simplification: % 107.37/14.48 --------------------------------- % 107.37/14.48 % 107.37/14.48 (DIFF-rempty-rcons) % 108.03/14.50 vRow(vrempty) & ! [v0: vVal] : ! [v1: vRow] : ( ~ (vrcons(v0, v1) = vrempty) % 108.03/14.50 | ~ vVal(v0) | ~ vRow(v1)) % 108.03/14.50 % 108.03/14.50 (DIFF-tempty-tcons) % 108.03/14.50 vRawTable(vtempty) & ! [v0: vRow] : ! [v1: vRawTable] : ( ~ (vtcons(v0, v1) % 108.03/14.50 = vtempty) | ~ vRawTable(v1) | ~ vRow(v0)) % 108.03/14.50 % 108.03/14.50 (DIFF-ttempty-ttcons) % 108.03/14.50 vTType(vttempty) & ! [v0: vName] : ! [v1: vFType] : ! [v2: vTType] : ( ~ % 108.03/14.50 (vttcons(v0, v1, v2) = vttempty) | ~ vTType(v2) | ~ vFType(v1) | ~ % 108.03/14.50 vName(v0)) % 108.03/14.50 % 108.03/14.50 (dropFirstColRaw-1) % 108.03/14.51 vRow(vrempty) & ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ % 108.03/14.51 (vdropFirstColRaw(v0) = v1) | ~ vRawTable(v0) | ? [v2: vRawTable] : ? % 108.03/14.51 [v3: vRawTable] : (vdropFirstColRaw(v2) = v3 & vtcons(vrempty, v1) = v3 & % 108.03/14.51 vtcons(vrempty, v0) = v2 & vRawTable(v3) & vRawTable(v2))) & ! [v0: % 108.03/14.51 vRawTable] : ! [v1: vRawTable] : ( ~ (vtcons(vrempty, v0) = v1) | ~ % 108.03/14.51 vRawTable(v0) | ? [v2: vRawTable] : ? [v3: vRawTable] : % 108.03/14.51 (vdropFirstColRaw(v1) = v2 & vdropFirstColRaw(v0) = v3 & vtcons(vrempty, v3) % 108.03/14.51 = v2 & vRawTable(v3) & vRawTable(v2))) % 108.03/14.51 % 108.03/14.51 (dropFirstColRaw-INV) % 108.03/14.51 vRawTable(vtempty) & vRow(vrempty) & ! [v0: vRawTable] : ! [v1: vRawTable] : % 108.03/14.51 (v1 = vtempty | ~ (vdropFirstColRaw(v0) = v1) | ~ vRawTable(v0) | ? [v2: % 108.03/14.51 vVal] : ? [v3: vRow] : ? [v4: vRawTable] : ? [v5: vRow] : ? [v6: % 108.03/14.51 vRawTable] : ? [v7: vRawTable] : ? [v8: vRawTable] : ? [v9: vRawTable] % 108.03/14.51 : ? [v10: vRawTable] : ? [v11: vRawTable] : ? [v12: vRawTable] : % 108.03/14.51 (vVal(v2) & vRawTable(v9) & vRawTable(v4) & vRow(v3) & ((v12 = v1 & v10 = v0 % 108.03/14.51 & vdropFirstColRaw(v9) = v11 & vtcons(vrempty, v11) = v1 & % 108.03/14.51 vtcons(vrempty, v9) = v0 & vRawTable(v11) & vRawTable(v1)) | (v8 = v1 % 108.03/14.51 & v6 = v0 & vdropFirstColRaw(v4) = v7 & vtcons(v5, v4) = v0 & % 108.03/14.51 vtcons(v3, v7) = v1 & vrcons(v2, v3) = v5 & vRawTable(v7) & % 108.03/14.51 vRawTable(v1) & vRow(v5))))) & ! [v0: vRawTable] : ! [v1: vRawTable] % 108.03/14.51 : (v0 = vtempty | ~ (vdropFirstColRaw(v0) = v1) | ~ vRawTable(v0) | ? [v2: % 108.03/14.51 vVal] : ? [v3: vRow] : ? [v4: vRawTable] : ? [v5: vRow] : ? [v6: % 108.03/14.51 vRawTable] : ? [v7: vRawTable] : ? [v8: vRawTable] : ? [v9: vRawTable] % 108.03/14.51 : ? [v10: vRawTable] : ? [v11: vRawTable] : ? [v12: vRawTable] : % 108.03/14.51 (vVal(v2) & vRawTable(v9) & vRawTable(v4) & vRow(v3) & ((v12 = v1 & v10 = v0 % 108.03/14.51 & vdropFirstColRaw(v9) = v11 & vtcons(vrempty, v11) = v1 & % 108.03/14.51 vtcons(vrempty, v9) = v0 & vRawTable(v11) & vRawTable(v1)) | (v8 = v1 % 108.03/14.51 & v6 = v0 & vdropFirstColRaw(v4) = v7 & vtcons(v5, v4) = v0 & % 108.03/14.51 vtcons(v3, v7) = v1 & vrcons(v2, v3) = v5 & vRawTable(v7) & % 108.03/14.51 vRawTable(v1) & vRow(v5))))) % 108.03/14.51 % 108.03/14.51 (dropFirstColRawPreservesWelltypedRaw-tcons-IH0) % 108.03/14.51 vRawTable(vrt2) & ? [v0: vRawTable] : (vdropFirstColRaw(vrt2) = v0 & % 108.03/14.51 vRawTable(v0) & ! [v1: vName] : ! [v2: vFType] : ! [v3: vTType] : ! [v4: % 108.03/14.51 vTType] : ( ~ (vttcons(v1, v2, v3) = v4) | ~ vTType(v3) | ~ vFType(v2) | % 108.03/14.51 ~ vName(v1) | ~ vwelltypedRawtable(v4, vrt2) | vwelltypedRawtable(v3, % 108.03/14.51 v0))) % 108.03/14.51 % 108.03/14.51 (dropFirstColRawPreservesWelltypedRaw-tcons-rempty) % 108.03/14.51 vRawTable(vrt2) & vRow(vrempty) & ? [v0: vRawTable] : ? [v1: vRawTable] : ? % 108.03/14.51 [v2: vName] : ? [v3: vFType] : ? [v4: vTType] : ? [v5: vTType] : % 108.03/14.51 (vdropFirstColRaw(v0) = v1 & vtcons(vrempty, vrt2) = v0 & vttcons(v2, v3, v4) % 108.03/14.51 = v5 & vTType(v5) & vTType(v4) & vFType(v3) & vRawTable(v1) & vRawTable(v0) % 108.03/14.51 & vName(v2) & vwelltypedRawtable(v5, v0) & ~ vwelltypedRawtable(v4, v1)) % 108.03/14.51 % 108.03/14.51 (welltypedRawtable-1) % 108.03/14.52 ! [v0: vTType] : ! [v1: vRow] : ! [v2: vRawTable] : ! [v3: vRawTable] : ( % 108.03/14.52 ~ (vtcons(v1, v2) = v3) | ~ vTType(v0) | ~ vRawTable(v2) | ~ vRow(v1) | % 108.03/14.52 ~ vwelltypedRow(v0, v1) | ~ vwelltypedRawtable(v0, v2) | % 108.03/14.52 vwelltypedRawtable(v0, v3)) & ! [v0: vTType] : ! [v1: vRow] : ! [v2: % 108.03/14.52 vRawTable] : ! [v3: vRawTable] : ( ~ (vtcons(v1, v2) = v3) | ~ vTType(v0) % 108.03/14.52 | ~ vRawTable(v2) | ~ vRow(v1) | ~ vwelltypedRawtable(v0, v3) | % 108.03/14.52 vwelltypedRow(v0, v1)) & ! [v0: vTType] : ! [v1: vRow] : ! [v2: % 108.03/14.52 vRawTable] : ! [v3: vRawTable] : ( ~ (vtcons(v1, v2) = v3) | ~ vTType(v0) % 108.03/14.52 | ~ vRawTable(v2) | ~ vRow(v1) | ~ vwelltypedRawtable(v0, v3) | % 108.03/14.52 vwelltypedRawtable(v0, v2)) % 108.03/14.52 % 108.03/14.52 (welltypedRow-true-INV) % 108.03/14.52 vTType(vttempty) & vRow(vrempty) & ! [v0: vTType] : ! [v1: vRow] : (v1 = % 108.03/14.52 vrempty | ~ vTType(v0) | ~ vRow(v1) | ~ vwelltypedRow(v0, v1) | ? [v2: % 108.03/14.52 vVal] : ? [v3: vTType] : ? [v4: vFType] : ? [v5: vName] : ? [v6: vRow] % 108.03/14.52 : (vfieldType(v2) = v4 & vrcons(v2, v6) = v1 & vttcons(v5, v4, v3) = v0 & % 108.03/14.52 vTType(v3) & vVal(v2) & vFType(v4) & vName(v5) & vRow(v6) & % 108.03/14.52 vwelltypedRow(v3, v6))) & ! [v0: vTType] : ! [v1: vRow] : (v0 = vttempty % 108.03/14.52 | ~ vTType(v0) | ~ vRow(v1) | ~ vwelltypedRow(v0, v1) | ? [v2: vVal] : % 108.03/14.52 ? [v3: vTType] : ? [v4: vFType] : ? [v5: vName] : ? [v6: vRow] : % 108.03/14.52 (vfieldType(v2) = v4 & vrcons(v2, v6) = v1 & vttcons(v5, v4, v3) = v0 & % 108.03/14.52 vTType(v3) & vVal(v2) & vFType(v4) & vName(v5) & vRow(v6) & % 108.03/14.52 vwelltypedRow(v3, v6))) % 108.03/14.52 % 108.03/14.52 (function-axioms) % 108.03/14.54 ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vPred] : ! [v3: vAttrL] : % 108.03/14.54 ! [v4: vRawTable] : (v1 = v0 | ~ (vfilterRows(v4, v3, v2) = v1) | ~ % 108.03/14.54 (vfilterRows(v4, v3, v2) = v0)) & ! [v0: vOptVal] : ! [v1: vOptVal] : ! % 108.03/14.54 [v2: vRow] : ! [v3: vAttrL] : ! [v4: vExp] : (v1 = v0 | ~ (vevalExpRow(v4, % 108.03/14.54 v3, v2) = v1) | ~ (vevalExpRow(v4, v3, v2) = v0)) & ! [v0: % 108.03/14.54 vOptRawTable] : ! [v1: vOptRawTable] : ! [v2: vRawTable] : ! [v3: vAttrL] % 108.03/14.54 : ! [v4: vAttrL] : (v1 = v0 | ~ (vprojectCols(v4, v3, v2) = v1) | ~ % 108.03/14.54 (vprojectCols(v4, v3, v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: % 108.03/14.54 vOptRawTable] : ! [v2: vRawTable] : ! [v3: vAttrL] : ! [v4: vName] : (v1 % 108.03/14.54 = v0 | ~ (vfindCol(v4, v3, v2) = v1) | ~ (vfindCol(v4, v3, v2) = v0)) & ! % 108.03/14.54 [v0: vTStore] : ! [v1: vTStore] : ! [v2: vTStore] : ! [v3: vTable] : ! % 108.03/14.54 [v4: vName] : (v1 = v0 | ~ (vbindStore(v4, v3, v2) = v1) | ~ (vbindStore(v4, % 108.03/14.54 v3, v2) = v0)) & ! [v0: vTTContext] : ! [v1: vTTContext] : ! [v2: % 108.03/14.54 vTTContext] : ! [v3: vTType] : ! [v4: vName] : (v1 = v0 | ~ % 108.03/14.54 (vbindContext(v4, v3, v2) = v1) | ~ (vbindContext(v4, v3, v2) = v0)) & ! % 108.03/14.54 [v0: vTType] : ! [v1: vTType] : ! [v2: vTType] : ! [v3: vFType] : ! [v4: % 108.03/14.54 vName] : (v1 = v0 | ~ (vttcons(v4, v3, v2) = v1) | ~ (vttcons(v4, v3, v2) % 108.03/14.54 = v0)) & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vPred] : ! [v3: % 108.03/14.54 vName] : ! [v4: vSelect] : (v1 = v0 | ~ (vselectFromWhere(v4, v3, v2) = % 108.03/14.54 v1) | ~ (vselectFromWhere(v4, v3, v2) = v0)) & ! [v0: vOptFType] : ! % 108.03/14.54 [v1: vOptFType] : ! [v2: vTType] : ! [v3: vExp] : (v1 = v0 | ~ % 108.03/14.54 (vtypeOfExp(v3, v2) = v1) | ~ (vtypeOfExp(v3, v2) = v0)) & ! [v0: % 108.03/14.54 vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vSelect] : (v1 = % 108.03/14.54 v0 | ~ (vprojectType(v3, v2) = v1) | ~ (vprojectType(v3, v2) = v0)) & ! % 108.03/14.54 [v0: vOptTType] : ! [v1: vOptTType] : ! [v2: vTType] : ! [v3: vAttrL] : (v1 % 108.03/14.54 = v0 | ~ (vprojectTypeAttrL(v3, v2) = v1) | ~ (vprojectTypeAttrL(v3, v2) = % 108.03/14.54 v0)) & ! [v0: vOptFType] : ! [v1: vOptFType] : ! [v2: vTType] : ! [v3: % 108.03/14.54 vName] : (v1 = v0 | ~ (vfindColType(v3, v2) = v1) | ~ (vfindColType(v3, % 108.03/14.54 v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: vTStore] % 108.03/14.54 : ! [v3: vQuery] : (v1 = v0 | ~ (vreduce(v3, v2) = v1) | ~ (vreduce(v3, v2) % 108.03/14.54 = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! [v2: vPred] : ! [v3: % 108.03/14.54 vTable] : (v1 = v0 | ~ (vfilterTable(v3, v2) = v1) | ~ (vfilterTable(v3, % 108.03/14.54 v2) = v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! [v2: vTable] : % 108.03/14.54 ! [v3: vSelect] : (v1 = v0 | ~ (vprojectTable(v3, v2) = v1) | ~ % 108.03/14.54 (vprojectTable(v3, v2) = v0)) & ! [v0: vOptTType] : ! [v1: vOptTType] : ! % 108.03/14.54 [v2: vTTContext] : ! [v3: vName] : (v1 = v0 | ~ (vlookupContext(v3, v2) = % 108.03/14.54 v1) | ~ (vlookupContext(v3, v2) = v0)) & ! [v0: vOptTable] : ! [v1: % 108.03/14.54 vOptTable] : ! [v2: vTStore] : ! [v3: vName] : (v1 = v0 | ~ % 108.03/14.54 (vlookupStore(v3, v2) = v1) | ~ (vlookupStore(v3, v2) = v0)) & ! [v0: % 108.03/14.54 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : % 108.03/14.54 (v1 = v0 | ~ (vrawDifference(v3, v2) = v1) | ~ (vrawDifference(v3, v2) = % 108.03/14.54 v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! % 108.03/14.54 [v3: vRawTable] : (v1 = v0 | ~ (vrawIntersection(v3, v2) = v1) | ~ % 108.03/14.54 (vrawIntersection(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : % 108.03/14.54 ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ (vrawUnion(v3, v2) = % 108.03/14.54 v1) | ~ (vrawUnion(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: % 108.03/14.54 vRawTable] : ! [v2: vRawTable] : ! [v3: vRawTable] : (v1 = v0 | ~ % 108.03/14.54 (vattachColToFrontRaw(v3, v2) = v1) | ~ (vattachColToFrontRaw(v3, v2) = % 108.03/14.54 v0)) & ! [v0: vAttrL] : ! [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: % 108.03/14.54 vAttrL] : (v1 = v0 | ~ (vappend(v3, v2) = v1) | ~ (vappend(v3, v2) = v0)) % 108.03/14.54 & ! [v0: vAttrL] : ! [v1: vAttrL] : ! [v2: vAttrL] : ! [v3: vName] : (v1 = % 108.03/14.54 v0 | ~ (vacons(v3, v2) = v1) | ~ (vacons(v3, v2) = v0)) & ! [v0: vPred] : % 108.03/14.54 ! [v1: vPred] : ! [v2: vExp] : ! [v3: vExp] : (v1 = v0 | ~ (vlt(v3, v2) = % 108.03/14.54 v1) | ~ (vlt(v3, v2) = v0)) & ! [v0: vPred] : ! [v1: vPred] : ! [v2: % 108.03/14.54 vExp] : ! [v3: vExp] : (v1 = v0 | ~ (vgt(v3, v2) = v1) | ~ (vgt(v3, v2) = % 108.03/14.54 v0)) & ! [v0: vPred] : ! [v1: vPred] : ! [v2: vExp] : ! [v3: vExp] : % 108.03/14.54 (v1 = v0 | ~ (veq(v3, v2) = v1) | ~ (veq(v3, v2) = v0)) & ! [v0: vPred] : % 108.03/14.54 ! [v1: vPred] : ! [v2: vPred] : ! [v3: vPred] : (v1 = v0 | ~ (vand(v3, v2) % 108.03/14.54 = v1) | ~ (vand(v3, v2) = v0)) & ! [v0: vTable] : ! [v1: vTable] : ! % 108.03/14.54 [v2: vRawTable] : ! [v3: vAttrL] : (v1 = v0 | ~ (vtable(v3, v2) = v1) | ~ % 108.03/14.54 (vtable(v3, v2) = v0)) & ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: % 108.03/14.54 vRawTable] : ! [v3: vRow] : (v1 = v0 | ~ (vtcons(v3, v2) = v1) | ~ % 108.03/14.54 (vtcons(v3, v2) = v0)) & ! [v0: vRow] : ! [v1: vRow] : ! [v2: vRow] : ! % 108.03/14.54 [v3: vVal] : (v1 = v0 | ~ (vrcons(v3, v2) = v1) | ~ (vrcons(v3, v2) = v0)) & % 108.03/14.54 ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = % 108.03/14.54 v0 | ~ (vDifference(v3, v2) = v1) | ~ (vDifference(v3, v2) = v0)) & ! % 108.03/14.54 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 108.03/14.54 | ~ (vIntersection(v3, v2) = v1) | ~ (vIntersection(v3, v2) = v0)) & ! % 108.03/14.54 [v0: vQuery] : ! [v1: vQuery] : ! [v2: vQuery] : ! [v3: vQuery] : (v1 = v0 % 108.03/14.54 | ~ (vUnion(v3, v2) = v1) | ~ (vUnion(v3, v2) = v0)) & ! [v0: vRawTable] % 108.03/14.54 : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 108.03/14.54 (vprojectEmptyCol(v2) = v1) | ~ (vprojectEmptyCol(v2) = v0)) & ! [v0: % 108.03/14.54 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 108.03/14.54 (vdropFirstColRaw(v2) = v1) | ~ (vdropFirstColRaw(v2) = v0)) & ! [v0: % 108.03/14.54 vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : (v1 = v0 | ~ % 108.03/14.54 (vprojectFirstRaw(v2) = v1) | ~ (vprojectFirstRaw(v2) = v0)) & ! [v0: % 108.03/14.54 vFType] : ! [v1: vFType] : ! [v2: vVal] : (v1 = v0 | ~ (vfieldType(v2) = % 108.03/14.54 v1) | ~ (vfieldType(v2) = v0)) & ! [v0: vAttrL] : ! [v1: vAttrL] : ! % 108.03/14.54 [v2: vTable] : (v1 = v0 | ~ (vgetAttrL(v2) = v1) | ~ (vgetAttrL(v2) = v0)) & % 108.03/14.54 ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vTable] : (v1 = v0 | ~ % 108.03/14.54 (vgetRaw(v2) = v1) | ~ (vgetRaw(v2) = v0)) & ! [v0: vFType] : ! [v1: % 108.03/14.54 vFType] : ! [v2: vOptFType] : (v1 = v0 | ~ (vgetFType(v2) = v1) | ~ % 108.03/14.54 (vgetFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vOptVal] : % 108.03/14.54 (v1 = v0 | ~ (vgetVal(v2) = v1) | ~ (vgetVal(v2) = v0)) & ! [v0: vQuery] : % 108.03/14.54 ! [v1: vQuery] : ! [v2: vOptQuery] : (v1 = v0 | ~ (vgetQuery(v2) = v1) | ~ % 108.03/14.54 (vgetQuery(v2) = v0)) & ! [v0: vTType] : ! [v1: vTType] : ! [v2: % 108.03/14.54 vOptTType] : (v1 = v0 | ~ (vgetTType(v2) = v1) | ~ (vgetTType(v2) = v0)) & % 108.03/14.54 ! [v0: vTable] : ! [v1: vTable] : ! [v2: vOptTable] : (v1 = v0 | ~ % 108.03/14.54 (vgetTable(v2) = v1) | ~ (vgetTable(v2) = v0)) & ! [v0: vRawTable] : ! % 108.03/14.54 [v1: vRawTable] : ! [v2: vOptRawTable] : (v1 = v0 | ~ (vgetRawTable(v2) = % 108.03/14.54 v1) | ~ (vgetRawTable(v2) = v0)) & ! [v0: vOptFType] : ! [v1: % 108.03/14.54 vOptFType] : ! [v2: vFType] : (v1 = v0 | ~ (vsomeFType(v2) = v1) | ~ % 108.03/14.54 (vsomeFType(v2) = v0)) & ! [v0: vVal] : ! [v1: vVal] : ! [v2: vVal] : (v1 % 108.03/14.54 = v0 | ~ (venumVal(v2) = v1) | ~ (venumVal(v2) = v0)) & ! [v0: vPred] : % 108.03/14.54 ! [v1: vPred] : ! [v2: vPred] : (v1 = v0 | ~ (vnot(v2) = v1) | ~ (vnot(v2) % 108.03/14.54 = v0)) & ! [v0: vOptVal] : ! [v1: vOptVal] : ! [v2: vVal] : (v1 = v0 | % 108.03/14.54 ~ (vsomeVal(v2) = v1) | ~ (vsomeVal(v2) = v0)) & ! [v0: vExp] : ! [v1: % 108.03/14.54 vExp] : ! [v2: vName] : (v1 = v0 | ~ (vlookup(v2) = v1) | ~ (vlookup(v2) % 108.03/14.54 = v0)) & ! [v0: vExp] : ! [v1: vExp] : ! [v2: vVal] : (v1 = v0 | ~ % 108.03/14.54 (vconstant(v2) = v1) | ~ (vconstant(v2) = v0)) & ! [v0: vName] : ! [v1: % 108.03/14.54 vName] : ! [v2: vName] : (v1 = v0 | ~ (venumName(v2) = v1) | ~ % 108.03/14.54 (venumName(v2) = v0)) & ! [v0: vOptQuery] : ! [v1: vOptQuery] : ! [v2: % 108.03/14.54 vQuery] : (v1 = v0 | ~ (vsomeQuery(v2) = v1) | ~ (vsomeQuery(v2) = v0)) & % 108.03/14.54 ! [v0: vFType] : ! [v1: vFType] : ! [v2: vFType] : (v1 = v0 | ~ % 108.03/14.54 (venumFType(v2) = v1) | ~ (venumFType(v2) = v0)) & ! [v0: vOptTType] : ! % 108.03/14.54 [v1: vOptTType] : ! [v2: vTType] : (v1 = v0 | ~ (vsomeTType(v2) = v1) | ~ % 108.03/14.54 (vsomeTType(v2) = v0)) & ! [v0: vOptRawTable] : ! [v1: vOptRawTable] : ! % 108.03/14.54 [v2: vRawTable] : (v1 = v0 | ~ (vsomeRawTable(v2) = v1) | ~ % 108.03/14.54 (vsomeRawTable(v2) = v0)) & ! [v0: vOptTable] : ! [v1: vOptTable] : ! % 108.03/14.54 [v2: vTable] : (v1 = v0 | ~ (vsomeTable(v2) = v1) | ~ (vsomeTable(v2) = v0)) % 108.03/14.54 & ! [v0: vQuery] : ! [v1: vQuery] : ! [v2: vTable] : (v1 = v0 | ~ % 108.03/14.54 (vtvalue(v2) = v1) | ~ (vtvalue(v2) = v0)) & ! [v0: vSelect] : ! [v1: % 108.03/14.54 vSelect] : ! [v2: vAttrL] : (v1 = v0 | ~ (vlist(v2) = v1) | ~ (vlist(v2) % 108.03/14.54 = v0)) % 108.03/14.54 % 108.03/14.54 Further assumptions not needed in the proof: % 108.03/14.54 -------------------------------------------- % 108.03/14.54 DIFF-Intersection-Difference, DIFF-Union-Difference, DIFF-Union-Intersection, % 108.03/14.54 DIFF-aempty-acons, DIFF-all-list, DIFF-and-eq, DIFF-and-gt, DIFF-and-lt, % 108.03/14.54 DIFF-and-not, DIFF-constant-lookup, DIFF-emptyContext-bindContext, % 108.03/14.54 DIFF-emptyStore-bindStore, DIFF-eq-gt, DIFF-eq-lt, DIFF-gt-lt, % 108.03/14.54 DIFF-initFType-enumFType, DIFF-initName-enumName, DIFF-initVal-enumVal, % 108.03/14.54 DIFF-noFType-someFType, DIFF-noQuery-someQuery, DIFF-noRawTable-someRawTable, % 108.03/14.54 DIFF-noTType-someTType, DIFF-noTable-someTable, DIFF-noVal-someVal, DIFF-not-eq, % 108.03/14.54 DIFF-not-gt, DIFF-not-lt, DIFF-ptrue-and, DIFF-ptrue-eq, DIFF-ptrue-gt, % 108.03/14.54 DIFF-ptrue-lt, DIFF-ptrue-not, DIFF-selectFromWhere-Difference, % 108.03/14.54 DIFF-selectFromWhere-Intersection, DIFF-selectFromWhere-Union, % 108.03/14.54 DIFF-tvalue-Difference, DIFF-tvalue-Intersection, DIFF-tvalue-Union, % 108.03/14.54 DIFF-tvalue-selectFromWhere, EQ-Difference, EQ-Intersection, EQ-Union, EQ-acons, % 108.03/14.54 EQ-and, EQ-bindContext, EQ-bindStore, EQ-constant, EQ-enumFType, EQ-enumName, % 108.03/14.54 EQ-enumVal, EQ-eq, EQ-gt, EQ-list, EQ-lookup, EQ-lt, EQ-not, EQ-rcons, % 108.03/14.54 EQ-selectFromWhere, EQ-someFType, EQ-someQuery, EQ-someRawTable, EQ-someTType, % 108.03/14.54 EQ-someTable, EQ-someVal, EQ-table, EQ-tcons, EQ-ttcons, EQ-tvalue, TDifference, % 108.03/14.54 TDifference_inv1, TDifference_inv2, TIntersection, TIntersection_inv1, % 108.03/14.54 TIntersection_inv2, TSelectFromWhere, TSelectFromWhere_inv, TTTContextDuplicate, % 108.03/14.54 TTTContextSwap, TUnion, TUnion_inv1, TUnion_inv2, Ttvalue, Ttvalue_inv, % 108.03/14.54 append-0, append-1, append-INV, attachColToFrontRaw-0, attachColToFrontRaw-1, % 108.03/14.54 attachColToFrontRaw-2, attachColToFrontRaw-INV, dom-AttrL, dom-Exp, % 108.03/14.54 dom-OptFType, dom-OptQuery, dom-OptRawTable, dom-OptTType, dom-OptTable, % 108.03/14.54 dom-OptVal, dom-Pred, dom-Query, dom-RawTable, dom-Row, dom-Select, dom-TStore, % 108.03/14.54 dom-TTContext, dom-TType, dom-Table, dropFirstColRaw-0, dropFirstColRaw-2, % 108.03/14.54 evalExpRow-0, evalExpRow-1, evalExpRow-2, evalExpRow-3, evalExpRow-INV, % 108.03/14.54 filterRows-0, filterRows-1, filterRows-2, filterRows-INV, filterSingleRow-0, % 108.03/14.54 filterSingleRow-1, filterSingleRow-2, filterSingleRow-3, filterSingleRow-4, % 108.03/14.54 filterSingleRow-5, filterSingleRow-false-INV, filterSingleRow-true-INV, % 108.03/14.54 filterTable-0, filterTable-INV, findCol-0, findCol-1, findCol-2, findCol-INV, % 108.03/14.54 findColType-0, findColType-1, findColType-2, findColType-INV, getAttrL-0, % 108.03/14.54 getAttrL-INV, getFType-0, getQuery-0, getRaw-0, getRaw-INV, getRawTable-0, % 108.03/14.54 getTType-0, getTable-0, getVal-0, isSomeFType-0, isSomeFType-1, % 108.03/14.54 isSomeFType-false-INV, isSomeFType-true-INV, isSomeQuery-0, isSomeQuery-1, % 108.03/14.54 isSomeQuery-false-INV, isSomeQuery-true-INV, isSomeRawTable-0, isSomeRawTable-1, % 108.03/14.54 isSomeRawTable-false-INV, isSomeRawTable-true-INV, isSomeTType-0, isSomeTType-1, % 108.03/14.54 isSomeTType-false-INV, isSomeTType-true-INV, isSomeTable-0, isSomeTable-1, % 108.03/14.54 isSomeTable-false-INV, isSomeTable-true-INV, isSomeVal-0, isSomeVal-1, % 108.03/14.54 isSomeVal-false-INV, isSomeVal-true-INV, isValue-0, isValue-1, isValue-2, % 108.03/14.54 isValue-3, isValue-4, isValue-false-INV, isValue-true-INV, lookupContext-0, % 108.03/14.54 lookupContext-1, lookupContext-2, lookupContext-INV, lookupStore-0, % 108.03/14.54 lookupStore-1, lookupStore-2, lookupStore-INV, matchingAttrL-0, matchingAttrL-1, % 108.03/14.54 matchingAttrL-2, matchingAttrL-false-INV, matchingAttrL-true-INV, projectCols-0, % 108.03/14.54 projectCols-1, projectCols-2, projectCols-INV, projectEmptyCol-0, % 108.03/14.54 projectEmptyCol-1, projectEmptyCol-INV, projectFirstRaw-0, projectFirstRaw-1, % 108.03/14.54 projectFirstRaw-2, projectFirstRaw-INV, projectTable-0, projectTable-1, % 108.03/14.54 projectTable-2, projectTable-INV, projectType-0, projectType-1, projectType-INV, % 108.03/14.54 projectTypeAttrL-0, projectTypeAttrL-1, projectTypeAttrL-2, % 108.03/14.54 projectTypeAttrL-INV, rawDifference-0, rawDifference-1, rawDifference-2, % 108.03/14.54 rawDifference-3, rawDifference-4, rawDifference-INV, rawIntersection-0, % 108.03/14.54 rawIntersection-1, rawIntersection-2, rawIntersection-3, rawIntersection-4, % 108.03/14.54 rawIntersection-INV, rawUnion-0, rawUnion-1, rawUnion-2, rawUnion-INV, reduce-0, % 108.03/14.54 reduce-1, reduce-10, reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, % 108.03/14.54 reduce-16, reduce-17, reduce-18, reduce-2, reduce-3, reduce-4, reduce-5, % 108.03/14.54 reduce-6, reduce-7, reduce-8, reduce-9, reduce-INV, rowIn-0, rowIn-1, % 108.03/14.54 rowIn-false-INV, rowIn-true-INV, sameLength-0, sameLength-1, sameLength-2, % 108.03/14.54 sameLength-false-INV, sameLength-true-INV, storeContextConsistent-0, % 108.03/14.54 storeContextConsistent-1, storeContextConsistent-2, % 108.03/14.54 storeContextConsistent-false-INV, storeContextConsistent-true-INV, tcheckPred-0, % 108.03/14.54 tcheckPred-1, tcheckPred-2, tcheckPred-3, tcheckPred-4, tcheckPred-5, % 108.03/14.54 tcheckPred-false-INV, tcheckPred-true-INV, typeOfExp-0, typeOfExp-1, % 108.03/14.54 typeOfExp-2, typeOfExp-3, typeOfExp-INV, welltypedRawtable-0, % 108.03/14.54 welltypedRawtable-false-INV, welltypedRawtable-true-INV, welltypedRow-0, % 108.03/14.54 welltypedRow-1, welltypedRow-2, welltypedRow-false-INV, welltypedtable-0, % 108.03/14.54 welltypedtable-false-INV, welltypedtable-true-INV % 108.03/14.54 % 108.03/14.54 Those formulas are unsatisfiable: % 108.03/14.54 --------------------------------- % 108.03/14.54 % 108.03/14.54 Begin of proof % 108.03/14.54 | % 108.03/14.54 | ALPHA: (DIFF-ttempty-ttcons) implies: % 108.03/14.54 | (1) ! [v0: vName] : ! [v1: vFType] : ! [v2: vTType] : ( ~ (vttcons(v0, % 108.03/14.54 | v1, v2) = vttempty) | ~ vTType(v2) | ~ vFType(v1) | ~ % 108.03/14.54 | vName(v0)) % 108.03/14.54 | % 108.03/14.54 | ALPHA: (DIFF-rempty-rcons) implies: % 108.03/14.54 | (2) ! [v0: vVal] : ! [v1: vRow] : ( ~ (vrcons(v0, v1) = vrempty) | ~ % 108.03/14.54 | vVal(v0) | ~ vRow(v1)) % 108.03/14.54 | % 108.03/14.54 | ALPHA: (DIFF-tempty-tcons) implies: % 108.03/14.54 | (3) ! [v0: vRow] : ! [v1: vRawTable] : ( ~ (vtcons(v0, v1) = vtempty) | % 108.03/14.54 | ~ vRawTable(v1) | ~ vRow(v0)) % 108.03/14.54 | % 108.03/14.54 | ALPHA: (welltypedRow-true-INV) implies: % 108.03/14.54 | (4) ! [v0: vTType] : ! [v1: vRow] : (v0 = vttempty | ~ vTType(v0) | ~ % 108.03/14.54 | vRow(v1) | ~ vwelltypedRow(v0, v1) | ? [v2: vVal] : ? [v3: vTType] % 108.03/14.54 | : ? [v4: vFType] : ? [v5: vName] : ? [v6: vRow] : (vfieldType(v2) % 108.03/14.54 | = v4 & vrcons(v2, v6) = v1 & vttcons(v5, v4, v3) = v0 & vTType(v3) % 108.03/14.54 | & vVal(v2) & vFType(v4) & vName(v5) & vRow(v6) & vwelltypedRow(v3, % 108.03/14.54 | v6))) % 108.03/14.54 | % 108.03/14.54 | ALPHA: (welltypedRawtable-1) implies: % 108.03/14.55 | (5) ! [v0: vTType] : ! [v1: vRow] : ! [v2: vRawTable] : ! [v3: % 108.03/14.55 | vRawTable] : ( ~ (vtcons(v1, v2) = v3) | ~ vTType(v0) | ~ % 108.03/14.55 | vRawTable(v2) | ~ vRow(v1) | ~ vwelltypedRawtable(v0, v3) | % 108.03/14.55 | vwelltypedRawtable(v0, v2)) % 108.03/14.55 | (6) ! [v0: vTType] : ! [v1: vRow] : ! [v2: vRawTable] : ! [v3: % 108.03/14.55 | vRawTable] : ( ~ (vtcons(v1, v2) = v3) | ~ vTType(v0) | ~ % 108.03/14.55 | vRawTable(v2) | ~ vRow(v1) | ~ vwelltypedRawtable(v0, v3) | % 108.03/14.55 | vwelltypedRow(v0, v1)) % 108.03/14.55 | % 108.03/14.55 | ALPHA: (dropFirstColRaw-1) implies: % 108.03/14.55 | (7) ! [v0: vRawTable] : ! [v1: vRawTable] : ( ~ (vdropFirstColRaw(v0) = % 108.03/14.55 | v1) | ~ vRawTable(v0) | ? [v2: vRawTable] : ? [v3: vRawTable] : % 108.03/14.55 | (vdropFirstColRaw(v2) = v3 & vtcons(vrempty, v1) = v3 & % 108.03/14.55 | vtcons(vrempty, v0) = v2 & vRawTable(v3) & vRawTable(v2))) % 108.03/14.55 | % 108.03/14.55 | ALPHA: (dropFirstColRaw-INV) implies: % 108.03/14.55 | (8) ! [v0: vRawTable] : ! [v1: vRawTable] : (v0 = vtempty | ~ % 108.03/14.55 | (vdropFirstColRaw(v0) = v1) | ~ vRawTable(v0) | ? [v2: vVal] : ? % 108.03/14.55 | [v3: vRow] : ? [v4: vRawTable] : ? [v5: vRow] : ? [v6: vRawTable] % 108.03/14.55 | : ? [v7: vRawTable] : ? [v8: vRawTable] : ? [v9: vRawTable] : ? % 108.03/14.55 | [v10: vRawTable] : ? [v11: vRawTable] : ? [v12: vRawTable] : % 108.03/14.55 | (vVal(v2) & vRawTable(v9) & vRawTable(v4) & vRow(v3) & ((v12 = v1 & % 108.03/14.55 | v10 = v0 & vdropFirstColRaw(v9) = v11 & vtcons(vrempty, v11) = % 108.03/14.55 | v1 & vtcons(vrempty, v9) = v0 & vRawTable(v11) & vRawTable(v1)) % 108.03/14.55 | | (v8 = v1 & v6 = v0 & vdropFirstColRaw(v4) = v7 & vtcons(v5, v4) % 108.03/14.55 | = v0 & vtcons(v3, v7) = v1 & vrcons(v2, v3) = v5 & % 108.03/14.55 | vRawTable(v7) & vRawTable(v1) & vRow(v5))))) % 108.03/14.55 | % 108.03/14.55 | ALPHA: (dropFirstColRawPreservesWelltypedRaw-tcons-IH0) implies: % 108.03/14.55 | (9) ? [v0: vRawTable] : (vdropFirstColRaw(vrt2) = v0 & vRawTable(v0) & ! % 108.03/14.55 | [v1: vName] : ! [v2: vFType] : ! [v3: vTType] : ! [v4: vTType] : ( % 108.03/14.55 | ~ (vttcons(v1, v2, v3) = v4) | ~ vTType(v3) | ~ vFType(v2) | ~ % 108.03/14.55 | vName(v1) | ~ vwelltypedRawtable(v4, vrt2) | % 108.03/14.55 | vwelltypedRawtable(v3, v0))) % 108.03/14.55 | % 108.03/14.55 | ALPHA: (dropFirstColRawPreservesWelltypedRaw-tcons-rempty) implies: % 108.03/14.55 | (10) vRow(vrempty) % 108.03/14.55 | (11) vRawTable(vrt2) % 108.03/14.55 | (12) ? [v0: vRawTable] : ? [v1: vRawTable] : ? [v2: vName] : ? [v3: % 108.03/14.55 | vFType] : ? [v4: vTType] : ? [v5: vTType] : (vdropFirstColRaw(v0) % 108.03/14.55 | = v1 & vtcons(vrempty, vrt2) = v0 & vttcons(v2, v3, v4) = v5 & % 108.03/14.55 | vTType(v5) & vTType(v4) & vFType(v3) & vRawTable(v1) & vRawTable(v0) % 108.03/14.55 | & vName(v2) & vwelltypedRawtable(v5, v0) & ~ vwelltypedRawtable(v4, % 108.03/14.55 | v1)) % 108.03/14.55 | % 108.03/14.55 | ALPHA: (function-axioms) implies: % 108.03/14.55 | (13) ! [v0: vRawTable] : ! [v1: vRawTable] : ! [v2: vRawTable] : ! [v3: % 108.03/14.55 | vRow] : (v1 = v0 | ~ (vtcons(v3, v2) = v1) | ~ (vtcons(v3, v2) = % 108.03/14.55 | v0)) % 108.03/14.55 | % 108.03/14.55 | DELTA: instantiating (9) with fresh symbol all_313_0 gives: % 108.03/14.55 | (14) vdropFirstColRaw(vrt2) = all_313_0 & vRawTable(all_313_0) & ! [v0: % 108.03/14.55 | vName] : ! [v1: vFType] : ! [v2: vTType] : ! [v3: vTType] : ( ~ % 108.03/14.55 | (vttcons(v0, v1, v2) = v3) | ~ vTType(v2) | ~ vFType(v1) | ~ % 108.03/14.55 | vName(v0) | ~ vwelltypedRawtable(v3, vrt2) | vwelltypedRawtable(v2, % 108.03/14.55 | all_313_0)) % 108.03/14.55 | % 108.03/14.55 | ALPHA: (14) implies: % 108.03/14.55 | (15) vdropFirstColRaw(vrt2) = all_313_0 % 108.03/14.56 | (16) ! [v0: vName] : ! [v1: vFType] : ! [v2: vTType] : ! [v3: vTType] : % 108.03/14.56 | ( ~ (vttcons(v0, v1, v2) = v3) | ~ vTType(v2) | ~ vFType(v1) | ~ % 108.03/14.56 | vName(v0) | ~ vwelltypedRawtable(v3, vrt2) | vwelltypedRawtable(v2, % 108.03/14.56 | all_313_0)) % 108.03/14.56 | % 108.03/14.56 | DELTA: instantiating (12) with fresh symbols all_317_0, all_317_1, all_317_2, % 108.03/14.56 | all_317_3, all_317_4, all_317_5 gives: % 108.03/14.56 | (17) vdropFirstColRaw(all_317_5) = all_317_4 & vtcons(vrempty, vrt2) = % 108.03/14.56 | all_317_5 & vttcons(all_317_3, all_317_2, all_317_1) = all_317_0 & % 108.03/14.56 | vTType(all_317_0) & vTType(all_317_1) & vFType(all_317_2) & % 108.03/14.56 | vRawTable(all_317_4) & vRawTable(all_317_5) & vName(all_317_3) & % 108.03/14.56 | vwelltypedRawtable(all_317_0, all_317_5) & ~ % 108.03/14.56 | vwelltypedRawtable(all_317_1, all_317_4) % 108.03/14.56 | % 108.03/14.56 | ALPHA: (17) implies: % 108.03/14.56 | (18) vwelltypedRawtable(all_317_0, all_317_5) % 108.03/14.56 | (19) vName(all_317_3) % 108.03/14.56 | (20) vRawTable(all_317_5) % 108.03/14.56 | (21) vFType(all_317_2) % 108.03/14.56 | (22) vTType(all_317_1) % 108.03/14.56 | (23) vTType(all_317_0) % 108.03/14.56 | (24) vttcons(all_317_3, all_317_2, all_317_1) = all_317_0 % 108.03/14.56 | (25) vtcons(vrempty, vrt2) = all_317_5 % 108.03/14.56 | (26) vdropFirstColRaw(all_317_5) = all_317_4 % 108.03/14.56 | % 108.03/14.56 | GROUND_INST: instantiating (16) with all_317_3, all_317_2, all_317_1, % 108.03/14.56 | all_317_0, simplifying with (19), (21), (22), (24) gives: % 108.03/14.56 | (27) ~ vwelltypedRawtable(all_317_0, vrt2) | vwelltypedRawtable(all_317_1, % 108.03/14.56 | all_313_0) % 108.03/14.56 | % 108.03/14.56 | GROUND_INST: instantiating (1) with all_317_3, all_317_2, all_317_1, % 108.03/14.56 | simplifying with (19), (21), (22) gives: % 108.03/14.56 | (28) ~ (vttcons(all_317_3, all_317_2, all_317_1) = vttempty) % 108.03/14.56 | % 108.03/14.56 | GROUND_INST: instantiating (6) with all_317_0, vrempty, vrt2, all_317_5, % 108.03/14.56 | simplifying with (10), (11), (18), (23), (25) gives: % 108.03/14.56 | (29) vwelltypedRow(all_317_0, vrempty) % 108.03/14.56 | % 108.03/14.56 | GROUND_INST: instantiating (5) with all_317_0, vrempty, vrt2, all_317_5, % 108.03/14.56 | simplifying with (10), (11), (18), (23), (25) gives: % 108.03/14.56 | (30) vwelltypedRawtable(all_317_0, vrt2) % 108.03/14.56 | % 108.03/14.56 | GROUND_INST: instantiating (3) with vrempty, vrt2, simplifying with (10), (11) % 108.03/14.56 | gives: % 108.03/14.56 | (31) ~ (vtcons(vrempty, vrt2) = vtempty) % 108.03/14.56 | % 108.03/14.56 | GROUND_INST: instantiating (7) with vrt2, all_313_0, simplifying with (11), % 108.03/14.56 | (15) gives: % 108.03/14.56 | (32) ? [v0: vRawTable] : ? [v1: vRawTable] : (vdropFirstColRaw(v0) = v1 & % 108.03/14.56 | vtcons(vrempty, all_313_0) = v1 & vtcons(vrempty, vrt2) = v0 & % 108.03/14.56 | vRawTable(v1) & vRawTable(v0)) % 108.03/14.56 | % 108.03/14.56 | GROUND_INST: instantiating (8) with all_317_5, all_317_4, simplifying with % 108.03/14.56 | (20), (26) gives: % 108.03/14.56 | (33) all_317_5 = vtempty | ? [v0: vVal] : ? [v1: vRow] : ? [v2: % 108.03/14.56 | vRawTable] : ? [v3: vRow] : ? [v4: int] : ? [v5: vRawTable] : ? % 108.03/14.56 | [v6: int] : ? [v7: vRawTable] : ? [v8: int] : ? [v9: vRawTable] : % 108.03/14.56 | ? [v10: int] : (vVal(v0) & vRawTable(v7) & vRawTable(v2) & vRow(v1) & % 108.03/14.56 | ((v10 = all_317_4 & v8 = all_317_5 & vdropFirstColRaw(v7) = v9 & % 108.03/14.56 | vtcons(vrempty, v9) = all_317_4 & vtcons(vrempty, v7) = % 108.03/14.56 | all_317_5 & vRawTable(v9) & vRawTable(all_317_4)) | (v6 = % 108.03/14.56 | all_317_4 & v4 = all_317_5 & vdropFirstColRaw(v2) = v5 & % 108.03/14.56 | vtcons(v3, v2) = all_317_5 & vtcons(v1, v5) = all_317_4 & % 108.03/14.56 | vrcons(v0, v1) = v3 & vRawTable(v5) & vRawTable(all_317_4) & % 108.03/14.56 | vRow(v3)))) % 108.03/14.56 | % 108.03/14.56 | DELTA: instantiating (32) with fresh symbols all_352_0, all_352_1 gives: % 108.03/14.56 | (34) vdropFirstColRaw(all_352_1) = all_352_0 & vtcons(vrempty, all_313_0) = % 108.03/14.56 | all_352_0 & vtcons(vrempty, vrt2) = all_352_1 & vRawTable(all_352_0) & % 108.03/14.56 | vRawTable(all_352_1) % 108.03/14.56 | % 108.03/14.56 | ALPHA: (34) implies: % 108.03/14.56 | (35) vtcons(vrempty, vrt2) = all_352_1 % 108.03/14.56 | % 108.03/14.56 | BETA: splitting (27) gives: % 108.03/14.56 | % 108.03/14.56 | Case 1: % 108.03/14.56 | | % 108.03/14.56 | | (36) ~ vwelltypedRawtable(all_317_0, vrt2) % 108.03/14.56 | | % 108.03/14.56 | | PRED_UNIFY: (30), (36) imply: % 108.03/14.56 | | (37) $false % 108.03/14.57 | | % 108.03/14.57 | | CLOSE: (37) is inconsistent. % 108.03/14.57 | | % 108.03/14.57 | Case 2: % 108.03/14.57 | | % 108.03/14.57 | | % 108.03/14.57 | | GROUND_INST: instantiating (13) with all_317_5, all_352_1, vrt2, vrempty, % 108.03/14.57 | | simplifying with (25), (35) gives: % 108.03/14.57 | | (38) all_352_1 = all_317_5 % 108.03/14.57 | | % 108.03/14.57 | | PRED_UNIFY: (24), (28) imply: % 108.03/14.57 | | (39) ~ (all_317_0 = vttempty) % 108.03/14.57 | | % 108.03/14.57 | | PRED_UNIFY: (31), (35) imply: % 108.03/14.57 | | (40) ~ (all_352_1 = vtempty) % 108.03/14.57 | | % 108.03/14.57 | | REDUCE: (38), (40) imply: % 108.03/14.57 | | (41) ~ (all_317_5 = vtempty) % 108.03/14.57 | | % 108.03/14.57 | | BETA: splitting (33) gives: % 108.03/14.57 | | % 108.03/14.57 | | Case 1: % 108.03/14.57 | | | % 108.03/14.57 | | | (42) all_317_5 = vtempty % 108.03/14.57 | | | % 108.03/14.57 | | | REDUCE: (41), (42) imply: % 108.03/14.57 | | | (43) $false % 108.03/14.57 | | | % 108.03/14.57 | | | CLOSE: (43) is inconsistent. % 108.03/14.57 | | | % 108.03/14.57 | | Case 2: % 108.03/14.57 | | | % 108.03/14.57 | | | % 108.03/14.57 | | | GROUND_INST: instantiating (4) with all_317_0, vrempty, simplifying with % 108.03/14.57 | | | (10), (23), (29) gives: % 108.03/14.57 | | | (44) all_317_0 = vttempty | ? [v0: vVal] : ? [v1: vTType] : ? [v2: % 108.03/14.57 | | | vFType] : ? [v3: vName] : ? [v4: vRow] : (vfieldType(v0) = v2 % 108.03/14.57 | | | & vrcons(v0, v4) = vrempty & vttcons(v3, v2, v1) = all_317_0 & % 108.03/14.57 | | | vTType(v1) & vVal(v0) & vFType(v2) & vName(v3) & vRow(v4) & % 108.03/14.57 | | | vwelltypedRow(v1, v4)) % 108.03/14.57 | | | % 108.03/14.57 | | | BETA: splitting (44) gives: % 108.03/14.57 | | | % 108.03/14.57 | | | Case 1: % 108.03/14.57 | | | | % 108.03/14.57 | | | | (45) all_317_0 = vttempty % 108.03/14.57 | | | | % 108.03/14.57 | | | | REDUCE: (39), (45) imply: % 108.03/14.57 | | | | (46) $false % 108.03/14.57 | | | | % 108.03/14.57 | | | | CLOSE: (46) is inconsistent. % 108.03/14.57 | | | | % 108.03/14.57 | | | Case 2: % 108.03/14.57 | | | | % 108.03/14.57 | | | | (47) ? [v0: vVal] : ? [v1: vTType] : ? [v2: vFType] : ? [v3: % 108.03/14.57 | | | | vName] : ? [v4: vRow] : (vfieldType(v0) = v2 & vrcons(v0, v4) % 108.03/14.57 | | | | = vrempty & vttcons(v3, v2, v1) = all_317_0 & vTType(v1) & % 108.03/14.57 | | | | vVal(v0) & vFType(v2) & vName(v3) & vRow(v4) & % 108.03/14.57 | | | | vwelltypedRow(v1, v4)) % 108.03/14.57 | | | | % 108.03/14.57 | | | | DELTA: instantiating (47) with fresh symbols all_539_0, all_539_1, % 108.03/14.57 | | | | all_539_2, all_539_3, all_539_4 gives: % 108.03/14.57 | | | | (48) vfieldType(all_539_4) = all_539_2 & vrcons(all_539_4, all_539_0) % 108.03/14.57 | | | | = vrempty & vttcons(all_539_1, all_539_2, all_539_3) = all_317_0 % 108.03/14.57 | | | | & vTType(all_539_3) & vVal(all_539_4) & vFType(all_539_2) & % 108.03/14.57 | | | | vName(all_539_1) & vRow(all_539_0) & vwelltypedRow(all_539_3, % 108.03/14.57 | | | | all_539_0) % 108.03/14.57 | | | | % 108.03/14.57 | | | | ALPHA: (48) implies: % 108.03/14.57 | | | | (49) vRow(all_539_0) % 108.03/14.57 | | | | (50) vVal(all_539_4) % 108.03/14.57 | | | | (51) vrcons(all_539_4, all_539_0) = vrempty % 108.03/14.57 | | | | % 108.03/14.57 | | | | GROUND_INST: instantiating (2) with all_539_4, all_539_0, simplifying % 108.03/14.57 | | | | with (49), (50), (51) gives: % 108.03/14.57 | | | | (52) $false % 108.03/14.57 | | | | % 108.03/14.57 | | | | CLOSE: (52) is inconsistent. % 108.03/14.57 | | | | % 108.03/14.57 | | | End of split % 108.03/14.57 | | | % 108.03/14.57 | | End of split % 108.03/14.57 | | % 108.03/14.57 | End of split % 108.03/14.57 | % 108.03/14.57 End of proof % 108.03/14.57 % SZS output end Proof for theBenchmark % 108.03/14.57 % 108.03/14.57 13944ms %------------------------------------------------------------------------------