%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM132+1 : TPTP v8.1.2. Released v6.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n020.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 84.26s 11.69s % Output : Proof 85.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : COM132+1 : TPTP v8.1.2. Released v6.4.0. % 0.10/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n020.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Aug 29 13:30:13 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.60 ________ _____ % 0.19/0.60 ___ __ \_________(_)________________________________ % 0.19/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.60 % 0.19/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.60 (2023-06-19) % 0.19/0.60 % 0.19/0.60 (c) Philipp Rümmer, 2009-2023 % 0.19/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.60 Amanda Stjerna. % 0.19/0.60 Free software under BSD-3-Clause. % 0.19/0.60 % 0.19/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.60 % 0.19/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.61 Running up to 7 provers in parallel. % 0.19/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.80/1.53 Prover 4: Preprocessing ... % 5.80/1.54 Prover 1: Preprocessing ... % 5.80/1.54 Prover 5: Preprocessing ... % 5.80/1.54 Prover 3: Preprocessing ... % 5.80/1.54 Prover 0: Preprocessing ... % 5.80/1.54 Prover 6: Preprocessing ... % 6.31/1.55 Prover 2: Preprocessing ... % 12.26/2.39 Prover 1: Constructing countermodel ... % 12.26/2.42 Prover 3: Constructing countermodel ... % 13.02/2.43 Prover 6: Proving ... % 13.02/2.43 Prover 5: Proving ... % 13.02/2.43 Prover 0: Proving ... % 13.02/2.51 Prover 4: Constructing countermodel ... % 13.02/2.55 Prover 2: Proving ... % 73.50/10.30 Prover 2: stopped % 73.50/10.30 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 74.44/10.43 Prover 7: Preprocessing ... % 76.20/10.64 Prover 7: Warning: ignoring some quantifiers % 76.20/10.66 Prover 7: Constructing countermodel ... % 84.26/11.67 Prover 7: Found proof (size 153) % 84.26/11.68 Prover 7: proved (1373ms) % 84.26/11.68 Prover 3: stopped % 84.26/11.68 Prover 6: stopped % 84.26/11.68 Prover 4: stopped % 84.26/11.68 Prover 0: stopped % 84.26/11.68 Prover 5: stopped % 84.26/11.69 Prover 1: stopped % 84.26/11.69 % 84.26/11.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 84.26/11.69 % 84.26/11.70 % SZS output start Proof for theBenchmark % 84.26/11.70 Assumptions after simplification: % 84.26/11.70 --------------------------------- % 84.26/11.70 % 84.26/11.70 (EQ-abs) % 84.54/11.73 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 84.54/11.73 $i] : ! [v6: $i] : (v5 = v2 | ~ (vabs(v3, v4, v5) = v6) | ~ (vabs(v0, v1, % 84.54/11.73 v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 84.54/11.73 ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 84.54/11.73 $i] : ! [v5: $i] : ! [v6: $i] : (v4 = v1 | ~ (vabs(v3, v4, v5) = v6) | ~ % 84.54/11.73 (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 84.54/11.73 $i(v1) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 84.54/11.73 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v3 = v0 | ~ (vabs(v3, v4, v5) = % 84.54/11.73 v6) | ~ (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 84.54/11.73 $i(v2) | ~ $i(v1) | ~ $i(v0)) % 84.54/11.73 % 84.54/11.74 (T-Strong) % 84.54/11.74 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 84.54/11.74 $i] : ( ~ (vbind(v0, v1, v2) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 84.54/11.74 $i(v1) | ~ $i(v0) | ~ vtcheck(v5, v3, v4) | vtcheck(v2, v3, v4) | % 84.54/11.74 visFreeVar(v0, v3)) % 84.54/11.74 % 84.54/11.74 (T-subst-abs-2-gen) % 84.54/11.74 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 84.54/11.74 $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : % 84.54/11.74 (v4 = v2 | ~ (vsubst(v2, v3, v9) = v10) | ~ (vbind(v2, v0, v1) = v8) | ~ % 84.54/11.74 (vabs(v4, v5, v6) = v9) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 84.54/11.74 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ vtcheck(v8, v9, v7) | ~ % 84.54/11.74 vtcheck(v1, v3, v0) | vtcheck(v1, v10, v7) | visFreeVar(v4, v3)) % 84.54/11.74 % 84.54/11.74 (T-subst-abs-3) % 84.54/11.74 $i(veabs) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: % 84.54/11.74 $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 84.54/11.74 ( ~ (v4 = v2) & vsubst(v2, v3, v8) = v9 & vbind(v2, v0, v1) = v7 & vabs(v4, % 84.54/11.74 v5, veabs) = v8 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 84.54/11.74 $i(v3) & $i(v2) & $i(v1) & $i(v0) & vtcheck(v7, v8, v6) & vtcheck(v1, v3, % 84.54/11.74 v0) & visFreeVar(v4, v3) & ~ vtcheck(v1, v9, v6)) % 84.54/11.74 % 84.54/11.74 (alpha-equiv-subst-abs) % 84.54/11.74 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 84.54/11.74 $i] : ! [v6: $i] : ( ~ (vsubst(v1, v4, v3) = v5) | ~ (vabs(v2, v0, v5) = % 84.54/11.74 v6) | ~ (vvar(v2) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 84.54/11.74 visFreeVar(v2, v3) | ? [v7: $i] : (vabs(v1, v0, v3) = v7 & $i(v7) & % 84.54/11.74 valphaEquivalent(v7, v6))) % 84.54/11.74 % 84.54/11.74 (alpha-equiv-typing) % 84.54/11.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 84.54/11.75 | ~ $i(v1) | ~ $i(v0) | ~ valphaEquivalent(v0, v2) | ~ vtcheck(v1, v0, % 84.54/11.75 v3) | vtcheck(v1, v2, v3)) % 84.54/11.75 % 84.54/11.75 (fresh-free-2) % 84.54/11.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 84.54/11.75 $i] : ! [v6: $i] : ( ~ (vgensym(v6) = v2) | ~ (vapp(v4, v5) = v6) | ~ % 84.54/11.75 (vapp(v0, v3) = v4) | ~ (vvar(v1) = v5) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 84.54/11.75 | ~ $i(v0) | ~ visFreeVar(v2, v3)) % 84.54/11.75 % 84.54/11.75 (fresh-unequal-var-3) % 84.54/11.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 84.54/11.75 $i] : ( ~ (vgensym(v5) = v2) | ~ (vapp(v3, v4) = v5) | ~ (vapp(v0, v1) = % 84.54/11.75 v3) | ~ (vvar(v2) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) % 84.54/11.75 % 84.54/11.75 (gensym-is-fresh) % 84.54/11.75 ! [v0: $i] : ! [v1: $i] : ( ~ (vgensym(v1) = v0) | ~ $i(v1) | ~ $i(v0) | % 84.54/11.75 ~ visFreeVar(v0, v1)) % 84.54/11.75 % 84.54/11.75 (isFreeVar1) % 84.54/11.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = v1 % 84.54/11.75 | ~ (vabs(v3, v0, v4) = v2) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 84.54/11.75 | ~ $i(v0) | ~ visFreeVar(v1, v4) | visFreeVar(v1, v2)) & ! [v0: $i] : ! % 84.54/11.75 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (vabs(v3, v0, v4) = % 84.54/11.75 v2) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 84.54/11.75 visFreeVar(v1, v2) | visFreeVar(v1, v4)) & ! [v0: $i] : ! [v1: $i] : ! % 84.54/11.75 [v2: $i] : ! [v3: $i] : ( ~ (vabs(v1, v0, v3) = v2) | ~ $i(v3) | ~ $i(v2) | % 84.54/11.75 ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v1, v2)) % 84.54/11.75 % 84.54/11.75 (isFreeVar2) % 84.68/11.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, v3) = % 84.68/11.75 v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v0, % 84.68/11.75 v3) | visFreeVar(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 84.68/11.75 [v3: $i] : ( ~ (vapp(v2, v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 84.68/11.75 $i(v0) | ~ visFreeVar(v0, v2) | visFreeVar(v0, v1)) & ! [v0: $i] : ! [v1: % 84.68/11.75 $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, v3) = v1) | ~ $i(v3) | ~ % 84.68/11.75 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v0, v1) | visFreeVar(v0, v3) % 84.68/11.75 | visFreeVar(v0, v2)) % 84.68/11.75 % 84.68/11.75 (isValue0) % 84.68/11.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vabs(v0, v1, v2) % 84.68/11.75 = v3) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | visValue(v3)) % 84.68/11.75 % 84.68/11.75 (isValue1) % 84.68/11.75 ! [v0: $i] : ! [v1: $i] : ( ~ (vvar(v0) = v1) | ~ $i(v1) | ~ $i(v0) | ~ % 84.68/11.75 visValue(v1)) % 84.68/11.75 % 84.68/11.75 (isValue2) % 84.68/11.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (vapp(v0, v1) = v2) | ~ $i(v2) % 84.68/11.75 | ~ $i(v1) | ~ $i(v0) | ~ visValue(v2)) % 84.68/11.75 % 84.68/11.75 (subst-INV) % 84.68/11.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vsubst(v0, v1, % 84.68/11.76 v2) = v3) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] % 84.68/11.76 : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 84.68/11.76 [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? % 84.68/11.76 [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : ? [v19: $i] : ? % 84.68/11.76 [v20: $i] : ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? % 84.68/11.76 [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? [v28: $i] : ? [v29: $i] : ? % 84.68/11.76 [v30: $i] : ? [v31: $i] : ? [v32: $i] : ? [v33: $i] : ? [v34: $i] : ? % 84.68/11.76 [v35: $i] : ? [v36: $i] : ? [v37: $i] : ? [v38: $i] : ? [v39: $i] : ? % 84.68/11.76 [v40: $i] : ? [v41: $i] : ? [v42: $i] : ? [v43: $i] : ? [v44: $i] : ? % 84.68/11.76 [v45: $i] : ? [v46: $i] : ? [v47: $i] : ? [v48: $i] : ($i(v47) & $i(v46) % 84.68/11.76 & $i(v45) & $i(v43) & $i(v42) & $i(v41) & $i(v36) & $i(v35) & $i(v34) & % 84.68/11.76 $i(v33) & $i(v31) & $i(v30) & $i(v29) & $i(v28) & $i(v27) & $i(v17) & % 84.68/11.76 $i(v16) & $i(v15) & $i(v14) & $i(v13) & $i(v12) & $i(v8) & $i(v7) & $i(v6) % 84.68/11.76 & $i(v5) & $i(v4) & ((v48 = v2 & v47 = v1 & v46 = v0 & v45 = v0 & v3 = v1 % 84.68/11.76 & vvar(v0) = v2) | (v44 = v2 & v42 = v0 & v41 = v1 & v3 = v2 & ~ (v43 % 84.68/11.76 = v0) & vvar(v43) = v2) | (v40 = v3 & v37 = v2 & v35 = v1 & v34 = v0 % 84.68/11.76 & vsubst(v0, v1, v36) = v39 & vsubst(v0, v1, v33) = v38 & vapp(v38, % 84.68/11.76 v39) = v3 & vapp(v33, v36) = v2 & $i(v39) & $i(v38)) | (v32 = v2 & % 84.68/11.76 v29 = v0 & v28 = v0 & v27 = v1 & v3 = v2 & vabs(v0, v30, v31) = v2) | % 84.68/11.76 (v26 = v3 & v22 = v16 & v18 = v2 & v13 = v1 & v12 = v0 & ~ (v15 = v0) & % 84.68/11.76 vsubst(v15, v23, v17) = v24 & vsubst(v0, v1, v25) = v3 & vgensym(v21) % 84.68/11.76 = v16 & vapp(v19, v20) = v21 & vapp(v1, v17) = v19 & vabs(v16, v14, % 84.68/11.76 v24) = v25 & vabs(v15, v14, v17) = v2 & vvar(v16) = v23 & vvar(v0) = % 84.68/11.76 v20 & $i(v25) & $i(v24) & $i(v23) & $i(v21) & $i(v20) & $i(v19) & % 84.68/11.76 visFreeVar(v15, v1)) | (v11 = v3 & v9 = v2 & v7 = v1 & v6 = v0 & ~ % 84.68/11.76 (v4 = v0) & vsubst(v0, v1, v8) = v10 & vabs(v4, v5, v10) = v3 & % 84.68/11.76 vabs(v4, v5, v8) = v2 & $i(v10) & ~ visFreeVar(v4, v1))))) % 84.68/11.76 % 84.68/11.76 (function-axioms) % 84.68/11.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 84.68/11.77 | ~ (vsubst(v4, v3, v2) = v1) | ~ (vsubst(v4, v3, v2) = v0)) & ! [v0: $i] % 84.68/11.77 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 84.68/11.77 (vbind(v4, v3, v2) = v1) | ~ (vbind(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 84.68/11.77 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (vabs(v4, % 84.68/11.77 v3, v2) = v1) | ~ (vabs(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 84.68/11.77 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (varrow(v3, v2) = v1) | ~ % 84.68/11.77 (varrow(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 84.68/11.77 $i] : (v1 = v0 | ~ (vlookup(v3, v2) = v1) | ~ (vlookup(v3, v2) = v0)) & ! % 84.68/11.77 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (vapp(v3, % 84.68/11.77 v2) = v1) | ~ (vapp(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 84.68/11.77 [v2: $i] : (v1 = v0 | ~ (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) & ! [v0: % 84.68/11.77 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (vgetSomeExp(v2) = v1) | ~ % 84.68/11.77 (vgetSomeExp(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 84.68/11.77 | ~ (vsomeExp(v2) = v1) | ~ (vsomeExp(v2) = v0)) & ! [v0: $i] : ! [v1: % 84.68/11.77 $i] : ! [v2: $i] : (v1 = v0 | ~ (vgensym(v2) = v1) | ~ (vgensym(v2) = % 84.68/11.77 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 84.68/11.77 (vgetSomeType(v2) = v1) | ~ (vgetSomeType(v2) = v0)) & ! [v0: $i] : ! % 84.68/11.77 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (vsomeType(v2) = v1) | ~ % 84.68/11.77 (vsomeType(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 84.68/11.77 ~ (vvar(v2) = v1) | ~ (vvar(v2) = v0)) % 84.68/11.77 % 84.68/11.77 Further assumptions not needed in the proof: % 84.68/11.77 -------------------------------------------- % 84.68/11.77 DIFF-abs-app, DIFF-empty-bind, DIFF-noExp-someExp, DIFF-noType-someType, % 84.68/11.77 DIFF-var-abs, DIFF-var-app, EQ-app, EQ-arrow, EQ-bind, EQ-empty, EQ-noExp, % 84.68/11.77 EQ-noType, EQ-someExp, EQ-someType, EQ-var, T-Context-Duplicate, T-Context-Swap, % 84.68/11.77 T-Weak, T-Weak-FreeVar, T-abs, T-app, T-inv, T-var, alpha-equiv-FreeVar, % 84.68/11.77 alpha-equiv-refl, alpha-equiv-sym, alpha-equiv-trans, getSomeExp0, getSomeType0, % 84.68/11.77 isFreeVar0, isSomeExp0, isSomeExp1, isSomeType0, isSomeType1, lookup-INV, % 84.68/11.77 lookup0, lookup1, lookup2, reduce-INV, reduce0, reduce1, reduce2, reduce3, % 84.68/11.77 reduce4, reduce5, reduce6, subst0, subst1, subst2, subst3, subst4, subst5 % 84.68/11.77 % 84.68/11.77 Those formulas are unsatisfiable: % 84.68/11.77 --------------------------------- % 84.68/11.77 % 84.68/11.77 Begin of proof % 84.68/11.77 | % 84.68/11.77 | ALPHA: (EQ-abs) implies: % 84.68/11.77 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 84.68/11.77 | ! [v5: $i] : ! [v6: $i] : (v3 = v0 | ~ (vabs(v3, v4, v5) = v6) | ~ % 84.68/11.77 | (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 84.68/11.77 | $i(v2) | ~ $i(v1) | ~ $i(v0)) % 84.68/11.77 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 84.68/11.77 | ! [v5: $i] : ! [v6: $i] : (v4 = v1 | ~ (vabs(v3, v4, v5) = v6) | ~ % 84.68/11.77 | (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 84.68/11.77 | $i(v2) | ~ $i(v1) | ~ $i(v0)) % 84.68/11.77 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 84.68/11.77 | ! [v5: $i] : ! [v6: $i] : (v5 = v2 | ~ (vabs(v3, v4, v5) = v6) | ~ % 84.68/11.77 | (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 84.68/11.77 | $i(v2) | ~ $i(v1) | ~ $i(v0)) % 84.68/11.77 | % 84.68/11.77 | ALPHA: (isFreeVar1) implies: % 84.68/11.77 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vabs(v1, % 84.68/11.77 | v0, v3) = v2) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 84.68/11.77 | ~ visFreeVar(v1, v2)) % 84.68/11.77 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 84.68/11.77 | ~ (vabs(v3, v0, v4) = v2) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 84.68/11.77 | $i(v1) | ~ $i(v0) | ~ visFreeVar(v1, v2) | visFreeVar(v1, v4)) % 84.68/11.77 | % 84.68/11.77 | ALPHA: (isFreeVar2) implies: % 84.68/11.77 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, % 84.68/11.77 | v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 84.68/11.77 | visFreeVar(v0, v2) | visFreeVar(v0, v1)) % 84.68/11.78 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, % 84.68/11.78 | v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 84.68/11.78 | visFreeVar(v0, v3) | visFreeVar(v0, v1)) % 84.68/11.78 | % 84.68/11.78 | ALPHA: (T-subst-abs-3) implies: % 84.68/11.78 | (8) $i(veabs) % 84.68/11.78 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 84.68/11.78 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ( % 84.68/11.78 | ~ (v4 = v2) & vsubst(v2, v3, v8) = v9 & vbind(v2, v0, v1) = v7 & % 84.68/11.78 | vabs(v4, v5, veabs) = v8 & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) % 84.68/11.78 | & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & vtcheck(v7, v8, v6) & % 84.68/11.78 | vtcheck(v1, v3, v0) & visFreeVar(v4, v3) & ~ vtcheck(v1, v9, v6)) % 84.68/11.78 | % 84.68/11.78 | ALPHA: (function-axioms) implies: % 84.68/11.78 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 84.68/11.78 | (v1 = v0 | ~ (vabs(v4, v3, v2) = v1) | ~ (vabs(v4, v3, v2) = v0)) % 84.68/11.78 | % 84.68/11.78 | DELTA: instantiating (9) with fresh symbols all_68_0, all_68_1, all_68_2, % 84.68/11.78 | all_68_3, all_68_4, all_68_5, all_68_6, all_68_7, all_68_8, all_68_9 % 84.68/11.78 | gives: % 84.68/11.78 | (11) ~ (all_68_5 = all_68_7) & vsubst(all_68_7, all_68_6, all_68_1) = % 84.68/11.78 | all_68_0 & vbind(all_68_7, all_68_9, all_68_8) = all_68_2 & % 84.68/11.78 | vabs(all_68_5, all_68_4, veabs) = all_68_1 & $i(all_68_0) & % 84.68/11.78 | $i(all_68_1) & $i(all_68_2) & $i(all_68_3) & $i(all_68_4) & % 84.68/11.78 | $i(all_68_5) & $i(all_68_6) & $i(all_68_7) & $i(all_68_8) & % 84.68/11.78 | $i(all_68_9) & vtcheck(all_68_2, all_68_1, all_68_3) & % 84.68/11.78 | vtcheck(all_68_8, all_68_6, all_68_9) & visFreeVar(all_68_5, all_68_6) % 84.68/11.78 | & ~ vtcheck(all_68_8, all_68_0, all_68_3) % 84.68/11.78 | % 84.68/11.78 | ALPHA: (11) implies: % 84.68/11.78 | (12) ~ (all_68_5 = all_68_7) % 84.68/11.78 | (13) ~ vtcheck(all_68_8, all_68_0, all_68_3) % 84.68/11.78 | (14) vtcheck(all_68_8, all_68_6, all_68_9) % 84.68/11.78 | (15) vtcheck(all_68_2, all_68_1, all_68_3) % 84.68/11.78 | (16) $i(all_68_9) % 84.68/11.78 | (17) $i(all_68_8) % 84.68/11.78 | (18) $i(all_68_7) % 84.68/11.78 | (19) $i(all_68_6) % 84.68/11.78 | (20) $i(all_68_5) % 84.68/11.78 | (21) $i(all_68_4) % 84.68/11.78 | (22) $i(all_68_3) % 84.68/11.78 | (23) $i(all_68_2) % 84.68/11.78 | (24) $i(all_68_1) % 84.68/11.78 | (25) $i(all_68_0) % 84.68/11.78 | (26) vabs(all_68_5, all_68_4, veabs) = all_68_1 % 84.68/11.78 | (27) vbind(all_68_7, all_68_9, all_68_8) = all_68_2 % 84.68/11.78 | (28) vsubst(all_68_7, all_68_6, all_68_1) = all_68_0 % 84.68/11.78 | % 84.68/11.78 | GROUND_INST: instantiating (isValue0) with all_68_5, all_68_4, veabs, % 84.68/11.78 | all_68_1, simplifying with (8), (20), (21), (24), (26) gives: % 84.68/11.78 | (29) visValue(all_68_1) % 84.68/11.78 | % 84.68/11.78 | GROUND_INST: instantiating (T-Strong) with all_68_7, all_68_9, all_68_8, % 84.68/11.78 | all_68_1, all_68_3, all_68_2, simplifying with (15), (16), (17), % 84.68/11.78 | (18), (22), (24), (27) gives: % 84.68/11.78 | (30) vtcheck(all_68_8, all_68_1, all_68_3) | visFreeVar(all_68_7, all_68_1) % 84.68/11.78 | % 84.68/11.78 | GROUND_INST: instantiating (subst-INV) with all_68_7, all_68_6, all_68_1, % 84.68/11.78 | all_68_0, simplifying with (18), (19), (24), (25), (28) gives: % 84.68/11.79 | (31) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 84.68/11.79 | ? [v5: int] : ? [v6: $i] : ? [v7: int] : ? [v8: $i] : ? [v9: $i] : % 84.68/11.79 | ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: % 84.68/11.79 | int] : ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : % 84.68/11.79 | ? [v19: $i] : ? [v20: $i] : ? [v21: $i] : ? [v22: int] : ? [v23: % 84.68/11.79 | $i] : ? [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? % 84.68/11.79 | [v28: int] : ? [v29: $i] : ? [v30: $i] : ? [v31: $i] : ? [v32: $i] % 84.68/11.79 | : ? [v33: int] : ? [v34: $i] : ? [v35: $i] : ? [v36: int] : ? % 84.68/11.79 | [v37: $i] : ? [v38: $i] : ? [v39: $i] : ? [v40: int] : ? [v41: $i] % 84.68/11.79 | : ? [v42: $i] : ? [v43: $i] : ? [v44: int] : ($i(v43) & $i(v42) & % 84.68/11.79 | $i(v41) & $i(v39) & $i(v38) & $i(v37) & $i(v32) & $i(v31) & $i(v30) % 84.68/11.79 | & $i(v29) & $i(v27) & $i(v26) & $i(v25) & $i(v24) & $i(v23) & % 84.68/11.79 | $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v4) & % 84.68/11.79 | $i(v3) & $i(v2) & $i(v1) & $i(v0) & ((v44 = all_68_1 & v43 = % 84.68/11.79 | all_68_6 & v42 = all_68_7 & v41 = all_68_7 & all_68_0 = all_68_6 % 84.68/11.79 | & vvar(all_68_7) = all_68_1) | (v40 = all_68_1 & v38 = all_68_7 % 84.68/11.79 | & v37 = all_68_6 & all_68_0 = all_68_1 & ~ (v39 = all_68_7) & % 84.68/11.79 | vvar(v39) = all_68_1) | (v36 = all_68_0 & v33 = all_68_1 & v31 = % 84.68/11.79 | all_68_6 & v30 = all_68_7 & vsubst(all_68_7, all_68_6, v32) = % 84.68/11.79 | v35 & vsubst(all_68_7, all_68_6, v29) = v34 & vapp(v34, v35) = % 84.68/11.79 | all_68_0 & vapp(v29, v32) = all_68_1 & $i(v35) & $i(v34)) | (v28 % 84.68/11.79 | = all_68_1 & v25 = all_68_7 & v24 = all_68_7 & v23 = all_68_6 & % 84.68/11.79 | all_68_0 = all_68_1 & vabs(all_68_7, v26, v27) = all_68_1) | % 84.68/11.79 | (v22 = all_68_0 & v18 = v12 & v14 = all_68_1 & v9 = all_68_6 & v8 % 84.68/11.79 | = all_68_7 & ~ (v11 = all_68_7) & vsubst(v11, v19, v13) = v20 & % 84.68/11.79 | vsubst(all_68_7, all_68_6, v21) = all_68_0 & vgensym(v17) = v12 % 84.68/11.79 | & vapp(v15, v16) = v17 & vapp(all_68_6, v13) = v15 & vabs(v12, % 84.68/11.79 | v10, v20) = v21 & vabs(v11, v10, v13) = all_68_1 & vvar(v12) = % 84.68/11.79 | v19 & vvar(all_68_7) = v16 & $i(v21) & $i(v20) & $i(v19) & % 84.68/11.79 | $i(v17) & $i(v16) & $i(v15) & visFreeVar(v11, all_68_6)) | (v7 = % 84.68/11.79 | all_68_0 & v5 = all_68_1 & v3 = all_68_6 & v2 = all_68_7 & ~ % 84.68/11.79 | (v0 = all_68_7) & vsubst(all_68_7, all_68_6, v4) = v6 & vabs(v0, % 84.68/11.79 | v1, v6) = all_68_0 & vabs(v0, v1, v4) = all_68_1 & $i(v6) & ~ % 84.68/11.79 | visFreeVar(v0, all_68_6)))) % 84.68/11.79 | % 84.68/11.79 | DELTA: instantiating (31) with fresh symbols all_78_0, all_78_1, all_78_2, % 84.68/11.79 | all_78_3, all_78_4, all_78_5, all_78_6, all_78_7, all_78_8, all_78_9, % 84.68/11.79 | all_78_10, all_78_11, all_78_12, all_78_13, all_78_14, all_78_15, % 84.68/11.79 | all_78_16, all_78_17, all_78_18, all_78_19, all_78_20, all_78_21, % 84.68/11.79 | all_78_22, all_78_23, all_78_24, all_78_25, all_78_26, all_78_27, % 84.68/11.79 | all_78_28, all_78_29, all_78_30, all_78_31, all_78_32, all_78_33, % 84.68/11.79 | all_78_34, all_78_35, all_78_36, all_78_37, all_78_38, all_78_39, % 84.68/11.79 | all_78_40, all_78_41, all_78_42, all_78_43, all_78_44 gives: % 84.68/11.80 | (32) $i(all_78_1) & $i(all_78_2) & $i(all_78_3) & $i(all_78_5) & % 84.68/11.80 | $i(all_78_6) & $i(all_78_7) & $i(all_78_12) & $i(all_78_13) & % 84.68/11.80 | $i(all_78_14) & $i(all_78_15) & $i(all_78_17) & $i(all_78_18) & % 84.68/11.80 | $i(all_78_19) & $i(all_78_20) & $i(all_78_21) & $i(all_78_31) & % 84.68/11.80 | $i(all_78_32) & $i(all_78_33) & $i(all_78_34) & $i(all_78_35) & % 84.68/11.80 | $i(all_78_36) & $i(all_78_40) & $i(all_78_41) & $i(all_78_42) & % 84.68/11.80 | $i(all_78_43) & $i(all_78_44) & ((all_78_0 = all_68_1 & all_78_1 = % 84.68/11.80 | all_68_6 & all_78_2 = all_68_7 & all_78_3 = all_68_7 & all_68_0 = % 84.68/11.80 | all_68_6 & vvar(all_68_7) = all_68_1) | (all_78_4 = all_68_1 & % 84.68/11.80 | all_78_6 = all_68_7 & all_78_7 = all_68_6 & all_68_0 = all_68_1 & % 84.68/11.80 | ~ (all_78_5 = all_68_7) & vvar(all_78_5) = all_68_1) | (all_78_8 = % 84.68/11.80 | all_68_0 & all_78_11 = all_68_1 & all_78_13 = all_68_6 & all_78_14 % 84.68/11.80 | = all_68_7 & vsubst(all_68_7, all_68_6, all_78_12) = all_78_9 & % 84.68/11.80 | vsubst(all_68_7, all_68_6, all_78_15) = all_78_10 & % 84.68/11.80 | vapp(all_78_10, all_78_9) = all_68_0 & vapp(all_78_15, all_78_12) % 84.68/11.80 | = all_68_1 & $i(all_78_9) & $i(all_78_10)) | (all_78_16 = all_68_1 % 84.68/11.80 | & all_78_19 = all_68_7 & all_78_20 = all_68_7 & all_78_21 = % 84.68/11.80 | all_68_6 & all_68_0 = all_68_1 & vabs(all_68_7, all_78_18, % 84.68/11.80 | all_78_17) = all_68_1) | (all_78_22 = all_68_0 & all_78_26 = % 84.68/11.80 | all_78_32 & all_78_30 = all_68_1 & all_78_35 = all_68_6 & % 84.68/11.80 | all_78_36 = all_68_7 & ~ (all_78_33 = all_68_7) & % 84.68/11.80 | vsubst(all_78_33, all_78_25, all_78_31) = all_78_24 & % 84.68/11.80 | vsubst(all_68_7, all_68_6, all_78_23) = all_68_0 & % 84.68/11.80 | vgensym(all_78_27) = all_78_32 & vapp(all_78_29, all_78_28) = % 84.68/11.80 | all_78_27 & vapp(all_68_6, all_78_31) = all_78_29 & % 84.68/11.80 | vabs(all_78_32, all_78_34, all_78_24) = all_78_23 & % 84.68/11.80 | vabs(all_78_33, all_78_34, all_78_31) = all_68_1 & vvar(all_78_32) % 84.68/11.80 | = all_78_25 & vvar(all_68_7) = all_78_28 & $i(all_78_23) & % 84.68/11.80 | $i(all_78_24) & $i(all_78_25) & $i(all_78_27) & $i(all_78_28) & % 84.68/11.80 | $i(all_78_29) & visFreeVar(all_78_33, all_68_6)) | (all_78_37 = % 84.68/11.80 | all_68_0 & all_78_39 = all_68_1 & all_78_41 = all_68_6 & all_78_42 % 84.68/11.80 | = all_68_7 & ~ (all_78_44 = all_68_7) & vsubst(all_68_7, % 84.68/11.80 | all_68_6, all_78_40) = all_78_38 & vabs(all_78_44, all_78_43, % 84.68/11.80 | all_78_38) = all_68_0 & vabs(all_78_44, all_78_43, all_78_40) = % 84.68/11.80 | all_68_1 & $i(all_78_38) & ~ visFreeVar(all_78_44, all_68_6))) % 84.68/11.80 | % 84.68/11.80 | ALPHA: (32) implies: % 84.68/11.80 | (33) $i(all_78_44) % 84.68/11.80 | (34) $i(all_78_43) % 84.68/11.80 | (35) $i(all_78_42) % 84.68/11.80 | (36) $i(all_78_41) % 84.68/11.80 | (37) $i(all_78_40) % 84.68/11.80 | (38) $i(all_78_36) % 84.68/11.80 | (39) $i(all_78_35) % 84.68/11.80 | (40) $i(all_78_34) % 84.68/11.80 | (41) $i(all_78_33) % 84.68/11.80 | (42) $i(all_78_32) % 84.68/11.80 | (43) $i(all_78_31) % 84.68/11.80 | (44) $i(all_78_20) % 84.68/11.80 | (45) $i(all_78_18) % 84.68/11.80 | (46) $i(all_78_17) % 84.68/11.80 | (47) $i(all_78_15) % 84.68/11.80 | (48) $i(all_78_12) % 84.68/11.80 | (49) $i(all_78_5) % 84.68/11.80 | (50) $i(all_78_3) % 84.68/11.80 | (51) (all_78_0 = all_68_1 & all_78_1 = all_68_6 & all_78_2 = all_68_7 & % 84.68/11.80 | all_78_3 = all_68_7 & all_68_0 = all_68_6 & vvar(all_68_7) = % 84.68/11.80 | all_68_1) | (all_78_4 = all_68_1 & all_78_6 = all_68_7 & all_78_7 = % 84.68/11.80 | all_68_6 & all_68_0 = all_68_1 & ~ (all_78_5 = all_68_7) & % 84.68/11.80 | vvar(all_78_5) = all_68_1) | (all_78_8 = all_68_0 & all_78_11 = % 84.68/11.80 | all_68_1 & all_78_13 = all_68_6 & all_78_14 = all_68_7 & % 84.68/11.80 | vsubst(all_68_7, all_68_6, all_78_12) = all_78_9 & vsubst(all_68_7, % 84.68/11.80 | all_68_6, all_78_15) = all_78_10 & vapp(all_78_10, all_78_9) = % 84.68/11.80 | all_68_0 & vapp(all_78_15, all_78_12) = all_68_1 & $i(all_78_9) & % 84.68/11.80 | $i(all_78_10)) | (all_78_16 = all_68_1 & all_78_19 = all_68_7 & % 84.68/11.80 | all_78_20 = all_68_7 & all_78_21 = all_68_6 & all_68_0 = all_68_1 & % 84.68/11.80 | vabs(all_68_7, all_78_18, all_78_17) = all_68_1) | (all_78_22 = % 84.68/11.80 | all_68_0 & all_78_26 = all_78_32 & all_78_30 = all_68_1 & all_78_35 % 84.68/11.80 | = all_68_6 & all_78_36 = all_68_7 & ~ (all_78_33 = all_68_7) & % 84.68/11.80 | vsubst(all_78_33, all_78_25, all_78_31) = all_78_24 & % 84.68/11.80 | vsubst(all_68_7, all_68_6, all_78_23) = all_68_0 & % 84.68/11.80 | vgensym(all_78_27) = all_78_32 & vapp(all_78_29, all_78_28) = % 84.68/11.80 | all_78_27 & vapp(all_68_6, all_78_31) = all_78_29 & vabs(all_78_32, % 84.68/11.80 | all_78_34, all_78_24) = all_78_23 & vabs(all_78_33, all_78_34, % 84.68/11.80 | all_78_31) = all_68_1 & vvar(all_78_32) = all_78_25 & % 84.68/11.80 | vvar(all_68_7) = all_78_28 & $i(all_78_23) & $i(all_78_24) & % 84.68/11.80 | $i(all_78_25) & $i(all_78_27) & $i(all_78_28) & $i(all_78_29) & % 84.68/11.80 | visFreeVar(all_78_33, all_68_6)) | (all_78_37 = all_68_0 & all_78_39 % 84.68/11.80 | = all_68_1 & all_78_41 = all_68_6 & all_78_42 = all_68_7 & ~ % 84.68/11.80 | (all_78_44 = all_68_7) & vsubst(all_68_7, all_68_6, all_78_40) = % 84.68/11.80 | all_78_38 & vabs(all_78_44, all_78_43, all_78_38) = all_68_0 & % 84.68/11.80 | vabs(all_78_44, all_78_43, all_78_40) = all_68_1 & $i(all_78_38) & % 84.68/11.80 | ~ visFreeVar(all_78_44, all_68_6)) % 84.68/11.80 | % 84.68/11.80 | BETA: splitting (30) gives: % 84.68/11.80 | % 84.68/11.80 | Case 1: % 84.68/11.80 | | % 84.68/11.80 | | (52) vtcheck(all_68_8, all_68_1, all_68_3) % 84.68/11.80 | | % 84.68/11.80 | | PRED_UNIFY: (13), (52) imply: % 84.68/11.80 | | (53) ~ (all_68_0 = all_68_1) % 84.68/11.80 | | % 84.68/11.80 | | BETA: splitting (51) gives: % 84.68/11.80 | | % 84.68/11.80 | | Case 1: % 84.68/11.80 | | | % 84.68/11.80 | | | (54) (all_78_0 = all_68_1 & all_78_1 = all_68_6 & all_78_2 = all_68_7 & % 84.68/11.80 | | | all_78_3 = all_68_7 & all_68_0 = all_68_6 & vvar(all_68_7) = % 84.68/11.80 | | | all_68_1) | (all_78_4 = all_68_1 & all_78_6 = all_68_7 & % 84.68/11.80 | | | all_78_7 = all_68_6 & all_68_0 = all_68_1 & ~ (all_78_5 = % 84.68/11.80 | | | all_68_7) & vvar(all_78_5) = all_68_1) | (all_78_8 = all_68_0 % 84.68/11.80 | | | & all_78_11 = all_68_1 & all_78_13 = all_68_6 & all_78_14 = % 84.68/11.80 | | | all_68_7 & vsubst(all_68_7, all_68_6, all_78_12) = all_78_9 & % 84.68/11.80 | | | vsubst(all_68_7, all_68_6, all_78_15) = all_78_10 & % 84.68/11.80 | | | vapp(all_78_10, all_78_9) = all_68_0 & vapp(all_78_15, % 84.68/11.80 | | | all_78_12) = all_68_1 & $i(all_78_9) & $i(all_78_10)) % 84.68/11.80 | | | % 84.68/11.80 | | | BETA: splitting (54) gives: % 84.68/11.80 | | | % 84.68/11.80 | | | Case 1: % 84.68/11.80 | | | | % 84.68/11.80 | | | | (55) all_78_0 = all_68_1 & all_78_1 = all_68_6 & all_78_2 = all_68_7 % 84.68/11.80 | | | | & all_78_3 = all_68_7 & all_68_0 = all_68_6 & vvar(all_68_7) = % 84.68/11.80 | | | | all_68_1 % 84.68/11.80 | | | | % 84.68/11.80 | | | | ALPHA: (55) implies: % 84.68/11.80 | | | | (56) vvar(all_68_7) = all_68_1 % 84.68/11.80 | | | | % 84.68/11.80 | | | | GROUND_INST: instantiating (isValue1) with all_68_7, all_68_1, % 84.68/11.80 | | | | simplifying with (18), (24), (29), (56) gives: % 84.68/11.80 | | | | (57) $false % 84.68/11.81 | | | | % 84.68/11.81 | | | | CLOSE: (57) is inconsistent. % 84.68/11.81 | | | | % 84.68/11.81 | | | Case 2: % 84.68/11.81 | | | | % 84.68/11.81 | | | | (58) (all_78_4 = all_68_1 & all_78_6 = all_68_7 & all_78_7 = all_68_6 % 84.68/11.81 | | | | & all_68_0 = all_68_1 & ~ (all_78_5 = all_68_7) & % 84.68/11.81 | | | | vvar(all_78_5) = all_68_1) | (all_78_8 = all_68_0 & all_78_11 % 84.68/11.81 | | | | = all_68_1 & all_78_13 = all_68_6 & all_78_14 = all_68_7 & % 84.68/11.81 | | | | vsubst(all_68_7, all_68_6, all_78_12) = all_78_9 & % 84.68/11.81 | | | | vsubst(all_68_7, all_68_6, all_78_15) = all_78_10 & % 84.68/11.81 | | | | vapp(all_78_10, all_78_9) = all_68_0 & vapp(all_78_15, % 84.68/11.81 | | | | all_78_12) = all_68_1 & $i(all_78_9) & $i(all_78_10)) % 84.68/11.81 | | | | % 84.68/11.81 | | | | BETA: splitting (58) gives: % 84.68/11.81 | | | | % 84.68/11.81 | | | | Case 1: % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | (59) all_78_4 = all_68_1 & all_78_6 = all_68_7 & all_78_7 = % 84.68/11.81 | | | | | all_68_6 & all_68_0 = all_68_1 & ~ (all_78_5 = all_68_7) & % 84.68/11.81 | | | | | vvar(all_78_5) = all_68_1 % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | ALPHA: (59) implies: % 84.68/11.81 | | | | | (60) vvar(all_78_5) = all_68_1 % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | GROUND_INST: instantiating (isValue1) with all_78_5, all_68_1, % 84.68/11.81 | | | | | simplifying with (24), (29), (49), (60) gives: % 84.68/11.81 | | | | | (61) $false % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | CLOSE: (61) is inconsistent. % 84.68/11.81 | | | | | % 84.68/11.81 | | | | Case 2: % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | (62) all_78_8 = all_68_0 & all_78_11 = all_68_1 & all_78_13 = % 84.68/11.81 | | | | | all_68_6 & all_78_14 = all_68_7 & vsubst(all_68_7, all_68_6, % 84.68/11.81 | | | | | all_78_12) = all_78_9 & vsubst(all_68_7, all_68_6, % 84.68/11.81 | | | | | all_78_15) = all_78_10 & vapp(all_78_10, all_78_9) = % 84.68/11.81 | | | | | all_68_0 & vapp(all_78_15, all_78_12) = all_68_1 & % 84.68/11.81 | | | | | $i(all_78_9) & $i(all_78_10) % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | ALPHA: (62) implies: % 84.68/11.81 | | | | | (63) vapp(all_78_15, all_78_12) = all_68_1 % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | GROUND_INST: instantiating (isValue2) with all_78_15, all_78_12, % 84.68/11.81 | | | | | all_68_1, simplifying with (24), (29), (47), (48), (63) % 84.68/11.81 | | | | | gives: % 84.68/11.81 | | | | | (64) $false % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | CLOSE: (64) is inconsistent. % 84.68/11.81 | | | | | % 84.68/11.81 | | | | End of split % 84.68/11.81 | | | | % 84.68/11.81 | | | End of split % 84.68/11.81 | | | % 84.68/11.81 | | Case 2: % 84.68/11.81 | | | % 84.68/11.81 | | | (65) (all_78_16 = all_68_1 & all_78_19 = all_68_7 & all_78_20 = % 84.68/11.81 | | | all_68_7 & all_78_21 = all_68_6 & all_68_0 = all_68_1 & % 84.68/11.81 | | | vabs(all_68_7, all_78_18, all_78_17) = all_68_1) | (all_78_22 = % 84.68/11.81 | | | all_68_0 & all_78_26 = all_78_32 & all_78_30 = all_68_1 & % 84.68/11.81 | | | all_78_35 = all_68_6 & all_78_36 = all_68_7 & ~ (all_78_33 = % 84.68/11.81 | | | all_68_7) & vsubst(all_78_33, all_78_25, all_78_31) = % 84.68/11.81 | | | all_78_24 & vsubst(all_68_7, all_68_6, all_78_23) = all_68_0 & % 84.68/11.81 | | | vgensym(all_78_27) = all_78_32 & vapp(all_78_29, all_78_28) = % 84.68/11.81 | | | all_78_27 & vapp(all_68_6, all_78_31) = all_78_29 & % 84.68/11.81 | | | vabs(all_78_32, all_78_34, all_78_24) = all_78_23 & % 84.68/11.81 | | | vabs(all_78_33, all_78_34, all_78_31) = all_68_1 & % 84.68/11.81 | | | vvar(all_78_32) = all_78_25 & vvar(all_68_7) = all_78_28 & % 84.68/11.81 | | | $i(all_78_23) & $i(all_78_24) & $i(all_78_25) & $i(all_78_27) & % 84.68/11.81 | | | $i(all_78_28) & $i(all_78_29) & visFreeVar(all_78_33, all_68_6)) % 84.68/11.81 | | | | (all_78_37 = all_68_0 & all_78_39 = all_68_1 & all_78_41 = % 84.68/11.81 | | | all_68_6 & all_78_42 = all_68_7 & ~ (all_78_44 = all_68_7) & % 84.68/11.81 | | | vsubst(all_68_7, all_68_6, all_78_40) = all_78_38 & % 84.68/11.81 | | | vabs(all_78_44, all_78_43, all_78_38) = all_68_0 & % 84.68/11.81 | | | vabs(all_78_44, all_78_43, all_78_40) = all_68_1 & $i(all_78_38) % 84.68/11.81 | | | & ~ visFreeVar(all_78_44, all_68_6)) % 84.68/11.81 | | | % 84.68/11.81 | | | BETA: splitting (65) gives: % 84.68/11.81 | | | % 84.68/11.81 | | | Case 1: % 84.68/11.81 | | | | % 84.68/11.81 | | | | (66) all_78_16 = all_68_1 & all_78_19 = all_68_7 & all_78_20 = % 84.68/11.81 | | | | all_68_7 & all_78_21 = all_68_6 & all_68_0 = all_68_1 & % 84.68/11.81 | | | | vabs(all_68_7, all_78_18, all_78_17) = all_68_1 % 84.68/11.81 | | | | % 84.68/11.81 | | | | ALPHA: (66) implies: % 84.68/11.81 | | | | (67) all_68_0 = all_68_1 % 84.68/11.81 | | | | % 84.68/11.81 | | | | REDUCE: (53), (67) imply: % 84.68/11.81 | | | | (68) $false % 84.68/11.81 | | | | % 84.68/11.81 | | | | CLOSE: (68) is inconsistent. % 84.68/11.81 | | | | % 84.68/11.81 | | | Case 2: % 84.68/11.81 | | | | % 84.68/11.81 | | | | (69) (all_78_22 = all_68_0 & all_78_26 = all_78_32 & all_78_30 = % 84.68/11.81 | | | | all_68_1 & all_78_35 = all_68_6 & all_78_36 = all_68_7 & ~ % 84.68/11.81 | | | | (all_78_33 = all_68_7) & vsubst(all_78_33, all_78_25, % 84.68/11.81 | | | | all_78_31) = all_78_24 & vsubst(all_68_7, all_68_6, % 84.68/11.81 | | | | all_78_23) = all_68_0 & vgensym(all_78_27) = all_78_32 & % 84.68/11.81 | | | | vapp(all_78_29, all_78_28) = all_78_27 & vapp(all_68_6, % 84.68/11.81 | | | | all_78_31) = all_78_29 & vabs(all_78_32, all_78_34, % 84.68/11.81 | | | | all_78_24) = all_78_23 & vabs(all_78_33, all_78_34, % 84.68/11.81 | | | | all_78_31) = all_68_1 & vvar(all_78_32) = all_78_25 & % 84.68/11.81 | | | | vvar(all_68_7) = all_78_28 & $i(all_78_23) & $i(all_78_24) & % 84.68/11.81 | | | | $i(all_78_25) & $i(all_78_27) & $i(all_78_28) & $i(all_78_29) % 84.68/11.81 | | | | & visFreeVar(all_78_33, all_68_6)) | (all_78_37 = all_68_0 & % 84.68/11.81 | | | | all_78_39 = all_68_1 & all_78_41 = all_68_6 & all_78_42 = % 84.68/11.81 | | | | all_68_7 & ~ (all_78_44 = all_68_7) & vsubst(all_68_7, % 84.68/11.81 | | | | all_68_6, all_78_40) = all_78_38 & vabs(all_78_44, % 84.68/11.81 | | | | all_78_43, all_78_38) = all_68_0 & vabs(all_78_44, % 84.68/11.81 | | | | all_78_43, all_78_40) = all_68_1 & $i(all_78_38) & ~ % 84.68/11.81 | | | | visFreeVar(all_78_44, all_68_6)) % 84.68/11.81 | | | | % 84.68/11.81 | | | | BETA: splitting (69) gives: % 84.68/11.81 | | | | % 84.68/11.81 | | | | Case 1: % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | (70) all_78_22 = all_68_0 & all_78_26 = all_78_32 & all_78_30 = % 84.68/11.81 | | | | | all_68_1 & all_78_35 = all_68_6 & all_78_36 = all_68_7 & ~ % 84.68/11.81 | | | | | (all_78_33 = all_68_7) & vsubst(all_78_33, all_78_25, % 84.68/11.81 | | | | | all_78_31) = all_78_24 & vsubst(all_68_7, all_68_6, % 84.68/11.81 | | | | | all_78_23) = all_68_0 & vgensym(all_78_27) = all_78_32 & % 84.68/11.81 | | | | | vapp(all_78_29, all_78_28) = all_78_27 & vapp(all_68_6, % 84.68/11.81 | | | | | all_78_31) = all_78_29 & vabs(all_78_32, all_78_34, % 84.68/11.81 | | | | | all_78_24) = all_78_23 & vabs(all_78_33, all_78_34, % 84.68/11.81 | | | | | all_78_31) = all_68_1 & vvar(all_78_32) = all_78_25 & % 84.68/11.81 | | | | | vvar(all_68_7) = all_78_28 & $i(all_78_23) & $i(all_78_24) & % 84.68/11.81 | | | | | $i(all_78_25) & $i(all_78_27) & $i(all_78_28) & $i(all_78_29) % 84.68/11.81 | | | | | & visFreeVar(all_78_33, all_68_6) % 84.68/11.81 | | | | | % 84.68/11.81 | | | | | ALPHA: (70) implies: % 84.68/11.82 | | | | | (71) all_78_36 = all_68_7 % 84.68/11.82 | | | | | (72) all_78_35 = all_68_6 % 84.68/11.82 | | | | | (73) $i(all_78_29) % 84.68/11.82 | | | | | (74) $i(all_78_28) % 84.68/11.82 | | | | | (75) $i(all_78_27) % 84.68/11.82 | | | | | (76) $i(all_78_24) % 84.68/11.82 | | | | | (77) $i(all_78_23) % 84.68/11.82 | | | | | (78) vvar(all_68_7) = all_78_28 % 84.68/11.82 | | | | | (79) vvar(all_78_32) = all_78_25 % 84.68/11.82 | | | | | (80) vabs(all_78_33, all_78_34, all_78_31) = all_68_1 % 84.68/11.82 | | | | | (81) vabs(all_78_32, all_78_34, all_78_24) = all_78_23 % 84.68/11.82 | | | | | (82) vapp(all_68_6, all_78_31) = all_78_29 % 84.68/11.82 | | | | | (83) vapp(all_78_29, all_78_28) = all_78_27 % 84.68/11.82 | | | | | (84) vgensym(all_78_27) = all_78_32 % 84.68/11.82 | | | | | (85) vsubst(all_68_7, all_68_6, all_78_23) = all_68_0 % 84.68/11.82 | | | | | (86) vsubst(all_78_33, all_78_25, all_78_31) = all_78_24 % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | GROUND_INST: instantiating (3) with all_68_5, all_68_4, veabs, % 84.68/11.82 | | | | | all_78_33, all_78_34, all_78_31, all_68_1, simplifying % 84.68/11.82 | | | | | with (8), (20), (21), (26), (40), (41), (43), (80) gives: % 84.68/11.82 | | | | | (87) all_78_31 = veabs % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | GROUND_INST: instantiating (2) with all_68_5, all_68_4, veabs, % 84.68/11.82 | | | | | all_78_33, all_78_34, all_78_31, all_68_1, simplifying % 84.68/11.82 | | | | | with (8), (20), (21), (26), (40), (41), (43), (80) gives: % 84.68/11.82 | | | | | (88) all_78_34 = all_68_4 % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | GROUND_INST: instantiating (1) with all_68_5, all_68_4, veabs, % 84.68/11.82 | | | | | all_78_33, all_78_34, all_78_31, all_68_1, simplifying % 84.68/11.82 | | | | | with (8), (20), (21), (26), (40), (41), (43), (80) gives: % 84.68/11.82 | | | | | (89) all_78_33 = all_68_5 % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | GROUND_INST: instantiating (fresh-unequal-var-3) with all_68_6, % 84.68/11.82 | | | | | all_78_31, all_78_32, all_78_29, all_78_28, all_78_27, % 84.68/11.82 | | | | | simplifying with (19), (42), (43), (82), (83), (84) % 84.68/11.82 | | | | | gives: % 84.68/11.82 | | | | | (90) ~ (vvar(all_78_32) = all_78_28) % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | GROUND_INST: instantiating (alpha-equiv-subst-abs) with all_78_34, % 84.68/11.82 | | | | | all_78_33, all_78_32, all_78_31, all_78_25, all_78_24, % 84.68/11.82 | | | | | all_78_23, simplifying with (40), (41), (42), (43), (79), % 84.68/11.82 | | | | | (81), (86) gives: % 84.68/11.82 | | | | | (91) visFreeVar(all_78_32, all_78_31) | ? [v0: $i] : % 84.68/11.82 | | | | | (vabs(all_78_33, all_78_34, all_78_31) = v0 & $i(v0) & % 84.68/11.82 | | | | | valphaEquivalent(v0, all_78_23)) % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | REDUCE: (82), (87) imply: % 84.68/11.82 | | | | | (92) vapp(all_68_6, veabs) = all_78_29 % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | REDUCE: (81), (88) imply: % 84.68/11.82 | | | | | (93) vabs(all_78_32, all_68_4, all_78_24) = all_78_23 % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | PRED_UNIFY: (78), (90) imply: % 84.68/11.82 | | | | | (94) ~ (all_78_32 = all_68_7) % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | GROUND_INST: instantiating (6) with all_78_32, all_78_29, all_68_6, % 84.68/11.82 | | | | | veabs, simplifying with (8), (19), (42), (73), (92) % 84.68/11.82 | | | | | gives: % 84.68/11.82 | | | | | (95) ~ visFreeVar(all_78_32, all_68_6) | visFreeVar(all_78_32, % 84.68/11.82 | | | | | all_78_29) % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | REF_CLOSE: (6), (8), (10), (13), (14), (15), (16), (17), (18), (19), % 84.68/11.82 | | | | | (21), (22), (23), (26), (27), (42), (73), (74), (75), (76), % 84.68/11.82 | | | | | (77), (78), (83), (84), (85), (87), (88), (89), (91), (92), % 84.68/11.82 | | | | | (93), (94), (95), (T-subst-abs-2-gen), % 84.68/11.82 | | | | | (alpha-equiv-typing), (fresh-free-2), (gensym-is-fresh) are % 84.68/11.82 | | | | | inconsistent by sub-proof #2. % 84.68/11.82 | | | | | % 84.68/11.82 | | | | Case 2: % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | (96) all_78_37 = all_68_0 & all_78_39 = all_68_1 & all_78_41 = % 84.68/11.82 | | | | | all_68_6 & all_78_42 = all_68_7 & ~ (all_78_44 = all_68_7) & % 84.68/11.82 | | | | | vsubst(all_68_7, all_68_6, all_78_40) = all_78_38 & % 84.68/11.82 | | | | | vabs(all_78_44, all_78_43, all_78_38) = all_68_0 & % 84.68/11.82 | | | | | vabs(all_78_44, all_78_43, all_78_40) = all_68_1 & % 84.68/11.82 | | | | | $i(all_78_38) & ~ visFreeVar(all_78_44, all_68_6) % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | ALPHA: (96) implies: % 84.68/11.82 | | | | | (97) ~ visFreeVar(all_78_44, all_68_6) % 84.68/11.82 | | | | | (98) vabs(all_78_44, all_78_43, all_78_40) = all_68_1 % 84.68/11.82 | | | | | % 84.68/11.82 | | | | | REF_CLOSE: (1), (8), (12), (13), (14), (15), (16), (17), (18), (19), % 84.68/11.82 | | | | | (20), (21), (22), (26), (27), (28), (33), (34), (37), (97), % 84.68/11.82 | | | | | (98), (T-subst-abs-2-gen) are inconsistent by sub-proof #1. % 84.68/11.82 | | | | | % 84.68/11.82 | | | | End of split % 84.68/11.82 | | | | % 84.68/11.82 | | | End of split % 84.68/11.82 | | | % 84.68/11.82 | | End of split % 84.68/11.82 | | % 84.68/11.82 | Case 2: % 84.68/11.82 | | % 84.68/11.82 | | (99) visFreeVar(all_68_7, all_68_1) % 84.68/11.82 | | % 85.04/11.82 | | GROUND_INST: instantiating (5) with all_68_4, all_68_7, all_68_1, all_68_5, % 85.04/11.82 | | veabs, simplifying with (8), (18), (20), (21), (24), (26), (99) % 85.04/11.82 | | gives: % 85.04/11.82 | | (100) visFreeVar(all_68_7, veabs) % 85.04/11.82 | | % 85.04/11.82 | | BETA: splitting (51) gives: % 85.04/11.82 | | % 85.04/11.82 | | Case 1: % 85.04/11.82 | | | % 85.04/11.83 | | | (101) (all_78_0 = all_68_1 & all_78_1 = all_68_6 & all_78_2 = all_68_7 % 85.04/11.83 | | | & all_78_3 = all_68_7 & all_68_0 = all_68_6 & vvar(all_68_7) = % 85.04/11.83 | | | all_68_1) | (all_78_4 = all_68_1 & all_78_6 = all_68_7 & % 85.04/11.83 | | | all_78_7 = all_68_6 & all_68_0 = all_68_1 & ~ (all_78_5 = % 85.04/11.83 | | | all_68_7) & vvar(all_78_5) = all_68_1) | (all_78_8 = all_68_0 % 85.04/11.83 | | | & all_78_11 = all_68_1 & all_78_13 = all_68_6 & all_78_14 = % 85.04/11.83 | | | all_68_7 & vsubst(all_68_7, all_68_6, all_78_12) = all_78_9 & % 85.04/11.83 | | | vsubst(all_68_7, all_68_6, all_78_15) = all_78_10 & % 85.04/11.83 | | | vapp(all_78_10, all_78_9) = all_68_0 & vapp(all_78_15, % 85.04/11.83 | | | all_78_12) = all_68_1 & $i(all_78_9) & $i(all_78_10)) % 85.04/11.83 | | | % 85.04/11.83 | | | BETA: splitting (101) gives: % 85.04/11.83 | | | % 85.04/11.83 | | | Case 1: % 85.04/11.83 | | | | % 85.04/11.83 | | | | (102) all_78_0 = all_68_1 & all_78_1 = all_68_6 & all_78_2 = all_68_7 % 85.04/11.83 | | | | & all_78_3 = all_68_7 & all_68_0 = all_68_6 & vvar(all_68_7) = % 85.04/11.83 | | | | all_68_1 % 85.04/11.83 | | | | % 85.04/11.83 | | | | ALPHA: (102) implies: % 85.04/11.83 | | | | (103) all_78_3 = all_68_7 % 85.04/11.83 | | | | (104) vvar(all_68_7) = all_68_1 % 85.04/11.83 | | | | % 85.04/11.83 | | | | GROUND_INST: instantiating (isValue1) with all_68_7, all_68_1, % 85.04/11.83 | | | | simplifying with (18), (24), (29), (104) gives: % 85.04/11.83 | | | | (105) $false % 85.04/11.83 | | | | % 85.04/11.83 | | | | CLOSE: (105) is inconsistent. % 85.04/11.83 | | | | % 85.04/11.83 | | | Case 2: % 85.04/11.83 | | | | % 85.04/11.83 | | | | (106) (all_78_4 = all_68_1 & all_78_6 = all_68_7 & all_78_7 = % 85.04/11.83 | | | | all_68_6 & all_68_0 = all_68_1 & ~ (all_78_5 = all_68_7) & % 85.04/11.83 | | | | vvar(all_78_5) = all_68_1) | (all_78_8 = all_68_0 & all_78_11 % 85.04/11.83 | | | | = all_68_1 & all_78_13 = all_68_6 & all_78_14 = all_68_7 & % 85.04/11.83 | | | | vsubst(all_68_7, all_68_6, all_78_12) = all_78_9 & % 85.04/11.83 | | | | vsubst(all_68_7, all_68_6, all_78_15) = all_78_10 & % 85.04/11.83 | | | | vapp(all_78_10, all_78_9) = all_68_0 & vapp(all_78_15, % 85.04/11.83 | | | | all_78_12) = all_68_1 & $i(all_78_9) & $i(all_78_10)) % 85.04/11.83 | | | | % 85.04/11.83 | | | | BETA: splitting (106) gives: % 85.04/11.83 | | | | % 85.04/11.83 | | | | Case 1: % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | (107) all_78_4 = all_68_1 & all_78_6 = all_68_7 & all_78_7 = % 85.04/11.83 | | | | | all_68_6 & all_68_0 = all_68_1 & ~ (all_78_5 = all_68_7) & % 85.04/11.83 | | | | | vvar(all_78_5) = all_68_1 % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | ALPHA: (107) implies: % 85.04/11.83 | | | | | (108) all_68_0 = all_68_1 % 85.04/11.83 | | | | | (109) vvar(all_78_5) = all_68_1 % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | GROUND_INST: instantiating (isValue1) with all_78_5, all_68_1, % 85.04/11.83 | | | | | simplifying with (24), (29), (49), (109) gives: % 85.04/11.83 | | | | | (110) $false % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | CLOSE: (110) is inconsistent. % 85.04/11.83 | | | | | % 85.04/11.83 | | | | Case 2: % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | (111) all_78_8 = all_68_0 & all_78_11 = all_68_1 & all_78_13 = % 85.04/11.83 | | | | | all_68_6 & all_78_14 = all_68_7 & vsubst(all_68_7, all_68_6, % 85.04/11.83 | | | | | all_78_12) = all_78_9 & vsubst(all_68_7, all_68_6, % 85.04/11.83 | | | | | all_78_15) = all_78_10 & vapp(all_78_10, all_78_9) = % 85.04/11.83 | | | | | all_68_0 & vapp(all_78_15, all_78_12) = all_68_1 & % 85.04/11.83 | | | | | $i(all_78_9) & $i(all_78_10) % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | ALPHA: (111) implies: % 85.04/11.83 | | | | | (112) vapp(all_78_15, all_78_12) = all_68_1 % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | GROUND_INST: instantiating (isValue2) with all_78_15, all_78_12, % 85.04/11.83 | | | | | all_68_1, simplifying with (24), (29), (47), (48), (112) % 85.04/11.83 | | | | | gives: % 85.04/11.83 | | | | | (113) $false % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | CLOSE: (113) is inconsistent. % 85.04/11.83 | | | | | % 85.04/11.83 | | | | End of split % 85.04/11.83 | | | | % 85.04/11.83 | | | End of split % 85.04/11.83 | | | % 85.04/11.83 | | Case 2: % 85.04/11.83 | | | % 85.04/11.83 | | | (114) (all_78_16 = all_68_1 & all_78_19 = all_68_7 & all_78_20 = % 85.04/11.83 | | | all_68_7 & all_78_21 = all_68_6 & all_68_0 = all_68_1 & % 85.04/11.83 | | | vabs(all_68_7, all_78_18, all_78_17) = all_68_1) | (all_78_22 = % 85.04/11.83 | | | all_68_0 & all_78_26 = all_78_32 & all_78_30 = all_68_1 & % 85.04/11.83 | | | all_78_35 = all_68_6 & all_78_36 = all_68_7 & ~ (all_78_33 = % 85.04/11.83 | | | all_68_7) & vsubst(all_78_33, all_78_25, all_78_31) = % 85.04/11.83 | | | all_78_24 & vsubst(all_68_7, all_68_6, all_78_23) = all_68_0 & % 85.04/11.83 | | | vgensym(all_78_27) = all_78_32 & vapp(all_78_29, all_78_28) = % 85.04/11.83 | | | all_78_27 & vapp(all_68_6, all_78_31) = all_78_29 & % 85.04/11.83 | | | vabs(all_78_32, all_78_34, all_78_24) = all_78_23 & % 85.04/11.83 | | | vabs(all_78_33, all_78_34, all_78_31) = all_68_1 & % 85.04/11.83 | | | vvar(all_78_32) = all_78_25 & vvar(all_68_7) = all_78_28 & % 85.04/11.83 | | | $i(all_78_23) & $i(all_78_24) & $i(all_78_25) & $i(all_78_27) & % 85.04/11.83 | | | $i(all_78_28) & $i(all_78_29) & visFreeVar(all_78_33, % 85.04/11.83 | | | all_68_6)) | (all_78_37 = all_68_0 & all_78_39 = all_68_1 & % 85.04/11.83 | | | all_78_41 = all_68_6 & all_78_42 = all_68_7 & ~ (all_78_44 = % 85.04/11.83 | | | all_68_7) & vsubst(all_68_7, all_68_6, all_78_40) = all_78_38 % 85.04/11.83 | | | & vabs(all_78_44, all_78_43, all_78_38) = all_68_0 & % 85.04/11.83 | | | vabs(all_78_44, all_78_43, all_78_40) = all_68_1 & % 85.04/11.83 | | | $i(all_78_38) & ~ visFreeVar(all_78_44, all_68_6)) % 85.04/11.83 | | | % 85.04/11.83 | | | BETA: splitting (114) gives: % 85.04/11.83 | | | % 85.04/11.83 | | | Case 1: % 85.04/11.83 | | | | % 85.04/11.83 | | | | (115) all_78_16 = all_68_1 & all_78_19 = all_68_7 & all_78_20 = % 85.04/11.83 | | | | all_68_7 & all_78_21 = all_68_6 & all_68_0 = all_68_1 & % 85.04/11.83 | | | | vabs(all_68_7, all_78_18, all_78_17) = all_68_1 % 85.04/11.83 | | | | % 85.04/11.83 | | | | ALPHA: (115) implies: % 85.04/11.83 | | | | (116) all_68_0 = all_68_1 % 85.04/11.83 | | | | (117) all_78_20 = all_68_7 % 85.04/11.83 | | | | (118) vabs(all_68_7, all_78_18, all_78_17) = all_68_1 % 85.04/11.83 | | | | % 85.04/11.83 | | | | GROUND_INST: instantiating (4) with all_78_18, all_68_7, all_68_1, % 85.04/11.83 | | | | all_78_17, simplifying with (18), (24), (45), (46), (99), % 85.04/11.83 | | | | (118) gives: % 85.04/11.83 | | | | (119) $false % 85.04/11.83 | | | | % 85.04/11.83 | | | | CLOSE: (119) is inconsistent. % 85.04/11.83 | | | | % 85.04/11.83 | | | Case 2: % 85.04/11.83 | | | | % 85.04/11.83 | | | | (120) (all_78_22 = all_68_0 & all_78_26 = all_78_32 & all_78_30 = % 85.04/11.83 | | | | all_68_1 & all_78_35 = all_68_6 & all_78_36 = all_68_7 & ~ % 85.04/11.83 | | | | (all_78_33 = all_68_7) & vsubst(all_78_33, all_78_25, % 85.04/11.83 | | | | all_78_31) = all_78_24 & vsubst(all_68_7, all_68_6, % 85.04/11.83 | | | | all_78_23) = all_68_0 & vgensym(all_78_27) = all_78_32 & % 85.04/11.83 | | | | vapp(all_78_29, all_78_28) = all_78_27 & vapp(all_68_6, % 85.04/11.83 | | | | all_78_31) = all_78_29 & vabs(all_78_32, all_78_34, % 85.04/11.83 | | | | all_78_24) = all_78_23 & vabs(all_78_33, all_78_34, % 85.04/11.83 | | | | all_78_31) = all_68_1 & vvar(all_78_32) = all_78_25 & % 85.04/11.83 | | | | vvar(all_68_7) = all_78_28 & $i(all_78_23) & $i(all_78_24) & % 85.04/11.83 | | | | $i(all_78_25) & $i(all_78_27) & $i(all_78_28) & $i(all_78_29) % 85.04/11.83 | | | | & visFreeVar(all_78_33, all_68_6)) | (all_78_37 = all_68_0 & % 85.04/11.83 | | | | all_78_39 = all_68_1 & all_78_41 = all_68_6 & all_78_42 = % 85.04/11.83 | | | | all_68_7 & ~ (all_78_44 = all_68_7) & vsubst(all_68_7, % 85.04/11.83 | | | | all_68_6, all_78_40) = all_78_38 & vabs(all_78_44, % 85.04/11.83 | | | | all_78_43, all_78_38) = all_68_0 & vabs(all_78_44, % 85.04/11.83 | | | | all_78_43, all_78_40) = all_68_1 & $i(all_78_38) & ~ % 85.04/11.83 | | | | visFreeVar(all_78_44, all_68_6)) % 85.04/11.83 | | | | % 85.04/11.83 | | | | BETA: splitting (120) gives: % 85.04/11.83 | | | | % 85.04/11.83 | | | | Case 1: % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | (121) all_78_22 = all_68_0 & all_78_26 = all_78_32 & all_78_30 = % 85.04/11.83 | | | | | all_68_1 & all_78_35 = all_68_6 & all_78_36 = all_68_7 & ~ % 85.04/11.83 | | | | | (all_78_33 = all_68_7) & vsubst(all_78_33, all_78_25, % 85.04/11.83 | | | | | all_78_31) = all_78_24 & vsubst(all_68_7, all_68_6, % 85.04/11.83 | | | | | all_78_23) = all_68_0 & vgensym(all_78_27) = all_78_32 & % 85.04/11.83 | | | | | vapp(all_78_29, all_78_28) = all_78_27 & vapp(all_68_6, % 85.04/11.83 | | | | | all_78_31) = all_78_29 & vabs(all_78_32, all_78_34, % 85.04/11.83 | | | | | all_78_24) = all_78_23 & vabs(all_78_33, all_78_34, % 85.04/11.83 | | | | | all_78_31) = all_68_1 & vvar(all_78_32) = all_78_25 & % 85.04/11.83 | | | | | vvar(all_68_7) = all_78_28 & $i(all_78_23) & $i(all_78_24) & % 85.04/11.83 | | | | | $i(all_78_25) & $i(all_78_27) & $i(all_78_28) & $i(all_78_29) % 85.04/11.83 | | | | | & visFreeVar(all_78_33, all_68_6) % 85.04/11.83 | | | | | % 85.04/11.83 | | | | | ALPHA: (121) implies: % 85.04/11.83 | | | | | (122) all_78_36 = all_68_7 % 85.04/11.83 | | | | | (123) all_78_35 = all_68_6 % 85.04/11.83 | | | | | (124) $i(all_78_29) % 85.04/11.83 | | | | | (125) $i(all_78_28) % 85.04/11.83 | | | | | (126) $i(all_78_27) % 85.04/11.83 | | | | | (127) $i(all_78_24) % 85.04/11.83 | | | | | (128) $i(all_78_23) % 85.04/11.83 | | | | | (129) vvar(all_68_7) = all_78_28 % 85.04/11.83 | | | | | (130) vvar(all_78_32) = all_78_25 % 85.04/11.83 | | | | | (131) vabs(all_78_33, all_78_34, all_78_31) = all_68_1 % 85.04/11.84 | | | | | (132) vabs(all_78_32, all_78_34, all_78_24) = all_78_23 % 85.04/11.84 | | | | | (133) vapp(all_68_6, all_78_31) = all_78_29 % 85.04/11.84 | | | | | (134) vapp(all_78_29, all_78_28) = all_78_27 % 85.04/11.84 | | | | | (135) vgensym(all_78_27) = all_78_32 % 85.04/11.84 | | | | | (136) vsubst(all_68_7, all_68_6, all_78_23) = all_68_0 % 85.04/11.84 | | | | | (137) vsubst(all_78_33, all_78_25, all_78_31) = all_78_24 % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | GROUND_INST: instantiating (3) with all_68_5, all_68_4, veabs, % 85.04/11.84 | | | | | all_78_33, all_78_34, all_78_31, all_68_1, simplifying % 85.04/11.84 | | | | | with (8), (20), (21), (26), (40), (41), (43), (131) % 85.04/11.84 | | | | | gives: % 85.04/11.84 | | | | | (138) all_78_31 = veabs % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | GROUND_INST: instantiating (2) with all_68_5, all_68_4, veabs, % 85.04/11.84 | | | | | all_78_33, all_78_34, all_78_31, all_68_1, simplifying % 85.04/11.84 | | | | | with (8), (20), (21), (26), (40), (41), (43), (131) % 85.04/11.84 | | | | | gives: % 85.04/11.84 | | | | | (139) all_78_34 = all_68_4 % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | GROUND_INST: instantiating (1) with all_68_5, all_68_4, veabs, % 85.04/11.84 | | | | | all_78_33, all_78_34, all_78_31, all_68_1, simplifying % 85.04/11.84 | | | | | with (8), (20), (21), (26), (40), (41), (43), (131) % 85.04/11.84 | | | | | gives: % 85.04/11.84 | | | | | (140) all_78_33 = all_68_5 % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | GROUND_INST: instantiating (7) with all_68_7, all_78_29, all_68_6, % 85.04/11.84 | | | | | veabs, simplifying with (8), (18), (19), (100), (124) % 85.04/11.84 | | | | | gives: % 85.04/11.84 | | | | | (141) ~ (vapp(all_68_6, veabs) = all_78_29) | visFreeVar(all_68_7, % 85.04/11.84 | | | | | all_78_29) % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | GROUND_INST: instantiating (fresh-unequal-var-3) with all_68_6, % 85.04/11.84 | | | | | all_78_31, all_78_32, all_78_29, all_78_28, all_78_27, % 85.04/11.84 | | | | | simplifying with (19), (42), (43), (133), (134), (135) % 85.04/11.84 | | | | | gives: % 85.04/11.84 | | | | | (142) ~ (vvar(all_78_32) = all_78_28) % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | GROUND_INST: instantiating (alpha-equiv-subst-abs) with all_78_34, % 85.04/11.84 | | | | | all_78_33, all_78_32, all_78_31, all_78_25, all_78_24, % 85.04/11.84 | | | | | all_78_23, simplifying with (40), (41), (42), (43), % 85.04/11.84 | | | | | (130), (132), (137) gives: % 85.04/11.84 | | | | | (143) visFreeVar(all_78_32, all_78_31) | ? [v0: $i] : % 85.04/11.84 | | | | | (vabs(all_78_33, all_78_34, all_78_31) = v0 & $i(v0) & % 85.04/11.84 | | | | | valphaEquivalent(v0, all_78_23)) % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | REDUCE: (133), (138) imply: % 85.04/11.84 | | | | | (144) vapp(all_68_6, veabs) = all_78_29 % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | REDUCE: (132), (139) imply: % 85.04/11.84 | | | | | (145) vabs(all_78_32, all_68_4, all_78_24) = all_78_23 % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | BETA: splitting (141) gives: % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | Case 1: % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | | (146) ~ (vapp(all_68_6, veabs) = all_78_29) % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | | PRED_UNIFY: (144), (146) imply: % 85.04/11.84 | | | | | | (147) $false % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | | CLOSE: (147) is inconsistent. % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | Case 2: % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | | PRED_UNIFY: (129), (142) imply: % 85.04/11.84 | | | | | | (148) ~ (all_78_32 = all_68_7) % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | | GROUND_INST: instantiating (6) with all_78_32, all_78_29, all_68_6, % 85.04/11.84 | | | | | | veabs, simplifying with (8), (19), (42), (124), (144) % 85.04/11.84 | | | | | | gives: % 85.04/11.84 | | | | | | (149) ~ visFreeVar(all_78_32, all_68_6) | visFreeVar(all_78_32, % 85.04/11.84 | | | | | | all_78_29) % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | | REF_CLOSE: (6), (8), (10), (13), (14), (15), (16), (17), (18), (19), % 85.04/11.84 | | | | | | (21), (22), (23), (26), (27), (42), (124), (125), (126), % 85.04/11.84 | | | | | | (127), (128), (129), (134), (135), (136), (138), (139), % 85.04/11.84 | | | | | | (140), (143), (144), (145), (148), (149), % 85.04/11.84 | | | | | | (T-subst-abs-2-gen), (alpha-equiv-typing), % 85.04/11.84 | | | | | | (fresh-free-2), (gensym-is-fresh) are inconsistent by % 85.04/11.84 | | | | | | sub-proof #2. % 85.04/11.84 | | | | | | % 85.04/11.84 | | | | | End of split % 85.04/11.84 | | | | | % 85.04/11.84 | | | | Case 2: % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | (150) all_78_37 = all_68_0 & all_78_39 = all_68_1 & all_78_41 = % 85.04/11.84 | | | | | all_68_6 & all_78_42 = all_68_7 & ~ (all_78_44 = all_68_7) & % 85.04/11.84 | | | | | vsubst(all_68_7, all_68_6, all_78_40) = all_78_38 & % 85.04/11.84 | | | | | vabs(all_78_44, all_78_43, all_78_38) = all_68_0 & % 85.04/11.84 | | | | | vabs(all_78_44, all_78_43, all_78_40) = all_68_1 & % 85.04/11.84 | | | | | $i(all_78_38) & ~ visFreeVar(all_78_44, all_68_6) % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | ALPHA: (150) implies: % 85.04/11.84 | | | | | (151) all_78_42 = all_68_7 % 85.04/11.84 | | | | | (152) all_78_41 = all_68_6 % 85.04/11.84 | | | | | (153) ~ visFreeVar(all_78_44, all_68_6) % 85.04/11.84 | | | | | (154) vabs(all_78_44, all_78_43, all_78_40) = all_68_1 % 85.04/11.84 | | | | | % 85.04/11.84 | | | | | REF_CLOSE: (1), (8), (12), (13), (14), (15), (16), (17), (18), (19), % 85.04/11.84 | | | | | (20), (21), (22), (26), (27), (28), (33), (34), (37), % 85.04/11.84 | | | | | (153), (154), (T-subst-abs-2-gen) are inconsistent by % 85.04/11.84 | | | | | sub-proof #1. % 85.04/11.84 | | | | | % 85.04/11.84 | | | | End of split % 85.04/11.84 | | | | % 85.04/11.84 | | | End of split % 85.04/11.84 | | | % 85.04/11.84 | | End of split % 85.04/11.84 | | % 85.04/11.84 | End of split % 85.04/11.84 | % 85.04/11.84 End of proof % 85.04/11.84 % 85.04/11.84 Sub-proof #1 shows that the following formulas are inconsistent: % 85.04/11.84 ---------------------------------------------------------------- % 85.04/11.84 (1) $i(all_78_40) % 85.04/11.84 (2) $i(all_68_7) % 85.04/11.84 (3) $i(all_68_3) % 85.04/11.84 (4) $i(all_78_43) % 85.04/11.84 (5) $i(all_68_9) % 85.04/11.84 (6) $i(all_68_4) % 85.04/11.84 (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 85.04/11.84 [v5: $i] : ! [v6: $i] : (v3 = v0 | ~ (vabs(v3, v4, v5) = v6) | ~ % 85.04/11.84 (vabs(v0, v1, v2) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) % 85.04/11.84 | ~ $i(v1) | ~ $i(v0)) % 85.04/11.84 (8) $i(all_68_6) % 85.04/11.84 (9) $i(veabs) % 85.04/11.84 (10) vtcheck(all_68_8, all_68_6, all_68_9) % 85.04/11.84 (11) $i(all_78_44) % 85.04/11.84 (12) vabs(all_78_44, all_78_43, all_78_40) = all_68_1 % 85.04/11.84 (13) vabs(all_68_5, all_68_4, veabs) = all_68_1 % 85.04/11.84 (14) $i(all_68_8) % 85.04/11.84 (15) ~ (all_68_5 = all_68_7) % 85.04/11.84 (16) vtcheck(all_68_2, all_68_1, all_68_3) % 85.04/11.84 (17) ~ visFreeVar(all_78_44, all_68_6) % 85.04/11.84 (18) vbind(all_68_7, all_68_9, all_68_8) = all_68_2 % 85.04/11.84 (19) vsubst(all_68_7, all_68_6, all_68_1) = all_68_0 % 85.04/11.85 (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 85.04/11.85 [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! % 85.04/11.85 [v10: $i] : (v4 = v2 | ~ (vsubst(v2, v3, v9) = v10) | ~ (vbind(v2, v0, % 85.04/11.85 v1) = v8) | ~ (vabs(v4, v5, v6) = v9) | ~ $i(v7) | ~ $i(v6) | % 85.04/11.85 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 85.04/11.85 ~ vtcheck(v8, v9, v7) | ~ vtcheck(v1, v3, v0) | vtcheck(v1, v10, v7) % 85.04/11.85 | visFreeVar(v4, v3)) % 85.04/11.85 (21) ~ vtcheck(all_68_8, all_68_0, all_68_3) % 85.04/11.85 (22) $i(all_68_5) % 85.04/11.85 % 85.04/11.85 Begin of proof % 85.04/11.85 | % 85.04/11.85 | GROUND_INST: instantiating (20) with all_68_9, all_68_8, all_68_7, all_68_6, % 85.04/11.85 | all_78_44, all_78_43, all_78_40, all_68_3, all_68_2, all_68_1, % 85.04/11.85 | all_68_0, simplifying with (1), (2), (3), (4), (5), (8), (10), % 85.04/11.85 | (11), (12), (14), (16), (17), (18), (19), (21) gives: % 85.04/11.85 | (23) all_78_44 = all_68_7 % 85.04/11.85 | % 85.04/11.85 | GROUND_INST: instantiating (7) with all_68_5, all_68_4, veabs, all_78_44, % 85.04/11.85 | all_78_43, all_78_40, all_68_1, simplifying with (1), (4), (6), % 85.04/11.85 | (9), (11), (12), (13), (22) gives: % 85.04/11.85 | (24) all_78_44 = all_68_5 % 85.04/11.85 | % 85.04/11.85 | COMBINE_EQS: (23), (24) imply: % 85.04/11.85 | (25) all_68_5 = all_68_7 % 85.04/11.85 | % 85.04/11.85 | REDUCE: (15), (25) imply: % 85.04/11.85 | (26) $false % 85.04/11.85 | % 85.04/11.85 | CLOSE: (26) is inconsistent. % 85.04/11.85 | % 85.04/11.85 End of proof % 85.04/11.85 % 85.04/11.85 Sub-proof #2 shows that the following formulas are inconsistent: % 85.04/11.85 ---------------------------------------------------------------- % 85.04/11.85 (1) $i(all_78_27) % 85.04/11.85 (2) all_78_33 = all_68_5 % 85.04/11.85 (3) $i(all_78_23) % 85.04/11.85 (4) vabs(all_78_32, all_68_4, all_78_24) = all_78_23 % 85.04/11.85 (5) $i(all_78_28) % 85.04/11.85 (6) $i(all_68_7) % 85.04/11.85 (7) $i(all_68_2) % 85.04/11.85 (8) vvar(all_68_7) = all_78_28 % 85.04/11.85 (9) $i(all_78_24) % 85.04/11.85 (10) $i(all_78_29) % 85.04/11.85 (11) $i(all_68_3) % 85.04/11.85 (12) $i(all_68_9) % 85.04/11.85 (13) ! [v0: $i] : ! [v1: $i] : ( ~ (vgensym(v1) = v0) | ~ $i(v1) | ~ % 85.04/11.85 $i(v0) | ~ visFreeVar(v0, v1)) % 85.04/11.85 (14) $i(all_68_4) % 85.04/11.85 (15) $i(all_68_6) % 85.04/11.85 (16) $i(veabs) % 85.04/11.85 (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 85.04/11.85 [v5: $i] : ! [v6: $i] : ( ~ (vgensym(v6) = v2) | ~ (vapp(v4, v5) = v6) % 85.04/11.85 | ~ (vapp(v0, v3) = v4) | ~ (vvar(v1) = v5) | ~ $i(v3) | ~ $i(v2) % 85.04/11.85 | ~ $i(v1) | ~ $i(v0) | ~ visFreeVar(v2, v3)) % 85.04/11.85 (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (vapp(v2, % 85.04/11.85 v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 85.04/11.85 visFreeVar(v0, v2) | visFreeVar(v0, v1)) % 85.04/11.85 (19) vtcheck(all_68_8, all_68_6, all_68_9) % 85.04/11.85 (20) visFreeVar(all_78_32, all_78_31) | ? [v0: $i] : (vabs(all_78_33, % 85.04/11.85 all_78_34, all_78_31) = v0 & $i(v0) & valphaEquivalent(v0, % 85.04/11.85 all_78_23)) % 85.04/11.85 (21) vabs(all_68_5, all_68_4, veabs) = all_68_1 % 85.04/11.85 (22) $i(all_68_8) % 85.04/11.85 (23) ~ visFreeVar(all_78_32, all_68_6) | visFreeVar(all_78_32, all_78_29) % 85.04/11.85 (24) vtcheck(all_68_2, all_68_1, all_68_3) % 85.04/11.85 (25) vapp(all_68_6, veabs) = all_78_29 % 85.04/11.85 (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 85.04/11.85 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ valphaEquivalent(v0, v2) | ~ % 85.04/11.85 vtcheck(v1, v0, v3) | vtcheck(v1, v2, v3)) % 85.04/11.85 (27) vsubst(all_68_7, all_68_6, all_78_23) = all_68_0 % 85.04/11.85 (28) ~ (all_78_32 = all_68_7) % 85.04/11.85 (29) vgensym(all_78_27) = all_78_32 % 85.04/11.85 (30) vbind(all_68_7, all_68_9, all_68_8) = all_68_2 % 85.04/11.85 (31) vapp(all_78_29, all_78_28) = all_78_27 % 85.04/11.85 (32) $i(all_78_32) % 85.04/11.85 (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 85.04/11.85 [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! % 85.04/11.85 [v10: $i] : (v4 = v2 | ~ (vsubst(v2, v3, v9) = v10) | ~ (vbind(v2, v0, % 85.04/11.85 v1) = v8) | ~ (vabs(v4, v5, v6) = v9) | ~ $i(v7) | ~ $i(v6) | % 85.04/11.85 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 85.04/11.85 ~ vtcheck(v8, v9, v7) | ~ vtcheck(v1, v3, v0) | vtcheck(v1, v10, v7) % 85.04/11.85 | visFreeVar(v4, v3)) % 85.04/11.85 (34) ~ vtcheck(all_68_8, all_68_0, all_68_3) % 85.04/11.85 (35) all_78_31 = veabs % 85.04/11.85 (36) all_78_34 = all_68_4 % 85.04/11.85 (37) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 85.04/11.85 (v1 = v0 | ~ (vabs(v4, v3, v2) = v1) | ~ (vabs(v4, v3, v2) = v0)) % 85.04/11.85 % 85.04/11.85 Begin of proof % 85.04/11.85 | % 85.04/11.85 | BETA: splitting (20) gives: % 85.04/11.85 | % 85.04/11.85 | Case 1: % 85.04/11.85 | | % 85.04/11.85 | | (38) visFreeVar(all_78_32, all_78_31) % 85.04/11.85 | | % 85.04/11.85 | | REDUCE: (35), (38) imply: % 85.04/11.85 | | (39) visFreeVar(all_78_32, veabs) % 85.04/11.85 | | % 85.04/11.85 | | GROUND_INST: instantiating (17) with all_68_6, all_68_7, all_78_32, veabs, % 85.04/11.85 | | all_78_29, all_78_28, all_78_27, simplifying with (6), (8), % 85.04/11.85 | | (15), (16), (25), (29), (31), (32), (39) gives: % 85.04/11.85 | | (40) $false % 85.04/11.85 | | % 85.04/11.85 | | CLOSE: (40) is inconsistent. % 85.04/11.85 | | % 85.04/11.85 | Case 2: % 85.04/11.85 | | % 85.04/11.85 | | (41) ? [v0: $i] : (vabs(all_78_33, all_78_34, all_78_31) = v0 & $i(v0) & % 85.04/11.85 | | valphaEquivalent(v0, all_78_23)) % 85.04/11.85 | | % 85.04/11.85 | | DELTA: instantiating (41) with fresh symbol all_210_0 gives: % 85.04/11.85 | | (42) vabs(all_78_33, all_78_34, all_78_31) = all_210_0 & $i(all_210_0) & % 85.04/11.85 | | valphaEquivalent(all_210_0, all_78_23) % 85.04/11.85 | | % 85.04/11.85 | | ALPHA: (42) implies: % 85.04/11.85 | | (43) valphaEquivalent(all_210_0, all_78_23) % 85.04/11.85 | | (44) $i(all_210_0) % 85.04/11.85 | | (45) vabs(all_78_33, all_78_34, all_78_31) = all_210_0 % 85.04/11.85 | | % 85.04/11.85 | | REDUCE: (2), (35), (36), (45) imply: % 85.04/11.85 | | (46) vabs(all_68_5, all_68_4, veabs) = all_210_0 % 85.04/11.85 | | % 85.04/11.85 | | GROUND_INST: instantiating (37) with all_68_1, all_210_0, veabs, all_68_4, % 85.04/11.85 | | all_68_5, simplifying with (21), (46) gives: % 85.04/11.85 | | (47) all_210_0 = all_68_1 % 85.04/11.85 | | % 85.04/11.85 | | REDUCE: (44), (47) imply: % 85.04/11.85 | | (48) $i(all_68_1) % 85.04/11.85 | | % 85.04/11.85 | | REDUCE: (43), (47) imply: % 85.04/11.85 | | (49) valphaEquivalent(all_68_1, all_78_23) % 85.04/11.85 | | % 85.04/11.85 | | GROUND_INST: instantiating (26) with all_68_1, all_68_2, all_78_23, % 85.04/11.85 | | all_68_3, simplifying with (3), (7), (11), (24), (48), (49) % 85.04/11.85 | | gives: % 85.04/11.86 | | (50) vtcheck(all_68_2, all_78_23, all_68_3) % 85.04/11.86 | | % 85.04/11.86 | | GROUND_INST: instantiating (33) with all_68_9, all_68_8, all_68_7, all_68_6, % 85.04/11.86 | | all_78_32, all_68_4, all_78_24, all_68_3, all_68_2, all_78_23, % 85.04/11.86 | | all_68_0, simplifying with (4), (6), (9), (11), (12), (14), % 85.04/11.86 | | (15), (19), (22), (27), (30), (32), (34), (50) gives: % 85.04/11.86 | | (51) all_78_32 = all_68_7 | visFreeVar(all_78_32, all_68_6) % 85.04/11.86 | | % 85.04/11.86 | | BETA: splitting (51) gives: % 85.04/11.86 | | % 85.04/11.86 | | Case 1: % 85.04/11.86 | | | % 85.04/11.86 | | | (52) visFreeVar(all_78_32, all_68_6) % 85.04/11.86 | | | % 85.04/11.86 | | | BETA: splitting (23) gives: % 85.04/11.86 | | | % 85.04/11.86 | | | Case 1: % 85.04/11.86 | | | | % 85.04/11.86 | | | | (53) ~ visFreeVar(all_78_32, all_68_6) % 85.04/11.86 | | | | % 85.04/11.86 | | | | PRED_UNIFY: (52), (53) imply: % 85.04/11.86 | | | | (54) $false % 85.04/11.86 | | | | % 85.04/11.86 | | | | CLOSE: (54) is inconsistent. % 85.04/11.86 | | | | % 85.04/11.86 | | | Case 2: % 85.04/11.86 | | | | % 85.04/11.86 | | | | (55) visFreeVar(all_78_32, all_78_29) % 85.04/11.86 | | | | % 85.04/11.86 | | | | GROUND_INST: instantiating (18) with all_78_32, all_78_27, all_78_29, % 85.04/11.86 | | | | all_78_28, simplifying with (1), (5), (10), (31), (32), % 85.04/11.86 | | | | (55) gives: % 85.04/11.86 | | | | (56) visFreeVar(all_78_32, all_78_27) % 85.04/11.86 | | | | % 85.04/11.86 | | | | GROUND_INST: instantiating (13) with all_78_32, all_78_27, simplifying % 85.04/11.86 | | | | with (1), (29), (32), (56) gives: % 85.04/11.86 | | | | (57) $false % 85.04/11.86 | | | | % 85.04/11.86 | | | | CLOSE: (57) is inconsistent. % 85.04/11.86 | | | | % 85.04/11.86 | | | End of split % 85.04/11.86 | | | % 85.04/11.86 | | Case 2: % 85.04/11.86 | | | % 85.04/11.86 | | | (58) all_78_32 = all_68_7 % 85.04/11.86 | | | % 85.04/11.86 | | | REDUCE: (28), (58) imply: % 85.04/11.86 | | | (59) $false % 85.04/11.86 | | | % 85.04/11.86 | | | CLOSE: (59) is inconsistent. % 85.04/11.86 | | | % 85.04/11.86 | | End of split % 85.04/11.86 | | % 85.04/11.86 | End of split % 85.04/11.86 | % 85.04/11.86 End of proof % 85.04/11.86 % SZS output end Proof for theBenchmark % 85.04/11.86 % 85.04/11.86 11253ms %------------------------------------------------------------------------------