%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM223_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 06:21:36 PM UTC 2026 % Result : Theorem 84.00s 11.68s % Output : Proof 123.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : COM223_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.31 % Computer : n021.cluster.edu % 0.13/0.31 % Model : x86_64 x86_64 % 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.31 % Memory : 8042.1875MB % 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Mon May 4 19:05:55 EDT 2026 % 0.13/0.32 % CPUTime : % 0.45/0.59 ________ _____ % 0.45/0.59 ___ __ \_________(_)________________________________ % 0.45/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.45/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.45/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.45/0.59 % 0.45/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.45/0.59 (2023-06-19) % 0.45/0.59 % 0.45/0.59 (c) Philipp Rümmer, 2009-2023 % 0.45/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.45/0.59 Amanda Stjerna. % 0.45/0.59 Free software under BSD-3-Clause. % 0.45/0.59 % 0.45/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.45/0.59 % 0.45/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.45/0.60 Running up to 7 provers in parallel. % 0.63/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.63/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.63/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.63/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.63/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.63/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.63/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.74/1.56 Prover 1: Preprocessing ... % 5.74/1.57 Prover 4: Preprocessing ... % 6.43/1.63 Prover 5: Preprocessing ... % 6.43/1.63 Prover 2: Preprocessing ... % 6.43/1.63 Prover 6: Preprocessing ... % 6.43/1.63 Prover 3: Preprocessing ... % 6.43/1.63 Prover 0: Preprocessing ... % 16.93/3.08 Prover 1: Warning: ignoring some quantifiers % 16.93/3.09 Prover 3: Warning: ignoring some quantifiers % 17.78/3.14 Prover 6: Proving ... % 17.78/3.14 Prover 3: Constructing countermodel ... % 17.78/3.14 Prover 1: Constructing countermodel ... % 19.04/3.31 Prover 5: Proving ... % 19.04/3.35 Prover 4: Warning: ignoring some quantifiers % 19.83/3.40 Prover 4: Constructing countermodel ... % 20.63/3.59 Prover 0: Proving ... % 23.64/3.93 Prover 2: Proving ... % 73.76/10.30 Prover 2: stopped % 73.76/10.32 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 75.34/10.50 Prover 7: Preprocessing ... % 77.70/10.80 Prover 7: Warning: ignoring some quantifiers % 77.70/10.83 Prover 7: Constructing countermodel ... % 84.00/11.68 Prover 5: proved (11063ms) % 84.00/11.68 % 84.00/11.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 84.00/11.68 % 84.00/11.69 Prover 3: stopped % 84.75/11.70 Prover 6: stopped % 84.75/11.71 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 84.75/11.71 Prover 0: stopped % 84.75/11.71 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 84.75/11.71 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 84.75/11.72 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 86.28/11.91 Prover 8: Preprocessing ... % 86.28/11.92 Prover 13: Preprocessing ... % 86.28/11.94 Prover 10: Preprocessing ... % 86.28/11.94 Prover 11: Preprocessing ... % 87.13/12.08 Prover 8: Warning: ignoring some quantifiers % 87.13/12.09 Prover 8: Constructing countermodel ... % 87.92/12.16 Prover 10: Warning: ignoring some quantifiers % 87.92/12.18 Prover 10: Constructing countermodel ... % 87.92/12.19 Prover 11: Warning: ignoring some quantifiers % 87.92/12.19 Prover 13: Warning: ignoring some quantifiers % 88.59/12.20 Prover 13: Constructing countermodel ... % 88.59/12.20 Prover 11: Constructing countermodel ... % 116.88/15.88 Prover 13: stopped % 116.88/15.88 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 117.67/15.98 Prover 1: stopped % 117.67/15.98 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 117.67/16.01 Prover 16: Preprocessing ... % 118.56/16.09 Prover 19: Preprocessing ... % 119.37/16.16 Prover 16: Warning: ignoring some quantifiers % 119.37/16.16 Prover 16: Constructing countermodel ... % 120.75/16.35 Prover 19: Warning: ignoring some quantifiers % 120.75/16.36 Prover 19: Constructing countermodel ... % 122.36/16.54 Prover 16: Found proof (size 75) % 122.36/16.54 Prover 16: proved (655ms) % 122.36/16.54 Prover 19: stopped % 122.36/16.54 Prover 7: stopped % 122.36/16.54 Prover 10: stopped % 122.36/16.54 Prover 8: stopped % 122.36/16.55 Prover 11: stopped % 122.36/16.58 Prover 4: stopped % 122.36/16.58 % 122.36/16.58 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 122.36/16.58 % 122.36/16.59 % SZS output start Proof for theBenchmark % 122.36/16.59 Assumptions after simplification: % 122.36/16.59 --------------------------------- % 122.36/16.59 % 122.36/16.59 (DIFF-B-Nat) % 122.36/16.59 ~ (vB = vNat) & vTy(vB) & vTy(vNat) % 122.36/16.59 % 122.36/16.59 (EQ-someTerm) % 122.95/16.62 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : (v1 = v0 | ~ % 122.95/16.62 (vsomeTerm(v1) = v2) | ~ (vsomeTerm(v0) = v2) | ~ vTerm(v1) | ~ % 122.95/16.62 vTerm(v0)) % 122.95/16.62 % 122.95/16.62 (Preservation-Plus-IH1) % 122.95/16.62 vTerm(vt2) & ? [v0: vOptTerm] : (vreduce(vt2) = v0 & vOptTerm(v0) & ! [v1: % 122.95/16.62 vTy] : ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ % 122.95/16.62 vTerm(v2) | ~ vptchecksimple(vt2, v1) | vptchecksimple(v2, v1))) % 122.95/16.62 % 122.95/16.62 (Preservation-Plus-isNV-True-isNV-False-isSomeTerm-True) % 122.95/16.62 vTerm(vt1) & vTerm(vt2) & ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: % 122.95/16.62 vOptTerm] : ? [v3: vTy] : ? [v4: vTerm] : (vreduce(v1) = v2 & vreduce(vt2) % 122.95/16.62 = v0 & vsomeTerm(v4) = v2 & vPlus(vt1, vt2) = v1 & vTy(v3) & vOptTerm(v2) & % 122.95/16.62 vOptTerm(v0) & vTerm(v4) & vTerm(v1) & vptchecksimple(v1, v3) & % 122.95/16.62 visSomeTerm(v0) & visNV(vt1) & ~ vptchecksimple(v4, v3) & ~ visNV(vt2)) % 122.95/16.62 % 122.95/16.62 (TPlus) % 122.95/16.62 vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, % 122.95/16.62 v1) = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v1, vNat) | % 122.95/16.62 ~ vptchecksimple(v0, vNat) | vptchecksimple(v2, vNat)) % 122.95/16.62 % 122.95/16.62 (TPlus_inv0) % 122.95/16.62 vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTy] : ! [v3: vTerm] : % 122.95/16.62 (v2 = vNat | ~ (vPlus(v0, v1) = v3) | ~ vTy(v2) | ~ vTerm(v1) | ~ % 122.95/16.62 vTerm(v0) | ~ vptchecksimple(v3, v2)) % 122.95/16.62 % 122.95/16.62 (TPlus_inv2) % 122.95/16.63 vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, % 122.95/16.63 v1) = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, vNat) | % 122.95/16.63 vptchecksimple(v1, vNat)) % 122.95/16.63 % 122.95/16.63 (TZero) % 122.95/16.63 vTy(vNat) & vTerm(vZero) & vptchecksimple(vZero, vNat) % 122.95/16.63 % 122.95/16.63 (TZero_inv) % 122.95/16.63 vTy(vNat) & vTerm(vZero) & ! [v0: vTy] : (v0 = vNat | ~ vTy(v0) | ~ % 122.95/16.63 vptchecksimple(vZero, v0)) % 122.95/16.63 % 122.95/16.63 (Tiszero) % 122.95/16.63 vTy(vB) & vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) % 122.95/16.63 | ~ vTerm(v0) | ~ vptchecksimple(v0, vNat) | vptchecksimple(v1, vB)) % 122.95/16.63 % 122.95/16.63 (Tiszero_inv2) % 122.95/16.63 vTy(vB) & ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vB | ~ % 122.95/16.63 (vIszero(v0) = v2) | ~ vTy(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, v1)) % 122.95/16.63 % 122.95/16.63 (getTerm-0) % 122.95/16.63 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vsomeTerm(v0) = v1) | ~ vTerm(v0) | % 122.95/16.63 vgetTerm(v1) = v0) % 122.95/16.63 % 122.95/16.63 (isNVisNat) % 122.95/16.63 vTy(vNat) & ! [v0: vTerm] : ( ~ vTerm(v0) | ~ visNV(v0) | vptchecksimple(v0, % 122.95/16.63 vNat)) % 122.95/16.63 % 122.95/16.63 (isSomeTerm-true-INV) % 122.95/16.63 ! [v0: vOptTerm] : ( ~ vOptTerm(v0) | ~ visSomeTerm(v0) | ? [v1: vTerm] : % 122.95/16.63 (vsomeTerm(v1) = v0 & vTerm(v1))) % 122.95/16.63 % 122.95/16.63 (reduce-12) % 122.95/16.63 vTerm(vTrue) & vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : % 122.95/16.63 (vreduce(v0) = v1 & vsomeTerm(vTrue) = v1 & vIszero(vZero) = v0 & vOptTerm(v1) % 122.95/16.63 & vTerm(v0)) % 122.95/16.63 % 122.95/16.63 (reduce-19) % 122.95/16.64 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = v2) | % 122.95/16.64 ~ vTerm(v1) | ~ vTerm(v0) | ~ visNV(v0) | visNV(v1) | ? [v3: vOptTerm] : % 122.95/16.64 ? [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : ? [v7: vOptTerm] : % 122.95/16.64 (vreduce(v1) = v3 & vOptTerm(v3) & ( ~ visSomeTerm(v3) | (v7 = v4 & % 122.95/16.64 vreduce(v2) = v4 & vgetTerm(v3) = v5 & vsomeTerm(v6) = v4 & vPlus(v0, % 122.95/16.64 v5) = v6 & vOptTerm(v4) & vTerm(v6) & vTerm(v5))))) % 122.95/16.64 % 122.95/16.64 (reduce-23) % 122.95/16.64 vOptTerm(vnoTerm) & vTerm(vFalse) & vTerm(vTrue) & vTerm(vZero) & ? [v0: % 122.95/16.64 vTerm] : ? [v1: vTerm] : (vIszero(vZero) = v1 & vPred(vZero) = v0 & % 122.95/16.64 vTerm(v1) & vTerm(v0) & ? [v2: vTerm] : (v2 = v1 | v2 = v0 | ~ vTerm(v2) | % 122.95/16.64 ? [v3: vOptTerm] : ? [v4: vTerm] : ? [v5: vTerm] : ? [v6: vTerm] : ? % 122.95/16.64 [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : ? [v10: vTerm] : ? [v11: % 122.95/16.64 vTerm] : ? [v12: vTerm] : ? [v13: vTerm] : ? [v14: vTerm] : ? [v15: % 122.95/16.64 vTerm] : ? [v16: vTerm] : ? [v17: vTerm] : ? [v18: vTerm] : ? [v19: % 122.95/16.64 vTerm] : ? [v20: vTerm] : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: % 122.95/16.64 vTerm] : ? [v24: vTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: % 122.95/16.64 vTerm] : ? [v28: vTerm] : (vTerm(v27) & vTerm(v26) & vTerm(v24) & % 122.95/16.64 vTerm(v23) & vTerm(v21) & vTerm(v20) & vTerm(v19) & vTerm(v17) & % 122.95/16.64 vTerm(v14) & vTerm(v12) & vTerm(v9) & vTerm(v7) & vTerm(v5) & vTerm(v4) % 122.95/16.64 & ((v28 = v2 & vIfelse(vTrue, v26, v27) = v2) | (v25 = v2 & % 122.95/16.64 vIfelse(vFalse, v23, v24) = v2) | (v22 = v2 & vIfelse(v19, v20, v21) % 122.95/16.64 = v2) | (v18 = v2 & vSucc(v17) = v2) | (v16 = v2 & vPred(v15) = v2 & % 122.95/16.64 vSucc(v14) = v15 & vTerm(v15)) | (v13 = v2 & vPred(v12) = v2) | (v11 % 122.95/16.64 = v2 & vIszero(v10) = v2 & vSucc(v9) = v10 & vTerm(v10)) | (v8 = v2 % 122.95/16.64 & vIszero(v7) = v2) | (v6 = v2 & vPlus(v4, v5) = v2) | (v3 = vnoTerm % 122.95/16.64 & vreduce(v2) = vnoTerm))))) % 122.95/16.64 % 122.95/16.64 (reduce-INV) % 122.95/16.66 vOptTerm(vnoTerm) & vTerm(vFalse) & vTerm(vTrue) & vTerm(vZero) & ? [v0: % 122.95/16.66 vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 122.95/16.66 vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 122.95/16.66 vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 122.95/16.66 vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & ? [v5: % 122.95/16.66 vTerm] : ( ~ vTerm(v5) | ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 122.95/16.66 vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: vOptTerm] : ? % 122.95/16.66 [v12: vTerm] : ? [v13: vTerm] : ? [v14: vTerm] : ? [v15: vOptTerm] : ? % 122.95/16.66 [v16: vOptTerm] : ? [v17: vTerm] : ? [v18: vTerm] : ? [v19: vTerm] : ? % 122.95/16.66 [v20: vOptTerm] : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : % 122.95/16.66 ? [v24: vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 122.95/16.66 ? [v28: vOptTerm] : ? [v29: vOptTerm] : ? [v30: vTerm] : ? [v31: % 122.95/16.66 vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: vTerm] : ? % 122.95/16.66 [v35: vTerm] : ? [v36: vTerm] : ? [v37: vTerm] : ? [v38: vOptTerm] : ? % 122.95/16.66 [v39: vTerm] : ? [v40: vOptTerm] : ? [v41: vOptTerm] : ? [v42: vTerm] : % 122.95/16.66 ? [v43: vTerm] : ? [v44: vOptTerm] : ? [v45: vOptTerm] : ? [v46: % 122.95/16.66 vTerm] : ? [v47: vTerm] : ? [v48: vTerm] : ? [v49: vOptTerm] : ? % 122.95/16.66 [v50: vTerm] : ? [v51: vOptTerm] : ? [v52: vTerm] : ? [v53: vOptTerm] : % 122.95/16.66 ? [v54: vTerm] : ? [v55: vTerm] : ? [v56: vOptTerm] : ? [v57: vTerm] : % 122.95/16.66 ? [v58: vOptTerm] : ? [v59: vTerm] : ? [v60: vTerm] : ? [v61: vTerm] : % 122.95/16.66 ? [v62: vOptTerm] : ? [v63: vTerm] : ? [v64: vTerm] : ? [v65: vTerm] : % 122.95/16.66 ? [v66: vTerm] : ? [v67: vOptTerm] : ? [v68: vOptTerm] : ? [v69: % 122.95/16.66 vTerm] : ? [v70: vTerm] : ? [v71: vOptTerm] : ? [v72: vOptTerm] : ? % 122.95/16.66 [v73: vTerm] : ? [v74: vTerm] : ? [v75: vTerm] : ? [v76: vOptTerm] : ? % 122.95/16.66 [v77: vTerm] : ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: vOptTerm] : % 122.95/16.66 ? [v81: vTerm] : ? [v82: vTerm] : ? [v83: vOptTerm] : ? [v84: vTerm] : % 122.95/16.66 ? [v85: vOptTerm] : ? [v86: vTerm] : ? [v87: vTerm] : ? [v88: vTerm] : % 122.95/16.66 ? [v89: vOptTerm] : ? [v90: vTerm] : ? [v91: vTerm] : ? [v92: vTerm] : % 122.95/16.66 ? [v93: vOptTerm] : ? [v94: vTerm] : ? [v95: vOptTerm] : ? [v96: % 122.95/16.66 vOptTerm] : ? [v97: vTerm] : ? [v98: vTerm] : ? [v99: vOptTerm] : ? % 122.95/16.66 [v100: vOptTerm] : ? [v101: vTerm] : ? [v102: vTerm] : ? [v103: vTerm] % 122.95/16.66 : ? [v104: vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: % 122.95/16.66 vTerm] : ? [v108: vOptTerm] : ? [v109: vOptTerm] : ? [v110: vTerm] : % 122.95/16.66 ? [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : ? [v114: % 122.95/16.66 vOptTerm] : ? [v115: vOptTerm] : ? [v116: vTerm] : ? [v117: vTerm] : % 122.95/16.66 ? [v118: vTerm] : ? [v119: vOptTerm] : ? [v120: vTerm] : ? [v121: % 122.95/16.66 vTerm] : ? [v122: vTerm] : ? [v123: vOptTerm] : ? [v124: vTerm] : ? % 122.95/16.66 [v125: vTerm] : ? [v126: vTerm] : ? [v127: vOptTerm] : (vreduce(v5) = v6 % 122.95/16.66 & vOptTerm(v114) & vOptTerm(v108) & vOptTerm(v99) & vOptTerm(v95) & % 122.95/16.66 vOptTerm(v83) & vOptTerm(v78) & vOptTerm(v71) & vOptTerm(v67) & % 122.95/16.66 vOptTerm(v56) & vOptTerm(v51) & vOptTerm(v44) & vOptTerm(v40) & % 122.95/16.66 vOptTerm(v28) & vOptTerm(v23) & vOptTerm(v15) & vOptTerm(v10) & % 122.95/16.66 vOptTerm(v6) & vTerm(v125) & vTerm(v124) & vTerm(v121) & vTerm(v120) & % 122.95/16.66 vTerm(v113) & vTerm(v112) & vTerm(v111) & vTerm(v107) & vTerm(v106) & % 122.95/16.66 vTerm(v105) & vTerm(v98) & vTerm(v94) & vTerm(v90) & vTerm(v82) & % 122.95/16.66 vTerm(v77) & vTerm(v70) & vTerm(v66) & vTerm(v63) & vTerm(v55) & % 122.95/16.66 vTerm(v50) & vTerm(v43) & vTerm(v39) & vTerm(v35) & vTerm(v34) & % 122.95/16.66 vTerm(v27) & vTerm(v26) & vTerm(v22) & vTerm(v21) & vTerm(v14) & % 122.95/16.66 vTerm(v13) & vTerm(v9) & vTerm(v8) & vTerm(v7) & ((v127 = v6 & v126 = v5 % 122.95/16.66 & vsomeTerm(v124) = v6 & vIfelse(vTrue, v124, v125) = v5) | (v123 = % 122.95/16.66 v6 & v122 = v5 & vsomeTerm(v121) = v6 & vIfelse(vFalse, v120, v121) % 122.95/16.66 = v5) | (v119 = v6 & v116 = v5 & v115 = v114 & ~ (v111 = vFalse) & % 122.95/16.66 ~ (v111 = vTrue) & vreduce(v111) = v114 & vgetTerm(v114) = v117 & % 122.95/16.66 vsomeTerm(v118) = v6 & vIfelse(v117, v112, v113) = v118 & % 122.95/16.66 vIfelse(v111, v112, v113) = v5 & vTerm(v118) & vTerm(v117) & % 122.95/16.67 visSomeTerm(v114)) | (v110 = v5 & v109 = v108 & v6 = vnoTerm & ~ % 122.95/16.67 (v105 = vFalse) & ~ (v105 = vTrue) & vreduce(v105) = v108 & % 122.95/16.67 vIfelse(v105, v106, v107) = v5 & ~ visSomeTerm(v108)) | (v104 = v6 % 122.95/16.67 & v101 = v5 & v100 = v99 & vreduce(v98) = v99 & vgetTerm(v99) = v102 % 122.95/16.67 & vsomeTerm(v103) = v6 & vSucc(v102) = v103 & vSucc(v98) = v5 & % 122.95/16.67 vTerm(v103) & vTerm(v102) & visSomeTerm(v99)) | (v97 = v5 & v96 = % 122.95/16.67 v95 & v6 = vnoTerm & vreduce(v94) = v95 & vSucc(v94) = v5 & ~ % 122.95/16.67 visSomeTerm(v95)) | (v93 = v6 & v92 = v5 & vsomeTerm(v90) = v6 & % 122.95/16.67 vPred(v91) = v5 & vSucc(v90) = v91 & vTerm(v91) & visNV(v90)) | (v89 % 122.95/16.67 = v6 & v86 = v5 & v85 = v83 & vreduce(v84) = v83 & vgetTerm(v83) = % 122.95/16.67 v87 & vsomeTerm(v88) = v6 & vPred(v87) = v88 & vPred(v84) = v5 & % 122.95/16.67 vSucc(v82) = v84 & vTerm(v88) & vTerm(v87) & vTerm(v84) & % 122.95/16.67 visSomeTerm(v83) & ~ visNV(v82)) | (v81 = v5 & v80 = v78 & v6 = % 122.95/16.67 vnoTerm & vreduce(v79) = v78 & vPred(v79) = v5 & vSucc(v77) = v79 & % 122.95/16.67 vTerm(v79) & ~ visSomeTerm(v78) & ~ visNV(v77)) | (v76 = v6 & v73 % 122.95/16.67 = v5 & v72 = v71 & ~ (v70 = vZero) & vreduce(v70) = v71 & % 122.95/16.67 vgetTerm(v71) = v74 & vsomeTerm(v75) = v6 & vPred(v74) = v75 & % 122.95/16.67 vPred(v70) = v5 & vTerm(v75) & vTerm(v74) & visSomeTerm(v71) & ! % 122.95/16.67 [v128: vTerm] : ( ~ (vSucc(v128) = v70) | ~ vTerm(v128))) | (v69 = % 122.95/16.67 v5 & v68 = v67 & v6 = vnoTerm & ~ (v66 = vZero) & vreduce(v66) = % 122.95/16.67 v67 & vPred(v66) = v5 & ~ visSomeTerm(v67) & ! [v128: vTerm] : ( ~ % 122.95/16.67 (vSucc(v128) = v66) | ~ vTerm(v128))) | (v65 = v5 & v6 = v4 & % 122.95/16.67 vIszero(v64) = v5 & vSucc(v63) = v64 & vTerm(v64) & visNV(v63)) | % 122.95/16.67 (v62 = v6 & v59 = v5 & v58 = v56 & vreduce(v57) = v56 & vgetTerm(v56) % 122.95/16.67 = v60 & vsomeTerm(v61) = v6 & vIszero(v60) = v61 & vIszero(v57) = v5 % 122.95/16.67 & vSucc(v55) = v57 & vTerm(v61) & vTerm(v60) & vTerm(v57) & % 122.95/16.67 visSomeTerm(v56) & ~ visNV(v55)) | (v54 = v5 & v53 = v51 & v6 = % 122.95/16.67 vnoTerm & vreduce(v52) = v51 & vIszero(v52) = v5 & vSucc(v50) = v52 % 122.95/16.67 & vTerm(v52) & ~ visSomeTerm(v51) & ~ visNV(v50)) | (v49 = v6 & % 122.95/16.67 v46 = v5 & v45 = v44 & ~ (v43 = vZero) & vreduce(v43) = v44 & % 122.95/16.67 vgetTerm(v44) = v47 & vsomeTerm(v48) = v6 & vIszero(v47) = v48 & % 122.95/16.67 vIszero(v43) = v5 & vTerm(v48) & vTerm(v47) & visSomeTerm(v44) & ! % 122.95/16.67 [v128: vTerm] : ( ~ (vSucc(v128) = v43) | ~ vTerm(v128))) | (v42 = % 122.95/16.67 v5 & v41 = v40 & v6 = vnoTerm & ~ (v39 = vZero) & vreduce(v39) = % 122.95/16.67 v40 & vIszero(v39) = v5 & ~ visSomeTerm(v40) & ! [v128: vTerm] : ( % 122.95/16.67 ~ (vSucc(v128) = v39) | ~ vTerm(v128))) | (v38 = v6 & v36 = v5 & % 122.95/16.67 vplusop(v34, v35) = v37 & vsomeTerm(v37) = v6 & vPlus(v34, v35) = v5 % 122.95/16.67 & vTerm(v37) & visNV(v35) & visNV(v34)) | (v33 = v6 & v30 = v5 & v29 % 122.95/16.67 = v28 & vreduce(v27) = v28 & vgetTerm(v28) = v31 & vsomeTerm(v32) = % 122.95/16.67 v6 & vPlus(v26, v31) = v32 & vPlus(v26, v27) = v5 & vTerm(v32) & % 122.95/16.67 vTerm(v31) & visSomeTerm(v28) & visNV(v26) & ~ visNV(v27)) | (v25 = % 122.95/16.67 v5 & v24 = v23 & v6 = vnoTerm & vreduce(v22) = v23 & vPlus(v21, v22) % 122.95/16.67 = v5 & visNV(v21) & ~ visSomeTerm(v23) & ~ visNV(v22)) | (v20 = v6 % 122.95/16.67 & v17 = v5 & v16 = v15 & vreduce(v13) = v15 & vgetTerm(v15) = v18 & % 122.95/16.67 vsomeTerm(v19) = v6 & vPlus(v18, v14) = v19 & vPlus(v13, v14) = v5 & % 122.95/16.67 vTerm(v19) & vTerm(v18) & visSomeTerm(v15) & ~ visNV(v13)) | (v12 = % 122.95/16.67 v5 & v11 = v10 & v6 = vnoTerm & vreduce(v8) = v10 & vPlus(v8, v9) = % 122.95/16.67 v5 & ~ visSomeTerm(v10) & ~ visNV(v8)) | (v7 = v5 & v6 = vnoTerm & % 122.95/16.67 ~ (v5 = v2) & ~ (v5 = v0) & ! [v128: vTerm] : ! [v129: vTerm] : % 122.95/16.67 ! [v130: vTerm] : ( ~ (vIfelse(v128, v129, v130) = v5) | ~ % 122.95/16.67 vTerm(v130) | ~ vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] % 122.95/16.67 : ! [v129: vTerm] : ( ~ (vPlus(v128, v129) = v5) | ~ vTerm(v129) | % 122.95/16.67 ~ vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 122.95/16.67 (vSucc(v128) = v129) | ~ vTerm(v128) | ? [v130: vTerm] : ( ~ % 122.95/16.67 (v130 = v5) & vIszero(v129) = v130 & vTerm(v130))) & ! [v128: % 122.95/16.67 vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = v129) | ~ % 122.95/16.67 vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = v5) & vPred(v129) = % 122.95/16.67 v130 & vTerm(v130))) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 122.95/16.67 (vIfelse(vFalse, v128, v129) = v5) | ~ vTerm(v129) | ~ % 122.95/16.67 vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 122.95/16.67 (vIfelse(vTrue, v128, v129) = v5) | ~ vTerm(v129) | ~ % 122.95/16.67 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vIszero(v128) = v5) | ~ % 122.95/16.67 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vPred(v128) = v5) | ~ % 122.95/16.67 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vSucc(v128) = v5) | ~ % 122.95/16.67 vTerm(v128))) | (v6 = v3 & v5 = v2) | (v6 = v1 & v5 = v0))))) % 122.95/16.67 % 122.95/16.67 (function-axioms) % 122.95/16.67 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 122.95/16.67 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 122.95/16.67 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] % 122.95/16.67 : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ (vplusop(v3, v2) = v0)) & ! [v0: % 122.95/16.67 vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ % 122.95/16.67 (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) & ! [v0: vOptTerm] : ! % 122.95/16.67 [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vreduce(v2) = v1) | ~ % 122.95/16.67 (vreduce(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 122.95/16.67 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 122.95/16.67 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 122.95/16.67 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 122.95/16.67 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 122.95/16.67 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 122.95/16.67 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 122.95/16.67 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 122.95/16.67 % 122.95/16.67 Further assumptions not needed in the proof: % 122.95/16.67 -------------------------------------------- % 122.95/16.67 DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, DIFF-False-Pred, % 122.95/16.67 DIFF-False-Succ, DIFF-False-Zero, DIFF-Ifelse-Iszero, DIFF-Ifelse-Plus, % 122.95/16.67 DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, DIFF-Iszero-Plus, % 122.95/16.67 DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, DIFF-Succ-Plus, % 122.95/16.67 DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, DIFF-True-Iszero, % 122.95/16.67 DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, DIFF-True-Zero, % 122.95/16.67 DIFF-Zero-Iszero, DIFF-Zero-Plus, DIFF-Zero-Pred, DIFF-Zero-Succ, % 122.95/16.67 DIFF-noTerm-someTerm, EQ-Ifelse, EQ-Iszero, EQ-Plus, EQ-Pred, EQ-Succ, % 122.95/16.67 Preservation-Plus-IH0, TPlus_inv1, TPred, TPred_inv1, TPred_inv2, TSucc, % 122.95/16.67 TSucc_inv1, TSucc_inv2, Tfalse, Tif, Tif_inv1, Tif_inv2, Tif_inv3, Tiszero_inv1, % 122.95/16.67 Ttrue, dom-OptTerm, dom-Term, dom-Ty, isNV-0, isNV-1, isNV-2, isNV-false-INV, % 122.95/16.67 isNV-true-INV, isSomeTerm-0, isSomeTerm-1, isSomeTerm-false-INV, isValue-0, % 122.95/16.67 isValue-1, isValue-2, isValue-false-INV, isValue-true-INV, plusop-0, plusop-1, % 122.95/16.67 plusop-2, plusop-INV, reduce-0, reduce-1, reduce-10, reduce-11, reduce-13, % 122.95/16.67 reduce-14, reduce-15, reduce-16, reduce-17, reduce-18, reduce-2, reduce-20, % 122.95/16.67 reduce-21, reduce-22, reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, % 122.95/16.67 reduce-8, reduce-9 % 122.95/16.67 % 122.95/16.67 Those formulas are unsatisfiable: % 122.95/16.67 --------------------------------- % 122.95/16.67 % 122.95/16.67 Begin of proof % 122.95/16.67 | % 122.95/16.67 | ALPHA: (DIFF-B-Nat) implies: % 122.95/16.67 | (1) ~ (vB = vNat) % 122.95/16.67 | % 122.95/16.67 | ALPHA: (reduce-12) implies: % 122.95/16.67 | (2) ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 122.95/16.67 | vsomeTerm(vTrue) = v1 & vIszero(vZero) = v0 & vOptTerm(v1) & % 122.95/16.67 | vTerm(v0)) % 122.95/16.67 | % 122.95/16.67 | ALPHA: (reduce-23) implies: % 122.95/16.68 | (3) ? [v0: vTerm] : ? [v1: vTerm] : (vIszero(vZero) = v1 & vPred(vZero) = % 122.95/16.68 | v0 & vTerm(v1) & vTerm(v0) & ? [v2: vTerm] : (v2 = v1 | v2 = v0 | ~ % 122.95/16.68 | vTerm(v2) | ? [v3: vOptTerm] : ? [v4: vTerm] : ? [v5: vTerm] : % 122.95/16.68 | ? [v6: vTerm] : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : % 122.95/16.68 | ? [v10: vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : ? [v13: % 122.95/16.68 | vTerm] : ? [v14: vTerm] : ? [v15: vTerm] : ? [v16: vTerm] : ? % 122.95/16.68 | [v17: vTerm] : ? [v18: vTerm] : ? [v19: vTerm] : ? [v20: vTerm] % 122.95/16.68 | : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: vTerm] : ? [v24: % 122.95/16.68 | vTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : ? % 122.95/16.68 | [v28: vTerm] : (vTerm(v27) & vTerm(v26) & vTerm(v24) & vTerm(v23) & % 122.95/16.68 | vTerm(v21) & vTerm(v20) & vTerm(v19) & vTerm(v17) & vTerm(v14) & % 122.95/16.68 | vTerm(v12) & vTerm(v9) & vTerm(v7) & vTerm(v5) & vTerm(v4) & % 122.95/16.68 | ((v28 = v2 & vIfelse(vTrue, v26, v27) = v2) | (v25 = v2 & % 122.95/16.68 | vIfelse(vFalse, v23, v24) = v2) | (v22 = v2 & vIfelse(v19, % 122.95/16.68 | v20, v21) = v2) | (v18 = v2 & vSucc(v17) = v2) | (v16 = v2 % 122.95/16.68 | & vPred(v15) = v2 & vSucc(v14) = v15 & vTerm(v15)) | (v13 = % 122.95/16.68 | v2 & vPred(v12) = v2) | (v11 = v2 & vIszero(v10) = v2 & % 122.95/16.68 | vSucc(v9) = v10 & vTerm(v10)) | (v8 = v2 & vIszero(v7) = v2) % 122.95/16.68 | | (v6 = v2 & vPlus(v4, v5) = v2) | (v3 = vnoTerm & vreduce(v2) % 122.95/16.68 | = vnoTerm))))) % 122.95/16.68 | % 122.95/16.68 | ALPHA: (reduce-INV) implies: % 122.95/16.70 | (4) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] % 122.95/16.70 | : ? [v4: vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 122.95/16.70 | vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 122.95/16.70 | vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & % 123.42/16.70 | ? [v5: vTerm] : ( ~ vTerm(v5) | ? [v6: vOptTerm] : ? [v7: vTerm] : % 123.42/16.70 | ? [v8: vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: % 123.42/16.70 | vOptTerm] : ? [v12: vTerm] : ? [v13: vTerm] : ? [v14: vTerm] : % 123.42/16.70 | ? [v15: vOptTerm] : ? [v16: vOptTerm] : ? [v17: vTerm] : ? % 123.42/16.70 | [v18: vTerm] : ? [v19: vTerm] : ? [v20: vOptTerm] : ? [v21: % 123.42/16.70 | vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : ? [v24: % 123.42/16.70 | vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 123.42/16.70 | ? [v28: vOptTerm] : ? [v29: vOptTerm] : ? [v30: vTerm] : ? % 123.42/16.70 | [v31: vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: % 123.42/16.70 | vTerm] : ? [v35: vTerm] : ? [v36: vTerm] : ? [v37: vTerm] : ? % 123.42/16.70 | [v38: vOptTerm] : ? [v39: vTerm] : ? [v40: vOptTerm] : ? [v41: % 123.42/16.70 | vOptTerm] : ? [v42: vTerm] : ? [v43: vTerm] : ? [v44: % 123.42/16.70 | vOptTerm] : ? [v45: vOptTerm] : ? [v46: vTerm] : ? [v47: % 123.42/16.70 | vTerm] : ? [v48: vTerm] : ? [v49: vOptTerm] : ? [v50: vTerm] : % 123.42/16.70 | ? [v51: vOptTerm] : ? [v52: vTerm] : ? [v53: vOptTerm] : ? % 123.42/16.70 | [v54: vTerm] : ? [v55: vTerm] : ? [v56: vOptTerm] : ? [v57: % 123.42/16.70 | vTerm] : ? [v58: vOptTerm] : ? [v59: vTerm] : ? [v60: vTerm] : % 123.42/16.70 | ? [v61: vTerm] : ? [v62: vOptTerm] : ? [v63: vTerm] : ? [v64: % 123.42/16.70 | vTerm] : ? [v65: vTerm] : ? [v66: vTerm] : ? [v67: vOptTerm] : % 123.42/16.70 | ? [v68: vOptTerm] : ? [v69: vTerm] : ? [v70: vTerm] : ? [v71: % 123.42/16.70 | vOptTerm] : ? [v72: vOptTerm] : ? [v73: vTerm] : ? [v74: % 123.42/16.70 | vTerm] : ? [v75: vTerm] : ? [v76: vOptTerm] : ? [v77: vTerm] : % 123.42/16.70 | ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: vOptTerm] : ? % 123.42/16.70 | [v81: vTerm] : ? [v82: vTerm] : ? [v83: vOptTerm] : ? [v84: % 123.42/16.70 | vTerm] : ? [v85: vOptTerm] : ? [v86: vTerm] : ? [v87: vTerm] : % 123.42/16.70 | ? [v88: vTerm] : ? [v89: vOptTerm] : ? [v90: vTerm] : ? [v91: % 123.42/16.70 | vTerm] : ? [v92: vTerm] : ? [v93: vOptTerm] : ? [v94: vTerm] : % 123.42/16.70 | ? [v95: vOptTerm] : ? [v96: vOptTerm] : ? [v97: vTerm] : ? % 123.42/16.70 | [v98: vTerm] : ? [v99: vOptTerm] : ? [v100: vOptTerm] : ? [v101: % 123.42/16.70 | vTerm] : ? [v102: vTerm] : ? [v103: vTerm] : ? [v104: % 123.42/16.70 | vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: % 123.42/16.70 | vTerm] : ? [v108: vOptTerm] : ? [v109: vOptTerm] : ? [v110: % 123.42/16.70 | vTerm] : ? [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : % 123.42/16.70 | ? [v114: vOptTerm] : ? [v115: vOptTerm] : ? [v116: vTerm] : ? % 123.42/16.70 | [v117: vTerm] : ? [v118: vTerm] : ? [v119: vOptTerm] : ? [v120: % 123.42/16.70 | vTerm] : ? [v121: vTerm] : ? [v122: vTerm] : ? [v123: % 123.42/16.70 | vOptTerm] : ? [v124: vTerm] : ? [v125: vTerm] : ? [v126: % 123.42/16.70 | vTerm] : ? [v127: vOptTerm] : (vreduce(v5) = v6 & vOptTerm(v114) % 123.42/16.70 | & vOptTerm(v108) & vOptTerm(v99) & vOptTerm(v95) & vOptTerm(v83) % 123.42/16.70 | & vOptTerm(v78) & vOptTerm(v71) & vOptTerm(v67) & vOptTerm(v56) & % 123.42/16.70 | vOptTerm(v51) & vOptTerm(v44) & vOptTerm(v40) & vOptTerm(v28) & % 123.42/16.70 | vOptTerm(v23) & vOptTerm(v15) & vOptTerm(v10) & vOptTerm(v6) & % 123.42/16.70 | vTerm(v125) & vTerm(v124) & vTerm(v121) & vTerm(v120) & % 123.42/16.70 | vTerm(v113) & vTerm(v112) & vTerm(v111) & vTerm(v107) & % 123.42/16.70 | vTerm(v106) & vTerm(v105) & vTerm(v98) & vTerm(v94) & vTerm(v90) % 123.42/16.70 | & vTerm(v82) & vTerm(v77) & vTerm(v70) & vTerm(v66) & vTerm(v63) % 123.42/16.70 | & vTerm(v55) & vTerm(v50) & vTerm(v43) & vTerm(v39) & vTerm(v35) % 123.42/16.70 | & vTerm(v34) & vTerm(v27) & vTerm(v26) & vTerm(v22) & vTerm(v21) % 123.42/16.70 | & vTerm(v14) & vTerm(v13) & vTerm(v9) & vTerm(v8) & vTerm(v7) & % 123.42/16.70 | ((v127 = v6 & v126 = v5 & vsomeTerm(v124) = v6 & vIfelse(vTrue, % 123.42/16.70 | v124, v125) = v5) | (v123 = v6 & v122 = v5 & % 123.42/16.70 | vsomeTerm(v121) = v6 & vIfelse(vFalse, v120, v121) = v5) | % 123.42/16.70 | (v119 = v6 & v116 = v5 & v115 = v114 & ~ (v111 = vFalse) & ~ % 123.42/16.70 | (v111 = vTrue) & vreduce(v111) = v114 & vgetTerm(v114) = v117 % 123.42/16.70 | & vsomeTerm(v118) = v6 & vIfelse(v117, v112, v113) = v118 & % 123.42/16.70 | vIfelse(v111, v112, v113) = v5 & vTerm(v118) & vTerm(v117) & % 123.42/16.70 | visSomeTerm(v114)) | (v110 = v5 & v109 = v108 & v6 = vnoTerm % 123.42/16.70 | & ~ (v105 = vFalse) & ~ (v105 = vTrue) & vreduce(v105) = % 123.42/16.70 | v108 & vIfelse(v105, v106, v107) = v5 & ~ visSomeTerm(v108)) % 123.42/16.70 | | (v104 = v6 & v101 = v5 & v100 = v99 & vreduce(v98) = v99 & % 123.42/16.70 | vgetTerm(v99) = v102 & vsomeTerm(v103) = v6 & vSucc(v102) = % 123.42/16.70 | v103 & vSucc(v98) = v5 & vTerm(v103) & vTerm(v102) & % 123.42/16.70 | visSomeTerm(v99)) | (v97 = v5 & v96 = v95 & v6 = vnoTerm & % 123.42/16.70 | vreduce(v94) = v95 & vSucc(v94) = v5 & ~ visSomeTerm(v95)) | % 123.42/16.70 | (v93 = v6 & v92 = v5 & vsomeTerm(v90) = v6 & vPred(v91) = v5 & % 123.42/16.70 | vSucc(v90) = v91 & vTerm(v91) & visNV(v90)) | (v89 = v6 & v86 % 123.42/16.70 | = v5 & v85 = v83 & vreduce(v84) = v83 & vgetTerm(v83) = v87 & % 123.42/16.70 | vsomeTerm(v88) = v6 & vPred(v87) = v88 & vPred(v84) = v5 & % 123.42/16.70 | vSucc(v82) = v84 & vTerm(v88) & vTerm(v87) & vTerm(v84) & % 123.42/16.70 | visSomeTerm(v83) & ~ visNV(v82)) | (v81 = v5 & v80 = v78 & % 123.42/16.70 | v6 = vnoTerm & vreduce(v79) = v78 & vPred(v79) = v5 & % 123.42/16.70 | vSucc(v77) = v79 & vTerm(v79) & ~ visSomeTerm(v78) & ~ % 123.42/16.70 | visNV(v77)) | (v76 = v6 & v73 = v5 & v72 = v71 & ~ (v70 = % 123.42/16.70 | vZero) & vreduce(v70) = v71 & vgetTerm(v71) = v74 & % 123.42/16.70 | vsomeTerm(v75) = v6 & vPred(v74) = v75 & vPred(v70) = v5 & % 123.42/16.70 | vTerm(v75) & vTerm(v74) & visSomeTerm(v71) & ! [v128: vTerm] % 123.42/16.70 | : ( ~ (vSucc(v128) = v70) | ~ vTerm(v128))) | (v69 = v5 & % 123.42/16.70 | v68 = v67 & v6 = vnoTerm & ~ (v66 = vZero) & vreduce(v66) = % 123.42/16.70 | v67 & vPred(v66) = v5 & ~ visSomeTerm(v67) & ! [v128: % 123.42/16.70 | vTerm] : ( ~ (vSucc(v128) = v66) | ~ vTerm(v128))) | (v65 % 123.42/16.70 | = v5 & v6 = v4 & vIszero(v64) = v5 & vSucc(v63) = v64 & % 123.42/16.70 | vTerm(v64) & visNV(v63)) | (v62 = v6 & v59 = v5 & v58 = v56 & % 123.42/16.70 | vreduce(v57) = v56 & vgetTerm(v56) = v60 & vsomeTerm(v61) = % 123.42/16.70 | v6 & vIszero(v60) = v61 & vIszero(v57) = v5 & vSucc(v55) = % 123.42/16.70 | v57 & vTerm(v61) & vTerm(v60) & vTerm(v57) & visSomeTerm(v56) % 123.42/16.70 | & ~ visNV(v55)) | (v54 = v5 & v53 = v51 & v6 = vnoTerm & % 123.42/16.70 | vreduce(v52) = v51 & vIszero(v52) = v5 & vSucc(v50) = v52 & % 123.42/16.70 | vTerm(v52) & ~ visSomeTerm(v51) & ~ visNV(v50)) | (v49 = v6 % 123.42/16.70 | & v46 = v5 & v45 = v44 & ~ (v43 = vZero) & vreduce(v43) = % 123.42/16.70 | v44 & vgetTerm(v44) = v47 & vsomeTerm(v48) = v6 & % 123.42/16.70 | vIszero(v47) = v48 & vIszero(v43) = v5 & vTerm(v48) & % 123.42/16.70 | vTerm(v47) & visSomeTerm(v44) & ! [v128: vTerm] : ( ~ % 123.42/16.70 | (vSucc(v128) = v43) | ~ vTerm(v128))) | (v42 = v5 & v41 = % 123.42/16.70 | v40 & v6 = vnoTerm & ~ (v39 = vZero) & vreduce(v39) = v40 & % 123.42/16.70 | vIszero(v39) = v5 & ~ visSomeTerm(v40) & ! [v128: vTerm] : % 123.42/16.70 | ( ~ (vSucc(v128) = v39) | ~ vTerm(v128))) | (v38 = v6 & v36 % 123.42/16.70 | = v5 & vplusop(v34, v35) = v37 & vsomeTerm(v37) = v6 & % 123.42/16.70 | vPlus(v34, v35) = v5 & vTerm(v37) & visNV(v35) & visNV(v34)) % 123.42/16.70 | | (v33 = v6 & v30 = v5 & v29 = v28 & vreduce(v27) = v28 & % 123.42/16.70 | vgetTerm(v28) = v31 & vsomeTerm(v32) = v6 & vPlus(v26, v31) = % 123.42/16.70 | v32 & vPlus(v26, v27) = v5 & vTerm(v32) & vTerm(v31) & % 123.42/16.70 | visSomeTerm(v28) & visNV(v26) & ~ visNV(v27)) | (v25 = v5 & % 123.42/16.70 | v24 = v23 & v6 = vnoTerm & vreduce(v22) = v23 & vPlus(v21, % 123.42/16.70 | v22) = v5 & visNV(v21) & ~ visSomeTerm(v23) & ~ % 123.42/16.70 | visNV(v22)) | (v20 = v6 & v17 = v5 & v16 = v15 & vreduce(v13) % 123.42/16.70 | = v15 & vgetTerm(v15) = v18 & vsomeTerm(v19) = v6 & % 123.42/16.70 | vPlus(v18, v14) = v19 & vPlus(v13, v14) = v5 & vTerm(v19) & % 123.42/16.70 | vTerm(v18) & visSomeTerm(v15) & ~ visNV(v13)) | (v12 = v5 & % 123.42/16.70 | v11 = v10 & v6 = vnoTerm & vreduce(v8) = v10 & vPlus(v8, v9) % 123.42/16.70 | = v5 & ~ visSomeTerm(v10) & ~ visNV(v8)) | (v7 = v5 & v6 = % 123.42/16.70 | vnoTerm & ~ (v5 = v2) & ~ (v5 = v0) & ! [v128: vTerm] : ! % 123.42/16.70 | [v129: vTerm] : ! [v130: vTerm] : ( ~ (vIfelse(v128, v129, % 123.42/16.70 | v130) = v5) | ~ vTerm(v130) | ~ vTerm(v129) | ~ % 123.42/16.70 | vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 123.42/16.70 | (vPlus(v128, v129) = v5) | ~ vTerm(v129) | ~ vTerm(v128)) % 123.42/16.70 | & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = % 123.42/16.70 | v129) | ~ vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = % 123.42/16.70 | v5) & vIszero(v129) = v130 & vTerm(v130))) & ! [v128: % 123.42/16.70 | vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = v129) | ~ % 123.42/16.70 | vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = v5) & % 123.42/16.70 | vPred(v129) = v130 & vTerm(v130))) & ! [v128: vTerm] : % 123.42/16.70 | ! [v129: vTerm] : ( ~ (vIfelse(vFalse, v128, v129) = v5) | ~ % 123.42/16.70 | vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] : ! % 123.42/16.70 | [v129: vTerm] : ( ~ (vIfelse(vTrue, v128, v129) = v5) | ~ % 123.42/16.70 | vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] : ( ~ % 123.42/16.70 | (vIszero(v128) = v5) | ~ vTerm(v128)) & ! [v128: vTerm] : % 123.42/16.70 | ( ~ (vPred(v128) = v5) | ~ vTerm(v128)) & ! [v128: vTerm] : % 123.42/16.70 | ( ~ (vSucc(v128) = v5) | ~ vTerm(v128))) | (v6 = v3 & v5 = % 123.42/16.70 | v2) | (v6 = v1 & v5 = v0))))) % 123.42/16.70 | % 123.42/16.70 | ALPHA: (TZero) implies: % 123.42/16.70 | (5) vptchecksimple(vZero, vNat) % 123.42/16.70 | % 123.42/16.70 | ALPHA: (TZero_inv) implies: % 123.42/16.70 | (6) vTerm(vZero) % 123.42/16.70 | % 123.42/16.70 | ALPHA: (Tiszero) implies: % 123.42/16.70 | (7) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) | ~ vTerm(v0) % 123.42/16.70 | | ~ vptchecksimple(v0, vNat) | vptchecksimple(v1, vB)) % 123.42/16.70 | % 123.42/16.70 | ALPHA: (Tiszero_inv2) implies: % 123.42/16.70 | (8) vTy(vB) % 123.42/16.70 | % 123.42/16.70 | ALPHA: (TPlus) implies: % 123.42/16.70 | (9) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = % 123.42/16.70 | v2) | ~ vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v1, vNat) | % 123.42/16.70 | ~ vptchecksimple(v0, vNat) | vptchecksimple(v2, vNat)) % 123.42/16.70 | % 123.42/16.70 | ALPHA: (TPlus_inv0) implies: % 123.42/16.70 | (10) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTy] : ! [v3: vTerm] : (v2 % 123.42/16.70 | = vNat | ~ (vPlus(v0, v1) = v3) | ~ vTy(v2) | ~ vTerm(v1) | ~ % 123.42/16.70 | vTerm(v0) | ~ vptchecksimple(v3, v2)) % 123.42/16.70 | % 123.42/16.70 | ALPHA: (TPlus_inv2) implies: % 123.42/16.71 | (11) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) % 123.42/16.71 | = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, vNat) % 123.42/16.71 | | vptchecksimple(v1, vNat)) % 123.42/16.71 | % 123.42/16.71 | ALPHA: (Preservation-Plus-IH1) implies: % 123.42/16.71 | (12) ? [v0: vOptTerm] : (vreduce(vt2) = v0 & vOptTerm(v0) & ! [v1: vTy] : % 123.42/16.71 | ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ % 123.42/16.71 | vTerm(v2) | ~ vptchecksimple(vt2, v1) | vptchecksimple(v2, v1))) % 123.42/16.71 | % 123.42/16.71 | ALPHA: (isNVisNat) implies: % 123.42/16.71 | (13) ! [v0: vTerm] : ( ~ vTerm(v0) | ~ visNV(v0) | vptchecksimple(v0, % 123.42/16.71 | vNat)) % 123.42/16.71 | % 123.42/16.71 | ALPHA: (Preservation-Plus-isNV-True-isNV-False-isSomeTerm-True) implies: % 123.42/16.71 | (14) vTerm(vt2) % 123.42/16.71 | (15) vTerm(vt1) % 123.42/16.71 | (16) ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: vOptTerm] : ? [v3: vTy] % 123.42/16.71 | : ? [v4: vTerm] : (vreduce(v1) = v2 & vreduce(vt2) = v0 & % 123.42/16.71 | vsomeTerm(v4) = v2 & vPlus(vt1, vt2) = v1 & vTy(v3) & vOptTerm(v2) & % 123.42/16.71 | vOptTerm(v0) & vTerm(v4) & vTerm(v1) & vptchecksimple(v1, v3) & % 123.42/16.71 | visSomeTerm(v0) & visNV(vt1) & ~ vptchecksimple(v4, v3) & ~ % 123.42/16.71 | visNV(vt2)) % 123.42/16.71 | % 123.42/16.71 | ALPHA: (function-axioms) implies: % 123.42/16.71 | (17) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 123.42/16.71 | (vIszero(v2) = v1) | ~ (vIszero(v2) = v0)) % 123.42/16.71 | (18) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : (v1 = v0 | ~ % 123.42/16.71 | (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) % 123.42/16.71 | (19) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 123.42/16.71 | (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) % 123.42/16.71 | % 123.42/16.71 | DELTA: instantiating (2) with fresh symbols all_93_0, all_93_1 gives: % 123.42/16.71 | (20) vreduce(all_93_1) = all_93_0 & vsomeTerm(vTrue) = all_93_0 & % 123.42/16.71 | vIszero(vZero) = all_93_1 & vOptTerm(all_93_0) & vTerm(all_93_1) % 123.42/16.71 | % 123.42/16.71 | ALPHA: (20) implies: % 123.42/16.71 | (21) vIszero(vZero) = all_93_1 % 123.42/16.71 | % 123.42/16.71 | DELTA: instantiating (12) with fresh symbol all_96_0 gives: % 123.42/16.71 | (22) vreduce(vt2) = all_96_0 & vOptTerm(all_96_0) & ! [v0: vTy] : ! [v1: % 123.42/16.71 | vTerm] : ( ~ (vsomeTerm(v1) = all_96_0) | ~ vTy(v0) | ~ vTerm(v1) % 123.42/16.71 | | ~ vptchecksimple(vt2, v0) | vptchecksimple(v1, v0)) % 123.42/16.71 | % 123.42/16.71 | ALPHA: (22) implies: % 123.42/16.72 | (23) vreduce(vt2) = all_96_0 % 123.42/16.72 | (24) ! [v0: vTy] : ! [v1: vTerm] : ( ~ (vsomeTerm(v1) = all_96_0) | ~ % 123.42/16.72 | vTy(v0) | ~ vTerm(v1) | ~ vptchecksimple(vt2, v0) | % 123.42/16.72 | vptchecksimple(v1, v0)) % 123.42/16.72 | % 123.42/16.72 | DELTA: instantiating (16) with fresh symbols all_111_0, all_111_1, all_111_2, % 123.42/16.72 | all_111_3, all_111_4 gives: % 123.42/16.72 | (25) vreduce(all_111_3) = all_111_2 & vreduce(vt2) = all_111_4 & % 123.42/16.72 | vsomeTerm(all_111_0) = all_111_2 & vPlus(vt1, vt2) = all_111_3 & % 123.42/16.72 | vTy(all_111_1) & vOptTerm(all_111_2) & vOptTerm(all_111_4) & % 123.42/16.72 | vTerm(all_111_0) & vTerm(all_111_3) & vptchecksimple(all_111_3, % 123.42/16.72 | all_111_1) & visSomeTerm(all_111_4) & visNV(vt1) & ~ % 123.42/16.72 | vptchecksimple(all_111_0, all_111_1) & ~ visNV(vt2) % 123.42/16.72 | % 123.42/16.72 | ALPHA: (25) implies: % 123.42/16.72 | (26) ~ visNV(vt2) % 123.42/16.72 | (27) ~ vptchecksimple(all_111_0, all_111_1) % 123.42/16.72 | (28) visNV(vt1) % 123.42/16.72 | (29) visSomeTerm(all_111_4) % 123.42/16.72 | (30) vptchecksimple(all_111_3, all_111_1) % 123.42/16.72 | (31) vTerm(all_111_0) % 123.42/16.72 | (32) vOptTerm(all_111_4) % 123.42/16.72 | (33) vTy(all_111_1) % 123.42/16.72 | (34) vPlus(vt1, vt2) = all_111_3 % 123.42/16.72 | (35) vsomeTerm(all_111_0) = all_111_2 % 123.42/16.72 | (36) vreduce(vt2) = all_111_4 % 123.42/16.72 | (37) vreduce(all_111_3) = all_111_2 % 123.42/16.72 | % 123.42/16.72 | DELTA: instantiating (3) with fresh symbols all_114_0, all_114_1 gives: % 123.42/16.72 | (38) vIszero(vZero) = all_114_0 & vPred(vZero) = all_114_1 & % 123.42/16.72 | vTerm(all_114_0) & vTerm(all_114_1) & ? [v0: any] : (v0 = all_114_0 | % 123.42/16.72 | v0 = all_114_1 | ~ vTerm(v0) | ? [v1: vOptTerm] : ? [v2: vTerm] : % 123.42/16.72 | ? [v3: vTerm] : ? [v4: any] : ? [v5: vTerm] : ? [v6: any] : ? % 123.42/16.72 | [v7: vTerm] : ? [v8: vTerm] : ? [v9: any] : ? [v10: vTerm] : ? % 123.42/16.72 | [v11: any] : ? [v12: vTerm] : ? [v13: vTerm] : ? [v14: any] : ? % 123.42/16.72 | [v15: vTerm] : ? [v16: any] : ? [v17: vTerm] : ? [v18: vTerm] : % 123.42/16.72 | ? [v19: vTerm] : ? [v20: any] : ? [v21: vTerm] : ? [v22: vTerm] : % 123.42/16.72 | ? [v23: any] : ? [v24: vTerm] : ? [v25: vTerm] : ? [v26: any] : % 123.42/16.72 | (vTerm(v25) & vTerm(v24) & vTerm(v22) & vTerm(v21) & vTerm(v19) & % 123.42/16.72 | vTerm(v18) & vTerm(v17) & vTerm(v15) & vTerm(v12) & vTerm(v10) & % 123.42/16.72 | vTerm(v7) & vTerm(v5) & vTerm(v3) & vTerm(v2) & ((v26 = v0 & % 123.42/16.72 | vIfelse(vTrue, v24, v25) = v0) | (v23 = v0 & vIfelse(vFalse, % 123.42/16.72 | v21, v22) = v0) | (v20 = v0 & vIfelse(v17, v18, v19) = v0) | % 123.42/16.72 | (v16 = v0 & vSucc(v15) = v0) | (v14 = v0 & vPred(v13) = v0 & % 123.42/16.72 | vSucc(v12) = v13 & vTerm(v13)) | (v11 = v0 & vPred(v10) = v0) % 123.42/16.72 | | (v9 = v0 & vIszero(v8) = v0 & vSucc(v7) = v8 & vTerm(v8)) | % 123.42/16.72 | (v6 = v0 & vIszero(v5) = v0) | (v4 = v0 & vPlus(v2, v3) = v0) | % 123.42/16.72 | (v1 = vnoTerm & vreduce(v0) = vnoTerm)))) % 123.42/16.72 | % 123.42/16.72 | ALPHA: (38) implies: % 123.42/16.72 | (39) vIszero(vZero) = all_114_0 % 123.42/16.72 | % 123.42/16.72 | DELTA: instantiating (4) with fresh symbols all_117_0, all_117_1, all_117_2, % 123.42/16.72 | all_117_3, all_117_4 gives: % 123.42/16.74 | (40) vsomeTerm(vFalse) = all_117_0 & vsomeTerm(vTrue) = all_117_1 & % 123.42/16.74 | vsomeTerm(vZero) = all_117_3 & vIszero(vZero) = all_117_2 & % 123.42/16.74 | vPred(vZero) = all_117_4 & vOptTerm(all_117_0) & vOptTerm(all_117_1) & % 123.42/16.74 | vOptTerm(all_117_3) & vTerm(all_117_2) & vTerm(all_117_4) & ? [v0: % 123.42/16.74 | vTerm] : ( ~ vTerm(v0) | ? [v1: vOptTerm] : ? [v2: vTerm] : ? % 123.42/16.74 | [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : ? [v6: vOptTerm] % 123.42/16.74 | : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : ? [v10: % 123.42/16.74 | vOptTerm] : ? [v11: vOptTerm] : ? [v12: vTerm] : ? [v13: vTerm] % 123.42/16.74 | : ? [v14: vTerm] : ? [v15: vOptTerm] : ? [v16: vTerm] : ? [v17: % 123.42/16.74 | vTerm] : ? [v18: vOptTerm] : ? [v19: vOptTerm] : ? [v20: vTerm] % 123.42/16.74 | : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : ? [v24: % 123.42/16.74 | vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 123.42/16.74 | ? [v28: vOptTerm] : ? [v29: vTerm] : ? [v30: vTerm] : ? [v31: % 123.42/16.74 | vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: vTerm] : % 123.42/16.74 | ? [v35: vOptTerm] : ? [v36: vOptTerm] : ? [v37: vTerm] : ? [v38: % 123.42/16.74 | vTerm] : ? [v39: vOptTerm] : ? [v40: vOptTerm] : ? [v41: vTerm] % 123.42/16.74 | : ? [v42: vTerm] : ? [v43: vTerm] : ? [v44: vOptTerm] : ? [v45: % 123.42/16.74 | vTerm] : ? [v46: vOptTerm] : ? [v47: vTerm] : ? [v48: vOptTerm] % 123.42/16.74 | : ? [v49: vTerm] : ? [v50: vTerm] : ? [v51: vOptTerm] : ? [v52: % 123.42/16.74 | vTerm] : ? [v53: vOptTerm] : ? [v54: vTerm] : ? [v55: vTerm] : % 123.42/16.74 | ? [v56: vTerm] : ? [v57: vOptTerm] : ? [v58: vTerm] : ? [v59: % 123.42/16.74 | vTerm] : ? [v60: vTerm] : ? [v61: vTerm] : ? [v62: vOptTerm] : % 123.42/16.74 | ? [v63: vOptTerm] : ? [v64: vTerm] : ? [v65: vTerm] : ? [v66: % 123.42/16.74 | vOptTerm] : ? [v67: vOptTerm] : ? [v68: vTerm] : ? [v69: vTerm] % 123.42/16.74 | : ? [v70: vTerm] : ? [v71: vOptTerm] : ? [v72: vTerm] : ? [v73: % 123.42/16.74 | vOptTerm] : ? [v74: vTerm] : ? [v75: vOptTerm] : ? [v76: vTerm] % 123.42/16.74 | : ? [v77: vTerm] : ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: % 123.42/16.74 | vOptTerm] : ? [v81: vTerm] : ? [v82: vTerm] : ? [v83: vTerm] : % 123.42/16.74 | ? [v84: vOptTerm] : ? [v85: vTerm] : ? [v86: vTerm] : ? [v87: % 123.42/16.74 | vTerm] : ? [v88: vOptTerm] : ? [v89: vTerm] : ? [v90: vOptTerm] % 123.42/16.74 | : ? [v91: vOptTerm] : ? [v92: vTerm] : ? [v93: vTerm] : ? [v94: % 123.42/16.74 | vOptTerm] : ? [v95: vOptTerm] : ? [v96: vTerm] : ? [v97: vTerm] % 123.42/16.74 | : ? [v98: vTerm] : ? [v99: vOptTerm] : ? [v100: vTerm] : ? % 123.42/16.74 | [v101: vTerm] : ? [v102: vTerm] : ? [v103: vOptTerm] : ? [v104: % 123.42/16.74 | vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: vTerm] % 123.42/16.74 | : ? [v108: vTerm] : ? [v109: vOptTerm] : ? [v110: vOptTerm] : ? % 123.42/16.74 | [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : ? [v114: % 123.42/16.74 | vOptTerm] : ? [v115: vTerm] : ? [v116: vTerm] : ? [v117: vTerm] % 123.42/16.74 | : ? [v118: vOptTerm] : ? [v119: vTerm] : ? [v120: vTerm] : ? % 123.42/16.74 | [v121: vTerm] : ? [v122: vOptTerm] : (vreduce(v0) = v1 & % 123.42/16.74 | vOptTerm(v109) & vOptTerm(v103) & vOptTerm(v94) & vOptTerm(v90) & % 123.42/16.74 | vOptTerm(v78) & vOptTerm(v73) & vOptTerm(v66) & vOptTerm(v62) & % 123.42/16.74 | vOptTerm(v51) & vOptTerm(v46) & vOptTerm(v39) & vOptTerm(v35) & % 123.42/16.74 | vOptTerm(v23) & vOptTerm(v18) & vOptTerm(v10) & vOptTerm(v5) & % 123.42/16.74 | vOptTerm(v1) & vTerm(v120) & vTerm(v119) & vTerm(v116) & % 123.42/16.74 | vTerm(v115) & vTerm(v108) & vTerm(v107) & vTerm(v106) & % 123.42/16.74 | vTerm(v102) & vTerm(v101) & vTerm(v100) & vTerm(v93) & vTerm(v89) % 123.42/16.74 | & vTerm(v85) & vTerm(v77) & vTerm(v72) & vTerm(v65) & vTerm(v61) & % 123.42/16.74 | vTerm(v58) & vTerm(v50) & vTerm(v45) & vTerm(v38) & vTerm(v34) & % 123.42/16.74 | vTerm(v30) & vTerm(v29) & vTerm(v22) & vTerm(v21) & vTerm(v17) & % 123.42/16.74 | vTerm(v16) & vTerm(v9) & vTerm(v8) & vTerm(v4) & vTerm(v3) & % 123.42/16.74 | vTerm(v2) & ((v122 = v1 & v121 = v0 & vsomeTerm(v119) = v1 & % 123.42/16.74 | vIfelse(vTrue, v119, v120) = v0) | (v118 = v1 & v117 = v0 & % 123.42/16.74 | vsomeTerm(v116) = v1 & vIfelse(vFalse, v115, v116) = v0) | % 123.42/16.74 | (v114 = v1 & v111 = v0 & v110 = v109 & ~ (v106 = vFalse) & ~ % 123.42/16.74 | (v106 = vTrue) & vreduce(v106) = v109 & vgetTerm(v109) = v112 % 123.42/16.74 | & vsomeTerm(v113) = v1 & vIfelse(v112, v107, v108) = v113 & % 123.42/16.74 | vIfelse(v106, v107, v108) = v0 & vTerm(v113) & vTerm(v112) & % 123.42/16.74 | visSomeTerm(v109)) | (v105 = v0 & v104 = v103 & v1 = vnoTerm & % 123.42/16.74 | ~ (v100 = vFalse) & ~ (v100 = vTrue) & vreduce(v100) = v103 % 123.42/16.74 | & vIfelse(v100, v101, v102) = v0 & ~ visSomeTerm(v103)) | % 123.42/16.74 | (v99 = v1 & v96 = v0 & v95 = v94 & vreduce(v93) = v94 & % 123.42/16.74 | vgetTerm(v94) = v97 & vsomeTerm(v98) = v1 & vSucc(v97) = v98 & % 123.42/16.74 | vSucc(v93) = v0 & vTerm(v98) & vTerm(v97) & visSomeTerm(v94)) % 123.42/16.74 | | (v92 = v0 & v91 = v90 & v1 = vnoTerm & vreduce(v89) = v90 & % 123.42/16.74 | vSucc(v89) = v0 & ~ visSomeTerm(v90)) | (v88 = v1 & v87 = v0 % 123.42/16.74 | & vsomeTerm(v85) = v1 & vPred(v86) = v0 & vSucc(v85) = v86 & % 123.42/16.74 | vTerm(v86) & visNV(v85)) | (v84 = v1 & v81 = v0 & v80 = v78 & % 123.42/16.74 | vreduce(v79) = v78 & vgetTerm(v78) = v82 & vsomeTerm(v83) = v1 % 123.42/16.74 | & vPred(v82) = v83 & vPred(v79) = v0 & vSucc(v77) = v79 & % 123.42/16.74 | vTerm(v83) & vTerm(v82) & vTerm(v79) & visSomeTerm(v78) & ~ % 123.42/16.74 | visNV(v77)) | (v76 = v0 & v75 = v73 & v1 = vnoTerm & % 123.42/16.74 | vreduce(v74) = v73 & vPred(v74) = v0 & vSucc(v72) = v74 & % 123.42/16.74 | vTerm(v74) & ~ visSomeTerm(v73) & ~ visNV(v72)) | (v71 = v1 % 123.42/16.74 | & v68 = v0 & v67 = v66 & ~ (v65 = vZero) & vreduce(v65) = v66 % 123.42/16.74 | & vgetTerm(v66) = v69 & vsomeTerm(v70) = v1 & vPred(v69) = v70 % 123.42/16.74 | & vPred(v65) = v0 & vTerm(v70) & vTerm(v69) & visSomeTerm(v66) % 123.42/16.74 | & ! [v123: vTerm] : ( ~ (vSucc(v123) = v65) | ~ % 123.42/16.74 | vTerm(v123))) | (v64 = v0 & v63 = v62 & v1 = vnoTerm & ~ % 123.42/16.74 | (v61 = vZero) & vreduce(v61) = v62 & vPred(v61) = v0 & ~ % 123.42/16.74 | visSomeTerm(v62) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v61) % 123.42/16.74 | | ~ vTerm(v123))) | (v60 = v0 & v1 = all_117_0 & % 123.42/16.74 | vIszero(v59) = v0 & vSucc(v58) = v59 & vTerm(v59) & % 123.42/16.74 | visNV(v58)) | (v57 = v1 & v54 = v0 & v53 = v51 & vreduce(v52) % 123.42/16.74 | = v51 & vgetTerm(v51) = v55 & vsomeTerm(v56) = v1 & % 123.42/16.74 | vIszero(v55) = v56 & vIszero(v52) = v0 & vSucc(v50) = v52 & % 123.42/16.74 | vTerm(v56) & vTerm(v55) & vTerm(v52) & visSomeTerm(v51) & ~ % 123.42/16.74 | visNV(v50)) | (v49 = v0 & v48 = v46 & v1 = vnoTerm & % 123.42/16.74 | vreduce(v47) = v46 & vIszero(v47) = v0 & vSucc(v45) = v47 & % 123.42/16.74 | vTerm(v47) & ~ visSomeTerm(v46) & ~ visNV(v45)) | (v44 = v1 % 123.42/16.74 | & v41 = v0 & v40 = v39 & ~ (v38 = vZero) & vreduce(v38) = v39 % 123.42/16.74 | & vgetTerm(v39) = v42 & vsomeTerm(v43) = v1 & vIszero(v42) = % 123.42/16.74 | v43 & vIszero(v38) = v0 & vTerm(v43) & vTerm(v42) & % 123.42/16.74 | visSomeTerm(v39) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v38) % 123.42/16.74 | | ~ vTerm(v123))) | (v37 = v0 & v36 = v35 & v1 = vnoTerm & % 123.42/16.74 | ~ (v34 = vZero) & vreduce(v34) = v35 & vIszero(v34) = v0 & ~ % 123.42/16.74 | visSomeTerm(v35) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v34) % 123.42/16.74 | | ~ vTerm(v123))) | (v33 = v1 & v31 = v0 & vplusop(v29, % 123.42/16.74 | v30) = v32 & vsomeTerm(v32) = v1 & vPlus(v29, v30) = v0 & % 123.42/16.74 | vTerm(v32) & visNV(v30) & visNV(v29)) | (v28 = v1 & v25 = v0 & % 123.42/16.74 | v24 = v23 & vreduce(v22) = v23 & vgetTerm(v23) = v26 & % 123.42/16.74 | vsomeTerm(v27) = v1 & vPlus(v21, v26) = v27 & vPlus(v21, v22) % 123.42/16.74 | = v0 & vTerm(v27) & vTerm(v26) & visSomeTerm(v23) & visNV(v21) % 123.42/16.74 | & ~ visNV(v22)) | (v20 = v0 & v19 = v18 & v1 = vnoTerm & % 123.42/16.74 | vreduce(v17) = v18 & vPlus(v16, v17) = v0 & visNV(v16) & ~ % 123.42/16.74 | visSomeTerm(v18) & ~ visNV(v17)) | (v15 = v1 & v12 = v0 & v11 % 123.42/16.74 | = v10 & vreduce(v8) = v10 & vgetTerm(v10) = v13 & % 123.42/16.74 | vsomeTerm(v14) = v1 & vPlus(v13, v9) = v14 & vPlus(v8, v9) = % 123.42/16.74 | v0 & vTerm(v14) & vTerm(v13) & visSomeTerm(v10) & ~ % 123.42/16.74 | visNV(v8)) | (v7 = v0 & v6 = v5 & v1 = vnoTerm & vreduce(v3) = % 123.42/16.74 | v5 & vPlus(v3, v4) = v0 & ~ visSomeTerm(v5) & ~ visNV(v3)) | % 123.42/16.74 | (v2 = v0 & v1 = vnoTerm & ~ (v0 = all_117_2) & ~ (v0 = % 123.42/16.74 | all_117_4) & ! [v123: vTerm] : ! [v124: vTerm] : ! [v125: % 123.42/16.74 | vTerm] : ( ~ (vIfelse(v123, v124, v125) = v0) | ~ % 123.42/16.74 | vTerm(v125) | ~ vTerm(v124) | ~ vTerm(v123)) & ! [v123: % 123.42/16.74 | vTerm] : ! [v124: vTerm] : ( ~ (vPlus(v123, v124) = v0) | % 123.42/16.74 | ~ vTerm(v124) | ~ vTerm(v123)) & ! [v123: vTerm] : ! % 123.42/16.74 | [v124: vTerm] : ( ~ (vSucc(v123) = v124) | ~ vTerm(v123) | ? % 123.42/16.74 | [v125: vTerm] : ( ~ (v125 = v0) & vIszero(v124) = v125 & % 123.42/16.74 | vTerm(v125))) & ! [v123: vTerm] : ! [v124: vTerm] : ( ~ % 123.42/16.74 | (vSucc(v123) = v124) | ~ vTerm(v123) | ? [v125: vTerm] : ( % 123.42/16.74 | ~ (v125 = v0) & vPred(v124) = v125 & vTerm(v125))) & ! % 123.42/16.74 | [v123: vTerm] : ! [v124: vTerm] : ( ~ (vIfelse(vFalse, v123, % 123.42/16.74 | v124) = v0) | ~ vTerm(v124) | ~ vTerm(v123)) & ! % 123.42/16.74 | [v123: vTerm] : ! [v124: vTerm] : ( ~ (vIfelse(vTrue, v123, % 123.42/16.74 | v124) = v0) | ~ vTerm(v124) | ~ vTerm(v123)) & ! % 123.42/16.74 | [v123: vTerm] : ( ~ (vIszero(v123) = v0) | ~ vTerm(v123)) & % 123.42/16.74 | ! [v123: vTerm] : ( ~ (vPred(v123) = v0) | ~ vTerm(v123)) & % 123.42/16.74 | ! [v123: vTerm] : ( ~ (vSucc(v123) = v0) | ~ vTerm(v123))) | % 123.42/16.74 | (v1 = all_117_1 & v0 = all_117_2) | (v1 = all_117_3 & v0 = % 123.42/16.74 | all_117_4)))) % 123.42/16.74 | % 123.42/16.74 | ALPHA: (40) implies: % 123.42/16.74 | (41) vIszero(vZero) = all_117_2 % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (17) with all_114_0, all_117_2, vZero, simplifying % 123.42/16.74 | with (39), (41) gives: % 123.42/16.74 | (42) all_117_2 = all_114_0 % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (17) with all_93_1, all_117_2, vZero, simplifying % 123.42/16.74 | with (21), (41) gives: % 123.42/16.74 | (43) all_117_2 = all_93_1 % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (19) with all_96_0, all_111_4, vt2, simplifying % 123.42/16.74 | with (23), (36) gives: % 123.42/16.74 | (44) all_111_4 = all_96_0 % 123.42/16.74 | % 123.42/16.74 | COMBINE_EQS: (42), (43) imply: % 123.42/16.74 | (45) all_114_0 = all_93_1 % 123.42/16.74 | % 123.42/16.74 | REDUCE: (32), (44) imply: % 123.42/16.74 | (46) vOptTerm(all_96_0) % 123.42/16.74 | % 123.42/16.74 | REDUCE: (29), (44) imply: % 123.42/16.74 | (47) visSomeTerm(all_96_0) % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (13) with vt1, simplifying with (15), (28) gives: % 123.42/16.74 | (48) vptchecksimple(vt1, vNat) % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (isSomeTerm-true-INV) with all_96_0, simplifying % 123.42/16.74 | with (46), (47) gives: % 123.42/16.74 | (49) ? [v0: vTerm] : (vsomeTerm(v0) = all_96_0 & vTerm(v0)) % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (7) with vZero, all_93_1, simplifying with (5), % 123.42/16.74 | (6), (21) gives: % 123.42/16.74 | (50) vptchecksimple(all_93_1, vB) % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (11) with vt1, vt2, all_111_3, simplifying with % 123.42/16.74 | (14), (15), (34) gives: % 123.42/16.74 | (51) ~ vptchecksimple(all_111_3, vNat) | vptchecksimple(vt2, vNat) % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (10) with vt1, vt2, all_111_1, all_111_3, % 123.42/16.74 | simplifying with (14), (15), (30), (33), (34) gives: % 123.42/16.74 | (52) all_111_1 = vNat % 123.42/16.74 | % 123.42/16.74 | GROUND_INST: instantiating (reduce-19) with vt1, vt2, all_111_3, simplifying % 123.42/16.74 | with (14), (15), (26), (28), (34) gives: % 123.42/16.74 | (53) ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: % 123.42/16.74 | vTerm] : ? [v4: vOptTerm] : (vreduce(vt2) = v0 & vOptTerm(v0) & ( ~ % 123.42/16.74 | visSomeTerm(v0) | (v4 = v1 & vreduce(all_111_3) = v1 & % 123.42/16.74 | vgetTerm(v0) = v2 & vsomeTerm(v3) = v1 & vPlus(vt1, v2) = v3 & % 123.42/16.74 | vOptTerm(v1) & vTerm(v3) & vTerm(v2)))) % 123.42/16.74 | % 123.42/16.74 | DELTA: instantiating (49) with fresh symbol all_130_0 gives: % 123.42/16.74 | (54) vsomeTerm(all_130_0) = all_96_0 & vTerm(all_130_0) % 123.42/16.74 | % 123.42/16.74 | ALPHA: (54) implies: % 123.42/16.74 | (55) vTerm(all_130_0) % 123.42/16.74 | (56) vsomeTerm(all_130_0) = all_96_0 % 123.42/16.74 | % 123.42/16.74 | DELTA: instantiating (53) with fresh symbols all_135_0, all_135_1, all_135_2, % 123.42/16.74 | all_135_3, all_135_4 gives: % 123.42/16.74 | (57) vreduce(vt2) = all_135_4 & vOptTerm(all_135_4) & ( ~ % 123.42/16.74 | visSomeTerm(all_135_4) | (all_135_0 = all_135_3 & vreduce(all_111_3) % 123.42/16.74 | = all_135_3 & vgetTerm(all_135_4) = all_135_2 & % 123.42/16.74 | vsomeTerm(all_135_1) = all_135_3 & vPlus(vt1, all_135_2) = % 123.42/16.74 | all_135_1 & vOptTerm(all_135_3) & vTerm(all_135_1) & % 123.42/16.74 | vTerm(all_135_2))) % 123.42/16.74 | % 123.42/16.74 | ALPHA: (57) implies: % 123.42/16.74 | (58) vreduce(vt2) = all_135_4 % 123.42/16.74 | (59) ~ visSomeTerm(all_135_4) | (all_135_0 = all_135_3 & % 123.42/16.74 | vreduce(all_111_3) = all_135_3 & vgetTerm(all_135_4) = all_135_2 & % 123.42/16.74 | vsomeTerm(all_135_1) = all_135_3 & vPlus(vt1, all_135_2) = all_135_1 % 123.42/16.74 | & vOptTerm(all_135_3) & vTerm(all_135_1) & vTerm(all_135_2)) % 123.42/16.74 | % 123.42/16.75 | REDUCE: (33), (52) imply: % 123.42/16.75 | (60) vTy(vNat) % 123.42/16.75 | % 123.42/16.75 | REDUCE: (30), (52) imply: % 123.42/16.75 | (61) vptchecksimple(all_111_3, vNat) % 123.42/16.75 | % 123.42/16.75 | REDUCE: (27), (52) imply: % 123.42/16.75 | (62) ~ vptchecksimple(all_111_0, vNat) % 123.42/16.75 | % 123.42/16.75 | BETA: splitting (51) gives: % 123.42/16.75 | % 123.42/16.75 | Case 1: % 123.42/16.75 | | % 123.42/16.75 | | (63) ~ vptchecksimple(all_111_3, vNat) % 123.42/16.75 | | % 123.42/16.75 | | PRED_UNIFY: (61), (63) imply: % 123.42/16.75 | | (64) $false % 123.42/16.75 | | % 123.42/16.75 | | CLOSE: (64) is inconsistent. % 123.42/16.75 | | % 123.42/16.75 | Case 2: % 123.42/16.75 | | % 123.42/16.75 | | (65) vptchecksimple(vt2, vNat) % 123.42/16.75 | | % 123.42/16.75 | | GROUND_INST: instantiating (19) with all_96_0, all_135_4, vt2, simplifying % 123.42/16.75 | | with (23), (58) gives: % 123.42/16.75 | | (66) all_135_4 = all_96_0 % 123.42/16.75 | | % 123.42/16.75 | | BETA: splitting (59) gives: % 123.42/16.75 | | % 123.42/16.75 | | Case 1: % 123.42/16.75 | | | % 123.42/16.75 | | | (67) ~ visSomeTerm(all_135_4) % 123.42/16.75 | | | % 123.42/16.75 | | | REDUCE: (66), (67) imply: % 123.42/16.75 | | | (68) ~ visSomeTerm(all_96_0) % 123.42/16.75 | | | % 123.42/16.75 | | | PRED_UNIFY: (47), (68) imply: % 123.42/16.75 | | | (69) $false % 123.42/16.75 | | | % 123.42/16.75 | | | CLOSE: (69) is inconsistent. % 123.42/16.75 | | | % 123.42/16.75 | | Case 2: % 123.42/16.75 | | | % 123.42/16.75 | | | (70) all_135_0 = all_135_3 & vreduce(all_111_3) = all_135_3 & % 123.42/16.75 | | | vgetTerm(all_135_4) = all_135_2 & vsomeTerm(all_135_1) = all_135_3 % 123.42/16.75 | | | & vPlus(vt1, all_135_2) = all_135_1 & vOptTerm(all_135_3) & % 123.42/16.75 | | | vTerm(all_135_1) & vTerm(all_135_2) % 123.42/16.75 | | | % 123.42/16.75 | | | ALPHA: (70) implies: % 123.42/16.75 | | | (71) vTerm(all_135_2) % 123.42/16.75 | | | (72) vTerm(all_135_1) % 123.42/16.75 | | | (73) vPlus(vt1, all_135_2) = all_135_1 % 123.42/16.75 | | | (74) vsomeTerm(all_135_1) = all_135_3 % 123.42/16.75 | | | (75) vgetTerm(all_135_4) = all_135_2 % 123.42/16.75 | | | (76) vreduce(all_111_3) = all_135_3 % 123.42/16.75 | | | % 123.42/16.75 | | | REDUCE: (66), (75) imply: % 123.42/16.75 | | | (77) vgetTerm(all_96_0) = all_135_2 % 123.42/16.75 | | | % 123.42/16.75 | | | GROUND_INST: instantiating (19) with all_111_2, all_135_3, all_111_3, % 123.42/16.75 | | | simplifying with (37), (76) gives: % 123.42/16.75 | | | (78) all_135_3 = all_111_2 % 123.42/16.75 | | | % 123.42/16.75 | | | REDUCE: (74), (78) imply: % 123.42/16.75 | | | (79) vsomeTerm(all_135_1) = all_111_2 % 123.42/16.75 | | | % 123.42/16.75 | | | GROUND_INST: instantiating (10) with vt1, all_135_2, vB, all_93_1, % 123.42/16.75 | | | simplifying with (8), (15), (50), (71) gives: % 123.42/16.75 | | | (80) vB = vNat | ~ (vPlus(vt1, all_135_2) = all_93_1) % 123.42/16.75 | | | % 123.42/16.75 | | | GROUND_INST: instantiating (24) with vNat, all_130_0, simplifying with % 123.42/16.75 | | | (55), (56), (60), (65) gives: % 123.42/16.75 | | | (81) vptchecksimple(all_130_0, vNat) % 123.42/16.75 | | | % 123.42/16.75 | | | GROUND_INST: instantiating (getTerm-0) with all_130_0, all_96_0, % 123.42/16.75 | | | simplifying with (55), (56) gives: % 123.42/16.75 | | | (82) vgetTerm(all_96_0) = all_130_0 % 123.42/16.75 | | | % 123.42/16.75 | | | GROUND_INST: instantiating (EQ-someTerm) with all_111_0, all_135_1, % 123.42/16.75 | | | all_111_2, simplifying with (31), (35), (72), (79) gives: % 123.42/16.75 | | | (83) all_135_1 = all_111_0 % 123.42/16.75 | | | % 123.42/16.75 | | | REDUCE: (73), (83) imply: % 123.42/16.75 | | | (84) vPlus(vt1, all_135_2) = all_111_0 % 123.42/16.75 | | | % 123.42/16.75 | | | BETA: splitting (80) gives: % 123.42/16.75 | | | % 123.42/16.75 | | | Case 1: % 123.42/16.75 | | | | % 123.42/16.75 | | | | % 123.42/16.75 | | | | GROUND_INST: instantiating (18) with all_135_2, all_130_0, all_96_0, % 123.42/16.75 | | | | simplifying with (77), (82) gives: % 123.42/16.75 | | | | (85) all_135_2 = all_130_0 % 123.42/16.75 | | | | % 123.42/16.75 | | | | REDUCE: (84), (85) imply: % 123.42/16.75 | | | | (86) vPlus(vt1, all_130_0) = all_111_0 % 123.42/16.75 | | | | % 123.42/16.75 | | | | GROUND_INST: instantiating (9) with vt1, all_130_0, all_111_0, % 123.42/16.75 | | | | simplifying with (15), (48), (55), (62), (81), (86) gives: % 123.42/16.75 | | | | (87) $false % 123.42/16.75 | | | | % 123.42/16.75 | | | | CLOSE: (87) is inconsistent. % 123.42/16.75 | | | | % 123.42/16.75 | | | Case 2: % 123.42/16.75 | | | | % 123.42/16.75 | | | | (88) vB = vNat % 123.42/16.75 | | | | % 123.42/16.75 | | | | REDUCE: (1), (88) imply: % 123.42/16.75 | | | | (89) $false % 123.42/16.75 | | | | % 123.42/16.75 | | | | CLOSE: (89) is inconsistent. % 123.42/16.75 | | | | % 123.42/16.75 | | | End of split % 123.42/16.75 | | | % 123.42/16.75 | | End of split % 123.42/16.75 | | % 123.42/16.75 | End of split % 123.42/16.75 | % 123.42/16.75 End of proof % 123.42/16.75 % SZS output end Proof for theBenchmark % 123.42/16.75 % 123.42/16.75 16164ms %------------------------------------------------------------------------------