%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM132+2 : TPTP v8.1.2. Released v6.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n028.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 : Wed Aug 30 18:44:33 EDT 2023 % Result : Theorem 83.37s 11.56s % Output : Proof 83.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM132+2 : TPTP v8.1.2. Released v6.4.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Aug 29 13:38:10 EDT 2023 % 0.19/0.34 % CPUTime : % 0.54/0.62 ________ _____ % 0.54/0.62 ___ __ \_________(_)________________________________ % 0.54/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.54/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.54/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.54/0.62 % 0.54/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.54/0.62 (2023-06-19) % 0.54/0.62 % 0.54/0.62 (c) Philipp Rümmer, 2009-2023 % 0.54/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.54/0.62 Amanda Stjerna. % 0.54/0.62 Free software under BSD-3-Clause. % 0.54/0.62 % 0.54/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.54/0.62 % 0.54/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.54/0.64 Running up to 7 provers in parallel. % 0.54/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.54/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.54/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.54/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.54/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.54/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.54/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.82/1.37 Prover 1: Preprocessing ... % 3.82/1.37 Prover 4: Preprocessing ... % 3.82/1.41 Prover 5: Preprocessing ... % 3.82/1.41 Prover 3: Preprocessing ... % 3.82/1.41 Prover 2: Preprocessing ... % 3.82/1.41 Prover 0: Preprocessing ... % 4.81/1.41 Prover 6: Preprocessing ... % 10.34/2.17 Prover 1: Constructing countermodel ... % 10.60/2.20 Prover 6: Constructing countermodel ... % 10.60/2.20 Prover 3: Constructing countermodel ... % 10.90/2.23 Prover 4: Constructing countermodel ... % 10.90/2.23 Prover 5: Proving ... % 10.92/2.24 Prover 0: Proving ... % 11.42/2.31 Prover 2: Proving ... % 73.75/10.33 Prover 2: stopped % 73.75/10.35 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 73.75/10.44 Prover 7: Preprocessing ... % 75.81/10.60 Prover 7: Warning: ignoring some quantifiers % 75.81/10.61 Prover 7: Constructing countermodel ... % 82.83/11.55 Prover 7: Found proof (size 153) % 83.37/11.55 Prover 7: proved (1204ms) % 83.37/11.55 Prover 6: stopped % 83.37/11.55 Prover 3: stopped % 83.37/11.56 Prover 1: stopped % 83.37/11.56 Prover 0: stopped % 83.37/11.56 Prover 4: stopped % 83.37/11.56 Prover 5: stopped % 83.37/11.56 % 83.37/11.56 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 83.37/11.56 % 83.45/11.57 % SZS output start Proof for theBenchmark % 83.45/11.57 Assumptions after simplification: % 83.45/11.57 --------------------------------- % 83.45/11.57 % 83.45/11.57 (EQ-abs) % 83.45/11.60 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 83.45/11.60 $i] : ! [v6: $i] : (v5 = v2 | ~ (vabs(v3, v4, v5) = v6) | ~ (vabs(v0, v1, % 83.45/11.60 v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 83.45/11.60 ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 83.45/11.60 $i] : ! [v5: $i] : ! [v6: $i] : (v4 = v1 | ~ (vabs(v3, v4, v5) = v6) | ~ % 83.45/11.61 (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 83.45/11.61 $i(v1) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 83.45/11.61 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v3 = v0 | ~ (vabs(v3, v4, v5) = % 83.45/11.61 v6) | ~ (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 83.45/11.61 $i(v2) | ~ $i(v1) | ~ $i(v0)) % 83.45/11.61 % 83.45/11.61 (T-Strong) % 83.45/11.61 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 83.45/11.61 $i] : ( ~ (vbind(v0, v1, v2) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 83.45/11.61 $i(v1) | ~ $i(v0) | ~ vtcheck(v5, v3, v4) | vtcheck(v2, v3, v4) | % 83.45/11.61 visFreeVar(v0, v3)) % 83.45/11.61 % 83.45/11.61 (T-subst-abs-2-gen) % 83.66/11.61 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 83.66/11.61 $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : % 83.66/11.61 (v4 = v2 | ~ (vsubst(v2, v3, v9) = v10) | ~ (vbind(v2, v0, v1) = v8) | ~ % 83.66/11.61 (vabs(v4, v5, v6) = v9) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 83.66/11.61 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ vtcheck(v8, v9, v7) | ~ % 83.66/11.61 vtcheck(v1, v3, v0) | vtcheck(v1, v10, v7) | visFreeVar(v4, v3)) % 83.66/11.61 % 83.66/11.61 (T-subst-abs-3) % 83.66/11.61 $i(veabs) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: % 83.66/11.61 $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 83.66/11.61 ( ~ (v4 = v2) & vsubst(v2, v3, v8) = v9 & vbind(v2, v0, v1) = v7 & vabs(v4, % 83.66/11.62 v5, veabs) = v8 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 83.66/11.62 $i(v3) & $i(v2) & $i(v1) & $i(v0) & vtcheck(v7, v8, v6) & vtcheck(v1, v3, % 83.66/11.62 v0) & visFreeVar(v4, v3) & ~ vtcheck(v1, v9, v6)) % 83.66/11.62 % 83.66/11.62 (alpha-equiv-subst-abs) % 83.66/11.62 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 83.66/11.62 $i] : ! [v6: $i] : ( ~ (vsubst(v1, v4, v3) = v5) | ~ (vabs(v2, v0, v5) = % 83.66/11.62 v6) | ~ (vvar(v2) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 83.66/11.62 visFreeVar(v2, v3) | ? [v7: $i] : (vabs(v1, v0, v3) = v7 & $i(v7) & % 83.66/11.62 valphaEquivalent(v7, v6))) % 83.66/11.62 % 83.66/11.62 (alpha-equiv-typing) % 83.66/11.62 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 83.66/11.62 | ~ $i(v1) | ~ $i(v0) | ~ valphaEquivalent(v0, v2) | ~ vtcheck(v1, v0, % 83.66/11.62 v3) | vtcheck(v1, v2, v3)) % 83.66/11.62 % 83.66/11.62 (fresh-free-2) % 83.66/11.62 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 83.66/11.62 $i] : ! [v6: $i] : ( ~ (vgensym(v6) = v2) | ~ (vapp(v4, v5) = v6) | ~ % 83.66/11.62 (vapp(v0, v3) = v4) | ~ (vvar(v1) = v5) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 83.66/11.62 | ~ $i(v0) | ~ visFreeVar(v2, v3)) % 83.66/11.62 % 83.66/11.62 (fresh-unequal-var-3) % 83.66/11.62 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 83.66/11.62 $i] : ( ~ (vgensym(v5) = v2) | ~ (vapp(v3, v4) = v5) | ~ (vapp(v0, v1) = % 83.66/11.62 v3) | ~ (vvar(v2) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) % 83.66/11.62 % 83.66/11.62 (gensym-is-fresh) % 83.66/11.62 ! [v0: $i] : ! [v1: $i] : ( ~ (vgensym(v1) = v0) | ~ $i(v1) | ~ $i(v0) | % 83.66/11.62 ~ visFreeVar(v0, v1)) % 83.66/11.62 % 83.66/11.62 (isFreeVar1) % 83.66/11.63 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = v1 % 83.66/11.63 | ~ (vabs(v3, v0, v4) = v2) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 83.66/11.63 | ~ $i(v0) | ~ visFreeVar(v1, v4) | visFreeVar(v1, v2)) & ! [v0: $i] : ! % 83.66/11.63 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (vabs(v3, v0, v4) = % 83.66/11.63 v2) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 83.66/11.63 visFreeVar(v1, v2) | visFreeVar(v1, v4)) & ! [v0: $i] : ! [v1: $i] : ! % 83.66/11.63 [v2: $i] : ! [v3: $i] : ( ~ (vabs(v1, v0, v3) = v2) | ~ $i(v3) | ~ $i(v2) | % 83.66/11.63 ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v1, v2)) % 83.66/11.63 % 83.66/11.63 (isFreeVar2) % 83.66/11.63 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, v3) = % 83.66/11.63 v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v0, % 83.66/11.63 v3) | visFreeVar(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 83.66/11.63 [v3: $i] : ( ~ (vapp(v2, v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 83.66/11.63 $i(v0) | ~ visFreeVar(v0, v2) | visFreeVar(v0, v1)) & ! [v0: $i] : ! [v1: % 83.66/11.63 $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, v3) = v1) | ~ $i(v3) | ~ % 83.66/11.63 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v0, v1) | visFreeVar(v0, v3) % 83.66/11.63 | visFreeVar(v0, v2)) % 83.66/11.63 % 83.66/11.63 (isValue0) % 83.66/11.63 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vabs(v0, v1, v2) % 83.66/11.63 = v3) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | visValue(v3)) % 83.66/11.63 % 83.66/11.63 (isValue1) % 83.66/11.63 ! [v0: $i] : ! [v1: $i] : ( ~ (vvar(v0) = v1) | ~ $i(v1) | ~ $i(v0) | ~ % 83.66/11.63 visValue(v1)) % 83.66/11.63 % 83.66/11.63 (isValue2) % 83.66/11.63 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (vapp(v0, v1) = v2) | ~ $i(v2) % 83.66/11.63 | ~ $i(v1) | ~ $i(v0) | ~ visValue(v2)) % 83.66/11.63 % 83.66/11.63 (subst-INV) % 83.66/11.64 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vsubst(v0, v1, % 83.66/11.64 v2) = v3) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] % 83.66/11.64 : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 83.66/11.64 [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? % 83.66/11.64 [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : ? [v19: $i] : ? % 83.66/11.64 [v20: $i] : ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? % 83.66/11.64 [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? [v28: $i] : ? [v29: $i] : ? % 83.66/11.64 [v30: $i] : ? [v31: $i] : ? [v32: $i] : ? [v33: $i] : ? [v34: $i] : ? % 83.66/11.64 [v35: $i] : ? [v36: $i] : ? [v37: $i] : ? [v38: $i] : ? [v39: $i] : ? % 83.66/11.64 [v40: $i] : ? [v41: $i] : ? [v42: $i] : ? [v43: $i] : ? [v44: $i] : ? % 83.66/11.64 [v45: $i] : ? [v46: $i] : ? [v47: $i] : ? [v48: $i] : ($i(v47) & $i(v46) % 83.66/11.64 & $i(v45) & $i(v43) & $i(v42) & $i(v41) & $i(v36) & $i(v35) & $i(v34) & % 83.66/11.64 $i(v33) & $i(v31) & $i(v30) & $i(v29) & $i(v28) & $i(v27) & $i(v17) & % 83.66/11.64 $i(v16) & $i(v15) & $i(v14) & $i(v13) & $i(v12) & $i(v8) & $i(v7) & $i(v6) % 83.66/11.64 & $i(v5) & $i(v4) & ((v48 = v2 & v47 = v1 & v46 = v0 & v45 = v0 & v3 = v1 % 83.66/11.64 & vvar(v0) = v2) | (v44 = v2 & v42 = v0 & v41 = v1 & v3 = v2 & ~ (v43 % 83.66/11.64 = v0) & vvar(v43) = v2) | (v40 = v3 & v37 = v2 & v35 = v1 & v34 = v0 % 83.66/11.64 & vsubst(v0, v1, v36) = v39 & vsubst(v0, v1, v33) = v38 & vapp(v38, % 83.66/11.64 v39) = v3 & vapp(v33, v36) = v2 & $i(v39) & $i(v38)) | (v32 = v2 & % 83.66/11.64 v29 = v0 & v28 = v0 & v27 = v1 & v3 = v2 & vabs(v0, v30, v31) = v2) | % 83.66/11.64 (v26 = v3 & v22 = v16 & v18 = v2 & v13 = v1 & v12 = v0 & ~ (v15 = v0) & % 83.66/11.64 vsubst(v15, v23, v17) = v24 & vsubst(v0, v1, v25) = v3 & vgensym(v21) % 83.66/11.64 = v16 & vapp(v19, v20) = v21 & vapp(v1, v17) = v19 & vabs(v16, v14, % 83.66/11.64 v24) = v25 & vabs(v15, v14, v17) = v2 & vvar(v16) = v23 & vvar(v0) = % 83.66/11.64 v20 & $i(v25) & $i(v24) & $i(v23) & $i(v21) & $i(v20) & $i(v19) & % 83.66/11.64 visFreeVar(v15, v1)) | (v11 = v3 & v9 = v2 & v7 = v1 & v6 = v0 & ~ % 83.66/11.64 (v4 = v0) & vsubst(v0, v1, v8) = v10 & vabs(v4, v5, v10) = v3 & % 83.66/11.64 vabs(v4, v5, v8) = v2 & $i(v10) & ~ visFreeVar(v4, v1))))) % 83.66/11.64 % 83.66/11.64 (function-axioms) % 83.66/11.64 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 83.66/11.64 | ~ (vsubst(v4, v3, v2) = v1) | ~ (vsubst(v4, v3, v2) = v0)) & ! [v0: $i] % 83.66/11.64 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 83.66/11.64 (vbind(v4, v3, v2) = v1) | ~ (vbind(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 83.66/11.64 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (vabs(v4, % 83.66/11.64 v3, v2) = v1) | ~ (vabs(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 83.66/11.64 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (varrow(v3, v2) = v1) | ~ % 83.66/11.64 (varrow(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 83.66/11.64 $i] : (v1 = v0 | ~ (vlookup(v3, v2) = v1) | ~ (vlookup(v3, v2) = v0)) & ! % 83.66/11.64 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (vapp(v3, % 83.66/11.64 v2) = v1) | ~ (vapp(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 83.66/11.64 [v2: $i] : (v1 = v0 | ~ (vgensym(v2) = v1) | ~ (vgensym(v2) = v0)) & ! [v0: % 83.66/11.64 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (vgetSomeType(v2) = v1) | ~ % 83.66/11.64 (vgetSomeType(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 83.66/11.64 v0 | ~ (vsomeType(v2) = v1) | ~ (vsomeType(v2) = v0)) & ! [v0: $i] : ! % 83.66/11.64 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (vvar(v2) = v1) | ~ (vvar(v2) = v0)) % 83.66/11.64 % 83.66/11.64 Further assumptions not needed in the proof: % 83.66/11.64 -------------------------------------------- % 83.66/11.64 DIFF-abs-app, DIFF-empty-bind, DIFF-noType-someType, DIFF-var-abs, DIFF-var-app, % 83.66/11.64 EQ-app, EQ-arrow, EQ-bind, EQ-empty, EQ-noType, EQ-someType, EQ-var, % 83.66/11.64 T-Context-Duplicate, T-Context-Swap, T-Weak, T-Weak-FreeVar, T-abs, T-app, % 83.66/11.64 T-inv, T-var, alpha-equiv-FreeVar, alpha-equiv-refl, alpha-equiv-sym, % 83.66/11.64 alpha-equiv-trans, getSomeType0, isFreeVar0, isSomeType0, isSomeType1, % 83.66/11.64 lookup-INV, lookup0, lookup1, lookup2, subst0, subst1, subst2, subst3, subst4, % 83.66/11.64 subst5 % 83.66/11.64 % 83.66/11.64 Those formulas are unsatisfiable: % 83.66/11.64 --------------------------------- % 83.66/11.64 % 83.66/11.64 Begin of proof % 83.66/11.65 | % 83.66/11.65 | ALPHA: (EQ-abs) implies: % 83.66/11.65 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 83.66/11.65 | ! [v5: $i] : ! [v6: $i] : (v3 = v0 | ~ (vabs(v3, v4, v5) = v6) | ~ % 83.66/11.65 | (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 83.66/11.65 | $i(v2) | ~ $i(v1) | ~ $i(v0)) % 83.66/11.65 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 83.66/11.65 | ! [v5: $i] : ! [v6: $i] : (v4 = v1 | ~ (vabs(v3, v4, v5) = v6) | ~ % 83.66/11.65 | (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 83.66/11.65 | $i(v2) | ~ $i(v1) | ~ $i(v0)) % 83.66/11.65 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 83.66/11.65 | ! [v5: $i] : ! [v6: $i] : (v5 = v2 | ~ (vabs(v3, v4, v5) = v6) | ~ % 83.66/11.65 | (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 83.66/11.65 | $i(v2) | ~ $i(v1) | ~ $i(v0)) % 83.66/11.65 | % 83.66/11.65 | ALPHA: (isFreeVar1) implies: % 83.66/11.65 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vabs(v1, % 83.66/11.65 | v0, v3) = v2) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 83.66/11.65 | ~ visFreeVar(v1, v2)) % 83.66/11.65 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 83.66/11.65 | ~ (vabs(v3, v0, v4) = v2) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 83.66/11.65 | $i(v1) | ~ $i(v0) | ~ visFreeVar(v1, v2) | visFreeVar(v1, v4)) % 83.66/11.65 | % 83.66/11.65 | ALPHA: (isFreeVar2) implies: % 83.66/11.65 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, % 83.66/11.65 | v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 83.66/11.65 | visFreeVar(v0, v2) | visFreeVar(v0, v1)) % 83.66/11.65 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, % 83.66/11.65 | v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 83.66/11.65 | visFreeVar(v0, v3) | visFreeVar(v0, v1)) % 83.66/11.65 | % 83.66/11.65 | ALPHA: (T-subst-abs-3) implies: % 83.66/11.65 | (8) $i(veabs) % 83.66/11.65 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 83.66/11.65 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ( % 83.66/11.65 | ~ (v4 = v2) & vsubst(v2, v3, v8) = v9 & vbind(v2, v0, v1) = v7 & % 83.66/11.65 | vabs(v4, v5, veabs) = v8 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) % 83.66/11.65 | & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & vtcheck(v7, v8, v6) & % 83.66/11.65 | vtcheck(v1, v3, v0) & visFreeVar(v4, v3) & ~ vtcheck(v1, v9, v6)) % 83.66/11.65 | % 83.66/11.65 | ALPHA: (function-axioms) implies: % 83.66/11.65 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 83.66/11.65 | (v1 = v0 | ~ (vabs(v4, v3, v2) = v1) | ~ (vabs(v4, v3, v2) = v0)) % 83.66/11.65 | % 83.66/11.66 | DELTA: instantiating (9) with fresh symbols all_55_0, all_55_1, all_55_2, % 83.66/11.66 | all_55_3, all_55_4, all_55_5, all_55_6, all_55_7, all_55_8, all_55_9 % 83.66/11.66 | gives: % 83.66/11.66 | (11) ~ (all_55_5 = all_55_7) & vsubst(all_55_7, all_55_6, all_55_1) = % 83.66/11.66 | all_55_0 & vbind(all_55_7, all_55_9, all_55_8) = all_55_2 & % 83.66/11.66 | vabs(all_55_5, all_55_4, veabs) = all_55_1 & $i(all_55_0) & % 83.66/11.66 | $i(all_55_1) & $i(all_55_2) & $i(all_55_3) & $i(all_55_4) & % 83.66/11.66 | $i(all_55_5) & $i(all_55_6) & $i(all_55_7) & $i(all_55_8) & % 83.66/11.66 | $i(all_55_9) & vtcheck(all_55_2, all_55_1, all_55_3) & % 83.66/11.66 | vtcheck(all_55_8, all_55_6, all_55_9) & visFreeVar(all_55_5, all_55_6) % 83.66/11.66 | & ~ vtcheck(all_55_8, all_55_0, all_55_3) % 83.66/11.66 | % 83.66/11.66 | ALPHA: (11) implies: % 83.66/11.66 | (12) ~ (all_55_5 = all_55_7) % 83.66/11.66 | (13) ~ vtcheck(all_55_8, all_55_0, all_55_3) % 83.66/11.66 | (14) vtcheck(all_55_8, all_55_6, all_55_9) % 83.66/11.66 | (15) vtcheck(all_55_2, all_55_1, all_55_3) % 83.66/11.66 | (16) $i(all_55_9) % 83.66/11.66 | (17) $i(all_55_8) % 83.66/11.66 | (18) $i(all_55_7) % 83.66/11.66 | (19) $i(all_55_6) % 83.66/11.66 | (20) $i(all_55_5) % 83.66/11.66 | (21) $i(all_55_4) % 83.66/11.66 | (22) $i(all_55_3) % 83.66/11.66 | (23) $i(all_55_2) % 83.66/11.66 | (24) $i(all_55_1) % 83.66/11.66 | (25) $i(all_55_0) % 83.66/11.66 | (26) vabs(all_55_5, all_55_4, veabs) = all_55_1 % 83.66/11.66 | (27) vbind(all_55_7, all_55_9, all_55_8) = all_55_2 % 83.66/11.66 | (28) vsubst(all_55_7, all_55_6, all_55_1) = all_55_0 % 83.66/11.66 | % 83.66/11.66 | GROUND_INST: instantiating (isValue0) with all_55_5, all_55_4, veabs, % 83.66/11.66 | all_55_1, simplifying with (8), (20), (21), (24), (26) gives: % 83.66/11.66 | (29) visValue(all_55_1) % 83.66/11.66 | % 83.66/11.66 | GROUND_INST: instantiating (T-Strong) with all_55_7, all_55_9, all_55_8, % 83.66/11.66 | all_55_1, all_55_3, all_55_2, simplifying with (15), (16), (17), % 83.66/11.66 | (18), (22), (24), (27) gives: % 83.66/11.66 | (30) vtcheck(all_55_8, all_55_1, all_55_3) | visFreeVar(all_55_7, all_55_1) % 83.66/11.66 | % 83.66/11.66 | GROUND_INST: instantiating (subst-INV) with all_55_7, all_55_6, all_55_1, % 83.66/11.66 | all_55_0, simplifying with (18), (19), (24), (25), (28) gives: % 83.66/11.66 | (31) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 83.66/11.66 | ? [v5: int] : ? [v6: $i] : ? [v7: int] : ? [v8: $i] : ? [v9: $i] : % 83.66/11.67 | ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: % 83.66/11.67 | int] : ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : % 83.66/11.67 | ? [v19: $i] : ? [v20: $i] : ? [v21: $i] : ? [v22: int] : ? [v23: % 83.66/11.67 | $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? % 83.66/11.67 | [v28: int] : ? [v29: $i] : ? [v30: $i] : ? [v31: $i] : ? [v32: $i] % 83.66/11.67 | : ? [v33: int] : ? [v34: $i] : ? [v35: $i] : ? [v36: int] : ? % 83.66/11.67 | [v37: $i] : ? [v38: $i] : ? [v39: $i] : ? [v40: int] : ? [v41: $i] % 83.66/11.67 | : ? [v42: $i] : ? [v43: $i] : ? [v44: int] : ($i(v43) & $i(v42) & % 83.66/11.67 | $i(v41) & $i(v39) & $i(v38) & $i(v37) & $i(v32) & $i(v31) & $i(v30) % 83.66/11.67 | & $i(v29) & $i(v27) & $i(v26) & $i(v25) & $i(v24) & $i(v23) & % 83.66/11.67 | $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v4) & % 83.66/11.67 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & ((v44 = all_55_1 & v43 = % 83.66/11.67 | all_55_6 & v42 = all_55_7 & v41 = all_55_7 & all_55_0 = all_55_6 % 83.66/11.67 | & vvar(all_55_7) = all_55_1) | (v40 = all_55_1 & v38 = all_55_7 % 83.66/11.67 | & v37 = all_55_6 & all_55_0 = all_55_1 & ~ (v39 = all_55_7) & % 83.66/11.67 | vvar(v39) = all_55_1) | (v36 = all_55_0 & v33 = all_55_1 & v31 = % 83.66/11.67 | all_55_6 & v30 = all_55_7 & vsubst(all_55_7, all_55_6, v32) = % 83.66/11.67 | v35 & vsubst(all_55_7, all_55_6, v29) = v34 & vapp(v34, v35) = % 83.66/11.67 | all_55_0 & vapp(v29, v32) = all_55_1 & $i(v35) & $i(v34)) | (v28 % 83.66/11.67 | = all_55_1 & v25 = all_55_7 & v24 = all_55_7 & v23 = all_55_6 & % 83.66/11.67 | all_55_0 = all_55_1 & vabs(all_55_7, v26, v27) = all_55_1) | % 83.66/11.67 | (v22 = all_55_0 & v18 = v12 & v14 = all_55_1 & v9 = all_55_6 & v8 % 83.66/11.67 | = all_55_7 & ~ (v11 = all_55_7) & vsubst(v11, v19, v13) = v20 & % 83.66/11.67 | vsubst(all_55_7, all_55_6, v21) = all_55_0 & vgensym(v17) = v12 % 83.66/11.67 | & vapp(v15, v16) = v17 & vapp(all_55_6, v13) = v15 & vabs(v12, % 83.66/11.67 | v10, v20) = v21 & vabs(v11, v10, v13) = all_55_1 & vvar(v12) = % 83.66/11.67 | v19 & vvar(all_55_7) = v16 & $i(v21) & $i(v20) & $i(v19) & % 83.66/11.67 | $i(v17) & $i(v16) & $i(v15) & visFreeVar(v11, all_55_6)) | (v7 = % 83.66/11.67 | all_55_0 & v5 = all_55_1 & v3 = all_55_6 & v2 = all_55_7 & ~ % 83.66/11.67 | (v0 = all_55_7) & vsubst(all_55_7, all_55_6, v4) = v6 & vabs(v0, % 83.66/11.67 | v1, v6) = all_55_0 & vabs(v0, v1, v4) = all_55_1 & $i(v6) & ~ % 83.66/11.67 | visFreeVar(v0, all_55_6)))) % 83.66/11.67 | % 83.66/11.67 | DELTA: instantiating (31) with fresh symbols all_63_0, all_63_1, all_63_2, % 83.66/11.67 | all_63_3, all_63_4, all_63_5, all_63_6, all_63_7, all_63_8, all_63_9, % 83.66/11.67 | all_63_10, all_63_11, all_63_12, all_63_13, all_63_14, all_63_15, % 83.66/11.67 | all_63_16, all_63_17, all_63_18, all_63_19, all_63_20, all_63_21, % 83.66/11.67 | all_63_22, all_63_23, all_63_24, all_63_25, all_63_26, all_63_27, % 83.66/11.67 | all_63_28, all_63_29, all_63_30, all_63_31, all_63_32, all_63_33, % 83.66/11.67 | all_63_34, all_63_35, all_63_36, all_63_37, all_63_38, all_63_39, % 83.66/11.67 | all_63_40, all_63_41, all_63_42, all_63_43, all_63_44 gives: % 83.66/11.67 | (32) $i(all_63_1) & $i(all_63_2) & $i(all_63_3) & $i(all_63_5) & % 83.66/11.67 | $i(all_63_6) & $i(all_63_7) & $i(all_63_12) & $i(all_63_13) & % 83.66/11.67 | $i(all_63_14) & $i(all_63_15) & $i(all_63_17) & $i(all_63_18) & % 83.66/11.67 | $i(all_63_19) & $i(all_63_20) & $i(all_63_21) & $i(all_63_31) & % 83.66/11.67 | $i(all_63_32) & $i(all_63_33) & $i(all_63_34) & $i(all_63_35) & % 83.66/11.67 | $i(all_63_36) & $i(all_63_40) & $i(all_63_41) & $i(all_63_42) & % 83.66/11.67 | $i(all_63_43) & $i(all_63_44) & ((all_63_0 = all_55_1 & all_63_1 = % 83.66/11.67 | all_55_6 & all_63_2 = all_55_7 & all_63_3 = all_55_7 & all_55_0 = % 83.66/11.67 | all_55_6 & vvar(all_55_7) = all_55_1) | (all_63_4 = all_55_1 & % 83.66/11.67 | all_63_6 = all_55_7 & all_63_7 = all_55_6 & all_55_0 = all_55_1 & % 83.66/11.67 | ~ (all_63_5 = all_55_7) & vvar(all_63_5) = all_55_1) | (all_63_8 = % 83.66/11.67 | all_55_0 & all_63_11 = all_55_1 & all_63_13 = all_55_6 & all_63_14 % 83.66/11.67 | = all_55_7 & vsubst(all_55_7, all_55_6, all_63_12) = all_63_9 & % 83.66/11.67 | vsubst(all_55_7, all_55_6, all_63_15) = all_63_10 & % 83.66/11.67 | vapp(all_63_10, all_63_9) = all_55_0 & vapp(all_63_15, all_63_12) % 83.66/11.67 | = all_55_1 & $i(all_63_9) & $i(all_63_10)) | (all_63_16 = all_55_1 % 83.66/11.67 | & all_63_19 = all_55_7 & all_63_20 = all_55_7 & all_63_21 = % 83.66/11.67 | all_55_6 & all_55_0 = all_55_1 & vabs(all_55_7, all_63_18, % 83.66/11.67 | all_63_17) = all_55_1) | (all_63_22 = all_55_0 & all_63_26 = % 83.66/11.67 | all_63_32 & all_63_30 = all_55_1 & all_63_35 = all_55_6 & % 83.66/11.67 | all_63_36 = all_55_7 & ~ (all_63_33 = all_55_7) & % 83.66/11.67 | vsubst(all_63_33, all_63_25, all_63_31) = all_63_24 & % 83.66/11.67 | vsubst(all_55_7, all_55_6, all_63_23) = all_55_0 & % 83.66/11.67 | vgensym(all_63_27) = all_63_32 & vapp(all_63_29, all_63_28) = % 83.66/11.67 | all_63_27 & vapp(all_55_6, all_63_31) = all_63_29 & % 83.66/11.67 | vabs(all_63_32, all_63_34, all_63_24) = all_63_23 & % 83.66/11.67 | vabs(all_63_33, all_63_34, all_63_31) = all_55_1 & vvar(all_63_32) % 83.66/11.67 | = all_63_25 & vvar(all_55_7) = all_63_28 & $i(all_63_23) & % 83.66/11.67 | $i(all_63_24) & $i(all_63_25) & $i(all_63_27) & $i(all_63_28) & % 83.66/11.67 | $i(all_63_29) & visFreeVar(all_63_33, all_55_6)) | (all_63_37 = % 83.66/11.67 | all_55_0 & all_63_39 = all_55_1 & all_63_41 = all_55_6 & all_63_42 % 83.66/11.67 | = all_55_7 & ~ (all_63_44 = all_55_7) & vsubst(all_55_7, % 83.66/11.67 | all_55_6, all_63_40) = all_63_38 & vabs(all_63_44, all_63_43, % 83.66/11.67 | all_63_38) = all_55_0 & vabs(all_63_44, all_63_43, all_63_40) = % 83.66/11.67 | all_55_1 & $i(all_63_38) & ~ visFreeVar(all_63_44, all_55_6))) % 83.66/11.67 | % 83.66/11.67 | ALPHA: (32) implies: % 83.66/11.67 | (33) $i(all_63_44) % 83.66/11.67 | (34) $i(all_63_43) % 83.66/11.67 | (35) $i(all_63_42) % 83.66/11.67 | (36) $i(all_63_41) % 83.66/11.67 | (37) $i(all_63_40) % 83.66/11.67 | (38) $i(all_63_36) % 83.66/11.67 | (39) $i(all_63_35) % 83.66/11.67 | (40) $i(all_63_34) % 83.66/11.67 | (41) $i(all_63_33) % 83.66/11.67 | (42) $i(all_63_32) % 83.66/11.67 | (43) $i(all_63_31) % 83.66/11.67 | (44) $i(all_63_20) % 83.66/11.67 | (45) $i(all_63_18) % 83.66/11.67 | (46) $i(all_63_17) % 83.66/11.67 | (47) $i(all_63_15) % 83.66/11.67 | (48) $i(all_63_12) % 83.66/11.67 | (49) $i(all_63_5) % 83.66/11.67 | (50) $i(all_63_3) % 83.66/11.67 | (51) (all_63_0 = all_55_1 & all_63_1 = all_55_6 & all_63_2 = all_55_7 & % 83.66/11.67 | all_63_3 = all_55_7 & all_55_0 = all_55_6 & vvar(all_55_7) = % 83.66/11.67 | all_55_1) | (all_63_4 = all_55_1 & all_63_6 = all_55_7 & all_63_7 = % 83.66/11.67 | all_55_6 & all_55_0 = all_55_1 & ~ (all_63_5 = all_55_7) & % 83.66/11.67 | vvar(all_63_5) = all_55_1) | (all_63_8 = all_55_0 & all_63_11 = % 83.66/11.67 | all_55_1 & all_63_13 = all_55_6 & all_63_14 = all_55_7 & % 83.66/11.67 | vsubst(all_55_7, all_55_6, all_63_12) = all_63_9 & vsubst(all_55_7, % 83.66/11.67 | all_55_6, all_63_15) = all_63_10 & vapp(all_63_10, all_63_9) = % 83.66/11.67 | all_55_0 & vapp(all_63_15, all_63_12) = all_55_1 & $i(all_63_9) & % 83.66/11.67 | $i(all_63_10)) | (all_63_16 = all_55_1 & all_63_19 = all_55_7 & % 83.66/11.68 | all_63_20 = all_55_7 & all_63_21 = all_55_6 & all_55_0 = all_55_1 & % 83.66/11.68 | vabs(all_55_7, all_63_18, all_63_17) = all_55_1) | (all_63_22 = % 83.66/11.68 | all_55_0 & all_63_26 = all_63_32 & all_63_30 = all_55_1 & all_63_35 % 83.66/11.68 | = all_55_6 & all_63_36 = all_55_7 & ~ (all_63_33 = all_55_7) & % 83.66/11.68 | vsubst(all_63_33, all_63_25, all_63_31) = all_63_24 & % 83.66/11.68 | vsubst(all_55_7, all_55_6, all_63_23) = all_55_0 & % 83.66/11.68 | vgensym(all_63_27) = all_63_32 & vapp(all_63_29, all_63_28) = % 83.66/11.68 | all_63_27 & vapp(all_55_6, all_63_31) = all_63_29 & vabs(all_63_32, % 83.66/11.68 | all_63_34, all_63_24) = all_63_23 & vabs(all_63_33, all_63_34, % 83.66/11.68 | all_63_31) = all_55_1 & vvar(all_63_32) = all_63_25 & % 83.66/11.68 | vvar(all_55_7) = all_63_28 & $i(all_63_23) & $i(all_63_24) & % 83.66/11.68 | $i(all_63_25) & $i(all_63_27) & $i(all_63_28) & $i(all_63_29) & % 83.66/11.68 | visFreeVar(all_63_33, all_55_6)) | (all_63_37 = all_55_0 & all_63_39 % 83.66/11.68 | = all_55_1 & all_63_41 = all_55_6 & all_63_42 = all_55_7 & ~ % 83.66/11.68 | (all_63_44 = all_55_7) & vsubst(all_55_7, all_55_6, all_63_40) = % 83.66/11.68 | all_63_38 & vabs(all_63_44, all_63_43, all_63_38) = all_55_0 & % 83.66/11.68 | vabs(all_63_44, all_63_43, all_63_40) = all_55_1 & $i(all_63_38) & % 83.66/11.68 | ~ visFreeVar(all_63_44, all_55_6)) % 83.66/11.68 | % 83.66/11.68 | BETA: splitting (30) gives: % 83.66/11.68 | % 83.66/11.68 | Case 1: % 83.66/11.68 | | % 83.66/11.68 | | (52) vtcheck(all_55_8, all_55_1, all_55_3) % 83.66/11.68 | | % 83.66/11.68 | | PRED_UNIFY: (13), (52) imply: % 83.66/11.68 | | (53) ~ (all_55_0 = all_55_1) % 83.66/11.68 | | % 83.66/11.68 | | BETA: splitting (51) gives: % 83.66/11.68 | | % 83.66/11.68 | | Case 1: % 83.66/11.68 | | | % 83.66/11.68 | | | (54) (all_63_0 = all_55_1 & all_63_1 = all_55_6 & all_63_2 = all_55_7 & % 83.66/11.68 | | | all_63_3 = all_55_7 & all_55_0 = all_55_6 & vvar(all_55_7) = % 83.66/11.68 | | | all_55_1) | (all_63_4 = all_55_1 & all_63_6 = all_55_7 & % 83.66/11.68 | | | all_63_7 = all_55_6 & all_55_0 = all_55_1 & ~ (all_63_5 = % 83.66/11.68 | | | all_55_7) & vvar(all_63_5) = all_55_1) | (all_63_8 = all_55_0 % 83.66/11.68 | | | & all_63_11 = all_55_1 & all_63_13 = all_55_6 & all_63_14 = % 83.66/11.68 | | | all_55_7 & vsubst(all_55_7, all_55_6, all_63_12) = all_63_9 & % 83.66/11.68 | | | vsubst(all_55_7, all_55_6, all_63_15) = all_63_10 & % 83.66/11.68 | | | vapp(all_63_10, all_63_9) = all_55_0 & vapp(all_63_15, % 83.66/11.68 | | | all_63_12) = all_55_1 & $i(all_63_9) & $i(all_63_10)) % 83.66/11.68 | | | % 83.66/11.68 | | | BETA: splitting (54) gives: % 83.66/11.68 | | | % 83.66/11.68 | | | Case 1: % 83.66/11.68 | | | | % 83.66/11.68 | | | | (55) all_63_0 = all_55_1 & all_63_1 = all_55_6 & all_63_2 = all_55_7 % 83.66/11.68 | | | | & all_63_3 = all_55_7 & all_55_0 = all_55_6 & vvar(all_55_7) = % 83.66/11.68 | | | | all_55_1 % 83.66/11.68 | | | | % 83.66/11.68 | | | | ALPHA: (55) implies: % 83.66/11.68 | | | | (56) vvar(all_55_7) = all_55_1 % 83.66/11.68 | | | | % 83.66/11.68 | | | | GROUND_INST: instantiating (isValue1) with all_55_7, all_55_1, % 83.66/11.68 | | | | simplifying with (18), (24), (29), (56) gives: % 83.66/11.68 | | | | (57) $false % 83.66/11.68 | | | | % 83.66/11.68 | | | | CLOSE: (57) is inconsistent. % 83.66/11.68 | | | | % 83.66/11.68 | | | Case 2: % 83.66/11.68 | | | | % 83.66/11.68 | | | | (58) (all_63_4 = all_55_1 & all_63_6 = all_55_7 & all_63_7 = all_55_6 % 83.66/11.68 | | | | & all_55_0 = all_55_1 & ~ (all_63_5 = all_55_7) & % 83.66/11.68 | | | | vvar(all_63_5) = all_55_1) | (all_63_8 = all_55_0 & all_63_11 % 83.66/11.68 | | | | = all_55_1 & all_63_13 = all_55_6 & all_63_14 = all_55_7 & % 83.66/11.68 | | | | vsubst(all_55_7, all_55_6, all_63_12) = all_63_9 & % 83.66/11.68 | | | | vsubst(all_55_7, all_55_6, all_63_15) = all_63_10 & % 83.66/11.68 | | | | vapp(all_63_10, all_63_9) = all_55_0 & vapp(all_63_15, % 83.66/11.68 | | | | all_63_12) = all_55_1 & $i(all_63_9) & $i(all_63_10)) % 83.66/11.68 | | | | % 83.66/11.68 | | | | BETA: splitting (58) gives: % 83.66/11.68 | | | | % 83.66/11.68 | | | | Case 1: % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | (59) all_63_4 = all_55_1 & all_63_6 = all_55_7 & all_63_7 = % 83.66/11.68 | | | | | all_55_6 & all_55_0 = all_55_1 & ~ (all_63_5 = all_55_7) & % 83.66/11.68 | | | | | vvar(all_63_5) = all_55_1 % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | ALPHA: (59) implies: % 83.66/11.68 | | | | | (60) vvar(all_63_5) = all_55_1 % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | GROUND_INST: instantiating (isValue1) with all_63_5, all_55_1, % 83.66/11.68 | | | | | simplifying with (24), (29), (49), (60) gives: % 83.66/11.68 | | | | | (61) $false % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | CLOSE: (61) is inconsistent. % 83.66/11.68 | | | | | % 83.66/11.68 | | | | Case 2: % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | (62) all_63_8 = all_55_0 & all_63_11 = all_55_1 & all_63_13 = % 83.66/11.68 | | | | | all_55_6 & all_63_14 = all_55_7 & vsubst(all_55_7, all_55_6, % 83.66/11.68 | | | | | all_63_12) = all_63_9 & vsubst(all_55_7, all_55_6, % 83.66/11.68 | | | | | all_63_15) = all_63_10 & vapp(all_63_10, all_63_9) = % 83.66/11.68 | | | | | all_55_0 & vapp(all_63_15, all_63_12) = all_55_1 & % 83.66/11.68 | | | | | $i(all_63_9) & $i(all_63_10) % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | ALPHA: (62) implies: % 83.66/11.68 | | | | | (63) vapp(all_63_15, all_63_12) = all_55_1 % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | GROUND_INST: instantiating (isValue2) with all_63_15, all_63_12, % 83.66/11.68 | | | | | all_55_1, simplifying with (24), (29), (47), (48), (63) % 83.66/11.68 | | | | | gives: % 83.66/11.68 | | | | | (64) $false % 83.66/11.68 | | | | | % 83.66/11.68 | | | | | CLOSE: (64) is inconsistent. % 83.66/11.68 | | | | | % 83.66/11.68 | | | | End of split % 83.66/11.68 | | | | % 83.66/11.68 | | | End of split % 83.66/11.68 | | | % 83.66/11.68 | | Case 2: % 83.66/11.68 | | | % 83.66/11.69 | | | (65) (all_63_16 = all_55_1 & all_63_19 = all_55_7 & all_63_20 = % 83.66/11.69 | | | all_55_7 & all_63_21 = all_55_6 & all_55_0 = all_55_1 & % 83.66/11.69 | | | vabs(all_55_7, all_63_18, all_63_17) = all_55_1) | (all_63_22 = % 83.66/11.69 | | | all_55_0 & all_63_26 = all_63_32 & all_63_30 = all_55_1 & % 83.66/11.69 | | | all_63_35 = all_55_6 & all_63_36 = all_55_7 & ~ (all_63_33 = % 83.66/11.69 | | | all_55_7) & vsubst(all_63_33, all_63_25, all_63_31) = % 83.66/11.69 | | | all_63_24 & vsubst(all_55_7, all_55_6, all_63_23) = all_55_0 & % 83.66/11.69 | | | vgensym(all_63_27) = all_63_32 & vapp(all_63_29, all_63_28) = % 83.66/11.69 | | | all_63_27 & vapp(all_55_6, all_63_31) = all_63_29 & % 83.66/11.69 | | | vabs(all_63_32, all_63_34, all_63_24) = all_63_23 & % 83.66/11.69 | | | vabs(all_63_33, all_63_34, all_63_31) = all_55_1 & % 83.66/11.69 | | | vvar(all_63_32) = all_63_25 & vvar(all_55_7) = all_63_28 & % 83.66/11.69 | | | $i(all_63_23) & $i(all_63_24) & $i(all_63_25) & $i(all_63_27) & % 83.66/11.69 | | | $i(all_63_28) & $i(all_63_29) & visFreeVar(all_63_33, all_55_6)) % 83.66/11.69 | | | | (all_63_37 = all_55_0 & all_63_39 = all_55_1 & all_63_41 = % 83.66/11.69 | | | all_55_6 & all_63_42 = all_55_7 & ~ (all_63_44 = all_55_7) & % 83.66/11.69 | | | vsubst(all_55_7, all_55_6, all_63_40) = all_63_38 & % 83.66/11.69 | | | vabs(all_63_44, all_63_43, all_63_38) = all_55_0 & % 83.66/11.69 | | | vabs(all_63_44, all_63_43, all_63_40) = all_55_1 & $i(all_63_38) % 83.66/11.69 | | | & ~ visFreeVar(all_63_44, all_55_6)) % 83.66/11.69 | | | % 83.66/11.69 | | | BETA: splitting (65) gives: % 83.66/11.69 | | | % 83.66/11.69 | | | Case 1: % 83.66/11.69 | | | | % 83.66/11.69 | | | | (66) all_63_16 = all_55_1 & all_63_19 = all_55_7 & all_63_20 = % 83.66/11.69 | | | | all_55_7 & all_63_21 = all_55_6 & all_55_0 = all_55_1 & % 83.66/11.69 | | | | vabs(all_55_7, all_63_18, all_63_17) = all_55_1 % 83.66/11.69 | | | | % 83.66/11.69 | | | | ALPHA: (66) implies: % 83.66/11.69 | | | | (67) all_55_0 = all_55_1 % 83.66/11.69 | | | | % 83.66/11.69 | | | | REDUCE: (53), (67) imply: % 83.66/11.69 | | | | (68) $false % 83.66/11.69 | | | | % 83.66/11.69 | | | | CLOSE: (68) is inconsistent. % 83.66/11.69 | | | | % 83.66/11.69 | | | Case 2: % 83.66/11.69 | | | | % 83.66/11.69 | | | | (69) (all_63_22 = all_55_0 & all_63_26 = all_63_32 & all_63_30 = % 83.66/11.69 | | | | all_55_1 & all_63_35 = all_55_6 & all_63_36 = all_55_7 & ~ % 83.66/11.69 | | | | (all_63_33 = all_55_7) & vsubst(all_63_33, all_63_25, % 83.66/11.69 | | | | all_63_31) = all_63_24 & vsubst(all_55_7, all_55_6, % 83.66/11.69 | | | | all_63_23) = all_55_0 & vgensym(all_63_27) = all_63_32 & % 83.66/11.69 | | | | vapp(all_63_29, all_63_28) = all_63_27 & vapp(all_55_6, % 83.66/11.69 | | | | all_63_31) = all_63_29 & vabs(all_63_32, all_63_34, % 83.66/11.69 | | | | all_63_24) = all_63_23 & vabs(all_63_33, all_63_34, % 83.66/11.69 | | | | all_63_31) = all_55_1 & vvar(all_63_32) = all_63_25 & % 83.66/11.69 | | | | vvar(all_55_7) = all_63_28 & $i(all_63_23) & $i(all_63_24) & % 83.66/11.69 | | | | $i(all_63_25) & $i(all_63_27) & $i(all_63_28) & $i(all_63_29) % 83.66/11.69 | | | | & visFreeVar(all_63_33, all_55_6)) | (all_63_37 = all_55_0 & % 83.66/11.69 | | | | all_63_39 = all_55_1 & all_63_41 = all_55_6 & all_63_42 = % 83.66/11.69 | | | | all_55_7 & ~ (all_63_44 = all_55_7) & vsubst(all_55_7, % 83.66/11.69 | | | | all_55_6, all_63_40) = all_63_38 & vabs(all_63_44, % 83.66/11.69 | | | | all_63_43, all_63_38) = all_55_0 & vabs(all_63_44, % 83.66/11.69 | | | | all_63_43, all_63_40) = all_55_1 & $i(all_63_38) & ~ % 83.66/11.69 | | | | visFreeVar(all_63_44, all_55_6)) % 83.66/11.69 | | | | % 83.66/11.69 | | | | BETA: splitting (69) gives: % 83.66/11.69 | | | | % 83.66/11.69 | | | | Case 1: % 83.66/11.69 | | | | | % 83.66/11.69 | | | | | (70) all_63_22 = all_55_0 & all_63_26 = all_63_32 & all_63_30 = % 83.66/11.69 | | | | | all_55_1 & all_63_35 = all_55_6 & all_63_36 = all_55_7 & ~ % 83.66/11.69 | | | | | (all_63_33 = all_55_7) & vsubst(all_63_33, all_63_25, % 83.66/11.69 | | | | | all_63_31) = all_63_24 & vsubst(all_55_7, all_55_6, % 83.66/11.69 | | | | | all_63_23) = all_55_0 & vgensym(all_63_27) = all_63_32 & % 83.66/11.69 | | | | | vapp(all_63_29, all_63_28) = all_63_27 & vapp(all_55_6, % 83.66/11.69 | | | | | all_63_31) = all_63_29 & vabs(all_63_32, all_63_34, % 83.66/11.69 | | | | | all_63_24) = all_63_23 & vabs(all_63_33, all_63_34, % 83.66/11.69 | | | | | all_63_31) = all_55_1 & vvar(all_63_32) = all_63_25 & % 83.66/11.69 | | | | | vvar(all_55_7) = all_63_28 & $i(all_63_23) & $i(all_63_24) & % 83.66/11.69 | | | | | $i(all_63_25) & $i(all_63_27) & $i(all_63_28) & $i(all_63_29) % 83.66/11.69 | | | | | & visFreeVar(all_63_33, all_55_6) % 83.66/11.69 | | | | | % 83.66/11.69 | | | | | ALPHA: (70) implies: % 83.66/11.69 | | | | | (71) all_63_36 = all_55_7 % 83.66/11.69 | | | | | (72) all_63_35 = all_55_6 % 83.66/11.69 | | | | | (73) $i(all_63_29) % 83.66/11.69 | | | | | (74) $i(all_63_28) % 83.66/11.69 | | | | | (75) $i(all_63_27) % 83.66/11.69 | | | | | (76) $i(all_63_24) % 83.66/11.69 | | | | | (77) $i(all_63_23) % 83.66/11.69 | | | | | (78) vvar(all_55_7) = all_63_28 % 83.66/11.69 | | | | | (79) vvar(all_63_32) = all_63_25 % 83.66/11.69 | | | | | (80) vabs(all_63_33, all_63_34, all_63_31) = all_55_1 % 83.66/11.69 | | | | | (81) vabs(all_63_32, all_63_34, all_63_24) = all_63_23 % 83.66/11.69 | | | | | (82) vapp(all_55_6, all_63_31) = all_63_29 % 83.66/11.69 | | | | | (83) vapp(all_63_29, all_63_28) = all_63_27 % 83.66/11.69 | | | | | (84) vgensym(all_63_27) = all_63_32 % 83.66/11.69 | | | | | (85) vsubst(all_55_7, all_55_6, all_63_23) = all_55_0 % 83.66/11.69 | | | | | (86) vsubst(all_63_33, all_63_25, all_63_31) = all_63_24 % 83.66/11.69 | | | | | % 83.66/11.69 | | | | | GROUND_INST: instantiating (3) with all_55_5, all_55_4, veabs, % 83.66/11.69 | | | | | all_63_33, all_63_34, all_63_31, all_55_1, simplifying % 83.66/11.69 | | | | | with (8), (20), (21), (26), (40), (41), (43), (80) gives: % 83.66/11.69 | | | | | (87) all_63_31 = veabs % 83.66/11.69 | | | | | % 83.66/11.70 | | | | | GROUND_INST: instantiating (2) with all_55_5, all_55_4, veabs, % 83.66/11.70 | | | | | all_63_33, all_63_34, all_63_31, all_55_1, simplifying % 83.66/11.70 | | | | | with (8), (20), (21), (26), (40), (41), (43), (80) gives: % 83.66/11.70 | | | | | (88) all_63_34 = all_55_4 % 83.66/11.70 | | | | | % 83.66/11.70 | | | | | GROUND_INST: instantiating (1) with all_55_5, all_55_4, veabs, % 83.66/11.70 | | | | | all_63_33, all_63_34, all_63_31, all_55_1, simplifying % 83.66/11.70 | | | | | with (8), (20), (21), (26), (40), (41), (43), (80) gives: % 83.66/11.70 | | | | | (89) all_63_33 = all_55_5 % 83.66/11.70 | | | | | % 83.66/11.70 | | | | | GROUND_INST: instantiating (fresh-unequal-var-3) with all_55_6, % 83.66/11.70 | | | | | all_63_31, all_63_32, all_63_29, all_63_28, all_63_27, % 83.66/11.70 | | | | | simplifying with (19), (42), (43), (82), (83), (84) % 83.66/11.70 | | | | | gives: % 83.66/11.70 | | | | | (90) ~ (vvar(all_63_32) = all_63_28) % 83.66/11.70 | | | | | % 83.66/11.70 | | | | | GROUND_INST: instantiating (alpha-equiv-subst-abs) with all_63_34, % 83.66/11.70 | | | | | all_63_33, all_63_32, all_63_31, all_63_25, all_63_24, % 83.66/11.70 | | | | | all_63_23, simplifying with (40), (41), (42), (43), (79), % 83.66/11.70 | | | | | (81), (86) gives: % 83.66/11.70 | | | | | (91) visFreeVar(all_63_32, all_63_31) | ? [v0: $i] : % 83.66/11.70 | | | | | (vabs(all_63_33, all_63_34, all_63_31) = v0 & $i(v0) & % 83.66/11.70 | | | | | valphaEquivalent(v0, all_63_23)) % 83.66/11.70 | | | | | % 83.66/11.70 | | | | | REDUCE: (82), (87) imply: % 83.66/11.70 | | | | | (92) vapp(all_55_6, veabs) = all_63_29 % 83.66/11.70 | | | | | % 83.66/11.70 | | | | | REDUCE: (81), (88) imply: % 83.66/11.70 | | | | | (93) vabs(all_63_32, all_55_4, all_63_24) = all_63_23 % 83.66/11.70 | | | | | % 83.66/11.70 | | | | | PRED_UNIFY: (78), (90) imply: % 83.66/11.70 | | | | | (94) ~ (all_63_32 = all_55_7) % 83.66/11.70 | | | | | % 83.66/11.70 | | | | | GROUND_INST: instantiating (6) with all_63_32, all_63_29, all_55_6, % 83.66/11.70 | | | | | veabs, simplifying with (8), (19), (42), (73), (92) % 83.66/11.70 | | | | | gives: % 83.66/11.70 | | | | | (95) ~ visFreeVar(all_63_32, all_55_6) | visFreeVar(all_63_32, % 83.66/11.70 | | | | | all_63_29) % 83.66/11.70 | | | | | % 83.66/11.71 | | | | | REF_CLOSE: (6), (8), (10), (13), (14), (15), (16), (17), (18), (19), % 83.66/11.71 | | | | | (21), (22), (23), (26), (27), (42), (73), (74), (75), (76), % 83.66/11.71 | | | | | (77), (78), (83), (84), (85), (87), (88), (89), (91), (92), % 83.66/11.71 | | | | | (93), (94), (95), (T-subst-abs-2-gen), % 83.66/11.71 | | | | | (alpha-equiv-typing), (fresh-free-2), (gensym-is-fresh) are % 83.66/11.71 | | | | | inconsistent by sub-proof #2. % 83.66/11.71 | | | | | % 83.66/11.71 | | | | Case 2: % 83.66/11.71 | | | | | % 83.66/11.71 | | | | | (96) all_63_37 = all_55_0 & all_63_39 = all_55_1 & all_63_41 = % 83.66/11.71 | | | | | all_55_6 & all_63_42 = all_55_7 & ~ (all_63_44 = all_55_7) & % 83.66/11.71 | | | | | vsubst(all_55_7, all_55_6, all_63_40) = all_63_38 & % 83.66/11.71 | | | | | vabs(all_63_44, all_63_43, all_63_38) = all_55_0 & % 83.66/11.71 | | | | | vabs(all_63_44, all_63_43, all_63_40) = all_55_1 & % 83.66/11.71 | | | | | $i(all_63_38) & ~ visFreeVar(all_63_44, all_55_6) % 83.66/11.71 | | | | | % 83.66/11.71 | | | | | ALPHA: (96) implies: % 83.66/11.71 | | | | | (97) ~ visFreeVar(all_63_44, all_55_6) % 83.66/11.71 | | | | | (98) vabs(all_63_44, all_63_43, all_63_40) = all_55_1 % 83.66/11.71 | | | | | % 83.66/11.71 | | | | | REF_CLOSE: (1), (8), (12), (13), (14), (15), (16), (17), (18), (19), % 83.66/11.71 | | | | | (20), (21), (22), (26), (27), (28), (33), (34), (37), (97), % 83.66/11.71 | | | | | (98), (T-subst-abs-2-gen) are inconsistent by sub-proof #1. % 83.66/11.71 | | | | | % 83.66/11.71 | | | | End of split % 83.66/11.71 | | | | % 83.66/11.71 | | | End of split % 83.66/11.71 | | | % 83.66/11.71 | | End of split % 83.66/11.71 | | % 83.66/11.71 | Case 2: % 83.66/11.71 | | % 83.66/11.71 | | (99) visFreeVar(all_55_7, all_55_1) % 83.66/11.71 | | % 83.66/11.71 | | GROUND_INST: instantiating (5) with all_55_4, all_55_7, all_55_1, all_55_5, % 83.66/11.71 | | veabs, simplifying with (8), (18), (20), (21), (24), (26), (99) % 83.66/11.71 | | gives: % 83.66/11.71 | | (100) visFreeVar(all_55_7, veabs) % 83.66/11.71 | | % 83.66/11.71 | | BETA: splitting (51) gives: % 83.66/11.71 | | % 83.66/11.71 | | Case 1: % 83.66/11.71 | | | % 83.66/11.71 | | | (101) (all_63_0 = all_55_1 & all_63_1 = all_55_6 & all_63_2 = all_55_7 % 83.66/11.71 | | | & all_63_3 = all_55_7 & all_55_0 = all_55_6 & vvar(all_55_7) = % 83.66/11.71 | | | all_55_1) | (all_63_4 = all_55_1 & all_63_6 = all_55_7 & % 83.66/11.71 | | | all_63_7 = all_55_6 & all_55_0 = all_55_1 & ~ (all_63_5 = % 83.66/11.71 | | | all_55_7) & vvar(all_63_5) = all_55_1) | (all_63_8 = all_55_0 % 83.66/11.71 | | | & all_63_11 = all_55_1 & all_63_13 = all_55_6 & all_63_14 = % 83.66/11.71 | | | all_55_7 & vsubst(all_55_7, all_55_6, all_63_12) = all_63_9 & % 83.66/11.71 | | | vsubst(all_55_7, all_55_6, all_63_15) = all_63_10 & % 83.66/11.71 | | | vapp(all_63_10, all_63_9) = all_55_0 & vapp(all_63_15, % 83.66/11.71 | | | all_63_12) = all_55_1 & $i(all_63_9) & $i(all_63_10)) % 83.66/11.71 | | | % 83.66/11.71 | | | BETA: splitting (101) gives: % 83.66/11.71 | | | % 83.66/11.71 | | | Case 1: % 83.66/11.71 | | | | % 83.66/11.71 | | | | (102) all_63_0 = all_55_1 & all_63_1 = all_55_6 & all_63_2 = all_55_7 % 83.66/11.71 | | | | & all_63_3 = all_55_7 & all_55_0 = all_55_6 & vvar(all_55_7) = % 83.66/11.71 | | | | all_55_1 % 83.66/11.71 | | | | % 83.66/11.71 | | | | ALPHA: (102) implies: % 83.66/11.71 | | | | (103) all_63_3 = all_55_7 % 83.66/11.71 | | | | (104) vvar(all_55_7) = all_55_1 % 83.66/11.71 | | | | % 83.66/11.71 | | | | GROUND_INST: instantiating (isValue1) with all_55_7, all_55_1, % 83.66/11.71 | | | | simplifying with (18), (24), (29), (104) gives: % 83.66/11.71 | | | | (105) $false % 83.66/11.71 | | | | % 83.66/11.71 | | | | CLOSE: (105) is inconsistent. % 83.66/11.71 | | | | % 83.66/11.71 | | | Case 2: % 83.66/11.71 | | | | % 83.92/11.71 | | | | (106) (all_63_4 = all_55_1 & all_63_6 = all_55_7 & all_63_7 = % 83.92/11.71 | | | | all_55_6 & all_55_0 = all_55_1 & ~ (all_63_5 = all_55_7) & % 83.92/11.71 | | | | vvar(all_63_5) = all_55_1) | (all_63_8 = all_55_0 & all_63_11 % 83.92/11.71 | | | | = all_55_1 & all_63_13 = all_55_6 & all_63_14 = all_55_7 & % 83.92/11.71 | | | | vsubst(all_55_7, all_55_6, all_63_12) = all_63_9 & % 83.92/11.71 | | | | vsubst(all_55_7, all_55_6, all_63_15) = all_63_10 & % 83.92/11.71 | | | | vapp(all_63_10, all_63_9) = all_55_0 & vapp(all_63_15, % 83.92/11.71 | | | | all_63_12) = all_55_1 & $i(all_63_9) & $i(all_63_10)) % 83.92/11.71 | | | | % 83.92/11.71 | | | | BETA: splitting (106) gives: % 83.92/11.71 | | | | % 83.92/11.71 | | | | Case 1: % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | (107) all_63_4 = all_55_1 & all_63_6 = all_55_7 & all_63_7 = % 83.92/11.71 | | | | | all_55_6 & all_55_0 = all_55_1 & ~ (all_63_5 = all_55_7) & % 83.92/11.71 | | | | | vvar(all_63_5) = all_55_1 % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | ALPHA: (107) implies: % 83.92/11.71 | | | | | (108) all_55_0 = all_55_1 % 83.92/11.71 | | | | | (109) vvar(all_63_5) = all_55_1 % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | GROUND_INST: instantiating (isValue1) with all_63_5, all_55_1, % 83.92/11.71 | | | | | simplifying with (24), (29), (49), (109) gives: % 83.92/11.71 | | | | | (110) $false % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | CLOSE: (110) is inconsistent. % 83.92/11.71 | | | | | % 83.92/11.71 | | | | Case 2: % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | (111) all_63_8 = all_55_0 & all_63_11 = all_55_1 & all_63_13 = % 83.92/11.71 | | | | | all_55_6 & all_63_14 = all_55_7 & vsubst(all_55_7, all_55_6, % 83.92/11.71 | | | | | all_63_12) = all_63_9 & vsubst(all_55_7, all_55_6, % 83.92/11.71 | | | | | all_63_15) = all_63_10 & vapp(all_63_10, all_63_9) = % 83.92/11.71 | | | | | all_55_0 & vapp(all_63_15, all_63_12) = all_55_1 & % 83.92/11.71 | | | | | $i(all_63_9) & $i(all_63_10) % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | ALPHA: (111) implies: % 83.92/11.71 | | | | | (112) vapp(all_63_15, all_63_12) = all_55_1 % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | GROUND_INST: instantiating (isValue2) with all_63_15, all_63_12, % 83.92/11.71 | | | | | all_55_1, simplifying with (24), (29), (47), (48), (112) % 83.92/11.71 | | | | | gives: % 83.92/11.71 | | | | | (113) $false % 83.92/11.71 | | | | | % 83.92/11.71 | | | | | CLOSE: (113) is inconsistent. % 83.92/11.71 | | | | | % 83.92/11.71 | | | | End of split % 83.92/11.71 | | | | % 83.92/11.71 | | | End of split % 83.92/11.71 | | | % 83.92/11.71 | | Case 2: % 83.92/11.71 | | | % 83.92/11.71 | | | (114) (all_63_16 = all_55_1 & all_63_19 = all_55_7 & all_63_20 = % 83.92/11.71 | | | all_55_7 & all_63_21 = all_55_6 & all_55_0 = all_55_1 & % 83.92/11.71 | | | vabs(all_55_7, all_63_18, all_63_17) = all_55_1) | (all_63_22 = % 83.92/11.71 | | | all_55_0 & all_63_26 = all_63_32 & all_63_30 = all_55_1 & % 83.92/11.71 | | | all_63_35 = all_55_6 & all_63_36 = all_55_7 & ~ (all_63_33 = % 83.92/11.71 | | | all_55_7) & vsubst(all_63_33, all_63_25, all_63_31) = % 83.92/11.71 | | | all_63_24 & vsubst(all_55_7, all_55_6, all_63_23) = all_55_0 & % 83.92/11.71 | | | vgensym(all_63_27) = all_63_32 & vapp(all_63_29, all_63_28) = % 83.92/11.71 | | | all_63_27 & vapp(all_55_6, all_63_31) = all_63_29 & % 83.92/11.71 | | | vabs(all_63_32, all_63_34, all_63_24) = all_63_23 & % 83.92/11.71 | | | vabs(all_63_33, all_63_34, all_63_31) = all_55_1 & % 83.92/11.71 | | | vvar(all_63_32) = all_63_25 & vvar(all_55_7) = all_63_28 & % 83.92/11.71 | | | $i(all_63_23) & $i(all_63_24) & $i(all_63_25) & $i(all_63_27) & % 83.92/11.71 | | | $i(all_63_28) & $i(all_63_29) & visFreeVar(all_63_33, % 83.92/11.71 | | | all_55_6)) | (all_63_37 = all_55_0 & all_63_39 = all_55_1 & % 83.92/11.71 | | | all_63_41 = all_55_6 & all_63_42 = all_55_7 & ~ (all_63_44 = % 83.92/11.71 | | | all_55_7) & vsubst(all_55_7, all_55_6, all_63_40) = all_63_38 % 83.92/11.71 | | | & vabs(all_63_44, all_63_43, all_63_38) = all_55_0 & % 83.92/11.71 | | | vabs(all_63_44, all_63_43, all_63_40) = all_55_1 & % 83.92/11.71 | | | $i(all_63_38) & ~ visFreeVar(all_63_44, all_55_6)) % 83.92/11.71 | | | % 83.92/11.71 | | | BETA: splitting (114) gives: % 83.92/11.71 | | | % 83.92/11.71 | | | Case 1: % 83.92/11.71 | | | | % 83.92/11.71 | | | | (115) all_63_16 = all_55_1 & all_63_19 = all_55_7 & all_63_20 = % 83.92/11.71 | | | | all_55_7 & all_63_21 = all_55_6 & all_55_0 = all_55_1 & % 83.92/11.71 | | | | vabs(all_55_7, all_63_18, all_63_17) = all_55_1 % 83.92/11.71 | | | | % 83.92/11.71 | | | | ALPHA: (115) implies: % 83.92/11.71 | | | | (116) all_55_0 = all_55_1 % 83.92/11.71 | | | | (117) all_63_20 = all_55_7 % 83.92/11.71 | | | | (118) vabs(all_55_7, all_63_18, all_63_17) = all_55_1 % 83.92/11.72 | | | | % 83.92/11.72 | | | | GROUND_INST: instantiating (4) with all_63_18, all_55_7, all_55_1, % 83.92/11.72 | | | | all_63_17, simplifying with (18), (24), (45), (46), (99), % 83.92/11.72 | | | | (118) gives: % 83.92/11.72 | | | | (119) $false % 83.92/11.72 | | | | % 83.92/11.72 | | | | CLOSE: (119) is inconsistent. % 83.92/11.72 | | | | % 83.92/11.72 | | | Case 2: % 83.92/11.72 | | | | % 83.92/11.72 | | | | (120) (all_63_22 = all_55_0 & all_63_26 = all_63_32 & all_63_30 = % 83.92/11.72 | | | | all_55_1 & all_63_35 = all_55_6 & all_63_36 = all_55_7 & ~ % 83.92/11.72 | | | | (all_63_33 = all_55_7) & vsubst(all_63_33, all_63_25, % 83.92/11.72 | | | | all_63_31) = all_63_24 & vsubst(all_55_7, all_55_6, % 83.92/11.72 | | | | all_63_23) = all_55_0 & vgensym(all_63_27) = all_63_32 & % 83.92/11.72 | | | | vapp(all_63_29, all_63_28) = all_63_27 & vapp(all_55_6, % 83.92/11.72 | | | | all_63_31) = all_63_29 & vabs(all_63_32, all_63_34, % 83.92/11.72 | | | | all_63_24) = all_63_23 & vabs(all_63_33, all_63_34, % 83.92/11.72 | | | | all_63_31) = all_55_1 & vvar(all_63_32) = all_63_25 & % 83.92/11.72 | | | | vvar(all_55_7) = all_63_28 & $i(all_63_23) & $i(all_63_24) & % 83.92/11.72 | | | | $i(all_63_25) & $i(all_63_27) & $i(all_63_28) & $i(all_63_29) % 83.92/11.72 | | | | & visFreeVar(all_63_33, all_55_6)) | (all_63_37 = all_55_0 & % 83.92/11.72 | | | | all_63_39 = all_55_1 & all_63_41 = all_55_6 & all_63_42 = % 83.92/11.72 | | | | all_55_7 & ~ (all_63_44 = all_55_7) & vsubst(all_55_7, % 83.92/11.72 | | | | all_55_6, all_63_40) = all_63_38 & vabs(all_63_44, % 83.92/11.72 | | | | all_63_43, all_63_38) = all_55_0 & vabs(all_63_44, % 83.92/11.72 | | | | all_63_43, all_63_40) = all_55_1 & $i(all_63_38) & ~ % 83.92/11.72 | | | | visFreeVar(all_63_44, all_55_6)) % 83.92/11.72 | | | | % 83.92/11.72 | | | | BETA: splitting (120) gives: % 83.92/11.72 | | | | % 83.92/11.72 | | | | Case 1: % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | (121) all_63_22 = all_55_0 & all_63_26 = all_63_32 & all_63_30 = % 83.92/11.72 | | | | | all_55_1 & all_63_35 = all_55_6 & all_63_36 = all_55_7 & ~ % 83.92/11.72 | | | | | (all_63_33 = all_55_7) & vsubst(all_63_33, all_63_25, % 83.92/11.72 | | | | | all_63_31) = all_63_24 & vsubst(all_55_7, all_55_6, % 83.92/11.72 | | | | | all_63_23) = all_55_0 & vgensym(all_63_27) = all_63_32 & % 83.92/11.72 | | | | | vapp(all_63_29, all_63_28) = all_63_27 & vapp(all_55_6, % 83.92/11.72 | | | | | all_63_31) = all_63_29 & vabs(all_63_32, all_63_34, % 83.92/11.72 | | | | | all_63_24) = all_63_23 & vabs(all_63_33, all_63_34, % 83.92/11.72 | | | | | all_63_31) = all_55_1 & vvar(all_63_32) = all_63_25 & % 83.92/11.72 | | | | | vvar(all_55_7) = all_63_28 & $i(all_63_23) & $i(all_63_24) & % 83.92/11.72 | | | | | $i(all_63_25) & $i(all_63_27) & $i(all_63_28) & $i(all_63_29) % 83.92/11.72 | | | | | & visFreeVar(all_63_33, all_55_6) % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | ALPHA: (121) implies: % 83.92/11.72 | | | | | (122) all_63_36 = all_55_7 % 83.92/11.72 | | | | | (123) all_63_35 = all_55_6 % 83.92/11.72 | | | | | (124) $i(all_63_29) % 83.92/11.72 | | | | | (125) $i(all_63_28) % 83.92/11.72 | | | | | (126) $i(all_63_27) % 83.92/11.72 | | | | | (127) $i(all_63_24) % 83.92/11.72 | | | | | (128) $i(all_63_23) % 83.92/11.72 | | | | | (129) vvar(all_55_7) = all_63_28 % 83.92/11.72 | | | | | (130) vvar(all_63_32) = all_63_25 % 83.92/11.72 | | | | | (131) vabs(all_63_33, all_63_34, all_63_31) = all_55_1 % 83.92/11.72 | | | | | (132) vabs(all_63_32, all_63_34, all_63_24) = all_63_23 % 83.92/11.72 | | | | | (133) vapp(all_55_6, all_63_31) = all_63_29 % 83.92/11.72 | | | | | (134) vapp(all_63_29, all_63_28) = all_63_27 % 83.92/11.72 | | | | | (135) vgensym(all_63_27) = all_63_32 % 83.92/11.72 | | | | | (136) vsubst(all_55_7, all_55_6, all_63_23) = all_55_0 % 83.92/11.72 | | | | | (137) vsubst(all_63_33, all_63_25, all_63_31) = all_63_24 % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | GROUND_INST: instantiating (3) with all_55_5, all_55_4, veabs, % 83.92/11.72 | | | | | all_63_33, all_63_34, all_63_31, all_55_1, simplifying % 83.92/11.72 | | | | | with (8), (20), (21), (26), (40), (41), (43), (131) % 83.92/11.72 | | | | | gives: % 83.92/11.72 | | | | | (138) all_63_31 = veabs % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | GROUND_INST: instantiating (2) with all_55_5, all_55_4, veabs, % 83.92/11.72 | | | | | all_63_33, all_63_34, all_63_31, all_55_1, simplifying % 83.92/11.72 | | | | | with (8), (20), (21), (26), (40), (41), (43), (131) % 83.92/11.72 | | | | | gives: % 83.92/11.72 | | | | | (139) all_63_34 = all_55_4 % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | GROUND_INST: instantiating (1) with all_55_5, all_55_4, veabs, % 83.92/11.72 | | | | | all_63_33, all_63_34, all_63_31, all_55_1, simplifying % 83.92/11.72 | | | | | with (8), (20), (21), (26), (40), (41), (43), (131) % 83.92/11.72 | | | | | gives: % 83.92/11.72 | | | | | (140) all_63_33 = all_55_5 % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | GROUND_INST: instantiating (7) with all_55_7, all_63_29, all_55_6, % 83.92/11.72 | | | | | veabs, simplifying with (8), (18), (19), (100), (124) % 83.92/11.72 | | | | | gives: % 83.92/11.72 | | | | | (141) ~ (vapp(all_55_6, veabs) = all_63_29) | visFreeVar(all_55_7, % 83.92/11.72 | | | | | all_63_29) % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | GROUND_INST: instantiating (fresh-unequal-var-3) with all_55_6, % 83.92/11.72 | | | | | all_63_31, all_63_32, all_63_29, all_63_28, all_63_27, % 83.92/11.72 | | | | | simplifying with (19), (42), (43), (133), (134), (135) % 83.92/11.72 | | | | | gives: % 83.92/11.72 | | | | | (142) ~ (vvar(all_63_32) = all_63_28) % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | GROUND_INST: instantiating (alpha-equiv-subst-abs) with all_63_34, % 83.92/11.72 | | | | | all_63_33, all_63_32, all_63_31, all_63_25, all_63_24, % 83.92/11.72 | | | | | all_63_23, simplifying with (40), (41), (42), (43), % 83.92/11.72 | | | | | (130), (132), (137) gives: % 83.92/11.72 | | | | | (143) visFreeVar(all_63_32, all_63_31) | ? [v0: $i] : % 83.92/11.72 | | | | | (vabs(all_63_33, all_63_34, all_63_31) = v0 & $i(v0) & % 83.92/11.72 | | | | | valphaEquivalent(v0, all_63_23)) % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | REDUCE: (133), (138) imply: % 83.92/11.72 | | | | | (144) vapp(all_55_6, veabs) = all_63_29 % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | REDUCE: (132), (139) imply: % 83.92/11.72 | | | | | (145) vabs(all_63_32, all_55_4, all_63_24) = all_63_23 % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | BETA: splitting (141) gives: % 83.92/11.72 | | | | | % 83.92/11.72 | | | | | Case 1: % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | | (146) ~ (vapp(all_55_6, veabs) = all_63_29) % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | | PRED_UNIFY: (144), (146) imply: % 83.92/11.72 | | | | | | (147) $false % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | | CLOSE: (147) is inconsistent. % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | Case 2: % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | | PRED_UNIFY: (129), (142) imply: % 83.92/11.72 | | | | | | (148) ~ (all_63_32 = all_55_7) % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | | GROUND_INST: instantiating (6) with all_63_32, all_63_29, all_55_6, % 83.92/11.72 | | | | | | veabs, simplifying with (8), (19), (42), (124), (144) % 83.92/11.72 | | | | | | gives: % 83.92/11.72 | | | | | | (149) ~ visFreeVar(all_63_32, all_55_6) | visFreeVar(all_63_32, % 83.92/11.72 | | | | | | all_63_29) % 83.92/11.72 | | | | | | % 83.92/11.72 | | | | | | REF_CLOSE: (6), (8), (10), (13), (14), (15), (16), (17), (18), (19), % 83.92/11.72 | | | | | | (21), (22), (23), (26), (27), (42), (124), (125), (126), % 83.92/11.73 | | | | | | (127), (128), (129), (134), (135), (136), (138), (139), % 83.92/11.73 | | | | | | (140), (143), (144), (145), (148), (149), % 83.92/11.73 | | | | | | (T-subst-abs-2-gen), (alpha-equiv-typing), % 83.92/11.73 | | | | | | (fresh-free-2), (gensym-is-fresh) are inconsistent by % 83.92/11.73 | | | | | | sub-proof #2. % 83.92/11.73 | | | | | | % 83.92/11.73 | | | | | End of split % 83.92/11.73 | | | | | % 83.92/11.73 | | | | Case 2: % 83.92/11.73 | | | | | % 83.92/11.73 | | | | | (150) all_63_37 = all_55_0 & all_63_39 = all_55_1 & all_63_41 = % 83.92/11.73 | | | | | all_55_6 & all_63_42 = all_55_7 & ~ (all_63_44 = all_55_7) & % 83.92/11.73 | | | | | vsubst(all_55_7, all_55_6, all_63_40) = all_63_38 & % 83.92/11.73 | | | | | vabs(all_63_44, all_63_43, all_63_38) = all_55_0 & % 83.92/11.73 | | | | | vabs(all_63_44, all_63_43, all_63_40) = all_55_1 & % 83.92/11.73 | | | | | $i(all_63_38) & ~ visFreeVar(all_63_44, all_55_6) % 83.92/11.73 | | | | | % 83.92/11.73 | | | | | ALPHA: (150) implies: % 83.92/11.73 | | | | | (151) all_63_42 = all_55_7 % 83.92/11.73 | | | | | (152) all_63_41 = all_55_6 % 83.92/11.73 | | | | | (153) ~ visFreeVar(all_63_44, all_55_6) % 83.92/11.73 | | | | | (154) vabs(all_63_44, all_63_43, all_63_40) = all_55_1 % 83.92/11.73 | | | | | % 83.92/11.73 | | | | | REF_CLOSE: (1), (8), (12), (13), (14), (15), (16), (17), (18), (19), % 83.92/11.73 | | | | | (20), (21), (22), (26), (27), (28), (33), (34), (37), % 83.92/11.73 | | | | | (153), (154), (T-subst-abs-2-gen) are inconsistent by % 83.92/11.73 | | | | | sub-proof #1. % 83.92/11.73 | | | | | % 83.92/11.73 | | | | End of split % 83.92/11.73 | | | | % 83.92/11.73 | | | End of split % 83.92/11.73 | | | % 83.92/11.73 | | End of split % 83.92/11.73 | | % 83.92/11.73 | End of split % 83.92/11.73 | % 83.92/11.73 End of proof % 83.92/11.73 % 83.92/11.73 Sub-proof #1 shows that the following formulas are inconsistent: % 83.92/11.73 ---------------------------------------------------------------- % 83.92/11.73 (1) $i(all_55_8) % 83.92/11.73 (2) $i(all_63_44) % 83.92/11.73 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 83.92/11.73 [v5: $i] : ! [v6: $i] : (v3 = v0 | ~ (vabs(v3, v4, v5) = v6) | ~ % 83.92/11.73 (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) % 83.92/11.73 | ~ $i(v1) | ~ $i(v0)) % 83.92/11.73 (4) $i(all_55_3) % 83.92/11.73 (5) ~ vtcheck(all_55_8, all_55_0, all_55_3) % 83.92/11.73 (6) $i(all_55_6) % 83.92/11.73 (7) ~ (all_55_5 = all_55_7) % 83.92/11.73 (8) ~ visFreeVar(all_63_44, all_55_6) % 83.92/11.73 (9) $i(veabs) % 83.92/11.73 (10) vtcheck(all_55_8, all_55_6, all_55_9) % 83.92/11.73 (11) vsubst(all_55_7, all_55_6, all_55_1) = all_55_0 % 83.92/11.73 (12) vabs(all_63_44, all_63_43, all_63_40) = all_55_1 % 83.92/11.73 (13) vtcheck(all_55_2, all_55_1, all_55_3) % 83.92/11.73 (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 83.92/11.73 [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! % 83.92/11.73 [v10: $i] : (v4 = v2 | ~ (vsubst(v2, v3, v9) = v10) | ~ (vbind(v2, v0, % 83.92/11.73 v1) = v8) | ~ (vabs(v4, v5, v6) = v9) | ~ $i(v7) | ~ $i(v6) | % 83.92/11.73 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 83.92/11.73 ~ vtcheck(v8, v9, v7) | ~ vtcheck(v1, v3, v0) | vtcheck(v1, v10, v7) % 83.92/11.73 | visFreeVar(v4, v3)) % 83.92/11.73 (15) $i(all_63_43) % 83.92/11.73 (16) $i(all_55_5) % 83.92/11.73 (17) $i(all_63_40) % 83.92/11.73 (18) $i(all_55_7) % 83.92/11.73 (19) $i(all_55_4) % 83.92/11.73 (20) vbind(all_55_7, all_55_9, all_55_8) = all_55_2 % 83.92/11.73 (21) vabs(all_55_5, all_55_4, veabs) = all_55_1 % 83.92/11.73 (22) $i(all_55_9) % 83.92/11.73 % 83.92/11.73 Begin of proof % 83.92/11.73 | % 83.92/11.73 | GROUND_INST: instantiating (14) with all_55_9, all_55_8, all_55_7, all_55_6, % 83.92/11.73 | all_63_44, all_63_43, all_63_40, all_55_3, all_55_2, all_55_1, % 83.92/11.73 | all_55_0, simplifying with (1), (2), (4), (5), (6), (8), (10), % 83.92/11.73 | (11), (12), (13), (15), (17), (18), (20), (22) gives: % 83.92/11.73 | (23) all_63_44 = all_55_7 % 83.92/11.73 | % 83.92/11.73 | GROUND_INST: instantiating (3) with all_55_5, all_55_4, veabs, all_63_44, % 83.92/11.73 | all_63_43, all_63_40, all_55_1, simplifying with (2), (9), (12), % 83.92/11.73 | (15), (16), (17), (19), (21) gives: % 83.92/11.73 | (24) all_63_44 = all_55_5 % 83.92/11.73 | % 83.92/11.73 | COMBINE_EQS: (23), (24) imply: % 83.92/11.73 | (25) all_55_5 = all_55_7 % 83.92/11.73 | % 83.92/11.73 | REDUCE: (7), (25) imply: % 83.92/11.73 | (26) $false % 83.92/11.73 | % 83.92/11.73 | CLOSE: (26) is inconsistent. % 83.92/11.73 | % 83.92/11.73 End of proof % 83.92/11.73 % 83.92/11.73 Sub-proof #2 shows that the following formulas are inconsistent: % 83.92/11.73 ---------------------------------------------------------------- % 83.92/11.73 (1) $i(all_55_8) % 83.92/11.73 (2) $i(all_63_24) % 83.92/11.73 (3) vvar(all_55_7) = all_63_28 % 83.92/11.73 (4) $i(all_63_28) % 83.92/11.73 (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, v3) % 83.92/11.73 = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 83.92/11.73 visFreeVar(v0, v2) | visFreeVar(v0, v1)) % 83.92/11.73 (6) vabs(all_63_32, all_55_4, all_63_24) = all_63_23 % 83.92/11.73 (7) $i(all_63_29) % 83.92/11.73 (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 83.92/11.73 [v5: $i] : ! [v6: $i] : ( ~ (vgensym(v6) = v2) | ~ (vapp(v4, v5) = v6) % 83.92/11.73 | ~ (vapp(v0, v3) = v4) | ~ (vvar(v1) = v5) | ~ $i(v3) | ~ $i(v2) | % 83.92/11.73 ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v2, v3)) % 83.92/11.73 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 83.92/11.73 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ valphaEquivalent(v0, v2) | ~ % 83.92/11.73 vtcheck(v1, v0, v3) | vtcheck(v1, v2, v3)) % 83.92/11.73 (10) ~ visFreeVar(all_63_32, all_55_6) | visFreeVar(all_63_32, all_63_29) % 83.92/11.73 (11) $i(all_63_23) % 83.92/11.73 (12) vgensym(all_63_27) = all_63_32 % 83.92/11.73 (13) all_63_34 = all_55_4 % 83.92/11.73 (14) $i(all_55_3) % 83.92/11.73 (15) ~ vtcheck(all_55_8, all_55_0, all_55_3) % 83.92/11.73 (16) $i(all_55_6) % 83.92/11.73 (17) vapp(all_55_6, veabs) = all_63_29 % 83.92/11.73 (18) $i(veabs) % 83.92/11.73 (19) vtcheck(all_55_8, all_55_6, all_55_9) % 83.92/11.73 (20) visFreeVar(all_63_32, all_63_31) | ? [v0: $i] : (vabs(all_63_33, % 83.92/11.73 all_63_34, all_63_31) = v0 & $i(v0) & valphaEquivalent(v0, % 83.92/11.73 all_63_23)) % 83.92/11.73 (21) vtcheck(all_55_2, all_55_1, all_55_3) % 83.92/11.73 (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 83.92/11.73 [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! % 83.92/11.73 [v10: $i] : (v4 = v2 | ~ (vsubst(v2, v3, v9) = v10) | ~ (vbind(v2, v0, % 83.92/11.73 v1) = v8) | ~ (vabs(v4, v5, v6) = v9) | ~ $i(v7) | ~ $i(v6) | % 83.92/11.73 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 83.92/11.73 ~ vtcheck(v8, v9, v7) | ~ vtcheck(v1, v3, v0) | vtcheck(v1, v10, v7) % 83.92/11.73 | visFreeVar(v4, v3)) % 83.92/11.74 (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 83.92/11.74 (v1 = v0 | ~ (vabs(v4, v3, v2) = v1) | ~ (vabs(v4, v3, v2) = v0)) % 83.92/11.74 (24) all_63_33 = all_55_5 % 83.92/11.74 (25) $i(all_63_32) % 83.92/11.74 (26) vsubst(all_55_7, all_55_6, all_63_23) = all_55_0 % 83.92/11.74 (27) vapp(all_63_29, all_63_28) = all_63_27 % 83.92/11.74 (28) $i(all_55_2) % 83.92/11.74 (29) $i(all_55_7) % 83.92/11.74 (30) $i(all_63_27) % 83.92/11.74 (31) $i(all_55_4) % 83.92/11.74 (32) ! [v0: $i] : ! [v1: $i] : ( ~ (vgensym(v1) = v0) | ~ $i(v1) | ~ % 83.92/11.74 $i(v0) | ~ visFreeVar(v0, v1)) % 83.92/11.74 (33) all_63_31 = veabs % 83.92/11.74 (34) vbind(all_55_7, all_55_9, all_55_8) = all_55_2 % 83.92/11.74 (35) ~ (all_63_32 = all_55_7) % 83.92/11.74 (36) vabs(all_55_5, all_55_4, veabs) = all_55_1 % 83.92/11.74 (37) $i(all_55_9) % 83.92/11.74 % 83.92/11.74 Begin of proof % 83.92/11.74 | % 83.92/11.74 | BETA: splitting (20) gives: % 83.92/11.74 | % 83.92/11.74 | Case 1: % 83.92/11.74 | | % 83.92/11.74 | | (38) visFreeVar(all_63_32, all_63_31) % 83.92/11.74 | | % 83.92/11.74 | | REDUCE: (33), (38) imply: % 83.92/11.74 | | (39) visFreeVar(all_63_32, veabs) % 83.92/11.74 | | % 83.92/11.74 | | GROUND_INST: instantiating (8) with all_55_6, all_55_7, all_63_32, veabs, % 83.92/11.74 | | all_63_29, all_63_28, all_63_27, simplifying with (3), (12), % 83.92/11.74 | | (16), (17), (18), (25), (27), (29), (39) gives: % 83.92/11.74 | | (40) $false % 83.92/11.74 | | % 83.92/11.74 | | CLOSE: (40) is inconsistent. % 83.92/11.74 | | % 83.92/11.74 | Case 2: % 83.92/11.74 | | % 83.92/11.74 | | (41) ? [v0: $i] : (vabs(all_63_33, all_63_34, all_63_31) = v0 & $i(v0) & % 83.92/11.74 | | valphaEquivalent(v0, all_63_23)) % 83.92/11.74 | | % 83.92/11.74 | | DELTA: instantiating (41) with fresh symbol all_195_0 gives: % 83.92/11.74 | | (42) vabs(all_63_33, all_63_34, all_63_31) = all_195_0 & $i(all_195_0) & % 83.92/11.74 | | valphaEquivalent(all_195_0, all_63_23) % 83.92/11.74 | | % 83.92/11.74 | | ALPHA: (42) implies: % 83.92/11.74 | | (43) valphaEquivalent(all_195_0, all_63_23) % 83.92/11.74 | | (44) $i(all_195_0) % 83.92/11.74 | | (45) vabs(all_63_33, all_63_34, all_63_31) = all_195_0 % 83.92/11.74 | | % 83.92/11.74 | | REDUCE: (13), (24), (33), (45) imply: % 83.92/11.74 | | (46) vabs(all_55_5, all_55_4, veabs) = all_195_0 % 83.92/11.74 | | % 83.92/11.74 | | GROUND_INST: instantiating (23) with all_55_1, all_195_0, veabs, all_55_4, % 83.92/11.74 | | all_55_5, simplifying with (36), (46) gives: % 83.92/11.74 | | (47) all_195_0 = all_55_1 % 83.92/11.74 | | % 83.92/11.74 | | REDUCE: (44), (47) imply: % 83.92/11.74 | | (48) $i(all_55_1) % 83.92/11.74 | | % 83.92/11.74 | | REDUCE: (43), (47) imply: % 83.92/11.74 | | (49) valphaEquivalent(all_55_1, all_63_23) % 83.92/11.74 | | % 83.92/11.74 | | GROUND_INST: instantiating (9) with all_55_1, all_55_2, all_63_23, all_55_3, % 83.92/11.74 | | simplifying with (11), (14), (21), (28), (48), (49) gives: % 83.92/11.74 | | (50) vtcheck(all_55_2, all_63_23, all_55_3) % 83.92/11.74 | | % 83.92/11.74 | | GROUND_INST: instantiating (22) with all_55_9, all_55_8, all_55_7, all_55_6, % 83.92/11.74 | | all_63_32, all_55_4, all_63_24, all_55_3, all_55_2, all_63_23, % 83.92/11.74 | | all_55_0, simplifying with (1), (2), (6), (14), (15), (16), % 83.92/11.74 | | (19), (25), (26), (29), (31), (34), (37), (50) gives: % 83.92/11.74 | | (51) all_63_32 = all_55_7 | visFreeVar(all_63_32, all_55_6) % 83.92/11.74 | | % 83.92/11.74 | | BETA: splitting (51) gives: % 83.92/11.74 | | % 83.92/11.74 | | Case 1: % 83.92/11.74 | | | % 83.92/11.74 | | | (52) visFreeVar(all_63_32, all_55_6) % 83.92/11.74 | | | % 83.92/11.74 | | | BETA: splitting (10) gives: % 83.92/11.74 | | | % 83.92/11.74 | | | Case 1: % 83.92/11.74 | | | | % 83.92/11.74 | | | | (53) ~ visFreeVar(all_63_32, all_55_6) % 83.92/11.74 | | | | % 83.92/11.74 | | | | PRED_UNIFY: (52), (53) imply: % 83.92/11.74 | | | | (54) $false % 83.92/11.74 | | | | % 83.92/11.74 | | | | CLOSE: (54) is inconsistent. % 83.92/11.74 | | | | % 83.92/11.74 | | | Case 2: % 83.92/11.74 | | | | % 83.92/11.74 | | | | (55) visFreeVar(all_63_32, all_63_29) % 83.92/11.74 | | | | % 83.92/11.74 | | | | GROUND_INST: instantiating (5) with all_63_32, all_63_27, all_63_29, % 83.92/11.74 | | | | all_63_28, simplifying with (4), (7), (25), (27), (30), % 83.92/11.74 | | | | (55) gives: % 83.92/11.74 | | | | (56) visFreeVar(all_63_32, all_63_27) % 83.92/11.74 | | | | % 83.92/11.74 | | | | GROUND_INST: instantiating (32) with all_63_32, all_63_27, simplifying % 83.92/11.74 | | | | with (12), (25), (30), (56) gives: % 83.92/11.74 | | | | (57) $false % 83.92/11.74 | | | | % 83.92/11.74 | | | | CLOSE: (57) is inconsistent. % 83.92/11.74 | | | | % 83.92/11.74 | | | End of split % 83.92/11.74 | | | % 83.92/11.74 | | Case 2: % 83.92/11.74 | | | % 83.92/11.74 | | | (58) all_63_32 = all_55_7 % 83.92/11.74 | | | % 83.92/11.74 | | | REDUCE: (35), (58) imply: % 83.92/11.74 | | | (59) $false % 83.92/11.74 | | | % 83.92/11.74 | | | CLOSE: (59) is inconsistent. % 83.92/11.74 | | | % 83.92/11.74 | | End of split % 83.92/11.74 | | % 83.92/11.74 | End of split % 83.92/11.74 | % 83.92/11.74 End of proof % 83.92/11.74 % SZS output end Proof for theBenchmark % 83.92/11.74 % 83.92/11.74 11118ms %------------------------------------------------------------------------------