%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM240_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 : n011.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:37 PM UTC 2026 % Result : Theorem 16.25s 2.96s % Output : Proof 20.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.16 % Problem : COM240_1 : TPTP v9.3.0. Released v9.3.0. % 0.10/0.16 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.38 % Computer : n011.cluster.edu % 0.16/0.38 % Model : x86_64 x86_64 % 0.16/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.38 % Memory : 8042.1875MB % 0.16/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.38 % CPULimit : 300 % 0.16/0.38 % WCLimit : 300 % 0.16/0.38 % DateTime : Mon May 4 19:27:02 EDT 2026 % 0.16/0.38 % CPUTime : % 0.61/0.64 ________ _____ % 0.61/0.64 ___ __ \_________(_)________________________________ % 0.61/0.64 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.61/0.64 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.61/0.64 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.61/0.64 % 0.61/0.64 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.61/0.64 (2023-06-19) % 0.61/0.64 % 0.61/0.64 (c) Philipp Rümmer, 2009-2023 % 0.61/0.64 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.61/0.64 Amanda Stjerna. % 0.61/0.64 Free software under BSD-3-Clause. % 0.61/0.64 % 0.61/0.64 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.61/0.64 % 0.61/0.64 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.61/0.65 Running up to 7 provers in parallel. % 0.61/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.61/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.61/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.61/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.61/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.61/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.61/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.79/1.52 Prover 1: Preprocessing ... % 5.79/1.55 Prover 4: Preprocessing ... % 5.79/1.57 Prover 2: Preprocessing ... % 5.79/1.57 Prover 3: Preprocessing ... % 5.79/1.57 Prover 5: Preprocessing ... % 5.79/1.57 Prover 6: Preprocessing ... % 5.79/1.57 Prover 0: Preprocessing ... % 13.32/2.59 Prover 1: Warning: ignoring some quantifiers % 14.06/2.60 Prover 3: Warning: ignoring some quantifiers % 14.06/2.63 Prover 3: Constructing countermodel ... % 14.06/2.65 Prover 1: Constructing countermodel ... % 14.06/2.69 Prover 6: Proving ... % 14.79/2.73 Prover 4: Warning: ignoring some quantifiers % 14.79/2.79 Prover 5: Proving ... % 15.51/2.82 Prover 4: Constructing countermodel ... % 16.25/2.96 Prover 3: proved (2302ms) % 16.25/2.96 % 16.25/2.96 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 16.25/2.96 % 16.25/2.98 Prover 6: stopped % 16.25/2.99 Prover 0: Proving ... % 16.25/2.99 Prover 0: stopped % 16.25/3.00 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 16.25/3.00 Prover 5: stopped % 16.25/3.00 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 16.25/3.00 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 16.25/3.00 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 17.92/3.15 Prover 7: Preprocessing ... % 17.92/3.17 Prover 2: Proving ... % 17.92/3.18 Prover 2: stopped % 17.92/3.20 Prover 1: Found proof (size 33) % 17.92/3.20 Prover 1: proved (2528ms) % 17.92/3.20 Prover 4: stopped % 18.50/3.20 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 18.50/3.21 Prover 11: Preprocessing ... % 18.50/3.23 Prover 7: stopped % 18.50/3.23 Prover 10: Preprocessing ... % 18.50/3.27 Prover 8: Preprocessing ... % 18.50/3.29 Prover 11: stopped % 18.50/3.30 Prover 10: stopped % 19.25/3.36 Prover 13: Preprocessing ... % 19.84/3.42 Prover 13: stopped % 19.84/3.45 Prover 8: Warning: ignoring some quantifiers % 19.84/3.47 Prover 8: Constructing countermodel ... % 19.84/3.49 Prover 8: stopped % 19.84/3.49 % 19.84/3.49 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 19.84/3.49 % 19.84/3.49 % SZS output start Proof for theBenchmark % 20.35/3.50 Assumptions after simplification: % 20.35/3.50 --------------------------------- % 20.35/3.50 % 20.35/3.50 (DIFF-noTerm-someTerm) % 20.35/3.52 vOptTerm(vnoTerm) & ! [v0: vTerm] : ( ~ (vsomeTerm(v0) = vnoTerm) | ~ % 20.35/3.52 vTerm(v0)) % 20.35/3.52 % 20.35/3.52 (Progress-Pred-Zero) % 20.35/3.53 vOptTerm(vnoTerm) & vTerm(vt1) & vTerm(vZero) & ? [v0: vTerm] : ? [v1: any] % 20.35/3.53 : ? [v2: vOptTerm] : (vreduce(v0) = v2 & visValue(v0) = v1 & vPred(vt1) = v0 % 20.35/3.53 & vOptTerm(v2) & vTerm(v0) & ? [v3: vTy] : (v2 = vnoTerm & vt1 = vZero & ~ % 20.35/3.53 (v1 = 0) & vptchecksimple(v0, v3) = 0 & vTy(v3))) % 20.35/3.53 % 20.35/3.53 (reduce-23) % 20.35/3.53 vOptTerm(vnoTerm) & vTerm(vFalse) & vTerm(vTrue) & vTerm(vZero) & ? [v0: % 20.35/3.53 vTerm] : ? [v1: vTerm] : (vIszero(vZero) = v1 & vPred(vZero) = v0 & % 20.35/3.53 vTerm(v1) & vTerm(v0) & ! [v2: vTerm] : ! [v3: vOptTerm] : (v3 = vnoTerm | % 20.35/3.53 v2 = v1 | v2 = v0 | ~ (vreduce(v2) = v3) | ~ vTerm(v2) | ? [v4: vTerm] % 20.35/3.53 : ? [v5: vTerm] : ? [v6: vTerm] : (vIfelse(v4, v5, v6) = v2 & vTerm(v6) % 20.35/3.53 & vTerm(v5) & vTerm(v4)) | ? [v4: vTerm] : ? [v5: vTerm] : (vPlus(v4, % 20.35/3.53 v5) = v2 & vTerm(v5) & vTerm(v4)) | ? [v4: vTerm] : ? [v5: vTerm] : % 20.35/3.53 (vIszero(v5) = v2 & vSucc(v4) = v5 & vTerm(v5) & vTerm(v4)) | ? [v4: % 20.35/3.53 vTerm] : ? [v5: vTerm] : (vPred(v5) = v2 & vSucc(v4) = v5 & vTerm(v5) & % 20.35/3.53 vTerm(v4)) | ? [v4: vTerm] : ? [v5: vTerm] : (vIfelse(vFalse, v4, v5) % 20.35/3.53 = v2 & vTerm(v5) & vTerm(v4)) | ? [v4: vTerm] : ? [v5: vTerm] : % 20.35/3.53 (vIfelse(vTrue, v4, v5) = v2 & vTerm(v5) & vTerm(v4)) | ? [v4: vTerm] : % 20.35/3.53 (vIszero(v4) = v2 & vTerm(v4)) | ? [v4: vTerm] : (vPred(v4) = v2 & % 20.35/3.53 vTerm(v4)) | ? [v4: vTerm] : (vSucc(v4) = v2 & vTerm(v4)))) % 20.35/3.53 % 20.35/3.53 (reduce-6) % 20.35/3.53 vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 20.35/3.53 vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 20.35/3.53 % 20.35/3.53 (reduce-INV) % 20.35/3.55 vOptTerm(vnoTerm) & vTerm(vFalse) & vTerm(vTrue) & vTerm(vZero) & ? [v0: % 20.35/3.55 vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 20.35/3.55 vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 20.35/3.55 vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 20.35/3.55 vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & ! [v5: % 20.35/3.55 vTerm] : ! [v6: vOptTerm] : ( ~ (vreduce(v5) = v6) | ~ vTerm(v5) | ? % 20.35/3.55 [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? % 20.35/3.55 [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & vreduce(v8) = v9 & % 20.35/3.55 visSomeTerm(v9) = 0 & visNV(v8) = v10 & visNV(v7) = 0 & vgetTerm(v9) = % 20.35/3.55 v11 & vsomeTerm(v12) = v6 & vPlus(v7, v11) = v12 & vPlus(v7, v8) = v5 & % 20.35/3.55 vOptTerm(v9) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) & % 20.35/3.55 vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? % 20.35/3.55 [v10: int] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & % 20.35/3.55 vreduce(v7) = v9 & visSomeTerm(v9) = 0 & visNV(v7) = v10 & vgetTerm(v9) % 20.35/3.55 = v11 & vsomeTerm(v12) = v6 & vPlus(v11, v8) = v12 & vPlus(v7, v8) = v5 % 20.35/3.55 & vOptTerm(v9) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) & % 20.35/3.55 vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : ? % 20.35/3.55 [v10: vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = 0) & % 20.35/3.55 vreduce(v10) = v8 & visSomeTerm(v8) = 0 & visNV(v7) = v9 & vgetTerm(v8) % 20.35/3.55 = v11 & vsomeTerm(v12) = v6 & vIszero(v11) = v12 & vIszero(v10) = v5 & % 20.35/3.55 vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) % 20.35/3.55 & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: % 20.35/3.55 int] : ? [v10: vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = % 20.35/3.55 0) & vreduce(v10) = v8 & visSomeTerm(v8) = 0 & visNV(v7) = v9 & % 20.35/3.55 vgetTerm(v8) = v11 & vsomeTerm(v12) = v6 & vPred(v11) = v12 & vPred(v10) % 20.35/3.55 = v5 & vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v12) & % 20.35/3.55 vTerm(v11) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : % 20.35/3.55 ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: vTerm] : ? [v12: vTerm] : % 20.35/3.55 ( ~ (v7 = vFalse) & ~ (v7 = vTrue) & vreduce(v7) = v10 & visSomeTerm(v10) % 20.35/3.55 = 0 & vgetTerm(v10) = v11 & vsomeTerm(v12) = v6 & vIfelse(v11, v8, v9) = % 20.35/3.55 v12 & vIfelse(v7, v8, v9) = v5 & vOptTerm(v10) & vOptTerm(v6) & % 20.35/3.55 vTerm(v12) & vTerm(v11) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: % 20.35/3.55 vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? [v11: % 20.35/3.55 int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & vreduce(v8) = v9 & % 20.35/3.55 visSomeTerm(v9) = v11 & visNV(v8) = v10 & visNV(v7) = 0 & vPlus(v7, v8) % 20.35/3.55 = v5 & vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.55 vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? [v11: int] : (v6 = % 20.35/3.55 vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & vreduce(v7) = v9 & % 20.35/3.55 visSomeTerm(v9) = v11 & visNV(v7) = v10 & vPlus(v7, v8) = v5 & % 20.35/3.55 vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.55 vOptTerm] : ? [v9: int] : ? [v10: vTerm] : ? [v11: int] : (v6 = % 20.35/3.55 vnoTerm & ~ (v11 = 0) & ~ (v9 = 0) & vreduce(v10) = v8 & % 20.35/3.55 visSomeTerm(v8) = v11 & visNV(v7) = v9 & vIszero(v10) = v5 & vSucc(v7) = % 20.35/3.55 v10 & vOptTerm(v8) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.55 vOptTerm] : ? [v9: int] : ? [v10: vTerm] : ? [v11: int] : (v6 = % 20.35/3.55 vnoTerm & ~ (v11 = 0) & ~ (v9 = 0) & vreduce(v10) = v8 & % 20.35/3.55 visSomeTerm(v8) = v11 & visNV(v7) = v9 & vPred(v10) = v5 & vSucc(v7) = % 20.35/3.55 v10 & vOptTerm(v8) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.55 vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: int] : (v6 = % 20.35/3.55 vnoTerm & ~ (v11 = 0) & ~ (v7 = vFalse) & ~ (v7 = vTrue) & % 20.35/3.55 vreduce(v7) = v10 & visSomeTerm(v10) = v11 & vIfelse(v7, v8, v9) = v5 & % 20.35/3.55 vOptTerm(v10) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? % 20.35/3.55 [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : ( ~ (v7 = vZero) & % 20.35/3.55 vreduce(v7) = v8 & visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & % 20.35/3.55 vsomeTerm(v10) = v6 & vIszero(v9) = v10 & vIszero(v7) = v5 & % 20.35/3.55 vOptTerm(v8) & vOptTerm(v6) & vTerm(v10) & vTerm(v9) & vTerm(v7) & ! % 20.35/3.55 [v11: vTerm] : ( ~ (vSucc(v11) = v7) | ~ vTerm(v11))) | ? [v7: vTerm] % 20.35/3.55 : ? [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : ( ~ (v7 = vZero) % 20.35/3.55 & vreduce(v7) = v8 & visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & % 20.35/3.55 vsomeTerm(v10) = v6 & vPred(v9) = v10 & vPred(v7) = v5 & vOptTerm(v8) & % 20.35/3.55 vOptTerm(v6) & vTerm(v10) & vTerm(v9) & vTerm(v7) & ! [v11: vTerm] : ( % 20.35/3.55 ~ (vSucc(v11) = v7) | ~ vTerm(v11))) | ? [v7: vTerm] : ? [v8: % 20.35/3.55 vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : (vreduce(v7) = v8 & % 20.35/3.55 visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & % 20.35/3.55 vSucc(v9) = v10 & vSucc(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & % 20.35/3.55 vTerm(v10) & vTerm(v9) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] % 20.35/3.55 : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & ~ (v7 = vZero) & % 20.35/3.55 vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vIszero(v7) = v5 & % 20.35/3.55 vOptTerm(v8) & vTerm(v7) & ! [v10: vTerm] : ( ~ (vSucc(v10) = v7) | ~ % 20.35/3.55 vTerm(v10))) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : (v6 % 20.35/3.55 = vnoTerm & ~ (v9 = 0) & ~ (v7 = vZero) & vreduce(v7) = v8 & % 20.35/3.55 visSomeTerm(v8) = v9 & vPred(v7) = v5 & vOptTerm(v8) & vTerm(v7) & ! % 20.35/3.55 [v10: vTerm] : ( ~ (vSucc(v10) = v7) | ~ vTerm(v10))) | ? [v7: vTerm] % 20.35/3.55 : ? [v8: vOptTerm] : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & % 20.35/3.55 vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vSucc(v7) = v5 & vOptTerm(v8) % 20.35/3.55 & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : % 20.35/3.55 (vplusop(v7, v8) = v9 & visNV(v8) = 0 & visNV(v7) = 0 & vsomeTerm(v9) = v6 % 20.35/3.55 & vPlus(v7, v8) = v5 & vOptTerm(v6) & vTerm(v9) & vTerm(v8) & vTerm(v7)) % 20.35/3.55 | ? [v7: vTerm] : ? [v8: vTerm] : (v6 = v4 & visNV(v7) = 0 & vIszero(v8) % 20.35/3.55 = v5 & vSucc(v7) = v8 & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? % 20.35/3.55 [v8: vTerm] : (visNV(v7) = 0 & vsomeTerm(v7) = v6 & vPred(v8) = v5 & % 20.35/3.55 vSucc(v7) = v8 & vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] % 20.35/3.55 : ? [v8: vTerm] : (vsomeTerm(v8) = v6 & vIfelse(vFalse, v7, v8) = v5 & % 20.35/3.55 vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] % 20.35/3.55 : (vsomeTerm(v7) = v6 & vIfelse(vTrue, v7, v8) = v5 & vOptTerm(v6) & % 20.35/3.55 vTerm(v8) & vTerm(v7)) | (v6 = v3 & v5 = v2) | (v6 = v1 & v5 = v0) | (v6 % 20.35/3.55 = vnoTerm & ~ (v5 = v2) & ~ (v5 = v0) & ! [v7: vTerm] : ! [v8: % 20.35/3.55 vTerm] : ! [v9: vTerm] : ( ~ (vIfelse(v7, v8, v9) = v5) | ~ % 20.35/3.55 vTerm(v9) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : ! [v8: % 20.35/3.55 vTerm] : ( ~ (vPlus(v7, v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! % 20.35/3.55 [v7: vTerm] : ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ vTerm(v7) | ? % 20.35/3.55 [v9: vTerm] : ( ~ (v9 = v5) & vIszero(v8) = v9 & vTerm(v9))) & ! [v7: % 20.35/3.55 vTerm] : ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ vTerm(v7) | ? % 20.35/3.55 [v9: vTerm] : ( ~ (v9 = v5) & vPred(v8) = v9 & vTerm(v9))) & ! [v7: % 20.35/3.55 vTerm] : ! [v8: vTerm] : ( ~ (vIfelse(vFalse, v7, v8) = v5) | ~ % 20.35/3.55 vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : ! [v8: vTerm] : ( ~ % 20.35/3.55 (vIfelse(vTrue, v7, v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: % 20.35/3.55 vTerm] : ( ~ (vIszero(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.35/3.55 (vPred(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ (vSucc(v7) = % 20.35/3.55 v5) | ~ vTerm(v7))))) % 20.35/3.55 % 20.35/3.55 (function-axioms) % 20.35/3.55 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 20.35/3.55 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 20.35/3.55 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 20.35/3.55 vTy] : ! [v3: vTerm] : (v1 = v0 | ~ (vptchecksimple(v3, v2) = v1) | ~ % 20.35/3.55 (vptchecksimple(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: % 20.35/3.55 vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ % 20.35/3.55 (vplusop(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : % 20.35/3.55 ! [v3: vTerm] : (v1 = v0 | ~ (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) % 20.35/3.55 & ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.35/3.55 (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) & ! [v0: MultipleValueBool] : % 20.35/3.55 ! [v1: MultipleValueBool] : ! [v2: vOptTerm] : (v1 = v0 | ~ (visSomeTerm(v2) % 20.35/3.55 = v1) | ~ (visSomeTerm(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.35/3.55 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visValue(v2) = v1) | ~ % 20.35/3.55 (visValue(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.35/3.55 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visNV(v2) = v1) | ~ % 20.35/3.55 (visNV(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 20.35/3.55 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 20.35/3.55 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.35/3.55 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 20.35/3.55 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 20.35/3.55 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.35/3.55 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 20.35/3.55 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 20.35/3.55 % 20.35/3.55 Further assumptions not needed in the proof: % 20.35/3.55 -------------------------------------------- % 20.35/3.55 DIFF-B-Nat, DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, % 20.35/3.55 DIFF-False-Pred, DIFF-False-Succ, DIFF-False-Zero, DIFF-Ifelse-Iszero, % 20.35/3.55 DIFF-Ifelse-Plus, DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, % 20.35/3.55 DIFF-Iszero-Plus, DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, % 20.35/3.55 DIFF-Succ-Plus, DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, % 20.35/3.55 DIFF-True-Iszero, DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, % 20.35/3.55 DIFF-True-Zero, DIFF-Zero-Iszero, DIFF-Zero-Plus, DIFF-Zero-Pred, % 20.35/3.55 DIFF-Zero-Succ, EQ-Ifelse, EQ-Iszero, EQ-Plus, EQ-Pred, EQ-Succ, EQ-someTerm, % 20.35/3.55 Progress-Pred-IH0, TPlus, TPlus_inv0, TPlus_inv1, TPlus_inv2, TPred, TPred_inv1, % 20.35/3.55 TPred_inv2, TSucc, TSucc_inv1, TSucc_inv2, TZero, TZero_inv, Tfalse, Tif, % 20.35/3.55 Tif_inv1, Tif_inv2, Tif_inv3, Tiszero, Tiszero_inv1, Tiszero_inv2, Ttrue, % 20.35/3.55 dom-OptTerm, dom-Term, dom-Ty, getTerm-0, isNV-0, isNV-1, isNV-2, % 20.35/3.55 isNV-false-INV, isNV-true-INV, isSomeTerm-0, isSomeTerm-1, isSomeTerm-false-INV, % 20.35/3.55 isSomeTerm-true-INV, isValue-0, isValue-1, isValue-2, isValue-false-INV, % 20.35/3.55 isValue-true-INV, plusop-0, plusop-1, plusop-2, plusop-INV, reduce-0, reduce-1, % 20.35/3.55 reduce-10, reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, reduce-16, % 20.35/3.55 reduce-17, reduce-18, reduce-19, reduce-2, reduce-20, reduce-21, reduce-22, % 20.35/3.55 reduce-3, reduce-4, reduce-5, reduce-7, reduce-8, reduce-9 % 20.35/3.55 % 20.35/3.55 Those formulas are unsatisfiable: % 20.35/3.55 --------------------------------- % 20.35/3.55 % 20.35/3.55 Begin of proof % 20.35/3.56 | % 20.35/3.56 | ALPHA: (DIFF-noTerm-someTerm) implies: % 20.35/3.56 | (1) ! [v0: vTerm] : ( ~ (vsomeTerm(v0) = vnoTerm) | ~ vTerm(v0)) % 20.35/3.56 | % 20.35/3.56 | ALPHA: (reduce-6) implies: % 20.35/3.56 | (2) ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 20.35/3.56 | vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 20.35/3.56 | % 20.35/3.56 | ALPHA: (reduce-23) implies: % 20.35/3.56 | (3) ? [v0: vTerm] : ? [v1: vTerm] : (vIszero(vZero) = v1 & vPred(vZero) = % 20.35/3.56 | v0 & vTerm(v1) & vTerm(v0) & ! [v2: vTerm] : ! [v3: vOptTerm] : (v3 % 20.35/3.56 | = vnoTerm | v2 = v1 | v2 = v0 | ~ (vreduce(v2) = v3) | ~ % 20.35/3.56 | vTerm(v2) | ? [v4: vTerm] : ? [v5: vTerm] : ? [v6: vTerm] : % 20.35/3.56 | (vIfelse(v4, v5, v6) = v2 & vTerm(v6) & vTerm(v5) & vTerm(v4)) | ? % 20.35/3.56 | [v4: vTerm] : ? [v5: vTerm] : (vPlus(v4, v5) = v2 & vTerm(v5) & % 20.35/3.56 | vTerm(v4)) | ? [v4: vTerm] : ? [v5: vTerm] : (vIszero(v5) = v2 % 20.35/3.56 | & vSucc(v4) = v5 & vTerm(v5) & vTerm(v4)) | ? [v4: vTerm] : ? % 20.35/3.56 | [v5: vTerm] : (vPred(v5) = v2 & vSucc(v4) = v5 & vTerm(v5) & % 20.35/3.56 | vTerm(v4)) | ? [v4: vTerm] : ? [v5: vTerm] : (vIfelse(vFalse, % 20.35/3.56 | v4, v5) = v2 & vTerm(v5) & vTerm(v4)) | ? [v4: vTerm] : ? % 20.35/3.56 | [v5: vTerm] : (vIfelse(vTrue, v4, v5) = v2 & vTerm(v5) & vTerm(v4)) % 20.35/3.56 | | ? [v4: vTerm] : (vIszero(v4) = v2 & vTerm(v4)) | ? [v4: vTerm] % 20.35/3.56 | : (vPred(v4) = v2 & vTerm(v4)) | ? [v4: vTerm] : (vSucc(v4) = v2 & % 20.35/3.56 | vTerm(v4)))) % 20.35/3.56 | % 20.35/3.56 | ALPHA: (reduce-INV) implies: % 20.35/3.57 | (4) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] % 20.35/3.57 | : ? [v4: vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 20.35/3.57 | vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 20.35/3.57 | vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & % 20.35/3.57 | ! [v5: vTerm] : ! [v6: vOptTerm] : ( ~ (vreduce(v5) = v6) | ~ % 20.35/3.57 | vTerm(v5) | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : % 20.35/3.57 | ? [v10: int] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & % 20.35/3.57 | vreduce(v8) = v9 & visSomeTerm(v9) = 0 & visNV(v8) = v10 & % 20.35/3.57 | visNV(v7) = 0 & vgetTerm(v9) = v11 & vsomeTerm(v12) = v6 & % 20.35/3.57 | vPlus(v7, v11) = v12 & vPlus(v7, v8) = v5 & vOptTerm(v9) & % 20.35/3.57 | vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) & vTerm(v7)) | % 20.35/3.57 | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] % 20.35/3.57 | : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & vreduce(v7) = % 20.35/3.57 | v9 & visSomeTerm(v9) = 0 & visNV(v7) = v10 & vgetTerm(v9) = v11 & % 20.35/3.57 | vsomeTerm(v12) = v6 & vPlus(v11, v8) = v12 & vPlus(v7, v8) = v5 & % 20.35/3.57 | vOptTerm(v9) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) % 20.35/3.57 | & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] % 20.35/3.57 | : ? [v10: vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = % 20.35/3.57 | 0) & vreduce(v10) = v8 & visSomeTerm(v8) = 0 & visNV(v7) = v9 & % 20.35/3.57 | vgetTerm(v8) = v11 & vsomeTerm(v12) = v6 & vIszero(v11) = v12 & % 20.35/3.57 | vIszero(v10) = v5 & vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) % 20.35/3.57 | & vTerm(v12) & vTerm(v11) & vTerm(v10) & vTerm(v7)) | ? [v7: % 20.35/3.57 | vTerm] : ? [v8: vOptTerm] : ? [v9: int] : ? [v10: vTerm] : ? % 20.35/3.57 | [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = 0) & vreduce(v10) = v8 & % 20.35/3.57 | visSomeTerm(v8) = 0 & visNV(v7) = v9 & vgetTerm(v8) = v11 & % 20.35/3.57 | vsomeTerm(v12) = v6 & vPred(v11) = v12 & vPred(v10) = v5 & % 20.35/3.57 | vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v12) & % 20.35/3.57 | vTerm(v11) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.57 | vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: vTerm] : % 20.35/3.57 | ? [v12: vTerm] : ( ~ (v7 = vFalse) & ~ (v7 = vTrue) & vreduce(v7) % 20.35/3.57 | = v10 & visSomeTerm(v10) = 0 & vgetTerm(v10) = v11 & % 20.35/3.57 | vsomeTerm(v12) = v6 & vIfelse(v11, v8, v9) = v12 & vIfelse(v7, % 20.35/3.57 | v8, v9) = v5 & vOptTerm(v10) & vOptTerm(v6) & vTerm(v12) & % 20.35/3.57 | vTerm(v11) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] % 20.35/3.57 | : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? [v11: % 20.35/3.57 | int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & vreduce(v8) % 20.35/3.57 | = v9 & visSomeTerm(v9) = v11 & visNV(v8) = v10 & visNV(v7) = 0 & % 20.35/3.57 | vPlus(v7, v8) = v5 & vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? % 20.35/3.57 | [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : % 20.35/3.57 | ? [v11: int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & % 20.35/3.57 | vreduce(v7) = v9 & visSomeTerm(v9) = v11 & visNV(v7) = v10 & % 20.35/3.57 | vPlus(v7, v8) = v5 & vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? % 20.35/3.57 | [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : ? [v10: vTerm] : % 20.35/3.57 | ? [v11: int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v9 = 0) & % 20.35/3.57 | vreduce(v10) = v8 & visSomeTerm(v8) = v11 & visNV(v7) = v9 & % 20.35/3.57 | vIszero(v10) = v5 & vSucc(v7) = v10 & vOptTerm(v8) & vTerm(v10) & % 20.35/3.57 | vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : % 20.35/3.57 | ? [v10: vTerm] : ? [v11: int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ % 20.35/3.57 | (v9 = 0) & vreduce(v10) = v8 & visSomeTerm(v8) = v11 & visNV(v7) % 20.35/3.57 | = v9 & vPred(v10) = v5 & vSucc(v7) = v10 & vOptTerm(v8) & % 20.35/3.57 | vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : ? % 20.35/3.57 | [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: int] : (v6 = vnoTerm & % 20.35/3.57 | ~ (v11 = 0) & ~ (v7 = vFalse) & ~ (v7 = vTrue) & vreduce(v7) = % 20.35/3.57 | v10 & visSomeTerm(v10) = v11 & vIfelse(v7, v8, v9) = v5 & % 20.35/3.57 | vOptTerm(v10) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: % 20.35/3.57 | vTerm] : ? [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : ( % 20.35/3.57 | ~ (v7 = vZero) & vreduce(v7) = v8 & visSomeTerm(v8) = 0 & % 20.35/3.57 | vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & vIszero(v9) = v10 & % 20.35/3.57 | vIszero(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v10) & % 20.35/3.57 | vTerm(v9) & vTerm(v7) & ! [v11: vTerm] : ( ~ (vSucc(v11) = v7) | % 20.35/3.57 | ~ vTerm(v11))) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: % 20.35/3.57 | vTerm] : ? [v10: vTerm] : ( ~ (v7 = vZero) & vreduce(v7) = v8 & % 20.35/3.57 | visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & % 20.35/3.57 | vPred(v9) = v10 & vPred(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & % 20.35/3.57 | vTerm(v10) & vTerm(v9) & vTerm(v7) & ! [v11: vTerm] : ( ~ % 20.35/3.57 | (vSucc(v11) = v7) | ~ vTerm(v11))) | ? [v7: vTerm] : ? [v8: % 20.35/3.57 | vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : (vreduce(v7) = v8 % 20.35/3.57 | & visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & % 20.35/3.57 | vSucc(v9) = v10 & vSucc(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & % 20.35/3.57 | vTerm(v10) & vTerm(v9) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.57 | vOptTerm] : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & ~ (v7 = % 20.35/3.57 | vZero) & vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vIszero(v7) % 20.35/3.57 | = v5 & vOptTerm(v8) & vTerm(v7) & ! [v10: vTerm] : ( ~ % 20.35/3.57 | (vSucc(v10) = v7) | ~ vTerm(v10))) | ? [v7: vTerm] : ? [v8: % 20.35/3.57 | vOptTerm] : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & ~ (v7 = % 20.35/3.57 | vZero) & vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vPred(v7) = % 20.35/3.57 | v5 & vOptTerm(v8) & vTerm(v7) & ! [v10: vTerm] : ( ~ (vSucc(v10) % 20.35/3.57 | = v7) | ~ vTerm(v10))) | ? [v7: vTerm] : ? [v8: vOptTerm] % 20.35/3.57 | : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & vreduce(v7) = v8 & % 20.35/3.57 | visSomeTerm(v8) = v9 & vSucc(v7) = v5 & vOptTerm(v8) & vTerm(v7)) % 20.35/3.57 | | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : (vplusop(v7, % 20.35/3.57 | v8) = v9 & visNV(v8) = 0 & visNV(v7) = 0 & vsomeTerm(v9) = v6 & % 20.35/3.57 | vPlus(v7, v8) = v5 & vOptTerm(v6) & vTerm(v9) & vTerm(v8) & % 20.35/3.57 | vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : (v6 = v4 & % 20.35/3.57 | visNV(v7) = 0 & vIszero(v8) = v5 & vSucc(v7) = v8 & vTerm(v8) & % 20.35/3.57 | vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : (visNV(v7) = 0 & % 20.35/3.57 | vsomeTerm(v7) = v6 & vPred(v8) = v5 & vSucc(v7) = v8 & % 20.35/3.57 | vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.57 | vTerm] : (vsomeTerm(v8) = v6 & vIfelse(vFalse, v7, v8) = v5 & % 20.35/3.57 | vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.35/3.57 | vTerm] : (vsomeTerm(v7) = v6 & vIfelse(vTrue, v7, v8) = v5 & % 20.35/3.57 | vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | (v6 = v3 & v5 = v2) | (v6 % 20.35/3.57 | = v1 & v5 = v0) | (v6 = vnoTerm & ~ (v5 = v2) & ~ (v5 = v0) & % 20.35/3.57 | ! [v7: vTerm] : ! [v8: vTerm] : ! [v9: vTerm] : ( ~ % 20.35/3.57 | (vIfelse(v7, v8, v9) = v5) | ~ vTerm(v9) | ~ vTerm(v8) | ~ % 20.35/3.57 | vTerm(v7)) & ! [v7: vTerm] : ! [v8: vTerm] : ( ~ (vPlus(v7, % 20.35/3.57 | v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : % 20.35/3.57 | ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ vTerm(v7) | ? [v9: % 20.35/3.57 | vTerm] : ( ~ (v9 = v5) & vIszero(v8) = v9 & vTerm(v9))) & ! % 20.35/3.57 | [v7: vTerm] : ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ % 20.35/3.57 | vTerm(v7) | ? [v9: vTerm] : ( ~ (v9 = v5) & vPred(v8) = v9 & % 20.35/3.57 | vTerm(v9))) & ! [v7: vTerm] : ! [v8: vTerm] : ( ~ % 20.35/3.57 | (vIfelse(vFalse, v7, v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & % 20.35/3.57 | ! [v7: vTerm] : ! [v8: vTerm] : ( ~ (vIfelse(vTrue, v7, v8) = % 20.35/3.57 | v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.35/3.57 | (vIszero(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.35/3.57 | (vPred(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.35/3.57 | (vSucc(v7) = v5) | ~ vTerm(v7))))) % 20.35/3.57 | % 20.35/3.57 | ALPHA: (Progress-Pred-Zero) implies: % 20.35/3.58 | (5) vTerm(vt1) % 20.35/3.58 | (6) ? [v0: vTerm] : ? [v1: any] : ? [v2: vOptTerm] : (vreduce(v0) = v2 & % 20.35/3.58 | visValue(v0) = v1 & vPred(vt1) = v0 & vOptTerm(v2) & vTerm(v0) & ? % 20.35/3.58 | [v3: vTy] : (v2 = vnoTerm & vt1 = vZero & ~ (v1 = 0) & % 20.35/3.58 | vptchecksimple(v0, v3) = 0 & vTy(v3))) % 20.35/3.58 | % 20.35/3.58 | ALPHA: (function-axioms) implies: % 20.35/3.58 | (7) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.35/3.58 | (vPred(v2) = v1) | ~ (vPred(v2) = v0)) % 20.35/3.58 | (8) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.35/3.58 | (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) % 20.35/3.58 | (9) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.35/3.58 | (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) % 20.35/3.58 | % 20.35/3.58 | DELTA: instantiating (2) with fresh symbols all_99_0, all_99_1 gives: % 20.35/3.58 | (10) vreduce(all_99_1) = all_99_0 & vsomeTerm(vZero) = all_99_0 & % 20.35/3.58 | vPred(vZero) = all_99_1 & vOptTerm(all_99_0) & vTerm(all_99_1) % 20.35/3.58 | % 20.35/3.58 | ALPHA: (10) implies: % 20.35/3.58 | (11) vPred(vZero) = all_99_1 % 20.35/3.58 | (12) vsomeTerm(vZero) = all_99_0 % 20.35/3.58 | (13) vreduce(all_99_1) = all_99_0 % 20.35/3.58 | % 20.35/3.58 | DELTA: instantiating (6) with fresh symbols all_109_0, all_109_1, all_109_2 % 20.35/3.58 | gives: % 20.35/3.58 | (14) vreduce(all_109_2) = all_109_0 & visValue(all_109_2) = all_109_1 & % 20.35/3.58 | vPred(vt1) = all_109_2 & vOptTerm(all_109_0) & vTerm(all_109_2) & ? % 20.35/3.58 | [v0: vTy] : (all_109_0 = vnoTerm & vt1 = vZero & ~ (all_109_1 = 0) & % 20.35/3.58 | vptchecksimple(all_109_2, v0) = 0 & vTy(v0)) % 20.35/3.58 | % 20.35/3.58 | ALPHA: (14) implies: % 20.35/3.58 | (15) vPred(vt1) = all_109_2 % 20.35/3.58 | (16) vreduce(all_109_2) = all_109_0 % 20.35/3.58 | (17) ? [v0: vTy] : (all_109_0 = vnoTerm & vt1 = vZero & ~ (all_109_1 = 0) % 20.35/3.58 | & vptchecksimple(all_109_2, v0) = 0 & vTy(v0)) % 20.35/3.58 | % 20.35/3.58 | DELTA: instantiating (3) with fresh symbols all_112_0, all_112_1 gives: % 20.35/3.59 | (18) vIszero(vZero) = all_112_0 & vPred(vZero) = all_112_1 & % 20.35/3.59 | vTerm(all_112_0) & vTerm(all_112_1) & ! [v0: any] : ! [v1: vOptTerm] % 20.35/3.59 | : (v1 = vnoTerm | v0 = all_112_0 | v0 = all_112_1 | ~ (vreduce(v0) = % 20.35/3.59 | v1) | ~ vTerm(v0) | ? [v2: vTerm] : ? [v3: vTerm] : ? [v4: % 20.35/3.59 | vTerm] : (vIfelse(v2, v3, v4) = v0 & vTerm(v4) & vTerm(v3) & % 20.35/3.59 | vTerm(v2)) | ? [v2: vTerm] : ? [v3: vTerm] : (vPlus(v2, v3) = v0 % 20.35/3.59 | & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: vTerm] : % 20.35/3.59 | (vIszero(v3) = v0 & vSucc(v2) = v3 & vTerm(v3) & vTerm(v2)) | ? % 20.35/3.59 | [v2: vTerm] : ? [v3: vTerm] : (vPred(v3) = v0 & vSucc(v2) = v3 & % 20.35/3.59 | vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: vTerm] : % 20.35/3.59 | (vIfelse(vFalse, v2, v3) = v0 & vTerm(v3) & vTerm(v2)) | ? [v2: % 20.35/3.59 | vTerm] : ? [v3: vTerm] : (vIfelse(vTrue, v2, v3) = v0 & vTerm(v3) % 20.35/3.59 | & vTerm(v2)) | ? [v2: vTerm] : (vIszero(v2) = v0 & vTerm(v2)) | % 20.35/3.59 | ? [v2: vTerm] : (vPred(v2) = v0 & vTerm(v2)) | ? [v2: vTerm] : % 20.35/3.59 | (vSucc(v2) = v0 & vTerm(v2))) % 20.35/3.59 | % 20.35/3.59 | ALPHA: (18) implies: % 20.35/3.59 | (19) vPred(vZero) = all_112_1 % 20.35/3.59 | % 20.35/3.59 | DELTA: instantiating (17) with fresh symbol all_115_0 gives: % 20.35/3.59 | (20) all_109_0 = vnoTerm & vt1 = vZero & ~ (all_109_1 = 0) & % 20.35/3.59 | vptchecksimple(all_109_2, all_115_0) = 0 & vTy(all_115_0) % 20.35/3.59 | % 20.35/3.59 | ALPHA: (20) implies: % 20.35/3.59 | (21) vt1 = vZero % 20.35/3.59 | (22) all_109_0 = vnoTerm % 20.35/3.59 | % 20.35/3.59 | DELTA: instantiating (4) with fresh symbols all_117_0, all_117_1, all_117_2, % 20.35/3.59 | all_117_3, all_117_4 gives: % 20.35/3.59 | (23) vsomeTerm(vFalse) = all_117_0 & vsomeTerm(vTrue) = all_117_1 & % 20.35/3.60 | vsomeTerm(vZero) = all_117_3 & vIszero(vZero) = all_117_2 & % 20.35/3.60 | vPred(vZero) = all_117_4 & vOptTerm(all_117_0) & vOptTerm(all_117_1) & % 20.35/3.60 | vOptTerm(all_117_3) & vTerm(all_117_2) & vTerm(all_117_4) & ! [v0: % 20.35/3.60 | vTerm] : ! [v1: vOptTerm] : ( ~ (vreduce(v0) = v1) | ~ vTerm(v0) | % 20.35/3.60 | ? [v2: vTerm] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: int] : % 20.35/3.60 | ? [v6: vTerm] : ? [v7: vTerm] : ( ~ (v5 = 0) & vreduce(v3) = v4 & % 20.35/3.60 | visSomeTerm(v4) = 0 & visNV(v3) = v5 & visNV(v2) = 0 & % 20.35/3.60 | vgetTerm(v4) = v6 & vsomeTerm(v7) = v1 & vPlus(v2, v6) = v7 & % 20.35/3.60 | vPlus(v2, v3) = v0 & vOptTerm(v4) & vOptTerm(v1) & vTerm(v7) & % 20.35/3.60 | vTerm(v6) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 20.35/3.60 | vTerm] : ? [v4: vOptTerm] : ? [v5: int] : ? [v6: vTerm] : ? % 20.35/3.60 | [v7: vTerm] : ( ~ (v5 = 0) & vreduce(v2) = v4 & visSomeTerm(v4) = 0 % 20.35/3.60 | & visNV(v2) = v5 & vgetTerm(v4) = v6 & vsomeTerm(v7) = v1 & % 20.35/3.60 | vPlus(v6, v3) = v7 & vPlus(v2, v3) = v0 & vOptTerm(v4) & % 20.35/3.60 | vOptTerm(v1) & vTerm(v7) & vTerm(v6) & vTerm(v3) & vTerm(v2)) | ? % 20.35/3.60 | [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? % 20.35/3.60 | [v6: vTerm] : ? [v7: vTerm] : ( ~ (v4 = 0) & vreduce(v5) = v3 & % 20.35/3.60 | visSomeTerm(v3) = 0 & visNV(v2) = v4 & vgetTerm(v3) = v6 & % 20.35/3.60 | vsomeTerm(v7) = v1 & vIszero(v6) = v7 & vIszero(v5) = v0 & % 20.35/3.60 | vSucc(v2) = v5 & vOptTerm(v3) & vOptTerm(v1) & vTerm(v7) & % 20.35/3.60 | vTerm(v6) & vTerm(v5) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 20.35/3.60 | vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? [v6: vTerm] : ? % 20.35/3.60 | [v7: vTerm] : ( ~ (v4 = 0) & vreduce(v5) = v3 & visSomeTerm(v3) = 0 % 20.35/3.60 | & visNV(v2) = v4 & vgetTerm(v3) = v6 & vsomeTerm(v7) = v1 & % 20.35/3.60 | vPred(v6) = v7 & vPred(v5) = v0 & vSucc(v2) = v5 & vOptTerm(v3) & % 20.35/3.60 | vOptTerm(v1) & vTerm(v7) & vTerm(v6) & vTerm(v5) & vTerm(v2)) | ? % 20.35/3.60 | [v2: vTerm] : ? [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : % 20.35/3.60 | ? [v6: vTerm] : ? [v7: vTerm] : ( ~ (v2 = vFalse) & ~ (v2 = vTrue) % 20.35/3.60 | & vreduce(v2) = v5 & visSomeTerm(v5) = 0 & vgetTerm(v5) = v6 & % 20.35/3.60 | vsomeTerm(v7) = v1 & vIfelse(v6, v3, v4) = v7 & vIfelse(v2, v3, % 20.35/3.60 | v4) = v0 & vOptTerm(v5) & vOptTerm(v1) & vTerm(v7) & vTerm(v6) & % 20.35/3.60 | vTerm(v4) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 20.35/3.60 | vTerm] : ? [v4: vOptTerm] : ? [v5: int] : ? [v6: int] : (v1 = % 20.35/3.60 | vnoTerm & ~ (v6 = 0) & ~ (v5 = 0) & vreduce(v3) = v4 & % 20.35/3.60 | visSomeTerm(v4) = v6 & visNV(v3) = v5 & visNV(v2) = 0 & vPlus(v2, % 20.35/3.60 | v3) = v0 & vOptTerm(v4) & vTerm(v3) & vTerm(v2)) | ? [v2: % 20.35/3.60 | vTerm] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: int] : ? % 20.35/3.60 | [v6: int] : (v1 = vnoTerm & ~ (v6 = 0) & ~ (v5 = 0) & vreduce(v2) % 20.35/3.60 | = v4 & visSomeTerm(v4) = v6 & visNV(v2) = v5 & vPlus(v2, v3) = v0 % 20.35/3.60 | & vOptTerm(v4) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 20.35/3.60 | vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? [v6: int] : (v1 = % 20.35/3.60 | vnoTerm & ~ (v6 = 0) & ~ (v4 = 0) & vreduce(v5) = v3 & % 20.35/3.60 | visSomeTerm(v3) = v6 & visNV(v2) = v4 & vIszero(v5) = v0 & % 20.35/3.60 | vSucc(v2) = v5 & vOptTerm(v3) & vTerm(v5) & vTerm(v2)) | ? [v2: % 20.35/3.60 | vTerm] : ? [v3: vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? % 20.35/3.60 | [v6: int] : (v1 = vnoTerm & ~ (v6 = 0) & ~ (v4 = 0) & vreduce(v5) % 20.35/3.60 | = v3 & visSomeTerm(v3) = v6 & visNV(v2) = v4 & vPred(v5) = v0 & % 20.35/3.60 | vSucc(v2) = v5 & vOptTerm(v3) & vTerm(v5) & vTerm(v2)) | ? [v2: % 20.35/3.60 | vTerm] : ? [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : ? % 20.35/3.60 | [v6: int] : (v1 = vnoTerm & ~ (v6 = 0) & ~ (v2 = vFalse) & ~ (v2 % 20.35/3.60 | = vTrue) & vreduce(v2) = v5 & visSomeTerm(v5) = v6 & vIfelse(v2, % 20.35/3.60 | v3, v4) = v0 & vOptTerm(v5) & vTerm(v4) & vTerm(v3) & vTerm(v2)) % 20.35/3.60 | | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: vTerm] : ? [v5: % 20.35/3.60 | vTerm] : ( ~ (v2 = vZero) & vreduce(v2) = v3 & visSomeTerm(v3) = 0 % 20.35/3.60 | & vgetTerm(v3) = v4 & vsomeTerm(v5) = v1 & vIszero(v4) = v5 & % 20.35/3.60 | vIszero(v2) = v0 & vOptTerm(v3) & vOptTerm(v1) & vTerm(v5) & % 20.35/3.60 | vTerm(v4) & vTerm(v2) & ! [v6: vTerm] : ( ~ (vSucc(v6) = v2) | ~ % 20.35/3.60 | vTerm(v6))) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 20.35/3.60 | vTerm] : ? [v5: vTerm] : ( ~ (v2 = vZero) & vreduce(v2) = v3 & % 20.35/3.60 | visSomeTerm(v3) = 0 & vgetTerm(v3) = v4 & vsomeTerm(v5) = v1 & % 20.35/3.60 | vPred(v4) = v5 & vPred(v2) = v0 & vOptTerm(v3) & vOptTerm(v1) & % 20.35/3.60 | vTerm(v5) & vTerm(v4) & vTerm(v2) & ! [v6: vTerm] : ( ~ % 20.35/3.60 | (vSucc(v6) = v2) | ~ vTerm(v6))) | ? [v2: vTerm] : ? [v3: % 20.35/3.60 | vOptTerm] : ? [v4: vTerm] : ? [v5: vTerm] : (vreduce(v2) = v3 & % 20.35/3.60 | visSomeTerm(v3) = 0 & vgetTerm(v3) = v4 & vsomeTerm(v5) = v1 & % 20.35/3.60 | vSucc(v4) = v5 & vSucc(v2) = v0 & vOptTerm(v3) & vOptTerm(v1) & % 20.35/3.60 | vTerm(v5) & vTerm(v4) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 20.35/3.60 | vOptTerm] : ? [v4: int] : (v1 = vnoTerm & ~ (v4 = 0) & ~ (v2 = % 20.35/3.60 | vZero) & vreduce(v2) = v3 & visSomeTerm(v3) = v4 & vIszero(v2) = % 20.35/3.60 | v0 & vOptTerm(v3) & vTerm(v2) & ! [v5: vTerm] : ( ~ (vSucc(v5) = % 20.35/3.60 | v2) | ~ vTerm(v5))) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? % 20.35/3.60 | [v4: int] : (v1 = vnoTerm & ~ (v4 = 0) & ~ (v2 = vZero) & % 20.35/3.60 | vreduce(v2) = v3 & visSomeTerm(v3) = v4 & vPred(v2) = v0 & % 20.35/3.60 | vOptTerm(v3) & vTerm(v2) & ! [v5: vTerm] : ( ~ (vSucc(v5) = v2) | % 20.35/3.60 | ~ vTerm(v5))) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 20.35/3.60 | int] : (v1 = vnoTerm & ~ (v4 = 0) & vreduce(v2) = v3 & % 20.35/3.60 | visSomeTerm(v3) = v4 & vSucc(v2) = v0 & vOptTerm(v3) & vTerm(v2)) % 20.35/3.60 | | ? [v2: vTerm] : ? [v3: vTerm] : ? [v4: vTerm] : (vplusop(v2, % 20.35/3.60 | v3) = v4 & visNV(v3) = 0 & visNV(v2) = 0 & vsomeTerm(v4) = v1 & % 20.35/3.60 | vPlus(v2, v3) = v0 & vOptTerm(v1) & vTerm(v4) & vTerm(v3) & % 20.35/3.60 | vTerm(v2)) | ? [v2: vTerm] : ? [v3: vTerm] : (v1 = all_117_0 & % 20.35/3.60 | visNV(v2) = 0 & vIszero(v3) = v0 & vSucc(v2) = v3 & vTerm(v3) & % 20.84/3.60 | vTerm(v2)) | ? [v2: vTerm] : ? [v3: vTerm] : (visNV(v2) = 0 & % 20.84/3.60 | vsomeTerm(v2) = v1 & vPred(v3) = v0 & vSucc(v2) = v3 & % 20.84/3.60 | vOptTerm(v1) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 20.84/3.60 | vTerm] : (vsomeTerm(v3) = v1 & vIfelse(vFalse, v2, v3) = v0 & % 20.84/3.60 | vOptTerm(v1) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 20.84/3.60 | vTerm] : (vsomeTerm(v2) = v1 & vIfelse(vTrue, v2, v3) = v0 & % 20.84/3.60 | vOptTerm(v1) & vTerm(v3) & vTerm(v2)) | (v1 = all_117_1 & v0 = % 20.84/3.60 | all_117_2) | (v1 = all_117_3 & v0 = all_117_4) | (v1 = vnoTerm & % 20.84/3.60 | ~ (v0 = all_117_2) & ~ (v0 = all_117_4) & ! [v2: vTerm] : ! % 20.84/3.60 | [v3: vTerm] : ! [v4: vTerm] : ( ~ (vIfelse(v2, v3, v4) = v0) | ~ % 20.84/3.60 | vTerm(v4) | ~ vTerm(v3) | ~ vTerm(v2)) & ! [v2: vTerm] : ! % 20.84/3.60 | [v3: vTerm] : ( ~ (vPlus(v2, v3) = v0) | ~ vTerm(v3) | ~ % 20.84/3.60 | vTerm(v2)) & ! [v2: vTerm] : ! [v3: vTerm] : ( ~ (vSucc(v2) = % 20.84/3.60 | v3) | ~ vTerm(v2) | ? [v4: vTerm] : ( ~ (v4 = v0) & % 20.84/3.60 | vIszero(v3) = v4 & vTerm(v4))) & ! [v2: vTerm] : ! [v3: % 20.84/3.60 | vTerm] : ( ~ (vSucc(v2) = v3) | ~ vTerm(v2) | ? [v4: vTerm] : % 20.84/3.60 | ( ~ (v4 = v0) & vPred(v3) = v4 & vTerm(v4))) & ! [v2: vTerm] : % 20.84/3.60 | ! [v3: vTerm] : ( ~ (vIfelse(vFalse, v2, v3) = v0) | ~ vTerm(v3) % 20.84/3.60 | | ~ vTerm(v2)) & ! [v2: vTerm] : ! [v3: vTerm] : ( ~ % 20.84/3.60 | (vIfelse(vTrue, v2, v3) = v0) | ~ vTerm(v3) | ~ vTerm(v2)) & % 20.84/3.60 | ! [v2: vTerm] : ( ~ (vIszero(v2) = v0) | ~ vTerm(v2)) & ! [v2: % 20.84/3.60 | vTerm] : ( ~ (vPred(v2) = v0) | ~ vTerm(v2)) & ! [v2: vTerm] : % 20.84/3.60 | ( ~ (vSucc(v2) = v0) | ~ vTerm(v2)))) % 20.84/3.60 | % 20.84/3.60 | ALPHA: (23) implies: % 20.84/3.60 | (24) vPred(vZero) = all_117_4 % 20.84/3.60 | (25) vsomeTerm(vZero) = all_117_3 % 20.84/3.60 | % 20.84/3.60 | REDUCE: (16), (22) imply: % 20.84/3.60 | (26) vreduce(all_109_2) = vnoTerm % 20.84/3.60 | % 20.84/3.60 | REDUCE: (15), (21) imply: % 20.84/3.60 | (27) vPred(vZero) = all_109_2 % 20.84/3.60 | % 20.84/3.60 | REDUCE: (5), (21) imply: % 20.84/3.60 | (28) vTerm(vZero) % 20.84/3.60 | % 20.84/3.60 | GROUND_INST: instantiating (7) with all_112_1, all_117_4, vZero, simplifying % 20.84/3.60 | with (19), (24) gives: % 20.84/3.60 | (29) all_117_4 = all_112_1 % 20.84/3.60 | % 20.84/3.60 | GROUND_INST: instantiating (7) with all_109_2, all_117_4, vZero, simplifying % 20.84/3.60 | with (24), (27) gives: % 20.84/3.60 | (30) all_117_4 = all_109_2 % 20.84/3.60 | % 20.84/3.60 | GROUND_INST: instantiating (7) with all_99_1, all_117_4, vZero, simplifying % 20.84/3.60 | with (11), (24) gives: % 20.84/3.60 | (31) all_117_4 = all_99_1 % 20.84/3.60 | % 20.84/3.60 | GROUND_INST: instantiating (8) with all_99_0, all_117_3, vZero, simplifying % 20.84/3.60 | with (12), (25) gives: % 20.84/3.60 | (32) all_117_3 = all_99_0 % 20.84/3.60 | % 20.84/3.60 | COMBINE_EQS: (29), (31) imply: % 20.84/3.60 | (33) all_112_1 = all_99_1 % 20.84/3.60 | % 20.84/3.60 | COMBINE_EQS: (29), (30) imply: % 20.84/3.60 | (34) all_112_1 = all_109_2 % 20.84/3.60 | % 20.84/3.60 | COMBINE_EQS: (33), (34) imply: % 20.84/3.60 | (35) all_109_2 = all_99_1 % 20.84/3.60 | % 20.84/3.60 | SIMP: (35) implies: % 20.84/3.60 | (36) all_109_2 = all_99_1 % 20.84/3.60 | % 20.84/3.60 | REDUCE: (26), (36) imply: % 20.84/3.60 | (37) vreduce(all_99_1) = vnoTerm % 20.84/3.60 | % 20.84/3.60 | GROUND_INST: instantiating (9) with all_99_0, vnoTerm, all_99_1, simplifying % 20.84/3.60 | with (13), (37) gives: % 20.84/3.60 | (38) all_99_0 = vnoTerm % 20.84/3.60 | % 20.84/3.60 | REDUCE: (12), (38) imply: % 20.84/3.60 | (39) vsomeTerm(vZero) = vnoTerm % 20.84/3.60 | % 20.84/3.60 | GROUND_INST: instantiating (1) with vZero, simplifying with (28), (39) gives: % 20.84/3.60 | (40) $false % 20.84/3.60 | % 20.84/3.60 | CLOSE: (40) is inconsistent. % 20.84/3.60 | % 20.84/3.60 End of proof % 20.84/3.60 % SZS output end Proof for theBenchmark % 20.84/3.60 % 20.84/3.60 2963ms %------------------------------------------------------------------------------