%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM244_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 : n023.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 15.20s 2.88s % Output : Proof 21.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : COM244_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.19/0.35 % Computer : n023.cluster.edu % 0.19/0.35 % Model : x86_64 x86_64 % 0.19/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.35 % Memory : 8042.1875MB % 0.19/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.35 % CPULimit : 300 % 0.19/0.35 % WCLimit : 300 % 0.19/0.35 % DateTime : Mon May 4 19:34:08 EDT 2026 % 0.19/0.36 % CPUTime : % 0.67/0.63 ________ _____ % 0.67/0.63 ___ __ \_________(_)________________________________ % 0.67/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.67/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.67/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.67/0.63 % 0.67/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.67/0.63 (2023-06-19) % 0.67/0.63 % 0.67/0.63 (c) Philipp Rümmer, 2009-2023 % 0.67/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.67/0.63 Amanda Stjerna. % 0.67/0.63 Free software under BSD-3-Clause. % 0.67/0.63 % 0.67/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.67/0.63 % 0.67/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.67/0.64 Running up to 7 provers in parallel. % 0.67/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.67/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.67/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.67/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.67/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.67/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.67/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.52/1.52 Prover 1: Preprocessing ... % 5.52/1.55 Prover 4: Preprocessing ... % 5.52/1.57 Prover 5: Preprocessing ... % 5.52/1.57 Prover 3: Preprocessing ... % 5.52/1.57 Prover 6: Preprocessing ... % 5.52/1.57 Prover 2: Preprocessing ... % 5.52/1.57 Prover 0: Preprocessing ... % 13.72/2.61 Prover 3: Warning: ignoring some quantifiers % 13.72/2.61 Prover 1: Warning: ignoring some quantifiers % 13.72/2.62 Prover 6: Proving ... % 13.72/2.63 Prover 3: Constructing countermodel ... % 13.72/2.64 Prover 1: Constructing countermodel ... % 15.20/2.81 Prover 5: Proving ... % 15.20/2.87 Prover 4: Warning: ignoring some quantifiers % 15.20/2.88 Prover 3: proved (2223ms) % 15.20/2.88 % 15.20/2.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.20/2.88 % 15.20/2.88 Prover 6: stopped % 15.20/2.88 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 15.20/2.88 Prover 5: stopped % 16.00/2.90 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.00/2.90 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 16.00/2.92 Prover 4: Constructing countermodel ... % 16.84/3.03 Prover 0: Proving ... % 16.84/3.04 Prover 0: stopped % 16.84/3.06 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 16.84/3.11 Prover 2: Proving ... % 16.84/3.11 Prover 2: stopped % 17.61/3.13 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 17.61/3.15 Prover 7: Preprocessing ... % 17.61/3.16 Prover 8: Preprocessing ... % 17.61/3.18 Prover 10: Preprocessing ... % 18.24/3.29 Prover 11: Preprocessing ... % 18.97/3.32 Prover 1: Found proof (size 31) % 18.97/3.32 Prover 1: proved (2671ms) % 18.97/3.32 Prover 4: stopped % 18.97/3.32 Prover 10: stopped % 18.97/3.33 Prover 13: Preprocessing ... % 18.97/3.37 Prover 11: stopped % 19.69/3.42 Prover 13: stopped % 19.69/3.44 Prover 8: Warning: ignoring some quantifiers % 19.69/3.46 Prover 8: Constructing countermodel ... % 19.69/3.48 Prover 8: stopped % 20.30/3.53 Prover 7: Warning: ignoring some quantifiers % 20.30/3.54 Prover 7: Constructing countermodel ... % 20.30/3.56 Prover 7: stopped % 20.30/3.56 % 20.30/3.57 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.30/3.57 % 20.30/3.57 % SZS output start Proof for theBenchmark % 20.30/3.59 Assumptions after simplification: % 20.30/3.59 --------------------------------- % 20.30/3.59 % 20.30/3.59 (Progress-Zero) % 20.76/3.64 vOptTerm(vnoTerm) & vTerm(vZero) & ? [v0: any] : ? [v1: vOptTerm] : % 20.76/3.64 (vreduce(vZero) = v1 & visValue(vZero) = v0 & vOptTerm(v1) & ? [v2: vTy] : % 20.76/3.64 (v1 = vnoTerm & ~ (v0 = 0) & vptchecksimple(vZero, v2) = 0 & vTy(v2))) % 20.76/3.64 % 20.76/3.64 (isNV-0) % 20.76/3.64 visNV(vZero) = 0 & vTerm(vZero) % 20.76/3.64 % 20.76/3.64 (isValue-false-INV) % 20.76/3.64 vTerm(vFalse) & vTerm(vTrue) & ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ % 20.76/3.64 (visValue(v0) = v1) | ~ vTerm(v0) | ? [v2: int] : ( ~ (v2 = 0) & ~ (v0 = % 20.76/3.64 vFalse) & ~ (v0 = vTrue) & visNV(v0) = v2)) % 20.76/3.64 % 20.76/3.64 (reduce-6) % 20.76/3.64 vTerm(vZero) & ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 20.76/3.64 vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 20.76/3.64 % 20.76/3.64 (reduce-7) % 20.76/3.65 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vsomeTerm(v0) = v1) | ~ vTerm(v0) | % 20.76/3.65 ? [v2: any] : ? [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : % 20.76/3.65 (vreduce(v4) = v5 & visNV(v0) = v2 & vPred(v3) = v4 & vSucc(v0) = v3 & % 20.76/3.65 vOptTerm(v5) & vTerm(v4) & vTerm(v3) & ( ~ (v2 = 0) | v5 = v1))) % 20.76/3.65 % 20.76/3.65 (reduce-INV) % 20.76/3.67 vOptTerm(vnoTerm) & vTerm(vFalse) & vTerm(vTrue) & vTerm(vZero) & ? [v0: % 20.76/3.67 vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 20.76/3.67 vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 20.76/3.67 vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 20.76/3.67 vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & ! [v5: % 20.76/3.67 vTerm] : ! [v6: vOptTerm] : ( ~ (vreduce(v5) = v6) | ~ vTerm(v5) | ? % 20.76/3.67 [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? % 20.76/3.67 [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & vreduce(v8) = v9 & % 20.76/3.67 visSomeTerm(v9) = 0 & visNV(v8) = v10 & visNV(v7) = 0 & vgetTerm(v9) = % 20.76/3.67 v11 & vsomeTerm(v12) = v6 & vPlus(v7, v11) = v12 & vPlus(v7, v8) = v5 & % 20.76/3.67 vOptTerm(v9) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) & % 20.76/3.67 vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? % 20.76/3.67 [v10: int] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & % 20.76/3.67 vreduce(v7) = v9 & visSomeTerm(v9) = 0 & visNV(v7) = v10 & vgetTerm(v9) % 20.76/3.67 = v11 & vsomeTerm(v12) = v6 & vPlus(v11, v8) = v12 & vPlus(v7, v8) = v5 % 20.76/3.67 & vOptTerm(v9) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) & % 20.76/3.67 vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : ? % 20.76/3.67 [v10: vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = 0) & % 20.76/3.67 vreduce(v10) = v8 & visSomeTerm(v8) = 0 & visNV(v7) = v9 & vgetTerm(v8) % 20.76/3.67 = v11 & vsomeTerm(v12) = v6 & vIszero(v11) = v12 & vIszero(v10) = v5 & % 20.76/3.67 vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) % 20.76/3.67 & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: % 20.76/3.67 int] : ? [v10: vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = % 20.76/3.67 0) & vreduce(v10) = v8 & visSomeTerm(v8) = 0 & visNV(v7) = v9 & % 20.76/3.67 vgetTerm(v8) = v11 & vsomeTerm(v12) = v6 & vPred(v11) = v12 & vPred(v10) % 20.76/3.67 = v5 & vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v12) & % 20.76/3.67 vTerm(v11) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : % 20.76/3.67 ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: vTerm] : ? [v12: vTerm] : % 20.76/3.67 ( ~ (v7 = vFalse) & ~ (v7 = vTrue) & vreduce(v7) = v10 & visSomeTerm(v10) % 20.76/3.67 = 0 & vgetTerm(v10) = v11 & vsomeTerm(v12) = v6 & vIfelse(v11, v8, v9) = % 20.76/3.67 v12 & vIfelse(v7, v8, v9) = v5 & vOptTerm(v10) & vOptTerm(v6) & % 20.76/3.67 vTerm(v12) & vTerm(v11) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: % 20.76/3.67 vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? [v11: % 20.76/3.67 int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & vreduce(v8) = v9 & % 20.76/3.67 visSomeTerm(v9) = v11 & visNV(v8) = v10 & visNV(v7) = 0 & vPlus(v7, v8) % 20.76/3.67 = v5 & vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.67 vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? [v11: int] : (v6 = % 20.76/3.67 vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & vreduce(v7) = v9 & % 20.76/3.67 visSomeTerm(v9) = v11 & visNV(v7) = v10 & vPlus(v7, v8) = v5 & % 20.76/3.67 vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.67 vOptTerm] : ? [v9: int] : ? [v10: vTerm] : ? [v11: int] : (v6 = % 20.76/3.67 vnoTerm & ~ (v11 = 0) & ~ (v9 = 0) & vreduce(v10) = v8 & % 20.76/3.67 visSomeTerm(v8) = v11 & visNV(v7) = v9 & vIszero(v10) = v5 & vSucc(v7) = % 20.76/3.67 v10 & vOptTerm(v8) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.67 vOptTerm] : ? [v9: int] : ? [v10: vTerm] : ? [v11: int] : (v6 = % 20.76/3.67 vnoTerm & ~ (v11 = 0) & ~ (v9 = 0) & vreduce(v10) = v8 & % 20.76/3.67 visSomeTerm(v8) = v11 & visNV(v7) = v9 & vPred(v10) = v5 & vSucc(v7) = % 20.76/3.67 v10 & vOptTerm(v8) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.67 vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: int] : (v6 = % 20.76/3.67 vnoTerm & ~ (v11 = 0) & ~ (v7 = vFalse) & ~ (v7 = vTrue) & % 20.76/3.67 vreduce(v7) = v10 & visSomeTerm(v10) = v11 & vIfelse(v7, v8, v9) = v5 & % 20.76/3.67 vOptTerm(v10) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? % 20.76/3.67 [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : ( ~ (v7 = vZero) & % 20.76/3.67 vreduce(v7) = v8 & visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & % 20.76/3.67 vsomeTerm(v10) = v6 & vIszero(v9) = v10 & vIszero(v7) = v5 & % 20.76/3.67 vOptTerm(v8) & vOptTerm(v6) & vTerm(v10) & vTerm(v9) & vTerm(v7) & ! % 20.76/3.67 [v11: vTerm] : ( ~ (vSucc(v11) = v7) | ~ vTerm(v11))) | ? [v7: vTerm] % 20.76/3.67 : ? [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : ( ~ (v7 = vZero) % 20.76/3.67 & vreduce(v7) = v8 & visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & % 20.76/3.67 vsomeTerm(v10) = v6 & vPred(v9) = v10 & vPred(v7) = v5 & vOptTerm(v8) & % 20.76/3.67 vOptTerm(v6) & vTerm(v10) & vTerm(v9) & vTerm(v7) & ! [v11: vTerm] : ( % 20.76/3.67 ~ (vSucc(v11) = v7) | ~ vTerm(v11))) | ? [v7: vTerm] : ? [v8: % 20.76/3.67 vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : (vreduce(v7) = v8 & % 20.76/3.67 visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & % 20.76/3.67 vSucc(v9) = v10 & vSucc(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & % 20.76/3.67 vTerm(v10) & vTerm(v9) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] % 20.76/3.67 : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & ~ (v7 = vZero) & % 20.76/3.67 vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vIszero(v7) = v5 & % 20.76/3.67 vOptTerm(v8) & vTerm(v7) & ! [v10: vTerm] : ( ~ (vSucc(v10) = v7) | ~ % 20.76/3.67 vTerm(v10))) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : (v6 % 20.76/3.67 = vnoTerm & ~ (v9 = 0) & ~ (v7 = vZero) & vreduce(v7) = v8 & % 20.76/3.67 visSomeTerm(v8) = v9 & vPred(v7) = v5 & vOptTerm(v8) & vTerm(v7) & ! % 20.76/3.67 [v10: vTerm] : ( ~ (vSucc(v10) = v7) | ~ vTerm(v10))) | ? [v7: vTerm] % 20.76/3.67 : ? [v8: vOptTerm] : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & % 20.76/3.67 vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vSucc(v7) = v5 & vOptTerm(v8) % 20.76/3.67 & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : % 20.76/3.67 (vplusop(v7, v8) = v9 & visNV(v8) = 0 & visNV(v7) = 0 & vsomeTerm(v9) = v6 % 20.76/3.67 & vPlus(v7, v8) = v5 & vOptTerm(v6) & vTerm(v9) & vTerm(v8) & vTerm(v7)) % 20.76/3.67 | ? [v7: vTerm] : ? [v8: vTerm] : (v6 = v4 & visNV(v7) = 0 & vIszero(v8) % 20.76/3.67 = v5 & vSucc(v7) = v8 & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? % 20.76/3.67 [v8: vTerm] : (visNV(v7) = 0 & vsomeTerm(v7) = v6 & vPred(v8) = v5 & % 20.76/3.67 vSucc(v7) = v8 & vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] % 20.76/3.67 : ? [v8: vTerm] : (vsomeTerm(v8) = v6 & vIfelse(vFalse, v7, v8) = v5 & % 20.76/3.67 vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] % 20.76/3.67 : (vsomeTerm(v7) = v6 & vIfelse(vTrue, v7, v8) = v5 & vOptTerm(v6) & % 20.76/3.67 vTerm(v8) & vTerm(v7)) | (v6 = v3 & v5 = v2) | (v6 = v1 & v5 = v0) | (v6 % 20.76/3.67 = vnoTerm & ~ (v5 = v2) & ~ (v5 = v0) & ! [v7: vTerm] : ! [v8: % 20.76/3.67 vTerm] : ! [v9: vTerm] : ( ~ (vIfelse(v7, v8, v9) = v5) | ~ % 20.76/3.67 vTerm(v9) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : ! [v8: % 20.76/3.67 vTerm] : ( ~ (vPlus(v7, v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! % 20.76/3.67 [v7: vTerm] : ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ vTerm(v7) | ? % 20.76/3.67 [v9: vTerm] : ( ~ (v9 = v5) & vIszero(v8) = v9 & vTerm(v9))) & ! [v7: % 20.76/3.67 vTerm] : ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ vTerm(v7) | ? % 20.76/3.67 [v9: vTerm] : ( ~ (v9 = v5) & vPred(v8) = v9 & vTerm(v9))) & ! [v7: % 20.76/3.67 vTerm] : ! [v8: vTerm] : ( ~ (vIfelse(vFalse, v7, v8) = v5) | ~ % 20.76/3.67 vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : ! [v8: vTerm] : ( ~ % 20.76/3.67 (vIfelse(vTrue, v7, v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: % 20.76/3.67 vTerm] : ( ~ (vIszero(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.76/3.67 (vPred(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ (vSucc(v7) = % 20.76/3.67 v5) | ~ vTerm(v7))))) % 20.76/3.67 % 20.76/3.67 (function-axioms) % 20.76/3.67 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 20.76/3.67 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 20.76/3.67 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 20.76/3.67 vTy] : ! [v3: vTerm] : (v1 = v0 | ~ (vptchecksimple(v3, v2) = v1) | ~ % 20.76/3.67 (vptchecksimple(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: % 20.76/3.67 vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ % 20.76/3.67 (vplusop(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : % 20.76/3.67 ! [v3: vTerm] : (v1 = v0 | ~ (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) % 20.76/3.67 & ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.76/3.67 (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) & ! [v0: MultipleValueBool] : % 20.76/3.67 ! [v1: MultipleValueBool] : ! [v2: vOptTerm] : (v1 = v0 | ~ (visSomeTerm(v2) % 20.76/3.67 = v1) | ~ (visSomeTerm(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.76/3.67 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visValue(v2) = v1) | ~ % 20.76/3.67 (visValue(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 20.76/3.67 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visNV(v2) = v1) | ~ % 20.76/3.67 (visNV(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 20.76/3.67 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 20.76/3.67 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.76/3.67 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 20.76/3.67 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 20.76/3.67 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.76/3.67 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 20.76/3.67 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 20.76/3.67 % 20.76/3.67 Further assumptions not needed in the proof: % 20.76/3.67 -------------------------------------------- % 20.76/3.67 DIFF-B-Nat, DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, % 20.76/3.67 DIFF-False-Pred, DIFF-False-Succ, DIFF-False-Zero, DIFF-Ifelse-Iszero, % 20.76/3.67 DIFF-Ifelse-Plus, DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, % 20.76/3.67 DIFF-Iszero-Plus, DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, % 20.76/3.67 DIFF-Succ-Plus, DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, % 20.76/3.67 DIFF-True-Iszero, DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, % 20.76/3.67 DIFF-True-Zero, DIFF-Zero-Iszero, DIFF-Zero-Plus, DIFF-Zero-Pred, % 20.76/3.67 DIFF-Zero-Succ, DIFF-noTerm-someTerm, EQ-Ifelse, EQ-Iszero, EQ-Plus, EQ-Pred, % 20.76/3.67 EQ-Succ, EQ-someTerm, TPlus, TPlus_inv0, TPlus_inv1, TPlus_inv2, TPred, % 20.76/3.67 TPred_inv1, TPred_inv2, TSucc, TSucc_inv1, TSucc_inv2, TZero, TZero_inv, Tfalse, % 20.76/3.67 Tif, Tif_inv1, Tif_inv2, Tif_inv3, Tiszero, Tiszero_inv1, Tiszero_inv2, Ttrue, % 20.76/3.67 dom-OptTerm, dom-Term, dom-Ty, getTerm-0, isNV-1, isNV-2, isNV-false-INV, % 20.76/3.67 isNV-true-INV, isSomeTerm-0, isSomeTerm-1, isSomeTerm-false-INV, % 20.76/3.67 isSomeTerm-true-INV, isValue-0, isValue-1, isValue-2, isValue-true-INV, % 20.76/3.67 plusop-0, plusop-1, plusop-2, plusop-INV, reduce-0, reduce-1, reduce-10, % 20.76/3.67 reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, reduce-16, reduce-17, % 20.76/3.67 reduce-18, reduce-19, reduce-2, reduce-20, reduce-21, reduce-22, reduce-23, % 20.76/3.67 reduce-3, reduce-4, reduce-5, reduce-8, reduce-9 % 20.76/3.67 % 20.76/3.67 Those formulas are unsatisfiable: % 20.76/3.67 --------------------------------- % 20.76/3.67 % 20.76/3.67 Begin of proof % 20.76/3.68 | % 20.76/3.68 | ALPHA: (isNV-0) implies: % 20.76/3.68 | (1) visNV(vZero) = 0 % 20.76/3.68 | % 20.76/3.68 | ALPHA: (isValue-false-INV) implies: % 20.76/3.68 | (2) ! [v0: vTerm] : ! [v1: int] : (v1 = 0 | ~ (visValue(v0) = v1) | ~ % 20.76/3.68 | vTerm(v0) | ? [v2: int] : ( ~ (v2 = 0) & ~ (v0 = vFalse) & ~ (v0 = % 20.76/3.68 | vTrue) & visNV(v0) = v2)) % 20.76/3.68 | % 20.76/3.68 | ALPHA: (reduce-6) implies: % 20.76/3.68 | (3) ? [v0: vTerm] : ? [v1: vOptTerm] : (vreduce(v0) = v1 & % 20.76/3.68 | vsomeTerm(vZero) = v1 & vPred(vZero) = v0 & vOptTerm(v1) & vTerm(v0)) % 20.76/3.68 | % 20.76/3.68 | ALPHA: (reduce-INV) implies: % 20.76/3.69 | (4) ? [v0: vTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] % 20.76/3.69 | : ? [v4: vOptTerm] : (vsomeTerm(vFalse) = v4 & vsomeTerm(vTrue) = v3 & % 20.76/3.69 | vsomeTerm(vZero) = v1 & vIszero(vZero) = v2 & vPred(vZero) = v0 & % 20.76/3.69 | vOptTerm(v4) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v2) & vTerm(v0) & % 20.76/3.69 | ! [v5: vTerm] : ! [v6: vOptTerm] : ( ~ (vreduce(v5) = v6) | ~ % 20.76/3.69 | vTerm(v5) | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : % 20.76/3.69 | ? [v10: int] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & % 20.76/3.69 | vreduce(v8) = v9 & visSomeTerm(v9) = 0 & visNV(v8) = v10 & % 20.76/3.69 | visNV(v7) = 0 & vgetTerm(v9) = v11 & vsomeTerm(v12) = v6 & % 20.76/3.69 | vPlus(v7, v11) = v12 & vPlus(v7, v8) = v5 & vOptTerm(v9) & % 20.76/3.69 | vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) & vTerm(v7)) | % 20.76/3.69 | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] % 20.76/3.69 | : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v10 = 0) & vreduce(v7) = % 20.76/3.69 | v9 & visSomeTerm(v9) = 0 & visNV(v7) = v10 & vgetTerm(v9) = v11 & % 20.76/3.69 | vsomeTerm(v12) = v6 & vPlus(v11, v8) = v12 & vPlus(v7, v8) = v5 & % 20.76/3.69 | vOptTerm(v9) & vOptTerm(v6) & vTerm(v12) & vTerm(v11) & vTerm(v8) % 20.76/3.69 | & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] % 20.76/3.69 | : ? [v10: vTerm] : ? [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = % 20.76/3.69 | 0) & vreduce(v10) = v8 & visSomeTerm(v8) = 0 & visNV(v7) = v9 & % 20.76/3.69 | vgetTerm(v8) = v11 & vsomeTerm(v12) = v6 & vIszero(v11) = v12 & % 20.76/3.69 | vIszero(v10) = v5 & vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) % 20.76/3.69 | & vTerm(v12) & vTerm(v11) & vTerm(v10) & vTerm(v7)) | ? [v7: % 20.76/3.69 | vTerm] : ? [v8: vOptTerm] : ? [v9: int] : ? [v10: vTerm] : ? % 20.76/3.69 | [v11: vTerm] : ? [v12: vTerm] : ( ~ (v9 = 0) & vreduce(v10) = v8 & % 20.76/3.69 | visSomeTerm(v8) = 0 & visNV(v7) = v9 & vgetTerm(v8) = v11 & % 20.76/3.69 | vsomeTerm(v12) = v6 & vPred(v11) = v12 & vPred(v10) = v5 & % 20.76/3.69 | vSucc(v7) = v10 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v12) & % 20.76/3.69 | vTerm(v11) & vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.69 | vTerm] : ? [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: vTerm] : % 20.76/3.69 | ? [v12: vTerm] : ( ~ (v7 = vFalse) & ~ (v7 = vTrue) & vreduce(v7) % 20.76/3.69 | = v10 & visSomeTerm(v10) = 0 & vgetTerm(v10) = v11 & % 20.76/3.69 | vsomeTerm(v12) = v6 & vIfelse(v11, v8, v9) = v12 & vIfelse(v7, % 20.76/3.69 | v8, v9) = v5 & vOptTerm(v10) & vOptTerm(v6) & vTerm(v12) & % 20.76/3.69 | vTerm(v11) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] % 20.76/3.69 | : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : ? [v11: % 20.76/3.69 | int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & vreduce(v8) % 20.76/3.69 | = v9 & visSomeTerm(v9) = v11 & visNV(v8) = v10 & visNV(v7) = 0 & % 20.76/3.69 | vPlus(v7, v8) = v5 & vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? % 20.76/3.69 | [v7: vTerm] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: int] : % 20.76/3.69 | ? [v11: int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v10 = 0) & % 20.76/3.69 | vreduce(v7) = v9 & visSomeTerm(v9) = v11 & visNV(v7) = v10 & % 20.76/3.69 | vPlus(v7, v8) = v5 & vOptTerm(v9) & vTerm(v8) & vTerm(v7)) | ? % 20.76/3.69 | [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : ? [v10: vTerm] : % 20.76/3.69 | ? [v11: int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ (v9 = 0) & % 20.76/3.69 | vreduce(v10) = v8 & visSomeTerm(v8) = v11 & visNV(v7) = v9 & % 20.76/3.69 | vIszero(v10) = v5 & vSucc(v7) = v10 & vOptTerm(v8) & vTerm(v10) & % 20.76/3.69 | vTerm(v7)) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: int] : % 20.76/3.69 | ? [v10: vTerm] : ? [v11: int] : (v6 = vnoTerm & ~ (v11 = 0) & ~ % 20.76/3.69 | (v9 = 0) & vreduce(v10) = v8 & visSomeTerm(v8) = v11 & visNV(v7) % 20.76/3.69 | = v9 & vPred(v10) = v5 & vSucc(v7) = v10 & vOptTerm(v8) & % 20.76/3.69 | vTerm(v10) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : ? % 20.76/3.69 | [v9: vTerm] : ? [v10: vOptTerm] : ? [v11: int] : (v6 = vnoTerm & % 20.76/3.69 | ~ (v11 = 0) & ~ (v7 = vFalse) & ~ (v7 = vTrue) & vreduce(v7) = % 20.76/3.69 | v10 & visSomeTerm(v10) = v11 & vIfelse(v7, v8, v9) = v5 & % 20.76/3.69 | vOptTerm(v10) & vTerm(v9) & vTerm(v8) & vTerm(v7)) | ? [v7: % 20.76/3.69 | vTerm] : ? [v8: vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : ( % 20.76/3.69 | ~ (v7 = vZero) & vreduce(v7) = v8 & visSomeTerm(v8) = 0 & % 20.76/3.69 | vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & vIszero(v9) = v10 & % 20.76/3.69 | vIszero(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & vTerm(v10) & % 20.76/3.69 | vTerm(v9) & vTerm(v7) & ! [v11: vTerm] : ( ~ (vSucc(v11) = v7) | % 20.76/3.69 | ~ vTerm(v11))) | ? [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: % 20.76/3.69 | vTerm] : ? [v10: vTerm] : ( ~ (v7 = vZero) & vreduce(v7) = v8 & % 20.76/3.69 | visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & % 20.76/3.69 | vPred(v9) = v10 & vPred(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & % 20.76/3.69 | vTerm(v10) & vTerm(v9) & vTerm(v7) & ! [v11: vTerm] : ( ~ % 20.76/3.69 | (vSucc(v11) = v7) | ~ vTerm(v11))) | ? [v7: vTerm] : ? [v8: % 20.76/3.69 | vOptTerm] : ? [v9: vTerm] : ? [v10: vTerm] : (vreduce(v7) = v8 % 20.76/3.69 | & visSomeTerm(v8) = 0 & vgetTerm(v8) = v9 & vsomeTerm(v10) = v6 & % 20.76/3.69 | vSucc(v9) = v10 & vSucc(v7) = v5 & vOptTerm(v8) & vOptTerm(v6) & % 20.76/3.69 | vTerm(v10) & vTerm(v9) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.69 | vOptTerm] : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & ~ (v7 = % 20.76/3.69 | vZero) & vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vIszero(v7) % 20.76/3.69 | = v5 & vOptTerm(v8) & vTerm(v7) & ! [v10: vTerm] : ( ~ % 20.76/3.69 | (vSucc(v10) = v7) | ~ vTerm(v10))) | ? [v7: vTerm] : ? [v8: % 20.76/3.69 | vOptTerm] : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & ~ (v7 = % 20.76/3.69 | vZero) & vreduce(v7) = v8 & visSomeTerm(v8) = v9 & vPred(v7) = % 20.76/3.69 | v5 & vOptTerm(v8) & vTerm(v7) & ! [v10: vTerm] : ( ~ (vSucc(v10) % 20.76/3.69 | = v7) | ~ vTerm(v10))) | ? [v7: vTerm] : ? [v8: vOptTerm] % 20.76/3.69 | : ? [v9: int] : (v6 = vnoTerm & ~ (v9 = 0) & vreduce(v7) = v8 & % 20.76/3.69 | visSomeTerm(v8) = v9 & vSucc(v7) = v5 & vOptTerm(v8) & vTerm(v7)) % 20.76/3.69 | | ? [v7: vTerm] : ? [v8: vTerm] : ? [v9: vTerm] : (vplusop(v7, % 20.76/3.69 | v8) = v9 & visNV(v8) = 0 & visNV(v7) = 0 & vsomeTerm(v9) = v6 & % 20.76/3.69 | vPlus(v7, v8) = v5 & vOptTerm(v6) & vTerm(v9) & vTerm(v8) & % 20.76/3.69 | vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : (v6 = v4 & % 20.76/3.69 | visNV(v7) = 0 & vIszero(v8) = v5 & vSucc(v7) = v8 & vTerm(v8) & % 20.76/3.69 | vTerm(v7)) | ? [v7: vTerm] : ? [v8: vTerm] : (visNV(v7) = 0 & % 20.76/3.69 | vsomeTerm(v7) = v6 & vPred(v8) = v5 & vSucc(v7) = v8 & % 20.76/3.69 | vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.69 | vTerm] : (vsomeTerm(v8) = v6 & vIfelse(vFalse, v7, v8) = v5 & % 20.76/3.69 | vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | ? [v7: vTerm] : ? [v8: % 20.76/3.69 | vTerm] : (vsomeTerm(v7) = v6 & vIfelse(vTrue, v7, v8) = v5 & % 20.76/3.69 | vOptTerm(v6) & vTerm(v8) & vTerm(v7)) | (v6 = v3 & v5 = v2) | (v6 % 20.76/3.69 | = v1 & v5 = v0) | (v6 = vnoTerm & ~ (v5 = v2) & ~ (v5 = v0) & % 20.76/3.69 | ! [v7: vTerm] : ! [v8: vTerm] : ! [v9: vTerm] : ( ~ % 20.76/3.69 | (vIfelse(v7, v8, v9) = v5) | ~ vTerm(v9) | ~ vTerm(v8) | ~ % 20.76/3.69 | vTerm(v7)) & ! [v7: vTerm] : ! [v8: vTerm] : ( ~ (vPlus(v7, % 20.76/3.69 | v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : % 20.76/3.69 | ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ vTerm(v7) | ? [v9: % 20.76/3.69 | vTerm] : ( ~ (v9 = v5) & vIszero(v8) = v9 & vTerm(v9))) & ! % 20.76/3.69 | [v7: vTerm] : ! [v8: vTerm] : ( ~ (vSucc(v7) = v8) | ~ % 20.76/3.69 | vTerm(v7) | ? [v9: vTerm] : ( ~ (v9 = v5) & vPred(v8) = v9 & % 20.76/3.69 | vTerm(v9))) & ! [v7: vTerm] : ! [v8: vTerm] : ( ~ % 20.76/3.69 | (vIfelse(vFalse, v7, v8) = v5) | ~ vTerm(v8) | ~ vTerm(v7)) & % 20.76/3.69 | ! [v7: vTerm] : ! [v8: vTerm] : ( ~ (vIfelse(vTrue, v7, v8) = % 20.76/3.69 | v5) | ~ vTerm(v8) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.76/3.69 | (vIszero(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.76/3.69 | (vPred(v7) = v5) | ~ vTerm(v7)) & ! [v7: vTerm] : ( ~ % 20.76/3.69 | (vSucc(v7) = v5) | ~ vTerm(v7))))) % 20.76/3.69 | % 20.76/3.69 | ALPHA: (Progress-Zero) implies: % 20.76/3.70 | (5) vTerm(vZero) % 20.76/3.70 | (6) ? [v0: any] : ? [v1: vOptTerm] : (vreduce(vZero) = v1 & % 20.76/3.70 | visValue(vZero) = v0 & vOptTerm(v1) & ? [v2: vTy] : (v1 = vnoTerm & % 20.76/3.70 | ~ (v0 = 0) & vptchecksimple(vZero, v2) = 0 & vTy(v2))) % 20.76/3.70 | % 20.76/3.70 | ALPHA: (function-axioms) implies: % 20.76/3.70 | (7) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 20.76/3.70 | (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) % 21.23/3.70 | (8) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 21.23/3.70 | vTerm] : (v1 = v0 | ~ (visNV(v2) = v1) | ~ (visNV(v2) = v0)) % 21.23/3.70 | % 21.23/3.70 | DELTA: instantiating (3) with fresh symbols all_101_0, all_101_1 gives: % 21.23/3.70 | (9) vreduce(all_101_1) = all_101_0 & vsomeTerm(vZero) = all_101_0 & % 21.23/3.70 | vPred(vZero) = all_101_1 & vOptTerm(all_101_0) & vTerm(all_101_1) % 21.23/3.70 | % 21.23/3.70 | ALPHA: (9) implies: % 21.23/3.70 | (10) vsomeTerm(vZero) = all_101_0 % 21.23/3.70 | % 21.23/3.70 | DELTA: instantiating (6) with fresh symbols all_103_0, all_103_1 gives: % 21.23/3.70 | (11) vreduce(vZero) = all_103_0 & visValue(vZero) = all_103_1 & % 21.23/3.70 | vOptTerm(all_103_0) & ? [v0: vTy] : (all_103_0 = vnoTerm & ~ % 21.23/3.70 | (all_103_1 = 0) & vptchecksimple(vZero, v0) = 0 & vTy(v0)) % 21.23/3.70 | % 21.23/3.70 | ALPHA: (11) implies: % 21.23/3.70 | (12) visValue(vZero) = all_103_1 % 21.23/3.70 | (13) ? [v0: vTy] : (all_103_0 = vnoTerm & ~ (all_103_1 = 0) & % 21.23/3.70 | vptchecksimple(vZero, v0) = 0 & vTy(v0)) % 21.23/3.70 | % 21.23/3.70 | DELTA: instantiating (13) with fresh symbol all_112_0 gives: % 21.23/3.70 | (14) all_103_0 = vnoTerm & ~ (all_103_1 = 0) & vptchecksimple(vZero, % 21.23/3.70 | all_112_0) = 0 & vTy(all_112_0) % 21.23/3.70 | % 21.23/3.70 | ALPHA: (14) implies: % 21.23/3.70 | (15) ~ (all_103_1 = 0) % 21.23/3.70 | % 21.23/3.70 | DELTA: instantiating (4) with fresh symbols all_114_0, all_114_1, all_114_2, % 21.23/3.70 | all_114_3, all_114_4 gives: % 21.23/3.71 | (16) vsomeTerm(vFalse) = all_114_0 & vsomeTerm(vTrue) = all_114_1 & % 21.23/3.71 | vsomeTerm(vZero) = all_114_3 & vIszero(vZero) = all_114_2 & % 21.23/3.71 | vPred(vZero) = all_114_4 & vOptTerm(all_114_0) & vOptTerm(all_114_1) & % 21.23/3.71 | vOptTerm(all_114_3) & vTerm(all_114_2) & vTerm(all_114_4) & ! [v0: % 21.23/3.71 | vTerm] : ! [v1: vOptTerm] : ( ~ (vreduce(v0) = v1) | ~ vTerm(v0) | % 21.23/3.71 | ? [v2: vTerm] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: int] : % 21.23/3.71 | ? [v6: vTerm] : ? [v7: vTerm] : ( ~ (v5 = 0) & vreduce(v3) = v4 & % 21.23/3.71 | visSomeTerm(v4) = 0 & visNV(v3) = v5 & visNV(v2) = 0 & % 21.23/3.71 | vgetTerm(v4) = v6 & vsomeTerm(v7) = v1 & vPlus(v2, v6) = v7 & % 21.23/3.71 | vPlus(v2, v3) = v0 & vOptTerm(v4) & vOptTerm(v1) & vTerm(v7) & % 21.23/3.71 | vTerm(v6) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vTerm] : ? [v4: vOptTerm] : ? [v5: int] : ? [v6: vTerm] : ? % 21.23/3.71 | [v7: vTerm] : ( ~ (v5 = 0) & vreduce(v2) = v4 & visSomeTerm(v4) = 0 % 21.23/3.71 | & visNV(v2) = v5 & vgetTerm(v4) = v6 & vsomeTerm(v7) = v1 & % 21.23/3.71 | vPlus(v6, v3) = v7 & vPlus(v2, v3) = v0 & vOptTerm(v4) & % 21.23/3.71 | vOptTerm(v1) & vTerm(v7) & vTerm(v6) & vTerm(v3) & vTerm(v2)) | ? % 21.23/3.71 | [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? % 21.23/3.71 | [v6: vTerm] : ? [v7: vTerm] : ( ~ (v4 = 0) & vreduce(v5) = v3 & % 21.23/3.71 | visSomeTerm(v3) = 0 & visNV(v2) = v4 & vgetTerm(v3) = v6 & % 21.23/3.71 | vsomeTerm(v7) = v1 & vIszero(v6) = v7 & vIszero(v5) = v0 & % 21.23/3.71 | vSucc(v2) = v5 & vOptTerm(v3) & vOptTerm(v1) & vTerm(v7) & % 21.23/3.71 | vTerm(v6) & vTerm(v5) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? [v6: vTerm] : ? % 21.23/3.71 | [v7: vTerm] : ( ~ (v4 = 0) & vreduce(v5) = v3 & visSomeTerm(v3) = 0 % 21.23/3.71 | & visNV(v2) = v4 & vgetTerm(v3) = v6 & vsomeTerm(v7) = v1 & % 21.23/3.71 | vPred(v6) = v7 & vPred(v5) = v0 & vSucc(v2) = v5 & vOptTerm(v3) & % 21.23/3.71 | vOptTerm(v1) & vTerm(v7) & vTerm(v6) & vTerm(v5) & vTerm(v2)) | ? % 21.23/3.71 | [v2: vTerm] : ? [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : % 21.23/3.71 | ? [v6: vTerm] : ? [v7: vTerm] : ( ~ (v2 = vFalse) & ~ (v2 = vTrue) % 21.23/3.71 | & vreduce(v2) = v5 & visSomeTerm(v5) = 0 & vgetTerm(v5) = v6 & % 21.23/3.71 | vsomeTerm(v7) = v1 & vIfelse(v6, v3, v4) = v7 & vIfelse(v2, v3, % 21.23/3.71 | v4) = v0 & vOptTerm(v5) & vOptTerm(v1) & vTerm(v7) & vTerm(v6) & % 21.23/3.71 | vTerm(v4) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vTerm] : ? [v4: vOptTerm] : ? [v5: int] : ? [v6: int] : (v1 = % 21.23/3.71 | vnoTerm & ~ (v6 = 0) & ~ (v5 = 0) & vreduce(v3) = v4 & % 21.23/3.71 | visSomeTerm(v4) = v6 & visNV(v3) = v5 & visNV(v2) = 0 & vPlus(v2, % 21.23/3.71 | v3) = v0 & vOptTerm(v4) & vTerm(v3) & vTerm(v2)) | ? [v2: % 21.23/3.71 | vTerm] : ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: int] : ? % 21.23/3.71 | [v6: int] : (v1 = vnoTerm & ~ (v6 = 0) & ~ (v5 = 0) & vreduce(v2) % 21.23/3.71 | = v4 & visSomeTerm(v4) = v6 & visNV(v2) = v5 & vPlus(v2, v3) = v0 % 21.23/3.71 | & vOptTerm(v4) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? [v6: int] : (v1 = % 21.23/3.71 | vnoTerm & ~ (v6 = 0) & ~ (v4 = 0) & vreduce(v5) = v3 & % 21.23/3.71 | visSomeTerm(v3) = v6 & visNV(v2) = v4 & vIszero(v5) = v0 & % 21.23/3.71 | vSucc(v2) = v5 & vOptTerm(v3) & vTerm(v5) & vTerm(v2)) | ? [v2: % 21.23/3.71 | vTerm] : ? [v3: vOptTerm] : ? [v4: int] : ? [v5: vTerm] : ? % 21.23/3.71 | [v6: int] : (v1 = vnoTerm & ~ (v6 = 0) & ~ (v4 = 0) & vreduce(v5) % 21.23/3.71 | = v3 & visSomeTerm(v3) = v6 & visNV(v2) = v4 & vPred(v5) = v0 & % 21.23/3.71 | vSucc(v2) = v5 & vOptTerm(v3) & vTerm(v5) & vTerm(v2)) | ? [v2: % 21.23/3.71 | vTerm] : ? [v3: vTerm] : ? [v4: vTerm] : ? [v5: vOptTerm] : ? % 21.23/3.71 | [v6: int] : (v1 = vnoTerm & ~ (v6 = 0) & ~ (v2 = vFalse) & ~ (v2 % 21.23/3.71 | = vTrue) & vreduce(v2) = v5 & visSomeTerm(v5) = v6 & vIfelse(v2, % 21.23/3.71 | v3, v4) = v0 & vOptTerm(v5) & vTerm(v4) & vTerm(v3) & vTerm(v2)) % 21.23/3.71 | | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: vTerm] : ? [v5: % 21.23/3.71 | vTerm] : ( ~ (v2 = vZero) & vreduce(v2) = v3 & visSomeTerm(v3) = 0 % 21.23/3.71 | & vgetTerm(v3) = v4 & vsomeTerm(v5) = v1 & vIszero(v4) = v5 & % 21.23/3.71 | vIszero(v2) = v0 & vOptTerm(v3) & vOptTerm(v1) & vTerm(v5) & % 21.23/3.71 | vTerm(v4) & vTerm(v2) & ! [v6: vTerm] : ( ~ (vSucc(v6) = v2) | ~ % 21.23/3.71 | vTerm(v6))) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 21.23/3.71 | vTerm] : ? [v5: vTerm] : ( ~ (v2 = vZero) & vreduce(v2) = v3 & % 21.23/3.71 | visSomeTerm(v3) = 0 & vgetTerm(v3) = v4 & vsomeTerm(v5) = v1 & % 21.23/3.71 | vPred(v4) = v5 & vPred(v2) = v0 & vOptTerm(v3) & vOptTerm(v1) & % 21.23/3.71 | vTerm(v5) & vTerm(v4) & vTerm(v2) & ! [v6: vTerm] : ( ~ % 21.23/3.71 | (vSucc(v6) = v2) | ~ vTerm(v6))) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vOptTerm] : ? [v4: vTerm] : ? [v5: vTerm] : (vreduce(v2) = v3 & % 21.23/3.71 | visSomeTerm(v3) = 0 & vgetTerm(v3) = v4 & vsomeTerm(v5) = v1 & % 21.23/3.71 | vSucc(v4) = v5 & vSucc(v2) = v0 & vOptTerm(v3) & vOptTerm(v1) & % 21.23/3.71 | vTerm(v5) & vTerm(v4) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vOptTerm] : ? [v4: int] : (v1 = vnoTerm & ~ (v4 = 0) & ~ (v2 = % 21.23/3.71 | vZero) & vreduce(v2) = v3 & visSomeTerm(v3) = v4 & vIszero(v2) = % 21.23/3.71 | v0 & vOptTerm(v3) & vTerm(v2) & ! [v5: vTerm] : ( ~ (vSucc(v5) = % 21.23/3.71 | v2) | ~ vTerm(v5))) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? % 21.23/3.71 | [v4: int] : (v1 = vnoTerm & ~ (v4 = 0) & ~ (v2 = vZero) & % 21.23/3.71 | vreduce(v2) = v3 & visSomeTerm(v3) = v4 & vPred(v2) = v0 & % 21.23/3.71 | vOptTerm(v3) & vTerm(v2) & ! [v5: vTerm] : ( ~ (vSucc(v5) = v2) | % 21.23/3.71 | ~ vTerm(v5))) | ? [v2: vTerm] : ? [v3: vOptTerm] : ? [v4: % 21.23/3.71 | int] : (v1 = vnoTerm & ~ (v4 = 0) & vreduce(v2) = v3 & % 21.23/3.71 | visSomeTerm(v3) = v4 & vSucc(v2) = v0 & vOptTerm(v3) & vTerm(v2)) % 21.23/3.71 | | ? [v2: vTerm] : ? [v3: vTerm] : ? [v4: vTerm] : (vplusop(v2, % 21.23/3.71 | v3) = v4 & visNV(v3) = 0 & visNV(v2) = 0 & vsomeTerm(v4) = v1 & % 21.23/3.71 | vPlus(v2, v3) = v0 & vOptTerm(v1) & vTerm(v4) & vTerm(v3) & % 21.23/3.71 | vTerm(v2)) | ? [v2: vTerm] : ? [v3: vTerm] : (v1 = all_114_0 & % 21.23/3.71 | visNV(v2) = 0 & vIszero(v3) = v0 & vSucc(v2) = v3 & vTerm(v3) & % 21.23/3.71 | vTerm(v2)) | ? [v2: vTerm] : ? [v3: vTerm] : (visNV(v2) = 0 & % 21.23/3.71 | vsomeTerm(v2) = v1 & vPred(v3) = v0 & vSucc(v2) = v3 & % 21.23/3.71 | vOptTerm(v1) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vTerm] : (vsomeTerm(v3) = v1 & vIfelse(vFalse, v2, v3) = v0 & % 21.23/3.71 | vOptTerm(v1) & vTerm(v3) & vTerm(v2)) | ? [v2: vTerm] : ? [v3: % 21.23/3.71 | vTerm] : (vsomeTerm(v2) = v1 & vIfelse(vTrue, v2, v3) = v0 & % 21.23/3.71 | vOptTerm(v1) & vTerm(v3) & vTerm(v2)) | (v1 = all_114_1 & v0 = % 21.23/3.71 | all_114_2) | (v1 = all_114_3 & v0 = all_114_4) | (v1 = vnoTerm & % 21.23/3.71 | ~ (v0 = all_114_2) & ~ (v0 = all_114_4) & ! [v2: vTerm] : ! % 21.23/3.71 | [v3: vTerm] : ! [v4: vTerm] : ( ~ (vIfelse(v2, v3, v4) = v0) | ~ % 21.23/3.71 | vTerm(v4) | ~ vTerm(v3) | ~ vTerm(v2)) & ! [v2: vTerm] : ! % 21.23/3.71 | [v3: vTerm] : ( ~ (vPlus(v2, v3) = v0) | ~ vTerm(v3) | ~ % 21.23/3.71 | vTerm(v2)) & ! [v2: vTerm] : ! [v3: vTerm] : ( ~ (vSucc(v2) = % 21.23/3.71 | v3) | ~ vTerm(v2) | ? [v4: vTerm] : ( ~ (v4 = v0) & % 21.23/3.71 | vIszero(v3) = v4 & vTerm(v4))) & ! [v2: vTerm] : ! [v3: % 21.23/3.71 | vTerm] : ( ~ (vSucc(v2) = v3) | ~ vTerm(v2) | ? [v4: vTerm] : % 21.23/3.71 | ( ~ (v4 = v0) & vPred(v3) = v4 & vTerm(v4))) & ! [v2: vTerm] : % 21.23/3.71 | ! [v3: vTerm] : ( ~ (vIfelse(vFalse, v2, v3) = v0) | ~ vTerm(v3) % 21.23/3.71 | | ~ vTerm(v2)) & ! [v2: vTerm] : ! [v3: vTerm] : ( ~ % 21.23/3.71 | (vIfelse(vTrue, v2, v3) = v0) | ~ vTerm(v3) | ~ vTerm(v2)) & % 21.23/3.71 | ! [v2: vTerm] : ( ~ (vIszero(v2) = v0) | ~ vTerm(v2)) & ! [v2: % 21.23/3.71 | vTerm] : ( ~ (vPred(v2) = v0) | ~ vTerm(v2)) & ! [v2: vTerm] : % 21.23/3.71 | ( ~ (vSucc(v2) = v0) | ~ vTerm(v2)))) % 21.23/3.71 | % 21.23/3.71 | ALPHA: (16) implies: % 21.23/3.71 | (17) vsomeTerm(vZero) = all_114_3 % 21.23/3.71 | % 21.23/3.72 | GROUND_INST: instantiating (7) with all_101_0, all_114_3, vZero, simplifying % 21.23/3.72 | with (10), (17) gives: % 21.23/3.72 | (18) all_114_3 = all_101_0 % 21.23/3.72 | % 21.23/3.72 | GROUND_INST: instantiating (reduce-7) with vZero, all_101_0, simplifying with % 21.23/3.72 | (5), (10) gives: % 21.23/3.72 | (19) ? [v0: any] : ? [v1: vTerm] : ? [v2: vTerm] : ? [v3: vOptTerm] : % 21.23/3.72 | (vreduce(v2) = v3 & visNV(vZero) = v0 & vPred(v1) = v2 & vSucc(vZero) % 21.23/3.72 | = v1 & vOptTerm(v3) & vTerm(v2) & vTerm(v1) & ( ~ (v0 = 0) | v3 = % 21.23/3.72 | all_101_0)) % 21.23/3.72 | % 21.23/3.72 | GROUND_INST: instantiating (2) with vZero, all_103_1, simplifying with (5), % 21.23/3.72 | (12) gives: % 21.23/3.72 | (20) all_103_1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & ~ (vFalse = vZero) & ~ % 21.23/3.72 | (vTrue = vZero) & visNV(vZero) = v0) % 21.23/3.72 | % 21.23/3.72 | DELTA: instantiating (19) with fresh symbols all_165_0, all_165_1, all_165_2, % 21.23/3.72 | all_165_3 gives: % 21.23/3.72 | (21) vreduce(all_165_1) = all_165_0 & visNV(vZero) = all_165_3 & % 21.23/3.72 | vPred(all_165_2) = all_165_1 & vSucc(vZero) = all_165_2 & % 21.23/3.72 | vOptTerm(all_165_0) & vTerm(all_165_1) & vTerm(all_165_2) & ( ~ % 21.23/3.72 | (all_165_3 = 0) | all_165_0 = all_101_0) % 21.23/3.72 | % 21.23/3.72 | ALPHA: (21) implies: % 21.23/3.72 | (22) visNV(vZero) = all_165_3 % 21.23/3.72 | % 21.23/3.72 | BETA: splitting (20) gives: % 21.23/3.72 | % 21.23/3.72 | Case 1: % 21.23/3.72 | | % 21.23/3.72 | | (23) all_103_1 = 0 % 21.23/3.72 | | % 21.23/3.72 | | REDUCE: (15), (23) imply: % 21.23/3.72 | | (24) $false % 21.23/3.72 | | % 21.23/3.72 | | CLOSE: (24) is inconsistent. % 21.23/3.72 | | % 21.23/3.72 | Case 2: % 21.23/3.72 | | % 21.23/3.72 | | (25) ? [v0: int] : ( ~ (v0 = 0) & ~ (vFalse = vZero) & ~ (vTrue = % 21.23/3.72 | | vZero) & visNV(vZero) = v0) % 21.23/3.72 | | % 21.23/3.72 | | DELTA: instantiating (25) with fresh symbol all_173_0 gives: % 21.23/3.72 | | (26) ~ (all_173_0 = 0) & ~ (vFalse = vZero) & ~ (vTrue = vZero) & % 21.23/3.72 | | visNV(vZero) = all_173_0 % 21.23/3.72 | | % 21.23/3.72 | | ALPHA: (26) implies: % 21.23/3.72 | | (27) ~ (all_173_0 = 0) % 21.23/3.72 | | (28) visNV(vZero) = all_173_0 % 21.23/3.72 | | % 21.23/3.72 | | GROUND_INST: instantiating (8) with 0, all_173_0, vZero, simplifying with % 21.23/3.72 | | (1), (28) gives: % 21.23/3.72 | | (29) all_173_0 = 0 % 21.23/3.72 | | % 21.23/3.72 | | GROUND_INST: instantiating (8) with all_165_3, all_173_0, vZero, simplifying % 21.23/3.72 | | with (22), (28) gives: % 21.23/3.72 | | (30) all_173_0 = all_165_3 % 21.23/3.72 | | % 21.23/3.72 | | COMBINE_EQS: (29), (30) imply: % 21.23/3.72 | | (31) all_165_3 = 0 % 21.23/3.72 | | % 21.23/3.72 | | REDUCE: (27), (29) imply: % 21.23/3.72 | | (32) $false % 21.23/3.72 | | % 21.23/3.72 | | CLOSE: (32) is inconsistent. % 21.23/3.72 | | % 21.23/3.72 | End of split % 21.23/3.72 | % 21.23/3.72 End of proof % 21.23/3.72 % SZS output end Proof for theBenchmark % 21.23/3.72 % 21.23/3.72 3092ms %------------------------------------------------------------------------------