%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM235_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 : n026.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 28.73s 4.78s % Output : Proof 42.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM235_1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.34 % Computer : n026.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 19:18:38 EDT 2026 % 0.16/0.34 % CPUTime : % 0.49/0.60 ________ _____ % 0.49/0.60 ___ __ \_________(_)________________________________ % 0.49/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.49/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.49/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.49/0.60 % 0.49/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.49/0.60 (2023-06-19) % 0.49/0.60 % 0.49/0.60 (c) Philipp Rümmer, 2009-2023 % 0.49/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.49/0.60 Amanda Stjerna. % 0.49/0.60 Free software under BSD-3-Clause. % 0.49/0.60 % 0.49/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.49/0.60 % 0.49/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.49/0.61 Running up to 7 provers in parallel. % 0.67/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.67/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.67/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.67/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.67/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.67/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.67/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.32/1.57 Prover 1: Preprocessing ... % 5.32/1.57 Prover 4: Preprocessing ... % 5.87/1.60 Prover 6: Preprocessing ... % 5.87/1.60 Prover 5: Preprocessing ... % 5.87/1.60 Prover 3: Preprocessing ... % 5.87/1.60 Prover 2: Preprocessing ... % 5.87/1.60 Prover 0: Preprocessing ... % 13.85/2.73 Prover 1: Warning: ignoring some quantifiers % 13.85/2.77 Prover 3: Warning: ignoring some quantifiers % 13.85/2.79 Prover 1: Constructing countermodel ... % 14.60/2.80 Prover 3: Constructing countermodel ... % 14.60/2.84 Prover 6: Proving ... % 15.17/2.93 Prover 5: Proving ... % 15.17/3.00 Prover 4: Warning: ignoring some quantifiers % 16.04/3.08 Prover 4: Constructing countermodel ... % 16.69/3.14 Prover 0: Proving ... % 18.03/3.36 Prover 2: Proving ... % 28.73/4.78 Prover 0: proved (4161ms) % 28.73/4.78 % 28.73/4.78 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.73/4.78 % 28.73/4.78 Prover 3: stopped % 29.50/4.80 Prover 6: stopped % 29.50/4.80 Prover 2: stopped % 29.50/4.81 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.50/4.81 Prover 5: stopped % 29.50/4.82 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 29.50/4.82 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 29.50/4.82 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 29.50/4.82 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 31.07/5.13 Prover 7: Preprocessing ... % 31.92/5.16 Prover 8: Preprocessing ... % 32.48/5.23 Prover 10: Preprocessing ... % 32.48/5.23 Prover 13: Preprocessing ... % 32.48/5.23 Prover 11: Preprocessing ... % 33.97/5.49 Prover 8: Warning: ignoring some quantifiers % 34.76/5.52 Prover 8: Constructing countermodel ... % 34.76/5.55 Prover 11: Warning: ignoring some quantifiers % 34.76/5.56 Prover 7: Warning: ignoring some quantifiers % 34.76/5.57 Prover 11: Constructing countermodel ... % 34.76/5.58 Prover 7: Constructing countermodel ... % 34.76/5.58 Prover 10: Warning: ignoring some quantifiers % 35.55/5.60 Prover 10: Constructing countermodel ... % 36.32/5.76 Prover 13: Warning: ignoring some quantifiers % 36.32/5.79 Prover 13: Constructing countermodel ... % 41.75/6.48 Prover 4: Found proof (size 73) % 41.75/6.48 Prover 4: proved (5847ms) % 41.75/6.48 Prover 13: stopped % 41.75/6.48 Prover 1: stopped % 41.75/6.48 Prover 11: stopped % 41.75/6.49 Prover 7: stopped % 41.75/6.49 Prover 8: stopped % 41.75/6.50 Prover 10: stopped % 41.75/6.50 % 41.75/6.50 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.75/6.50 % 42.49/6.51 % SZS output start Proof for theBenchmark % 42.49/6.51 Assumptions after simplification: % 42.49/6.51 --------------------------------- % 42.49/6.51 % 42.49/6.51 (DIFF-False-Zero) % 42.49/6.51 ~ (vFalse = vZero) & vTerm(vFalse) & vTerm(vZero) % 42.49/6.51 % 42.49/6.51 (DIFF-True-Zero) % 42.49/6.52 ~ (vTrue = vZero) & vTerm(vTrue) & vTerm(vZero) % 42.49/6.52 % 42.49/6.52 (DIFF-noTerm-someTerm) % 42.49/6.54 vOptTerm(vnoTerm) & ! [v0: vTerm] : ( ~ (vsomeTerm(v0) = vnoTerm) | ~ % 42.49/6.54 vTerm(v0)) % 42.49/6.54 % 42.49/6.54 (Progress-Plus-isNV-True-isNV-True) % 42.49/6.54 vOptTerm(vnoTerm) & vTerm(vt1) & vTerm(vt2) & ? [v0: vTerm] : ? [v1: int] : % 42.49/6.54 ? [v2: vTy] : ( ~ (v1 = 0) & vptchecksimple(v0, v2) = 0 & vreduce(v0) = % 42.49/6.54 vnoTerm & visValue(v0) = v1 & visNV(vt1) = 0 & visNV(vt2) = 0 & vPlus(vt1, % 42.49/6.54 vt2) = v0 & vTy(v2) & vTerm(v0)) % 42.49/6.54 % 42.49/6.54 (TZero_inv) % 42.49/6.54 vTy(vNat) & vTerm(vZero) & ! [v0: vTy] : (v0 = vNat | ~ % 42.49/6.54 (vptchecksimple(vZero, v0) = 0) | ~ vTy(v0)) % 42.49/6.54 % 42.49/6.54 (isNV-0) % 42.49/6.54 visNV(vZero) = 0 & vTerm(vZero) % 42.49/6.54 % 42.49/6.54 (isValue-2) % 42.49/6.55 vTerm(vFalse) & vTerm(vTrue) & ! [v0: vTerm] : ! [v1: any] : (v0 = vFalse | % 42.49/6.55 v0 = vTrue | ~ (visValue(v0) = v1) | ~ vTerm(v0) | ? [v2: any] : % 42.49/6.55 (visNV(v0) = v2 & ( ~ (v2 = 0) | v1 = 0) & ( ~ (v1 = 0) | v2 = 0))) & ! % 42.49/6.55 [v0: vTerm] : ! [v1: any] : (v0 = vFalse | v0 = vTrue | ~ (visNV(v0) = v1) | % 42.49/6.55 ~ vTerm(v0) | ? [v2: any] : (visValue(v0) = v2 & ( ~ (v2 = 0) | v1 = 0) & % 42.49/6.55 ( ~ (v1 = 0) | v2 = 0))) % 42.49/6.55 % 42.49/6.55 (reduce-18) % 42.49/6.55 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vplusop(v0, v1) = v2) % 42.49/6.55 | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: any] : ? [v5: vTerm] % 42.49/6.55 : ? [v6: vOptTerm] : ? [v7: vOptTerm] : (vreduce(v5) = v6 & visNV(v1) = v4 % 42.49/6.55 & visNV(v0) = v3 & vsomeTerm(v2) = v7 & vPlus(v0, v1) = v5 & vOptTerm(v7) % 42.49/6.55 & vOptTerm(v6) & vTerm(v5) & ( ~ (v4 = 0) | ~ (v3 = 0) | v7 = v6))) & ! % 42.49/6.55 [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = v2) | ~ % 42.49/6.55 vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: any] : ? [v5: vOptTerm] : % 42.49/6.55 ? [v6: vTerm] : ? [v7: vOptTerm] : (vreduce(v2) = v5 & vplusop(v0, v1) = % 42.49/6.55 v6 & visNV(v1) = v4 & visNV(v0) = v3 & vsomeTerm(v6) = v7 & vOptTerm(v7) & % 42.49/6.55 vOptTerm(v5) & vTerm(v6) & ( ~ (v4 = 0) | ~ (v3 = 0) | v7 = v5))) % 42.49/6.55 % 42.49/6.55 (reduce-19) % 42.49/6.55 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : ! [v3: vTerm] : ! [v4: % 42.49/6.55 vTerm] : ( ~ (vreduce(v1) = v2) | ~ (vgetTerm(v2) = v3) | ~ (vPlus(v0, v3) % 42.49/6.55 = v4) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v5: any] : ? [v6: any] : ? % 42.49/6.55 [v7: any] : ? [v8: vTerm] : ? [v9: vOptTerm] : ? [v10: vOptTerm] : % 42.49/6.55 (vreduce(v8) = v9 & visSomeTerm(v2) = v7 & visNV(v1) = v6 & visNV(v0) = v5 & % 42.49/6.55 vsomeTerm(v4) = v10 & vPlus(v0, v1) = v8 & vOptTerm(v10) & vOptTerm(v9) & % 42.49/6.55 vTerm(v8) & ( ~ (v7 = 0) | ~ (v5 = 0) | v10 = v9 | v6 = 0))) & ! [v0: % 42.49/6.55 vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = v2) | ~ % 42.49/6.55 vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: any] : ? [v5: vOptTerm] : % 42.49/6.55 ? [v6: any] : ? [v7: vOptTerm] : ? [v8: vTerm] : ? [v9: vTerm] : ? % 42.49/6.55 [v10: vOptTerm] : (vreduce(v2) = v7 & vreduce(v1) = v5 & visSomeTerm(v5) = % 42.49/6.55 v6 & visNV(v1) = v4 & visNV(v0) = v3 & vgetTerm(v5) = v8 & vsomeTerm(v9) = % 42.49/6.55 v10 & vPlus(v0, v8) = v9 & vOptTerm(v10) & vOptTerm(v7) & vOptTerm(v5) & % 42.49/6.55 vTerm(v9) & vTerm(v8) & ( ~ (v6 = 0) | ~ (v3 = 0) | v10 = v7 | v4 = 0))) % 42.49/6.55 % 42.49/6.55 (reduce-20) % 42.49/6.56 vOptTerm(vnoTerm) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ % 42.49/6.56 (vPlus(v0, v1) = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: % 42.49/6.56 any] : ? [v5: vOptTerm] : ? [v6: any] : ? [v7: vOptTerm] : (vreduce(v2) % 42.49/6.56 = v7 & vreduce(v1) = v5 & visSomeTerm(v5) = v6 & visNV(v1) = v4 & % 42.49/6.56 visNV(v0) = v3 & vOptTerm(v7) & vOptTerm(v5) & ( ~ (v3 = 0) | v7 = vnoTerm % 42.49/6.56 | v6 = 0 | v4 = 0))) % 42.49/6.56 % 42.49/6.56 (reduce-21) % 42.49/6.56 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : ! [v3: vTerm] : ! [v4: % 42.49/6.56 vTerm] : ( ~ (vreduce(v0) = v2) | ~ (vgetTerm(v2) = v3) | ~ (vPlus(v3, v1) % 42.49/6.56 = v4) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v5: any] : ? [v6: any] : ? % 42.49/6.56 [v7: vTerm] : ? [v8: vOptTerm] : ? [v9: vOptTerm] : (vreduce(v7) = v8 & % 42.49/6.56 visSomeTerm(v2) = v6 & visNV(v0) = v5 & vsomeTerm(v4) = v9 & vPlus(v0, v1) % 42.49/6.56 = v7 & vOptTerm(v9) & vOptTerm(v8) & vTerm(v7) & ( ~ (v6 = 0) | v9 = v8 | % 42.49/6.56 v5 = 0))) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ % 42.49/6.56 (vPlus(v0, v1) = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: % 42.49/6.56 vOptTerm] : ? [v5: any] : ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 42.49/6.56 vTerm] : ? [v9: vOptTerm] : (vreduce(v2) = v6 & vreduce(v0) = v4 & % 42.49/6.56 visSomeTerm(v4) = v5 & visNV(v0) = v3 & vgetTerm(v4) = v7 & vsomeTerm(v8) % 42.49/6.56 = v9 & vPlus(v7, v1) = v8 & vOptTerm(v9) & vOptTerm(v6) & vOptTerm(v4) & % 42.49/6.56 vTerm(v8) & vTerm(v7) & ( ~ (v5 = 0) | v9 = v6 | v3 = 0))) % 42.49/6.56 % 42.49/6.56 (reduce-22) % 42.49/6.56 vOptTerm(vnoTerm) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ % 42.49/6.56 (vPlus(v0, v1) = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: % 42.49/6.56 vOptTerm] : ? [v5: any] : ? [v6: vOptTerm] : (vreduce(v2) = v6 & % 42.49/6.56 vreduce(v0) = v4 & visSomeTerm(v4) = v5 & visNV(v0) = v3 & vOptTerm(v6) & % 42.49/6.56 vOptTerm(v4) & (v6 = vnoTerm | v5 = 0 | v3 = 0))) % 42.49/6.56 % 42.49/6.56 (function-axioms) % 42.49/6.57 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 42.49/6.57 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 42.49/6.57 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 42.49/6.57 vTy] : ! [v3: vTerm] : (v1 = v0 | ~ (vptchecksimple(v3, v2) = v1) | ~ % 42.49/6.57 (vptchecksimple(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: % 42.49/6.57 vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ % 42.49/6.57 (vplusop(v3, v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : % 42.49/6.57 ! [v3: vTerm] : (v1 = v0 | ~ (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) % 42.49/6.57 & ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 42.49/6.57 (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) & ! [v0: MultipleValueBool] : % 42.49/6.57 ! [v1: MultipleValueBool] : ! [v2: vOptTerm] : (v1 = v0 | ~ (visSomeTerm(v2) % 42.49/6.57 = v1) | ~ (visSomeTerm(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 42.49/6.57 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visValue(v2) = v1) | ~ % 42.49/6.57 (visValue(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 42.49/6.57 MultipleValueBool] : ! [v2: vTerm] : (v1 = v0 | ~ (visNV(v2) = v1) | ~ % 42.49/6.57 (visNV(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 42.49/6.57 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 42.49/6.57 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 42.49/6.57 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 42.49/6.57 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 42.49/6.57 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 42.49/6.57 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 42.49/6.57 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 42.49/6.57 % 42.49/6.57 Further assumptions not needed in the proof: % 42.49/6.57 -------------------------------------------- % 42.49/6.57 DIFF-B-Nat, DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, % 42.49/6.57 DIFF-False-Pred, DIFF-False-Succ, DIFF-Ifelse-Iszero, DIFF-Ifelse-Plus, % 42.49/6.57 DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, DIFF-Iszero-Plus, % 42.49/6.57 DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, DIFF-Succ-Plus, % 42.49/6.57 DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, DIFF-True-Iszero, % 42.49/6.57 DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, DIFF-Zero-Iszero, % 42.49/6.57 DIFF-Zero-Plus, DIFF-Zero-Pred, DIFF-Zero-Succ, EQ-Ifelse, EQ-Iszero, EQ-Plus, % 42.49/6.57 EQ-Pred, EQ-Succ, EQ-someTerm, PlusPreservation, Progress-Plus-IH0, % 42.49/6.57 Progress-Plus-IH1, TPlus, TPlus_inv0, TPlus_inv1, TPlus_inv2, TPred, TPred_inv1, % 42.49/6.57 TPred_inv2, TSucc, TSucc_inv1, TSucc_inv2, TZero, Tfalse, Tif, Tif_inv1, % 42.49/6.57 Tif_inv2, Tif_inv3, Tiszero, Tiszero_inv1, Tiszero_inv2, Ttrue, dom-OptTerm, % 42.49/6.57 dom-Term, dom-Ty, getTerm-0, isNV-1, isNV-2, isNV-false-INV, isNV-true-INV, % 42.49/6.57 isNVisNat, isSomeTerm-0, isSomeTerm-1, isSomeTerm-false-INV, % 42.49/6.57 isSomeTerm-true-INV, isValue-0, isValue-1, isValue-false-INV, isValue-true-INV, % 42.49/6.57 plusop-0, plusop-1, plusop-2, plusop-INV, reduce-0, reduce-1, reduce-10, % 42.49/6.57 reduce-11, reduce-12, reduce-13, reduce-14, reduce-15, reduce-16, reduce-17, % 42.49/6.57 reduce-2, reduce-23, reduce-3, reduce-4, reduce-5, reduce-6, reduce-7, reduce-8, % 42.49/6.57 reduce-9, reduce-INV % 42.49/6.57 % 42.49/6.57 Those formulas are unsatisfiable: % 42.49/6.57 --------------------------------- % 42.49/6.57 % 42.49/6.57 Begin of proof % 42.49/6.57 | % 42.49/6.57 | ALPHA: (DIFF-True-Zero) implies: % 42.49/6.57 | (1) ~ (vTrue = vZero) % 42.49/6.57 | % 42.49/6.57 | ALPHA: (DIFF-False-Zero) implies: % 42.49/6.57 | (2) ~ (vFalse = vZero) % 42.49/6.57 | % 42.49/6.57 | ALPHA: (DIFF-noTerm-someTerm) implies: % 42.49/6.57 | (3) ! [v0: vTerm] : ( ~ (vsomeTerm(v0) = vnoTerm) | ~ vTerm(v0)) % 42.49/6.57 | % 42.49/6.57 | ALPHA: (isNV-0) implies: % 42.49/6.57 | (4) visNV(vZero) = 0 % 42.49/6.57 | % 42.49/6.57 | ALPHA: (isValue-2) implies: % 42.49/6.57 | (5) ! [v0: vTerm] : ! [v1: any] : (v0 = vFalse | v0 = vTrue | ~ % 42.49/6.57 | (visNV(v0) = v1) | ~ vTerm(v0) | ? [v2: any] : (visValue(v0) = v2 & % 42.49/6.57 | ( ~ (v2 = 0) | v1 = 0) & ( ~ (v1 = 0) | v2 = 0))) % 42.49/6.57 | % 42.49/6.57 | ALPHA: (reduce-18) implies: % 42.49/6.57 | (6) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = % 42.49/6.57 | v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: any] : % 42.49/6.57 | ? [v5: vOptTerm] : ? [v6: vTerm] : ? [v7: vOptTerm] : (vreduce(v2) % 42.49/6.57 | = v5 & vplusop(v0, v1) = v6 & visNV(v1) = v4 & visNV(v0) = v3 & % 42.49/6.57 | vsomeTerm(v6) = v7 & vOptTerm(v7) & vOptTerm(v5) & vTerm(v6) & ( ~ % 42.49/6.57 | (v4 = 0) | ~ (v3 = 0) | v7 = v5))) % 42.49/6.57 | % 42.49/6.57 | ALPHA: (reduce-19) implies: % 42.49/6.58 | (7) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = % 42.49/6.58 | v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: any] : % 42.49/6.58 | ? [v5: vOptTerm] : ? [v6: any] : ? [v7: vOptTerm] : ? [v8: vTerm] % 42.49/6.58 | : ? [v9: vTerm] : ? [v10: vOptTerm] : (vreduce(v2) = v7 & % 42.49/6.58 | vreduce(v1) = v5 & visSomeTerm(v5) = v6 & visNV(v1) = v4 & % 42.49/6.58 | visNV(v0) = v3 & vgetTerm(v5) = v8 & vsomeTerm(v9) = v10 & % 42.49/6.58 | vPlus(v0, v8) = v9 & vOptTerm(v10) & vOptTerm(v7) & vOptTerm(v5) & % 42.49/6.58 | vTerm(v9) & vTerm(v8) & ( ~ (v6 = 0) | ~ (v3 = 0) | v10 = v7 | v4 % 42.49/6.58 | = 0))) % 42.49/6.58 | % 42.49/6.58 | ALPHA: (reduce-20) implies: % 42.49/6.58 | (8) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = % 42.49/6.58 | v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: any] : % 42.49/6.58 | ? [v5: vOptTerm] : ? [v6: any] : ? [v7: vOptTerm] : (vreduce(v2) = % 42.49/6.58 | v7 & vreduce(v1) = v5 & visSomeTerm(v5) = v6 & visNV(v1) = v4 & % 42.49/6.58 | visNV(v0) = v3 & vOptTerm(v7) & vOptTerm(v5) & ( ~ (v3 = 0) | v7 = % 42.49/6.58 | vnoTerm | v6 = 0 | v4 = 0))) % 42.49/6.58 | % 42.49/6.58 | ALPHA: (reduce-21) implies: % 42.49/6.58 | (9) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) = % 42.49/6.58 | v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: % 42.49/6.58 | vOptTerm] : ? [v5: any] : ? [v6: vOptTerm] : ? [v7: vTerm] : ? % 42.49/6.58 | [v8: vTerm] : ? [v9: vOptTerm] : (vreduce(v2) = v6 & vreduce(v0) = % 42.49/6.58 | v4 & visSomeTerm(v4) = v5 & visNV(v0) = v3 & vgetTerm(v4) = v7 & % 42.49/6.58 | vsomeTerm(v8) = v9 & vPlus(v7, v1) = v8 & vOptTerm(v9) & % 42.49/6.58 | vOptTerm(v6) & vOptTerm(v4) & vTerm(v8) & vTerm(v7) & ( ~ (v5 = 0) % 42.49/6.58 | | v9 = v6 | v3 = 0))) % 42.49/6.58 | % 42.49/6.58 | ALPHA: (reduce-22) implies: % 42.49/6.58 | (10) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, v1) % 42.49/6.58 | = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ? [v3: any] : ? [v4: % 42.49/6.58 | vOptTerm] : ? [v5: any] : ? [v6: vOptTerm] : (vreduce(v2) = v6 & % 42.49/6.58 | vreduce(v0) = v4 & visSomeTerm(v4) = v5 & visNV(v0) = v3 & % 42.49/6.58 | vOptTerm(v6) & vOptTerm(v4) & (v6 = vnoTerm | v5 = 0 | v3 = 0))) % 42.49/6.58 | % 42.49/6.58 | ALPHA: (TZero_inv) implies: % 42.49/6.58 | (11) vTerm(vZero) % 42.49/6.58 | % 42.49/6.58 | ALPHA: (Progress-Plus-isNV-True-isNV-True) implies: % 42.49/6.58 | (12) vTerm(vt2) % 42.49/6.58 | (13) vTerm(vt1) % 42.49/6.58 | (14) ? [v0: vTerm] : ? [v1: int] : ? [v2: vTy] : ( ~ (v1 = 0) & % 42.49/6.58 | vptchecksimple(v0, v2) = 0 & vreduce(v0) = vnoTerm & visValue(v0) = % 42.49/6.58 | v1 & visNV(vt1) = 0 & visNV(vt2) = 0 & vPlus(vt1, vt2) = v0 & % 42.49/6.58 | vTy(v2) & vTerm(v0)) % 42.49/6.58 | % 42.49/6.58 | ALPHA: (function-axioms) implies: % 42.49/6.58 | (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 42.49/6.58 | vTerm] : (v1 = v0 | ~ (visNV(v2) = v1) | ~ (visNV(v2) = v0)) % 42.49/6.58 | (16) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 42.49/6.58 | (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) % 42.49/6.58 | % 42.49/6.59 | DELTA: instantiating (14) with fresh symbols all_111_0, all_111_1, all_111_2 % 42.49/6.59 | gives: % 42.49/6.59 | (17) ~ (all_111_1 = 0) & vptchecksimple(all_111_2, all_111_0) = 0 & % 42.49/6.59 | vreduce(all_111_2) = vnoTerm & visValue(all_111_2) = all_111_1 & % 42.49/6.59 | visNV(vt1) = 0 & visNV(vt2) = 0 & vPlus(vt1, vt2) = all_111_2 & % 42.49/6.59 | vTy(all_111_0) & vTerm(all_111_2) % 42.49/6.59 | % 42.49/6.59 | ALPHA: (17) implies: % 42.49/6.59 | (18) vPlus(vt1, vt2) = all_111_2 % 42.49/6.59 | (19) visNV(vt2) = 0 % 42.49/6.59 | (20) visNV(vt1) = 0 % 42.49/6.59 | (21) vreduce(all_111_2) = vnoTerm % 42.49/6.59 | % 42.49/6.59 | GROUND_INST: instantiating (7) with vt1, vt2, all_111_2, simplifying with % 42.49/6.59 | (12), (13), (18) gives: % 42.49/6.59 | (22) ? [v0: any] : ? [v1: any] : ? [v2: vOptTerm] : ? [v3: any] : ? % 42.49/6.59 | [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : ? [v7: vOptTerm] : % 42.49/6.59 | (vreduce(all_111_2) = v4 & vreduce(vt2) = v2 & visSomeTerm(v2) = v3 & % 42.49/6.59 | visNV(vt1) = v0 & visNV(vt2) = v1 & vgetTerm(v2) = v5 & % 42.49/6.59 | vsomeTerm(v6) = v7 & vPlus(vt1, v5) = v6 & vOptTerm(v7) & % 42.49/6.59 | vOptTerm(v4) & vOptTerm(v2) & vTerm(v6) & vTerm(v5) & ( ~ (v3 = 0) | % 42.49/6.59 | ~ (v0 = 0) | v7 = v4 | v1 = 0)) % 42.49/6.59 | % 42.49/6.59 | GROUND_INST: instantiating (9) with vt1, vt2, all_111_2, simplifying with % 42.49/6.59 | (12), (13), (18) gives: % 42.49/6.59 | (23) ? [v0: any] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: vOptTerm] : % 42.49/6.59 | ? [v4: vTerm] : ? [v5: vTerm] : ? [v6: vOptTerm] : % 42.49/6.59 | (vreduce(all_111_2) = v3 & vreduce(vt1) = v1 & visSomeTerm(v1) = v2 & % 42.49/6.59 | visNV(vt1) = v0 & vgetTerm(v1) = v4 & vsomeTerm(v5) = v6 & vPlus(v4, % 42.49/6.59 | vt2) = v5 & vOptTerm(v6) & vOptTerm(v3) & vOptTerm(v1) & vTerm(v5) % 42.49/6.59 | & vTerm(v4) & ( ~ (v2 = 0) | v6 = v3 | v0 = 0)) % 42.49/6.59 | % 42.49/6.59 | GROUND_INST: instantiating (8) with vt1, vt2, all_111_2, simplifying with % 42.49/6.59 | (12), (13), (18) gives: % 42.49/6.59 | (24) ? [v0: any] : ? [v1: any] : ? [v2: vOptTerm] : ? [v3: any] : ? % 42.49/6.59 | [v4: vOptTerm] : (vreduce(all_111_2) = v4 & vreduce(vt2) = v2 & % 42.49/6.59 | visSomeTerm(v2) = v3 & visNV(vt1) = v0 & visNV(vt2) = v1 & % 42.49/6.59 | vOptTerm(v4) & vOptTerm(v2) & ( ~ (v0 = 0) | v4 = vnoTerm | v3 = 0 | % 42.49/6.59 | v1 = 0)) % 42.49/6.59 | % 42.49/6.59 | GROUND_INST: instantiating (6) with vt1, vt2, all_111_2, simplifying with % 42.49/6.59 | (12), (13), (18) gives: % 42.49/6.59 | (25) ? [v0: any] : ? [v1: any] : ? [v2: vOptTerm] : ? [v3: vTerm] : ? % 42.49/6.59 | [v4: vOptTerm] : (vreduce(all_111_2) = v2 & vplusop(vt1, vt2) = v3 & % 42.49/6.59 | visNV(vt1) = v0 & visNV(vt2) = v1 & vsomeTerm(v3) = v4 & % 42.49/6.59 | vOptTerm(v4) & vOptTerm(v2) & vTerm(v3) & ( ~ (v1 = 0) | ~ (v0 = 0) % 42.49/6.59 | | v4 = v2)) % 42.49/6.59 | % 42.49/6.59 | GROUND_INST: instantiating (10) with vt1, vt2, all_111_2, simplifying with % 42.49/6.59 | (12), (13), (18) gives: % 42.49/6.60 | (26) ? [v0: any] : ? [v1: vOptTerm] : ? [v2: any] : ? [v3: vOptTerm] : % 42.49/6.60 | (vreduce(all_111_2) = v3 & vreduce(vt1) = v1 & visSomeTerm(v1) = v2 & % 42.49/6.60 | visNV(vt1) = v0 & vOptTerm(v3) & vOptTerm(v1) & (v3 = vnoTerm | v2 = % 42.49/6.60 | 0 | v0 = 0)) % 42.49/6.60 | % 42.49/6.60 | GROUND_INST: instantiating (5) with vZero, 0, simplifying with (4), (11) % 42.49/6.60 | gives: % 42.49/6.60 | (27) vFalse = vZero | vTrue = vZero | visValue(vZero) = 0 % 42.49/6.60 | % 42.49/6.60 | DELTA: instantiating (26) with fresh symbols all_183_0, all_183_1, all_183_2, % 42.49/6.60 | all_183_3 gives: % 42.98/6.60 | (28) vreduce(all_111_2) = all_183_0 & vreduce(vt1) = all_183_2 & % 42.98/6.60 | visSomeTerm(all_183_2) = all_183_1 & visNV(vt1) = all_183_3 & % 42.98/6.60 | vOptTerm(all_183_0) & vOptTerm(all_183_2) & (all_183_0 = vnoTerm | % 42.98/6.60 | all_183_1 = 0 | all_183_3 = 0) % 42.98/6.60 | % 42.98/6.60 | ALPHA: (28) implies: % 42.98/6.60 | (29) visNV(vt1) = all_183_3 % 42.98/6.60 | % 42.98/6.60 | DELTA: instantiating (25) with fresh symbols all_189_0, all_189_1, all_189_2, % 42.98/6.60 | all_189_3, all_189_4 gives: % 42.98/6.60 | (30) vreduce(all_111_2) = all_189_2 & vplusop(vt1, vt2) = all_189_1 & % 42.98/6.60 | visNV(vt1) = all_189_4 & visNV(vt2) = all_189_3 & vsomeTerm(all_189_1) % 42.98/6.60 | = all_189_0 & vOptTerm(all_189_0) & vOptTerm(all_189_2) & % 42.98/6.60 | vTerm(all_189_1) & ( ~ (all_189_3 = 0) | ~ (all_189_4 = 0) | % 42.98/6.60 | all_189_0 = all_189_2) % 42.98/6.60 | % 42.98/6.60 | ALPHA: (30) implies: % 42.98/6.60 | (31) vTerm(all_189_1) % 42.98/6.60 | (32) vsomeTerm(all_189_1) = all_189_0 % 42.98/6.60 | (33) visNV(vt2) = all_189_3 % 42.98/6.60 | (34) visNV(vt1) = all_189_4 % 42.98/6.60 | (35) vreduce(all_111_2) = all_189_2 % 42.98/6.60 | (36) ~ (all_189_3 = 0) | ~ (all_189_4 = 0) | all_189_0 = all_189_2 % 42.98/6.60 | % 42.98/6.60 | DELTA: instantiating (24) with fresh symbols all_191_0, all_191_1, all_191_2, % 42.98/6.60 | all_191_3, all_191_4 gives: % 42.98/6.60 | (37) vreduce(all_111_2) = all_191_0 & vreduce(vt2) = all_191_2 & % 42.98/6.60 | visSomeTerm(all_191_2) = all_191_1 & visNV(vt1) = all_191_4 & % 42.98/6.60 | visNV(vt2) = all_191_3 & vOptTerm(all_191_0) & vOptTerm(all_191_2) & ( % 42.98/6.60 | ~ (all_191_4 = 0) | all_191_0 = vnoTerm | all_191_1 = 0 | all_191_3 % 42.98/6.60 | = 0) % 42.98/6.60 | % 42.98/6.60 | ALPHA: (37) implies: % 42.98/6.60 | (38) visNV(vt2) = all_191_3 % 42.98/6.60 | (39) visNV(vt1) = all_191_4 % 42.98/6.60 | (40) vreduce(all_111_2) = all_191_0 % 42.98/6.60 | % 42.98/6.60 | DELTA: instantiating (23) with fresh symbols all_203_0, all_203_1, all_203_2, % 42.98/6.60 | all_203_3, all_203_4, all_203_5, all_203_6 gives: % 42.98/6.60 | (41) vreduce(all_111_2) = all_203_3 & vreduce(vt1) = all_203_5 & % 42.98/6.60 | visSomeTerm(all_203_5) = all_203_4 & visNV(vt1) = all_203_6 & % 42.98/6.60 | vgetTerm(all_203_5) = all_203_2 & vsomeTerm(all_203_1) = all_203_0 & % 42.98/6.60 | vPlus(all_203_2, vt2) = all_203_1 & vOptTerm(all_203_0) & % 42.98/6.60 | vOptTerm(all_203_3) & vOptTerm(all_203_5) & vTerm(all_203_1) & % 42.98/6.60 | vTerm(all_203_2) & ( ~ (all_203_4 = 0) | all_203_0 = all_203_3 | % 42.98/6.60 | all_203_6 = 0) % 42.98/6.60 | % 42.98/6.60 | ALPHA: (41) implies: % 42.98/6.60 | (42) visNV(vt1) = all_203_6 % 42.98/6.60 | % 42.98/6.60 | DELTA: instantiating (22) with fresh symbols all_205_0, all_205_1, all_205_2, % 42.98/6.60 | all_205_3, all_205_4, all_205_5, all_205_6, all_205_7 gives: % 42.98/6.60 | (43) vreduce(all_111_2) = all_205_3 & vreduce(vt2) = all_205_5 & % 42.98/6.60 | visSomeTerm(all_205_5) = all_205_4 & visNV(vt1) = all_205_7 & % 42.98/6.60 | visNV(vt2) = all_205_6 & vgetTerm(all_205_5) = all_205_2 & % 42.98/6.60 | vsomeTerm(all_205_1) = all_205_0 & vPlus(vt1, all_205_2) = all_205_1 & % 42.98/6.60 | vOptTerm(all_205_0) & vOptTerm(all_205_3) & vOptTerm(all_205_5) & % 42.98/6.60 | vTerm(all_205_1) & vTerm(all_205_2) & ( ~ (all_205_4 = 0) | ~ % 42.98/6.60 | (all_205_7 = 0) | all_205_0 = all_205_3 | all_205_6 = 0) % 42.98/6.60 | % 42.98/6.60 | ALPHA: (43) implies: % 42.98/6.60 | (44) visNV(vt2) = all_205_6 % 42.98/6.60 | (45) visNV(vt1) = all_205_7 % 42.98/6.60 | % 42.98/6.60 | BETA: splitting (27) gives: % 42.98/6.60 | % 42.98/6.60 | Case 1: % 42.98/6.60 | | % 42.98/6.60 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with 0, all_205_6, vt2, simplifying with % 42.98/6.61 | | (19), (44) gives: % 42.98/6.61 | | (46) all_205_6 = 0 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with all_191_3, all_205_6, vt2, simplifying % 42.98/6.61 | | with (38), (44) gives: % 42.98/6.61 | | (47) all_205_6 = all_191_3 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with all_189_3, all_205_6, vt2, simplifying % 42.98/6.61 | | with (33), (44) gives: % 42.98/6.61 | | (48) all_205_6 = all_189_3 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with 0, all_191_4, vt1, simplifying with % 42.98/6.61 | | (20), (39) gives: % 42.98/6.61 | | (49) all_191_4 = 0 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with all_191_4, all_203_6, vt1, simplifying % 42.98/6.61 | | with (39), (42) gives: % 42.98/6.61 | | (50) all_203_6 = all_191_4 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with all_189_4, all_203_6, vt1, simplifying % 42.98/6.61 | | with (34), (42) gives: % 42.98/6.61 | | (51) all_203_6 = all_189_4 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with all_203_6, all_205_7, vt1, simplifying % 42.98/6.61 | | with (42), (45) gives: % 42.98/6.61 | | (52) all_205_7 = all_203_6 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (15) with all_183_3, all_205_7, vt1, simplifying % 42.98/6.61 | | with (29), (45) gives: % 42.98/6.61 | | (53) all_205_7 = all_183_3 % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (16) with vnoTerm, all_191_0, all_111_2, % 42.98/6.61 | | simplifying with (21), (40) gives: % 42.98/6.61 | | (54) all_191_0 = vnoTerm % 42.98/6.61 | | % 42.98/6.61 | | GROUND_INST: instantiating (16) with all_189_2, all_191_0, all_111_2, % 42.98/6.61 | | simplifying with (35), (40) gives: % 42.98/6.61 | | (55) all_191_0 = all_189_2 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (46), (47) imply: % 42.98/6.61 | | (56) all_191_3 = 0 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (47), (48) imply: % 42.98/6.61 | | (57) all_191_3 = all_189_3 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (52), (53) imply: % 42.98/6.61 | | (58) all_203_6 = all_183_3 % 42.98/6.61 | | % 42.98/6.61 | | SIMP: (58) implies: % 42.98/6.61 | | (59) all_203_6 = all_183_3 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (50), (51) imply: % 42.98/6.61 | | (60) all_191_4 = all_189_4 % 42.98/6.61 | | % 42.98/6.61 | | SIMP: (60) implies: % 42.98/6.61 | | (61) all_191_4 = all_189_4 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (51), (59) imply: % 42.98/6.61 | | (62) all_189_4 = all_183_3 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (54), (55) imply: % 42.98/6.61 | | (63) all_189_2 = vnoTerm % 42.98/6.61 | | % 42.98/6.61 | | SIMP: (63) implies: % 42.98/6.61 | | (64) all_189_2 = vnoTerm % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (56), (57) imply: % 42.98/6.61 | | (65) all_189_3 = 0 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (49), (61) imply: % 42.98/6.61 | | (66) all_189_4 = 0 % 42.98/6.61 | | % 42.98/6.61 | | SIMP: (66) implies: % 42.98/6.61 | | (67) all_189_4 = 0 % 42.98/6.61 | | % 42.98/6.61 | | COMBINE_EQS: (62), (67) imply: % 42.98/6.61 | | (68) all_183_3 = 0 % 42.98/6.61 | | % 42.98/6.61 | | BETA: splitting (36) gives: % 42.98/6.61 | | % 42.98/6.61 | | Case 1: % 42.98/6.61 | | | % 42.98/6.61 | | | (69) ~ (all_189_3 = 0) % 42.98/6.61 | | | % 42.98/6.61 | | | REDUCE: (65), (69) imply: % 42.98/6.61 | | | (70) $false % 42.98/6.61 | | | % 42.98/6.61 | | | CLOSE: (70) is inconsistent. % 42.98/6.61 | | | % 42.98/6.61 | | Case 2: % 42.98/6.61 | | | % 42.98/6.61 | | | (71) ~ (all_189_4 = 0) | all_189_0 = all_189_2 % 42.98/6.61 | | | % 42.98/6.61 | | | BETA: splitting (71) gives: % 42.98/6.61 | | | % 42.98/6.61 | | | Case 1: % 42.98/6.61 | | | | % 42.98/6.61 | | | | (72) ~ (all_189_4 = 0) % 42.98/6.61 | | | | % 42.98/6.61 | | | | REDUCE: (67), (72) imply: % 42.98/6.61 | | | | (73) $false % 42.98/6.61 | | | | % 42.98/6.61 | | | | CLOSE: (73) is inconsistent. % 42.98/6.61 | | | | % 42.98/6.61 | | | Case 2: % 42.98/6.61 | | | | % 42.98/6.61 | | | | (74) all_189_0 = all_189_2 % 42.98/6.61 | | | | % 42.98/6.61 | | | | COMBINE_EQS: (64), (74) imply: % 42.98/6.61 | | | | (75) all_189_0 = vnoTerm % 42.98/6.61 | | | | % 42.98/6.61 | | | | REDUCE: (32), (75) imply: % 42.98/6.61 | | | | (76) vsomeTerm(all_189_1) = vnoTerm % 42.98/6.61 | | | | % 42.98/6.61 | | | | GROUND_INST: instantiating (3) with all_189_1, simplifying with (31), % 42.98/6.61 | | | | (76) gives: % 42.98/6.61 | | | | (77) $false % 42.98/6.62 | | | | % 42.98/6.62 | | | | CLOSE: (77) is inconsistent. % 42.98/6.62 | | | | % 42.98/6.62 | | | End of split % 42.98/6.62 | | | % 42.98/6.62 | | End of split % 42.98/6.62 | | % 42.98/6.62 | Case 2: % 42.98/6.62 | | % 42.98/6.62 | | (78) vFalse = vZero | vTrue = vZero % 42.98/6.62 | | % 42.98/6.62 | | BETA: splitting (78) gives: % 42.98/6.62 | | % 42.98/6.62 | | Case 1: % 42.98/6.62 | | | % 42.98/6.62 | | | (79) vFalse = vZero % 42.98/6.62 | | | % 42.98/6.62 | | | REDUCE: (2), (79) imply: % 42.98/6.62 | | | (80) $false % 42.98/6.62 | | | % 42.98/6.62 | | | CLOSE: (80) is inconsistent. % 42.98/6.62 | | | % 42.98/6.62 | | Case 2: % 42.98/6.62 | | | % 42.98/6.62 | | | (81) vTrue = vZero % 42.98/6.62 | | | % 42.98/6.62 | | | REDUCE: (1), (81) imply: % 42.98/6.62 | | | (82) $false % 42.98/6.62 | | | % 42.98/6.62 | | | CLOSE: (82) is inconsistent. % 42.98/6.62 | | | % 42.98/6.62 | | End of split % 42.98/6.62 | | % 42.98/6.62 | End of split % 42.98/6.62 | % 42.98/6.62 End of proof % 42.98/6.62 % SZS output end Proof for theBenchmark % 42.98/6.62 % 42.98/6.62 6018ms %------------------------------------------------------------------------------