%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM218_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 : n012.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:35 PM UTC 2026 % Result : Theorem 33.28s 5.13s % Output : Proof 81.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : COM218_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.10 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.11/0.30 % Computer : n012.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Mon May 4 19:00:00 EDT 2026 % 0.11/0.30 % CPUTime : % 0.54/0.57 ________ _____ % 0.54/0.57 ___ __ \_________(_)________________________________ % 0.54/0.57 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.54/0.57 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.54/0.57 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.54/0.57 % 0.54/0.57 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.54/0.57 (2023-06-19) % 0.54/0.57 % 0.54/0.57 (c) Philipp Rümmer, 2009-2023 % 0.54/0.57 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.54/0.57 Amanda Stjerna. % 0.54/0.57 Free software under BSD-3-Clause. % 0.54/0.57 % 0.54/0.57 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.54/0.57 % 0.54/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.54/0.59 Running up to 7 provers in parallel. % 0.54/0.61 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.54/0.61 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.54/0.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.54/0.61 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.54/0.61 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.54/0.61 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.54/0.61 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 6.31/1.65 Prover 1: Preprocessing ... % 6.31/1.67 Prover 4: Preprocessing ... % 6.31/1.68 Prover 5: Preprocessing ... % 6.31/1.68 Prover 0: Preprocessing ... % 6.31/1.68 Prover 2: Preprocessing ... % 6.31/1.68 Prover 3: Preprocessing ... % 6.31/1.69 Prover 6: Preprocessing ... % 17.11/3.04 Prover 1: Warning: ignoring some quantifiers % 17.84/3.14 Prover 3: Warning: ignoring some quantifiers % 17.84/3.14 Prover 1: Constructing countermodel ... % 17.84/3.19 Prover 3: Constructing countermodel ... % 18.41/3.20 Prover 6: Proving ... % 18.41/3.23 Prover 5: Proving ... % 19.96/3.41 Prover 4: Warning: ignoring some quantifiers % 19.96/3.49 Prover 4: Constructing countermodel ... % 20.75/3.55 Prover 0: Proving ... % 21.45/3.60 Prover 2: Proving ... % 33.28/5.13 Prover 5: proved (4520ms) % 33.28/5.13 % 33.28/5.13 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.28/5.13 % 33.28/5.13 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 33.28/5.13 Prover 3: stopped % 33.28/5.13 Prover 0: stopped % 33.28/5.14 Prover 2: stopped % 33.28/5.14 Prover 6: stopped % 33.28/5.15 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 33.28/5.15 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 33.28/5.15 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 33.28/5.15 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 34.62/5.37 Prover 7: Preprocessing ... % 34.62/5.39 Prover 10: Preprocessing ... % 34.62/5.40 Prover 8: Preprocessing ... % 35.39/5.42 Prover 11: Preprocessing ... % 35.39/5.42 Prover 13: Preprocessing ... % 37.75/5.70 Prover 8: Warning: ignoring some quantifiers % 37.75/5.71 Prover 8: Constructing countermodel ... % 37.75/5.76 Prover 10: Warning: ignoring some quantifiers % 37.75/5.77 Prover 10: Constructing countermodel ... % 38.55/5.80 Prover 7: Warning: ignoring some quantifiers % 38.55/5.82 Prover 11: Warning: ignoring some quantifiers % 38.55/5.83 Prover 11: Constructing countermodel ... % 38.55/5.83 Prover 7: Constructing countermodel ... % 39.34/5.94 Prover 13: Warning: ignoring some quantifiers % 39.34/5.97 Prover 13: Constructing countermodel ... % 72.46/10.18 Prover 13: stopped % 73.12/10.20 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 73.90/10.34 Prover 16: Preprocessing ... % 76.29/10.63 Prover 16: Warning: ignoring some quantifiers % 76.29/10.68 Prover 16: Constructing countermodel ... % 80.39/11.19 Prover 16: Found proof (size 76) % 80.39/11.19 Prover 16: proved (1001ms) % 80.39/11.20 Prover 4: stopped % 81.01/11.20 Prover 7: stopped % 81.01/11.20 Prover 8: stopped % 81.01/11.20 Prover 1: stopped % 81.01/11.21 Prover 10: stopped % 81.01/11.23 Prover 11: stopped % 81.01/11.23 % 81.01/11.23 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.01/11.23 % 81.01/11.24 % SZS output start Proof for theBenchmark % 81.01/11.24 Assumptions after simplification: % 81.01/11.24 --------------------------------- % 81.01/11.24 % 81.01/11.24 (DIFF-False-Zero) % 81.01/11.25 ~ (vFalse = vZero) & vTerm(vFalse) & vTerm(vZero) % 81.01/11.25 % 81.01/11.25 (EQ-someTerm) % 81.01/11.27 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : (v1 = v0 | ~ % 81.01/11.27 (vsomeTerm(v1) = v2) | ~ (vsomeTerm(v0) = v2) | ~ vTerm(v1) | ~ % 81.01/11.27 vTerm(v0)) % 81.01/11.27 % 81.01/11.27 (Preservation-Ifelse-IH0) % 81.01/11.27 vTerm(vt1) & ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: % 81.01/11.27 vTy] : ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ % 81.01/11.27 vTerm(v2) | ~ vptchecksimple(vt1, v1) | vptchecksimple(v2, v1))) % 81.01/11.27 % 81.01/11.27 (Preservation-Ifelse-t1-isSomeTerm-True) % 81.01/11.27 vTerm(vt1) & vTerm(vt2) & vTerm(vt3) & vTerm(vFalse) & vTerm(vTrue) & ? [v0: % 81.01/11.27 vOptTerm] : ? [v1: vTerm] : ? [v2: vOptTerm] : ? [v3: vTy] : ? [v4: % 81.01/11.27 vTerm] : ( ~ (vt1 = vFalse) & ~ (vt1 = vTrue) & vreduce(v1) = v2 & % 81.01/11.27 vreduce(vt1) = v0 & vsomeTerm(v4) = v2 & vIfelse(vt1, vt2, vt3) = v1 & % 81.01/11.27 vTy(v3) & vOptTerm(v2) & vOptTerm(v0) & vTerm(v4) & vTerm(v1) & % 81.01/11.27 vptchecksimple(v1, v3) & visSomeTerm(v0) & ~ vptchecksimple(v4, v3)) % 81.01/11.27 % 81.01/11.27 (TZero_inv) % 81.01/11.27 vTy(vNat) & vTerm(vZero) & ! [v0: vTy] : (v0 = vNat | ~ vTy(v0) | ~ % 81.01/11.27 vptchecksimple(vZero, v0)) % 81.01/11.27 % 81.01/11.27 (Tif) % 81.01/11.27 vTy(vB) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTy] : ! [v3: vTerm] : ! % 81.01/11.27 [v4: vTerm] : ( ~ (vIfelse(v0, v1, v3) = v4) | ~ vTy(v2) | ~ vTerm(v3) | ~ % 81.01/11.27 vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v3, v2) | ~ vptchecksimple(v1, % 81.01/11.27 v2) | ~ vptchecksimple(v0, vB) | vptchecksimple(v4, v2)) % 81.01/11.27 % 81.01/11.27 (Tif_inv1) % 81.01/11.27 vTy(vB) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTy] : ! % 81.01/11.27 [v4: vTerm] : ( ~ (vIfelse(v0, v1, v2) = v4) | ~ vTy(v3) | ~ vTerm(v2) | ~ % 81.01/11.27 vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v4, v3) | vptchecksimple(v0, % 81.01/11.27 vB)) % 81.01/11.27 % 81.01/11.27 (Tif_inv2) % 81.01/11.27 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTy] : ! [v4: % 81.01/11.27 vTerm] : ( ~ (vIfelse(v0, v1, v2) = v4) | ~ vTy(v3) | ~ vTerm(v2) | ~ % 81.01/11.27 vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v4, v3) | vptchecksimple(v1, % 81.01/11.28 v3)) % 81.01/11.28 % 81.01/11.28 (Tif_inv3) % 81.01/11.28 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTy] : ! [v4: % 81.01/11.28 vTerm] : ( ~ (vIfelse(v0, v1, v2) = v4) | ~ vTy(v3) | ~ vTerm(v2) | ~ % 81.01/11.28 vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v4, v3) | vptchecksimple(v2, % 81.01/11.28 v3)) % 81.01/11.28 % 81.01/11.28 (Tiszero_inv2) % 81.01/11.28 vTy(vB) & ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vB | ~ % 81.01/11.28 (vIszero(v0) = v2) | ~ vTy(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, v1)) % 81.01/11.28 % 81.01/11.28 (Ttrue) % 81.01/11.28 vTy(vB) & vTerm(vTrue) & vptchecksimple(vTrue, vB) % 81.01/11.28 % 81.01/11.28 (getTerm-0) % 81.01/11.28 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vsomeTerm(v0) = v1) | ~ vTerm(v0) | % 81.01/11.28 vgetTerm(v1) = v0) % 81.01/11.28 % 81.01/11.28 (isSomeTerm-true-INV) % 81.01/11.28 ! [v0: vOptTerm] : ( ~ vOptTerm(v0) | ~ visSomeTerm(v0) | ? [v1: vTerm] : % 81.01/11.28 (vsomeTerm(v1) = v0 & vTerm(v1))) % 81.01/11.28 % 81.01/11.28 (reduce-2) % 81.01/11.28 vTerm(vFalse) & vTerm(vTrue) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: % 81.01/11.28 vTerm] : ! [v3: vTerm] : ( ~ (vIfelse(v0, v1, v2) = v3) | ~ vTerm(v2) | ~ % 81.01/11.28 vTerm(v1) | ~ vTerm(v0) | ? [v4: vOptTerm] : ? [v5: vOptTerm] : ? [v6: % 81.01/11.28 vTerm] : ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: % 81.01/11.28 vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : (vTerm(v12) & vTerm(v11) & % 81.01/11.28 vTerm(v10) & vTerm(v9) & ((v12 = v2 & v11 = v1 & v0 = vTrue) | (v10 = v2 & % 81.01/11.28 v9 = v1 & v0 = vFalse) | (vreduce(v0) = v4 & vOptTerm(v4) & ( ~ % 81.01/11.28 visSomeTerm(v4) | (v8 = v5 & vreduce(v3) = v5 & vgetTerm(v4) = v6 & % 81.01/11.28 vsomeTerm(v7) = v5 & vIfelse(v6, v1, v2) = v7 & vOptTerm(v5) & % 81.01/11.28 vTerm(v7) & vTerm(v6))))))) % 81.01/11.28 % 81.01/11.28 (reduce-6) % 81.01/11.28 vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 81.01/11.28 vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 81.01/11.28 % 81.01/11.28 (reduce-INV) % 81.47/11.30 vOptTerm(vnoTerm) & vTerm(vFalse) & vTerm(vTrue) & vTerm(vZero) & ? [v0: % 81.47/11.30 vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 81.47/11.30 vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 81.47/11.30 vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 81.47/11.30 vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & ? [v5: % 81.47/11.30 vTerm] : ( ~ vTerm(v5) | ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 81.47/11.30 vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: vOptTerm] : ? % 81.47/11.30 [v12: vTerm] : ? [v13: vTerm] : ? [v14: vTerm] : ? [v15: vOptTerm] : ? % 81.47/11.30 [v16: vOptTerm] : ? [v17: vTerm] : ? [v18: vTerm] : ? [v19: vTerm] : ? % 81.47/11.30 [v20: vOptTerm] : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : % 81.47/11.30 ? [v24: vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 81.47/11.30 ? [v28: vOptTerm] : ? [v29: vOptTerm] : ? [v30: vTerm] : ? [v31: % 81.47/11.30 vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: vTerm] : ? % 81.47/11.30 [v35: vTerm] : ? [v36: vTerm] : ? [v37: vTerm] : ? [v38: vOptTerm] : ? % 81.47/11.30 [v39: vTerm] : ? [v40: vOptTerm] : ? [v41: vOptTerm] : ? [v42: vTerm] : % 81.47/11.30 ? [v43: vTerm] : ? [v44: vOptTerm] : ? [v45: vOptTerm] : ? [v46: % 81.47/11.30 vTerm] : ? [v47: vTerm] : ? [v48: vTerm] : ? [v49: vOptTerm] : ? % 81.47/11.30 [v50: vTerm] : ? [v51: vOptTerm] : ? [v52: vTerm] : ? [v53: vOptTerm] : % 81.47/11.30 ? [v54: vTerm] : ? [v55: vTerm] : ? [v56: vOptTerm] : ? [v57: vTerm] : % 81.47/11.30 ? [v58: vOptTerm] : ? [v59: vTerm] : ? [v60: vTerm] : ? [v61: vTerm] : % 81.47/11.30 ? [v62: vOptTerm] : ? [v63: vTerm] : ? [v64: vTerm] : ? [v65: vTerm] : % 81.47/11.30 ? [v66: vTerm] : ? [v67: vOptTerm] : ? [v68: vOptTerm] : ? [v69: % 81.47/11.30 vTerm] : ? [v70: vTerm] : ? [v71: vOptTerm] : ? [v72: vOptTerm] : ? % 81.47/11.30 [v73: vTerm] : ? [v74: vTerm] : ? [v75: vTerm] : ? [v76: vOptTerm] : ? % 81.47/11.30 [v77: vTerm] : ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: vOptTerm] : % 81.47/11.30 ? [v81: vTerm] : ? [v82: vTerm] : ? [v83: vOptTerm] : ? [v84: vTerm] : % 81.47/11.30 ? [v85: vOptTerm] : ? [v86: vTerm] : ? [v87: vTerm] : ? [v88: vTerm] : % 81.47/11.30 ? [v89: vOptTerm] : ? [v90: vTerm] : ? [v91: vTerm] : ? [v92: vTerm] : % 81.47/11.30 ? [v93: vOptTerm] : ? [v94: vTerm] : ? [v95: vOptTerm] : ? [v96: % 81.47/11.30 vOptTerm] : ? [v97: vTerm] : ? [v98: vTerm] : ? [v99: vOptTerm] : ? % 81.47/11.30 [v100: vOptTerm] : ? [v101: vTerm] : ? [v102: vTerm] : ? [v103: vTerm] % 81.47/11.30 : ? [v104: vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: % 81.47/11.30 vTerm] : ? [v108: vOptTerm] : ? [v109: vOptTerm] : ? [v110: vTerm] : % 81.47/11.30 ? [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : ? [v114: % 81.47/11.30 vOptTerm] : ? [v115: vOptTerm] : ? [v116: vTerm] : ? [v117: vTerm] : % 81.47/11.30 ? [v118: vTerm] : ? [v119: vOptTerm] : ? [v120: vTerm] : ? [v121: % 81.47/11.30 vTerm] : ? [v122: vTerm] : ? [v123: vOptTerm] : ? [v124: vTerm] : ? % 81.47/11.30 [v125: vTerm] : ? [v126: vTerm] : ? [v127: vOptTerm] : (vreduce(v5) = v6 % 81.47/11.30 & vOptTerm(v114) & vOptTerm(v108) & vOptTerm(v99) & vOptTerm(v95) & % 81.47/11.30 vOptTerm(v83) & vOptTerm(v78) & vOptTerm(v71) & vOptTerm(v67) & % 81.47/11.30 vOptTerm(v56) & vOptTerm(v51) & vOptTerm(v44) & vOptTerm(v40) & % 81.47/11.30 vOptTerm(v28) & vOptTerm(v23) & vOptTerm(v15) & vOptTerm(v10) & % 81.47/11.30 vOptTerm(v6) & vTerm(v125) & vTerm(v124) & vTerm(v121) & vTerm(v120) & % 81.47/11.30 vTerm(v113) & vTerm(v112) & vTerm(v111) & vTerm(v107) & vTerm(v106) & % 81.47/11.30 vTerm(v105) & vTerm(v98) & vTerm(v94) & vTerm(v90) & vTerm(v82) & % 81.47/11.30 vTerm(v77) & vTerm(v70) & vTerm(v66) & vTerm(v63) & vTerm(v55) & % 81.47/11.30 vTerm(v50) & vTerm(v43) & vTerm(v39) & vTerm(v35) & vTerm(v34) & % 81.47/11.30 vTerm(v27) & vTerm(v26) & vTerm(v22) & vTerm(v21) & vTerm(v14) & % 81.47/11.30 vTerm(v13) & vTerm(v9) & vTerm(v8) & vTerm(v7) & ((v127 = v6 & v126 = v5 % 81.47/11.30 & vsomeTerm(v124) = v6 & vIfelse(vTrue, v124, v125) = v5) | (v123 = % 81.47/11.30 v6 & v122 = v5 & vsomeTerm(v121) = v6 & vIfelse(vFalse, v120, v121) % 81.47/11.30 = v5) | (v119 = v6 & v116 = v5 & v115 = v114 & ~ (v111 = vFalse) & % 81.47/11.30 ~ (v111 = vTrue) & vreduce(v111) = v114 & vgetTerm(v114) = v117 & % 81.47/11.30 vsomeTerm(v118) = v6 & vIfelse(v117, v112, v113) = v118 & % 81.47/11.30 vIfelse(v111, v112, v113) = v5 & vTerm(v118) & vTerm(v117) & % 81.47/11.30 visSomeTerm(v114)) | (v110 = v5 & v109 = v108 & v6 = vnoTerm & ~ % 81.47/11.30 (v105 = vFalse) & ~ (v105 = vTrue) & vreduce(v105) = v108 & % 81.47/11.30 vIfelse(v105, v106, v107) = v5 & ~ visSomeTerm(v108)) | (v104 = v6 % 81.47/11.30 & v101 = v5 & v100 = v99 & vreduce(v98) = v99 & vgetTerm(v99) = v102 % 81.47/11.30 & vsomeTerm(v103) = v6 & vSucc(v102) = v103 & vSucc(v98) = v5 & % 81.47/11.30 vTerm(v103) & vTerm(v102) & visSomeTerm(v99)) | (v97 = v5 & v96 = % 81.47/11.30 v95 & v6 = vnoTerm & vreduce(v94) = v95 & vSucc(v94) = v5 & ~ % 81.47/11.30 visSomeTerm(v95)) | (v93 = v6 & v92 = v5 & vsomeTerm(v90) = v6 & % 81.47/11.30 vPred(v91) = v5 & vSucc(v90) = v91 & vTerm(v91) & visNV(v90)) | (v89 % 81.47/11.30 = v6 & v86 = v5 & v85 = v83 & vreduce(v84) = v83 & vgetTerm(v83) = % 81.47/11.30 v87 & vsomeTerm(v88) = v6 & vPred(v87) = v88 & vPred(v84) = v5 & % 81.47/11.30 vSucc(v82) = v84 & vTerm(v88) & vTerm(v87) & vTerm(v84) & % 81.47/11.30 visSomeTerm(v83) & ~ visNV(v82)) | (v81 = v5 & v80 = v78 & v6 = % 81.47/11.30 vnoTerm & vreduce(v79) = v78 & vPred(v79) = v5 & vSucc(v77) = v79 & % 81.47/11.30 vTerm(v79) & ~ visSomeTerm(v78) & ~ visNV(v77)) | (v76 = v6 & v73 % 81.47/11.30 = v5 & v72 = v71 & ~ (v70 = vZero) & vreduce(v70) = v71 & % 81.47/11.30 vgetTerm(v71) = v74 & vsomeTerm(v75) = v6 & vPred(v74) = v75 & % 81.47/11.30 vPred(v70) = v5 & vTerm(v75) & vTerm(v74) & visSomeTerm(v71) & ! % 81.47/11.30 [v128: vTerm] : ( ~ (vSucc(v128) = v70) | ~ vTerm(v128))) | (v69 = % 81.47/11.30 v5 & v68 = v67 & v6 = vnoTerm & ~ (v66 = vZero) & vreduce(v66) = % 81.47/11.30 v67 & vPred(v66) = v5 & ~ visSomeTerm(v67) & ! [v128: vTerm] : ( ~ % 81.47/11.30 (vSucc(v128) = v66) | ~ vTerm(v128))) | (v65 = v5 & v6 = v4 & % 81.47/11.30 vIszero(v64) = v5 & vSucc(v63) = v64 & vTerm(v64) & visNV(v63)) | % 81.47/11.30 (v62 = v6 & v59 = v5 & v58 = v56 & vreduce(v57) = v56 & vgetTerm(v56) % 81.47/11.30 = v60 & vsomeTerm(v61) = v6 & vIszero(v60) = v61 & vIszero(v57) = v5 % 81.47/11.30 & vSucc(v55) = v57 & vTerm(v61) & vTerm(v60) & vTerm(v57) & % 81.47/11.30 visSomeTerm(v56) & ~ visNV(v55)) | (v54 = v5 & v53 = v51 & v6 = % 81.47/11.30 vnoTerm & vreduce(v52) = v51 & vIszero(v52) = v5 & vSucc(v50) = v52 % 81.47/11.30 & vTerm(v52) & ~ visSomeTerm(v51) & ~ visNV(v50)) | (v49 = v6 & % 81.47/11.30 v46 = v5 & v45 = v44 & ~ (v43 = vZero) & vreduce(v43) = v44 & % 81.47/11.30 vgetTerm(v44) = v47 & vsomeTerm(v48) = v6 & vIszero(v47) = v48 & % 81.47/11.30 vIszero(v43) = v5 & vTerm(v48) & vTerm(v47) & visSomeTerm(v44) & ! % 81.47/11.30 [v128: vTerm] : ( ~ (vSucc(v128) = v43) | ~ vTerm(v128))) | (v42 = % 81.47/11.30 v5 & v41 = v40 & v6 = vnoTerm & ~ (v39 = vZero) & vreduce(v39) = % 81.47/11.30 v40 & vIszero(v39) = v5 & ~ visSomeTerm(v40) & ! [v128: vTerm] : ( % 81.47/11.30 ~ (vSucc(v128) = v39) | ~ vTerm(v128))) | (v38 = v6 & v36 = v5 & % 81.47/11.30 vplusop(v34, v35) = v37 & vsomeTerm(v37) = v6 & vPlus(v34, v35) = v5 % 81.47/11.30 & vTerm(v37) & visNV(v35) & visNV(v34)) | (v33 = v6 & v30 = v5 & v29 % 81.47/11.30 = v28 & vreduce(v27) = v28 & vgetTerm(v28) = v31 & vsomeTerm(v32) = % 81.47/11.30 v6 & vPlus(v26, v31) = v32 & vPlus(v26, v27) = v5 & vTerm(v32) & % 81.47/11.30 vTerm(v31) & visSomeTerm(v28) & visNV(v26) & ~ visNV(v27)) | (v25 = % 81.47/11.30 v5 & v24 = v23 & v6 = vnoTerm & vreduce(v22) = v23 & vPlus(v21, v22) % 81.47/11.30 = v5 & visNV(v21) & ~ visSomeTerm(v23) & ~ visNV(v22)) | (v20 = v6 % 81.47/11.30 & v17 = v5 & v16 = v15 & vreduce(v13) = v15 & vgetTerm(v15) = v18 & % 81.47/11.30 vsomeTerm(v19) = v6 & vPlus(v18, v14) = v19 & vPlus(v13, v14) = v5 & % 81.47/11.30 vTerm(v19) & vTerm(v18) & visSomeTerm(v15) & ~ visNV(v13)) | (v12 = % 81.47/11.30 v5 & v11 = v10 & v6 = vnoTerm & vreduce(v8) = v10 & vPlus(v8, v9) = % 81.47/11.30 v5 & ~ visSomeTerm(v10) & ~ visNV(v8)) | (v7 = v5 & v6 = vnoTerm & % 81.47/11.30 ~ (v5 = v2) & ~ (v5 = v0) & ! [v128: vTerm] : ! [v129: vTerm] : % 81.47/11.30 ! [v130: vTerm] : ( ~ (vIfelse(v128, v129, v130) = v5) | ~ % 81.47/11.30 vTerm(v130) | ~ vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] % 81.47/11.30 : ! [v129: vTerm] : ( ~ (vPlus(v128, v129) = v5) | ~ vTerm(v129) | % 81.47/11.30 ~ vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 81.47/11.30 (vSucc(v128) = v129) | ~ vTerm(v128) | ? [v130: vTerm] : ( ~ % 81.47/11.30 (v130 = v5) & vIszero(v129) = v130 & vTerm(v130))) & ! [v128: % 81.47/11.30 vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = v129) | ~ % 81.47/11.30 vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = v5) & vPred(v129) = % 81.47/11.30 v130 & vTerm(v130))) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 81.47/11.30 (vIfelse(vFalse, v128, v129) = v5) | ~ vTerm(v129) | ~ % 81.47/11.30 vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 81.47/11.30 (vIfelse(vTrue, v128, v129) = v5) | ~ vTerm(v129) | ~ % 81.47/11.30 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vIszero(v128) = v5) | ~ % 81.47/11.30 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vPred(v128) = v5) | ~ % 81.47/11.30 vTerm(v128)) & ! [v128: vTerm] : ( ~ (vSucc(v128) = v5) | ~ % 81.47/11.30 vTerm(v128))) | (v6 = v3 & v5 = v2) | (v6 = v1 & v5 = v0))))) % 81.47/11.30 % 81.47/11.30 (function-axioms) % 81.47/11.30 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 81.47/11.30 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 81.47/11.30 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] % 81.47/11.30 : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ (vplusop(v3, v2) = v0)) & ! [v0: % 81.47/11.30 vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ % 81.47/11.30 (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) & ! [v0: vOptTerm] : ! % 81.47/11.30 [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vreduce(v2) = v1) | ~ % 81.47/11.30 (vreduce(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 81.47/11.30 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 81.47/11.30 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 81.47/11.30 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 81.47/11.30 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 81.47/11.30 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 81.47/11.30 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 81.47/11.30 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 81.47/11.30 % 81.47/11.30 Further assumptions not needed in the proof: % 81.47/11.30 -------------------------------------------- % 81.47/11.31 DIFF-B-Nat, DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, % 81.47/11.31 DIFF-False-Pred, DIFF-False-Succ, DIFF-Ifelse-Iszero, DIFF-Ifelse-Plus, % 81.47/11.31 DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, DIFF-Iszero-Plus, % 81.47/11.31 DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, DIFF-Succ-Plus, % 81.47/11.31 DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, DIFF-True-Iszero, % 81.47/11.31 DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, DIFF-True-Zero, % 81.47/11.31 DIFF-Zero-Iszero, DIFF-Zero-Plus, DIFF-Zero-Pred, DIFF-Zero-Succ, % 81.47/11.31 DIFF-noTerm-someTerm, EQ-Ifelse, EQ-Iszero, EQ-Plus, EQ-Pred, EQ-Succ, % 81.47/11.31 Preservation-Ifelse-IH1, Preservation-Ifelse-IH2, TPlus, TPlus_inv0, TPlus_inv1, % 81.47/11.31 TPlus_inv2, TPred, TPred_inv1, TPred_inv2, TSucc, TSucc_inv1, TSucc_inv2, TZero, % 81.47/11.31 Tfalse, Tiszero, Tiszero_inv1, dom-OptTerm, dom-Term, dom-Ty, isNV-0, isNV-1, % 81.47/11.31 isNV-2, isNV-false-INV, isNV-true-INV, isSomeTerm-0, isSomeTerm-1, % 81.47/11.31 isSomeTerm-false-INV, isValue-0, isValue-1, isValue-2, isValue-false-INV, % 81.47/11.31 isValue-true-INV, plusop-0, plusop-1, plusop-2, plusop-INV, reduce-0, reduce-1, % 81.47/11.31 reduce-10, reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, reduce-16, % 81.47/11.31 reduce-17, reduce-18, reduce-19, reduce-20, reduce-21, reduce-22, reduce-23, % 81.47/11.31 reduce-3, reduce-4, reduce-5, reduce-7, reduce-8, reduce-9 % 81.47/11.31 % 81.47/11.31 Those formulas are unsatisfiable: % 81.47/11.31 --------------------------------- % 81.47/11.31 % 81.47/11.31 Begin of proof % 81.47/11.31 | % 81.47/11.31 | ALPHA: (DIFF-False-Zero) implies: % 81.47/11.31 | (1) ~ (vFalse = vZero) % 81.47/11.31 | % 81.47/11.31 | ALPHA: (reduce-2) implies: % 81.47/11.31 | (2) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ( ~ % 81.47/11.31 | (vIfelse(v0, v1, v2) = v3) | ~ vTerm(v2) | ~ vTerm(v1) | ~ % 81.47/11.31 | vTerm(v0) | ? [v4: vOptTerm] : ? [v5: vOptTerm] : ? [v6: vTerm] : % 81.47/11.31 | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] % 81.47/11.31 | : ? [v11: vTerm] : ? [v12: vTerm] : (vTerm(v12) & vTerm(v11) & % 81.47/11.31 | vTerm(v10) & vTerm(v9) & ((v12 = v2 & v11 = v1 & v0 = vTrue) | (v10 % 81.47/11.31 | = v2 & v9 = v1 & v0 = vFalse) | (vreduce(v0) = v4 & % 81.47/11.31 | vOptTerm(v4) & ( ~ visSomeTerm(v4) | (v8 = v5 & vreduce(v3) = % 81.47/11.31 | v5 & vgetTerm(v4) = v6 & vsomeTerm(v7) = v5 & vIfelse(v6, % 81.47/11.31 | v1, v2) = v7 & vOptTerm(v5) & vTerm(v7) & vTerm(v6))))))) % 81.47/11.31 | % 81.47/11.31 | ALPHA: (reduce-6) implies: % 81.47/11.31 | (3) ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 81.47/11.31 | vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 81.47/11.31 | % 81.47/11.31 | ALPHA: (reduce-INV) implies: % 81.47/11.32 | (4) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] % 81.47/11.32 | : ? [v4: vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 81.47/11.32 | vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 81.47/11.32 | vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & % 81.47/11.32 | ? [v5: vTerm] : ( ~ vTerm(v5) | ? [v6: vOptTerm] : ? [v7: vTerm] : % 81.47/11.32 | ? [v8: vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: % 81.47/11.32 | vOptTerm] : ? [v12: vTerm] : ? [v13: vTerm] : ? [v14: vTerm] : % 81.47/11.32 | ? [v15: vOptTerm] : ? [v16: vOptTerm] : ? [v17: vTerm] : ? % 81.47/11.32 | [v18: vTerm] : ? [v19: vTerm] : ? [v20: vOptTerm] : ? [v21: % 81.47/11.32 | vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : ? [v24: % 81.47/11.32 | vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 81.47/11.32 | ? [v28: vOptTerm] : ? [v29: vOptTerm] : ? [v30: vTerm] : ? % 81.47/11.32 | [v31: vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: % 81.47/11.32 | vTerm] : ? [v35: vTerm] : ? [v36: vTerm] : ? [v37: vTerm] : ? % 81.47/11.32 | [v38: vOptTerm] : ? [v39: vTerm] : ? [v40: vOptTerm] : ? [v41: % 81.47/11.32 | vOptTerm] : ? [v42: vTerm] : ? [v43: vTerm] : ? [v44: % 81.47/11.32 | vOptTerm] : ? [v45: vOptTerm] : ? [v46: vTerm] : ? [v47: % 81.47/11.32 | vTerm] : ? [v48: vTerm] : ? [v49: vOptTerm] : ? [v50: vTerm] : % 81.47/11.32 | ? [v51: vOptTerm] : ? [v52: vTerm] : ? [v53: vOptTerm] : ? % 81.47/11.32 | [v54: vTerm] : ? [v55: vTerm] : ? [v56: vOptTerm] : ? [v57: % 81.47/11.32 | vTerm] : ? [v58: vOptTerm] : ? [v59: vTerm] : ? [v60: vTerm] : % 81.47/11.32 | ? [v61: vTerm] : ? [v62: vOptTerm] : ? [v63: vTerm] : ? [v64: % 81.47/11.32 | vTerm] : ? [v65: vTerm] : ? [v66: vTerm] : ? [v67: vOptTerm] : % 81.47/11.32 | ? [v68: vOptTerm] : ? [v69: vTerm] : ? [v70: vTerm] : ? [v71: % 81.47/11.32 | vOptTerm] : ? [v72: vOptTerm] : ? [v73: vTerm] : ? [v74: % 81.47/11.32 | vTerm] : ? [v75: vTerm] : ? [v76: vOptTerm] : ? [v77: vTerm] : % 81.47/11.32 | ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: vOptTerm] : ? % 81.47/11.32 | [v81: vTerm] : ? [v82: vTerm] : ? [v83: vOptTerm] : ? [v84: % 81.47/11.32 | vTerm] : ? [v85: vOptTerm] : ? [v86: vTerm] : ? [v87: vTerm] : % 81.47/11.32 | ? [v88: vTerm] : ? [v89: vOptTerm] : ? [v90: vTerm] : ? [v91: % 81.47/11.32 | vTerm] : ? [v92: vTerm] : ? [v93: vOptTerm] : ? [v94: vTerm] : % 81.47/11.32 | ? [v95: vOptTerm] : ? [v96: vOptTerm] : ? [v97: vTerm] : ? % 81.47/11.32 | [v98: vTerm] : ? [v99: vOptTerm] : ? [v100: vOptTerm] : ? [v101: % 81.47/11.32 | vTerm] : ? [v102: vTerm] : ? [v103: vTerm] : ? [v104: % 81.47/11.32 | vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: % 81.47/11.32 | vTerm] : ? [v108: vOptTerm] : ? [v109: vOptTerm] : ? [v110: % 81.47/11.32 | vTerm] : ? [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : % 81.47/11.32 | ? [v114: vOptTerm] : ? [v115: vOptTerm] : ? [v116: vTerm] : ? % 81.47/11.32 | [v117: vTerm] : ? [v118: vTerm] : ? [v119: vOptTerm] : ? [v120: % 81.47/11.32 | vTerm] : ? [v121: vTerm] : ? [v122: vTerm] : ? [v123: % 81.47/11.32 | vOptTerm] : ? [v124: vTerm] : ? [v125: vTerm] : ? [v126: % 81.47/11.32 | vTerm] : ? [v127: vOptTerm] : (vreduce(v5) = v6 & vOptTerm(v114) % 81.47/11.32 | & vOptTerm(v108) & vOptTerm(v99) & vOptTerm(v95) & vOptTerm(v83) % 81.47/11.33 | & vOptTerm(v78) & vOptTerm(v71) & vOptTerm(v67) & vOptTerm(v56) & % 81.47/11.33 | vOptTerm(v51) & vOptTerm(v44) & vOptTerm(v40) & vOptTerm(v28) & % 81.47/11.33 | vOptTerm(v23) & vOptTerm(v15) & vOptTerm(v10) & vOptTerm(v6) & % 81.47/11.33 | vTerm(v125) & vTerm(v124) & vTerm(v121) & vTerm(v120) & % 81.47/11.33 | vTerm(v113) & vTerm(v112) & vTerm(v111) & vTerm(v107) & % 81.47/11.33 | vTerm(v106) & vTerm(v105) & vTerm(v98) & vTerm(v94) & vTerm(v90) % 81.47/11.33 | & vTerm(v82) & vTerm(v77) & vTerm(v70) & vTerm(v66) & vTerm(v63) % 81.47/11.33 | & vTerm(v55) & vTerm(v50) & vTerm(v43) & vTerm(v39) & vTerm(v35) % 81.47/11.33 | & vTerm(v34) & vTerm(v27) & vTerm(v26) & vTerm(v22) & vTerm(v21) % 81.47/11.33 | & vTerm(v14) & vTerm(v13) & vTerm(v9) & vTerm(v8) & vTerm(v7) & % 81.47/11.33 | ((v127 = v6 & v126 = v5 & vsomeTerm(v124) = v6 & vIfelse(vTrue, % 81.47/11.33 | v124, v125) = v5) | (v123 = v6 & v122 = v5 & % 81.47/11.33 | vsomeTerm(v121) = v6 & vIfelse(vFalse, v120, v121) = v5) | % 81.47/11.33 | (v119 = v6 & v116 = v5 & v115 = v114 & ~ (v111 = vFalse) & ~ % 81.47/11.33 | (v111 = vTrue) & vreduce(v111) = v114 & vgetTerm(v114) = v117 % 81.47/11.33 | & vsomeTerm(v118) = v6 & vIfelse(v117, v112, v113) = v118 & % 81.47/11.33 | vIfelse(v111, v112, v113) = v5 & vTerm(v118) & vTerm(v117) & % 81.47/11.33 | visSomeTerm(v114)) | (v110 = v5 & v109 = v108 & v6 = vnoTerm % 81.47/11.33 | & ~ (v105 = vFalse) & ~ (v105 = vTrue) & vreduce(v105) = % 81.47/11.33 | v108 & vIfelse(v105, v106, v107) = v5 & ~ visSomeTerm(v108)) % 81.47/11.33 | | (v104 = v6 & v101 = v5 & v100 = v99 & vreduce(v98) = v99 & % 81.47/11.33 | vgetTerm(v99) = v102 & vsomeTerm(v103) = v6 & vSucc(v102) = % 81.47/11.33 | v103 & vSucc(v98) = v5 & vTerm(v103) & vTerm(v102) & % 81.47/11.33 | visSomeTerm(v99)) | (v97 = v5 & v96 = v95 & v6 = vnoTerm & % 81.47/11.33 | vreduce(v94) = v95 & vSucc(v94) = v5 & ~ visSomeTerm(v95)) | % 81.47/11.33 | (v93 = v6 & v92 = v5 & vsomeTerm(v90) = v6 & vPred(v91) = v5 & % 81.47/11.33 | vSucc(v90) = v91 & vTerm(v91) & visNV(v90)) | (v89 = v6 & v86 % 81.47/11.33 | = v5 & v85 = v83 & vreduce(v84) = v83 & vgetTerm(v83) = v87 & % 81.47/11.33 | vsomeTerm(v88) = v6 & vPred(v87) = v88 & vPred(v84) = v5 & % 81.47/11.33 | vSucc(v82) = v84 & vTerm(v88) & vTerm(v87) & vTerm(v84) & % 81.47/11.33 | visSomeTerm(v83) & ~ visNV(v82)) | (v81 = v5 & v80 = v78 & % 81.47/11.33 | v6 = vnoTerm & vreduce(v79) = v78 & vPred(v79) = v5 & % 81.47/11.33 | vSucc(v77) = v79 & vTerm(v79) & ~ visSomeTerm(v78) & ~ % 81.47/11.33 | visNV(v77)) | (v76 = v6 & v73 = v5 & v72 = v71 & ~ (v70 = % 81.47/11.33 | vZero) & vreduce(v70) = v71 & vgetTerm(v71) = v74 & % 81.47/11.33 | vsomeTerm(v75) = v6 & vPred(v74) = v75 & vPred(v70) = v5 & % 81.47/11.33 | vTerm(v75) & vTerm(v74) & visSomeTerm(v71) & ! [v128: vTerm] % 81.47/11.33 | : ( ~ (vSucc(v128) = v70) | ~ vTerm(v128))) | (v69 = v5 & % 81.47/11.33 | v68 = v67 & v6 = vnoTerm & ~ (v66 = vZero) & vreduce(v66) = % 81.47/11.33 | v67 & vPred(v66) = v5 & ~ visSomeTerm(v67) & ! [v128: % 81.47/11.33 | vTerm] : ( ~ (vSucc(v128) = v66) | ~ vTerm(v128))) | (v65 % 81.47/11.33 | = v5 & v6 = v4 & vIszero(v64) = v5 & vSucc(v63) = v64 & % 81.47/11.33 | vTerm(v64) & visNV(v63)) | (v62 = v6 & v59 = v5 & v58 = v56 & % 81.47/11.33 | vreduce(v57) = v56 & vgetTerm(v56) = v60 & vsomeTerm(v61) = % 81.47/11.33 | v6 & vIszero(v60) = v61 & vIszero(v57) = v5 & vSucc(v55) = % 81.47/11.33 | v57 & vTerm(v61) & vTerm(v60) & vTerm(v57) & visSomeTerm(v56) % 81.47/11.33 | & ~ visNV(v55)) | (v54 = v5 & v53 = v51 & v6 = vnoTerm & % 81.47/11.33 | vreduce(v52) = v51 & vIszero(v52) = v5 & vSucc(v50) = v52 & % 81.47/11.33 | vTerm(v52) & ~ visSomeTerm(v51) & ~ visNV(v50)) | (v49 = v6 % 81.47/11.33 | & v46 = v5 & v45 = v44 & ~ (v43 = vZero) & vreduce(v43) = % 81.47/11.33 | v44 & vgetTerm(v44) = v47 & vsomeTerm(v48) = v6 & % 81.47/11.33 | vIszero(v47) = v48 & vIszero(v43) = v5 & vTerm(v48) & % 81.47/11.33 | vTerm(v47) & visSomeTerm(v44) & ! [v128: vTerm] : ( ~ % 81.47/11.33 | (vSucc(v128) = v43) | ~ vTerm(v128))) | (v42 = v5 & v41 = % 81.47/11.33 | v40 & v6 = vnoTerm & ~ (v39 = vZero) & vreduce(v39) = v40 & % 81.47/11.33 | vIszero(v39) = v5 & ~ visSomeTerm(v40) & ! [v128: vTerm] : % 81.47/11.33 | ( ~ (vSucc(v128) = v39) | ~ vTerm(v128))) | (v38 = v6 & v36 % 81.47/11.33 | = v5 & vplusop(v34, v35) = v37 & vsomeTerm(v37) = v6 & % 81.47/11.33 | vPlus(v34, v35) = v5 & vTerm(v37) & visNV(v35) & visNV(v34)) % 81.47/11.33 | | (v33 = v6 & v30 = v5 & v29 = v28 & vreduce(v27) = v28 & % 81.47/11.33 | vgetTerm(v28) = v31 & vsomeTerm(v32) = v6 & vPlus(v26, v31) = % 81.47/11.33 | v32 & vPlus(v26, v27) = v5 & vTerm(v32) & vTerm(v31) & % 81.47/11.33 | visSomeTerm(v28) & visNV(v26) & ~ visNV(v27)) | (v25 = v5 & % 81.47/11.33 | v24 = v23 & v6 = vnoTerm & vreduce(v22) = v23 & vPlus(v21, % 81.47/11.33 | v22) = v5 & visNV(v21) & ~ visSomeTerm(v23) & ~ % 81.47/11.33 | visNV(v22)) | (v20 = v6 & v17 = v5 & v16 = v15 & vreduce(v13) % 81.47/11.33 | = v15 & vgetTerm(v15) = v18 & vsomeTerm(v19) = v6 & % 81.47/11.33 | vPlus(v18, v14) = v19 & vPlus(v13, v14) = v5 & vTerm(v19) & % 81.47/11.33 | vTerm(v18) & visSomeTerm(v15) & ~ visNV(v13)) | (v12 = v5 & % 81.47/11.33 | v11 = v10 & v6 = vnoTerm & vreduce(v8) = v10 & vPlus(v8, v9) % 81.47/11.33 | = v5 & ~ visSomeTerm(v10) & ~ visNV(v8)) | (v7 = v5 & v6 = % 81.47/11.33 | vnoTerm & ~ (v5 = v2) & ~ (v5 = v0) & ! [v128: vTerm] : ! % 81.47/11.33 | [v129: vTerm] : ! [v130: vTerm] : ( ~ (vIfelse(v128, v129, % 81.47/11.33 | v130) = v5) | ~ vTerm(v130) | ~ vTerm(v129) | ~ % 81.47/11.33 | vTerm(v128)) & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ % 81.47/11.33 | (vPlus(v128, v129) = v5) | ~ vTerm(v129) | ~ vTerm(v128)) % 81.47/11.33 | & ! [v128: vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = % 81.47/11.33 | v129) | ~ vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = % 81.47/11.33 | v5) & vIszero(v129) = v130 & vTerm(v130))) & ! [v128: % 81.47/11.33 | vTerm] : ! [v129: vTerm] : ( ~ (vSucc(v128) = v129) | ~ % 81.47/11.33 | vTerm(v128) | ? [v130: vTerm] : ( ~ (v130 = v5) & % 81.47/11.33 | vPred(v129) = v130 & vTerm(v130))) & ! [v128: vTerm] : % 81.47/11.33 | ! [v129: vTerm] : ( ~ (vIfelse(vFalse, v128, v129) = v5) | ~ % 81.47/11.33 | vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] : ! % 81.47/11.33 | [v129: vTerm] : ( ~ (vIfelse(vTrue, v128, v129) = v5) | ~ % 81.47/11.33 | vTerm(v129) | ~ vTerm(v128)) & ! [v128: vTerm] : ( ~ % 81.47/11.33 | (vIszero(v128) = v5) | ~ vTerm(v128)) & ! [v128: vTerm] : % 81.47/11.33 | ( ~ (vPred(v128) = v5) | ~ vTerm(v128)) & ! [v128: vTerm] : % 81.47/11.33 | ( ~ (vSucc(v128) = v5) | ~ vTerm(v128))) | (v6 = v3 & v5 = % 81.47/11.33 | v2) | (v6 = v1 & v5 = v0))))) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (Ttrue) implies: % 81.47/11.33 | (5) vptchecksimple(vTrue, vB) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (Tif) implies: % 81.47/11.33 | (6) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTy] : ! [v3: vTerm] : ! % 81.47/11.33 | [v4: vTerm] : ( ~ (vIfelse(v0, v1, v3) = v4) | ~ vTy(v2) | ~ % 81.47/11.33 | vTerm(v3) | ~ vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v3, v2) | % 81.47/11.33 | ~ vptchecksimple(v1, v2) | ~ vptchecksimple(v0, vB) | % 81.47/11.33 | vptchecksimple(v4, v2)) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (Tif_inv1) implies: % 81.47/11.33 | (7) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTy] : ! % 81.47/11.33 | [v4: vTerm] : ( ~ (vIfelse(v0, v1, v2) = v4) | ~ vTy(v3) | ~ % 81.47/11.33 | vTerm(v2) | ~ vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v4, v3) | % 81.47/11.33 | vptchecksimple(v0, vB)) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (TZero_inv) implies: % 81.47/11.33 | (8) vTerm(vZero) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (Tiszero_inv2) implies: % 81.47/11.33 | (9) vTy(vB) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (Preservation-Ifelse-IH0) implies: % 81.47/11.33 | (10) ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: vTy] : % 81.47/11.33 | ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ % 81.47/11.33 | vTerm(v2) | ~ vptchecksimple(vt1, v1) | vptchecksimple(v2, v1))) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (Preservation-Ifelse-t1-isSomeTerm-True) implies: % 81.47/11.33 | (11) vTerm(vTrue) % 81.47/11.33 | (12) vTerm(vFalse) % 81.47/11.33 | (13) vTerm(vt3) % 81.47/11.33 | (14) vTerm(vt2) % 81.47/11.33 | (15) vTerm(vt1) % 81.47/11.33 | (16) ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: vOptTerm] : ? [v3: vTy] % 81.47/11.33 | : ? [v4: vTerm] : ( ~ (vt1 = vFalse) & ~ (vt1 = vTrue) & vreduce(v1) % 81.47/11.33 | = v2 & vreduce(vt1) = v0 & vsomeTerm(v4) = v2 & vIfelse(vt1, vt2, % 81.47/11.33 | vt3) = v1 & vTy(v3) & vOptTerm(v2) & vOptTerm(v0) & vTerm(v4) & % 81.47/11.33 | vTerm(v1) & vptchecksimple(v1, v3) & visSomeTerm(v0) & ~ % 81.47/11.33 | vptchecksimple(v4, v3)) % 81.47/11.33 | % 81.47/11.33 | ALPHA: (function-axioms) implies: % 81.47/11.33 | (17) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 81.47/11.33 | (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) % 81.47/11.33 | (18) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : (v1 = v0 | ~ % 81.47/11.33 | (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) % 81.47/11.33 | (19) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 81.47/11.33 | (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) % 81.47/11.33 | % 81.47/11.33 | DELTA: instantiating (3) with fresh symbols all_90_0, all_90_1 gives: % 81.47/11.34 | (20) vreduce(all_90_1) = all_90_0 & vsomeTerm(vZero) = all_90_0 & % 81.47/11.34 | vPred(vZero) = all_90_1 & vOptTerm(all_90_0) & vTerm(all_90_1) % 81.47/11.34 | % 81.47/11.34 | ALPHA: (20) implies: % 81.47/11.34 | (21) vsomeTerm(vZero) = all_90_0 % 81.47/11.34 | % 81.47/11.34 | DELTA: instantiating (10) with fresh symbol all_101_0 gives: % 81.47/11.34 | (22) vreduce(vt1) = all_101_0 & vOptTerm(all_101_0) & ! [v0: vTy] : ! % 81.47/11.34 | [v1: vTerm] : ( ~ (vsomeTerm(v1) = all_101_0) | ~ vTy(v0) | ~ % 81.47/11.34 | vTerm(v1) | ~ vptchecksimple(vt1, v0) | vptchecksimple(v1, v0)) % 81.47/11.34 | % 81.47/11.34 | ALPHA: (22) implies: % 81.47/11.34 | (23) vreduce(vt1) = all_101_0 % 81.47/11.34 | (24) ! [v0: vTy] : ! [v1: vTerm] : ( ~ (vsomeTerm(v1) = all_101_0) | ~ % 81.47/11.34 | vTy(v0) | ~ vTerm(v1) | ~ vptchecksimple(vt1, v0) | % 81.47/11.34 | vptchecksimple(v1, v0)) % 81.47/11.34 | % 81.47/11.34 | DELTA: instantiating (16) with fresh symbols all_113_0, all_113_1, all_113_2, % 81.47/11.34 | all_113_3, all_113_4 gives: % 81.47/11.34 | (25) ~ (vt1 = vFalse) & ~ (vt1 = vTrue) & vreduce(all_113_3) = all_113_2 % 81.47/11.34 | & vreduce(vt1) = all_113_4 & vsomeTerm(all_113_0) = all_113_2 & % 81.47/11.34 | vIfelse(vt1, vt2, vt3) = all_113_3 & vTy(all_113_1) & % 81.47/11.34 | vOptTerm(all_113_2) & vOptTerm(all_113_4) & vTerm(all_113_0) & % 81.47/11.34 | vTerm(all_113_3) & vptchecksimple(all_113_3, all_113_1) & % 81.47/11.34 | visSomeTerm(all_113_4) & ~ vptchecksimple(all_113_0, all_113_1) % 81.47/11.34 | % 81.47/11.34 | ALPHA: (25) implies: % 81.47/11.34 | (26) ~ (vt1 = vTrue) % 81.47/11.34 | (27) ~ (vt1 = vFalse) % 81.47/11.34 | (28) ~ vptchecksimple(all_113_0, all_113_1) % 81.47/11.34 | (29) visSomeTerm(all_113_4) % 81.47/11.34 | (30) vptchecksimple(all_113_3, all_113_1) % 81.47/11.34 | (31) vTerm(all_113_0) % 81.47/11.34 | (32) vOptTerm(all_113_4) % 81.47/11.34 | (33) vTy(all_113_1) % 81.47/11.34 | (34) vIfelse(vt1, vt2, vt3) = all_113_3 % 81.47/11.34 | (35) vsomeTerm(all_113_0) = all_113_2 % 81.47/11.34 | (36) vreduce(vt1) = all_113_4 % 81.47/11.34 | (37) vreduce(all_113_3) = all_113_2 % 81.47/11.34 | % 81.47/11.34 | DELTA: instantiating (4) with fresh symbols all_119_0, all_119_1, all_119_2, % 81.47/11.34 | all_119_3, all_119_4 gives: % 81.47/11.35 | (38) vsomeTerm(vFalse) = all_119_0 & vsomeTerm(vTrue) = all_119_1 & % 81.47/11.35 | vsomeTerm(vZero) = all_119_3 & vIszero(vZero) = all_119_2 & % 81.47/11.35 | vPred(vZero) = all_119_4 & vOptTerm(all_119_0) & vOptTerm(all_119_1) & % 81.47/11.35 | vOptTerm(all_119_3) & vTerm(all_119_2) & vTerm(all_119_4) & ? [v0: % 81.47/11.35 | vTerm] : ( ~ vTerm(v0) | ? [v1: vOptTerm] : ? [v2: vTerm] : ? % 81.47/11.35 | [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : ? [v6: vOptTerm] % 81.47/11.35 | : ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : ? [v10: % 81.47/11.35 | vOptTerm] : ? [v11: vOptTerm] : ? [v12: vTerm] : ? [v13: vTerm] % 81.47/11.35 | : ? [v14: vTerm] : ? [v15: vOptTerm] : ? [v16: vTerm] : ? [v17: % 81.47/11.35 | vTerm] : ? [v18: vOptTerm] : ? [v19: vOptTerm] : ? [v20: vTerm] % 81.47/11.35 | : ? [v21: vTerm] : ? [v22: vTerm] : ? [v23: vOptTerm] : ? [v24: % 81.47/11.35 | vOptTerm] : ? [v25: vTerm] : ? [v26: vTerm] : ? [v27: vTerm] : % 81.47/11.35 | ? [v28: vOptTerm] : ? [v29: vTerm] : ? [v30: vTerm] : ? [v31: % 81.47/11.35 | vTerm] : ? [v32: vTerm] : ? [v33: vOptTerm] : ? [v34: vTerm] : % 81.47/11.35 | ? [v35: vOptTerm] : ? [v36: vOptTerm] : ? [v37: vTerm] : ? [v38: % 81.47/11.35 | vTerm] : ? [v39: vOptTerm] : ? [v40: vOptTerm] : ? [v41: vTerm] % 81.47/11.35 | : ? [v42: vTerm] : ? [v43: vTerm] : ? [v44: vOptTerm] : ? [v45: % 81.47/11.35 | vTerm] : ? [v46: vOptTerm] : ? [v47: vTerm] : ? [v48: vOptTerm] % 81.47/11.35 | : ? [v49: vTerm] : ? [v50: vTerm] : ? [v51: vOptTerm] : ? [v52: % 81.47/11.35 | vTerm] : ? [v53: vOptTerm] : ? [v54: vTerm] : ? [v55: vTerm] : % 81.47/11.35 | ? [v56: vTerm] : ? [v57: vOptTerm] : ? [v58: vTerm] : ? [v59: % 81.47/11.35 | vTerm] : ? [v60: vTerm] : ? [v61: vTerm] : ? [v62: vOptTerm] : % 81.47/11.35 | ? [v63: vOptTerm] : ? [v64: vTerm] : ? [v65: vTerm] : ? [v66: % 81.47/11.35 | vOptTerm] : ? [v67: vOptTerm] : ? [v68: vTerm] : ? [v69: vTerm] % 81.47/11.35 | : ? [v70: vTerm] : ? [v71: vOptTerm] : ? [v72: vTerm] : ? [v73: % 81.47/11.35 | vOptTerm] : ? [v74: vTerm] : ? [v75: vOptTerm] : ? [v76: vTerm] % 81.47/11.35 | : ? [v77: vTerm] : ? [v78: vOptTerm] : ? [v79: vTerm] : ? [v80: % 81.47/11.35 | vOptTerm] : ? [v81: vTerm] : ? [v82: vTerm] : ? [v83: vTerm] : % 81.47/11.35 | ? [v84: vOptTerm] : ? [v85: vTerm] : ? [v86: vTerm] : ? [v87: % 81.47/11.35 | vTerm] : ? [v88: vOptTerm] : ? [v89: vTerm] : ? [v90: vOptTerm] % 81.47/11.35 | : ? [v91: vOptTerm] : ? [v92: vTerm] : ? [v93: vTerm] : ? [v94: % 81.47/11.35 | vOptTerm] : ? [v95: vOptTerm] : ? [v96: vTerm] : ? [v97: vTerm] % 81.47/11.35 | : ? [v98: vTerm] : ? [v99: vOptTerm] : ? [v100: vTerm] : ? % 81.47/11.35 | [v101: vTerm] : ? [v102: vTerm] : ? [v103: vOptTerm] : ? [v104: % 81.47/11.35 | vOptTerm] : ? [v105: vTerm] : ? [v106: vTerm] : ? [v107: vTerm] % 81.47/11.35 | : ? [v108: vTerm] : ? [v109: vOptTerm] : ? [v110: vOptTerm] : ? % 81.47/11.35 | [v111: vTerm] : ? [v112: vTerm] : ? [v113: vTerm] : ? [v114: % 81.47/11.35 | vOptTerm] : ? [v115: vTerm] : ? [v116: vTerm] : ? [v117: vTerm] % 81.47/11.35 | : ? [v118: vOptTerm] : ? [v119: vTerm] : ? [v120: vTerm] : ? % 81.47/11.35 | [v121: vTerm] : ? [v122: vOptTerm] : (vreduce(v0) = v1 & % 81.47/11.35 | vOptTerm(v109) & vOptTerm(v103) & vOptTerm(v94) & vOptTerm(v90) & % 81.47/11.35 | vOptTerm(v78) & vOptTerm(v73) & vOptTerm(v66) & vOptTerm(v62) & % 81.47/11.35 | vOptTerm(v51) & vOptTerm(v46) & vOptTerm(v39) & vOptTerm(v35) & % 81.47/11.35 | vOptTerm(v23) & vOptTerm(v18) & vOptTerm(v10) & vOptTerm(v5) & % 81.47/11.35 | vOptTerm(v1) & vTerm(v120) & vTerm(v119) & vTerm(v116) & % 81.47/11.35 | vTerm(v115) & vTerm(v108) & vTerm(v107) & vTerm(v106) & % 81.47/11.35 | vTerm(v102) & vTerm(v101) & vTerm(v100) & vTerm(v93) & vTerm(v89) % 81.47/11.35 | & vTerm(v85) & vTerm(v77) & vTerm(v72) & vTerm(v65) & vTerm(v61) & % 81.47/11.35 | vTerm(v58) & vTerm(v50) & vTerm(v45) & vTerm(v38) & vTerm(v34) & % 81.47/11.35 | vTerm(v30) & vTerm(v29) & vTerm(v22) & vTerm(v21) & vTerm(v17) & % 81.47/11.35 | vTerm(v16) & vTerm(v9) & vTerm(v8) & vTerm(v4) & vTerm(v3) & % 81.47/11.35 | vTerm(v2) & ((v122 = v1 & v121 = v0 & vsomeTerm(v119) = v1 & % 81.47/11.35 | vIfelse(vTrue, v119, v120) = v0) | (v118 = v1 & v117 = v0 & % 81.47/11.35 | vsomeTerm(v116) = v1 & vIfelse(vFalse, v115, v116) = v0) | % 81.47/11.35 | (v114 = v1 & v111 = v0 & v110 = v109 & ~ (v106 = vFalse) & ~ % 81.47/11.35 | (v106 = vTrue) & vreduce(v106) = v109 & vgetTerm(v109) = v112 % 81.47/11.35 | & vsomeTerm(v113) = v1 & vIfelse(v112, v107, v108) = v113 & % 81.47/11.35 | vIfelse(v106, v107, v108) = v0 & vTerm(v113) & vTerm(v112) & % 81.47/11.35 | visSomeTerm(v109)) | (v105 = v0 & v104 = v103 & v1 = vnoTerm & % 81.47/11.35 | ~ (v100 = vFalse) & ~ (v100 = vTrue) & vreduce(v100) = v103 % 81.47/11.35 | & vIfelse(v100, v101, v102) = v0 & ~ visSomeTerm(v103)) | % 81.47/11.35 | (v99 = v1 & v96 = v0 & v95 = v94 & vreduce(v93) = v94 & % 81.47/11.35 | vgetTerm(v94) = v97 & vsomeTerm(v98) = v1 & vSucc(v97) = v98 & % 81.47/11.35 | vSucc(v93) = v0 & vTerm(v98) & vTerm(v97) & visSomeTerm(v94)) % 81.47/11.35 | | (v92 = v0 & v91 = v90 & v1 = vnoTerm & vreduce(v89) = v90 & % 81.47/11.35 | vSucc(v89) = v0 & ~ visSomeTerm(v90)) | (v88 = v1 & v87 = v0 % 81.47/11.35 | & vsomeTerm(v85) = v1 & vPred(v86) = v0 & vSucc(v85) = v86 & % 81.47/11.35 | vTerm(v86) & visNV(v85)) | (v84 = v1 & v81 = v0 & v80 = v78 & % 81.47/11.35 | vreduce(v79) = v78 & vgetTerm(v78) = v82 & vsomeTerm(v83) = v1 % 81.47/11.35 | & vPred(v82) = v83 & vPred(v79) = v0 & vSucc(v77) = v79 & % 81.47/11.35 | vTerm(v83) & vTerm(v82) & vTerm(v79) & visSomeTerm(v78) & ~ % 81.47/11.35 | visNV(v77)) | (v76 = v0 & v75 = v73 & v1 = vnoTerm & % 81.47/11.35 | vreduce(v74) = v73 & vPred(v74) = v0 & vSucc(v72) = v74 & % 81.47/11.35 | vTerm(v74) & ~ visSomeTerm(v73) & ~ visNV(v72)) | (v71 = v1 % 81.47/11.35 | & v68 = v0 & v67 = v66 & ~ (v65 = vZero) & vreduce(v65) = v66 % 81.47/11.35 | & vgetTerm(v66) = v69 & vsomeTerm(v70) = v1 & vPred(v69) = v70 % 81.47/11.35 | & vPred(v65) = v0 & vTerm(v70) & vTerm(v69) & visSomeTerm(v66) % 81.47/11.35 | & ! [v123: vTerm] : ( ~ (vSucc(v123) = v65) | ~ % 81.47/11.35 | vTerm(v123))) | (v64 = v0 & v63 = v62 & v1 = vnoTerm & ~ % 81.47/11.35 | (v61 = vZero) & vreduce(v61) = v62 & vPred(v61) = v0 & ~ % 81.47/11.35 | visSomeTerm(v62) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v61) % 81.47/11.35 | | ~ vTerm(v123))) | (v60 = v0 & v1 = all_119_0 & % 81.47/11.35 | vIszero(v59) = v0 & vSucc(v58) = v59 & vTerm(v59) & % 81.47/11.35 | visNV(v58)) | (v57 = v1 & v54 = v0 & v53 = v51 & vreduce(v52) % 81.47/11.35 | = v51 & vgetTerm(v51) = v55 & vsomeTerm(v56) = v1 & % 81.47/11.35 | vIszero(v55) = v56 & vIszero(v52) = v0 & vSucc(v50) = v52 & % 81.47/11.35 | vTerm(v56) & vTerm(v55) & vTerm(v52) & visSomeTerm(v51) & ~ % 81.47/11.35 | visNV(v50)) | (v49 = v0 & v48 = v46 & v1 = vnoTerm & % 81.47/11.35 | vreduce(v47) = v46 & vIszero(v47) = v0 & vSucc(v45) = v47 & % 81.47/11.35 | vTerm(v47) & ~ visSomeTerm(v46) & ~ visNV(v45)) | (v44 = v1 % 81.47/11.35 | & v41 = v0 & v40 = v39 & ~ (v38 = vZero) & vreduce(v38) = v39 % 81.47/11.35 | & vgetTerm(v39) = v42 & vsomeTerm(v43) = v1 & vIszero(v42) = % 81.47/11.35 | v43 & vIszero(v38) = v0 & vTerm(v43) & vTerm(v42) & % 81.47/11.35 | visSomeTerm(v39) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v38) % 81.47/11.35 | | ~ vTerm(v123))) | (v37 = v0 & v36 = v35 & v1 = vnoTerm & % 81.47/11.35 | ~ (v34 = vZero) & vreduce(v34) = v35 & vIszero(v34) = v0 & ~ % 81.47/11.35 | visSomeTerm(v35) & ! [v123: vTerm] : ( ~ (vSucc(v123) = v34) % 81.47/11.35 | | ~ vTerm(v123))) | (v33 = v1 & v31 = v0 & vplusop(v29, % 81.47/11.35 | v30) = v32 & vsomeTerm(v32) = v1 & vPlus(v29, v30) = v0 & % 81.47/11.35 | vTerm(v32) & visNV(v30) & visNV(v29)) | (v28 = v1 & v25 = v0 & % 81.47/11.35 | v24 = v23 & vreduce(v22) = v23 & vgetTerm(v23) = v26 & % 81.47/11.35 | vsomeTerm(v27) = v1 & vPlus(v21, v26) = v27 & vPlus(v21, v22) % 81.47/11.35 | = v0 & vTerm(v27) & vTerm(v26) & visSomeTerm(v23) & visNV(v21) % 81.47/11.35 | & ~ visNV(v22)) | (v20 = v0 & v19 = v18 & v1 = vnoTerm & % 81.47/11.35 | vreduce(v17) = v18 & vPlus(v16, v17) = v0 & visNV(v16) & ~ % 81.47/11.35 | visSomeTerm(v18) & ~ visNV(v17)) | (v15 = v1 & v12 = v0 & v11 % 81.47/11.35 | = v10 & vreduce(v8) = v10 & vgetTerm(v10) = v13 & % 81.47/11.35 | vsomeTerm(v14) = v1 & vPlus(v13, v9) = v14 & vPlus(v8, v9) = % 81.47/11.35 | v0 & vTerm(v14) & vTerm(v13) & visSomeTerm(v10) & ~ % 81.47/11.35 | visNV(v8)) | (v7 = v0 & v6 = v5 & v1 = vnoTerm & vreduce(v3) = % 81.47/11.35 | v5 & vPlus(v3, v4) = v0 & ~ visSomeTerm(v5) & ~ visNV(v3)) | % 81.47/11.35 | (v2 = v0 & v1 = vnoTerm & ~ (v0 = all_119_2) & ~ (v0 = % 81.47/11.35 | all_119_4) & ! [v123: vTerm] : ! [v124: vTerm] : ! [v125: % 81.47/11.35 | vTerm] : ( ~ (vIfelse(v123, v124, v125) = v0) | ~ % 81.47/11.35 | vTerm(v125) | ~ vTerm(v124) | ~ vTerm(v123)) & ! [v123: % 81.47/11.35 | vTerm] : ! [v124: vTerm] : ( ~ (vPlus(v123, v124) = v0) | % 81.47/11.35 | ~ vTerm(v124) | ~ vTerm(v123)) & ! [v123: vTerm] : ! % 81.47/11.35 | [v124: vTerm] : ( ~ (vSucc(v123) = v124) | ~ vTerm(v123) | ? % 81.47/11.35 | [v125: vTerm] : ( ~ (v125 = v0) & vIszero(v124) = v125 & % 81.47/11.35 | vTerm(v125))) & ! [v123: vTerm] : ! [v124: vTerm] : ( ~ % 81.47/11.35 | (vSucc(v123) = v124) | ~ vTerm(v123) | ? [v125: vTerm] : ( % 81.47/11.35 | ~ (v125 = v0) & vPred(v124) = v125 & vTerm(v125))) & ! % 81.47/11.35 | [v123: vTerm] : ! [v124: vTerm] : ( ~ (vIfelse(vFalse, v123, % 81.47/11.35 | v124) = v0) | ~ vTerm(v124) | ~ vTerm(v123)) & ! % 81.47/11.35 | [v123: vTerm] : ! [v124: vTerm] : ( ~ (vIfelse(vTrue, v123, % 81.47/11.35 | v124) = v0) | ~ vTerm(v124) | ~ vTerm(v123)) & ! % 81.47/11.35 | [v123: vTerm] : ( ~ (vIszero(v123) = v0) | ~ vTerm(v123)) & % 81.47/11.35 | ! [v123: vTerm] : ( ~ (vPred(v123) = v0) | ~ vTerm(v123)) & % 81.47/11.35 | ! [v123: vTerm] : ( ~ (vSucc(v123) = v0) | ~ vTerm(v123))) | % 81.47/11.35 | (v1 = all_119_1 & v0 = all_119_2) | (v1 = all_119_3 & v0 = % 81.47/11.35 | all_119_4)))) % 81.47/11.35 | % 81.47/11.35 | ALPHA: (38) implies: % 81.47/11.35 | (39) vsomeTerm(vZero) = all_119_3 % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (17) with all_90_0, all_119_3, vZero, simplifying % 81.47/11.35 | with (21), (39) gives: % 81.47/11.35 | (40) all_119_3 = all_90_0 % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (19) with all_101_0, all_113_4, vt1, simplifying % 81.47/11.35 | with (23), (36) gives: % 81.47/11.35 | (41) all_113_4 = all_101_0 % 81.47/11.35 | % 81.47/11.35 | REDUCE: (32), (41) imply: % 81.47/11.35 | (42) vOptTerm(all_101_0) % 81.47/11.35 | % 81.47/11.35 | REDUCE: (29), (41) imply: % 81.47/11.35 | (43) visSomeTerm(all_101_0) % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (isSomeTerm-true-INV) with all_101_0, simplifying % 81.47/11.35 | with (42), (43) gives: % 81.47/11.35 | (44) ? [v0: vTerm] : (vsomeTerm(v0) = all_101_0 & vTerm(v0)) % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (Tif_inv3) with vt1, vt2, vt3, all_113_1, % 81.47/11.35 | all_113_3, simplifying with (13), (14), (15), (30), (33), (34) % 81.47/11.35 | gives: % 81.47/11.35 | (45) vptchecksimple(vt3, all_113_1) % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (Tif_inv2) with vt1, vt2, vt3, all_113_1, % 81.47/11.35 | all_113_3, simplifying with (13), (14), (15), (30), (33), (34) % 81.47/11.35 | gives: % 81.47/11.35 | (46) vptchecksimple(vt2, all_113_1) % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (7) with vt1, vt2, vt3, all_113_1, all_113_3, % 81.47/11.35 | simplifying with (13), (14), (15), (30), (33), (34) gives: % 81.47/11.35 | (47) vptchecksimple(vt1, vB) % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (2) with vt1, vt2, vt3, all_113_3, simplifying with % 81.47/11.35 | (13), (14), (15), (34) gives: % 81.47/11.35 | (48) ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: % 81.47/11.35 | vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : ? % 81.47/11.35 | [v7: vTerm] : ? [v8: vTerm] : (vTerm(v8) & vTerm(v7) & vTerm(v6) & % 81.47/11.35 | vTerm(v5) & ((v8 = vt3 & v7 = vt2 & vt1 = vTrue) | (v6 = vt3 & v5 = % 81.47/11.35 | vt2 & vt1 = vFalse) | (vreduce(vt1) = v0 & vOptTerm(v0) & ( ~ % 81.47/11.35 | visSomeTerm(v0) | (v4 = v1 & vreduce(all_113_3) = v1 & % 81.47/11.35 | vgetTerm(v0) = v2 & vsomeTerm(v3) = v1 & vIfelse(v2, vt2, % 81.47/11.35 | vt3) = v3 & vOptTerm(v1) & vTerm(v3) & vTerm(v2)))))) % 81.47/11.35 | % 81.47/11.35 | GROUND_INST: instantiating (EQ-someTerm) with vZero, vFalse, all_90_0, % 81.47/11.35 | simplifying with (8), (12), (21) gives: % 81.47/11.35 | (49) vFalse = vZero | ~ (vsomeTerm(vFalse) = all_90_0) % 81.47/11.35 | % 81.47/11.35 | DELTA: instantiating (44) with fresh symbol all_132_0 gives: % 81.47/11.35 | (50) vsomeTerm(all_132_0) = all_101_0 & vTerm(all_132_0) % 81.47/11.35 | % 81.47/11.35 | ALPHA: (50) implies: % 81.47/11.35 | (51) vTerm(all_132_0) % 81.47/11.35 | (52) vsomeTerm(all_132_0) = all_101_0 % 81.47/11.35 | % 81.47/11.35 | DELTA: instantiating (48) with fresh symbols all_138_0, all_138_1, all_138_2, % 81.47/11.35 | all_138_3, all_138_4, all_138_5, all_138_6, all_138_7, all_138_8 gives: % 81.47/11.36 | (53) vTerm(all_138_0) & vTerm(all_138_1) & vTerm(all_138_2) & % 81.47/11.36 | vTerm(all_138_3) & ((all_138_0 = vt3 & all_138_1 = vt2 & vt1 = vTrue) % 81.47/11.36 | | (all_138_2 = vt3 & all_138_3 = vt2 & vt1 = vFalse) | (vreduce(vt1) % 81.47/11.36 | = all_138_8 & vOptTerm(all_138_8) & ( ~ visSomeTerm(all_138_8) | % 81.47/11.36 | (all_138_4 = all_138_7 & vreduce(all_113_3) = all_138_7 & % 81.47/11.36 | vgetTerm(all_138_8) = all_138_6 & vsomeTerm(all_138_5) = % 81.47/11.36 | all_138_7 & vIfelse(all_138_6, vt2, vt3) = all_138_5 & % 81.47/11.36 | vOptTerm(all_138_7) & vTerm(all_138_5) & vTerm(all_138_6))))) % 81.47/11.36 | % 81.47/11.36 | ALPHA: (53) implies: % 81.47/11.36 | (54) (all_138_0 = vt3 & all_138_1 = vt2 & vt1 = vTrue) | (all_138_2 = vt3 & % 81.47/11.36 | all_138_3 = vt2 & vt1 = vFalse) | (vreduce(vt1) = all_138_8 & % 81.47/11.36 | vOptTerm(all_138_8) & ( ~ visSomeTerm(all_138_8) | (all_138_4 = % 81.47/11.36 | all_138_7 & vreduce(all_113_3) = all_138_7 & vgetTerm(all_138_8) % 81.47/11.36 | = all_138_6 & vsomeTerm(all_138_5) = all_138_7 & % 81.47/11.36 | vIfelse(all_138_6, vt2, vt3) = all_138_5 & vOptTerm(all_138_7) & % 81.47/11.36 | vTerm(all_138_5) & vTerm(all_138_6)))) % 81.47/11.36 | % 81.47/11.36 | BETA: splitting (54) gives: % 81.47/11.36 | % 81.47/11.36 | Case 1: % 81.47/11.36 | | % 81.47/11.36 | | (55) all_138_0 = vt3 & all_138_1 = vt2 & vt1 = vTrue % 81.47/11.36 | | % 81.47/11.36 | | ALPHA: (55) implies: % 81.47/11.36 | | (56) vt1 = vTrue % 81.47/11.36 | | % 81.47/11.36 | | REDUCE: (26), (56) imply: % 81.47/11.36 | | (57) $false % 81.47/11.36 | | % 81.47/11.36 | | CLOSE: (57) is inconsistent. % 81.47/11.36 | | % 81.47/11.36 | Case 2: % 81.47/11.36 | | % 81.47/11.36 | | (58) (all_138_2 = vt3 & all_138_3 = vt2 & vt1 = vFalse) | (vreduce(vt1) = % 81.47/11.36 | | all_138_8 & vOptTerm(all_138_8) & ( ~ visSomeTerm(all_138_8) | % 81.47/11.36 | | (all_138_4 = all_138_7 & vreduce(all_113_3) = all_138_7 & % 81.47/11.36 | | vgetTerm(all_138_8) = all_138_6 & vsomeTerm(all_138_5) = % 81.47/11.36 | | all_138_7 & vIfelse(all_138_6, vt2, vt3) = all_138_5 & % 81.47/11.36 | | vOptTerm(all_138_7) & vTerm(all_138_5) & vTerm(all_138_6)))) % 81.47/11.36 | | % 81.47/11.36 | | BETA: splitting (58) gives: % 81.47/11.36 | | % 81.47/11.36 | | Case 1: % 81.47/11.36 | | | % 81.47/11.36 | | | (59) all_138_2 = vt3 & all_138_3 = vt2 & vt1 = vFalse % 81.47/11.36 | | | % 81.47/11.36 | | | ALPHA: (59) implies: % 81.47/11.36 | | | (60) vt1 = vFalse % 81.47/11.36 | | | % 81.47/11.36 | | | REDUCE: (27), (60) imply: % 81.47/11.36 | | | (61) $false % 81.47/11.36 | | | % 81.47/11.36 | | | CLOSE: (61) is inconsistent. % 81.47/11.36 | | | % 81.47/11.36 | | Case 2: % 81.47/11.36 | | | % 81.47/11.36 | | | (62) vreduce(vt1) = all_138_8 & vOptTerm(all_138_8) & ( ~ % 81.47/11.36 | | | visSomeTerm(all_138_8) | (all_138_4 = all_138_7 & % 81.47/11.36 | | | vreduce(all_113_3) = all_138_7 & vgetTerm(all_138_8) = % 81.47/11.36 | | | all_138_6 & vsomeTerm(all_138_5) = all_138_7 & % 81.47/11.36 | | | vIfelse(all_138_6, vt2, vt3) = all_138_5 & vOptTerm(all_138_7) % 81.47/11.36 | | | & vTerm(all_138_5) & vTerm(all_138_6))) % 81.47/11.36 | | | % 81.47/11.36 | | | ALPHA: (62) implies: % 81.47/11.36 | | | (63) vreduce(vt1) = all_138_8 % 81.47/11.36 | | | (64) ~ visSomeTerm(all_138_8) | (all_138_4 = all_138_7 & % 81.47/11.36 | | | vreduce(all_113_3) = all_138_7 & vgetTerm(all_138_8) = all_138_6 % 81.47/11.36 | | | & vsomeTerm(all_138_5) = all_138_7 & vIfelse(all_138_6, vt2, % 81.47/11.36 | | | vt3) = all_138_5 & vOptTerm(all_138_7) & vTerm(all_138_5) & % 81.47/11.36 | | | vTerm(all_138_6)) % 81.47/11.36 | | | % 81.47/11.36 | | | BETA: splitting (49) gives: % 81.47/11.36 | | | % 81.47/11.36 | | | Case 1: % 81.47/11.36 | | | | % 81.47/11.36 | | | | % 81.47/11.36 | | | | GROUND_INST: instantiating (19) with all_101_0, all_138_8, vt1, % 81.47/11.36 | | | | simplifying with (23), (63) gives: % 81.47/11.36 | | | | (65) all_138_8 = all_101_0 % 81.47/11.36 | | | | % 81.47/11.36 | | | | BETA: splitting (64) gives: % 81.47/11.36 | | | | % 81.47/11.36 | | | | Case 1: % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | (66) ~ visSomeTerm(all_138_8) % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | REDUCE: (65), (66) imply: % 81.47/11.36 | | | | | (67) ~ visSomeTerm(all_101_0) % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | PRED_UNIFY: (43), (67) imply: % 81.47/11.36 | | | | | (68) $false % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | CLOSE: (68) is inconsistent. % 81.47/11.36 | | | | | % 81.47/11.36 | | | | Case 2: % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | (69) all_138_4 = all_138_7 & vreduce(all_113_3) = all_138_7 & % 81.47/11.36 | | | | | vgetTerm(all_138_8) = all_138_6 & vsomeTerm(all_138_5) = % 81.47/11.36 | | | | | all_138_7 & vIfelse(all_138_6, vt2, vt3) = all_138_5 & % 81.47/11.36 | | | | | vOptTerm(all_138_7) & vTerm(all_138_5) & vTerm(all_138_6) % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | ALPHA: (69) implies: % 81.47/11.36 | | | | | (70) vTerm(all_138_6) % 81.47/11.36 | | | | | (71) vTerm(all_138_5) % 81.47/11.36 | | | | | (72) vIfelse(all_138_6, vt2, vt3) = all_138_5 % 81.47/11.36 | | | | | (73) vsomeTerm(all_138_5) = all_138_7 % 81.47/11.36 | | | | | (74) vgetTerm(all_138_8) = all_138_6 % 81.47/11.36 | | | | | (75) vreduce(all_113_3) = all_138_7 % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | REDUCE: (65), (74) imply: % 81.47/11.36 | | | | | (76) vgetTerm(all_101_0) = all_138_6 % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | GROUND_INST: instantiating (19) with all_113_2, all_138_7, all_113_3, % 81.47/11.36 | | | | | simplifying with (37), (75) gives: % 81.47/11.36 | | | | | (77) all_138_7 = all_113_2 % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | REDUCE: (73), (77) imply: % 81.47/11.36 | | | | | (78) vsomeTerm(all_138_5) = all_113_2 % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | GROUND_INST: instantiating (6) with vTrue, vt2, all_113_1, vt3, % 81.47/11.36 | | | | | all_138_5, simplifying with (5), (11), (13), (14), (33), % 81.47/11.36 | | | | | (45), (46) gives: % 81.47/11.36 | | | | | (79) ~ (vIfelse(vTrue, vt2, vt3) = all_138_5) | % 81.47/11.36 | | | | | vptchecksimple(all_138_5, all_113_1) % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | GROUND_INST: instantiating (24) with vB, all_132_0, simplifying with % 81.47/11.36 | | | | | (9), (47), (51), (52) gives: % 81.47/11.36 | | | | | (80) vptchecksimple(all_132_0, vB) % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | GROUND_INST: instantiating (getTerm-0) with all_132_0, all_101_0, % 81.47/11.36 | | | | | simplifying with (51), (52) gives: % 81.47/11.36 | | | | | (81) vgetTerm(all_101_0) = all_132_0 % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | GROUND_INST: instantiating (EQ-someTerm) with all_113_0, all_138_5, % 81.47/11.36 | | | | | all_113_2, simplifying with (31), (35), (71), (78) gives: % 81.47/11.36 | | | | | (82) all_138_5 = all_113_0 % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | REDUCE: (72), (82) imply: % 81.47/11.36 | | | | | (83) vIfelse(all_138_6, vt2, vt3) = all_113_0 % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | BETA: splitting (79) gives: % 81.47/11.36 | | | | | % 81.47/11.36 | | | | | Case 1: % 81.47/11.36 | | | | | | % 81.47/11.36 | | | | | | % 81.47/11.36 | | | | | | GROUND_INST: instantiating (18) with all_138_6, all_132_0, % 81.47/11.36 | | | | | | all_101_0, simplifying with (76), (81) gives: % 81.47/11.36 | | | | | | (84) all_138_6 = all_132_0 % 81.47/11.36 | | | | | | % 81.47/11.36 | | | | | | REDUCE: (83), (84) imply: % 81.47/11.36 | | | | | | (85) vIfelse(all_132_0, vt2, vt3) = all_113_0 % 81.47/11.36 | | | | | | % 81.47/11.36 | | | | | | GROUND_INST: instantiating (6) with all_132_0, vt2, all_113_1, vt3, % 81.47/11.36 | | | | | | all_113_0, simplifying with (13), (14), (28), (33), % 81.47/11.36 | | | | | | (45), (46), (51), (80), (85) gives: % 81.47/11.36 | | | | | | (86) $false % 81.47/11.36 | | | | | | % 81.47/11.36 | | | | | | CLOSE: (86) is inconsistent. % 81.47/11.36 | | | | | | % 81.47/11.36 | | | | | Case 2: % 81.47/11.36 | | | | | | % 81.47/11.37 | | | | | | (87) vptchecksimple(all_138_5, all_113_1) % 81.47/11.37 | | | | | | % 81.47/11.37 | | | | | | REDUCE: (82), (87) imply: % 81.47/11.37 | | | | | | (88) vptchecksimple(all_113_0, all_113_1) % 81.47/11.37 | | | | | | % 81.47/11.37 | | | | | | PRED_UNIFY: (28), (88) imply: % 81.47/11.37 | | | | | | (89) $false % 81.47/11.37 | | | | | | % 81.47/11.37 | | | | | | CLOSE: (89) is inconsistent. % 81.47/11.37 | | | | | | % 81.47/11.37 | | | | | End of split % 81.47/11.37 | | | | | % 81.47/11.37 | | | | End of split % 81.47/11.37 | | | | % 81.47/11.37 | | | Case 2: % 81.47/11.37 | | | | % 81.47/11.37 | | | | (90) vFalse = vZero % 81.47/11.37 | | | | % 81.47/11.37 | | | | REDUCE: (1), (90) imply: % 81.47/11.37 | | | | (91) $false % 81.47/11.37 | | | | % 81.47/11.37 | | | | CLOSE: (91) is inconsistent. % 81.47/11.37 | | | | % 81.47/11.37 | | | End of split % 81.47/11.37 | | | % 81.47/11.37 | | End of split % 81.47/11.37 | | % 81.47/11.37 | End of split % 81.47/11.37 | % 81.47/11.37 End of proof % 81.47/11.37 % SZS output end Proof for theBenchmark % 81.47/11.37 % 81.47/11.37 10790ms %------------------------------------------------------------------------------